rebuilt against ocaml 3.08.3

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

diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml
index 1bc76ebb841176b185fde2c0052e2168b7130d0a..b60abf25886ea34a60658fba9f21d7926a180e5d 100644 (file)
--- a/helm/ocaml/cic_transformations/acic2Ast.ml
+++ b/helm/ocaml/cic_transformations/acic2Ast.ml
@@ -25,6 +25,8 @@
 
 open Printf
 
+module Ast = CicAst
+
 let symbol_table = Hashtbl.create 1024
 
 let sort_of_string = function
@@ -32,14 +34,14 @@ let sort_of_string = function
   | "Set" -> `Set
   | "Type" -> `Type
   | "CProp" -> `CProp
+  | "?" -> `Meta
   | _ -> assert false
 
 let get_types uri =
-  match CicEnvironment.get_obj uri with
-  | Cic.Constant _ -> assert false
-  | Cic.Variable _ -> assert false
-  | Cic.CurrentProof _ -> assert false
-  | Cic.InductiveDefinition (l,_,_) -> l 
+  let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+    match o with
+      | Cic.InductiveDefinition (l,_,_,_) -> l 
+      | _ -> assert false
 
 let name_of_inductive_type uri i = 
   let types = get_types uri in
@@ -60,16 +62,17 @@ let constructor_of_inductive_type uri i j =
     fst (List.nth (constructors_of_inductive_type uri i) (j-1))
   with Not_found -> assert false)
 
-let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
+let ast_of_acic ids_to_inner_sorts acic =
+  let ids_to_uris = Hashtbl.create 503 in
   let register_uri id uri = Hashtbl.add ids_to_uris id uri in
   let sort_of_id id =
     try
       sort_of_string (Hashtbl.find ids_to_inner_sorts id)
     with Not_found -> assert false
   in
-  let module Ast = CicAst in
   let idref id t = Ast.AttributedTerm (`IdRef id, t) in
-  let rec aux = function
+  let rec aux =
+    function
     | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, None))
     | Cic.AVar (id,uri,subst) ->
         register_uri id (UriManager.string_of_uri uri);
@@ -84,11 +87,12 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
     | Cic.AProd (id,n,s,t) ->
         let binder_kind =
           match sort_of_id id with
-          | `Set | `Type -> `Pi
+          | `Set | `Type | `Meta -> `Pi
           | `Prop | `CProp -> `Forall
         in
         idref id (Ast.Binder (binder_kind, (n, Some (aux s)), aux t))
-    | Cic.ACast (id,v,t) -> idref id (aux v)
+    | Cic.ACast (id,v,t) ->
+        idref id (Ast.Appl [idref id (Ast.Symbol ("cast", 0)); aux v; aux t])
     | Cic.ALambda (id,n,s,t) ->
         idref id (Ast.Binder (`Lambda, (n, Some (aux s)), aux t))
     | Cic.ALetIn (id,n,s,t) -> idref id (Ast.LetIn ((n, None), aux s, aux t))
@@ -213,3 +217,78 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
   in
   aux acic, ids_to_uris
 
+let _ = (** fill symbol_table *)
+  let add_symbol name uri =
+    Hashtbl.add symbol_table uri
+      (fun aid sid args acic2ast ->
+        Ast.AttributedTerm (`IdRef aid,
+          Ast.Appl (Ast.AttributedTerm (`IdRef sid, Ast.Symbol (name, 0)) ::
+            List.map acic2ast args)))
+  in
+    (* eq *)
+  Hashtbl.add symbol_table HelmLibraryObjects.Logic.eq_XURI
+    (fun aid sid args acic2ast ->
+      Ast.AttributedTerm (`IdRef aid,
+        Ast.Appl (
+          Ast.AttributedTerm (`IdRef sid, Ast.Symbol ("eq", 0)) ::
+          List.map acic2ast (List.tl args))));
+    (* exists *)
+  Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI 
+    (fun aid sid args acic2ast ->
+     match (List.tl args) with
+       [Cic.ALambda (_,Cic.Name n,s,t)] ->
+         Ast.AttributedTerm (`IdRef aid,
+          Ast.Binder (`Exists, (Cic.Name n, Some (acic2ast s)), acic2ast t))
+    | _ -> raise Not_found);
+  add_symbol "and" HelmLibraryObjects.Logic.and_XURI;
+  add_symbol "or" HelmLibraryObjects.Logic.or_XURI;
+  add_symbol "iff" HelmLibraryObjects.Logic.iff_SURI;
+  add_symbol "not" HelmLibraryObjects.Logic.not_SURI;
+  add_symbol "inv" HelmLibraryObjects.Reals.rinv_SURI;
+  add_symbol "opp" HelmLibraryObjects.Reals.ropp_SURI;
+  add_symbol "leq" HelmLibraryObjects.Peano.le_XURI;
+  add_symbol "leq" HelmLibraryObjects.Reals.rle_SURI;
+  add_symbol "lt" HelmLibraryObjects.Peano.lt_SURI;
+  add_symbol "lt" HelmLibraryObjects.Reals.rlt_SURI;
+  add_symbol "geq" HelmLibraryObjects.Peano.ge_SURI;
+  add_symbol "geq" HelmLibraryObjects.Reals.rge_SURI;
+  add_symbol "gt" HelmLibraryObjects.Peano.gt_SURI;
+  add_symbol "gt" HelmLibraryObjects.Reals.rgt_SURI;
+  add_symbol "plus" HelmLibraryObjects.Peano.plus_SURI;
+  add_symbol "plus" HelmLibraryObjects.BinInt.zplus_SURI;
+  add_symbol "times" HelmLibraryObjects.Peano.mult_SURI;
+  add_symbol "times" HelmLibraryObjects.Reals.rmult_SURI;
+  add_symbol "minus" HelmLibraryObjects.Peano.minus_SURI;
+  add_symbol "minus" HelmLibraryObjects.Reals.rminus_SURI;
+  add_symbol "div" HelmLibraryObjects.Reals.rdiv_SURI;
+  Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI
+  (fun aid sid args acic2ast ->
+    Ast.AttributedTerm (`IdRef sid, Ast.Num ("0", 0)));
+  Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
+  (fun aid sid args acic2ast ->
+    Ast.AttributedTerm (`IdRef sid, Ast.Num ("1", 0)));
+    (* plus *)
+  Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI
+    (fun aid sid args acic2ast ->
+     let appl () =
+       Ast.AttributedTerm (`IdRef aid,
+        Ast.Appl (
+          Ast.AttributedTerm (`IdRef sid, Ast.Symbol ("plus", 0)) ::
+          List.map acic2ast args))
+     in
+      let rec aux acc = function
+        | [ Cic.AConst (nid, uri, []); n] when
+            UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
+              (match n with
+              | Cic.AConst (_, uri, []) when
+                 UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
+                   Ast.AttributedTerm (`IdRef aid,
+                    Ast.Num (string_of_int (acc + 2), 0))
+              | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
+                  UriManager.eq uri HelmLibraryObjects.Reals.rplus_URI ->
+                    aux (acc + 1) args
+              | _ -> appl ())
+        | _ -> appl ()
+      in
+      aux 0 args)
+