moved here CicAst and pretty printer

[helm.git] / helm / ocaml / cic_transformations / contentTable.ml

diff --git a/helm/ocaml/cic_transformations/contentTable.ml b/helm/ocaml/cic_transformations/contentTable.ml
new file mode 100644 (file)
index 0000000..7950ce2
--- /dev/null
+++ b/helm/ocaml/cic_transformations/contentTable.ml
@@ -0,0 +1,122 @@
+
+(* NOTATION *)
+
+let symbol_table = Hashtbl.create 503 ;;
+let lookup_symbol = Hashtbl.find symbol_table ;;
+
+let idref id t = CicAst.AttributedTerm (`IdRef id, t) ;;
+
+let add_symbol uri mnemonic =
+  Hashtbl.add symbol_table uri
+    (fun aid sid args ast_of_acic ->
+      idref aid (CicAst.Appl
+        (idref sid (CicAst.Symbol (mnemonic, 0)) :: List.map ast_of_acic args)))
+;;
+
+(* eq *)
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)" 
+  (fun aid sid args ast_of_acic ->
+    idref aid (CicAst.Appl
+      (idref sid (CicAst.Symbol ("eq", 0)) ::
+        List.map ast_of_acic (List.tl args)))) ;;
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#xpointer(1/1)" 
+  (fun aid sid args ast_of_acic ->
+    idref aid (CicAst.Appl
+      (idref sid (CicAst.Symbol ("eq", 0)) ::
+        List.map ast_of_acic (List.tl args)))) ;;
+
+(* and *)
+add_symbol "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)" "and" ;;
+
+(* or *)
+add_symbol "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)" "or" ;;
+
+(* iff *)
+add_symbol "cic:/Coq/Init/Logic/iff.con" "iff" ;;
+
+(* not *)
+add_symbol "cic:/Coq/Init/Logic/not.con" "not" ;;
+
+(* Rinv *)
+add_symbol "cic:/Coq/Reals/Rdefinitions/Rinv.con" "inv" ;;
+
+(* Ropp *)
+add_symbol "cic:/Coq/Reals/Rdefinitions/Ropp.con" "opp" ;;
+
+(* exists *)
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)" 
+  (fun aid sid args ast_of_acic ->
+   match (List.tl args) with
+     [Cic.ALambda (_,n,s,t)] ->
+       idref aid
+        (CicAst.Binder (`Exists, (n, Some (ast_of_acic s)), ast_of_acic t))
+  | _ -> raise Not_found);;
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)" 
+  (fun aid sid args ast_of_acic ->
+   match (List.tl args) with
+     [Cic.ALambda (_,n,s,t)] ->
+       idref aid
+        (CicAst.Binder (`Exists, (n, Some (ast_of_acic s)), ast_of_acic t))
+  | _ -> raise Not_found);;
+
+(* leq *) 
+add_symbol "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)" "leq" ;;
+add_symbol "cic:/Coq/Reals/Rdefinitions/Rle.con" "leq" ;;
+
+(* lt *)
+add_symbol "cic:/Coq/Init/Peano/lt.con" "lt" ;;
+add_symbol "cic:/Coq/Reals/Rdefinitions/Rlt.con" "lt" ;;
+
+(* geq *)
+add_symbol "cic:/Coq/Init/Peano/ge.con" "geq" ;;
+add_symbol "cic:/Coq/Reals/Rdefinitions/Rge.con" "geq" ;;
+
+(* gt *)
+add_symbol "cic:/Coq/Init/Peano/gt.con" "gt" ;;
+add_symbol "cic:/Coq/Reals/Rdefinitions/Rgt.con" "gt" ;;
+
+(* plus *)
+add_symbol "cic:/Coq/Init/Peano/plus.con" "plus" ;;
+add_symbol "cic:/Coq/ZArith/fast_integer/Zplus.con" "plus" ;;
+
+let rplus_uri =
+  UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con" ;;
+let r1_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" ;;
+
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con" 
+  (fun aid sid args ast_of_acic ->
+    let appl () =
+      idref aid (CicAst.Appl 
+        (idref sid (CicAst.Symbol ("plus", 0)) :: List.map ast_of_acic args))
+   in
+    let rec aux acc = function
+      | [ Cic.AConst (nid, uri, []); n] when UriManager.eq uri r1_uri ->
+            (match n with
+            | Cic.AConst (_, uri, []) when UriManager.eq uri r1_uri ->
+                idref aid (CicAst.Num (string_of_int (acc+2), 0))
+            | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args)
+              when UriManager.eq uri rplus_uri ->
+                aux (acc + 1) args
+            | _ -> appl ())
+      | _ -> appl ()
+    in
+    aux 0 args)
+;;
+
+(* zero and one *)
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R0.con" 
+  (fun _ sid _ _ -> idref sid (CicAst.Num ("0", 0))) ;;
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R1.con" 
+  (fun _ sid _ _ -> idref sid (CicAst.Num ("1", 0))) ;;
+
+(* times *) 
+add_symbol "cic:/Coq/Init/Peano/mult.con" "times" ;;
+add_symbol "cic:/Coq/Reals/Rdefinitions/Rmult.con" "times" ;;
+
+(* minus *)
+add_symbol "cic:/Coq/Arith/Minus/minus.con" "minus" ;;
+add_symbol "cic:/Coq/Reals/Rdefinitions/Rminus.con" "minus" ;;
+
+(* div *)
+add_symbol "cic:/Coq/Reals/Rdefinitions/Rdiv.con" "div" ;;
+