This commit was manufactured by cvs2svn to create branch 'moogle'.

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

diff --git a/helm/ocaml/cic_transformations/contentTable.ml b/helm/ocaml/cic_transformations/contentTable.ml
deleted file mode 100644 (file)
index c41a838..0000000
--- a/helm/ocaml/cic_transformations/contentTable.ml
+++ /dev/null
@@ -1,109 +0,0 @@
-
-(* 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 HelmLibraryObjects.Logic.eq_XURI
-  (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 HelmLibraryObjects.Logic.and_XURI "and" ;;
-
-(* or *)
-add_symbol HelmLibraryObjects.Logic.or_XURI "or" ;;
-
-(* iff *)
-add_symbol HelmLibraryObjects.Logic.iff_SURI "iff" ;;
-
-(* not *)
-add_symbol HelmLibraryObjects.Logic.not_SURI "not" ;;
-
-(* Rinv *)
-add_symbol HelmLibraryObjects.Reals.rinv_SURI "inv" ;;
-
-(* Ropp *)
-add_symbol HelmLibraryObjects.Reals.ropp_SURI "opp" ;;
-
-(* exists *)
-Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI
-  (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 HelmLibraryObjects.Peano.le_XURI "leq" ;;
-add_symbol HelmLibraryObjects.Reals.rle_SURI "leq" ;;
-
-(* lt *)
-add_symbol HelmLibraryObjects.Peano.lt_SURI "lt" ;;
-add_symbol HelmLibraryObjects.Reals.rlt_SURI "lt" ;;
-
-(* geq *)
-add_symbol HelmLibraryObjects.Peano.ge_SURI "geq" ;;
-add_symbol HelmLibraryObjects.Reals.rge_SURI "geq" ;;
-
-(* gt *)
-add_symbol HelmLibraryObjects.Peano.gt_SURI "gt" ;;
-add_symbol HelmLibraryObjects.Reals.rgt_SURI "gt" ;;
-
-(* plus *)
-add_symbol HelmLibraryObjects.Peano.plus_SURI "plus" ;;
-add_symbol HelmLibraryObjects.BinInt.zplus_SURI "plus" ;;
-
-let rplus_uri = HelmLibraryObjects.Reals.rplus_URI;;
-let r1_uri = HelmLibraryObjects.Reals.r1_URI;;
-
-Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI
-  (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 HelmLibraryObjects.Reals.r0_SURI
-  (fun _ sid _ _ -> idref sid (CicAst.Num ("0", 0))) ;;
-Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
-  (fun _ sid _ _ -> idref sid (CicAst.Num ("1", 0))) ;;
-
-(* times *) 
-add_symbol HelmLibraryObjects.Peano.mult_SURI "times" ;;
-add_symbol HelmLibraryObjects.Reals.rmult_SURI "times" ;;
-
-(* minus *)
-add_symbol HelmLibraryObjects.Peano.minus_SURI "minus" ;;
-add_symbol HelmLibraryObjects.Reals.rminus_SURI "minus" ;;
-
-(* div *)
-add_symbol HelmLibraryObjects.Reals.rdiv_SURI "div" ;;
-