Fix tests

prism-compiler/programs/ok/church_bools.test

@@ -0,0 +1,20 @@
+### 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);
+
+// and true true
+#0 #1 #1
+
+### Eval
+Type => #0 => #1 => #0
+
+### Type
+Type -> #0 -> #1 -> #2
+

prism-compiler/programs/ok/church_nats → prism-compiler/programs/ok/church_nats.test

@@ -2,11 +2,11 @@
 let Type -> #0 -> (#1 -> #2) -> #2;
 let Type => #0 => (#1 -> #2) => #1;
 let #1 => Type => #0 => (#1 -> #2) => #0 (#3 #2 #1 #0);
-#1 #0
+#0 #1
 
 ### Eval
-Type -> #0 -> (#1 -> #2) -> #2
+Type => #0 => (#1 -> #2) => #0 1
 
 ### Type
-Type => #0 => (#1 -> #2) => #0 #1
+Type -> #0 -> (#1 -> #2) -> #2
 

prism-compiler/resources/grammar

@@ -26,4 +26,7 @@ rule expr {
     }
 }
 
-rule layout = [' ' | '\n'];
+rule layout {
+    [' ' | '\n'];
+    "//" [^'\n']* "\n";
+}

prism-compiler/resources/program.pr

@@ -1 +1,8 @@
-Type
+// Nat : (T:Type) -> zero:T -> succ:(T->T) -> T
+let Type -> #0 -> (#1 -> #2) -> #2;
+// zero : Nat
+let Type => #0 => (#1 -> #2) => #1;
+// 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);
+#0 #1