From 733776d5de9e97407f2da3da31132faf9508498a Mon Sep 17 00:00:00 2001 From: jonathan Date: Fri, 7 Jun 2024 22:59:20 +0200 Subject: [PATCH] Add a temporary desugaring layer for names --- .gitignore | 4 - Cargo.lock | 243 ++++++++++++++++++ Cargo.toml | 3 + prism-compiler/programs/ok/church_bools.test | 21 +- prism-compiler/programs/ok/church_nats.test | 17 +- prism-compiler/programs/ok/free3.test | 8 +- prism-compiler/programs/ok/free5.test | 2 +- prism-compiler/programs/ok/id_fun1.test | 4 +- prism-compiler/programs/ok/id_fun2.test | 4 +- prism-compiler/programs/ok/id_fun3.test | 6 +- prism-compiler/programs/ok/id_fun4.test | 4 +- prism-compiler/programs/ok/id_fun5.test | 2 +- prism-compiler/programs/ok/id_fun6.test | 4 +- prism-compiler/programs/ok/id_fun7.test | 4 +- prism-compiler/programs/ok/id_fun8.test | 4 +- prism-compiler/programs/ok/id_fun_type.test | 4 +- prism-compiler/programs/ok/let1.test | 2 +- prism-compiler/programs/ok/let10.test | 8 +- prism-compiler/programs/ok/let11.test | 6 +- prism-compiler/programs/ok/let2.test | 14 +- prism-compiler/programs/ok/let3.test | 6 +- prism-compiler/programs/ok/let4.test | 6 +- prism-compiler/programs/ok/let5.test | 6 +- prism-compiler/programs/ok/let6.test | 4 +- prism-compiler/programs/ok/let7.test | 4 +- prism-compiler/programs/ok/let8.test | 8 +- prism-compiler/programs/ok/let9.test | 8 +- .../type_check_fails/breaks_label_values.test | 2 +- .../programs/type_check_fails/index_oob.test | 1 - .../type_check_fails/infinite_type.test | 2 +- .../type_check_fails/name_undefined.test | 1 + .../programs/type_check_fails/type_type.test | 2 +- .../programs/type_check_fails/weird1.test | 2 +- .../programs/type_check_fails/weird2.test | 2 +- .../programs/type_check_fails/weird4.test | 2 +- .../programs/type_check_fails/weird5.test | 2 +- prism-compiler/resources/grammar | 25 +- prism-compiler/resources/program.pr | 14 +- .../src/desugar/from_action_result.rs | 59 +++++ prism-compiler/src/desugar/mod.rs | 44 ++++ prism-compiler/src/lang/beta_reduce.rs | 3 +- prism-compiler/src/lang/beta_reduce_head.rs | 3 +- prism-compiler/src/lang/display.rs | 3 +- prism-compiler/src/lang/env.rs | 6 +- prism-compiler/src/lang/error.rs | 9 +- prism-compiler/src/lang/from_action_result.rs | 63 ----- prism-compiler/src/lang/from_parse_env.rs | 68 +++++ prism-compiler/src/lang/is_beta_equal.rs | 3 +- prism-compiler/src/lang/mod.rs | 7 +- prism-compiler/src/lang/type_check.rs | 3 +- prism-compiler/src/lib.rs | 1 + prism-compiler/src/parser.rs | 11 +- prism-compiler/tests/beta_reduce.rs | 5 +- prism-compiler/tests/beta_reduce_head.rs | 2 +- prism-compiler/tests/exhaustive.rs | 2 +- prism-compiler/tests/simplify.rs | 2 +- prism-compiler/tests/type_check.rs | 4 +- prism-parser/src/core/recovery.rs | 2 +- 58 files changed, 569 insertions(+), 192 deletions(-) create mode 100644 Cargo.lock delete mode 100644 prism-compiler/programs/type_check_fails/index_oob.test create mode 100644 prism-compiler/programs/type_check_fails/name_undefined.test create mode 100644 prism-compiler/src/desugar/from_action_result.rs create mode 100644 prism-compiler/src/desugar/mod.rs delete mode 100644 prism-compiler/src/lang/from_action_result.rs create mode 100644 prism-compiler/src/lang/from_parse_env.rs diff --git a/.gitignore b/.gitignore index d8739a55..9725e9ae 100644 --- a/.gitignore +++ b/.gitignore @@ -2,10 +2,6 @@ # will have compiled files and executables /target/ -# Remove Cargo.lock from gitignore if creating an executable, leave it for libraries -# More information here https://doc.rust-lang.org/cargo/guide/cargo-toml-vs-cargo-lock.html -Cargo.lock - # These are backup files generated by rustfmt **/*.rs.bk diff --git a/Cargo.lock b/Cargo.lock new file mode 100644 index 00000000..eab0580a --- /dev/null +++ b/Cargo.lock @@ -0,0 +1,243 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "archery" +version = "1.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8967cd1cc9e9e1954f644e14fbd6042fe9a37da96c52a67e44a2ac18261f8561" +dependencies = [ + "static_assertions", + "triomphe", +] + +[[package]] +name = "ariadne" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "44055e597c674aef7cb903b2b9f6e4cba1277ed0d2d61dae7cd52d7ffa81f8e2" +dependencies = [ + "unicode-width", + "yansi", +] + +[[package]] +name = "bincode" +version = "1.3.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b1f45e9417d87227c7a56d22e471c6206462cba514c7590c09aff4cf6d1ddcad" +dependencies = [ + "serde", +] + +[[package]] +name = "by_address" +version = "1.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "64fa3c856b712db6612c019f14756e64e4bcea13337a6b33b696333a9eaa2d06" + +[[package]] +name = "either" +version = "1.12.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3dca9240753cf90908d7e4aac30f630662b02aebaa1b58a3cadabdb23385b58b" + +[[package]] +name = "exhaustive" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c17d918b02c5e21eca6c159d2af826465c29c327677e724abe734d85eac36bb4" +dependencies = [ + "exhaustive_macros", +] + +[[package]] +name = "exhaustive_macros" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5ac620061b89f3ec8650a31c990f2129797a2f89e0ce8b947901df54a9987a47" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "itertools" +version = "0.13.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "413ee7dfc52ee1a4949ceeb7dbc8a33f2d6c088194d9f922fb8318faf1f01186" +dependencies = [ + "either", +] + +[[package]] +name = "itoa" +version = "1.0.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" + +[[package]] +name = "lazy_static" +version = "1.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" + +[[package]] +name = "prism-compiler" +version = "0.1.0" +dependencies = [ + "ariadne", + "exhaustive", + "lazy_static", + "prism-parser", + "rpds", + "test_each_file", +] + +[[package]] +name = "prism-parser" +version = "0.1.0" +dependencies = [ + "ariadne", + "bincode", + "by_address", + "itertools", + "lazy_static", + "serde", + "typed-arena", +] + +[[package]] +name = "prism-parser-bootstrap" +version = "0.1.0" +dependencies = [ + "bincode", + "prism-parser", + "serde", + "serde_json", +] + +[[package]] +name = "proc-macro2" +version = "1.0.85" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "22244ce15aa966053a896d1accb3a6e68469b97c7f33f284b99f0d576879fc23" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.36" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fa76aaf39101c457836aec0ce2316dbdc3ab723cdda1c6bd4e6ad4208acaca7" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "rpds" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a0e15515d3ce3313324d842629ea4905c25a13f81953eadb88f85516f59290a4" +dependencies = [ + "archery", +] + +[[package]] +name = "ryu" +version = "1.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f3cb5ba0dc43242ce17de99c180e96db90b235b8a9fdc9543c96d2209116bd9f" + +[[package]] +name = "serde" +version = "1.0.203" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7253ab4de971e72fb7be983802300c30b5a7f0c2e56fab8abfc6a214307c0094" +dependencies = [ + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.203" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "500cbc0ebeb6f46627f50f3f5811ccf6bf00643be300b4c3eabc0ef55dc5b5ba" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "serde_json" +version = "1.0.117" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "455182ea6142b14f93f4bc5320a2b31c1f266b66a4a5c858b013302a5d8cbfc3" +dependencies = [ + "itoa", + "ryu", + "serde", +] + +[[package]] +name = "static_assertions" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a2eb9349b6444b326872e140eb1cf5e7c522154d69e7a0ffb0fb81c06b37543f" + +[[package]] +name = "syn" +version = "2.0.66" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c42f3f41a2de00b01c0aaad383c5a45241efc8b2d1eda5661812fda5f3cdcff5" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "test_each_file" +version = "0.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0f1a92330478de0709111391059475f7d960692519e2c54c823c662408bab365" +dependencies = [ + "proc-macro2", + "quote", + "syn", + "unicode-ident", +] + +[[package]] +name = "triomphe" +version = "0.1.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1b2cb4fbb9995eeb36ac86fadf24031ccd58f99d6b4b2d7b911db70bddb80d90" + +[[package]] +name = "typed-arena" +version = "2.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6af6ae20167a9ece4bcb41af5b80f8a1f1df981f6391189ce00fd257af04126a" + +[[package]] +name = "unicode-ident" +version = "1.0.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b" + +[[package]] +name = "unicode-width" +version = "0.1.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0336d538f7abc86d282a4189614dfaa90810dfc2c6f6427eaf88e16311dd225d" + +[[package]] +name = "yansi" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cfe53a6657fd280eaa890a3bc59152892ffa3e30101319d168b781ed6529b049" diff --git a/Cargo.toml b/Cargo.toml index d1bcf410..c00d2318 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,6 +3,9 @@ members = ["prism-compiler", "prism-parser", "prism-parser-bootstrap"] default-members = ["prism-compiler", "prism-parser", "prism-parser-bootstrap"] resolver = "2" +[profile.test] +opt-level = 1 + [workspace.package] edition = "2021" version = "0.1.0" diff --git a/prism-compiler/programs/ok/church_bools.test b/prism-compiler/programs/ok/church_bools.test index 1c1b3c92..e03d7ba2 100644 --- a/prism-compiler/programs/ok/church_bools.test +++ b/prism-compiler/programs/ok/church_bools.test @@ -1,20 +1,15 @@ ### Input -// Bool = (T: Type) -> T -> T -> T -let Type -> #0 -> #1 -> #2; -// false (left) -let Type => #0 => #1 => #1; -// true (right) -let Type => #0 => #1 => #0; -// and : Bool -> Bool -> Bool -// = v1:Bool => v2:Bool => T:Type => t1:T => t2:T => (v1 T t1 (v2 T t1 t2)) -let #2 => #3 => Type => #0 => #1 => #4 #2 #1 (#3 #2 #1 #0); +let Bool = (T: Type) -> T -> T -> T; +let false = (T: Type) => (v1: T) => (v2: T) => v1; +let true = (T: Type) => (v1: T) => (v2: T) => v2; -// and true true -#0 #1 #1 +// and : Bool -> Bool -> Bool +let and = (b1: Bool) => (b2: Bool) => (T: Type) => (v1: T) => (v2: T) => b1 T v1 (b2 T v1 v2); +and true true ### Eval -Type => #0 => #1 => #0 +(T: Type) => (_: T) => (v2: T) => v2 ### Type -Type -> #0 -> #1 -> #2 +(T: Type) -> T -> T -> T diff --git a/prism-compiler/programs/ok/church_nats.test b/prism-compiler/programs/ok/church_nats.test index 9a40c1f5..2c5d0417 100644 --- a/prism-compiler/programs/ok/church_nats.test +++ b/prism-compiler/programs/ok/church_nats.test @@ -1,17 +1,14 @@ ### Input -// Nat : (T:Type) -> zero:T -> succ:(T->T) -> T -let Type -> #0 -> (#1 -> #2) -> #2; -// zero : Nat -let Type => #0 => (#1 -> #2) => #1; +let Nat = T: Type -> T -> (T -> T) -> T; +let zero = T: Type => z: T => s: (T -> T) => z; // add1 : Nat -> Nat -// = (v:Nat) => (T:Type) => zero:T => succ:(T->T) => succ (v T zero succ) -let #1 => Type => #0 => (#1 -> #2) => #0 (#3 #2 #1 #0); -// add1 zero -#0 #1 +let add1 = n: Nat => T: Type => z: T => s: (T -> T) => s (n T z s); + +add1 zero ### Eval -Type => #0 => (#1 -> #2) => #0 #1 +T: Type => z: T => s: (T -> T) => s z ### Type -Type -> #0 -> (#1 -> #2) -> #2 +T: Type -> T -> (T -> T) -> T diff --git a/prism-compiler/programs/ok/free3.test b/prism-compiler/programs/ok/free3.test index 5f192b8b..7b558a02 100644 --- a/prism-compiler/programs/ok/free3.test +++ b/prism-compiler/programs/ok/free3.test @@ -1,10 +1,10 @@ ### Input -let _; -#0 +let v = _; +v ### Eval -let _; -#0 +let v = _; +v ### Type _ \ No newline at end of file diff --git a/prism-compiler/programs/ok/free5.test b/prism-compiler/programs/ok/free5.test index 534b3046..d274859c 100644 --- a/prism-compiler/programs/ok/free5.test +++ b/prism-compiler/programs/ok/free5.test @@ -1,5 +1,5 @@ ### Input -(Type => _) Type +(_: Type => _) Type ### Eval _ diff --git a/prism-compiler/programs/ok/id_fun1.test b/prism-compiler/programs/ok/id_fun1.test index f8d7debb..c7d71430 100644 --- a/prism-compiler/programs/ok/id_fun1.test +++ b/prism-compiler/programs/ok/id_fun1.test @@ -1,8 +1,8 @@ ### Input -Type => #0 +v: Type => v ### Eval -Type => #0 +v: Type => v ### Type Type -> Type \ No newline at end of file diff --git a/prism-compiler/programs/ok/id_fun2.test b/prism-compiler/programs/ok/id_fun2.test index e7a6e493..d55865aa 100644 --- a/prism-compiler/programs/ok/id_fun2.test +++ b/prism-compiler/programs/ok/id_fun2.test @@ -1,8 +1,8 @@ ### Input -(Type -> Type) => #0 Type +f: (Type -> Type) => f Type ### Eval -(Type -> Type) => #0 Type +f: (Type -> Type) => f Type ### Type (Type -> Type) -> Type \ No newline at end of file diff --git a/prism-compiler/programs/ok/id_fun3.test b/prism-compiler/programs/ok/id_fun3.test index ed263092..42e50597 100644 --- a/prism-compiler/programs/ok/id_fun3.test +++ b/prism-compiler/programs/ok/id_fun3.test @@ -1,8 +1,8 @@ ### Input -Type => #0 => #0 +T: Type => v: T => v ### Eval -Type => #0 => #0 +T: Type => v: T => v ### Type -Type -> #0 -> #1 \ No newline at end of file +T: Type -> T -> T \ No newline at end of file diff --git a/prism-compiler/programs/ok/id_fun4.test b/prism-compiler/programs/ok/id_fun4.test index d0b132b9..522d48f7 100644 --- a/prism-compiler/programs/ok/id_fun4.test +++ b/prism-compiler/programs/ok/id_fun4.test @@ -1,8 +1,8 @@ ### Input -(Type => #0 => #0) Type +(T: Type => v: T => v) Type ### Eval -Type => #0 +v: Type => v ### Type Type -> Type \ No newline at end of file diff --git a/prism-compiler/programs/ok/id_fun5.test b/prism-compiler/programs/ok/id_fun5.test index b9b35dbd..c1f8b543 100644 --- a/prism-compiler/programs/ok/id_fun5.test +++ b/prism-compiler/programs/ok/id_fun5.test @@ -1,5 +1,5 @@ ### Input -(Type => #0 => #0) Type Type +(T: Type => v: T => v) Type Type ### Eval Type diff --git a/prism-compiler/programs/ok/id_fun6.test b/prism-compiler/programs/ok/id_fun6.test index b7c0dac3..97e257f5 100644 --- a/prism-compiler/programs/ok/id_fun6.test +++ b/prism-compiler/programs/ok/id_fun6.test @@ -1,8 +1,8 @@ ### Input -(Type => #0 => #0) (Type -> Type) +(T: Type => v: T => v) (Type -> Type) ### Eval -(Type -> Type) => #0 +f: (Type -> Type) => f ### Type (Type -> Type) -> (Type -> Type) \ No newline at end of file diff --git a/prism-compiler/programs/ok/id_fun7.test b/prism-compiler/programs/ok/id_fun7.test index e1914d0a..11196d2b 100644 --- a/prism-compiler/programs/ok/id_fun7.test +++ b/prism-compiler/programs/ok/id_fun7.test @@ -1,8 +1,8 @@ ### Input -(Type => #0 => #0) (Type -> Type) (Type => #0) +(T: Type => v: T => v) (Type -> Type) (v: Type => v) ### Eval -(Type => #0) +(v: Type => v) ### Type (Type -> Type) \ No newline at end of file diff --git a/prism-compiler/programs/ok/id_fun8.test b/prism-compiler/programs/ok/id_fun8.test index 0f8b16a7..657ef0be 100644 --- a/prism-compiler/programs/ok/id_fun8.test +++ b/prism-compiler/programs/ok/id_fun8.test @@ -1,8 +1,8 @@ ### Input -((Type -> Type) => #0) (Type => #0) +(f: (Type -> Type) => f) (v: Type => v) ### Eval -Type => #0 +v: Type => v ### Type Type -> Type \ No newline at end of file diff --git a/prism-compiler/programs/ok/id_fun_type.test b/prism-compiler/programs/ok/id_fun_type.test index 8233081d..226b6733 100644 --- a/prism-compiler/programs/ok/id_fun_type.test +++ b/prism-compiler/programs/ok/id_fun_type.test @@ -1,8 +1,8 @@ ### Input -Type -> #0 -> #1 +T: Type -> T -> T ### Eval -Type -> #0 -> #1 +T: Type -> T -> T ### Type Type diff --git a/prism-compiler/programs/ok/let1.test b/prism-compiler/programs/ok/let1.test index 44a94500..4d01acc1 100644 --- a/prism-compiler/programs/ok/let1.test +++ b/prism-compiler/programs/ok/let1.test @@ -1,5 +1,5 @@ ### Input -let Type; #0 +let v = Type; v ### Eval Type diff --git a/prism-compiler/programs/ok/let10.test b/prism-compiler/programs/ok/let10.test index 2877b251..6b7498e8 100644 --- a/prism-compiler/programs/ok/let10.test +++ b/prism-compiler/programs/ok/let10.test @@ -1,10 +1,10 @@ ### Input -let Type -> Type; -let #0 => #0; -#0 +let v = Type -> Type; +let w = x: v => x; +w ### Eval -(Type -> Type) => #0 +v: (Type -> Type) => v ### Type (Type -> Type) -> (Type -> Type) diff --git a/prism-compiler/programs/ok/let11.test b/prism-compiler/programs/ok/let11.test index d18a68c6..adda68ce 100644 --- a/prism-compiler/programs/ok/let11.test +++ b/prism-compiler/programs/ok/let11.test @@ -1,11 +1,11 @@ ### Input -(Type -> #0 -> (#1 -> #2) -> #2) => Type => #0 => (#1 -> #2) => #3 #2 #1 +a: (b: Type -> b -> (b -> b) -> b) => c: Type => d: c => e: (c -> c) => a c d ### Eval -(Type -> #0 -> (#1 -> #2) -> #2) => Type => #0 => (#1 -> #2) => #3 #2 #1 +a: (b: Type -> b -> (b -> b) -> b) => c: Type => d: c => e: (c -> c) => a c d ### Type -(Type -> #0 -> (#1 -> #2) -> #2) -> Type -> #0 -> (#1 -> #2) -> (#2 -> #3) -> #3 +a: (b: Type -> b -> (b -> b) -> b) -> c: Type -> c -> (c -> c) -> (c -> c) -> c diff --git a/prism-compiler/programs/ok/let2.test b/prism-compiler/programs/ok/let2.test index e2964483..e7599045 100644 --- a/prism-compiler/programs/ok/let2.test +++ b/prism-compiler/programs/ok/let2.test @@ -1,11 +1,11 @@ ### Input -let Type; -let Type -> Type; -let Type; -let #1; -let Type; -let Type; -#2 +let _ = Type; +let v = Type -> Type; +let _ = Type; +let w = v; +let _ = Type; +let _ = Type; +w ### Eval Type -> Type diff --git a/prism-compiler/programs/ok/let3.test b/prism-compiler/programs/ok/let3.test index 36a90492..28de00b7 100644 --- a/prism-compiler/programs/ok/let3.test +++ b/prism-compiler/programs/ok/let3.test @@ -1,7 +1,7 @@ ### Input -let Type -> Type; -let #0; -#0 +let v = Type -> Type; +let w = v; +w ### Eval Type -> Type diff --git a/prism-compiler/programs/ok/let4.test b/prism-compiler/programs/ok/let4.test index 3313298b..f337a6da 100644 --- a/prism-compiler/programs/ok/let4.test +++ b/prism-compiler/programs/ok/let4.test @@ -1,9 +1,9 @@ ### Input -let Type; -#0 => #0 +let T = Type; +v: T => v ### Eval -Type => #0 +v: Type => v ### Type Type -> Type diff --git a/prism-compiler/programs/ok/let5.test b/prism-compiler/programs/ok/let5.test index b9c20dbb..457d6e01 100644 --- a/prism-compiler/programs/ok/let5.test +++ b/prism-compiler/programs/ok/let5.test @@ -1,9 +1,9 @@ ### Input -let Type => #0; -#0 +let v = w: Type => w; +v ### Eval -Type => #0 +w: Type => w ### Type Type -> Type diff --git a/prism-compiler/programs/ok/let6.test b/prism-compiler/programs/ok/let6.test index 72a75c9c..6c3c36e6 100644 --- a/prism-compiler/programs/ok/let6.test +++ b/prism-compiler/programs/ok/let6.test @@ -1,6 +1,6 @@ ### Input -let Type => #0; -#0 Type +let v = w: Type => w; +v Type ### Eval Type diff --git a/prism-compiler/programs/ok/let7.test b/prism-compiler/programs/ok/let7.test index 5551bc4e..59eb2f8e 100644 --- a/prism-compiler/programs/ok/let7.test +++ b/prism-compiler/programs/ok/let7.test @@ -1,6 +1,6 @@ ### Input -let (Type => #0) Type; -#0 +let v = (w: Type => w) Type; +v ### Eval Type diff --git a/prism-compiler/programs/ok/let8.test b/prism-compiler/programs/ok/let8.test index a0200269..f702c678 100644 --- a/prism-compiler/programs/ok/let8.test +++ b/prism-compiler/programs/ok/let8.test @@ -1,10 +1,10 @@ ### Input -let (Type => #0) Type; -let Type -> Type; -#1 => #0 +let v = (w: Type => w) Type; +let x = Type -> Type; +y: v => y ### Eval -Type => #0 +w: Type => w ### Type Type -> Type diff --git a/prism-compiler/programs/ok/let9.test b/prism-compiler/programs/ok/let9.test index 07414c5e..dda3d25e 100644 --- a/prism-compiler/programs/ok/let9.test +++ b/prism-compiler/programs/ok/let9.test @@ -1,10 +1,10 @@ ### Input -let Type => #0; -let Type -> Type; -(#0 => #0) #1 +let v = w: Type => w; +let x = Type -> Type; +(y: x => y) v ### Eval -Type => #0 +v: Type => v ### Type Type -> Type diff --git a/prism-compiler/programs/type_check_fails/breaks_label_values.test b/prism-compiler/programs/type_check_fails/breaks_label_values.test index 2af2c806..2ca9f9cc 100644 --- a/prism-compiler/programs/type_check_fails/breaks_label_values.test +++ b/prism-compiler/programs/type_check_fails/breaks_label_values.test @@ -1 +1 @@ -_ -> #0 (#0 (#0 Type Type)) \ No newline at end of file +v: _ -> v (v (v Type Type)) \ No newline at end of file diff --git a/prism-compiler/programs/type_check_fails/index_oob.test b/prism-compiler/programs/type_check_fails/index_oob.test deleted file mode 100644 index a894faa4..00000000 --- a/prism-compiler/programs/type_check_fails/index_oob.test +++ /dev/null @@ -1 +0,0 @@ -#0 \ No newline at end of file diff --git a/prism-compiler/programs/type_check_fails/infinite_type.test b/prism-compiler/programs/type_check_fails/infinite_type.test index f6109f15..e7f969ac 100644 --- a/prism-compiler/programs/type_check_fails/infinite_type.test +++ b/prism-compiler/programs/type_check_fails/infinite_type.test @@ -1 +1 @@ -_ -> #0 #0 (#0 Type) \ No newline at end of file +v: _ -> v v (v Type) \ No newline at end of file diff --git a/prism-compiler/programs/type_check_fails/name_undefined.test b/prism-compiler/programs/type_check_fails/name_undefined.test new file mode 100644 index 00000000..c1b0730e --- /dev/null +++ b/prism-compiler/programs/type_check_fails/name_undefined.test @@ -0,0 +1 @@ +x \ No newline at end of file diff --git a/prism-compiler/programs/type_check_fails/type_type.test b/prism-compiler/programs/type_check_fails/type_type.test index 02b5527a..35ab272b 100644 --- a/prism-compiler/programs/type_check_fails/type_type.test +++ b/prism-compiler/programs/type_check_fails/type_type.test @@ -1 +1 @@ -Type Type -> #0 \ No newline at end of file +v: Type Type -> v \ No newline at end of file diff --git a/prism-compiler/programs/type_check_fails/weird1.test b/prism-compiler/programs/type_check_fails/weird1.test index 0d9d0001..04a49c91 100644 --- a/prism-compiler/programs/type_check_fails/weird1.test +++ b/prism-compiler/programs/type_check_fails/weird1.test @@ -1 +1 @@ -(Type => Type) -> #0 Type +v: (_: Type => Type) -> v Type diff --git a/prism-compiler/programs/type_check_fails/weird2.test b/prism-compiler/programs/type_check_fails/weird2.test index 04f3e8fd..72b260ea 100644 --- a/prism-compiler/programs/type_check_fails/weird2.test +++ b/prism-compiler/programs/type_check_fails/weird2.test @@ -1 +1 @@ -_ -> #0 #0 +v: _ -> v v diff --git a/prism-compiler/programs/type_check_fails/weird4.test b/prism-compiler/programs/type_check_fails/weird4.test index 7b3315df..03b7f6a1 100644 --- a/prism-compiler/programs/type_check_fails/weird4.test +++ b/prism-compiler/programs/type_check_fails/weird4.test @@ -1 +1 @@ -_ -> #0 Type #0 +v: _ -> v Type v diff --git a/prism-compiler/programs/type_check_fails/weird5.test b/prism-compiler/programs/type_check_fails/weird5.test index f1d0b5a1..6af0bdbf 100644 --- a/prism-compiler/programs/type_check_fails/weird5.test +++ b/prism-compiler/programs/type_check_fails/weird5.test @@ -1 +1 @@ -(_ -> #0 Type) -> #0 Type +w: (v: _ -> v Type) -> w Type diff --git a/prism-compiler/resources/grammar b/prism-compiler/resources/grammar index 3ce71aed..bdabe1bc 100644 --- a/prism-compiler/resources/grammar +++ b/prism-compiler/resources/grammar @@ -1,28 +1,26 @@ rule block { b <- "grammar" "{" g:grammar(expr) "}" ";" b:#adapt(g, block); - Let(v, b) <- "let" v:expr ";" b:block; + Let(n, v, b) <- "let" n:identifier "=" v:expr ";" b:block; expr; } rule expr { group fnconstruct { - FnConstruct(t, r) <- t:#next "=>" r:#this; + FnConstruct(n, t, r) <- "(" n:identifier ":" t:#next ")" "=>" r:#this; + FnConstruct(n, t, r) <- n:identifier ":" t:#next "=>" r:#this; } group fntype { - FnType(at, bt) <- at:#next "->" bt:#this; + FnType(n, at, bt) <- "(" n:identifier ":" at:#next ")" "->" bt:#this; + FnType(n, at, bt) <- n:identifier ":" at:#next "->" bt:#this; + FnType("_", at, bt) <- at:#next "->" bt:#this; } group fndestruct { FnDestruct(f, a) <- f:#this " " a:#next; } group base { - t <- "(" t:expr ")"; + t <- "(" t:block ")"; Type() <- "Type"; - Free() <- "_"; - - #[disable_layout] - #[disable_recovery] - #[error("De Bruijn Index")] - DeBruijnIndex(i) <- "#" i:#str([ '0'-'9' ]+); + Variable(n) <- n:identifier; } } @@ -30,3 +28,10 @@ rule layout { [' ' | '\n']; "//" [^'\n']* "\n"; } + +rule identifier { + #[error("Identifier")] + #[disable_layout] + #[disable_recovery] + n <- n:#str([ 'a'-'z' | 'A'-'Z' | '_' ] ['a'-'z' | 'A'-'Z' | '0'-'9' | '_' ]*); +} \ No newline at end of file diff --git a/prism-compiler/resources/program.pr b/prism-compiler/resources/program.pr index 67345d79..ffeab471 100644 --- a/prism-compiler/resources/program.pr +++ b/prism-compiler/resources/program.pr @@ -1 +1,13 @@ -Ty \ No newline at end of file +// Bool = (T: Type) -> T -> T -> T +let Type -> #0 -> #1 -> #2; +// false (left) +let Type => #0 => #1 => #1; +// true (right) +let Type => #0 => #1 => #0; +// and : Bool -> Bool -> Bool +// = v1:Bool => v2:Bool => T:Type => t1:T => t2:T => (v1 T t1 (v2 T t1 t2)) +let #2 => #3 => Type => #0 => #1 => #4 #2 #1 (#3 #2 #1 #0); + +// and true true +#0 #1 #1 + diff --git a/prism-compiler/src/desugar/from_action_result.rs b/prism-compiler/src/desugar/from_action_result.rs new file mode 100644 index 00000000..abae1a58 --- /dev/null +++ b/prism-compiler/src/desugar/from_action_result.rs @@ -0,0 +1,59 @@ +use prism_parser::rule_action::action_result::ActionResult; +use crate::desugar::{ParseEnv, SourceExpr, ParseIndex}; + +impl ParseEnv { + pub fn insert_from_action_result<'grm>( + &mut self, + value: &ActionResult<'_, 'grm>, + program: &str, + ) -> ParseIndex { + let ActionResult::Construct(span, constructor, args) = value else { + unreachable!("Parsing an expression always returns a Construct"); + }; + let inner = match *constructor { + "Type" => { + assert_eq!(args.len(), 0); + SourceExpr::Type + } + "Let" => { + assert_eq!(args.len(), 3); + SourceExpr::Let( + args[0].get_value(program).to_string(), + self.insert_from_action_result(&args[1], program), + self.insert_from_action_result(&args[2], program), + ) + } + "Variable" => { + assert_eq!(args.len(), 1); + SourceExpr::Variable( + args[0].get_value(program).to_string(), + ) + } + "FnType" => { + assert_eq!(args.len(), 3); + SourceExpr::FnType( + args[0].get_value(program).to_string(), + self.insert_from_action_result(&args[1], program), + self.insert_from_action_result(&args[2], program), + ) + } + "FnConstruct" => { + assert_eq!(args.len(), 3); + SourceExpr::FnConstruct( + args[0].get_value(program).to_string(), + self.insert_from_action_result(&args[1], program), + self.insert_from_action_result(&args[2], program), + ) + } + "FnDestruct" => { + assert_eq!(args.len(), 2); + SourceExpr::FnDestruct( + self.insert_from_action_result(&args[0], program), + self.insert_from_action_result(&args[1], program), + ) + } + _ => unreachable!(), + }; + self.store(inner, *span) + } +} diff --git a/prism-compiler/src/desugar/mod.rs b/prism-compiler/src/desugar/mod.rs new file mode 100644 index 00000000..bf4ceab9 --- /dev/null +++ b/prism-compiler/src/desugar/mod.rs @@ -0,0 +1,44 @@ +use prism_parser::core::span::Span; + +pub mod from_action_result; + +#[derive(Default)] +pub struct ParseEnv { + values: Vec, + value_spans: Vec, +} + +#[derive(Copy, Clone, Hash, Eq, PartialEq, Debug)] +pub struct ParseIndex(usize); + +impl ParseIndex { + pub fn index(self) -> usize { + self.0 + } +} + +impl ParseEnv { + pub fn store(&mut self, e: SourceExpr, span: Span) -> ParseIndex { + self.values.push(e); + self.value_spans.push(span); + ParseIndex(self.values.len() - 1) + } + + pub fn values(&self) -> &[SourceExpr] { + &self.values + } + + pub fn value_spans(&self) -> &[Span] { + &self.value_spans + } +} + +#[derive(Clone, Eq, PartialEq)] +pub enum SourceExpr { + Type, + Let(String, ParseIndex, ParseIndex), + Variable(String), + FnType(String, ParseIndex, ParseIndex), + FnConstruct(String, ParseIndex, ParseIndex), + FnDestruct(ParseIndex, ParseIndex), +} diff --git a/prism-compiler/src/lang/beta_reduce.rs b/prism-compiler/src/lang/beta_reduce.rs index 1b950b8e..f1d8ccf0 100644 --- a/prism-compiler/src/lang/beta_reduce.rs +++ b/prism-compiler/src/lang/beta_reduce.rs @@ -1,6 +1,7 @@ use crate::lang::env::{Env, EnvEntry, UniqueVariableId}; -use crate::lang::{PartialExpr, TcEnv, UnionIndex}; +use crate::lang::{PartialExpr, TcEnv}; use std::collections::HashMap; +use crate::lang::UnionIndex; impl TcEnv { pub fn beta_reduce(&mut self, i: UnionIndex) -> UnionIndex { diff --git a/prism-compiler/src/lang/beta_reduce_head.rs b/prism-compiler/src/lang/beta_reduce_head.rs index dbf9e73a..1431bb46 100644 --- a/prism-compiler/src/lang/beta_reduce_head.rs +++ b/prism-compiler/src/lang/beta_reduce_head.rs @@ -1,6 +1,7 @@ use crate::lang::env::Env; use crate::lang::env::EnvEntry::*; -use crate::lang::{PartialExpr, TcEnv, UnionIndex}; +use crate::lang::{PartialExpr, TcEnv}; +use crate::lang::UnionIndex; impl TcEnv { pub fn beta_reduce_head( diff --git a/prism-compiler/src/lang/display.rs b/prism-compiler/src/lang/display.rs index f3ff80a0..146a772d 100644 --- a/prism-compiler/src/lang/display.rs +++ b/prism-compiler/src/lang/display.rs @@ -1,7 +1,8 @@ use std::fmt::Write; use crate::lang::display::PrecedenceLevel::*; -use crate::lang::{PartialExpr, TcEnv, UnionIndex}; +use crate::lang::{PartialExpr, TcEnv}; +use crate::lang::UnionIndex; #[derive(Ord, PartialOrd, Eq, PartialEq, Copy, Clone, Default)] enum PrecedenceLevel { diff --git a/prism-compiler/src/lang/env.rs b/prism-compiler/src/lang/env.rs index 8d255f69..9558f8b9 100644 --- a/prism-compiler/src/lang/env.rs +++ b/prism-compiler/src/lang/env.rs @@ -1,6 +1,6 @@ -use crate::lang::{TcEnv, UnionIndex}; +use crate::lang::{TcEnv}; use rpds::Vector; -use std::ops::Index; +use crate::lang::UnionIndex; #[derive(Copy, Clone, Eq, PartialEq, Debug, Hash)] pub struct UniqueVariableId(usize); @@ -65,7 +65,7 @@ impl GenericEnv { } } -impl Index for GenericEnv { +impl std::ops::Index for GenericEnv { type Output = T; fn index(&self, index: usize) -> &Self::Output { diff --git a/prism-compiler/src/lang/error.rs b/prism-compiler/src/lang/error.rs index 5ab85518..30d14ca9 100644 --- a/prism-compiler/src/lang/error.rs +++ b/prism-compiler/src/lang/error.rs @@ -1,4 +1,5 @@ -use crate::lang::{TcEnv, UnionIndex, ValueOrigin}; +use crate::lang::{TcEnv, ValueOrigin}; +use crate::lang::UnionIndex; use ariadne::{Color, Label, Report, ReportKind, Source}; use prism_parser::core::span::Span; use std::io; @@ -20,6 +21,7 @@ pub enum TypeError { free_var: UnionIndex, inferred_var: UnionIndex, }, + UnknownName(Span), } impl TcEnv { @@ -117,6 +119,11 @@ impl TcEnv { .finish() } TypeError::BadInfer { .. } => report.finish(), + TypeError::UnknownName(name) => { + report.with_message("Undefined name within this scope.") + .with_label(Label::new(*name).with_message("This name is undefined.")) + .finish() + } }) } diff --git a/prism-compiler/src/lang/from_action_result.rs b/prism-compiler/src/lang/from_action_result.rs deleted file mode 100644 index 256cf91a..00000000 --- a/prism-compiler/src/lang/from_action_result.rs +++ /dev/null @@ -1,63 +0,0 @@ -use crate::lang::UnionIndex; -use crate::lang::{PartialExpr, TcEnv}; -use prism_parser::rule_action::action_result::ActionResult; - -impl TcEnv { - pub fn new() -> Self { - Self::default() - } - - pub fn insert_from_action_result<'grm>( - &mut self, - value: &ActionResult<'_, 'grm>, - src: &'grm str, - ) -> UnionIndex { - let ActionResult::Construct(span, constructor, args) = value else { - unreachable!("Parsing an expression always returns a Construct"); - }; - let inner = match *constructor { - "Type" => { - assert_eq!(args.len(), 0); - PartialExpr::Type - } - "Let" => { - assert_eq!(args.len(), 2); - PartialExpr::Let( - self.insert_from_action_result(&args[0], src), - self.insert_from_action_result(&args[1], src), - ) - } - "DeBruijnIndex" => { - assert_eq!(args.len(), 1); - PartialExpr::DeBruijnIndex(args[0].get_value(src).parse().unwrap()) - } - "FnType" => { - assert_eq!(args.len(), 2); - PartialExpr::FnType( - self.insert_from_action_result(&args[0], src), - self.insert_from_action_result(&args[1], src), - ) - } - "FnConstruct" => { - assert_eq!(args.len(), 2); - PartialExpr::FnConstruct( - self.insert_from_action_result(&args[0], src), - self.insert_from_action_result(&args[1], src), - ) - } - "FnDestruct" => { - assert_eq!(args.len(), 2); - PartialExpr::FnDestruct( - self.insert_from_action_result(&args[0], src), - self.insert_from_action_result(&args[1], src), - ) - } - "Free" => { - assert_eq!(args.len(), 0); - PartialExpr::Free - } - _ => unreachable!(), - }; - self.store_from_source(inner, *span) - } -} diff --git a/prism-compiler/src/lang/from_parse_env.rs b/prism-compiler/src/lang/from_parse_env.rs new file mode 100644 index 00000000..5e51bafe --- /dev/null +++ b/prism-compiler/src/lang/from_parse_env.rs @@ -0,0 +1,68 @@ +use crate::desugar::{ParseEnv, ParseIndex, SourceExpr}; +use crate::lang::{PartialExpr, TcEnv, UnionIndex, ValueOrigin}; +use crate::lang::error::TypeError; + +/// Stores the variables in scope + the depth of the scope +#[derive(Default, Clone)] +struct Scope<'a>(rpds::RedBlackTreeMap<&'a str, usize>, usize); + +impl<'a> Scope<'a> { + pub fn insert(&self, key: &'a str) -> Self { + Scope(self.0.insert(key, self.1), self.1 + 1) + } +} + +impl TcEnv { + pub fn insert_parse_env(&mut self, parse_env: &ParseEnv, root: ParseIndex) -> UnionIndex { + let mut names = vec![Scope::default(); parse_env.values().len()]; + + let start = self.values.len(); + let take_count = root.index() + 1; + + self.values.resize(start + take_count, PartialExpr::Free); + self.value_origins.resize(start + take_count, ValueOrigin::Failure); + + for (i, (expr, span)) in parse_env.values().iter().zip(parse_env.value_spans().iter()).take(take_count).enumerate().rev() { + self.value_origins[start+i] = ValueOrigin::SourceCode(*span); + self.values[start+i] = match expr { + SourceExpr::Type => { + PartialExpr::Type + } + SourceExpr::Let(name, value, body) => { + names[value.index()] = names[i].clone(); + names[body.index()] = names[i].insert(&name); + PartialExpr::Let(UnionIndex(value.index() + start), UnionIndex(body.index() + start)) + } + SourceExpr::Variable(name) => { + if name == "_" { + PartialExpr::Free + } else { + if let Some(depth) = names[i].0.get(name.as_str()) { + PartialExpr::DeBruijnIndex(names[i].1 - depth - 1) + } else { + self.errors.push(TypeError::UnknownName(*span)); + PartialExpr::Free + } + } + } + SourceExpr::FnType(name, arg_type, return_type) => { + names[arg_type.index()] = names[i].clone(); + names[return_type.index()] = names[i].insert(&name); + PartialExpr::FnType(UnionIndex(arg_type.index() + start), UnionIndex(return_type.index() + start)) + } + SourceExpr::FnConstruct(name, arg_type, body) => { + names[arg_type.index()] = names[i].clone(); + names[body.index()] = names[i].insert(&name); + PartialExpr::FnConstruct(UnionIndex(arg_type.index() + start), UnionIndex(body.index() + start)) + } + SourceExpr::FnDestruct(function, arg) => { + names[function.index()] = names[i].clone(); + names[arg.index()] = names[i].clone(); + PartialExpr::FnDestruct(UnionIndex(function.index() + start), UnionIndex(arg.index() + start)) + } + }; + names.pop(); + } + UnionIndex(root.index() + start) + } +} \ No newline at end of file diff --git a/prism-compiler/src/lang/is_beta_equal.rs b/prism-compiler/src/lang/is_beta_equal.rs index f0803ade..93fc17bb 100644 --- a/prism-compiler/src/lang/is_beta_equal.rs +++ b/prism-compiler/src/lang/is_beta_equal.rs @@ -1,6 +1,7 @@ use crate::lang::env::Env; use crate::lang::env::EnvEntry::*; -use crate::lang::{PartialExpr, TcEnv, UnionIndex}; +use crate::lang::{PartialExpr, TcEnv}; +use crate::lang::UnionIndex; impl TcEnv { pub fn is_beta_equal(&mut self, i1: UnionIndex, s1: &Env, i2: UnionIndex, s2: &Env) -> bool { diff --git a/prism-compiler/src/lang/mod.rs b/prism-compiler/src/lang/mod.rs index f56efd77..bf6f5c72 100644 --- a/prism-compiler/src/lang/mod.rs +++ b/prism-compiler/src/lang/mod.rs @@ -11,10 +11,10 @@ pub mod env; pub mod error; mod expect_beq; mod expect_beq_internal; -pub mod from_action_result; pub mod is_beta_equal; pub mod simplify; pub mod type_check; +mod from_parse_env; type QueuedConstraint = ( (Env, HashMap), @@ -23,9 +23,8 @@ type QueuedConstraint = ( #[derive(Default)] pub struct TcEnv { - // uf: UnionFind, - values: Vec, - value_origins: Vec, + pub values: Vec, + pub value_origins: Vec, value_types: HashMap, tc_id: usize, diff --git a/prism-compiler/src/lang/type_check.rs b/prism-compiler/src/lang/type_check.rs index c1ec9973..486d1146 100644 --- a/prism-compiler/src/lang/type_check.rs +++ b/prism-compiler/src/lang/type_check.rs @@ -1,7 +1,8 @@ use crate::lang::env::Env; use crate::lang::env::EnvEntry::*; use crate::lang::error::{AggregatedTypeError, TypeError}; -use crate::lang::{UnionIndex, ValueOrigin}; +use crate::lang::{ValueOrigin}; +use crate::lang::UnionIndex; use crate::lang::{PartialExpr, TcEnv}; use std::mem; diff --git a/prism-compiler/src/lib.rs b/prism-compiler/src/lib.rs index ab0f6276..0693af6f 100644 --- a/prism-compiler/src/lib.rs +++ b/prism-compiler/src/lib.rs @@ -1,2 +1,3 @@ pub mod lang; pub mod parser; +pub mod desugar; diff --git a/prism-compiler/src/parser.rs b/prism-compiler/src/parser.rs index 389e94e7..79161c42 100644 --- a/prism-compiler/src/parser.rs +++ b/prism-compiler/src/parser.rs @@ -1,4 +1,5 @@ use crate::lang::{TcEnv, UnionIndex}; +use crate::desugar::{ParseEnv}; use lazy_static::lazy_static; use prism_parser::error::aggregate_error::{AggregatedParseError, ParseResultExt}; use prism_parser::error::set_error::SetError; @@ -16,12 +17,14 @@ pub fn parse_prism_in_env<'p>( program: &'p str, env: &mut TcEnv, ) -> Result>> { - run_parser_rule::(&GRAMMAR, "block", program, |r| { - env.insert_from_action_result(r, program) - }) + let mut penv = ParseEnv::default(); + let idx = run_parser_rule::(&GRAMMAR, "block", program, |r| { + penv.insert_from_action_result(r, program) + })?; + Ok(env.insert_parse_env(&penv, idx)) } pub fn parse_prism(program: &str) -> Result<(TcEnv, UnionIndex), AggregatedParseError> { - let mut env = TcEnv::new(); + let mut env = TcEnv::default(); parse_prism_in_env(program, &mut env).map(|i| (env, i)) } diff --git a/prism-compiler/tests/beta_reduce.rs b/prism-compiler/tests/beta_reduce.rs index a462dca8..4823a3f6 100644 --- a/prism-compiler/tests/beta_reduce.rs +++ b/prism-compiler/tests/beta_reduce.rs @@ -15,7 +15,7 @@ fn test([test]: [&str; 1]) { } fn check(input: &str) { - let mut env = TcEnv::new(); + let mut env = TcEnv::default(); let input = parse_prism_in_env(input, &mut env).unwrap_or_eprint(); let sm = env.beta_reduce(input); @@ -30,3 +30,6 @@ fn check(input: &str) { } test_each_file! { for ["test"] in "prism-compiler/programs/ok" => test } + +#[test] +fn placeholder() {} diff --git a/prism-compiler/tests/beta_reduce_head.rs b/prism-compiler/tests/beta_reduce_head.rs index 522549c4..d4fd1bc5 100644 --- a/prism-compiler/tests/beta_reduce_head.rs +++ b/prism-compiler/tests/beta_reduce_head.rs @@ -9,7 +9,7 @@ fn test([test]: [&str; 1]) { let (input, rest) = rest.split_once("### Eval\n").unwrap(); let (eval, _expected_typ) = rest.split_once("### Type\n").unwrap(); - let mut env = TcEnv::new(); + let mut env = TcEnv::default(); let input = parse_prism_in_env(input, &mut env).unwrap_or_eprint(); let expected_eval = parse_prism_in_env(eval, &mut env).unwrap_or_eprint(); diff --git a/prism-compiler/tests/exhaustive.rs b/prism-compiler/tests/exhaustive.rs index 4292c253..23750bba 100644 --- a/prism-compiler/tests/exhaustive.rs +++ b/prism-compiler/tests/exhaustive.rs @@ -8,7 +8,7 @@ pub struct ExprWithEnv(pub TcEnv, pub UnionIndex); impl Exhaustive for ExprWithEnv { fn generate(u: &mut DataSourceTaker) -> exhaustive::Result { - let mut env = TcEnv::new(); + let mut env = TcEnv::default(); let idx = arbitrary_rec(0, &mut env, u)?; Ok(ExprWithEnv(env, idx)) } diff --git a/prism-compiler/tests/simplify.rs b/prism-compiler/tests/simplify.rs index 81f47b84..86504b65 100644 --- a/prism-compiler/tests/simplify.rs +++ b/prism-compiler/tests/simplify.rs @@ -15,7 +15,7 @@ fn test([test]: [&str; 1]) { } fn check(input: &str) { - let mut env = TcEnv::new(); + let mut env = TcEnv::default(); let input = parse_prism_in_env(input, &mut env).unwrap_or_eprint(); let sm = env.simplify(input); diff --git a/prism-compiler/tests/type_check.rs b/prism-compiler/tests/type_check.rs index ea266bda..5e2a07c3 100644 --- a/prism-compiler/tests/type_check.rs +++ b/prism-compiler/tests/type_check.rs @@ -10,7 +10,7 @@ fn test_ok([test]: [&str; 1]) { let (input_str, rest) = rest.split_once("### Eval\n").unwrap(); let (_eval, expected_typ) = rest.split_once("### Type\n").unwrap(); - let mut env = TcEnv::new(); + let mut env = TcEnv::default(); let input = parse_prism_in_env(input_str, &mut env).unwrap_or_eprint(); let typ = env.type_check(input).unwrap_or_eprint(&mut env, input_str); @@ -31,7 +31,7 @@ fn test_ok([test]: [&str; 1]) { test_each_file! { for ["test"] in "prism-compiler/programs/ok" as ok => test_ok } fn test_fail([test]: [&str; 1]) { - let mut env = TcEnv::new(); + let mut env = TcEnv::default(); let input = parse_prism_in_env(test, &mut env).unwrap_or_eprint(); match env.type_check(input) { diff --git a/prism-parser/src/core/recovery.rs b/prism-parser/src/core/recovery.rs index 7f679acb..a3ccd4d7 100644 --- a/prism-parser/src/core/recovery.rs +++ b/prism-parser/src/core/recovery.rs @@ -11,7 +11,7 @@ use crate::rule_action::action_result::ActionResult; use std::collections::HashMap; use std::sync::Arc; -const MAX_RECOVERIES: usize = 10; +const MAX_RECOVERIES: usize = 5; pub fn parse_with_recovery<'a, 'arn: 'a, 'grm: 'arn, O, E: ParseError>>( sub: &'a impl Parser<'arn, 'grm, O, E>,