X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Facic2Ast.ml;h=567b7f7bb6b38746d1f220251e0362d6d97691e4;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=1bc76ebb841176b185fde2c0052e2168b7130d0a;hpb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;p=helm.git

diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml
index 1bc76ebb8..567b7f7bb 100644
--- 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
@@ -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);
@@ -213,3 +216,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, -1)) ::
+            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", -1)) ::
+          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", -1)));
+  Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
+  (fun aid sid args acic2ast ->
+    Ast.AttributedTerm (`IdRef sid, Ast.Num ("1", -1)));
+    (* 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", -1)) ::
+          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), -1))
+              | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
+                  UriManager.eq uri HelmLibraryObjects.Reals.rplus_URI ->
+                    aux (acc + 1) args
+              | _ -> appl ())
+        | _ -> appl ()
+      in
+      aux 0 args)
+