Merge.

Makefile

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

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 = 

fc_p.mly

@@ -12,6 +12,7 @@
 %token DATA WHERE
 %token NTH SYM NEWTYPE
 %token TYPE FAMILY INSTANCE
+%token LET 
 
 %token <string>LIDENT 
 %token <string>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
+        }
 
 ;