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

diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml
index fc6d95531..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,17 +62,18 @@ 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
-    | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, []))
+  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);
         idref id
@@ -78,7 +81,7 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
     | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, astcontext_of_ciccontext l))
     | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
     | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
-    | Cic.ASort (id,Cic.Type) -> idref id (Ast.Sort `Type)
+    | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type) (* TASSI *)
     | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
     | Cic.AImplicit _ -> assert false
     | Cic.AProd (id,n,s,t) ->
@@ -166,7 +169,7 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
               ((name, capture_variables), rhs))
             constructors patterns
         in
-        idref id (Ast.Case (aux te, name, Some (aux ty), patterns))
+        idref id (Ast.Case (aux te, Some name, Some (aux ty), patterns))
     | Cic.AFix (id, no, funs) -> 
         let defs = 
           List.map
@@ -181,7 +184,7 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
             | _ -> assert false)
           with Not_found -> assert false
         in
-        idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, [])))
+        idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None)))
     | Cic.ACoFix (id, no, funs) -> 
         let defs = 
           List.map
@@ -195,11 +198,13 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
             | _ -> assert false)
           with Not_found -> assert false
         in
-        idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, [])))
+        idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, None)))
 
   and astsubst_of_cicsubst subst =
-    List.map (fun (uri, annterm) -> (UriManager.name_of_uri uri, aux annterm))
-      subst
+    Some
+      (List.map (fun (uri, annterm) ->
+        (UriManager.name_of_uri uri, aux annterm))
+        subst)
 
   and astcontext_of_ciccontext context =
     List.map
@@ -211,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)
+