- added attributes support

[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 24d2e07f3dc35db110bfd7dd6a2298a2d3a08ac9..b815d33bd4eb3a9be37f6d1bc2e83c7762878ffe 100644 (file)
--- a/helm/ocaml/cic_transformations/acic2Ast.ml
+++ b/helm/ocaml/cic_transformations/acic2Ast.ml
@@ -37,11 +37,12 @@ let sort_of_string = function
   | _ -> 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.Constant _ -> assert false
+      | Cic.Variable _ -> assert false
+      | Cic.CurrentProof _ -> assert false
+      | Cic.InductiveDefinition (l,_,_) -> l 
 
 let name_of_inductive_type uri i = 
   let types = get_types uri in
@@ -72,7 +73,6 @@ let ast_of_acic ids_to_inner_sorts acic =
   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) ->
@@ -92,7 +92,8 @@ prerr_endline "Acic2ast.aux";
           | `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", -1)); 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,9 +216,7 @@ 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 =