Add parser export, let binding

Makefile

@@ -22,4 +22,6 @@ parse :
 prj:
 	ocamlbuild prj.cma
 
-all:  parse prj
+all:  parse prj
+clean: 
+	ocamlbuild -clean

_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"

_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.

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;;

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

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 =