From 2ad0030123fd2db73162cb3229868709b6d158de Mon Sep 17 00:00:00 2001 From: bobzhang Date: Tue, 27 Dec 2011 13:57:25 -0500 Subject: [PATCH] Add parser export, let binding --- Makefile | 4 +- _build/_digests | 38 +- _build/_log | 139 +++++- cxt.ml | 10 + fc_l.mli | 7 +- fc_l.mll | 13 +- fc_p.mly | 72 ++- fc_p.output | 1188 ++++++++++++++++++++++++----------------------- script.sh | 2 +- test/1.ml | 8 +- 10 files changed, 853 insertions(+), 628 deletions(-) diff --git a/Makefile b/Makefile index b8081f0..a4e47d9 100644 --- a/Makefile +++ b/Makefile @@ -22,4 +22,6 @@ parse : prj: ocamlbuild prj.cma -all: parse prj \ No newline at end of file +all: parse prj +clean: + ocamlbuild -clean \ No newline at end of file diff --git a/_build/_digests b/_build/_digests index e9fdda6..2af3f70 100644 --- a/_build/_digests +++ b/_build/_digests @@ -1,32 +1,32 @@ -"Rule: ocaml: mli -> cmi (%=fc_l )": "n\0121x\\\208\136W\002f(y@\157\164\172" -"Rule: ocaml: mli -> cmi (%=fc_p )": "\244\r\217V\197\150x\204\164\161\162\152y)*\238" +"Rule: ocaml: mli -> cmi (%=fc_l )": "\201?\247{<\197b\005\187\2156\242\183\193\192S" +"Rule: ocaml: mli -> cmi (%=fc_p )": "\232\207\254t\138\223\237\240\139A\187\2056\218Mb" "Resource: /Users/bob/SourceCode/course/670/cis670-project/prj.mllib": "\129\n\239\005\007\182\135\154\166\002\142\217!\167>9" "Resource: /Users/bob/SourceCode/course/670/cis670-project/fc_syntax.ml": "w~+\219\246?\2233!Gs\014A\250g\018" -"Rule: ocamlyacc (%=fc_p )": "\139\190J\165\189\192a\13513p>\189\022\1341" -"Rule: ocamllex (%=fc_l )": "`\251\176@\000\018\005\230\023/\212\018\251'\028\224" -"Rule: ocaml dependencies ml (%=cxt )": "\014\005\127\140\199\rS\173\244{M\138\253!0\167" +"Rule: ocamlyacc (%=fc_p )": "\248\150\239+\174\255\237\158+\133\019\218\161\020\022\227" +"Rule: ocaml dependencies ml (%=cxt )": "\1414\000\230\162\166B\149\146\164\131y\023\202\192\253" +"Rule: ocamllex (%=fc_l )": "\162\182#\155\229\182\158\134\165\213\185\181\158\176\020\220" "Rule: ocaml dependencies ml (%=util )": "\2040\250\\\173A\192\147\248\190\165\005l\148\191\210" -"Rule: ocaml: cmo* -> byte (%=fc_l )": "\227\1570\216f\134T\162\168,\161\241IJfs" +"Rule: ocaml: cmo* -> byte (%=fc_l )": "\212\143\012yT\198\153\151\000\214Q\206\127\172\215B" "Rule: ocaml: ml -> cmo & cmi (%=check_term )": "U\151\215\227MW\192_\234\\\145_3\000\188\133" "Rule: ocaml: ml -> cmo & cmi (%=util )": "\254\201\136\022\162\150\193\176uF\195\184f\228\173\138" "Resource: /Users/bob/SourceCode/course/670/cis670-project/util.ml": ":\208\156B\188\190\177\031\2037\0315\215L#\249" -"Resource: /Users/bob/SourceCode/course/670/cis670-project/fc_l.mli": "\159\224\164\016\023\217\209k\005\159\175\172\133\016ZJ" -"Resource: /Users/bob/SourceCode/course/670/cis670-project/fc_l.mll": "\145\204K\134\001\233|J\027\224\1492g\246.F" -"Rule: ocaml: mllib & cmo* -> cma (%=prj )": "\208\221\175\022q\170FQ\179\020/\147n\254\156>" +"Resource: /Users/bob/SourceCode/course/670/cis670-project/fc_l.mli": "\t\213*\219xKDz\024d\195,\223\249\223&" +"Resource: /Users/bob/SourceCode/course/670/cis670-project/fc_l.mll": "yz\241\015(\155\214\253}-'\142\219\r\000\221" +"Rule: ocaml: mllib & cmo* -> cma (%=prj )": "\138IJ|\231\b\1552\232\186\184\219*\022M\014" "Rule: ocaml dependencies ml (%=check_term )": "\137\193\005W\211\017\235\023\018m\"%\174\131|u" "Rule: ocaml dependencies ml (%=test )": "\153\198\155\188\157\207\153\231\\X\163\167I\143\201\011" -"Rule: ocaml dependencies mli (%=fc_l )": "\246\242s\029\128\199\215\144\003\022\028\207\182\166\146\140" -"Rule: ocaml dependencies mli (%=fc_p )": "\163\140J\244\030\004\135\245\232\186\011\242\127\246oi" +"Rule: ocaml dependencies mli (%=fc_l )": "\172\231\232\002%\220T\145\191\168\003.t,\014\191" +"Rule: ocaml dependencies mli (%=fc_p )": "*\238\152C\140\021\131/\145b\016\179\211\234\234\195" "Resource: /Users/bob/SourceCode/course/670/cis670-project/test.ml": "\205\241U\253-\129d\127\155m\218\021\175c)\244" -"Resource: /Users/bob/SourceCode/course/670/cis670-project/fc_p.mly": "W\162l\215\152lm\197\141\237\018\132\225\2316\242" +"Resource: /Users/bob/SourceCode/course/670/cis670-project/fc_p.mly": "0(\243!\192H\161\237n\167gu\158\175\159w" "Rule: ocaml: ml -> cmo & cmi (%=test )": "i\165,8\231\n\139t\011\130\142L\160\017\186\209" -"Rule: ocaml: ml & cmi -> cmo (%=fc_l )": "V\159\127\171O\218\138\244\006\183{H@=\233z" -"Rule: ocaml: ml & cmi -> cmo (%=fc_p )": "\134\005\252V\209\200,MS-\215\132\n\0302`" -"Rule: ocaml: ml & ml.depends & *cmi -> .inferred.mli (%=fc_l )": "\000\247ho\146\163\003\255i\253\228;\139:r|" +"Rule: ocaml: ml & cmi -> cmo (%=fc_l )": "`\222;\239F\249J\186\002\254\025j\000DF\202" +"Rule: ocaml: ml & cmi -> cmo (%=fc_p )": "\176]z)\195\170k\006\156\1756\239\028G\147\249" +"Rule: ocaml: ml & ml.depends & *cmi -> .inferred.mli (%=fc_l )": "[\020\003\244\006%\n\021j\237\233\000Md\218T" "Rule: ocaml dependencies ml (%=fc_syntax )": "\218\015\195\136\158d\242_\237~\012wv\232B}" -"Rule: ocaml: ml -> cmo & cmi (%=cxt )": "\142_w\019\214;\219\171h\150\227\216\169M4\181" -"Rule: ocaml dependencies ml (%=fc_l )": "\234\215?\214P\229\026\1870\238aG\007S\181A" +"Rule: ocaml: ml -> cmo & cmi (%=cxt )": "\b\177\"E\196\162\224\006\141\012\007Gw\027O!" +"Rule: ocaml dependencies ml (%=fc_l )": " \019\172|'k\221!\182L_H;\1663\230" "Resource: /Users/bob/SourceCode/course/670/cis670-project/check_term.ml": "\216\0072\021\030\248(oY\250\147\174\250\209\224%" -"Rule: ocaml dependencies ml (%=fc_p )": "`iE\248\012\129\128\137\229\239!\243\2301AZ" +"Rule: ocaml dependencies ml (%=fc_p )": "0\173\199B>D\248\\\000\016+p\255\254#\170" "Rule: ocaml: ml -> cmo & cmi (%=fc_syntax )": "@\000{ \022cOf<\251\244HK\1526\138" -"Resource: /Users/bob/SourceCode/course/670/cis670-project/cxt.ml": "\207^\254w;\136(F\195\183\238\159\238\183\188\185" +"Resource: /Users/bob/SourceCode/course/670/cis670-project/cxt.ml": "v\022\171\191\184\253\150\170\141\177\208\2206\003\248\240" diff --git a/_build/_log b/_build/_log index 7e51556..db6950e 100644 --- a/_build/_log +++ b/_build/_log @@ -22,9 +22,7 @@ ocamlfind ocamlc -c -o cxt.cmo cxt.ml # cached # Target: fc_p.cmo, tags: { byte, compile, extension:cmo, extension:ml, file:fc_p.cmo, file:fc_p.ml, implem, ocaml, quiet, traverse } ocamlfind ocamlc -c -o fc_p.cmo fc_p.ml # cached # Target: check_term.ml.depends, tags: { extension:ml, file:check_term.ml, ocaml, ocamldep, quiet, traverse } -ocamlfind ocamldep -modules check_term.ml > check_term.ml.depends # cached -# Target: check_term.cmo, tags: { byte, compile, extension:cmo, extension:ml, file:check_term.cmo, file:check_term.ml, implem, ocaml, quiet, traverse } -ocamlfind ocamlc -c -o check_term.cmo check_term.ml # cached +ocamlfind ocamldep -modules check_term.ml > check_term.ml.depends # Target: fc_l.mli.depends, tags: { extension:mli, file:fc_l.mli, ocaml, ocamldep, quiet, traverse } ocamlfind ocamldep -modules fc_l.mli > fc_l.mli.depends # cached # Target: fc_l.cmi, tags: { byte, compile, extension:mli, file:fc_l.mli, interf, ocaml, quiet, traverse } @@ -36,9 +34,140 @@ ocamlfind ocamldep -modules fc_l.ml > fc_l.ml.depends # cached # Target: fc_l.cmo, tags: { byte, compile, extension:cmo, extension:ml, file:fc_l.cmo, file:fc_l.ml, implem, ocaml, quiet, traverse } ocamlfind ocamlc -c -o fc_l.cmo fc_l.ml # cached # Target: test.ml.depends, tags: { extension:ml, file:test.ml, ocaml, ocamldep, quiet, traverse } -ocamlfind ocamldep -modules test.ml > test.ml.depends # cached +ocamlfind ocamldep -modules test.ml > test.ml.depends +# Target: check_term.cmo, tags: { byte, compile, extension:cmo, extension:ml, file:check_term.cmo, file:check_term.ml, implem, ocaml, quiet, traverse } +ocamlfind ocamlc -c -o check_term.cmo check_term.ml ++ ocamlfind ocamlc -c -o check_term.cmo check_term.ml +File "check_term.ml", line 191, characters 24-27: +Warning 26: unused variable r''. +File "check_term.ml", line 191, characters 20-23: +Warning 26: unused variable k''. +File "check_term.ml", line 8, characters 10-29: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +(BDataCon (_, _)|BTermVar _|BCoer (_, _, _)|BTConst _) +File "check_term.ml", line 22, characters 11-20: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +(BDataCon (_, _)|BTermVar _|BCoer (_, _, _)|BTVar _) +File "check_term.ml", line 30, characters 10-48: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 32, characters 10-29: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 42, characters 11-30: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 66, characters 12-46: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +(BDataCon (_, _)|BTermVar _|BTConst _|BTVar _) +File "check_term.ml", line 68, characters 12-27: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 82, characters 12-19: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 88, characters 12-29: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 101, characters 12-59: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 103, characters 12-43: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 114, characters 12-36: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 123, characters 24-33: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +(BDataCon (_, _)|BTermVar _|BCoer (_, _, _)|BTVar _) +File "check_term.ml", line 139, characters 12-39: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 147, characters 12-130: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 151, characters 14-22: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 165, characters 14-26: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +(BDataCon (_, _)|BCoer (_, _, _)|BTConst _|BTVar _) +File "check_term.ml", line 174, characters 12-63: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 175, characters 12-20: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 183, characters 13-21: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 189, characters 10-44: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 191, characters 10-29: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 197, characters 13-33: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +(BTermVar _|BCoer (_, _, _)|BTConst _|BTVar _) +File "check_term.ml", line 205, characters 13-21: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 207, characters 13-36: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +(TyForall (_, _, _)|TyApp (_, _)|TyVar _) +File "check_term.ml", line 212, characters 15-24: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 229, characters 13-21: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 248, characters 13-186: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 254, characters 13-31: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 265, characters 12-23: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None +File "check_term.ml", line 266, characters 12-50: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a value that is not matched: +None # Target: test.cmo, tags: { byte, compile, extension:cmo, extension:ml, file:test.cmo, file:test.ml, implem, ocaml, quiet, traverse } -ocamlfind ocamlc -c -o test.cmo test.ml # cached +ocamlfind ocamlc -c -o test.cmo test.ml # Target: prj.cma, tags: { byte, extension:cma, file:prj.cma, library, link, ocaml, quiet, traverse } ocamlfind ocamlc -a fc_syntax.cmo util.cmo cxt.cmo fc_p.cmo check_term.cmo fc_l.cmo test.cmo -o prj.cma # Compilation successful. diff --git a/cxt.ml b/cxt.ml index fb7ea40..35d5b94 100644 --- a/cxt.ml +++ b/cxt.ml @@ -5,8 +5,18 @@ let datatype_tbl : (string,bool ) Hashtbl.t = Hashtbl.create 30 let function_tbl : (string, int ref ) Hashtbl.t= Hashtbl.create 30 +let new_type_tbl : (string, bool) Hashtbl.t = Hashtbl.create 30 + +let term_tbl : (string, fc_term) Hashtbl.t = Hashtbl.create 30 + let cxt : context ref = ref [] +let clear () = + Hashtbl.(clear datatype_tbl; + clear function_tbl; + clear new_type_tbl; + clear term_tbl + ) (* Hashtbl.print String.print Bool.print stdout Cxt.datatype_tbl;; diff --git a/fc_l.mli b/fc_l.mli index e6bbffc..2862eb9 100644 --- a/fc_l.mli +++ b/fc_l.mli @@ -12,11 +12,14 @@ val parser_of_entry : ((Lexing.lexbuf -> Fc_p.token) -> Lexing.lexbuf -> 'a) -> string -> 'a val parser_of_file : ((Lexing.lexbuf -> Fc_p.token) -> Lexing.lexbuf -> 'a) -> string -> 'a -val kind_p : string -> Fc_syntax.kind -val kind_and_role_p : string -> Fc_syntax.kind_and_role val input_f : string -> unit val input_p : string -> unit +val kind_p : string -> Fc_syntax.kind +val kind_and_role_p : string -> Fc_syntax.kind_and_role val ty_def_p : string -> Fc_syntax.fc_type +val term_p : string -> Fc_syntax.fc_term +val proof_p : string -> Fc_syntax.co_proof +val ty_dec_p : string -> unit val clause_p : string -> Fc_syntax.binder val test_ty : unit -> Fc_syntax.fc_type list val test : 'a -> unit diff --git a/fc_l.mll b/fc_l.mll index 07e5c48..4a95178 100644 --- a/fc_l.mll +++ b/fc_l.mll @@ -24,6 +24,7 @@ "TYPE",TYPE; "FAMILY",FAMILY; "INSTANCE",INSTANCE; + "LET",LET; ] let first = ref true } @@ -121,14 +122,17 @@ and comment = parse Lexing will close it??? *) parser_of_buf entry lexbuf - + + let input_f = parser_of_file input + let input_p = parser_of_entry input let kind_p = parser_of_entry kind let kind_and_role_p = parser_of_entry kind_and_role - let input_f = parser_of_file input - let input_p = parser_of_entry input let ty_def_p = parser_of_entry ty_def + let term_p = parser_of_entry term + let proof_p = parser_of_entry proof + let ty_dec_p = parser_of_entry ty_dec let clause_p = parser_of_entry clause - + let test_ty () = List.map ty_def_p ["((a -> (LIST a)) -> (LIST a) )" ; @@ -158,6 +162,7 @@ and comment = parse if Filename.check_suffix file ".ml" then let file_name = (Filename.concat dir file ) in prerr_endline ("check file: " ^ file_name); + Cxt.clear (); input_f file_name ) test_files let rec tokens str = diff --git a/fc_p.mly b/fc_p.mly index 19d0956..ac4a50a 100644 --- a/fc_p.mly +++ b/fc_p.mly @@ -12,6 +12,7 @@ %token DATA WHERE %token NTH SYM NEWTYPE %token TYPE FAMILY INSTANCE +%token LET %token LIDENT %token UIDENT @@ -100,7 +101,17 @@ ty_dec: data_type_head clauses SEMI { let data_ctors = $2 in List.iter (fun c -> cxt := c :: !cxt ) data_ctors } - | NEWTYPE UIDENT EQ UIDENT ty_def SEMI {} + | NEWTYPE UIDENT EQ UIDENT ty_def SEMI { + let name = $2 in + let ty1 = TyConst (TFunction name) in + let ty2 = $5 in + begin + Hashtbl.add new_type_tbl name true; + cxt:= ("axiom"^name, + BCoer([],TyEq(ty1,ty2),Type)) :: !cxt ; + + end + } | TYPE FAMILY UIDENT ty_kr_list SEMI { begin @@ -111,16 +122,17 @@ ty_dec: data_type_head clauses SEMI { end } - | TYPE INSTANCE ty_kr_list UIDENT type_list EQ ty_def SEMI { - let name = $4 in - let tys = $5 in - let type_cxt = $3 in - let ty2 = $7 in + | TYPE INSTANCE LBRACKET ty_kr_list RBRACKET UIDENT + type_list EQ ty_def SEMI { + let name = $6 in + let tys = $7 in + let type_cxt = $4 in + let ty2 = $9 in try let count_ref = Hashtbl.find function_tbl name in let ty = TyConst (TFunction name) in let ty1 = List.fold_left (fun x y -> TyApp(x,y)) ty tys in - cxt := (name ^ (string_of_int !count_ref), + cxt := ( "axiom" ^ name ^ (string_of_int !count_ref) , BCoer(type_cxt, TyEq (ty1,ty2),Code)) :: !cxt ; incr count_ref with Not_found @@ -212,26 +224,30 @@ ty_def: LIDENT { TyVar $1} | LPAREN ty_def TILDE kind ty_def RPAREN FARROW ty_def {TyApp(TyApp(TyApp(TyConst(TEquality $4),$2),$5),$8)} | UIDENT - { try - let _ = Hashtbl.find datatype_tbl $1 in - TyConst (Datatype $1) + { let name = $1 in + try + let _ = Hashtbl.find datatype_tbl name in + TyConst (Datatype name) with Not_found -> (try - let _ = Hashtbl.find function_tbl $1 in - TyConst (TFunction $1) + let _ = Hashtbl.find function_tbl name in + TyConst (TFunction name) with Not_found -> - (* TyConst (Datatype $1) *) - Parsing.( - let start_pos = rhs_start_pos 1 in - let end_pos = rhs_end_pos 1 in - let err_msg = sprintf - "%d.%d --- %d.%d: undefined type construtor %s" - start_pos.pos_lnum (start_pos.pos_cnum -start_pos.pos_bol) - end_pos.pos_lnum (end_pos.pos_cnum - end_pos.pos_bol) - $1 in - prerr_endline err_msg ; - raise Not_found - ) + try + let _ = Hashtbl.find new_type_tbl name in + TyConst (TFunction name) + with Not_found -> + (Parsing.( + let start_pos = rhs_start_pos 1 in + let end_pos = rhs_end_pos 1 in + let err_msg = sprintf + "%d.%d --- %d.%d: undefined type construtor %s" + start_pos.pos_lnum (start_pos.pos_cnum -start_pos.pos_bol) + end_pos.pos_lnum (end_pos.pos_cnum - end_pos.pos_bol) + name in + prerr_endline err_msg ; + raise Not_found + )) ) } @@ -272,7 +288,13 @@ term: LIDENT {FCVar $1} | LPAREN term RPAREN {$2} - + | LET LIDENT EQ term /* Just for debugging purpuose */ + { + let name = $2 in + let term = $4 in + Hashtbl.add term_tbl name term ; + term + } ; diff --git a/fc_p.output b/fc_p.output index c1e76df..d1b0284 100644 --- a/fc_p.output +++ b/fc_p.output @@ -22,76 +22,77 @@ 15 | NEWTYPE UIDENT EQ UIDENT ty_def SEMI 16 | TYPE FAMILY UIDENT ty_kr_list SEMI 17 | TYPE INSTANCE ty_kr_list UIDENT type_list EQ ty_def SEMI - - 18 data_type_head : DATA UIDENT ty_kr_list WHERE - - 19 ty_kr_list : ty_kr_list_aux - - 20 ty_kr_list_aux : - 21 | ty_kr_list_aux LPAREN LIDENT COLON kind_and_role RPAREN - - 22 type_list : type_list_aux - - 23 type_list_aux : - 24 | type_list_aux ty_def - - 25 tylist : tylist_aux - - 26 tylist_aux : - 27 | tylist LIDENT - - 28 clauses : LBRACKET clauses_aux RBRACKET - - 29 clauses_aux : - 30 | clauses_aux clause - - 31 clause : UIDENT DOUBLECOLON LBRACKET ty_kr_list RBRACKET ty_def - 32 | UIDENT DOUBLECOLON ty_def - - 33 ty_def : LIDENT - 34 | LPAREN ARROW RPAREN - 35 | LPAREN ty_def ARROW ty_def RPAREN - 36 | LPAREN TILDE kind RPAREN - 37 | LPAREN ty_def TILDE kind ty_def RPAREN FARROW ty_def - 38 | UIDENT - 39 | LPAREN ty_def ty_def RPAREN - 40 | FORALL LIDENT COLON kind_and_role ty_def - 41 | LPAREN ty_def RPAREN - - 42 term : LIDENT - 43 | LAMBDA LIDENT COLON ty_def ARROW term - 44 | LPAREN term term RPAREN - 45 | LAMBDA LIDENT COLON kind_and_role ARROW term - 46 | LPAREN term TAPP ty_def RPAREN - 47 | UIDENT - 48 | CASE LPAREN ty_def COMMA term RPAREN branches - 49 | LAMBDA LPAREN LIDENT COLON ty_def TILDE ty_def ARROW term - 50 | LPAREN term AT proof RPAREN - 51 | LPAREN term ARROW proof RPAREN - 52 | LPAREN term RPAREN - - 53 branches : LBRACKET bs RBRACKET - - 54 bs : - 55 | bs UIDENT FARROW term SEMI - - 56 proof : LIDENT - 57 | LTRI ty_def RTRI - 58 | LPAREN SYM proof RPAREN - 59 | LPAREN proof SEMI proof RPAREN - 60 | LPAREN proof proof RPAREN - 61 | LPAREN NTH INT proof RPAREN - 62 | FORALL LPAREN LIDENT COLON kind_and_role RPAREN proof - 63 | LPAREN proof AT ty_def RPAREN - - 64 %entry% : '\001' input - 65 | '\002' kind - 66 | '\003' kind_and_role - 67 | '\010' ty_def - 68 | '\005' term - 69 | '\006' proof - 70 | '\007' ty_dec - 71 | '\011' clause + 18 | TYPE INSTANCE UIDENT type_list EQ ty_def SEMI + + 19 data_type_head : DATA UIDENT ty_kr_list WHERE + + 20 ty_kr_list : ty_kr_list_aux + + 21 ty_kr_list_aux : + 22 | ty_kr_list_aux LPAREN LIDENT COLON kind_and_role RPAREN + + 23 type_list : type_list_aux + + 24 type_list_aux : + 25 | type_list_aux ty_def + + 26 tylist : tylist_aux + + 27 tylist_aux : + 28 | tylist LIDENT + + 29 clauses : LBRACKET clauses_aux RBRACKET + + 30 clauses_aux : + 31 | clauses_aux clause + + 32 clause : UIDENT DOUBLECOLON LBRACKET ty_kr_list RBRACKET ty_def + 33 | UIDENT DOUBLECOLON ty_def + + 34 ty_def : LIDENT + 35 | LPAREN ARROW RPAREN + 36 | LPAREN ty_def ARROW ty_def RPAREN + 37 | LPAREN TILDE kind RPAREN + 38 | LPAREN ty_def TILDE kind ty_def RPAREN FARROW ty_def + 39 | UIDENT + 40 | LPAREN ty_def ty_def RPAREN + 41 | FORALL LIDENT COLON kind_and_role ty_def + 42 | LPAREN ty_def RPAREN + + 43 term : LIDENT + 44 | LAMBDA LIDENT COLON ty_def ARROW term + 45 | LPAREN term term RPAREN + 46 | LAMBDA LIDENT COLON kind_and_role ARROW term + 47 | LPAREN term TAPP ty_def RPAREN + 48 | UIDENT + 49 | CASE LPAREN ty_def COMMA term RPAREN branches + 50 | LAMBDA LPAREN LIDENT COLON ty_def TILDE ty_def ARROW term + 51 | LPAREN term AT proof RPAREN + 52 | LPAREN term ARROW proof RPAREN + 53 | LPAREN term RPAREN + + 54 branches : LBRACKET bs RBRACKET + + 55 bs : + 56 | bs UIDENT FARROW term SEMI + + 57 proof : LIDENT + 58 | LTRI ty_def RTRI + 59 | LPAREN SYM proof RPAREN + 60 | LPAREN proof SEMI proof RPAREN + 61 | LPAREN proof proof RPAREN + 62 | LPAREN NTH INT proof RPAREN + 63 | FORALL LPAREN LIDENT COLON kind_and_role RPAREN proof + 64 | LPAREN proof AT ty_def RPAREN + + 65 %entry% : '\001' input + 66 | '\002' kind + 67 | '\003' kind_and_role + 68 | '\010' ty_def + 69 | '\005' term + 70 | '\006' proof + 71 | '\007' ty_dec + 72 | '\011' clause state 0 $accept : . %entry% $end (0) @@ -110,7 +111,7 @@ state 0 state 1 - %entry% : '\001' . input (64) + %entry% : '\001' . input (65) TYPE shift 10 CASE shift 11 @@ -131,7 +132,7 @@ state 1 state 2 - %entry% : '\002' . kind (65) + %entry% : '\002' . kind (66) STAR shift 24 LPAREN shift 25 @@ -142,7 +143,7 @@ state 2 state 3 - %entry% : '\003' . kind_and_role (66) + %entry% : '\003' . kind_and_role (67) STAR shift 28 LPAREN shift 29 @@ -152,7 +153,7 @@ state 3 state 4 - %entry% : '\010' . ty_def (67) + %entry% : '\010' . ty_def (68) FORALL shift 31 LIDENT shift 32 @@ -164,7 +165,7 @@ state 4 state 5 - %entry% : '\005' . term (68) + %entry% : '\005' . term (69) CASE shift 11 LIDENT shift 14 @@ -177,7 +178,7 @@ state 5 state 6 - %entry% : '\006' . proof (69) + %entry% : '\006' . proof (70) FORALL shift 37 LIDENT shift 38 @@ -189,7 +190,7 @@ state 6 state 7 - %entry% : '\007' . ty_dec (70) + %entry% : '\007' . ty_dec (71) TYPE shift 10 DATA shift 12 @@ -201,7 +202,7 @@ state 7 state 8 - %entry% : '\011' . clause (71) + %entry% : '\011' . clause (72) UIDENT shift 43 . error @@ -218,6 +219,7 @@ state 9 state 10 ty_dec : TYPE . FAMILY UIDENT ty_kr_list SEMI (16) ty_dec : TYPE . INSTANCE ty_kr_list UIDENT type_list EQ ty_def SEMI (17) + ty_dec : TYPE . INSTANCE UIDENT type_list EQ ty_def SEMI (18) FAMILY shift 45 INSTANCE shift 46 @@ -225,14 +227,14 @@ state 10 state 11 - term : CASE . LPAREN ty_def COMMA term RPAREN branches (48) + term : CASE . LPAREN ty_def COMMA term RPAREN branches (49) LPAREN shift 47 . error state 12 - data_type_head : DATA . UIDENT ty_kr_list WHERE (18) + data_type_head : DATA . UIDENT ty_kr_list WHERE (19) UIDENT shift 48 . error @@ -246,23 +248,23 @@ state 13 state 14 - term : LIDENT . (42) + term : LIDENT . (43) - . reduce 42 + . reduce 43 state 15 - term : UIDENT . (47) + term : UIDENT . (48) - . reduce 47 + . reduce 48 state 16 - term : LPAREN . term term RPAREN (44) - term : LPAREN . term TAPP ty_def RPAREN (46) - term : LPAREN . term AT proof RPAREN (50) - term : LPAREN . term ARROW proof RPAREN (51) - term : LPAREN . term RPAREN (52) + term : LPAREN . term term RPAREN (45) + term : LPAREN . term TAPP ty_def RPAREN (47) + term : LPAREN . term AT proof RPAREN (51) + term : LPAREN . term ARROW proof RPAREN (52) + term : LPAREN . term RPAREN (53) CASE shift 11 LIDENT shift 14 @@ -281,9 +283,9 @@ state 17 state 18 - term : LAMBDA . LIDENT COLON ty_def ARROW term (43) - term : LAMBDA . LIDENT COLON kind_and_role ARROW term (45) - term : LAMBDA . LPAREN LIDENT COLON ty_def TILDE ty_def ARROW term (49) + term : LAMBDA . LIDENT COLON ty_def ARROW term (44) + term : LAMBDA . LIDENT COLON kind_and_role ARROW term (46) + term : LAMBDA . LPAREN LIDENT COLON ty_def TILDE ty_def ARROW term (50) LIDENT shift 51 LPAREN shift 52 @@ -291,9 +293,9 @@ state 18 state 19 - %entry% : '\001' input . (64) + %entry% : '\001' input . (65) - . reduce 64 + . reduce 65 state 20 @@ -364,9 +366,9 @@ state 25 state 26 - %entry% : '\002' kind . (65) + %entry% : '\002' kind . (66) - . reduce 65 + . reduce 66 state 27 @@ -395,37 +397,37 @@ state 29 state 30 - %entry% : '\003' kind_and_role . (66) + %entry% : '\003' kind_and_role . (67) - . reduce 66 + . reduce 67 state 31 - ty_def : FORALL . LIDENT COLON kind_and_role ty_def (40) + ty_def : FORALL . LIDENT COLON kind_and_role ty_def (41) LIDENT shift 62 . error state 32 - ty_def : LIDENT . (33) + ty_def : LIDENT . (34) - . reduce 33 + . reduce 34 state 33 - ty_def : UIDENT . (38) + ty_def : UIDENT . (39) - . reduce 38 + . reduce 39 state 34 - ty_def : LPAREN . ARROW RPAREN (34) - ty_def : LPAREN . ty_def ARROW ty_def RPAREN (35) - ty_def : LPAREN . TILDE kind RPAREN (36) - ty_def : LPAREN . ty_def TILDE kind ty_def RPAREN FARROW ty_def (37) - ty_def : LPAREN . ty_def ty_def RPAREN (39) - ty_def : LPAREN . ty_def RPAREN (41) + ty_def : LPAREN . ARROW RPAREN (35) + ty_def : LPAREN . ty_def ARROW ty_def RPAREN (36) + ty_def : LPAREN . TILDE kind RPAREN (37) + ty_def : LPAREN . ty_def TILDE kind ty_def RPAREN FARROW ty_def (38) + ty_def : LPAREN . ty_def ty_def RPAREN (40) + ty_def : LPAREN . ty_def RPAREN (42) FORALL shift 31 LIDENT shift 32 @@ -439,36 +441,36 @@ state 34 state 35 - %entry% : '\010' ty_def . (67) + %entry% : '\010' ty_def . (68) - . reduce 67 + . reduce 68 state 36 - %entry% : '\005' term . (68) + %entry% : '\005' term . (69) - . reduce 68 + . reduce 69 state 37 - proof : FORALL . LPAREN LIDENT COLON kind_and_role RPAREN proof (62) + proof : FORALL . LPAREN LIDENT COLON kind_and_role RPAREN proof (63) LPAREN shift 66 . error state 38 - proof : LIDENT . (56) + proof : LIDENT . (57) - . reduce 56 + . reduce 57 state 39 - proof : LPAREN . SYM proof RPAREN (58) - proof : LPAREN . proof SEMI proof RPAREN (59) - proof : LPAREN . proof proof RPAREN (60) - proof : LPAREN . NTH INT proof RPAREN (61) - proof : LPAREN . proof AT ty_def RPAREN (63) + proof : LPAREN . SYM proof RPAREN (59) + proof : LPAREN . proof SEMI proof RPAREN (60) + proof : LPAREN . proof proof RPAREN (61) + proof : LPAREN . NTH INT proof RPAREN (62) + proof : LPAREN . proof AT ty_def RPAREN (64) FORALL shift 37 NTH shift 67 @@ -482,7 +484,7 @@ state 39 state 40 - proof : LTRI . ty_def RTRI (57) + proof : LTRI . ty_def RTRI (58) FORALL shift 31 LIDENT shift 32 @@ -494,29 +496,29 @@ state 40 state 41 - %entry% : '\006' proof . (69) + %entry% : '\006' proof . (70) - . reduce 69 + . reduce 70 state 42 - %entry% : '\007' ty_dec . (70) + %entry% : '\007' ty_dec . (71) - . reduce 70 + . reduce 71 state 43 - clause : UIDENT . DOUBLECOLON LBRACKET ty_kr_list RBRACKET ty_def (31) - clause : UIDENT . DOUBLECOLON ty_def (32) + clause : UIDENT . DOUBLECOLON LBRACKET ty_kr_list RBRACKET ty_def (32) + clause : UIDENT . DOUBLECOLON ty_def (33) DOUBLECOLON shift 71 . error state 44 - %entry% : '\011' clause . (71) + %entry% : '\011' clause . (72) - . reduce 71 + . reduce 72 state 45 @@ -526,18 +528,21 @@ state 45 . error +46: shift/reduce conflict (shift 73, reduce 21) on UIDENT state 46 ty_dec : TYPE INSTANCE . ty_kr_list UIDENT type_list EQ ty_def SEMI (17) - ty_kr_list_aux : . (20) + ty_dec : TYPE INSTANCE . UIDENT type_list EQ ty_def SEMI (18) + ty_kr_list_aux : . (21) - . reduce 20 + UIDENT shift 73 + LPAREN reduce 21 - ty_kr_list goto 73 - ty_kr_list_aux goto 74 + ty_kr_list goto 74 + ty_kr_list_aux goto 75 state 47 - term : CASE LPAREN . ty_def COMMA term RPAREN branches (48) + term : CASE LPAREN . ty_def COMMA term RPAREN branches (49) FORALL shift 31 LIDENT shift 32 @@ -545,59 +550,59 @@ state 47 LPAREN shift 34 . error - ty_def goto 75 + ty_def goto 76 state 48 - data_type_head : DATA UIDENT . ty_kr_list WHERE (18) - ty_kr_list_aux : . (20) + data_type_head : DATA UIDENT . ty_kr_list WHERE (19) + ty_kr_list_aux : . (21) - . reduce 20 + . reduce 21 - ty_kr_list goto 76 - ty_kr_list_aux goto 74 + ty_kr_list goto 77 + ty_kr_list_aux goto 75 state 49 ty_dec : NEWTYPE UIDENT . EQ UIDENT ty_def SEMI (15) - EQ shift 77 + EQ shift 78 . error state 50 - term : LPAREN term . term RPAREN (44) - term : LPAREN term . TAPP ty_def RPAREN (46) - term : LPAREN term . AT proof RPAREN (50) - term : LPAREN term . ARROW proof RPAREN (51) - term : LPAREN term . RPAREN (52) + term : LPAREN term . term RPAREN (45) + term : LPAREN term . TAPP ty_def RPAREN (47) + term : LPAREN term . AT proof RPAREN (51) + term : LPAREN term . ARROW proof RPAREN (52) + term : LPAREN term . RPAREN (53) CASE shift 11 LIDENT shift 14 UIDENT shift 15 - ARROW shift 78 + ARROW shift 79 LPAREN shift 16 - RPAREN shift 79 + RPAREN shift 80 LAMBDA shift 18 - AT shift 80 - TAPP shift 81 + AT shift 81 + TAPP shift 82 . error - term goto 82 + term goto 83 state 51 - term : LAMBDA LIDENT . COLON ty_def ARROW term (43) - term : LAMBDA LIDENT . COLON kind_and_role ARROW term (45) + term : LAMBDA LIDENT . COLON ty_def ARROW term (44) + term : LAMBDA LIDENT . COLON kind_and_role ARROW term (46) - COLON shift 83 + COLON shift 84 . error state 52 - term : LAMBDA LPAREN . LIDENT COLON ty_def TILDE ty_def ARROW term (49) + term : LAMBDA LPAREN . LIDENT COLON ty_def TILDE ty_def ARROW term (50) - LIDENT shift 84 + LIDENT shift 85 . error @@ -610,7 +615,7 @@ state 53 state 54 input_aux : input_aux term . SEMI (6) - SEMI shift 85 + SEMI shift 86 . error @@ -621,36 +626,36 @@ state 55 state 56 - clauses : LBRACKET . clauses_aux RBRACKET (28) - clauses_aux : . (29) + clauses : LBRACKET . clauses_aux RBRACKET (29) + clauses_aux : . (30) - . reduce 29 + . reduce 30 - clauses_aux goto 86 + clauses_aux goto 87 state 57 ty_dec : data_type_head clauses . SEMI (14) - SEMI shift 87 + SEMI shift 88 . error state 58 kind_and_role : STAR SLASH . role (11) - CODE shift 88 - TYPE shift 89 + CODE shift 89 + TYPE shift 90 . error - role goto 90 + role goto 91 state 59 kind : LPAREN kind . RPAREN (9) kind_and_role : LPAREN kind . RPAREN SLASH role (10) - RPAREN shift 91 + RPAREN shift 92 . error @@ -661,76 +666,76 @@ state 60 LPAREN shift 25 . error - kind goto 92 + kind goto 93 kind_and_role goto 27 state 61 kind_and_role : LPAREN kind . RPAREN SLASH role (10) - RPAREN shift 93 + RPAREN shift 94 . error state 62 - ty_def : FORALL LIDENT . COLON kind_and_role ty_def (40) + ty_def : FORALL LIDENT . COLON kind_and_role ty_def (41) - COLON shift 94 + COLON shift 95 . error state 63 - ty_def : LPAREN ARROW . RPAREN (34) + ty_def : LPAREN ARROW . RPAREN (35) - RPAREN shift 95 + RPAREN shift 96 . error state 64 - ty_def : LPAREN TILDE . kind RPAREN (36) + ty_def : LPAREN TILDE . kind RPAREN (37) STAR shift 24 LPAREN shift 25 . error - kind goto 96 + kind goto 97 kind_and_role goto 27 state 65 - ty_def : LPAREN ty_def . ARROW ty_def RPAREN (35) - ty_def : LPAREN ty_def . TILDE kind ty_def RPAREN FARROW ty_def (37) - ty_def : LPAREN ty_def . ty_def RPAREN (39) - ty_def : LPAREN ty_def . RPAREN (41) + ty_def : LPAREN ty_def . ARROW ty_def RPAREN (36) + ty_def : LPAREN ty_def . TILDE kind ty_def RPAREN FARROW ty_def (38) + ty_def : LPAREN ty_def . ty_def RPAREN (40) + ty_def : LPAREN ty_def . RPAREN (42) FORALL shift 31 LIDENT shift 32 UIDENT shift 33 - ARROW shift 97 + ARROW shift 98 LPAREN shift 34 - RPAREN shift 98 - TILDE shift 99 + RPAREN shift 99 + TILDE shift 100 . error - ty_def goto 100 + ty_def goto 101 state 66 - proof : FORALL LPAREN . LIDENT COLON kind_and_role RPAREN proof (62) + proof : FORALL LPAREN . LIDENT COLON kind_and_role RPAREN proof (63) - LIDENT shift 101 + LIDENT shift 102 . error state 67 - proof : LPAREN NTH . INT proof RPAREN (61) + proof : LPAREN NTH . INT proof RPAREN (62) - INT shift 102 + INT shift 103 . error state 68 - proof : LPAREN SYM . proof RPAREN (58) + proof : LPAREN SYM . proof RPAREN (59) FORALL shift 37 LIDENT shift 38 @@ -738,97 +743,107 @@ state 68 LTRI shift 40 . error - proof goto 103 + proof goto 104 state 69 - proof : LPAREN proof . SEMI proof RPAREN (59) - proof : LPAREN proof . proof RPAREN (60) - proof : LPAREN proof . AT ty_def RPAREN (63) + proof : LPAREN proof . SEMI proof RPAREN (60) + proof : LPAREN proof . proof RPAREN (61) + proof : LPAREN proof . AT ty_def RPAREN (64) FORALL shift 37 LIDENT shift 38 LPAREN shift 39 - SEMI shift 104 + SEMI shift 105 LTRI shift 40 - AT shift 105 + AT shift 106 . error - proof goto 106 + proof goto 107 state 70 - proof : LTRI ty_def . RTRI (57) + proof : LTRI ty_def . RTRI (58) - RTRI shift 107 + RTRI shift 108 . error state 71 - clause : UIDENT DOUBLECOLON . LBRACKET ty_kr_list RBRACKET ty_def (31) - clause : UIDENT DOUBLECOLON . ty_def (32) + clause : UIDENT DOUBLECOLON . LBRACKET ty_kr_list RBRACKET ty_def (32) + clause : UIDENT DOUBLECOLON . ty_def (33) FORALL shift 31 LIDENT shift 32 UIDENT shift 33 LPAREN shift 34 - LBRACKET shift 108 + LBRACKET shift 109 . error - ty_def goto 109 + ty_def goto 110 state 72 ty_dec : TYPE FAMILY UIDENT . ty_kr_list SEMI (16) - ty_kr_list_aux : . (20) + ty_kr_list_aux : . (21) - . reduce 20 + . reduce 21 - ty_kr_list goto 110 - ty_kr_list_aux goto 74 + ty_kr_list goto 111 + ty_kr_list_aux goto 75 state 73 - ty_dec : TYPE INSTANCE ty_kr_list . UIDENT type_list EQ ty_def SEMI (17) + ty_dec : TYPE INSTANCE UIDENT . type_list EQ ty_def SEMI (18) + type_list_aux : . (24) - UIDENT shift 111 - . error + . reduce 24 + + type_list goto 112 + type_list_aux goto 113 state 74 - ty_kr_list : ty_kr_list_aux . (19) - ty_kr_list_aux : ty_kr_list_aux . LPAREN LIDENT COLON kind_and_role RPAREN (21) + ty_dec : TYPE INSTANCE ty_kr_list . UIDENT type_list EQ ty_def SEMI (17) - LPAREN shift 112 - WHERE reduce 19 - UIDENT reduce 19 - SEMI reduce 19 - RBRACKET reduce 19 + UIDENT shift 114 + . error state 75 - term : CASE LPAREN ty_def . COMMA term RPAREN branches (48) + ty_kr_list : ty_kr_list_aux . (20) + ty_kr_list_aux : ty_kr_list_aux . LPAREN LIDENT COLON kind_and_role RPAREN (22) - COMMA shift 113 - . error + LPAREN shift 115 + WHERE reduce 20 + UIDENT reduce 20 + SEMI reduce 20 + RBRACKET reduce 20 state 76 - data_type_head : DATA UIDENT ty_kr_list . WHERE (18) + term : CASE LPAREN ty_def . COMMA term RPAREN branches (49) - WHERE shift 114 + COMMA shift 116 . error state 77 - ty_dec : NEWTYPE UIDENT EQ . UIDENT ty_def SEMI (15) + data_type_head : DATA UIDENT ty_kr_list . WHERE (19) - UIDENT shift 115 + WHERE shift 117 . error state 78 - term : LPAREN term ARROW . proof RPAREN (51) + ty_dec : NEWTYPE UIDENT EQ . UIDENT ty_def SEMI (15) + + UIDENT shift 118 + . error + + +state 79 + term : LPAREN term ARROW . proof RPAREN (52) FORALL shift 37 LIDENT shift 38 @@ -836,17 +851,17 @@ state 78 LTRI shift 40 . error - proof goto 116 + proof goto 119 -state 79 - term : LPAREN term RPAREN . (52) +state 80 + term : LPAREN term RPAREN . (53) - . reduce 52 + . reduce 53 -state 80 - term : LPAREN term AT . proof RPAREN (50) +state 81 + term : LPAREN term AT . proof RPAREN (51) FORALL shift 37 LIDENT shift 38 @@ -854,11 +869,11 @@ state 80 LTRI shift 40 . error - proof goto 117 + proof goto 120 -state 81 - term : LPAREN term TAPP . ty_def RPAREN (46) +state 82 + term : LPAREN term TAPP . ty_def RPAREN (47) FORALL shift 31 LIDENT shift 32 @@ -866,84 +881,84 @@ state 81 LPAREN shift 34 . error - ty_def goto 118 + ty_def goto 121 -state 82 - term : LPAREN term term . RPAREN (44) +state 83 + term : LPAREN term term . RPAREN (45) - RPAREN shift 119 + RPAREN shift 122 . error -state 83 - term : LAMBDA LIDENT COLON . ty_def ARROW term (43) - term : LAMBDA LIDENT COLON . kind_and_role ARROW term (45) +state 84 + term : LAMBDA LIDENT COLON . ty_def ARROW term (44) + term : LAMBDA LIDENT COLON . kind_and_role ARROW term (46) FORALL shift 31 LIDENT shift 32 UIDENT shift 33 STAR shift 28 - LPAREN shift 120 + LPAREN shift 123 . error - kind_and_role goto 121 - ty_def goto 122 + kind_and_role goto 124 + ty_def goto 125 -state 84 - term : LAMBDA LPAREN LIDENT . COLON ty_def TILDE ty_def ARROW term (49) +state 85 + term : LAMBDA LPAREN LIDENT . COLON ty_def TILDE ty_def ARROW term (50) - COLON shift 123 + COLON shift 126 . error -state 85 +state 86 input_aux : input_aux term SEMI . (6) . reduce 6 -state 86 - clauses : LBRACKET clauses_aux . RBRACKET (28) - clauses_aux : clauses_aux . clause (30) +state 87 + clauses : LBRACKET clauses_aux . RBRACKET (29) + clauses_aux : clauses_aux . clause (31) UIDENT shift 43 - RBRACKET shift 124 + RBRACKET shift 127 . error - clause goto 125 + clause goto 128 -state 87 +state 88 ty_dec : data_type_head clauses SEMI . (14) . reduce 14 -state 88 +state 89 role : CODE . (12) . reduce 12 -state 89 +state 90 role : TYPE . (13) . reduce 13 -state 90 +state 91 kind_and_role : STAR SLASH role . (11) . reduce 11 -state 91 +state 92 kind : LPAREN kind RPAREN . (9) kind_and_role : LPAREN kind RPAREN . SLASH role (10) - SLASH shift 126 + SLASH shift 129 $end reduce 9 FORALL reduce 9 LIDENT reduce 9 @@ -952,44 +967,44 @@ state 91 RPAREN reduce 9 -state 92 +state 93 kind : kind_and_role ARROW kind . (8) . reduce 8 -state 93 +state 94 kind_and_role : LPAREN kind RPAREN . SLASH role (10) - SLASH shift 126 + SLASH shift 129 . error -state 94 - ty_def : FORALL LIDENT COLON . kind_and_role ty_def (40) +state 95 + ty_def : FORALL LIDENT COLON . kind_and_role ty_def (41) STAR shift 28 LPAREN shift 29 . error - kind_and_role goto 127 + kind_and_role goto 130 -state 95 - ty_def : LPAREN ARROW RPAREN . (34) +state 96 + ty_def : LPAREN ARROW RPAREN . (35) - . reduce 34 + . reduce 35 -state 96 - ty_def : LPAREN TILDE kind . RPAREN (36) +state 97 + ty_def : LPAREN TILDE kind . RPAREN (37) - RPAREN shift 128 + RPAREN shift 131 . error -state 97 - ty_def : LPAREN ty_def ARROW . ty_def RPAREN (35) +state 98 + ty_def : LPAREN ty_def ARROW . ty_def RPAREN (36) FORALL shift 31 LIDENT shift 32 @@ -997,42 +1012,42 @@ state 97 LPAREN shift 34 . error - ty_def goto 129 + ty_def goto 132 -state 98 - ty_def : LPAREN ty_def RPAREN . (41) +state 99 + ty_def : LPAREN ty_def RPAREN . (42) - . reduce 41 + . reduce 42 -state 99 - ty_def : LPAREN ty_def TILDE . kind ty_def RPAREN FARROW ty_def (37) +state 100 + ty_def : LPAREN ty_def TILDE . kind ty_def RPAREN FARROW ty_def (38) STAR shift 24 LPAREN shift 25 . error - kind goto 130 + kind goto 133 kind_and_role goto 27 -state 100 - ty_def : LPAREN ty_def ty_def . RPAREN (39) +state 101 + ty_def : LPAREN ty_def ty_def . RPAREN (40) - RPAREN shift 131 + RPAREN shift 134 . error -state 101 - proof : FORALL LPAREN LIDENT . COLON kind_and_role RPAREN proof (62) +state 102 + proof : FORALL LPAREN LIDENT . COLON kind_and_role RPAREN proof (63) - COLON shift 132 + COLON shift 135 . error -state 102 - proof : LPAREN NTH INT . proof RPAREN (61) +state 103 + proof : LPAREN NTH INT . proof RPAREN (62) FORALL shift 37 LIDENT shift 38 @@ -1040,18 +1055,18 @@ state 102 LTRI shift 40 . error - proof goto 133 + proof goto 136 -state 103 - proof : LPAREN SYM proof . RPAREN (58) +state 104 + proof : LPAREN SYM proof . RPAREN (59) - RPAREN shift 134 + RPAREN shift 137 . error -state 104 - proof : LPAREN proof SEMI . proof RPAREN (59) +state 105 + proof : LPAREN proof SEMI . proof RPAREN (60) FORALL shift 37 LIDENT shift 38 @@ -1059,11 +1074,11 @@ state 104 LTRI shift 40 . error - proof goto 135 + proof goto 138 -state 105 - proof : LPAREN proof AT . ty_def RPAREN (63) +state 106 + proof : LPAREN proof AT . ty_def RPAREN (64) FORALL shift 31 LIDENT shift 32 @@ -1071,64 +1086,84 @@ state 105 LPAREN shift 34 . error - ty_def goto 136 + ty_def goto 139 -state 106 - proof : LPAREN proof proof . RPAREN (60) +state 107 + proof : LPAREN proof proof . RPAREN (61) - RPAREN shift 137 + RPAREN shift 140 . error -state 107 - proof : LTRI ty_def RTRI . (57) +state 108 + proof : LTRI ty_def RTRI . (58) - . reduce 57 + . reduce 58 -state 108 - clause : UIDENT DOUBLECOLON LBRACKET . ty_kr_list RBRACKET ty_def (31) - ty_kr_list_aux : . (20) +state 109 + clause : UIDENT DOUBLECOLON LBRACKET . ty_kr_list RBRACKET ty_def (32) + ty_kr_list_aux : . (21) - . reduce 20 + . reduce 21 - ty_kr_list goto 138 - ty_kr_list_aux goto 74 + ty_kr_list goto 141 + ty_kr_list_aux goto 75 -state 109 - clause : UIDENT DOUBLECOLON ty_def . (32) +state 110 + clause : UIDENT DOUBLECOLON ty_def . (33) - . reduce 32 + . reduce 33 -state 110 +state 111 ty_dec : TYPE FAMILY UIDENT ty_kr_list . SEMI (16) - SEMI shift 139 + SEMI shift 142 . error -state 111 +state 112 + ty_dec : TYPE INSTANCE UIDENT type_list . EQ ty_def SEMI (18) + + EQ shift 143 + . error + + +state 113 + type_list : type_list_aux . (23) + type_list_aux : type_list_aux . ty_def (25) + + FORALL shift 31 + LIDENT shift 32 + UIDENT shift 33 + LPAREN shift 34 + EQ reduce 23 + + ty_def goto 144 + + +state 114 ty_dec : TYPE INSTANCE ty_kr_list UIDENT . type_list EQ ty_def SEMI (17) - type_list_aux : . (23) + type_list_aux : . (24) - . reduce 23 + . reduce 24 - type_list goto 140 - type_list_aux goto 141 + type_list goto 145 + type_list_aux goto 113 -state 112 - ty_kr_list_aux : ty_kr_list_aux LPAREN . LIDENT COLON kind_and_role RPAREN (21) +state 115 + ty_kr_list_aux : ty_kr_list_aux LPAREN . LIDENT COLON kind_and_role RPAREN (22) - LIDENT shift 142 + LIDENT shift 146 . error -state 113 - term : CASE LPAREN ty_def COMMA . term RPAREN branches (48) +state 116 + term : CASE LPAREN ty_def COMMA . term RPAREN branches (49) CASE shift 11 LIDENT shift 14 @@ -1137,16 +1172,16 @@ state 113 LAMBDA shift 18 . error - term goto 143 + term goto 147 -state 114 - data_type_head : DATA UIDENT ty_kr_list WHERE . (18) +state 117 + data_type_head : DATA UIDENT ty_kr_list WHERE . (19) - . reduce 18 + . reduce 19 -state 115 +state 118 ty_dec : NEWTYPE UIDENT EQ UIDENT . ty_def SEMI (15) FORALL shift 31 @@ -1155,51 +1190,51 @@ state 115 LPAREN shift 34 . error - ty_def goto 144 + ty_def goto 148 -state 116 - term : LPAREN term ARROW proof . RPAREN (51) +state 119 + term : LPAREN term ARROW proof . RPAREN (52) - RPAREN shift 145 + RPAREN shift 149 . error -state 117 - term : LPAREN term AT proof . RPAREN (50) +state 120 + term : LPAREN term AT proof . RPAREN (51) - RPAREN shift 146 + RPAREN shift 150 . error -state 118 - term : LPAREN term TAPP ty_def . RPAREN (46) +state 121 + term : LPAREN term TAPP ty_def . RPAREN (47) - RPAREN shift 147 + RPAREN shift 151 . error -state 119 - term : LPAREN term term RPAREN . (44) +state 122 + term : LPAREN term term RPAREN . (45) - . reduce 44 + . reduce 45 -state 120 +state 123 kind_and_role : LPAREN . kind RPAREN SLASH role (10) - ty_def : LPAREN . ARROW RPAREN (34) - ty_def : LPAREN . ty_def ARROW ty_def RPAREN (35) - ty_def : LPAREN . TILDE kind RPAREN (36) - ty_def : LPAREN . ty_def TILDE kind ty_def RPAREN FARROW ty_def (37) - ty_def : LPAREN . ty_def ty_def RPAREN (39) - ty_def : LPAREN . ty_def RPAREN (41) + ty_def : LPAREN . ARROW RPAREN (35) + ty_def : LPAREN . ty_def ARROW ty_def RPAREN (36) + ty_def : LPAREN . TILDE kind RPAREN (37) + ty_def : LPAREN . ty_def TILDE kind ty_def RPAREN FARROW ty_def (38) + ty_def : LPAREN . ty_def ty_def RPAREN (40) + ty_def : LPAREN . ty_def RPAREN (42) FORALL shift 31 LIDENT shift 32 UIDENT shift 33 STAR shift 24 ARROW shift 63 - LPAREN shift 148 + LPAREN shift 152 TILDE shift 64 . error @@ -1208,22 +1243,22 @@ state 120 ty_def goto 65 -state 121 - term : LAMBDA LIDENT COLON kind_and_role . ARROW term (45) +state 124 + term : LAMBDA LIDENT COLON kind_and_role . ARROW term (46) - ARROW shift 149 + ARROW shift 153 . error -state 122 - term : LAMBDA LIDENT COLON ty_def . ARROW term (43) +state 125 + term : LAMBDA LIDENT COLON ty_def . ARROW term (44) - ARROW shift 150 + ARROW shift 154 . error -state 123 - term : LAMBDA LPAREN LIDENT COLON . ty_def TILDE ty_def ARROW term (49) +state 126 + term : LAMBDA LPAREN LIDENT COLON . ty_def TILDE ty_def ARROW term (50) FORALL shift 31 LIDENT shift 32 @@ -1231,33 +1266,33 @@ state 123 LPAREN shift 34 . error - ty_def goto 151 + ty_def goto 155 -state 124 - clauses : LBRACKET clauses_aux RBRACKET . (28) +state 127 + clauses : LBRACKET clauses_aux RBRACKET . (29) - . reduce 28 + . reduce 29 -state 125 - clauses_aux : clauses_aux clause . (30) +state 128 + clauses_aux : clauses_aux clause . (31) - . reduce 30 + . reduce 31 -state 126 +state 129 kind_and_role : LPAREN kind RPAREN SLASH . role (10) - CODE shift 88 - TYPE shift 89 + CODE shift 89 + TYPE shift 90 . error - role goto 152 + role goto 156 -state 127 - ty_def : FORALL LIDENT COLON kind_and_role . ty_def (40) +state 130 + ty_def : FORALL LIDENT COLON kind_and_role . ty_def (41) FORALL shift 31 LIDENT shift 32 @@ -1265,24 +1300,24 @@ state 127 LPAREN shift 34 . error - ty_def goto 153 + ty_def goto 157 -state 128 - ty_def : LPAREN TILDE kind RPAREN . (36) +state 131 + ty_def : LPAREN TILDE kind RPAREN . (37) - . reduce 36 + . reduce 37 -state 129 - ty_def : LPAREN ty_def ARROW ty_def . RPAREN (35) +state 132 + ty_def : LPAREN ty_def ARROW ty_def . RPAREN (36) - RPAREN shift 154 + RPAREN shift 158 . error -state 130 - ty_def : LPAREN ty_def TILDE kind . ty_def RPAREN FARROW ty_def (37) +state 133 + ty_def : LPAREN ty_def TILDE kind . ty_def RPAREN FARROW ty_def (38) FORALL shift 31 LIDENT shift 32 @@ -1290,146 +1325,151 @@ state 130 LPAREN shift 34 . error - ty_def goto 155 + ty_def goto 159 -state 131 - ty_def : LPAREN ty_def ty_def RPAREN . (39) +state 134 + ty_def : LPAREN ty_def ty_def RPAREN . (40) - . reduce 39 + . reduce 40 -state 132 - proof : FORALL LPAREN LIDENT COLON . kind_and_role RPAREN proof (62) +state 135 + proof : FORALL LPAREN LIDENT COLON . kind_and_role RPAREN proof (63) STAR shift 28 LPAREN shift 29 . error - kind_and_role goto 156 + kind_and_role goto 160 -state 133 - proof : LPAREN NTH INT proof . RPAREN (61) +state 136 + proof : LPAREN NTH INT proof . RPAREN (62) - RPAREN shift 157 + RPAREN shift 161 . error -state 134 - proof : LPAREN SYM proof RPAREN . (58) +state 137 + proof : LPAREN SYM proof RPAREN . (59) - . reduce 58 + . reduce 59 -state 135 - proof : LPAREN proof SEMI proof . RPAREN (59) +state 138 + proof : LPAREN proof SEMI proof . RPAREN (60) - RPAREN shift 158 + RPAREN shift 162 . error -state 136 - proof : LPAREN proof AT ty_def . RPAREN (63) +state 139 + proof : LPAREN proof AT ty_def . RPAREN (64) - RPAREN shift 159 + RPAREN shift 163 . error -state 137 - proof : LPAREN proof proof RPAREN . (60) +state 140 + proof : LPAREN proof proof RPAREN . (61) - . reduce 60 + . reduce 61 -state 138 - clause : UIDENT DOUBLECOLON LBRACKET ty_kr_list . RBRACKET ty_def (31) +state 141 + clause : UIDENT DOUBLECOLON LBRACKET ty_kr_list . RBRACKET ty_def (32) - RBRACKET shift 160 + RBRACKET shift 164 . error -state 139 +state 142 ty_dec : TYPE FAMILY UIDENT ty_kr_list SEMI . (16) . reduce 16 -state 140 - ty_dec : TYPE INSTANCE ty_kr_list UIDENT type_list . EQ ty_def SEMI (17) - - EQ shift 161 - . error - - -state 141 - type_list : type_list_aux . (22) - type_list_aux : type_list_aux . ty_def (24) +state 143 + ty_dec : TYPE INSTANCE UIDENT type_list EQ . ty_def SEMI (18) FORALL shift 31 LIDENT shift 32 UIDENT shift 33 LPAREN shift 34 - EQ reduce 22 + . error - ty_def goto 162 + ty_def goto 165 -state 142 - ty_kr_list_aux : ty_kr_list_aux LPAREN LIDENT . COLON kind_and_role RPAREN (21) +state 144 + type_list_aux : type_list_aux ty_def . (25) + + . reduce 25 + + +state 145 + ty_dec : TYPE INSTANCE ty_kr_list UIDENT type_list . EQ ty_def SEMI (17) - COLON shift 163 + EQ shift 166 . error -state 143 - term : CASE LPAREN ty_def COMMA term . RPAREN branches (48) +state 146 + ty_kr_list_aux : ty_kr_list_aux LPAREN LIDENT . COLON kind_and_role RPAREN (22) - RPAREN shift 164 + COLON shift 167 . error -state 144 +state 147 + term : CASE LPAREN ty_def COMMA term . RPAREN branches (49) + + RPAREN shift 168 + . error + + +state 148 ty_dec : NEWTYPE UIDENT EQ UIDENT ty_def . SEMI (15) - SEMI shift 165 + SEMI shift 169 . error -state 145 - term : LPAREN term ARROW proof RPAREN . (51) +state 149 + term : LPAREN term ARROW proof RPAREN . (52) - . reduce 51 + . reduce 52 -state 146 - term : LPAREN term AT proof RPAREN . (50) +state 150 + term : LPAREN term AT proof RPAREN . (51) - . reduce 50 + . reduce 51 -state 147 - term : LPAREN term TAPP ty_def RPAREN . (46) +state 151 + term : LPAREN term TAPP ty_def RPAREN . (47) - . reduce 46 + . reduce 47 -state 148 +state 152 kind : LPAREN . kind RPAREN (9) kind_and_role : LPAREN . kind RPAREN SLASH role (10) - ty_def : LPAREN . ARROW RPAREN (34) - ty_def : LPAREN . ty_def ARROW ty_def RPAREN (35) - ty_def : LPAREN . TILDE kind RPAREN (36) - ty_def : LPAREN . ty_def TILDE kind ty_def RPAREN FARROW ty_def (37) - ty_def : LPAREN . ty_def ty_def RPAREN (39) - ty_def : LPAREN . ty_def RPAREN (41) + ty_def : LPAREN . ARROW RPAREN (35) + ty_def : LPAREN . ty_def ARROW ty_def RPAREN (36) + ty_def : LPAREN . TILDE kind RPAREN (37) + ty_def : LPAREN . ty_def TILDE kind ty_def RPAREN FARROW ty_def (38) + ty_def : LPAREN . ty_def ty_def RPAREN (40) + ty_def : LPAREN . ty_def RPAREN (42) FORALL shift 31 LIDENT shift 32 UIDENT shift 33 STAR shift 24 ARROW shift 63 - LPAREN shift 148 + LPAREN shift 152 TILDE shift 64 . error @@ -1438,8 +1478,8 @@ state 148 ty_def goto 65 -state 149 - term : LAMBDA LIDENT COLON kind_and_role ARROW . term (45) +state 153 + term : LAMBDA LIDENT COLON kind_and_role ARROW . term (46) CASE shift 11 LIDENT shift 14 @@ -1448,11 +1488,11 @@ state 149 LAMBDA shift 18 . error - term goto 166 + term goto 170 -state 150 - term : LAMBDA LIDENT COLON ty_def ARROW . term (43) +state 154 + term : LAMBDA LIDENT COLON ty_def ARROW . term (44) CASE shift 11 LIDENT shift 14 @@ -1461,68 +1501,68 @@ state 150 LAMBDA shift 18 . error - term goto 167 + term goto 171 -state 151 - term : LAMBDA LPAREN LIDENT COLON ty_def . TILDE ty_def ARROW term (49) +state 155 + term : LAMBDA LPAREN LIDENT COLON ty_def . TILDE ty_def ARROW term (50) - TILDE shift 168 + TILDE shift 172 . error -state 152 +state 156 kind_and_role : LPAREN kind RPAREN SLASH role . (10) . reduce 10 -state 153 - ty_def : FORALL LIDENT COLON kind_and_role ty_def . (40) +state 157 + ty_def : FORALL LIDENT COLON kind_and_role ty_def . (41) - . reduce 40 + . reduce 41 -state 154 - ty_def : LPAREN ty_def ARROW ty_def RPAREN . (35) +state 158 + ty_def : LPAREN ty_def ARROW ty_def RPAREN . (36) - . reduce 35 + . reduce 36 -state 155 - ty_def : LPAREN ty_def TILDE kind ty_def . RPAREN FARROW ty_def (37) +state 159 + ty_def : LPAREN ty_def TILDE kind ty_def . RPAREN FARROW ty_def (38) - RPAREN shift 169 + RPAREN shift 173 . error -state 156 - proof : FORALL LPAREN LIDENT COLON kind_and_role . RPAREN proof (62) +state 160 + proof : FORALL LPAREN LIDENT COLON kind_and_role . RPAREN proof (63) - RPAREN shift 170 + RPAREN shift 174 . error -state 157 - proof : LPAREN NTH INT proof RPAREN . (61) +state 161 + proof : LPAREN NTH INT proof RPAREN . (62) - . reduce 61 + . reduce 62 -state 158 - proof : LPAREN proof SEMI proof RPAREN . (59) +state 162 + proof : LPAREN proof SEMI proof RPAREN . (60) - . reduce 59 + . reduce 60 -state 159 - proof : LPAREN proof AT ty_def RPAREN . (63) +state 163 + proof : LPAREN proof AT ty_def RPAREN . (64) - . reduce 63 + . reduce 64 -state 160 - clause : UIDENT DOUBLECOLON LBRACKET ty_kr_list RBRACKET . ty_def (31) +state 164 + clause : UIDENT DOUBLECOLON LBRACKET ty_kr_list RBRACKET . ty_def (32) FORALL shift 31 LIDENT shift 32 @@ -1530,10 +1570,17 @@ state 160 LPAREN shift 34 . error - ty_def goto 171 + ty_def goto 175 -state 161 +state 165 + ty_dec : TYPE INSTANCE UIDENT type_list EQ ty_def . SEMI (18) + + SEMI shift 176 + . error + + +state 166 ty_dec : TYPE INSTANCE ty_kr_list UIDENT type_list EQ . ty_def SEMI (17) FORALL shift 31 @@ -1542,54 +1589,48 @@ state 161 LPAREN shift 34 . error - ty_def goto 172 - - -state 162 - type_list_aux : type_list_aux ty_def . (24) - - . reduce 24 + ty_def goto 177 -state 163 - ty_kr_list_aux : ty_kr_list_aux LPAREN LIDENT COLON . kind_and_role RPAREN (21) +state 167 + ty_kr_list_aux : ty_kr_list_aux LPAREN LIDENT COLON . kind_and_role RPAREN (22) STAR shift 28 LPAREN shift 29 . error - kind_and_role goto 173 + kind_and_role goto 178 -state 164 - term : CASE LPAREN ty_def COMMA term RPAREN . branches (48) +state 168 + term : CASE LPAREN ty_def COMMA term RPAREN . branches (49) - LBRACKET shift 174 + LBRACKET shift 179 . error - branches goto 175 + branches goto 180 -state 165 +state 169 ty_dec : NEWTYPE UIDENT EQ UIDENT ty_def SEMI . (15) . reduce 15 -state 166 - term : LAMBDA LIDENT COLON kind_and_role ARROW term . (45) +state 170 + term : LAMBDA LIDENT COLON kind_and_role ARROW term . (46) - . reduce 45 + . reduce 46 -state 167 - term : LAMBDA LIDENT COLON ty_def ARROW term . (43) +state 171 + term : LAMBDA LIDENT COLON ty_def ARROW term . (44) - . reduce 43 + . reduce 44 -state 168 - term : LAMBDA LPAREN LIDENT COLON ty_def TILDE . ty_def ARROW term (49) +state 172 + term : LAMBDA LPAREN LIDENT COLON ty_def TILDE . ty_def ARROW term (50) FORALL shift 31 LIDENT shift 32 @@ -1597,18 +1638,18 @@ state 168 LPAREN shift 34 . error - ty_def goto 176 + ty_def goto 181 -state 169 - ty_def : LPAREN ty_def TILDE kind ty_def RPAREN . FARROW ty_def (37) +state 173 + ty_def : LPAREN ty_def TILDE kind ty_def RPAREN . FARROW ty_def (38) - FARROW shift 177 + FARROW shift 182 . error -state 170 - proof : FORALL LPAREN LIDENT COLON kind_and_role RPAREN . proof (62) +state 174 + proof : FORALL LPAREN LIDENT COLON kind_and_role RPAREN . proof (63) FORALL shift 37 LIDENT shift 38 @@ -1616,53 +1657,59 @@ state 170 LTRI shift 40 . error - proof goto 178 + proof goto 183 -state 171 - clause : UIDENT DOUBLECOLON LBRACKET ty_kr_list RBRACKET ty_def . (31) +state 175 + clause : UIDENT DOUBLECOLON LBRACKET ty_kr_list RBRACKET ty_def . (32) - . reduce 31 + . reduce 32 -state 172 +state 176 + ty_dec : TYPE INSTANCE UIDENT type_list EQ ty_def SEMI . (18) + + . reduce 18 + + +state 177 ty_dec : TYPE INSTANCE ty_kr_list UIDENT type_list EQ ty_def . SEMI (17) - SEMI shift 179 + SEMI shift 184 . error -state 173 - ty_kr_list_aux : ty_kr_list_aux LPAREN LIDENT COLON kind_and_role . RPAREN (21) +state 178 + ty_kr_list_aux : ty_kr_list_aux LPAREN LIDENT COLON kind_and_role . RPAREN (22) - RPAREN shift 180 + RPAREN shift 185 . error -state 174 - branches : LBRACKET . bs RBRACKET (53) - bs : . (54) +state 179 + branches : LBRACKET . bs RBRACKET (54) + bs : . (55) - . reduce 54 + . reduce 55 - bs goto 181 + bs goto 186 -state 175 - term : CASE LPAREN ty_def COMMA term RPAREN branches . (48) +state 180 + term : CASE LPAREN ty_def COMMA term RPAREN branches . (49) - . reduce 48 + . reduce 49 -state 176 - term : LAMBDA LPAREN LIDENT COLON ty_def TILDE ty_def . ARROW term (49) +state 181 + term : LAMBDA LPAREN LIDENT COLON ty_def TILDE ty_def . ARROW term (50) - ARROW shift 182 + ARROW shift 187 . error -state 177 - ty_def : LPAREN ty_def TILDE kind ty_def RPAREN FARROW . ty_def (37) +state 182 + ty_def : LPAREN ty_def TILDE kind ty_def RPAREN FARROW . ty_def (38) FORALL shift 31 LIDENT shift 32 @@ -1670,38 +1717,38 @@ state 177 LPAREN shift 34 . error - ty_def goto 183 + ty_def goto 188 -state 178 - proof : FORALL LPAREN LIDENT COLON kind_and_role RPAREN proof . (62) +state 183 + proof : FORALL LPAREN LIDENT COLON kind_and_role RPAREN proof . (63) - . reduce 62 + . reduce 63 -state 179 +state 184 ty_dec : TYPE INSTANCE ty_kr_list UIDENT type_list EQ ty_def SEMI . (17) . reduce 17 -state 180 - ty_kr_list_aux : ty_kr_list_aux LPAREN LIDENT COLON kind_and_role RPAREN . (21) +state 185 + ty_kr_list_aux : ty_kr_list_aux LPAREN LIDENT COLON kind_and_role RPAREN . (22) - . reduce 21 + . reduce 22 -state 181 - branches : LBRACKET bs . RBRACKET (53) - bs : bs . UIDENT FARROW term SEMI (55) +state 186 + branches : LBRACKET bs . RBRACKET (54) + bs : bs . UIDENT FARROW term SEMI (56) - UIDENT shift 184 - RBRACKET shift 185 + UIDENT shift 189 + RBRACKET shift 190 . error -state 182 - term : LAMBDA LPAREN LIDENT COLON ty_def TILDE ty_def ARROW . term (49) +state 187 + term : LAMBDA LPAREN LIDENT COLON ty_def TILDE ty_def ARROW . term (50) CASE shift 11 LIDENT shift 14 @@ -1710,36 +1757,36 @@ state 182 LAMBDA shift 18 . error - term goto 186 + term goto 191 -state 183 - ty_def : LPAREN ty_def TILDE kind ty_def RPAREN FARROW ty_def . (37) +state 188 + ty_def : LPAREN ty_def TILDE kind ty_def RPAREN FARROW ty_def . (38) - . reduce 37 + . reduce 38 -state 184 - bs : bs UIDENT . FARROW term SEMI (55) +state 189 + bs : bs UIDENT . FARROW term SEMI (56) - FARROW shift 187 + FARROW shift 192 . error -state 185 - branches : LBRACKET bs RBRACKET . (53) +state 190 + branches : LBRACKET bs RBRACKET . (54) - . reduce 53 + . reduce 54 -state 186 - term : LAMBDA LPAREN LIDENT COLON ty_def TILDE ty_def ARROW term . (49) +state 191 + term : LAMBDA LPAREN LIDENT COLON ty_def TILDE ty_def ARROW term . (50) - . reduce 49 + . reduce 50 -state 187 - bs : bs UIDENT FARROW . term SEMI (55) +state 192 + bs : bs UIDENT FARROW . term SEMI (56) CASE shift 11 LIDENT shift 14 @@ -1748,27 +1795,30 @@ state 187 LAMBDA shift 18 . error - term goto 188 + term goto 193 -state 188 - bs : bs UIDENT FARROW term . SEMI (55) +state 193 + bs : bs UIDENT FARROW term . SEMI (56) - SEMI shift 189 + SEMI shift 194 . error -state 189 - bs : bs UIDENT FARROW term SEMI . (55) +state 194 + bs : bs UIDENT FARROW term SEMI . (56) - . reduce 55 + . reduce 56 Rules never reduced: - tylist : tylist_aux (25) - tylist_aux : (26) - tylist_aux : tylist LIDENT (27) + tylist : tylist_aux (26) + tylist_aux : (27) + tylist_aux : tylist LIDENT (28) + + +State 46 contains 1 shift/reduce conflict. 45 terminals, 23 nonterminals -72 grammar rules, 190 states +73 grammar rules, 195 states diff --git a/script.sh b/script.sh index 88fec80..1ee3f91 100755 --- a/script.sh +++ b/script.sh @@ -1 +1 @@ -make all && ocaml -I _build _build/prj.cma -init driver.ml \ No newline at end of file +make clean && make all && ocaml -I _build _build/prj.cma -init driver.ml \ No newline at end of file diff --git a/test/1.ml b/test/1.ml index 47034fc..cce5d30 100644 --- a/test/1.ml +++ b/test/1.ml @@ -47,11 +47,15 @@ TYPE INSTANCE F Nat = Bool ; -TYPE INSTANCE (a:*/C) F (Maybe a) = (Tuple a) +TYPE INSTANCE { (a:*/C) } F (Maybe a) = (Tuple a) ; -\ x: (List Nat) -> CASE (Bool,x) { +NEWTYPE Age = MkAge Nat ; + +LET a = \ x: (List Nat) -> CASE (Bool,x) { Nil => True ; Cons => \ y:Nat -> ( \ xs : (List Nat) -> False ); } ; + +