version 0.7.1

[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 752dd321642243763245dddaba808c47385fd4b7..70036146e8240d697ab212f1f80e25c0444244cf 100644 (file)
--- a/helm/ocaml/cic_transformations/acic2Ast.ml
+++ b/helm/ocaml/cic_transformations/acic2Ast.ml
@@ -29,20 +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 =
   let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
     match o with
-      | Cic.Constant _ -> assert false
-      | Cic.Variable _ -> assert false
-      | Cic.CurrentProof _ -> assert false
-      | Cic.InductiveDefinition (l,_,_) -> l 
+      | Cic.InductiveDefinition (l,_,_,_) -> l 
+      | _ -> assert false
 
 let name_of_inductive_type uri i = 
   let types = get_types uri in
@@ -68,7 +59,7 @@ 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
@@ -88,11 +79,12 @@ let ast_of_acic ids_to_inner_sorts 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))
@@ -222,7 +214,7 @@ let _ = (** fill symbol_table *)
     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 *)
@@ -230,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 
@@ -263,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
@@ -283,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