Add a temporary desugaring layer for names

.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
 

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"

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
 

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
 

prism-compiler/programs/ok/free3.test

@@ -1,10 +1,10 @@
 ### Input
-let _;
-#0
+let v = _;
+v
 
 ### Eval
-let _;
-#0
+let v = _;
+v
 
 ### Type
 _

prism-compiler/programs/ok/free5.test

@@ -1,5 +1,5 @@
 ### Input
-(Type => _) Type
+(_: Type => _) Type
 
 ### Eval
 _

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

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

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
+T: Type -> T -> T

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

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