diff --git a/README.md b/README.md index 6866a429..60fb845b 100644 --- a/README.md +++ b/README.md @@ -1,12 +1,11 @@ # McLTT: A Bottom-up Approach to Implementing A Proof Assistant -In McLTT, we build a verified, runnable typechecker for Martin-Löf type theory. After -the accomplishment of this project, we will obtain an executable, to which we can feed -a program in Martin-Löf type theory, and this executable will check whether this -program has the specified type. McLTT is novel in that it is implemented in -Coq. Moreover, we will prove that the typechecking algorithm extracted from Coq is -sound and complete: a program passes typechecking if and only if it is a well-typed -program in MLTT. This will be the first verified proof assistant (despite being +McLTT is a verified, runnable typechecker for Martin-Löf type theory. This project provides an executable, to which we can feed +a program in Martin-Löf type theory to check whether this +program has the specified type. McLTT is novel in that it is implemented and verified in +Coq. More specifically, we proved that the typechecking algorithm extracted from Coq is +sound and complete: a program passes typechecker if and only if it is a well-typed +program in MLTT. This is the first verified proof assistant (despite being elementary) and serves as a basis for future extensions. ## Online Documentation @@ -83,7 +82,7 @@ or more directly _build/default/driver/mcltt.exe examples/nary.mcl # or your own example ``` -To build Coq proof only, you can go into and only build the Coq folder: +To build Coq proof only, you can go into and only build the `theories` directory: ``` cd theories make diff --git a/driver/Lexer.mll b/driver/Lexer.mll index b590befb..c74eddd1 100644 --- a/driver/Lexer.mll +++ b/driver/Lexer.mll @@ -40,29 +40,37 @@ | TYPE _ -> "Type" | VAR (_, s) -> s | EOF _ -> "" + | DOT _ -> "." + | LET _ -> "let" + | IN _ -> "in" + | EQ _ -> ":=" let get_range_of_token : token -> (position * position) = function | ARROW r - | AT r - | BAR r - | COLON r - | COMMA r - | DARROW r - | LPAREN r - | RPAREN r - | ZERO r - | SUCC r - | REC r - | RETURN r - | END r - | LAMBDA r - | PI r - | NAT r - | TYPE r - | EOF r - | INT (r, _) - | VAR (r, _) -> r + | AT r + | BAR r + | COLON r + | COMMA r + | DARROW r + | LPAREN r + | RPAREN r + | ZERO r + | SUCC r + | REC r + | RETURN r + | END r + | LAMBDA r + | PI r + | NAT r + | TYPE r + | EOF r + | INT (r, _) + | DOT r + | LET r + | IN r + | EQ r + | VAR (r, _) -> r let format_token (f: Format.formatter) (t: token): unit = Format.fprintf @@ -97,8 +105,12 @@ rule read = | "Nat" { NAT (get_range lexbuf) } | ['0'-'9']+ as lxm { INT (get_range lexbuf, int_of_string lxm) } | "Type" { TYPE (get_range lexbuf) } - | string { VAR (get_range lexbuf, Lexing.lexeme lexbuf) } | eof { EOF (get_range lexbuf) } + | "." { DOT (get_range lexbuf) } + | "let" {LET (get_range lexbuf) } + | "in" {IN (get_range lexbuf) } + | ":=" {EQ (get_range lexbuf) } + | string { VAR (get_range lexbuf, Lexing.lexeme lexbuf) } | _ as c { failwith (Format.asprintf "@[Lexer error:@ @[Unexpected character %C@ at %a@]@]@." c format_position lexbuf.lex_start_p) } and comment = parse diff --git a/driver/PrettyPrinter.ml b/driver/PrettyPrinter.ml index 5ffdb518..a4998625 100644 --- a/driver/PrettyPrinter.ml +++ b/driver/PrettyPrinter.ml @@ -56,7 +56,7 @@ let rec format_obj_prec (p : int) (f : Format.formatter) : Cst.obj -> unit = | Cst.Coq_natrec (escr, mx, em, ez, sx, sr, es) -> let impl f () = fprintf f - "@[@[rec %a@ return %s -> %a@]@ @[| zero =>@ \ + "@[@[rec %a@ return %s . %a@]@ @[| zero =>@ \ %a@]@ @[| succ %s, %s =>@ %a@]@ end@]" format_obj escr mx format_obj em format_obj ez sx sr format_obj es in diff --git a/driver/Test.ml b/driver/Test.ml index 475cd810..0c156c52 100644 --- a/driver/Test.ml +++ b/driver/Test.ml @@ -89,13 +89,13 @@ let%expect_test "identity function of Nat is of forall (x : Nat) -> Nat" = let%expect_test "recursion on a natural number that always returns zero is of \ Nat" = let _ = main_of_program_string - "rec 3 return y -> Nat | zero => 0 | succ n, r => 0 end : Nat" in + "rec 3 return y . Nat | zero => 0 | succ n, r => 0 end : Nat" in [%expect {| Parsed: - rec 3 return y -> Nat | zero => 0 | succ n, r => 0 end : Nat + rec 3 return y . Nat | zero => 0 | succ n, r => 0 end : Nat Elaborated: - rec 3 return x1 -> Nat | zero => 0 | succ x2, x3 => 0 end : Nat + rec 3 return x1 . Nat | zero => 0 | succ x2, x3 => 0 end : Nat Normalized Result: 0 : Nat |}] @@ -117,16 +117,15 @@ let%expect_test "simple_rec.mcl works" = [%expect {| Parsed: - fun (x : Nat) - -> rec x return y -> Nat | zero => 1 | succ n, r => succ r end + fun (x : Nat) -> rec x return y . Nat | zero => 1 | succ n, r => succ r end : forall (x : Nat) -> Nat Elaborated: fun (x1 : Nat) - -> rec x1 return x2 -> Nat | zero => 1 | succ x3, x4 => succ x4 end + -> rec x1 return x2 . Nat | zero => 1 | succ x3, x4 => succ x4 end : forall (x1 : Nat) -> Nat Normalized Result: fun (x1 : Nat) - -> rec x1 return x2 -> Nat | zero => 1 | succ x3, x4 => succ x4 end + -> rec x1 return x2 . Nat | zero => 1 | succ x3, x4 => succ x4 end : forall (x1 : Nat) -> Nat |}] @@ -291,14 +290,14 @@ let%expect_test "vector.mcl works" = (vec : Vec A (succ n)) -> vecRec A (succ n) vec (fun (l : Nat) - -> rec l return r -> Type@0 + -> rec l return r . Type@0 | zero => Nat | succ l, r => A end) 0 (fun (l : Nat) (a : A) - (r : rec l return r -> Type@0 + (r : rec l return r . Type@0 | zero => Nat | succ l, r => A end) @@ -391,14 +390,14 @@ let%expect_test "vector.mcl works" = (x25 : x1 A6 (succ x24)) -> x8 A6 (succ x24) x25 (fun (x26 : Nat) - -> rec x26 return x27 -> Type@0 + -> rec x26 return x27 . Type@0 | zero => Nat | succ x28, A7 => A6 end) 0 (fun (x29 : Nat) (x30 : A6) - (x31 : rec x29 return x32 -> Type@0 + (x31 : rec x29 return x32 . Type@0 | zero => Nat | succ x33, A8 => A6 end) @@ -477,19 +476,19 @@ let%expect_test "nary.mcl works" = -> Nary n) (n : Nat) (f : Nary n) - -> (rec n return y -> forall (g : Nary y) -> Nat + -> (rec n return y . forall (g : Nary y) -> Nat | zero => toNat | succ m, r => fun (g : Nary (succ m)) -> r (appNary m g (succ m)) end) f) (fun (n : Nat) - -> rec n return y -> Type@0 + -> rec n return y . Type@0 | zero => Nat | succ m, r => forall (a : Nat) -> r end) (fun (f : Nat) -> f) (fun (n : Nat) - (f : rec succ n return y -> Type@0 + (f : rec succ n return y . Type@0 | zero => Nat | succ m, r => forall (a : Nat) -> r end) @@ -505,7 +504,7 @@ let%expect_test "nary.mcl works" = -> add a (add b c)) (fun (a : Nat) (b : Nat) - -> rec a return y -> Nat | zero => b | succ m, r => succ r end)) + -> rec a return y . Nat | zero => b | succ m, r => succ r end)) : Nat Elaborated: (fun (x1 : forall (x2 : Nat) -> Type@0) @@ -516,20 +515,20 @@ let%expect_test "nary.mcl works" = -> x1 x6) (x9 : Nat) (x10 : x1 x9) - -> (rec x9 return x11 -> forall (x14 : x1 x11) -> Nat + -> (rec x9 return x11 . forall (x14 : x1 x11) -> Nat | zero => x3 | succ x12, x13 => fun (x15 : x1 (succ x12)) -> x13 (x5 x12 x15 (succ x12)) end) x10) (fun (x16 : Nat) - -> rec x16 return x17 -> Type@0 + -> rec x16 return x17 . Type@0 | zero => Nat | succ x18, A1 => forall (x19 : Nat) -> A1 end) (fun (x20 : Nat) -> x20) (fun (x21 : Nat) - (x22 : rec succ x21 return x23 -> Type@0 + (x22 : rec succ x21 return x23 . Type@0 | zero => Nat | succ x24, A2 => forall (x25 : Nat) -> A2 end) @@ -545,7 +544,7 @@ let%expect_test "nary.mcl works" = -> x27 x30 (x27 x31 x32)) (fun (x33 : Nat) (x34 : Nat) - -> rec x33 return x35 -> Nat + -> rec x33 return x35 . Nat | zero => x34 | succ x36, x37 => succ x37 end)) @@ -554,6 +553,337 @@ let%expect_test "nary.mcl works" = 6 : Nat |}] +let%expect_test "simple_let.mcl works" = + let _ = main_of_example "simple_let.mcl" in + [%expect + {| + Parsed: + (fun (x : Nat) -> succ x) 0 : Nat + Elaborated: + (fun (x1 : Nat) -> succ x1) 0 : Nat + Normalized Result: + 1 : Nat + |}] + +let%expect_test "let_two_vars.mcl works" = + let _ = main_of_example "let_two_vars.mcl" in + [%expect + {| + Parsed: + (fun (x : Nat) + (f : forall (y : Nat) -> Nat) + -> f x) 0 (fun (n : Nat) -> n) + : Nat + Elaborated: + (fun (x1 : Nat) + (x2 : forall (x3 : Nat) -> Nat) + -> x2 x1) 0 + (fun (x4 : Nat) -> x4) + : Nat + Normalized Result: + 0 : Nat + |}] + +let%expect_test "let_nary.mcl works" = + let _ = main_of_example "let_nary.mcl" in + [%expect + {| + Parsed: + (fun (Nary : forall (n : Nat) -> Type@0) + (toNat : forall (f : Nary 0) -> Nat) + (appNary : forall (n : Nat) + (f : Nary (succ n)) + (arg : Nat) + -> Nary n) + (n : Nat) + (f : Nary n) + -> (rec n return y . forall (g : Nary y) -> Nat + | zero => toNat + | succ m, r => fun (g : Nary (succ m)) -> r (appNary m g (succ m)) + end) + f) + (fun (n : Nat) + -> rec n return y . Type@0 + | zero => Nat + | succ m, r => forall (a : Nat) -> r + end) + (fun (f : Nat) -> f) + (fun (n : Nat) + (f : rec succ n return y . Type@0 + | zero => Nat + | succ m, r => forall (a : Nat) -> r + end) + (arg : Nat) + -> f arg) + 3 + ((fun (add : forall (a : Nat) + (b : Nat) + -> Nat) + (a : Nat) + (b : Nat) + (c : Nat) + -> add a (add b c)) + (fun (a : Nat) + (b : Nat) + -> rec a return y . Nat | zero => b | succ m, r => succ r end)) + : Nat + Elaborated: + (fun (x1 : forall (x2 : Nat) -> Type@0) + (x3 : forall (x4 : x1 0) -> Nat) + (x5 : forall (x6 : Nat) + (x7 : x1 (succ x6)) + (x8 : Nat) + -> x1 x6) + (x9 : Nat) + (x10 : x1 x9) + -> (rec x9 return x11 . forall (x14 : x1 x11) -> Nat + | zero => x3 + | succ x12, x13 => + fun (x15 : x1 (succ x12)) -> x13 (x5 x12 x15 (succ x12)) + end) + x10) + (fun (x16 : Nat) + -> rec x16 return x17 . Type@0 + | zero => Nat + | succ x18, A1 => forall (x19 : Nat) -> A1 + end) + (fun (x20 : Nat) -> x20) + (fun (x21 : Nat) + (x22 : rec succ x21 return x23 . Type@0 + | zero => Nat + | succ x24, A2 => forall (x25 : Nat) -> A2 + end) + (x26 : Nat) + -> x22 x26) + 3 + ((fun (x27 : forall (x28 : Nat) + (x29 : Nat) + -> Nat) + (x30 : Nat) + (x31 : Nat) + (x32 : Nat) + -> x27 x30 (x27 x31 x32)) + (fun (x33 : Nat) + (x34 : Nat) + -> rec x33 return x35 . Nat + | zero => x34 + | succ x36, x37 => succ x37 + end)) + : Nat + Normalized Result: + 6 : Nat + |}] + + +let%expect_test "let_vector.mcl works" = + let _ = main_of_example "let_vector.mcl" in + [%expect + {| + Parsed: + (fun (Vec : forall (A : Type@0) + (n : Nat) + -> Type@2) + (nil : forall (A : Type@0) -> Vec A 0) + (cons : forall (A : Type@0) + (n : Nat) + (head : A) + (tail : Vec A n) + -> Vec A (succ n)) + (vecRec : forall (A : Type@0) + (n : Nat) + (vec : Vec A n) + (C : forall (l : Nat) -> Type@1) + (nil : C 0) + (cons : forall (l : Nat) + (a : A) + (r : C l) + -> C (succ l)) + -> C n) + -> (fun (totalHead : forall (A : Type@0) + (n : Nat) + (vec : Vec A (succ n)) + -> A) + (vec : Vec (forall (n : Nat) -> Nat) 3) + -> totalHead (forall (n : Nat) -> Nat) 2 vec 4) + (fun (A : Type@0) + (n : Nat) + (vec : Vec A (succ n)) + -> vecRec A (succ n) vec + (fun (l : Nat) + -> rec l return r . Type@0 + | zero => Nat + | succ l, r => A + end) + 0 + (fun (l : Nat) + (a : A) + (r : rec l return r . Type@0 + | zero => Nat + | succ l, r => A + end) + -> a)) + (cons (forall (n : Nat) -> Nat) 2 + (fun (n : Nat) -> succ (succ (succ n))) + (cons (forall (n : Nat) -> Nat) 1 (fun (n : Nat) -> succ n) + (cons (forall (n : Nat) -> Nat) 0 + (fun (n : Nat) -> succ (succ n)) + (nil (forall (n : Nat) -> Nat)))))) + (fun (A : Type@0) + (n : Nat) + -> forall (C : forall (l : Nat) -> Type@1) + (nil : C 0) + (cons : forall (l : Nat) + (a : A) + (r : C l) + -> C (succ l)) + -> C n) + (fun (A : Type@0) + (C : forall (l : Nat) -> Type@1) + (nil : C 0) + (cons : forall (l : Nat) + (a : A) + (r : C l) + -> C (succ l)) + -> nil) + (fun (A : Type@0) + (n : Nat) + (head : A) + (tail : forall (C : forall (l : Nat) -> Type@1) + (nil : C 0) + (cons : forall (l : Nat) + (a : A) + (r : C l) + -> C (succ l)) + -> C n) + (C : forall (l : Nat) -> Type@1) + (nil : C 0) + (cons : forall (l : Nat) + (a : A) + (r : C l) + -> C (succ l)) + -> cons n head (tail C nil cons)) + (fun (A : Type@0) + (n : Nat) + (vec : forall (C : forall (l : Nat) -> Type@1) + (nil : C 0) + (cons : forall (l : Nat) + (a : A) + (r : C l) + -> C (succ l)) + -> C n) + (C : forall (l : Nat) -> Type@1) + (nil : C 0) + (cons : forall (l : Nat) + (a : A) + (r : C l) + -> C (succ l)) + -> vec C nil cons) + : Nat + Elaborated: + (fun (x1 : forall (A1 : Type@0) + (x2 : Nat) + -> Type@2) + (x3 : forall (A2 : Type@0) -> x1 A2 0) + (x4 : forall (A3 : Type@0) + (x5 : Nat) + (x6 : A3) + (x7 : x1 A3 x5) + -> x1 A3 (succ x5)) + (x8 : forall (A4 : Type@0) + (x9 : Nat) + (x10 : x1 A4 x9) + (x11 : forall (x12 : Nat) -> Type@1) + (x13 : x11 0) + (x14 : forall (x15 : Nat) + (x16 : A4) + (x17 : x11 x15) + -> x11 (succ x15)) + -> x11 x9) + -> (fun (x18 : forall (A5 : Type@0) + (x19 : Nat) + (x20 : x1 A5 (succ x19)) + -> A5) + (x21 : x1 (forall (x22 : Nat) -> Nat) 3) + -> x18 (forall (x23 : Nat) -> Nat) 2 x21 4) + (fun (A6 : Type@0) + (x24 : Nat) + (x25 : x1 A6 (succ x24)) + -> x8 A6 (succ x24) x25 + (fun (x26 : Nat) + -> rec x26 return x27 . Type@0 + | zero => Nat + | succ x28, A7 => A6 + end) + 0 + (fun (x29 : Nat) + (x30 : A6) + (x31 : rec x29 return x32 . Type@0 + | zero => Nat + | succ x33, A8 => A6 + end) + -> x30)) + (x4 (forall (x34 : Nat) -> Nat) 2 + (fun (x35 : Nat) -> succ (succ (succ x35))) + (x4 (forall (x36 : Nat) -> Nat) 1 (fun (x37 : Nat) -> succ x37) + (x4 (forall (x38 : Nat) -> Nat) 0 + (fun (x39 : Nat) -> succ (succ x39)) + (x3 (forall (x40 : Nat) -> Nat)))))) + (fun (A9 : Type@0) + (x41 : Nat) + -> forall (x42 : forall (x43 : Nat) -> Type@1) + (x44 : x42 0) + (x45 : forall (x46 : Nat) + (x47 : A9) + (x48 : x42 x46) + -> x42 (succ x46)) + -> x42 x41) + (fun (A10 : Type@0) + (x49 : forall (x50 : Nat) -> Type@1) + (x51 : x49 0) + (x52 : forall (x53 : Nat) + (x54 : A10) + (x55 : x49 x53) + -> x49 (succ x53)) + -> x51) + (fun (A11 : Type@0) + (x56 : Nat) + (x57 : A11) + (x58 : forall (x59 : forall (x60 : Nat) -> Type@1) + (x61 : x59 0) + (x62 : forall (x63 : Nat) + (x64 : A11) + (x65 : x59 x63) + -> x59 (succ x63)) + -> x59 x56) + (x66 : forall (x67 : Nat) -> Type@1) + (x68 : x66 0) + (x69 : forall (x70 : Nat) + (x71 : A11) + (x72 : x66 x70) + -> x66 (succ x70)) + -> x69 x56 x57 (x58 x66 x68 x69)) + (fun (A12 : Type@0) + (x73 : Nat) + (x74 : forall (x75 : forall (x76 : Nat) -> Type@1) + (x77 : x75 0) + (x78 : forall (x79 : Nat) + (x80 : A12) + (x81 : x75 x79) + -> x75 (succ x79)) + -> x75 x73) + (x82 : forall (x83 : Nat) -> Type@1) + (x84 : x82 0) + (x85 : forall (x86 : Nat) + (x87 : A12) + (x88 : x82 x86) + -> x82 (succ x86)) + -> x74 x82 x84 x85) + : Nat + Normalized Result: + 7 : Nat + |}] + + (* let%test "lambda" = *) (* parse "fun (x : Type 5).y" = Some (Coq_fn (x, Coq_typ 5, Coq_var y)) *) diff --git a/examples/let_nary.mcl b/examples/let_nary.mcl new file mode 100644 index 00000000..87d7b835 --- /dev/null +++ b/examples/let_nary.mcl @@ -0,0 +1,44 @@ +let ((Nary : forall (n : Nat) -> Type@0) := + ( + fun (n : Nat) + -> rec n return y . Type@0 + | zero => Nat + | succ m, r => forall (a : Nat) -> r + end + )) + + ((toNat : forall (f : Nary 0) -> Nat) := + ( + fun (f : Nat) -> f + )) + + ((appNary : forall (n : Nat) (f : Nary (succ n)) (arg : Nat) -> Nary n) := + ( + fun (n : Nat) + (f : rec succ n return y . Type@0 + | zero => Nat + | succ m, r => forall (a : Nat) -> r + end) + (arg : Nat) + -> f arg + )) + + ((n : Nat) := 3) + ((f : Nary n) := + ( + (fun (add : forall (a : Nat) (b : Nat) -> Nat) -> (fun (a : Nat) (b : Nat) (c : Nat) -> add a (add b c))) + ( + fun (a : Nat) + (b : Nat) + -> rec a return y . Nat + | zero => b + | succ m, r => succ r + end + ) + )) + +in + ((rec n return y . (forall (g : Nary y) -> Nat) + | zero => toNat + | succ m, r => fun (g : Nary (succ m)) -> r (appNary m g (succ m)) + end) f) : Nat \ No newline at end of file diff --git a/examples/let_two_vars.mcl b/examples/let_two_vars.mcl new file mode 100644 index 00000000..878b17aa --- /dev/null +++ b/examples/let_two_vars.mcl @@ -0,0 +1 @@ +let ((x : Nat) := 0) ((f : forall (y : Nat) -> Nat) := (fun (n : Nat) -> n)) in f x : Nat \ No newline at end of file diff --git a/examples/let_vector.mcl b/examples/let_vector.mcl new file mode 100644 index 00000000..52321c5a --- /dev/null +++ b/examples/let_vector.mcl @@ -0,0 +1,36 @@ +( +let ((Vec : forall (A : Type@0) (n : Nat) -> Type@2) := + (fun (A : Type@0) (n : Nat) -> forall (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n)) + + ((nil : forall (A : Type@0) -> Vec A 0) := + (fun (A : Type@0) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> nil)) + + ((cons : forall (A : Type@0) (n : Nat) (head : A) (tail : Vec A n) -> Vec A (succ n)) := + (fun (A : Type@0) (n : Nat) (head : A) (tail : forall (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> cons n head (tail C nil cons))) + + ((vecRec : forall (A : Type@0) (n : Nat) (vec : Vec A n) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n) := + (fun (A : Type@0) (n : Nat) (vec : forall (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> vec C nil cons)) + +in (let ((totalHead : forall (A : Type@0) (n : Nat) (vec : Vec A (succ n)) -> A) := + ( + fun (A : Type@0) (n : Nat) (vec : Vec A (succ n)) -> + vecRec A (succ n) vec (fun (l : Nat) -> rec l return r . Type@0 | zero => Nat | succ l, r => A end) 0 (fun (l : Nat) (a : A) (r : rec l return r . Type@0 | zero => Nat | succ l, r => A end) -> a) + )) + + ((vec : Vec (forall (n : Nat) -> Nat) 3) := + ( + cons (forall (n : Nat) -> Nat) 2 + (fun (n : Nat) -> succ (succ (succ n))) + ( + cons (forall (n : Nat) -> Nat) 1 + (fun (n : Nat) -> succ n) + ( + cons (forall (n : Nat) -> Nat) 0 + (fun (n : Nat) -> succ (succ n)) + (nil (forall (n : Nat) -> Nat)) + ) + ) + )) + + in totalHead ((forall (n : Nat) -> Nat)) 2 vec 4) +) : Nat \ No newline at end of file diff --git a/examples/nary.mcl b/examples/nary.mcl index cf9ffe62..4b8d7070 100644 --- a/examples/nary.mcl +++ b/examples/nary.mcl @@ -5,7 +5,7 @@ (appNary : forall (n : Nat) (f : Nary (succ n)) (arg : Nat) -> Nary n) (n : Nat) (f : Nary n) - -> (rec n return y -> (forall (g : Nary y) -> Nat) + -> (rec n return y . (forall (g : Nary y) -> Nat) | zero => toNat | succ m, r => fun (g : Nary (succ m)) -> r (appNary m g (succ m)) end) f @@ -13,7 +13,7 @@ (* Nary definition *) ( fun (n : Nat) - -> rec n return y -> Type@0 + -> rec n return y . Type@0 | zero => Nat | succ m, r => forall (a : Nat) -> r end @@ -23,7 +23,7 @@ (* appNary definition *) ( fun (n : Nat) - (f : rec succ n return y -> Type@0 + (f : rec succ n return y . Type@0 | zero => Nat | succ m, r => forall (a : Nat) -> r end) @@ -40,7 +40,7 @@ ( fun (a : Nat) (b : Nat) - -> rec a return y -> Nat + -> rec a return y . Nat | zero => b | succ m, r => succ r end diff --git a/examples/simple_let.mcl b/examples/simple_let.mcl new file mode 100644 index 00000000..8356abb2 --- /dev/null +++ b/examples/simple_let.mcl @@ -0,0 +1 @@ +let ((x : Nat) := zero) in succ x : Nat \ No newline at end of file diff --git a/examples/simple_rec.mcl b/examples/simple_rec.mcl index 1fc48404..cd5967d9 100644 --- a/examples/simple_rec.mcl +++ b/examples/simple_rec.mcl @@ -1,4 +1,4 @@ -(fun (x : Nat) -> rec x return y -> Nat +(fun (x : Nat) -> rec x return y . Nat | zero => 1 | succ n, r => succ r end) : forall (x : Nat) -> Nat diff --git a/examples/vector.mcl b/examples/vector.mcl index 5cd1bd14..c317d589 100644 --- a/examples/vector.mcl +++ b/examples/vector.mcl @@ -13,7 +13,7 @@ (* total head function *) ( fun (A : Type@0) (n : Nat) (vec : Vec A (succ n)) -> - vecRec A (succ n) vec (fun (l : Nat) -> rec l return r -> Type@0 | zero => Nat | succ l, r => A end) 0 (fun (l : Nat) (a : A) (r : rec l return r -> Type@0 | zero => Nat | succ l, r => A end) -> a) + vecRec A (succ n) vec (fun (l : Nat) -> rec l return r . Type@0 | zero => Nat | succ l, r => A end) 0 (fun (l : Nat) (a : A) (r : rec l return r . Type@0 | zero => Nat | succ l, r => A end) -> a) ) (* example vector *) ( diff --git a/theories/Core/Completeness/NatCases.v b/theories/Core/Completeness/NatCases.v index 9cf3fceb..57730c95 100644 --- a/theories/Core/Completeness/NatCases.v +++ b/theories/Core/Completeness/NatCases.v @@ -414,8 +414,8 @@ Proof. | _: env_relΓ ρ ?ρ0 |- _ => rename ρ0 into ρ' end. - assert {{ Dom ⇑ ℕ m ≈ ⇑ ℕ m' ∈ per_nat }} by (econstructor; eassumption). - assert {{ Dom ρ ↦ ⇑ ℕ m ≈ ρ' ↦ ⇑ ℕ m' ∈ env_relΓℕ }} as HinΓℕ by (apply_relation_equivalence; mauto). + assert {{ Dom ⇑ a m ≈ ⇑ b m' ∈ per_nat }} by (econstructor; eassumption). + assert {{ Dom ρ ↦ ⇑ a m ≈ ρ' ↦ ⇑ b m' ∈ env_relΓℕ }} as HinΓℕ by (apply_relation_equivalence; mauto). apply_relation_equivalence. (on_all_hyp: fun H => directed destruct (H _ _ HinΓℕ)). destruct_by_head per_univ. @@ -594,8 +594,8 @@ Proof. rename ρ1 into ρσ; rename ρ2 into ρ'σ end. - assert {{ Dom ⇑ ℕ m ≈ ⇑ ℕ m' ∈ per_nat }} by (econstructor; eassumption). - assert {{ Dom ρσ ↦ ⇑ ℕ m ≈ ρ'σ ↦ ⇑ ℕ m' ∈ env_relΔℕ }} as HinΔℕ by (apply_relation_equivalence; mauto). + assert {{ Dom ⇑ a m ≈ ⇑ b m' ∈ per_nat }} by (econstructor; eassumption). + assert {{ Dom ρσ ↦ ⇑ a m ≈ ρ'σ ↦ ⇑ b m' ∈ env_relΔℕ }} as HinΔℕ by (apply_relation_equivalence; mauto). apply_relation_equivalence. (on_all_hyp: fun H => directed destruct (H _ _ HinΔℕ)). destruct_by_head per_univ. diff --git a/theories/Core/Semantic/Evaluation/Definitions.v b/theories/Core/Semantic/Evaluation/Definitions.v index b0ff492f..174a772b 100644 --- a/theories/Core/Semantic/Evaluation/Definitions.v +++ b/theories/Core/Semantic/Evaluation/Definitions.v @@ -50,8 +50,8 @@ with eval_natrec : exp -> exp -> exp -> domain -> env -> domain -> Prop := {{ rec succ b ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ ms }} ) | eval_natrec_neut : `( {{ ⟦ MZ ⟧ ρ ↘ mz }} -> - {{ ⟦ A ⟧ ρ ↦ ⇑ ℕ m ↘ a }} -> - {{ rec ⇑ ℕ m ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ ⇑ a (rec m under ρ return A | zero -> mz | succ -> MS end) }} ) + {{ ⟦ A ⟧ ρ ↦ ⇑ b m ↘ a }} -> + {{ rec ⇑ b m ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ ⇑ a (rec m under ρ return A | zero -> mz | succ -> MS end) }} ) where "'rec' m '⟦return' A | 'zero' -> MZ | 'succ' -> MS 'end⟧' ρ '↘' r" := (eval_natrec A MZ MS m ρ r) (in custom judg) with eval_app : domain -> domain -> domain -> Prop := | eval_app_fn : diff --git a/theories/Core/Semantic/PER/Definitions.v b/theories/Core/Semantic/PER/Definitions.v index ed399204..1b22fc48 100644 --- a/theories/Core/Semantic/PER/Definitions.v +++ b/theories/Core/Semantic/PER/Definitions.v @@ -66,7 +66,7 @@ Inductive per_nat : relation domain := {{ Dom succ m ≈ succ n ∈ per_nat }} } | per_nat_neut : `{ {{ Dom m ≈ n ∈ per_bot }} -> - {{ Dom ⇑ ℕ m ≈ ⇑ ℕ n ∈ per_nat }} } + {{ Dom ⇑ a m ≈ ⇑ b n ∈ per_nat }} } . #[export] Hint Constructors per_nat : mcltt. diff --git a/theories/Core/Semantic/Readback/Definitions.v b/theories/Core/Semantic/Readback/Definitions.v index eaff8771..a958bdee 100644 --- a/theories/Core/Semantic/Readback/Definitions.v +++ b/theories/Core/Semantic/Readback/Definitions.v @@ -20,7 +20,7 @@ Inductive read_nf : nat -> domain_nf -> nf -> Prop := {{ Rnf ⇓ ℕ (succ m) in s ↘ succ M }} ) | read_nf_nat_neut : `( {{ Rne m in s ↘ M }} -> - {{ Rnf ⇓ ℕ (⇑ ℕ m) in s ↘ ⇑ M }} ) + {{ Rnf ⇓ ℕ (⇑ a m) in s ↘ ⇑ M }} ) | read_nf_fn : `( (** Normal form of arg type *) {{ Rtyp a in s ↘ A }} -> diff --git a/theories/Core/Soundness/LogicalRelation/Definitions.v b/theories/Core/Soundness/LogicalRelation/Definitions.v index 3dc2aa7c..1e6220e6 100644 --- a/theories/Core/Soundness/LogicalRelation/Definitions.v +++ b/theories/Core/Soundness/LogicalRelation/Definitions.v @@ -41,7 +41,7 @@ Inductive glu_nat : ctx -> exp -> domain -> Prop := | glu_nat_neut : `{ per_bot m m -> (forall {Δ σ M'}, {{ Δ ⊢w σ : Γ }} -> {{ Rne m in length Δ ↘ M' }} -> {{ Δ ⊢ M[σ] ≈ M' : ℕ }}) -> - glu_nat Γ M d{{{ ⇑ ℕ m }}} }. + glu_nat Γ M d{{{ ⇑ a m }}} }. #[export] Hint Constructors glu_nat : mcltt. diff --git a/theories/Core/Soundness/NatCases.v b/theories/Core/Soundness/NatCases.v index 90da4842..00c0b930 100644 --- a/theories/Core/Soundness/NatCases.v +++ b/theories/Core/Soundness/NatCases.v @@ -352,7 +352,7 @@ Qed. #[local] Hint Resolve cons_glu_sub_pred_q_nat_helper : mcltt. -Lemma glu_rel_exp_natrec_neut_helper : forall {i Γ SbΓ A MZ MS Δ M m σ ρ am P El}, +Lemma glu_rel_exp_natrec_neut_helper : forall {i Γ SbΓ A MZ MS Δ M a m σ ρ am P El}, {{ EG Γ ∈ glu_ctx_env ↘ SbΓ }} -> {{ Γ, ℕ ⊩ A : Type@i }} -> {{ Γ ⊩ A[Id,,zero] : Type@i }} -> @@ -362,10 +362,10 @@ Lemma glu_rel_exp_natrec_neut_helper : forall {i Γ SbΓ A MZ MS Δ M m σ ρ am {{ Dom m ≈ m ∈ per_bot }} -> (forall Δ' τ V, {{ Δ' ⊢w τ : Δ }} -> {{ Rne m in length Δ' ↘ V }} -> {{ Δ' ⊢ M[τ] ≈ V : ℕ }}) -> {{ Δ ⊢s σ ® ρ ∈ SbΓ }} -> - {{ ⟦ A ⟧ ρ ↦ ⇑ ℕ m ↘ am }} -> + {{ ⟦ A ⟧ ρ ↦ ⇑ a m ↘ am }} -> {{ DG am ∈ glu_univ_elem i ↘ P ↘ El }} -> exists r, - {{ rec ⇑ ℕ m ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ r }} /\ + {{ rec ⇑ a m ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ r }} /\ {{ Δ ⊢ rec M return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end : A[σ,,M] ® r ∈ El }}. Proof. intros * ? HA ? HMZ ? HMS **. @@ -380,7 +380,7 @@ Proof. invert_glu_rel_exp HA. pose (SbΓℕA := cons_glu_sub_pred i {{{ Γ, ℕ }}} A SbΓℕ). assert {{ EG Γ, ℕ, A ∈ glu_ctx_env ↘ SbΓℕA }} by (econstructor; mauto 3; reflexivity). - assert {{ Δ ⊢s σ,,M ® ρ ↦ ⇑ ℕ m ∈ SbΓℕ }} by (unfold SbΓℕ; mauto 3). + assert {{ Δ ⊢s σ,,M ® ρ ↦ ⇑ a m ∈ SbΓℕ }} by (unfold SbΓℕ; mauto 3). assert {{ Γ, ℕ, A ⊢ MS : A[Wk∘Wk,,succ #1] }} by mauto 2. invert_glu_rel_exp HMS. destruct_glu_rel_exp_with_sub. @@ -402,7 +402,7 @@ Proof. assert {{ ⊢ Δ, ℕ }} by mauto 3. assert {{ Δ, ℕ ⊢ A[q σ] : Type@i }} by mauto 3. assert {{ ⊢ Δ, ℕ, A[q σ] }} by mauto 2. - assert {{ Δ ⊢ M : ℕ }} by mauto 3. + assert {{ Δ ⊢ M : ℕ }} by mautosolve 3. assert {{ Δ ⊢ ℕ : Type@0 }} by mauto 3. assert {{ Δ ⊢ ℕ[σ] ≈ ℕ : Type@0 }} by mauto 3. assert {{ Δ ⊢ M : ℕ[σ] }} by mauto 3. diff --git a/theories/Extraction/Evaluation.v b/theories/Extraction/Evaluation.v index 65f81e5e..50c04d58 100644 --- a/theories/Extraction/Evaluation.v +++ b/theories/Extraction/Evaluation.v @@ -48,8 +48,8 @@ with eval_natrec_order : exp -> exp -> exp -> domain -> env -> Prop := eval_natrec_order A MZ MS d{{{ succ b }}} p ) | eno_neut : `( eval_exp_order MZ p -> - eval_exp_order A d{{{ p ↦ ⇑ ℕ m }}} -> - eval_natrec_order A MZ MS d{{{ ⇑ ℕ m }}} p ) + eval_exp_order A d{{{ p ↦ ⇑ a m }}} -> + eval_natrec_order A MZ MS d{{{ ⇑ a m }}} p ) with eval_app_order : domain -> domain -> Prop := | eao_fn : @@ -146,9 +146,9 @@ with eval_natrec_impl A MZ MS m p (H : eval_natrec_order A MZ MS m p) : { d | ev let (mr, Hmr) := eval_natrec_impl A MZ MS m p _ in let (r, Hr) := eval_exp_impl MS d{{{ p ↦ m ↦ mr }}} _ in exist _ r _ -| A, MZ, MS, d{{{ ⇑ ℕ m }}} , p, H => +| A, MZ, MS, d{{{ ⇑ a m }}} , p, H => let (mz, Hmz) := eval_exp_impl MZ p _ in - let (mA, HmA) := eval_exp_impl A d{{{ p ↦ ⇑ ℕ m }}} _ in + let (mA, HmA) := eval_exp_impl A d{{{ p ↦ ⇑ a m }}} _ in exist _ d{{{ ⇑ mA (rec m under p return A | zero -> mz | succ -> MS end) }}} _ with eval_app_impl m n (H : eval_app_order m n) : { d | eval_app m n d } by struct H := diff --git a/theories/Extraction/Readback.v b/theories/Extraction/Readback.v index e9e5df0d..4eb8b533 100644 --- a/theories/Extraction/Readback.v +++ b/theories/Extraction/Readback.v @@ -19,7 +19,7 @@ Inductive read_nf_order : nat -> domain_nf -> Prop := read_nf_order s d{{{ ⇓ ℕ (succ m) }}} ) | rnf_nat_neut : `( read_ne_order s m -> - read_nf_order s d{{{ ⇓ ℕ (⇑ ℕ m) }}} ) + read_nf_order s d{{{ ⇓ ℕ (⇑ a m) }}} ) | rnf_fn : `( read_typ_order s a -> eval_app_order m d{{{ ⇑! a s }}} -> @@ -119,7 +119,7 @@ Equations read_nf_impl s d (H : read_nf_order s d) : { m | {{ Rnf d in s ↘ m } | s, d{{{ ⇓ ℕ (succ m) }}} , H => let (M, HM) := read_nf_impl s d{{{ ⇓ ℕ m }}} _ in exist _ n{{{ succ M }}} _ -| s, d{{{ ⇓ ℕ (⇑ ℕ m) }}} , H => +| s, d{{{ ⇓ ℕ (⇑ ^_ m) }}} , H => let (M, HM) := read_ne_impl s m _ in exist _ n{{{ ⇑ M }}} _ | s, d{{{ ⇓ (Π a p B) m }}}, H => diff --git a/theories/Frontend/Parser.vy b/theories/Frontend/Parser.vy index 18010618..6980e1ab 100644 --- a/theories/Frontend/Parser.vy +++ b/theories/Frontend/Parser.vy @@ -10,14 +10,16 @@ Parameter loc : Type. %token VAR %token INT -%token END LAMBDA NAT PI REC RETURN SUCC TYPE ZERO (* keywords *) -%token ARROW "->" AT "@" BAR "|" COLON ":" COMMA "," DARROW "=>" LPAREN "(" RPAREN ")" EOF (* symbols *) +%token END LAMBDA NAT PI REC RETURN SUCC TYPE ZERO LET IN (* keywords *) +%token ARROW "->" AT "@" BAR "|" COLON ":" COMMA "," DARROW "=>" LPAREN "(" RPAREN ")" DOT "." EQ ":=" EOF (* symbols *) %start prog %type obj app_obj atomic_obj %type param %type params %type Cst.obj -> Cst.obj -> Cst.obj> fnbinder +%type <(string * Cst.obj) * Cst.obj> let_defn +%type let_defns %on_error_reduce obj params app_obj atomic_obj @@ -34,11 +36,14 @@ let obj := | ~ = fnbinder; ~ = params; "->"; ~ = obj; { List.fold_left (fun acc arg => fnbinder (fst arg) (snd arg) acc) params obj } | ~ = app_obj; <> - | REC; escr = obj; RETURN; mx = VAR; "->"; em = obj; + | REC; escr = obj; RETURN; mx = VAR; "."; em = obj; "|"; ZERO; "=>"; ez = obj; "|"; SUCC; sx = VAR; ","; sr = VAR; "=>"; ms = obj; END; { Cst.natrec escr (snd mx) em ez (snd sx) (snd sr) ms } | SUCC; ~ = obj; { Cst.succ obj } + + | LET; ds = let_defns; IN; body = obj; { List.fold_left (fun acc arg => Cst.app acc (snd arg)) (List.rev ds) (List.fold_left (fun acc arg => Cst.fn (fst (fst arg)) (snd (fst arg)) acc) ds body) } + let app_obj := | ~ = app_obj; ~ = atomic_obj; { Cst.app app_obj atomic_obj } @@ -64,6 +69,14 @@ let params := let param := | "("; x = VAR; ":"; ~ = obj; ")"; { (snd x, obj) } +(* Reversed nonempty list of definitions *) +let let_defns := + | ~ = let_defns; ~ = let_defn; { let_defn :: let_defns } + | ~ = let_defn; { [let_defn] } + +(* (x : A) := t *) +let let_defn := + | "("; ~ = param; ":="; ~ = obj; ")"; { (param, obj) } %% Extract Constant loc => "Lexing.position * Lexing.position". diff --git a/theories/Frontend/parserMessages.messages b/theories/Frontend/parserMessages.messages index 2599b992..bb70207a 100644 --- a/theories/Frontend/parserMessages.messages +++ b/theories/Frontend/parserMessages.messages @@ -1,6 +1,6 @@ prog: INT COLON INT SUCC ## -## Ends in an error in state: 50. +## Ends in an error in state: 61. ## ## prog -> obj COLON obj . EOF [ # ] ## @@ -11,7 +11,7 @@ prog: INT COLON INT SUCC ## This implies that, although the LR(1) items shown above provide an ## accurate view of the past (what has been recognized so far), they ## may provide an INCOMPLETE view of the future (what was expected next). -## In state 22, spurious reduction of production obj -> app_obj +## In state 25, spurious reduction of production obj -> app_obj ## Either an expression or the end of file is expected. @@ -70,7 +70,7 @@ prog: REC RPAREN ## ## Ends in an error in state: 7. ## -## obj -> REC . obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## obj -> REC . obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC @@ -81,7 +81,7 @@ This token is invalid for the beginning of an expression. prog: LAMBDA ZERO ## -## Ends in an error in state: 15. +## Ends in an error in state: 20. ## ## obj -> fnbinder . params ARROW obj [ RPAREN RETURN EOF END COLON BAR ] ## @@ -95,9 +95,9 @@ For example, prog: LAMBDA LPAREN ZERO ## -## Ends in an error in state: 16. +## Ends in an error in state: 13. ## -## param -> LPAREN . VAR COLON obj RPAREN [ LPAREN ARROW ] +## param -> LPAREN . VAR COLON obj RPAREN [ LPAREN EQ ARROW ] ## ## The known suffix of the stack is as follows: ## LPAREN @@ -107,9 +107,9 @@ A parameter should start with a valid identifier. prog: LAMBDA LPAREN VAR ZERO ## -## Ends in an error in state: 17. +## Ends in an error in state: 14. ## -## param -> LPAREN VAR . COLON obj RPAREN [ LPAREN ARROW ] +## param -> LPAREN VAR . COLON obj RPAREN [ LPAREN EQ ARROW ] ## ## The known suffix of the stack is as follows: ## LPAREN VAR @@ -120,9 +120,9 @@ where "?type" is the type of the parameter. prog: LAMBDA LPAREN VAR COLON RPAREN ## -## Ends in an error in state: 18. +## Ends in an error in state: 15. ## -## param -> LPAREN VAR COLON . obj RPAREN [ LPAREN ARROW ] +## param -> LPAREN VAR COLON . obj RPAREN [ LPAREN EQ ARROW ] ## ## The known suffix of the stack is as follows: ## LPAREN VAR COLON @@ -146,7 +146,7 @@ prog: LPAREN RPAREN prog: LPAREN INT DARROW ## -## Ends in an error in state: 13. +## Ends in an error in state: 38. ## ## atomic_obj -> LPAREN obj . RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT EOF END COLON BAR ] ## @@ -157,7 +157,7 @@ prog: LPAREN INT DARROW ## This implies that, although the LR(1) items shown above provide an ## accurate view of the past (what has been recognized so far), they ## may provide an INCOMPLETE view of the future (what was expected next). -## In state 22, spurious reduction of production obj -> app_obj +## In state 25, spurious reduction of production obj -> app_obj ## Either an expression or ")" is expected. @@ -165,9 +165,9 @@ This token is invalid for the beginning of an expression. prog: LAMBDA LPAREN VAR COLON INT DARROW ## -## Ends in an error in state: 19. +## Ends in an error in state: 18. ## -## param -> LPAREN VAR COLON obj . RPAREN [ LPAREN ARROW ] +## param -> LPAREN VAR COLON obj . RPAREN [ LPAREN EQ ARROW ] ## ## The known suffix of the stack is as follows: ## LPAREN VAR COLON obj @@ -176,7 +176,7 @@ prog: LAMBDA LPAREN VAR COLON INT DARROW ## This implies that, although the LR(1) items shown above provide an ## accurate view of the past (what has been recognized so far), they ## may provide an INCOMPLETE view of the future (what was expected next). -## In state 22, spurious reduction of production obj -> app_obj +## In state 25, spurious reduction of production obj -> app_obj ## Either an expression or ")" is expected. @@ -184,7 +184,7 @@ This token is invalid for the beginning of an expression. prog: LAMBDA LPAREN VAR COLON INT RPAREN ZERO ## -## Ends in an error in state: 24. +## Ends in an error in state: 21. ## ## obj -> fnbinder params . ARROW obj [ RPAREN RETURN EOF END COLON BAR ] ## params -> params . param [ LPAREN ARROW ] @@ -197,7 +197,7 @@ prog: LAMBDA LPAREN VAR COLON INT RPAREN ZERO prog: LAMBDA LPAREN VAR COLON INT RPAREN ARROW RPAREN ## -## Ends in an error in state: 25. +## Ends in an error in state: 22. ## ## obj -> fnbinder params ARROW . obj [ RPAREN RETURN EOF END COLON BAR ] ## @@ -210,9 +210,9 @@ This token is invalid for the beginning of an expression. prog: REC INT DARROW ## -## Ends in an error in state: 29. +## Ends in an error in state: 40. ## -## obj -> REC obj . RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## obj -> REC obj . RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj @@ -221,7 +221,7 @@ prog: REC INT DARROW ## This implies that, although the LR(1) items shown above provide an ## accurate view of the past (what has been recognized so far), they ## may provide an INCOMPLETE view of the future (what was expected next). -## In state 22, spurious reduction of production obj -> app_obj +## In state 25, spurious reduction of production obj -> app_obj ## Either an expression or "return" keyword is expected. @@ -229,9 +229,9 @@ This token is invalid for the beginning of an expression. prog: REC INT RETURN ZERO ## -## Ends in an error in state: 30. +## Ends in an error in state: 41. ## -## obj -> REC obj RETURN . VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## obj -> REC obj RETURN . VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj RETURN @@ -241,191 +241,191 @@ A motif should start with a valid identifier. prog: REC INT RETURN VAR ZERO ## -## Ends in an error in state: 31. +## Ends in an error in state: 42. ## -## obj -> REC obj RETURN VAR . ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## obj -> REC obj RETURN VAR . DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj RETURN VAR ## -A motif should have "->" after the scrutinee name. +A motif should have "." after the scrutinee name. -prog: REC INT RETURN VAR ARROW RPAREN +prog: REC INT RETURN VAR DOT RPAREN ## -## Ends in an error in state: 32. +## Ends in an error in state: 43. ## -## obj -> REC obj RETURN VAR ARROW . obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## obj -> REC obj RETURN VAR DOT . obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: -## REC obj RETURN VAR ARROW +## REC obj RETURN VAR DOT ## An expression is expected for a motif. This token is invalid for the beginning of an expression. -prog: REC INT RETURN VAR ARROW INT DARROW +prog: REC INT RETURN VAR DOT INT DARROW ## -## Ends in an error in state: 33. +## Ends in an error in state: 44. ## -## obj -> REC obj RETURN VAR ARROW obj . BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## obj -> REC obj RETURN VAR DOT obj . BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: -## REC obj RETURN VAR ARROW obj +## REC obj RETURN VAR DOT obj ## ## WARNING: This example involves spurious reductions. ## This implies that, although the LR(1) items shown above provide an ## accurate view of the past (what has been recognized so far), they ## may provide an INCOMPLETE view of the future (what was expected next). -## In state 22, spurious reduction of production obj -> app_obj +## In state 25, spurious reduction of production obj -> app_obj ## Either an expression or "|" is expected. This token is invalid for the beginning of an expression. -prog: REC INT RETURN VAR ARROW INT BAR VAR +prog: REC INT RETURN VAR DOT INT BAR VAR ## -## Ends in an error in state: 34. +## Ends in an error in state: 45. ## -## obj -> REC obj RETURN VAR ARROW obj BAR . ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## obj -> REC obj RETURN VAR DOT obj BAR . ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: -## REC obj RETURN VAR ARROW obj BAR +## REC obj RETURN VAR DOT obj BAR ## "zero" is expected for the first branch of "rec". -prog: REC INT RETURN VAR ARROW INT BAR ZERO ZERO +prog: REC INT RETURN VAR DOT INT BAR ZERO ZERO ## -## Ends in an error in state: 35. +## Ends in an error in state: 46. ## -## obj -> REC obj RETURN VAR ARROW obj BAR ZERO . DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO . DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: -## REC obj RETURN VAR ARROW obj BAR ZERO +## REC obj RETURN VAR DOT obj BAR ZERO ## "=>" is expected after a pattern for "rec". -prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW RPAREN +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW RPAREN ## -## Ends in an error in state: 36. +## Ends in an error in state: 47. ## -## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW . obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW . obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: -## REC obj RETURN VAR ARROW obj BAR ZERO DARROW +## REC obj RETURN VAR DOT obj BAR ZERO DARROW ## An expression is expected. This token is invalid for the beginning of an expression. -prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW INT DARROW +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT DARROW ## -## Ends in an error in state: 37. +## Ends in an error in state: 48. ## -## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj . BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj . BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: -## REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj +## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj ## ## WARNING: This example involves spurious reductions. ## This implies that, although the LR(1) items shown above provide an ## accurate view of the past (what has been recognized so far), they ## may provide an INCOMPLETE view of the future (what was expected next). -## In state 22, spurious reduction of production obj -> app_obj +## In state 25, spurious reduction of production obj -> app_obj ## Either an expression or "|" is expected. This token is invalid for the beginning of an expression. -prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW INT BAR ZERO +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR ZERO ## -## Ends in an error in state: 38. +## Ends in an error in state: 49. ## -## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR . SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR . SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: -## REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR +## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR ## "succ" is expected for the second branch of "rec". -prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW INT BAR SUCC ZERO +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC ZERO ## -## Ends in an error in state: 39. +## Ends in an error in state: 50. ## -## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC . VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC . VAR COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: -## REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC +## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC ## An identifier for the predecessor of the scrutinee is expected. -prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW INT BAR SUCC VAR ZERO +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR ZERO ## -## Ends in an error in state: 40. +## Ends in an error in state: 51. ## -## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR . COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR . COMMA VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: -## REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR +## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR ## "," is expected after "succ ?x". -prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW INT BAR SUCC VAR COMMA ZERO +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA ZERO ## -## Ends in an error in state: 41. +## Ends in an error in state: 52. ## -## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA . VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA . VAR DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: -## REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA +## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA ## An identifier for the recursion result is expected. -prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR ZERO +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR ZERO ## -## Ends in an error in state: 42. +## Ends in an error in state: 53. ## -## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR . DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR . DARROW obj END [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: -## REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR +## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR ## "=>" is expected after a pattern for "rec". -prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW RPAREN +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW RPAREN ## -## Ends in an error in state: 43. +## Ends in an error in state: 54. ## -## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW . obj END [ RPAREN RETURN EOF END COLON BAR ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW . obj END [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: -## REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW +## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW ## An expression is expected. This token is invalid for the beginning of an expression. -prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW INT DARROW +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW INT DARROW ## -## Ends in an error in state: 44. +## Ends in an error in state: 55. ## -## obj -> REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj . END [ RPAREN RETURN EOF END COLON BAR ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj . END [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: -## REC obj RETURN VAR ARROW obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj +## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj ## ## WARNING: This example involves spurious reductions. ## This implies that, although the LR(1) items shown above provide an ## accurate view of the past (what has been recognized so far), they ## may provide an INCOMPLETE view of the future (what was expected next). -## In state 22, spurious reduction of production obj -> app_obj +## In state 25, spurious reduction of production obj -> app_obj ## Either an expression or "end" is expected. @@ -433,7 +433,7 @@ This token is invalid for the beginning of an expression. prog: INT DARROW ## -## Ends in an error in state: 48. +## Ends in an error in state: 59. ## ## prog -> obj . COLON obj EOF [ # ] ## @@ -444,7 +444,7 @@ prog: INT DARROW ## This implies that, although the LR(1) items shown above provide an ## accurate view of the past (what has been recognized so far), they ## may provide an INCOMPLETE view of the future (what was expected next). -## In state 22, spurious reduction of production obj -> app_obj +## In state 25, spurious reduction of production obj -> app_obj ## Either an expression or ":" is expected. @@ -452,7 +452,7 @@ This token is invalid for the beginning of an expression. prog: INT COLON RPAREN ## -## Ends in an error in state: 49. +## Ends in an error in state: 60. ## ## prog -> obj COLON . obj EOF [ # ] ## @@ -462,3 +462,94 @@ prog: INT COLON RPAREN An expression is expected. This token is invalid for the beginning of an expression. + +prog: LET ZERO +## +## Ends in an error in state: 11. +## +## obj -> LET . let_defns IN obj [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET +## + +At least one variable binding is expected after a "let" + +prog: LET LPAREN ZERO +## +## Ends in an error in state: 12. +## +## let_defn -> LPAREN . param EQ obj RPAREN [ LPAREN IN ] +## +## The known suffix of the stack is as follows: +## LPAREN +## + +A variable "(x : ?A)" is expected after "let (", where "?A" is a type. + +prog: LET LPAREN LPAREN VAR COLON INT RPAREN ZERO +## +## Ends in an error in state: 29. +## +## let_defn -> LPAREN param . EQ obj RPAREN [ LPAREN IN ] +## +## The known suffix of the stack is as follows: +## LPAREN param +## + +Expected symbol ":=". + +prog: LET LPAREN LPAREN VAR COLON INT RPAREN EQ RPAREN +## +## Ends in an error in state: 30. +## +## let_defn -> LPAREN param EQ . obj RPAREN [ LPAREN IN ] +## +## The known suffix of the stack is as follows: +## LPAREN param EQ +## + +Expected a value for the variable. + +prog: LET LPAREN LPAREN VAR COLON INT RPAREN EQ INT SUCC +## +## Ends in an error in state: 31. +## +## let_defn -> LPAREN param EQ obj . RPAREN [ LPAREN IN ] +## +## The known suffix of the stack is as follows: +## LPAREN param EQ obj +## +## WARNING: This example involves spurious reductions. +## This implies that, although the LR(1) items shown above provide an +## accurate view of the past (what has been recognized so far), they +## may provide an INCOMPLETE view of the future (what was expected next). +## In state 25, spurious reduction of production obj -> app_obj +## + +Expected ")". + +prog: LET LPAREN LPAREN VAR COLON INT RPAREN EQ INT RPAREN ZERO +## +## Ends in an error in state: 33. +## +## let_defns -> let_defns . let_defn [ LPAREN IN ] +## obj -> LET let_defns . IN obj [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET let_defns +## + +Expected keyword "in". + +prog: LET LPAREN LPAREN VAR COLON INT RPAREN EQ INT RPAREN IN RPAREN +## +## Ends in an error in state: 34. +## +## obj -> LET let_defns IN . obj [ RPAREN RETURN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET let_defns IN +## + +Expected expression after "in". \ No newline at end of file