From 10b90d6f9db2387798ccdfad7e3d461a54694229 Mon Sep 17 00:00:00 2001 From: jonathan Date: Fri, 7 Jun 2024 14:35:24 +0200 Subject: [PATCH] Fix tests --- prism-compiler/programs/ok/church_bools.test | 20 +++++++++++++++++++ .../ok/{church_nats => church_nats.test} | 6 +++--- prism-compiler/resources/grammar | 5 ++++- prism-compiler/resources/program.pr | 9 ++++++++- 4 files changed, 35 insertions(+), 5 deletions(-) create mode 100644 prism-compiler/programs/ok/church_bools.test rename prism-compiler/programs/ok/{church_nats => church_nats.test} (82%) diff --git a/prism-compiler/programs/ok/church_bools.test b/prism-compiler/programs/ok/church_bools.test new file mode 100644 index 00000000..1c1b3c92 --- /dev/null +++ b/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 + diff --git a/prism-compiler/programs/ok/church_nats b/prism-compiler/programs/ok/church_nats.test similarity index 82% rename from prism-compiler/programs/ok/church_nats rename to prism-compiler/programs/ok/church_nats.test index 4bc28080..fcb5a423 100644 --- a/prism-compiler/programs/ok/church_nats +++ b/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 diff --git a/prism-compiler/resources/grammar b/prism-compiler/resources/grammar index 25999704..eb79408c 100644 --- a/prism-compiler/resources/grammar +++ b/prism-compiler/resources/grammar @@ -26,4 +26,7 @@ rule expr { } } -rule layout = [' ' | '\n']; +rule layout { + [' ' | '\n']; + "//" [^'\n']* "\n"; +} diff --git a/prism-compiler/resources/program.pr b/prism-compiler/resources/program.pr index d69dbe25..eca69eca 100644 --- a/prism-compiler/resources/program.pr +++ b/prism-compiler/resources/program.pr @@ -1 +1,8 @@ -Type \ No newline at end of file +// 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 \ No newline at end of file