- attributes support

- default instance is 0 (not -1 !)

diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml
index b815d33bd4eb3a9be37f6d1bc2e83c7762878ffe..1e4914e7f9bbbf250830d44654710119e3df65c0 100644 (file)
--- a/helm/ocaml/cic_transformations/acic2Ast.ml
+++ b/helm/ocaml/cic_transformations/acic2Ast.ml
@@ -39,10 +39,8 @@ let sort_of_string = function
 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
@@ -93,7 +91,7 @@ let ast_of_acic ids_to_inner_sorts acic =
         in
         idref id (Ast.Binder (binder_kind, (n, Some (aux s)), aux t))
     | Cic.ACast (id,v,t) ->
-        idref id (Ast.Appl [idref id (Ast.Symbol ("cast", -1)); aux v; aux 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))
@@ -223,7 +221,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 *)
@@ -231,7 +229,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 
@@ -264,17 +262,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
@@ -284,7 +282,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