X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Facic2Ast.ml;h=70036146e8240d697ab212f1f80e25c0444244cf;hb=ec54d490477ece51c19d79750dda9805ffda663c;hp=24d2e07f3dc35db110bfd7dd6a2298a2d3a08ac9;hpb=29969baf115afff7eb9ea9e2ca98d40ab7006dcc;p=helm.git

diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml
index 24d2e07f3..70036146e 100644
--- a/helm/ocaml/cic_transformations/acic2Ast.ml
+++ b/helm/ocaml/cic_transformations/acic2Ast.ml
@@ -29,19 +29,11 @@ module Ast = CicAst
 
 let symbol_table = Hashtbl.create 1024
 
-let sort_of_string = function
-  | "Prop" -> `Prop
-  | "Set" -> `Set
-  | "Type" -> `Type
-  | "CProp" -> `CProp
-  | _ -> 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
@@ -67,12 +59,11 @@ let ast_of_acic ids_to_inner_sorts acic =
   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)
+      Hashtbl.find ids_to_inner_sorts id
     with Not_found -> assert false
   in
   let idref id t = Ast.AttributedTerm (`IdRef id, t) in
   let rec aux =
-prerr_endline "Acic2ast.aux";
     function
     | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, None))
     | Cic.AVar (id,uri,subst) ->
@@ -88,11 +79,12 @@ prerr_endline "Acic2ast.aux";
     | 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))
@@ -215,16 +207,14 @@ prerr_endline "Acic2ast.aux";
       context
 
   in
-  let res = aux acic, ids_to_uris in
-prerr_endline "/Acic2ast.aux";
-  res
+  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)) ::
+          Ast.Appl (Ast.AttributedTerm (`IdRef sid, Ast.Symbol (name, 0)) ::
             List.map acic2ast args)))
   in
     (* eq *)
@@ -232,7 +222,7 @@ let _ = (** fill symbol_table *)
     (fun aid sid args acic2ast ->
       Ast.AttributedTerm (`IdRef aid,
         Ast.Appl (
-          Ast.AttributedTerm (`IdRef sid, Ast.Symbol ("eq", -1)) ::
+          Ast.AttributedTerm (`IdRef sid, Ast.Symbol ("eq", 0)) ::
           List.map acic2ast (List.tl args))));
     (* exists *)
   Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI 
@@ -265,17 +255,17 @@ let _ = (** fill symbol_table *)
   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)));
+    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", -1)));
+    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", -1)) ::
+          Ast.AttributedTerm (`IdRef sid, Ast.Symbol ("plus", 0)) ::
           List.map acic2ast args))
      in
       let rec aux acc = function
@@ -285,7 +275,7 @@ let _ = (** fill symbol_table *)
               | Cic.AConst (_, uri, []) when
                  UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
                    Ast.AttributedTerm (`IdRef aid,
-                    Ast.Num (string_of_int (acc + 2), -1))
+                    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