From 18480aa2132b68a227c5b1cdf0321eb05d4b05a7 Mon Sep 17 00:00:00 2001 From: AG-something Date: Tue, 10 Sep 2024 14:52:19 -0400 Subject: [PATCH 1/6] Changed -> to . in recursor --- driver/Lexer.mll | 41 ++++++----- examples/nary.mcl | 8 +-- examples/simple_rec.mcl | 2 +- examples/vector.mcl | 2 +- theories/Frontend/Parser.vy | 4 +- theories/Frontend/parserMessages.messages | 86 +++++++++++------------ 6 files changed, 73 insertions(+), 70 deletions(-) diff --git a/driver/Lexer.mll b/driver/Lexer.mll index cd92ae95..c18957d4 100644 --- a/driver/Lexer.mll +++ b/driver/Lexer.mll @@ -40,29 +40,31 @@ | TYPE _ -> "Type" | VAR (_, s) -> s | EOF _ -> "" + | DOT _ -> "." 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 + | VAR (r, _) -> r let format_token (f: Format.formatter) (t: token): unit = Format.fprintf @@ -99,6 +101,7 @@ rule read = | "Type" { TYPE (get_range lexbuf) } | string { VAR (get_range lexbuf, Lexing.lexeme lexbuf) } | eof { EOF (get_range lexbuf) } + | "." { DOT (get_range 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/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_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/Frontend/Parser.vy b/theories/Frontend/Parser.vy index 18010618..7a3ebe81 100644 --- a/theories/Frontend/Parser.vy +++ b/theories/Frontend/Parser.vy @@ -11,7 +11,7 @@ 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 ARROW "->" AT "@" BAR "|" COLON ":" COMMA "," DARROW "=>" LPAREN "(" RPAREN ")" DOT "." EOF (* symbols *) %start prog %type obj app_obj atomic_obj @@ -34,7 +34,7 @@ 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 } diff --git a/theories/Frontend/parserMessages.messages b/theories/Frontend/parserMessages.messages index d3002c11..c96892b2 100644 --- a/theories/Frontend/parserMessages.messages +++ b/theories/Frontend/parserMessages.messages @@ -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 @@ -212,7 +212,7 @@ prog: REC INT DARROW ## ## Ends in an error in state: 29. ## -## 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 @@ -231,7 +231,7 @@ prog: REC INT RETURN ZERO ## ## Ends in an error in state: 30. ## -## 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 @@ -249,29 +249,29 @@ prog: REC INT RETURN VAR ZERO ## 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. ## -## 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. ## -## 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 @@ -283,51 +283,51 @@ prog: REC INT RETURN VAR ARROW INT DARROW 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. ## -## 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. ## -## 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. ## -## 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. ## -## 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 @@ -339,87 +339,87 @@ prog: REC INT RETURN VAR ARROW INT BAR ZERO DARROW INT DARROW 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. ## -## 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. ## -## 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. ## -## 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. ## -## 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. ## -## 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. ## -## 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. ## -## 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 From 8550eb98c9fcedf06ae77f27ca47fd046599c910 Mon Sep 17 00:00:00 2001 From: AG-something Date: Thu, 12 Sep 2024 10:13:11 -0400 Subject: [PATCH 2/6] Added let-binders --- driver/Lexer.mll | 11 +- driver/Test.ml | 8 + examples/simple_let.mcl | 1 + examples/simple_let.mcl~ | 1 + parserErrors.messages | 0 theories/Frontend/Parser.vy | 7 +- theories/Frontend/par.msg | 511 +++++++++++++++++++++ theories/Frontend/parserErrors.messages | 530 ++++++++++++++++++++++ theories/Frontend/parserErrors.messages~ | 529 +++++++++++++++++++++ theories/Frontend/parserMessages.messages | 196 +++++--- 10 files changed, 1726 insertions(+), 68 deletions(-) create mode 100644 examples/simple_let.mcl create mode 100644 examples/simple_let.mcl~ create mode 100644 parserErrors.messages create mode 100644 theories/Frontend/par.msg create mode 100644 theories/Frontend/parserErrors.messages create mode 100644 theories/Frontend/parserErrors.messages~ diff --git a/driver/Lexer.mll b/driver/Lexer.mll index c18957d4..87bf2332 100644 --- a/driver/Lexer.mll +++ b/driver/Lexer.mll @@ -41,6 +41,9 @@ | VAR (_, s) -> s | EOF _ -> "" | DOT _ -> "." + | LET _ -> "let" + | IN _ -> "in" + | EQ _ -> "=" let get_range_of_token : token -> (position * position) = function @@ -64,6 +67,9 @@ | EOF r | INT (r, _) | DOT r + | LET r + | IN r + | EQ r | VAR (r, _) -> r let format_token (f: Format.formatter) (t: token): unit = @@ -99,9 +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/Test.ml b/driver/Test.ml index c25b8dcd..9e0f29cb 100644 --- a/driver/Test.ml +++ b/driver/Test.ml @@ -48,3 +48,11 @@ let%test "pi missing colon" = parse "pi (x Nat).x" = None let%test "ignore whitespace" = parse "fun (x \n : Type 4).x" = Some (Coq_fn (x, Coq_typ 4, Coq_var x)) + + +(* Tests for let-binders *) +let%test "let" = + parse "let x : Type 2 = Type 1 in x" = Some (Coq_app (Coq_fn (x, Coq_typ 2, Coq_var x), Coq_typ 1) + +let%test "let no type annotation" = + parse "let x = zero in x" = None diff --git a/examples/simple_let.mcl b/examples/simple_let.mcl new file mode 100644 index 00000000..6a8fc07c --- /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_let.mcl~ b/examples/simple_let.mcl~ new file mode 100644 index 00000000..763fba50 --- /dev/null +++ b/examples/simple_let.mcl~ @@ -0,0 +1 @@ +let x : Nat = zero in succ x \ No newline at end of file diff --git a/parserErrors.messages b/parserErrors.messages new file mode 100644 index 00000000..e69de29b diff --git a/theories/Frontend/Parser.vy b/theories/Frontend/Parser.vy index 7a3ebe81..bdf82256 100644 --- a/theories/Frontend/Parser.vy +++ b/theories/Frontend/Parser.vy @@ -10,8 +10,8 @@ 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 ")" DOT "." 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 @@ -40,10 +40,13 @@ let obj := END; { Cst.natrec escr (snd mx) em ez (snd sx) (snd sr) ms } | SUCC; ~ = obj; { Cst.succ obj } + | LET; p = param; "="; arg_obj = obj; IN; fun_obj = obj; { Cst.app (Cst.fn (fst p) (snd p) fun_obj) arg_obj } + let app_obj := | ~ = app_obj; ~ = atomic_obj; { Cst.app app_obj atomic_obj } | ~ = atomic_obj; <> + let atomic_obj := | TYPE; "@"; n = INT; { Cst.typ (snd n) } diff --git a/theories/Frontend/par.msg b/theories/Frontend/par.msg new file mode 100644 index 00000000..0e466968 --- /dev/null +++ b/theories/Frontend/par.msg @@ -0,0 +1,511 @@ +prog: RPAREN +## +## Ends in an error in state: 0. +## +## prog' -> . prog [ # ] +## +## The known suffix of the stack is as follows: +## +## + + + +prog: TYPE ZERO +## +## Ends in an error in state: 3. +## +## atomic_obj -> TYPE . AT INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## TYPE +## + + + +prog: TYPE AT ZERO +## +## Ends in an error in state: 4. +## +## atomic_obj -> TYPE AT . INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## TYPE AT +## + + + +prog: SUCC RPAREN +## +## Ends in an error in state: 6. +## +## obj -> SUCC . obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## SUCC +## + + + +prog: REC RPAREN +## +## Ends in an error in state: 7. +## +## obj -> REC . obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC +## + + + +prog: LPAREN RPAREN +## +## Ends in an error in state: 10. +## +## atomic_obj -> LPAREN . obj RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LPAREN +## + + + +prog: LET ZERO +## +## Ends in an error in state: 11. +## +## obj -> LET . param EQ obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET +## + + + +prog: LAMBDA LPAREN ZERO +## +## Ends in an error in state: 12. +## +## param -> LPAREN . VAR COLON obj RPAREN [ LPAREN EQ ARROW ] +## +## The known suffix of the stack is as follows: +## LPAREN +## + + + +prog: LAMBDA LPAREN VAR ZERO +## +## Ends in an error in state: 13. +## +## param -> LPAREN VAR . COLON obj RPAREN [ LPAREN EQ ARROW ] +## +## The known suffix of the stack is as follows: +## LPAREN VAR +## + + + +prog: LAMBDA LPAREN VAR COLON RPAREN +## +## Ends in an error in state: 14. +## +## param -> LPAREN VAR COLON . obj RPAREN [ LPAREN EQ ARROW ] +## +## The known suffix of the stack is as follows: +## LPAREN VAR COLON +## + + + +prog: LAMBDA LPAREN VAR COLON INT SUCC +## +## Ends in an error in state: 17. +## +## param -> LPAREN VAR COLON obj . RPAREN [ LPAREN EQ ARROW ] +## +## The known suffix of the stack is as follows: +## LPAREN VAR COLON 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 24, spurious reduction of production obj -> app_obj +## + + + +prog: LAMBDA ZERO +## +## Ends in an error in state: 19. +## +## obj -> fnbinder . params ARROW obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## fnbinder +## + + + +prog: LAMBDA LPAREN VAR COLON INT RPAREN ZERO +## +## Ends in an error in state: 20. +## +## obj -> fnbinder params . ARROW obj [ RPAREN RETURN IN EOF END COLON BAR ] +## params -> params . param [ LPAREN ARROW ] +## +## The known suffix of the stack is as follows: +## fnbinder params +## + + + +prog: LAMBDA LPAREN VAR COLON INT RPAREN ARROW RPAREN +## +## Ends in an error in state: 21. +## +## obj -> fnbinder params ARROW . obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## fnbinder params ARROW +## + + + +prog: LET LPAREN VAR COLON INT RPAREN ZERO +## +## Ends in an error in state: 28. +## +## obj -> LET param . EQ obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET param +## + + + +prog: LET LPAREN VAR COLON INT RPAREN EQ RPAREN +## +## Ends in an error in state: 29. +## +## obj -> LET param EQ . obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET param EQ +## + + + +prog: LET LPAREN VAR COLON INT RPAREN EQ INT SUCC +## +## Ends in an error in state: 30. +## +## obj -> LET param EQ obj . IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET 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 24, spurious reduction of production obj -> app_obj +## + + + +prog: LET LPAREN VAR COLON INT RPAREN EQ INT IN RPAREN +## +## Ends in an error in state: 31. +## +## obj -> LET param EQ obj IN . obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET param EQ obj IN +## + + + +prog: LPAREN INT SUCC +## +## Ends in an error in state: 33. +## +## atomic_obj -> LPAREN obj . RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LPAREN 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 24, spurious reduction of production obj -> app_obj +## + + + +prog: REC INT SUCC +## +## Ends in an error in state: 35. +## +## obj -> REC obj . RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC 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 24, spurious reduction of production obj -> app_obj +## + + + +prog: REC INT RETURN ZERO +## +## Ends in an error in state: 36. +## +## obj -> REC obj RETURN . VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN +## + + + +prog: REC INT RETURN VAR ZERO +## +## Ends in an error in state: 37. +## +## obj -> REC obj RETURN VAR . DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR +## + + + +prog: REC INT RETURN VAR DOT RPAREN +## +## Ends in an error in state: 38. +## +## obj -> REC obj RETURN VAR DOT . obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR DOT +## + + + +prog: REC INT RETURN VAR DOT INT SUCC +## +## Ends in an error in state: 39. +## +## obj -> REC obj RETURN VAR DOT obj . BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 24, spurious reduction of production obj -> app_obj +## + + + +prog: REC INT RETURN VAR DOT INT BAR VAR +## +## Ends in an error in state: 40. +## +## obj -> REC obj RETURN VAR DOT obj BAR . ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR DOT obj BAR +## + + + +prog: REC INT RETURN VAR DOT INT BAR ZERO ZERO +## +## Ends in an error in state: 41. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO . DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR DOT obj BAR ZERO +## + + + +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW RPAREN +## +## Ends in an error in state: 42. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW . obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR DOT obj BAR ZERO DARROW +## + + + +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT SUCC +## +## Ends in an error in state: 43. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj . BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 24, spurious reduction of production obj -> app_obj +## + + + +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR ZERO +## +## Ends in an error in state: 44. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR . SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR +## + + + +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC ZERO +## +## Ends in an error in state: 45. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC . VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC +## + + + +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR ZERO +## +## Ends in an error in state: 46. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR . COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR +## + + + +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA ZERO +## +## Ends in an error in state: 47. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA . VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA +## + + + +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR ZERO +## +## Ends in an error in state: 48. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR . DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR +## + + + +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW RPAREN +## +## Ends in an error in state: 49. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW . obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW +## + + + +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW INT SUCC +## +## Ends in an error in state: 50. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj . END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 24, spurious reduction of production obj -> app_obj +## + + + +prog: INT SUCC +## +## Ends in an error in state: 54. +## +## prog -> obj . COLON obj EOF [ # ] +## +## The known suffix of the stack is as follows: +## 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 24, spurious reduction of production obj -> app_obj +## + + + +prog: INT COLON RPAREN +## +## Ends in an error in state: 55. +## +## prog -> obj COLON . obj EOF [ # ] +## +## The known suffix of the stack is as follows: +## obj COLON +## + + + +prog: INT COLON INT SUCC +## +## Ends in an error in state: 56. +## +## prog -> obj COLON obj . EOF [ # ] +## +## The known suffix of the stack is as follows: +## obj COLON 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 24, spurious reduction of production obj -> app_obj +## + + + diff --git a/theories/Frontend/parserErrors.messages b/theories/Frontend/parserErrors.messages new file mode 100644 index 00000000..5f97ee7a --- /dev/null +++ b/theories/Frontend/parserErrors.messages @@ -0,0 +1,530 @@ +prog: INT COLON INT SUCC +## +## Ends in an error in state: 56. +## +## prog -> obj COLON obj . EOF [ # ] +## +## The known suffix of the stack is as follows: +## obj COLON 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 24, spurious reduction of production obj -> app_obj +## + +Either an expression or the end of file is expected. +This token is invalid for the beginning of an expression. + +prog: RPAREN +## +## Ends in an error in state: 0. +## +## prog' -> . prog [ # ] +## +## The known suffix of the stack is as follows: +## +## + +This token is invalid for the beginning of a program. + +prog: TYPE ZERO +## +## Ends in an error in state: 3. +## +## atomic_obj -> TYPE . AT INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## TYPE +## + +"Type" requires "@". + +prog: TYPE AT ZERO +## +## Ends in an error in state: 4. +## +## atomic_obj -> TYPE AT . INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## TYPE AT +## + +"Type" requires "@?level", where "?level" is an arabic numeral. + +prog: SUCC RPAREN +## +## Ends in an error in state: 6. +## +## obj -> SUCC . obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## SUCC +## + +An expression is expected after "succ". +This token is invalid for the beginning of an expression. + +prog: REC RPAREN +## +## Ends in an error in state: 7. +## +## obj -> REC . obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC +## + +An expression is expected after "rec". +This token is invalid for the beginning of an expression. + +prog: LAMBDA ZERO +## +## Ends in an error in state: 19. +## +## obj -> fnbinder . params ARROW obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## fnbinder +## + +"forall" requires a list of parenthesized parameters. +For example, + "(x : Nat) (y : Nat)" in "forall (x : Nat) (y : Nat) -> Nat" + +prog: LAMBDA LPAREN ZERO +## +## Ends in an error in state: 12. +## +## param -> LPAREN . VAR COLON obj RPAREN [ LPAREN EQ ARROW ] +## +## The known suffix of the stack is as follows: +## LPAREN +## + +A parameter should start with a valid identifier. + +prog: LAMBDA LPAREN VAR ZERO +## +## Ends in an error in state: 13. +## +## param -> LPAREN VAR . COLON obj RPAREN [ LPAREN EQ ARROW ] +## +## The known suffix of the stack is as follows: +## LPAREN VAR +## + +A parameter should have ": ?type" after the parameter name, +where "?type" is the type of the parameter. + +prog: LAMBDA LPAREN VAR COLON RPAREN +## +## Ends in an error in state: 14. +## +## param -> LPAREN VAR COLON . obj RPAREN [ LPAREN EQ ARROW ] +## +## The known suffix of the stack is as follows: +## LPAREN VAR COLON +## + +A parameter should have "?type" after ":", +where "?type" is the type of the parameter. + +prog: LPAREN RPAREN +## +## Ends in an error in state: 10. +## +## atomic_obj -> LPAREN . obj RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LPAREN +## + +"()" is an invalid expression. +"()" should have an expression in it to be an expression. + +prog: LPAREN INT DARROW +## +## Ends in an error in state: 33. +## +## atomic_obj -> LPAREN obj . RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LPAREN 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 24, spurious reduction of production obj -> app_obj +## + +Either an expression or ")" is expected. +This token is invalid for the beginning of an expression. + +prog: LAMBDA LPAREN VAR COLON INT DARROW +## +## Ends in an error in state: 17. +## +## param -> LPAREN VAR COLON obj . RPAREN [ LPAREN EQ ARROW ] +## +## The known suffix of the stack is as follows: +## LPAREN VAR COLON 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 24, spurious reduction of production obj -> app_obj +## + +Either an expression or ")" is expected. +This token is invalid for the beginning of an expression. + +prog: LAMBDA LPAREN VAR COLON INT RPAREN ZERO +## +## Ends in an error in state: 20. +## +## obj -> fnbinder params . ARROW obj [ RPAREN RETURN IN EOF END COLON BAR ] +## params -> params . param [ LPAREN ARROW ] +## +## The known suffix of the stack is as follows: +## fnbinder params +## + +"->" or another parameter is expected after a list of parameters for "fun". + +prog: LAMBDA LPAREN VAR COLON INT RPAREN ARROW RPAREN +## +## Ends in an error in state: 21. +## +## obj -> fnbinder params ARROW . obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## fnbinder params ARROW +## + +An expression is expected after "->". +This token is invalid for the beginning of an expression. + +prog: REC INT DARROW +## +## Ends in an error in state: 35. +## +## obj -> REC obj . RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC 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 24, spurious reduction of production obj -> app_obj +## + +Either an expression or "return" keyword is expected. +This token is invalid for the beginning of an expression. + +prog: REC INT RETURN ZERO +## +## Ends in an error in state: 36. +## +## obj -> REC obj RETURN . VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN +## + +A motif should start with a valid identifier. + +prog: REC INT RETURN VAR ZERO +## +## Ends in an error in state: 37. +## +## obj -> REC obj RETURN VAR . DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN 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. + +prog: REC INT RETURN VAR DOT RPAREN +## +## Ends in an error in state: 38. +## +## obj -> REC obj RETURN VAR DOT . obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 DOT INT DARROW +## +## Ends in an error in state: 39. +## +## obj -> REC obj RETURN VAR DOT obj . BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 24, 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 DOT INT BAR VAR +## +## Ends in an error in state: 40. +## +## obj -> REC obj RETURN VAR DOT obj BAR . ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR DOT obj BAR +## + +"zero" is expected for the first branch of "rec". + +prog: REC INT RETURN VAR DOT INT BAR ZERO ZERO +## +## Ends in an error in state: 41. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO . DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR DOT obj BAR ZERO +## + +"=>" is expected after a pattern for "rec". + +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW RPAREN +## +## Ends in an error in state: 42. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW . obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 DOT INT BAR ZERO DARROW INT DARROW +## +## Ends in an error in state: 43. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj . BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 24, 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 DOT INT BAR ZERO DARROW INT BAR ZERO +## +## Ends in an error in state: 44. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR . SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 DOT INT BAR ZERO DARROW INT BAR SUCC ZERO +## +## Ends in an error in state: 45. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC . VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 DOT INT BAR ZERO DARROW INT BAR SUCC VAR ZERO +## +## Ends in an error in state: 46. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR . COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR +## + +"," is expected after "succ ?x". + +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA ZERO +## +## Ends in an error in state: 47. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA . VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR ZERO +## +## Ends in an error in state: 48. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR . DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW RPAREN +## +## Ends in an error in state: 49. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW . obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW INT DARROW +## +## Ends in an error in state: 50. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj . END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 24, spurious reduction of production obj -> app_obj +## + +Either an expression or "end" is expected. +This token is invalid for the beginning of an expression. + +prog: INT DARROW +## +## Ends in an error in state: 54. +## +## prog -> obj . COLON obj EOF [ # ] +## +## The known suffix of the stack is as follows: +## 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 24, spurious reduction of production obj -> app_obj +## + +Either an expression or ":" is expected. +This token is invalid for the beginning of an expression. + +prog: INT COLON RPAREN +## +## Ends in an error in state: 55. +## +## prog -> obj COLON . obj EOF [ # ] +## +## The known suffix of the stack is as follows: +## obj COLON +## + +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 . param EQ obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET +## + + + +prog: LET LPAREN VAR COLON INT RPAREN ZERO +## +## Ends in an error in state: 28. +## +## obj -> LET param . EQ obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET param +## + + + +prog: LET LPAREN VAR COLON INT RPAREN EQ RPAREN +## +## Ends in an error in state: 29. +## +## obj -> LET param EQ . obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET param EQ +## + + + +prog: LET LPAREN VAR COLON INT RPAREN EQ INT SUCC +## +## Ends in an error in state: 30. +## +## obj -> LET param EQ obj . IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET 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 24, spurious reduction of production obj -> app_obj +## + + + +prog: LET LPAREN VAR COLON INT RPAREN EQ INT IN RPAREN +## +## Ends in an error in state: 31. +## +## obj -> LET param EQ obj IN . obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET param EQ obj IN +## + + diff --git a/theories/Frontend/parserErrors.messages~ b/theories/Frontend/parserErrors.messages~ new file mode 100644 index 00000000..15e566c8 --- /dev/null +++ b/theories/Frontend/parserErrors.messages~ @@ -0,0 +1,529 @@ +prog: INT COLON INT SUCC +## +## Ends in an error in state: 56. +## +## prog -> obj COLON obj . EOF [ # ] +## +## The known suffix of the stack is as follows: +## obj COLON 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 24, spurious reduction of production obj -> app_obj +## + +Either an expression or the end of file is expected. +This token is invalid for the beginning of an expression. + +prog: RPAREN +## +## Ends in an error in state: 0. +## +## prog' -> . prog [ # ] +## +## The known suffix of the stack is as follows: +## +## + +This token is invalid for the beginning of a program. + +prog: TYPE ZERO +## +## Ends in an error in state: 3. +## +## atomic_obj -> TYPE . AT INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## TYPE +## + +"Type" requires "@". + +prog: TYPE AT ZERO +## +## Ends in an error in state: 4. +## +## atomic_obj -> TYPE AT . INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## TYPE AT +## + +"Type" requires "@?level", where "?level" is an arabic numeral. + +prog: SUCC RPAREN +## +## Ends in an error in state: 6. +## +## obj -> SUCC . obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## SUCC +## + +An expression is expected after "succ". +This token is invalid for the beginning of an expression. + +prog: REC RPAREN +## +## Ends in an error in state: 7. +## +## obj -> REC . obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC +## + +An expression is expected after "rec". +This token is invalid for the beginning of an expression. + +prog: LAMBDA ZERO +## +## Ends in an error in state: 19. +## +## obj -> fnbinder . params ARROW obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## fnbinder +## + +"forall" requires a list of parenthesized parameters. +For example, + "(x : Nat) (y : Nat)" in "forall (x : Nat) (y : Nat) -> Nat" + +prog: LAMBDA LPAREN ZERO +## +## Ends in an error in state: 12. +## +## param -> LPAREN . VAR COLON obj RPAREN [ LPAREN EQ ARROW ] +## +## The known suffix of the stack is as follows: +## LPAREN +## + +A parameter should start with a valid identifier. + +prog: LAMBDA LPAREN VAR ZERO +## +## Ends in an error in state: 13. +## +## param -> LPAREN VAR . COLON obj RPAREN [ LPAREN EQ ARROW ] +## +## The known suffix of the stack is as follows: +## LPAREN VAR +## + +A parameter should have ": ?type" after the parameter name, +where "?type" is the type of the parameter. + +prog: LAMBDA LPAREN VAR COLON RPAREN +## +## Ends in an error in state: 14. +## +## param -> LPAREN VAR COLON . obj RPAREN [ LPAREN EQ ARROW ] +## +## The known suffix of the stack is as follows: +## LPAREN VAR COLON +## + +A parameter should have "?type" after ":", +where "?type" is the type of the parameter. + +prog: LPAREN RPAREN +## +## Ends in an error in state: 10. +## +## atomic_obj -> LPAREN . obj RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LPAREN +## + +"()" is an invalid expression. +"()" should have an expression in it to be an expression. + +prog: LPAREN INT DARROW +## +## Ends in an error in state: 33. +## +## atomic_obj -> LPAREN obj . RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LPAREN 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 24, spurious reduction of production obj -> app_obj +## + +Either an expression or ")" is expected. +This token is invalid for the beginning of an expression. + +prog: LAMBDA LPAREN VAR COLON INT DARROW +## +## Ends in an error in state: 17. +## +## param -> LPAREN VAR COLON obj . RPAREN [ LPAREN EQ ARROW ] +## +## The known suffix of the stack is as follows: +## LPAREN VAR COLON 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 24, spurious reduction of production obj -> app_obj +## + +Either an expression or ")" is expected. +This token is invalid for the beginning of an expression. + +prog: LAMBDA LPAREN VAR COLON INT RPAREN ZERO +## +## Ends in an error in state: 20. +## +## obj -> fnbinder params . ARROW obj [ RPAREN RETURN IN EOF END COLON BAR ] +## params -> params . param [ LPAREN ARROW ] +## +## The known suffix of the stack is as follows: +## fnbinder params +## + +"->" or another parameter is expected after a list of parameters for "fun". + +prog: LAMBDA LPAREN VAR COLON INT RPAREN ARROW RPAREN +## +## Ends in an error in state: 21. +## +## obj -> fnbinder params ARROW . obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## fnbinder params ARROW +## + +An expression is expected after "->". +This token is invalid for the beginning of an expression. + +prog: REC INT DARROW +## +## Ends in an error in state: 35. +## +## obj -> REC obj . RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC 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 24, spurious reduction of production obj -> app_obj +## + +Either an expression or "return" keyword is expected. +This token is invalid for the beginning of an expression. + +prog: REC INT RETURN ZERO +## +## Ends in an error in state: 36. +## +## obj -> REC obj RETURN . VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN +## + +A motif should start with a valid identifier. + +prog: REC INT RETURN VAR ZERO +## +## Ends in an error in state: 37. +## +## obj -> REC obj RETURN VAR . DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN 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. + +prog: REC INT RETURN VAR DOT RPAREN +## +## Ends in an error in state: 38. +## +## obj -> REC obj RETURN VAR DOT . obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 DOT INT DARROW +## +## Ends in an error in state: 39. +## +## obj -> REC obj RETURN VAR DOT obj . BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 24, 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 DOT INT BAR VAR +## +## Ends in an error in state: 40. +## +## obj -> REC obj RETURN VAR DOT obj BAR . ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR DOT obj BAR +## + +"zero" is expected for the first branch of "rec". + +prog: REC INT RETURN VAR DOT INT BAR ZERO ZERO +## +## Ends in an error in state: 41. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO . DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR DOT obj BAR ZERO +## + +"=>" is expected after a pattern for "rec". + +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW RPAREN +## +## Ends in an error in state: 42. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW . obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 DOT INT BAR ZERO DARROW INT DARROW +## +## Ends in an error in state: 43. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj . BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 24, 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 DOT INT BAR ZERO DARROW INT BAR ZERO +## +## Ends in an error in state: 44. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR . SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 DOT INT BAR ZERO DARROW INT BAR SUCC ZERO +## +## Ends in an error in state: 45. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC . VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 DOT INT BAR ZERO DARROW INT BAR SUCC VAR ZERO +## +## Ends in an error in state: 46. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR . COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR +## + +"," is expected after "succ ?x". + +prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA ZERO +## +## Ends in an error in state: 47. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA . VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR ZERO +## +## Ends in an error in state: 48. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR . DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW RPAREN +## +## Ends in an error in state: 49. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW . obj END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW INT DARROW +## +## Ends in an error in state: 50. +## +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj . END [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## 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 24, spurious reduction of production obj -> app_obj +## + +Either an expression or "end" is expected. +This token is invalid for the beginning of an expression. + +prog: INT DARROW +## +## Ends in an error in state: 54. +## +## prog -> obj . COLON obj EOF [ # ] +## +## The known suffix of the stack is as follows: +## 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 24, spurious reduction of production obj -> app_obj +## + +Either an expression or ":" is expected. +This token is invalid for the beginning of an expression. + +prog: INT COLON RPAREN +## +## Ends in an error in state: 55. +## +## prog -> obj COLON . obj EOF [ # ] +## +## The known suffix of the stack is as follows: +## obj COLON +## + +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 . param EQ obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET +## + + + +prog: LET LPAREN VAR COLON INT RPAREN ZERO +## +## Ends in an error in state: 28. +## +## obj -> LET param . EQ obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET param +## + + + +prog: LET LPAREN VAR COLON INT RPAREN EQ RPAREN +## +## Ends in an error in state: 29. +## +## obj -> LET param EQ . obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET param EQ +## + + + +prog: LET LPAREN VAR COLON INT RPAREN EQ INT SUCC +## +## Ends in an error in state: 30. +## +## obj -> LET param EQ obj . IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET 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 24, spurious reduction of production obj -> app_obj +## + + + +prog: LET LPAREN VAR COLON INT RPAREN EQ INT IN RPAREN +## +## Ends in an error in state: 31. +## +## obj -> LET param EQ obj IN . obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET param EQ obj IN +## + + diff --git a/theories/Frontend/parserMessages.messages b/theories/Frontend/parserMessages.messages index c96892b2..5f97ee7a 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: 56. ## ## 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 24, spurious reduction of production obj -> app_obj ## Either an expression or the end of file is expected. @@ -33,7 +33,7 @@ prog: TYPE ZERO ## ## Ends in an error in state: 3. ## -## atomic_obj -> TYPE . AT INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT EOF END COLON BAR ] +## atomic_obj -> TYPE . AT INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## TYPE @@ -45,7 +45,7 @@ prog: TYPE AT ZERO ## ## Ends in an error in state: 4. ## -## atomic_obj -> TYPE AT . INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT EOF END COLON BAR ] +## atomic_obj -> TYPE AT . INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## TYPE AT @@ -57,7 +57,7 @@ prog: SUCC RPAREN ## ## Ends in an error in state: 6. ## -## obj -> SUCC . obj [ RPAREN RETURN EOF END COLON BAR ] +## obj -> SUCC . obj [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## SUCC @@ -70,7 +70,7 @@ prog: REC RPAREN ## ## Ends in an error in state: 7. ## -## 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 ] +## obj -> REC . obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC @@ -81,9 +81,9 @@ 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: 19. ## -## obj -> fnbinder . params ARROW obj [ RPAREN RETURN EOF END COLON BAR ] +## obj -> fnbinder . params ARROW obj [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## fnbinder @@ -95,9 +95,9 @@ For example, prog: LAMBDA LPAREN ZERO ## -## Ends in an error in state: 16. +## Ends in an error in state: 12. ## -## 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: 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 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: 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 COLON @@ -135,7 +135,7 @@ prog: LPAREN RPAREN ## ## Ends in an error in state: 10. ## -## atomic_obj -> LPAREN . obj RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT EOF END COLON BAR ] +## atomic_obj -> LPAREN . obj RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## LPAREN @@ -146,9 +146,9 @@ prog: LPAREN RPAREN prog: LPAREN INT DARROW ## -## Ends in an error in state: 13. +## Ends in an error in state: 33. ## -## atomic_obj -> LPAREN obj . RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT EOF END COLON BAR ] +## atomic_obj -> LPAREN obj . RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## LPAREN obj @@ -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 24, 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: 17. ## -## 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 24, spurious reduction of production obj -> app_obj ## Either an expression or ")" is expected. @@ -184,9 +184,9 @@ 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: 20. ## -## obj -> fnbinder params . ARROW obj [ RPAREN RETURN EOF END COLON BAR ] +## obj -> fnbinder params . ARROW obj [ RPAREN RETURN IN EOF END COLON BAR ] ## params -> params . param [ LPAREN ARROW ] ## ## The known suffix of the stack is as follows: @@ -197,9 +197,9 @@ 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: 21. ## -## obj -> fnbinder params ARROW . obj [ RPAREN RETURN EOF END COLON BAR ] +## obj -> fnbinder params ARROW . obj [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## fnbinder params ARROW @@ -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: 35. ## -## 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 ] +## obj -> REC obj . RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN 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 24, 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: 36. ## -## 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 ] +## obj -> REC obj RETURN . VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj RETURN @@ -241,9 +241,9 @@ 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: 37. ## -## 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 IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj RETURN VAR @@ -253,9 +253,9 @@ A motif should have "." after the scrutinee name. prog: REC INT RETURN VAR DOT RPAREN ## -## Ends in an error in state: 32. +## Ends in an error in state: 38. ## -## 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 ] +## obj -> REC obj RETURN VAR DOT . obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj RETURN VAR DOT @@ -266,9 +266,9 @@ This token is invalid for the beginning of an expression. prog: REC INT RETURN VAR DOT INT DARROW ## -## Ends in an error in state: 33. +## Ends in an error in state: 39. ## -## 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 ] +## obj -> REC obj RETURN VAR DOT obj . BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj RETURN VAR DOT obj @@ -277,7 +277,7 @@ prog: REC INT RETURN VAR DOT 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 24, spurious reduction of production obj -> app_obj ## Either an expression or "|" is expected. @@ -285,9 +285,9 @@ This token is invalid for the beginning of an expression. prog: REC INT RETURN VAR DOT INT BAR VAR ## -## Ends in an error in state: 34. +## Ends in an error in state: 40. ## -## 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 ] +## obj -> REC obj RETURN VAR DOT obj BAR . ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj RETURN VAR DOT obj BAR @@ -297,9 +297,9 @@ prog: REC INT RETURN VAR DOT INT BAR VAR prog: REC INT RETURN VAR DOT INT BAR ZERO ZERO ## -## Ends in an error in state: 35. +## Ends in an error in state: 41. ## -## 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 ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO . DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj RETURN VAR DOT obj BAR ZERO @@ -309,9 +309,9 @@ prog: REC INT RETURN VAR DOT INT BAR ZERO ZERO prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW RPAREN ## -## Ends in an error in state: 36. +## Ends in an error in state: 42. ## -## 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 ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW . obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj RETURN VAR DOT obj BAR ZERO DARROW @@ -322,9 +322,9 @@ This token is invalid for the beginning of an expression. 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: 43. ## -## 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 ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj . BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj @@ -333,7 +333,7 @@ prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW 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 24, spurious reduction of production obj -> app_obj ## Either an expression or "|" is expected. @@ -341,9 +341,9 @@ This token is invalid for the beginning of an expression. 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: 44. ## -## 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 ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR . SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR @@ -353,9 +353,9 @@ prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR 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: 45. ## -## 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 ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC . VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC @@ -365,9 +365,9 @@ An identifier for the predecessor of the scrutinee is expected. 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: 46. ## -## 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 ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR . COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR @@ -377,9 +377,9 @@ prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR 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: 47. ## -## 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 ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA . VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA @@ -389,9 +389,9 @@ An identifier for the recursion result is expected. 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: 48. ## -## 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 ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR . DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR @@ -401,9 +401,9 @@ prog: REC INT RETURN VAR DOT 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 DARROW RPAREN ## -## Ends in an error in state: 43. +## Ends in an error in state: 49. ## -## 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 ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW . obj END [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW @@ -414,9 +414,9 @@ This token is invalid for the beginning of an expression. 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: 50. ## -## 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 ] +## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj . END [ RPAREN RETURN IN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj @@ -425,7 +425,7 @@ prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARR ## 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 24, 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: 54. ## ## 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 24, 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: 55. ## ## prog -> obj COLON . obj EOF [ # ] ## @@ -461,4 +461,70 @@ prog: INT COLON RPAREN ## An expression is expected. -This token is invalid for the beginning of an expression. \ No newline at end of file +This token is invalid for the beginning of an expression. + +prog: LET ZERO +## +## Ends in an error in state: 11. +## +## obj -> LET . param EQ obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET +## + + + +prog: LET LPAREN VAR COLON INT RPAREN ZERO +## +## Ends in an error in state: 28. +## +## obj -> LET param . EQ obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET param +## + + + +prog: LET LPAREN VAR COLON INT RPAREN EQ RPAREN +## +## Ends in an error in state: 29. +## +## obj -> LET param EQ . obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET param EQ +## + + + +prog: LET LPAREN VAR COLON INT RPAREN EQ INT SUCC +## +## Ends in an error in state: 30. +## +## obj -> LET param EQ obj . IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET 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 24, spurious reduction of production obj -> app_obj +## + + + +prog: LET LPAREN VAR COLON INT RPAREN EQ INT IN RPAREN +## +## Ends in an error in state: 31. +## +## obj -> LET param EQ obj IN . obj [ RPAREN RETURN IN EOF END COLON BAR ] +## +## The known suffix of the stack is as follows: +## LET param EQ obj IN +## + + From b9559a25418b045115f76759e173b9e3309a6d62 Mon Sep 17 00:00:00 2001 From: AG-something Date: Thu, 12 Sep 2024 10:23:02 -0400 Subject: [PATCH 3/6] Added error messages for bad let-bindings --- examples/simple_let.mcl~ | 1 - parserErrors.messages | 0 theories/Frontend/par.msg | 511 --------------------- theories/Frontend/parserErrors.messages | 530 ---------------------- theories/Frontend/parserErrors.messages~ | 529 --------------------- theories/Frontend/parserMessages.messages | 10 +- 6 files changed, 5 insertions(+), 1576 deletions(-) delete mode 100644 examples/simple_let.mcl~ delete mode 100644 parserErrors.messages delete mode 100644 theories/Frontend/par.msg delete mode 100644 theories/Frontend/parserErrors.messages delete mode 100644 theories/Frontend/parserErrors.messages~ diff --git a/examples/simple_let.mcl~ b/examples/simple_let.mcl~ deleted file mode 100644 index 763fba50..00000000 --- a/examples/simple_let.mcl~ +++ /dev/null @@ -1 +0,0 @@ -let x : Nat = zero in succ x \ No newline at end of file diff --git a/parserErrors.messages b/parserErrors.messages deleted file mode 100644 index e69de29b..00000000 diff --git a/theories/Frontend/par.msg b/theories/Frontend/par.msg deleted file mode 100644 index 0e466968..00000000 --- a/theories/Frontend/par.msg +++ /dev/null @@ -1,511 +0,0 @@ -prog: RPAREN -## -## Ends in an error in state: 0. -## -## prog' -> . prog [ # ] -## -## The known suffix of the stack is as follows: -## -## - - - -prog: TYPE ZERO -## -## Ends in an error in state: 3. -## -## atomic_obj -> TYPE . AT INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## TYPE -## - - - -prog: TYPE AT ZERO -## -## Ends in an error in state: 4. -## -## atomic_obj -> TYPE AT . INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## TYPE AT -## - - - -prog: SUCC RPAREN -## -## Ends in an error in state: 6. -## -## obj -> SUCC . obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## SUCC -## - - - -prog: REC RPAREN -## -## Ends in an error in state: 7. -## -## obj -> REC . obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC -## - - - -prog: LPAREN RPAREN -## -## Ends in an error in state: 10. -## -## atomic_obj -> LPAREN . obj RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LPAREN -## - - - -prog: LET ZERO -## -## Ends in an error in state: 11. -## -## obj -> LET . param EQ obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LET -## - - - -prog: LAMBDA LPAREN ZERO -## -## Ends in an error in state: 12. -## -## param -> LPAREN . VAR COLON obj RPAREN [ LPAREN EQ ARROW ] -## -## The known suffix of the stack is as follows: -## LPAREN -## - - - -prog: LAMBDA LPAREN VAR ZERO -## -## Ends in an error in state: 13. -## -## param -> LPAREN VAR . COLON obj RPAREN [ LPAREN EQ ARROW ] -## -## The known suffix of the stack is as follows: -## LPAREN VAR -## - - - -prog: LAMBDA LPAREN VAR COLON RPAREN -## -## Ends in an error in state: 14. -## -## param -> LPAREN VAR COLON . obj RPAREN [ LPAREN EQ ARROW ] -## -## The known suffix of the stack is as follows: -## LPAREN VAR COLON -## - - - -prog: LAMBDA LPAREN VAR COLON INT SUCC -## -## Ends in an error in state: 17. -## -## param -> LPAREN VAR COLON obj . RPAREN [ LPAREN EQ ARROW ] -## -## The known suffix of the stack is as follows: -## LPAREN VAR COLON 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 24, spurious reduction of production obj -> app_obj -## - - - -prog: LAMBDA ZERO -## -## Ends in an error in state: 19. -## -## obj -> fnbinder . params ARROW obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## fnbinder -## - - - -prog: LAMBDA LPAREN VAR COLON INT RPAREN ZERO -## -## Ends in an error in state: 20. -## -## obj -> fnbinder params . ARROW obj [ RPAREN RETURN IN EOF END COLON BAR ] -## params -> params . param [ LPAREN ARROW ] -## -## The known suffix of the stack is as follows: -## fnbinder params -## - - - -prog: LAMBDA LPAREN VAR COLON INT RPAREN ARROW RPAREN -## -## Ends in an error in state: 21. -## -## obj -> fnbinder params ARROW . obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## fnbinder params ARROW -## - - - -prog: LET LPAREN VAR COLON INT RPAREN ZERO -## -## Ends in an error in state: 28. -## -## obj -> LET param . EQ obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LET param -## - - - -prog: LET LPAREN VAR COLON INT RPAREN EQ RPAREN -## -## Ends in an error in state: 29. -## -## obj -> LET param EQ . obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LET param EQ -## - - - -prog: LET LPAREN VAR COLON INT RPAREN EQ INT SUCC -## -## Ends in an error in state: 30. -## -## obj -> LET param EQ obj . IN obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LET 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 24, spurious reduction of production obj -> app_obj -## - - - -prog: LET LPAREN VAR COLON INT RPAREN EQ INT IN RPAREN -## -## Ends in an error in state: 31. -## -## obj -> LET param EQ obj IN . obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LET param EQ obj IN -## - - - -prog: LPAREN INT SUCC -## -## Ends in an error in state: 33. -## -## atomic_obj -> LPAREN obj . RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LPAREN 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 24, spurious reduction of production obj -> app_obj -## - - - -prog: REC INT SUCC -## -## Ends in an error in state: 35. -## -## obj -> REC obj . RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC 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 24, spurious reduction of production obj -> app_obj -## - - - -prog: REC INT RETURN ZERO -## -## Ends in an error in state: 36. -## -## obj -> REC obj RETURN . VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN -## - - - -prog: REC INT RETURN VAR ZERO -## -## Ends in an error in state: 37. -## -## obj -> REC obj RETURN VAR . DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN VAR -## - - - -prog: REC INT RETURN VAR DOT RPAREN -## -## Ends in an error in state: 38. -## -## obj -> REC obj RETURN VAR DOT . obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN VAR DOT -## - - - -prog: REC INT RETURN VAR DOT INT SUCC -## -## Ends in an error in state: 39. -## -## obj -> REC obj RETURN VAR DOT obj . BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 24, spurious reduction of production obj -> app_obj -## - - - -prog: REC INT RETURN VAR DOT INT BAR VAR -## -## Ends in an error in state: 40. -## -## obj -> REC obj RETURN VAR DOT obj BAR . ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN VAR DOT obj BAR -## - - - -prog: REC INT RETURN VAR DOT INT BAR ZERO ZERO -## -## Ends in an error in state: 41. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO . DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN VAR DOT obj BAR ZERO -## - - - -prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW RPAREN -## -## Ends in an error in state: 42. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW . obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN VAR DOT obj BAR ZERO DARROW -## - - - -prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT SUCC -## -## Ends in an error in state: 43. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj . BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 24, spurious reduction of production obj -> app_obj -## - - - -prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR ZERO -## -## Ends in an error in state: 44. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR . SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR -## - - - -prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC ZERO -## -## Ends in an error in state: 45. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC . VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC -## - - - -prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR ZERO -## -## Ends in an error in state: 46. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR . COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR -## - - - -prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA ZERO -## -## Ends in an error in state: 47. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA . VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA -## - - - -prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR ZERO -## -## Ends in an error in state: 48. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR . DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR -## - - - -prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW RPAREN -## -## Ends in an error in state: 49. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW . obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW -## - - - -prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW INT SUCC -## -## Ends in an error in state: 50. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj . END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 24, spurious reduction of production obj -> app_obj -## - - - -prog: INT SUCC -## -## Ends in an error in state: 54. -## -## prog -> obj . COLON obj EOF [ # ] -## -## The known suffix of the stack is as follows: -## 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 24, spurious reduction of production obj -> app_obj -## - - - -prog: INT COLON RPAREN -## -## Ends in an error in state: 55. -## -## prog -> obj COLON . obj EOF [ # ] -## -## The known suffix of the stack is as follows: -## obj COLON -## - - - -prog: INT COLON INT SUCC -## -## Ends in an error in state: 56. -## -## prog -> obj COLON obj . EOF [ # ] -## -## The known suffix of the stack is as follows: -## obj COLON 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 24, spurious reduction of production obj -> app_obj -## - - - diff --git a/theories/Frontend/parserErrors.messages b/theories/Frontend/parserErrors.messages deleted file mode 100644 index 5f97ee7a..00000000 --- a/theories/Frontend/parserErrors.messages +++ /dev/null @@ -1,530 +0,0 @@ -prog: INT COLON INT SUCC -## -## Ends in an error in state: 56. -## -## prog -> obj COLON obj . EOF [ # ] -## -## The known suffix of the stack is as follows: -## obj COLON 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 24, spurious reduction of production obj -> app_obj -## - -Either an expression or the end of file is expected. -This token is invalid for the beginning of an expression. - -prog: RPAREN -## -## Ends in an error in state: 0. -## -## prog' -> . prog [ # ] -## -## The known suffix of the stack is as follows: -## -## - -This token is invalid for the beginning of a program. - -prog: TYPE ZERO -## -## Ends in an error in state: 3. -## -## atomic_obj -> TYPE . AT INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## TYPE -## - -"Type" requires "@". - -prog: TYPE AT ZERO -## -## Ends in an error in state: 4. -## -## atomic_obj -> TYPE AT . INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## TYPE AT -## - -"Type" requires "@?level", where "?level" is an arabic numeral. - -prog: SUCC RPAREN -## -## Ends in an error in state: 6. -## -## obj -> SUCC . obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## SUCC -## - -An expression is expected after "succ". -This token is invalid for the beginning of an expression. - -prog: REC RPAREN -## -## Ends in an error in state: 7. -## -## obj -> REC . obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC -## - -An expression is expected after "rec". -This token is invalid for the beginning of an expression. - -prog: LAMBDA ZERO -## -## Ends in an error in state: 19. -## -## obj -> fnbinder . params ARROW obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## fnbinder -## - -"forall" requires a list of parenthesized parameters. -For example, - "(x : Nat) (y : Nat)" in "forall (x : Nat) (y : Nat) -> Nat" - -prog: LAMBDA LPAREN ZERO -## -## Ends in an error in state: 12. -## -## param -> LPAREN . VAR COLON obj RPAREN [ LPAREN EQ ARROW ] -## -## The known suffix of the stack is as follows: -## LPAREN -## - -A parameter should start with a valid identifier. - -prog: LAMBDA LPAREN VAR ZERO -## -## Ends in an error in state: 13. -## -## param -> LPAREN VAR . COLON obj RPAREN [ LPAREN EQ ARROW ] -## -## The known suffix of the stack is as follows: -## LPAREN VAR -## - -A parameter should have ": ?type" after the parameter name, -where "?type" is the type of the parameter. - -prog: LAMBDA LPAREN VAR COLON RPAREN -## -## Ends in an error in state: 14. -## -## param -> LPAREN VAR COLON . obj RPAREN [ LPAREN EQ ARROW ] -## -## The known suffix of the stack is as follows: -## LPAREN VAR COLON -## - -A parameter should have "?type" after ":", -where "?type" is the type of the parameter. - -prog: LPAREN RPAREN -## -## Ends in an error in state: 10. -## -## atomic_obj -> LPAREN . obj RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LPAREN -## - -"()" is an invalid expression. -"()" should have an expression in it to be an expression. - -prog: LPAREN INT DARROW -## -## Ends in an error in state: 33. -## -## atomic_obj -> LPAREN obj . RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LPAREN 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 24, spurious reduction of production obj -> app_obj -## - -Either an expression or ")" is expected. -This token is invalid for the beginning of an expression. - -prog: LAMBDA LPAREN VAR COLON INT DARROW -## -## Ends in an error in state: 17. -## -## param -> LPAREN VAR COLON obj . RPAREN [ LPAREN EQ ARROW ] -## -## The known suffix of the stack is as follows: -## LPAREN VAR COLON 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 24, spurious reduction of production obj -> app_obj -## - -Either an expression or ")" is expected. -This token is invalid for the beginning of an expression. - -prog: LAMBDA LPAREN VAR COLON INT RPAREN ZERO -## -## Ends in an error in state: 20. -## -## obj -> fnbinder params . ARROW obj [ RPAREN RETURN IN EOF END COLON BAR ] -## params -> params . param [ LPAREN ARROW ] -## -## The known suffix of the stack is as follows: -## fnbinder params -## - -"->" or another parameter is expected after a list of parameters for "fun". - -prog: LAMBDA LPAREN VAR COLON INT RPAREN ARROW RPAREN -## -## Ends in an error in state: 21. -## -## obj -> fnbinder params ARROW . obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## fnbinder params ARROW -## - -An expression is expected after "->". -This token is invalid for the beginning of an expression. - -prog: REC INT DARROW -## -## Ends in an error in state: 35. -## -## obj -> REC obj . RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC 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 24, spurious reduction of production obj -> app_obj -## - -Either an expression or "return" keyword is expected. -This token is invalid for the beginning of an expression. - -prog: REC INT RETURN ZERO -## -## Ends in an error in state: 36. -## -## obj -> REC obj RETURN . VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN -## - -A motif should start with a valid identifier. - -prog: REC INT RETURN VAR ZERO -## -## Ends in an error in state: 37. -## -## obj -> REC obj RETURN VAR . DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN 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. - -prog: REC INT RETURN VAR DOT RPAREN -## -## Ends in an error in state: 38. -## -## obj -> REC obj RETURN VAR DOT . obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 DOT INT DARROW -## -## Ends in an error in state: 39. -## -## obj -> REC obj RETURN VAR DOT obj . BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 24, 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 DOT INT BAR VAR -## -## Ends in an error in state: 40. -## -## obj -> REC obj RETURN VAR DOT obj BAR . ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN VAR DOT obj BAR -## - -"zero" is expected for the first branch of "rec". - -prog: REC INT RETURN VAR DOT INT BAR ZERO ZERO -## -## Ends in an error in state: 41. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO . DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN VAR DOT obj BAR ZERO -## - -"=>" is expected after a pattern for "rec". - -prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW RPAREN -## -## Ends in an error in state: 42. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW . obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 DOT INT BAR ZERO DARROW INT DARROW -## -## Ends in an error in state: 43. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj . BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 24, 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 DOT INT BAR ZERO DARROW INT BAR ZERO -## -## Ends in an error in state: 44. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR . SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 DOT INT BAR ZERO DARROW INT BAR SUCC ZERO -## -## Ends in an error in state: 45. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC . VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 DOT INT BAR ZERO DARROW INT BAR SUCC VAR ZERO -## -## Ends in an error in state: 46. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR . COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR -## - -"," is expected after "succ ?x". - -prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA ZERO -## -## Ends in an error in state: 47. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA . VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR ZERO -## -## Ends in an error in state: 48. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR . DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW RPAREN -## -## Ends in an error in state: 49. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW . obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW INT DARROW -## -## Ends in an error in state: 50. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj . END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 24, spurious reduction of production obj -> app_obj -## - -Either an expression or "end" is expected. -This token is invalid for the beginning of an expression. - -prog: INT DARROW -## -## Ends in an error in state: 54. -## -## prog -> obj . COLON obj EOF [ # ] -## -## The known suffix of the stack is as follows: -## 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 24, spurious reduction of production obj -> app_obj -## - -Either an expression or ":" is expected. -This token is invalid for the beginning of an expression. - -prog: INT COLON RPAREN -## -## Ends in an error in state: 55. -## -## prog -> obj COLON . obj EOF [ # ] -## -## The known suffix of the stack is as follows: -## obj COLON -## - -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 . param EQ obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LET -## - - - -prog: LET LPAREN VAR COLON INT RPAREN ZERO -## -## Ends in an error in state: 28. -## -## obj -> LET param . EQ obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LET param -## - - - -prog: LET LPAREN VAR COLON INT RPAREN EQ RPAREN -## -## Ends in an error in state: 29. -## -## obj -> LET param EQ . obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LET param EQ -## - - - -prog: LET LPAREN VAR COLON INT RPAREN EQ INT SUCC -## -## Ends in an error in state: 30. -## -## obj -> LET param EQ obj . IN obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LET 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 24, spurious reduction of production obj -> app_obj -## - - - -prog: LET LPAREN VAR COLON INT RPAREN EQ INT IN RPAREN -## -## Ends in an error in state: 31. -## -## obj -> LET param EQ obj IN . obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LET param EQ obj IN -## - - diff --git a/theories/Frontend/parserErrors.messages~ b/theories/Frontend/parserErrors.messages~ deleted file mode 100644 index 15e566c8..00000000 --- a/theories/Frontend/parserErrors.messages~ +++ /dev/null @@ -1,529 +0,0 @@ -prog: INT COLON INT SUCC -## -## Ends in an error in state: 56. -## -## prog -> obj COLON obj . EOF [ # ] -## -## The known suffix of the stack is as follows: -## obj COLON 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 24, spurious reduction of production obj -> app_obj -## - -Either an expression or the end of file is expected. -This token is invalid for the beginning of an expression. - -prog: RPAREN -## -## Ends in an error in state: 0. -## -## prog' -> . prog [ # ] -## -## The known suffix of the stack is as follows: -## -## - -This token is invalid for the beginning of a program. - -prog: TYPE ZERO -## -## Ends in an error in state: 3. -## -## atomic_obj -> TYPE . AT INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## TYPE -## - -"Type" requires "@". - -prog: TYPE AT ZERO -## -## Ends in an error in state: 4. -## -## atomic_obj -> TYPE AT . INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## TYPE AT -## - -"Type" requires "@?level", where "?level" is an arabic numeral. - -prog: SUCC RPAREN -## -## Ends in an error in state: 6. -## -## obj -> SUCC . obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## SUCC -## - -An expression is expected after "succ". -This token is invalid for the beginning of an expression. - -prog: REC RPAREN -## -## Ends in an error in state: 7. -## -## obj -> REC . obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC -## - -An expression is expected after "rec". -This token is invalid for the beginning of an expression. - -prog: LAMBDA ZERO -## -## Ends in an error in state: 19. -## -## obj -> fnbinder . params ARROW obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## fnbinder -## - -"forall" requires a list of parenthesized parameters. -For example, - "(x : Nat) (y : Nat)" in "forall (x : Nat) (y : Nat) -> Nat" - -prog: LAMBDA LPAREN ZERO -## -## Ends in an error in state: 12. -## -## param -> LPAREN . VAR COLON obj RPAREN [ LPAREN EQ ARROW ] -## -## The known suffix of the stack is as follows: -## LPAREN -## - -A parameter should start with a valid identifier. - -prog: LAMBDA LPAREN VAR ZERO -## -## Ends in an error in state: 13. -## -## param -> LPAREN VAR . COLON obj RPAREN [ LPAREN EQ ARROW ] -## -## The known suffix of the stack is as follows: -## LPAREN VAR -## - -A parameter should have ": ?type" after the parameter name, -where "?type" is the type of the parameter. - -prog: LAMBDA LPAREN VAR COLON RPAREN -## -## Ends in an error in state: 14. -## -## param -> LPAREN VAR COLON . obj RPAREN [ LPAREN EQ ARROW ] -## -## The known suffix of the stack is as follows: -## LPAREN VAR COLON -## - -A parameter should have "?type" after ":", -where "?type" is the type of the parameter. - -prog: LPAREN RPAREN -## -## Ends in an error in state: 10. -## -## atomic_obj -> LPAREN . obj RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LPAREN -## - -"()" is an invalid expression. -"()" should have an expression in it to be an expression. - -prog: LPAREN INT DARROW -## -## Ends in an error in state: 33. -## -## atomic_obj -> LPAREN obj . RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LPAREN 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 24, spurious reduction of production obj -> app_obj -## - -Either an expression or ")" is expected. -This token is invalid for the beginning of an expression. - -prog: LAMBDA LPAREN VAR COLON INT DARROW -## -## Ends in an error in state: 17. -## -## param -> LPAREN VAR COLON obj . RPAREN [ LPAREN EQ ARROW ] -## -## The known suffix of the stack is as follows: -## LPAREN VAR COLON 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 24, spurious reduction of production obj -> app_obj -## - -Either an expression or ")" is expected. -This token is invalid for the beginning of an expression. - -prog: LAMBDA LPAREN VAR COLON INT RPAREN ZERO -## -## Ends in an error in state: 20. -## -## obj -> fnbinder params . ARROW obj [ RPAREN RETURN IN EOF END COLON BAR ] -## params -> params . param [ LPAREN ARROW ] -## -## The known suffix of the stack is as follows: -## fnbinder params -## - -"->" or another parameter is expected after a list of parameters for "fun". - -prog: LAMBDA LPAREN VAR COLON INT RPAREN ARROW RPAREN -## -## Ends in an error in state: 21. -## -## obj -> fnbinder params ARROW . obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## fnbinder params ARROW -## - -An expression is expected after "->". -This token is invalid for the beginning of an expression. - -prog: REC INT DARROW -## -## Ends in an error in state: 35. -## -## obj -> REC obj . RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC 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 24, spurious reduction of production obj -> app_obj -## - -Either an expression or "return" keyword is expected. -This token is invalid for the beginning of an expression. - -prog: REC INT RETURN ZERO -## -## Ends in an error in state: 36. -## -## obj -> REC obj RETURN . VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN -## - -A motif should start with a valid identifier. - -prog: REC INT RETURN VAR ZERO -## -## Ends in an error in state: 37. -## -## obj -> REC obj RETURN VAR . DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN 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. - -prog: REC INT RETURN VAR DOT RPAREN -## -## Ends in an error in state: 38. -## -## obj -> REC obj RETURN VAR DOT . obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 DOT INT DARROW -## -## Ends in an error in state: 39. -## -## obj -> REC obj RETURN VAR DOT obj . BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 24, 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 DOT INT BAR VAR -## -## Ends in an error in state: 40. -## -## obj -> REC obj RETURN VAR DOT obj BAR . ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN VAR DOT obj BAR -## - -"zero" is expected for the first branch of "rec". - -prog: REC INT RETURN VAR DOT INT BAR ZERO ZERO -## -## Ends in an error in state: 41. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO . DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN VAR DOT obj BAR ZERO -## - -"=>" is expected after a pattern for "rec". - -prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW RPAREN -## -## Ends in an error in state: 42. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW . obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 DOT INT BAR ZERO DARROW INT DARROW -## -## Ends in an error in state: 43. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj . BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 24, 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 DOT INT BAR ZERO DARROW INT BAR ZERO -## -## Ends in an error in state: 44. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR . SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 DOT INT BAR ZERO DARROW INT BAR SUCC ZERO -## -## Ends in an error in state: 45. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC . VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 DOT INT BAR ZERO DARROW INT BAR SUCC VAR ZERO -## -## Ends in an error in state: 46. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR . COMMA VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR -## - -"," is expected after "succ ?x". - -prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA ZERO -## -## Ends in an error in state: 47. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA . VAR DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR ZERO -## -## Ends in an error in state: 48. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR . DARROW obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW RPAREN -## -## Ends in an error in state: 49. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW . obj END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARROW INT DARROW -## -## Ends in an error in state: 50. -## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj . END [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## 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 24, spurious reduction of production obj -> app_obj -## - -Either an expression or "end" is expected. -This token is invalid for the beginning of an expression. - -prog: INT DARROW -## -## Ends in an error in state: 54. -## -## prog -> obj . COLON obj EOF [ # ] -## -## The known suffix of the stack is as follows: -## 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 24, spurious reduction of production obj -> app_obj -## - -Either an expression or ":" is expected. -This token is invalid for the beginning of an expression. - -prog: INT COLON RPAREN -## -## Ends in an error in state: 55. -## -## prog -> obj COLON . obj EOF [ # ] -## -## The known suffix of the stack is as follows: -## obj COLON -## - -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 . param EQ obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LET -## - - - -prog: LET LPAREN VAR COLON INT RPAREN ZERO -## -## Ends in an error in state: 28. -## -## obj -> LET param . EQ obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LET param -## - - - -prog: LET LPAREN VAR COLON INT RPAREN EQ RPAREN -## -## Ends in an error in state: 29. -## -## obj -> LET param EQ . obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LET param EQ -## - - - -prog: LET LPAREN VAR COLON INT RPAREN EQ INT SUCC -## -## Ends in an error in state: 30. -## -## obj -> LET param EQ obj . IN obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LET 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 24, spurious reduction of production obj -> app_obj -## - - - -prog: LET LPAREN VAR COLON INT RPAREN EQ INT IN RPAREN -## -## Ends in an error in state: 31. -## -## obj -> LET param EQ obj IN . obj [ RPAREN RETURN IN EOF END COLON BAR ] -## -## The known suffix of the stack is as follows: -## LET param EQ obj IN -## - - diff --git a/theories/Frontend/parserMessages.messages b/theories/Frontend/parserMessages.messages index 5f97ee7a..cc670e7b 100644 --- a/theories/Frontend/parserMessages.messages +++ b/theories/Frontend/parserMessages.messages @@ -473,7 +473,7 @@ prog: LET ZERO ## LET ## - +A variable "(x : ?A)" is expected after "let", where "?A" is a type. prog: LET LPAREN VAR COLON INT RPAREN ZERO ## @@ -485,7 +485,7 @@ prog: LET LPAREN VAR COLON INT RPAREN ZERO ## LET param ## - +Token "=" is expected after let-binding. prog: LET LPAREN VAR COLON INT RPAREN EQ RPAREN ## @@ -497,7 +497,7 @@ prog: LET LPAREN VAR COLON INT RPAREN EQ RPAREN ## LET param EQ ## - +An expression is expected after "=". prog: LET LPAREN VAR COLON INT RPAREN EQ INT SUCC ## @@ -515,7 +515,7 @@ prog: LET LPAREN VAR COLON INT RPAREN EQ INT SUCC ## In state 24, spurious reduction of production obj -> app_obj ## - +Expected token "in". prog: LET LPAREN VAR COLON INT RPAREN EQ INT IN RPAREN ## @@ -527,4 +527,4 @@ prog: LET LPAREN VAR COLON INT RPAREN EQ INT IN RPAREN ## LET param EQ obj IN ## - +An expression is expected. From 79c2d059ced1d99f0aa98d4aafb8a1566ae21392 Mon Sep 17 00:00:00 2001 From: AG-something Date: Tue, 1 Oct 2024 11:16:41 -0400 Subject: [PATCH 4/6] Changed equality symbol to := --- driver/Lexer.mll | 4 ++-- examples/simple_let.mcl | 2 +- theories/Frontend/Parser.vy | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/driver/Lexer.mll b/driver/Lexer.mll index 87bf2332..c7fe8781 100644 --- a/driver/Lexer.mll +++ b/driver/Lexer.mll @@ -43,7 +43,7 @@ | DOT _ -> "." | LET _ -> "let" | IN _ -> "in" - | EQ _ -> "=" + | EQ _ -> ":=" let get_range_of_token : token -> (position * position) = function @@ -109,7 +109,7 @@ rule read = | "." { DOT (get_range lexbuf) } | "let" {LET (get_range lexbuf) } | "in" {IN (get_range lexbuf) } - | "=" {EQ (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 = diff --git a/examples/simple_let.mcl b/examples/simple_let.mcl index 6a8fc07c..4b6b1fcd 100644 --- a/examples/simple_let.mcl +++ b/examples/simple_let.mcl @@ -1 +1 @@ -let (x : Nat) = zero in succ x : Nat \ No newline at end of file +let (x : Nat) := zero in succ x : Nat \ No newline at end of file diff --git a/theories/Frontend/Parser.vy b/theories/Frontend/Parser.vy index bdf82256..2f54fa40 100644 --- a/theories/Frontend/Parser.vy +++ b/theories/Frontend/Parser.vy @@ -11,7 +11,7 @@ Parameter loc : Type. %token VAR %token INT %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 *) +%token ARROW "->" AT "@" BAR "|" COLON ":" COMMA "," DARROW "=>" LPAREN "(" RPAREN ")" DOT "." EQ ":=" EOF (* symbols *) %start prog %type obj app_obj atomic_obj @@ -40,7 +40,7 @@ let obj := END; { Cst.natrec escr (snd mx) em ez (snd sx) (snd sr) ms } | SUCC; ~ = obj; { Cst.succ obj } - | LET; p = param; "="; arg_obj = obj; IN; fun_obj = obj; { Cst.app (Cst.fn (fst p) (snd p) fun_obj) arg_obj } + | LET; p = param; ":="; arg_obj = obj; IN; fun_obj = obj; { Cst.app (Cst.fn (fst p) (snd p) fun_obj) arg_obj } let app_obj := | ~ = app_obj; ~ = atomic_obj; { Cst.app app_obj atomic_obj } From 4864200eaeb09560eff0bb6a4f856884b1b35a26 Mon Sep 17 00:00:00 2001 From: Antoine-something Date: Fri, 11 Oct 2024 18:51:28 -0400 Subject: [PATCH 5/6] let-binding now works with multiple definitions; added let-binding versions of the big examples (nary and vector); added tests for all the let-binding examples --- driver/Test.ml | 333 +++++++++++++++++++++- examples/let_nary.mcl | 44 +++ examples/let_two_vars.mcl | 1 + examples/let_vector.mcl | 36 +++ examples/simple_let.mcl | 2 +- theories/Frontend/Parser.vy | 14 +- theories/Frontend/parserMessages.messages | 187 ++++++------ 7 files changed, 532 insertions(+), 85 deletions(-) create mode 100644 examples/let_nary.mcl create mode 100644 examples/let_two_vars.mcl create mode 100644 examples/let_vector.mcl diff --git a/driver/Test.ml b/driver/Test.ml index 475cd810..71a518eb 100644 --- a/driver/Test.ml +++ b/driver/Test.ml @@ -89,7 +89,7 @@ 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: @@ -554,6 +554,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/simple_let.mcl b/examples/simple_let.mcl index 4b6b1fcd..8356abb2 100644 --- a/examples/simple_let.mcl +++ b/examples/simple_let.mcl @@ -1 +1 @@ -let (x : Nat) := zero in succ x : Nat \ No newline at end of file +let ((x : Nat) := zero) in succ x : Nat \ No newline at end of file diff --git a/theories/Frontend/Parser.vy b/theories/Frontend/Parser.vy index 2f54fa40..6980e1ab 100644 --- a/theories/Frontend/Parser.vy +++ b/theories/Frontend/Parser.vy @@ -18,6 +18,8 @@ Parameter loc : Type. %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 @@ -39,14 +41,14 @@ let 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; p = param; ":="; arg_obj = obj; IN; fun_obj = obj; { Cst.app (Cst.fn (fst p) (snd p) fun_obj) arg_obj } let app_obj := | ~ = app_obj; ~ = atomic_obj; { Cst.app app_obj atomic_obj } | ~ = atomic_obj; <> - let atomic_obj := | TYPE; "@"; n = INT; { Cst.typ (snd n) } @@ -67,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 cc670e7b..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: 56. +## 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 24, 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. @@ -33,7 +33,7 @@ prog: TYPE ZERO ## ## Ends in an error in state: 3. ## -## atomic_obj -> TYPE . AT INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] +## atomic_obj -> TYPE . AT INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## TYPE @@ -45,7 +45,7 @@ prog: TYPE AT ZERO ## ## Ends in an error in state: 4. ## -## atomic_obj -> TYPE AT . INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] +## atomic_obj -> TYPE AT . INT [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## TYPE AT @@ -57,7 +57,7 @@ prog: SUCC RPAREN ## ## Ends in an error in state: 6. ## -## obj -> SUCC . obj [ RPAREN RETURN IN EOF END COLON BAR ] +## obj -> SUCC . obj [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## SUCC @@ -70,7 +70,7 @@ prog: REC RPAREN ## ## Ends in an error in state: 7. ## -## obj -> REC . obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN 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,9 +81,9 @@ This token is invalid for the beginning of an expression. prog: LAMBDA ZERO ## -## Ends in an error in state: 19. +## Ends in an error in state: 20. ## -## obj -> fnbinder . params ARROW obj [ RPAREN RETURN IN EOF END COLON BAR ] +## obj -> fnbinder . params ARROW obj [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## fnbinder @@ -95,7 +95,7 @@ For example, prog: LAMBDA LPAREN ZERO ## -## Ends in an error in state: 12. +## Ends in an error in state: 13. ## ## param -> LPAREN . VAR COLON obj RPAREN [ LPAREN EQ ARROW ] ## @@ -107,7 +107,7 @@ A parameter should start with a valid identifier. prog: LAMBDA LPAREN VAR ZERO ## -## Ends in an error in state: 13. +## Ends in an error in state: 14. ## ## param -> LPAREN VAR . COLON obj RPAREN [ LPAREN EQ ARROW ] ## @@ -120,7 +120,7 @@ where "?type" is the type of the parameter. prog: LAMBDA LPAREN VAR COLON RPAREN ## -## Ends in an error in state: 14. +## Ends in an error in state: 15. ## ## param -> LPAREN VAR COLON . obj RPAREN [ LPAREN EQ ARROW ] ## @@ -135,7 +135,7 @@ prog: LPAREN RPAREN ## ## Ends in an error in state: 10. ## -## atomic_obj -> LPAREN . obj RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] +## atomic_obj -> LPAREN . obj RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## LPAREN @@ -146,9 +146,9 @@ prog: LPAREN RPAREN prog: LPAREN INT DARROW ## -## Ends in an error in state: 33. +## Ends in an error in state: 38. ## -## atomic_obj -> LPAREN obj . RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT IN EOF END COLON BAR ] +## atomic_obj -> LPAREN obj . RPAREN [ ZERO VAR TYPE RPAREN RETURN NAT LPAREN INT EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## LPAREN obj @@ -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 24, spurious reduction of production obj -> app_obj +## In state 25, spurious reduction of production obj -> app_obj ## Either an expression or ")" is expected. @@ -165,7 +165,7 @@ This token is invalid for the beginning of an expression. prog: LAMBDA LPAREN VAR COLON INT DARROW ## -## Ends in an error in state: 17. +## Ends in an error in state: 18. ## ## param -> LPAREN VAR COLON obj . RPAREN [ LPAREN EQ ARROW ] ## @@ -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 24, spurious reduction of production obj -> app_obj +## In state 25, spurious reduction of production obj -> app_obj ## Either an expression or ")" is expected. @@ -184,9 +184,9 @@ This token is invalid for the beginning of an expression. prog: LAMBDA LPAREN VAR COLON INT RPAREN ZERO ## -## Ends in an error in state: 20. +## Ends in an error in state: 21. ## -## obj -> fnbinder params . ARROW obj [ RPAREN RETURN IN EOF END COLON BAR ] +## obj -> fnbinder params . ARROW obj [ RPAREN RETURN EOF END COLON BAR ] ## params -> params . param [ LPAREN ARROW ] ## ## The known suffix of the stack is as follows: @@ -197,9 +197,9 @@ prog: LAMBDA LPAREN VAR COLON INT RPAREN ZERO prog: LAMBDA LPAREN VAR COLON INT RPAREN ARROW RPAREN ## -## Ends in an error in state: 21. +## Ends in an error in state: 22. ## -## obj -> fnbinder params ARROW . obj [ RPAREN RETURN IN EOF END COLON BAR ] +## obj -> fnbinder params ARROW . obj [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## fnbinder params ARROW @@ -210,9 +210,9 @@ This token is invalid for the beginning of an expression. prog: REC INT DARROW ## -## Ends in an error in state: 35. +## Ends in an error in state: 40. ## -## obj -> REC obj . RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN 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 24, 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: 36. +## Ends in an error in state: 41. ## -## obj -> REC obj RETURN . VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN 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,9 +241,9 @@ A motif should start with a valid identifier. prog: REC INT RETURN VAR ZERO ## -## Ends in an error in state: 37. +## Ends in an error in state: 42. ## -## obj -> REC obj RETURN VAR . DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN 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 @@ -253,9 +253,9 @@ A motif should have "." after the scrutinee name. prog: REC INT RETURN VAR DOT RPAREN ## -## Ends in an error in state: 38. +## Ends in an error in state: 43. ## -## obj -> REC obj RETURN VAR DOT . obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN 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 DOT @@ -266,9 +266,9 @@ This token is invalid for the beginning of an expression. prog: REC INT RETURN VAR DOT INT DARROW ## -## Ends in an error in state: 39. +## Ends in an error in state: 44. ## -## obj -> REC obj RETURN VAR DOT obj . BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN 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 DOT obj @@ -277,7 +277,7 @@ prog: REC INT RETURN VAR DOT 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 24, spurious reduction of production obj -> app_obj +## In state 25, spurious reduction of production obj -> app_obj ## Either an expression or "|" is expected. @@ -285,9 +285,9 @@ This token is invalid for the beginning of an expression. prog: REC INT RETURN VAR DOT INT BAR VAR ## -## Ends in an error in state: 40. +## Ends in an error in state: 45. ## -## obj -> REC obj RETURN VAR DOT obj BAR . ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN 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 DOT obj BAR @@ -297,9 +297,9 @@ prog: REC INT RETURN VAR DOT INT BAR VAR prog: REC INT RETURN VAR DOT INT BAR ZERO ZERO ## -## Ends in an error in state: 41. +## Ends in an error in state: 46. ## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO . DARROW obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN 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 DOT obj BAR ZERO @@ -309,9 +309,9 @@ prog: REC INT RETURN VAR DOT INT BAR ZERO ZERO prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW RPAREN ## -## Ends in an error in state: 42. +## Ends in an error in state: 47. ## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW . obj BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN 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 DOT obj BAR ZERO DARROW @@ -322,9 +322,9 @@ This token is invalid for the beginning of an expression. prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT DARROW ## -## Ends in an error in state: 43. +## Ends in an error in state: 48. ## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj . BAR SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN 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 DOT obj BAR ZERO DARROW obj @@ -333,7 +333,7 @@ prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW 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 24, spurious reduction of production obj -> app_obj +## In state 25, spurious reduction of production obj -> app_obj ## Either an expression or "|" is expected. @@ -341,9 +341,9 @@ This token is invalid for the beginning of an expression. prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR ZERO ## -## Ends in an error in state: 44. +## Ends in an error in state: 49. ## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR . SUCC VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN 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 DOT obj BAR ZERO DARROW obj BAR @@ -353,9 +353,9 @@ prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR ZERO prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC ZERO ## -## Ends in an error in state: 45. +## Ends in an error in state: 50. ## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC . VAR COMMA VAR DARROW obj END [ RPAREN RETURN IN 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 DOT obj BAR ZERO DARROW obj BAR SUCC @@ -365,9 +365,9 @@ An identifier for the predecessor of the scrutinee is expected. prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR ZERO ## -## Ends in an error in state: 46. +## Ends in an error in state: 51. ## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR . COMMA VAR DARROW obj END [ RPAREN RETURN IN 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 DOT obj BAR ZERO DARROW obj BAR SUCC VAR @@ -377,9 +377,9 @@ prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR ZERO prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA ZERO ## -## Ends in an error in state: 47. +## Ends in an error in state: 52. ## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA . VAR DARROW obj END [ RPAREN RETURN IN 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 DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA @@ -389,9 +389,9 @@ An identifier for the recursion result is expected. prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR ZERO ## -## Ends in an error in state: 48. +## Ends in an error in state: 53. ## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR . DARROW obj END [ RPAREN RETURN IN 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 DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR @@ -401,9 +401,9 @@ prog: REC INT RETURN VAR DOT 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 DARROW RPAREN ## -## Ends in an error in state: 49. +## Ends in an error in state: 54. ## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW . obj END [ RPAREN RETURN IN 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 DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW @@ -414,9 +414,9 @@ This token is invalid for the beginning of an expression. 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: 50. +## Ends in an error in state: 55. ## -## obj -> REC obj RETURN VAR DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj . END [ RPAREN RETURN IN 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 DOT obj BAR ZERO DARROW obj BAR SUCC VAR COMMA VAR DARROW obj @@ -425,7 +425,7 @@ prog: REC INT RETURN VAR DOT INT BAR ZERO DARROW INT BAR SUCC VAR COMMA VAR DARR ## 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 24, 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: 54. +## 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 24, 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: 55. +## Ends in an error in state: 60. ## ## prog -> obj COLON . obj EOF [ # ] ## @@ -467,64 +467,89 @@ prog: LET ZERO ## ## Ends in an error in state: 11. ## -## obj -> LET . param EQ obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## obj -> LET . let_defns IN obj [ RPAREN RETURN EOF END COLON BAR ] ## ## The known suffix of the stack is as follows: ## LET ## -A variable "(x : ?A)" is expected after "let", where "?A" is a type. +At least one variable binding is expected after a "let" -prog: LET LPAREN VAR COLON INT RPAREN ZERO +prog: LET LPAREN ZERO ## -## Ends in an error in state: 28. +## Ends in an error in state: 12. ## -## obj -> LET param . EQ obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## let_defn -> LPAREN . param EQ obj RPAREN [ LPAREN IN ] ## ## The known suffix of the stack is as follows: -## LET param +## LPAREN ## -Token "=" is expected after let-binding. +A variable "(x : ?A)" is expected after "let (", where "?A" is a type. -prog: LET LPAREN VAR COLON INT RPAREN EQ RPAREN +prog: LET LPAREN LPAREN VAR COLON INT RPAREN ZERO ## ## Ends in an error in state: 29. ## -## obj -> LET param EQ . obj IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## let_defn -> LPAREN param . EQ obj RPAREN [ LPAREN IN ] ## ## The known suffix of the stack is as follows: -## LET param EQ +## LPAREN param ## -An expression is expected after "=". +Expected symbol ":=". -prog: LET LPAREN VAR COLON INT RPAREN EQ INT SUCC +prog: LET LPAREN LPAREN VAR COLON INT RPAREN EQ RPAREN ## ## Ends in an error in state: 30. ## -## obj -> LET param EQ obj . IN obj [ RPAREN RETURN IN EOF END COLON BAR ] +## let_defn -> LPAREN param EQ . obj RPAREN [ LPAREN IN ] ## ## The known suffix of the stack is as follows: -## LET param EQ obj +## 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 24, spurious reduction of production obj -> app_obj +## In state 25, spurious reduction of production obj -> app_obj ## -Expected token "in". +Expected ")". -prog: LET LPAREN VAR COLON INT RPAREN EQ INT IN RPAREN +prog: LET LPAREN LPAREN VAR COLON INT RPAREN EQ INT RPAREN ZERO ## -## Ends in an error in state: 31. +## Ends in an error in state: 33. ## -## obj -> LET param EQ obj IN . obj [ RPAREN RETURN IN EOF END COLON BAR ] +## 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 param EQ obj IN +## LET let_defns ## -An expression is expected. +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 From fe8ac70f2fad1d235968113a3d2b98416fc8497b Mon Sep 17 00:00:00 2001 From: Antoine-something Date: Sun, 13 Oct 2024 10:16:52 -0400 Subject: [PATCH 6/6] Replaced -> with . in pretty printer --- driver/PrettyPrinter.ml | 2 +- driver/Test.ml | 59 ++++++++++++++++++++--------------------- 2 files changed, 30 insertions(+), 31 deletions(-) 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 71a518eb..0c156c52 100644 --- a/driver/Test.ml +++ b/driver/Test.ml @@ -93,9 +93,9 @@ let%expect_test "recursion on a natural number that always returns zero is of \ [%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)) @@ -598,19 +597,19 @@ let%expect_test "let_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) @@ -626,7 +625,7 @@ let%expect_test "let_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) @@ -637,20 +636,20 @@ let%expect_test "let_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) @@ -666,7 +665,7 @@ let%expect_test "let_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)) @@ -711,14 +710,14 @@ let%expect_test "let_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) @@ -811,14 +810,14 @@ let%expect_test "let_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)