added attributes

diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
index 23c3a9b68446a3812f8682a7c2a0e96c78051ac4..4c028208f05043a12d43b12081b3b02efb9b453f 100644 (file)
--- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
+++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
@@ -109,7 +109,7 @@ let pp_annotation obj i2a curi =
       [None, "of", UriManager.string_of_uri (UriManager.cicuri_of_uri curi)]
       begin
        match obj with
-         C.AConstant (xid, xidobj, _, te, ty, _) ->
+         C.AConstant (xid, xidobj, _, te, ty, _, _) ->
           [< print_ann i2a xid ;
              (match xidobj,te with
                  Some xidobj, Some te ->
@@ -121,7 +121,7 @@ let pp_annotation obj i2a curi =
              ) ;
              print_term i2a ty
           >]
-       | C.AVariable (xid, _, bo, ty,_) ->
+       | C.AVariable (xid, _, bo, ty,_, _) ->
           [< print_ann i2a xid ;
              (match bo with
                  None -> [<>]
@@ -129,7 +129,7 @@ let pp_annotation obj i2a curi =
              ) ;
              print_term i2a ty
           >]
-       | C.ACurrentProof (xid, xidobj, _, conjs, bo, ty,_) ->
+       | C.ACurrentProof (xid, xidobj, _, conjs, bo, ty,_, _) ->
           [< print_ann i2a xid ;
              print_ann i2a xidobj ;
              List.fold_right
@@ -151,7 +151,7 @@ let pp_annotation obj i2a curi =
              print_term i2a bo ;
              print_term i2a ty
           >]
-       | C.AInductiveDefinition (xid, tys, params, paramsno) ->
+       | C.AInductiveDefinition (xid, tys, params, paramsno, _) ->
           [< print_ann i2a xid ;
              List.fold_right
               (fun x i -> [< print_mutual_inductive_type i2a x ; i >])

diff --git a/helm/ocaml/cic_annotations/cicXPath.ml b/helm/ocaml/cic_annotations/cicXPath.ml
index 75a598d91990728b4361452e750bc7669778cd6c..b9533d18f8a46ef77afca96a4196962c7ba8c672 100644 (file)
--- a/helm/ocaml/cic_annotations/cicXPath.ml
+++ b/helm/ocaml/cic_annotations/cicXPath.ml
@@ -100,7 +100,7 @@ let get_ids_to_targets annobj =
     in
      let add_target_obj annobj =
       match annobj with
-        C.AConstant (id,idbody,_,bo,ty,_) ->
+        C.AConstant (id,idbody,_,bo,ty,_,_) ->
          set_target id (C.Object annobj) ;
          (match idbody,bo with
              Some idbody,Some bo ->
@@ -110,14 +110,14 @@ let get_ids_to_targets annobj =
            | _,_ -> assert false
          ) ;
          add_target_term ty
-      | C.AVariable (id,_,None,ty,_) ->
+      | C.AVariable (id,_,None,ty,_,_) ->
          set_target id (C.Object annobj) ;
          add_target_term ty
-      | C.AVariable (id,_,Some bo,ty,_) ->
+      | C.AVariable (id,_,Some bo,ty,_,_) ->
          set_target id (C.Object annobj) ;
          add_target_term bo ;
          add_target_term ty
-      | C.ACurrentProof (id,idbody,_,cl,bo,ty,_) ->
+      | C.ACurrentProof (id,idbody,_,cl,bo,ty,_,_) ->
          set_target id (C.Object annobj) ;
          set_target idbody (C.ConstantBody annobj) ;
          List.iter (function (cid,_,context, t) as annconj ->
@@ -133,7 +133,7 @@ let get_ids_to_targets annobj =
           add_target_term t) cl ;
          add_target_term bo ;
          add_target_term ty
-      | C.AInductiveDefinition (id,itl,_,_) ->
+      | C.AInductiveDefinition (id,itl,_,_,_) ->
          set_target id (C.Object annobj) ;
          List.iter
           (function (_,_,_,arity,cl) ->

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index 5b95ab4d687290315d17dbfcd45a653776c80486..cf9760c2565dd4ae86c6ae445a1c62ee0ae88c6f 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -428,19 +428,19 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
    in
    let aobj =
     match obj with
-      C.Constant (id,Some bo,ty,params) ->
+      C.Constant (id,Some bo,ty,params,attrs) ->
        let bo' = eta_fix [] [] bo in
        let ty' = eta_fix [] [] ty in
        let abo = acic_term_of_cic_term' bo' (Some ty') in
        let aty = acic_term_of_cic_term' ty' None in
         C.AConstant
-         ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params)
-    | C.Constant (id,None,ty,params) ->
+         ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
+    | C.Constant (id,None,ty,params,attrs) ->
        let ty' = eta_fix [] [] ty in
        let aty = acic_term_of_cic_term' ty' None in
         C.AConstant
-         ("mettereaposto",None,id,None,aty,params)
-    | C.Variable (id,bo,ty,params) ->
+         ("mettereaposto",None,id,None,aty,params,attrs)
+    | C.Variable (id,bo,ty,params,attrs) ->
        let ty' = eta_fix [] [] ty in
        let abo =
         match bo with
@@ -451,8 +451,8 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
        in
        let aty = acic_term_of_cic_term' ty' None in
         C.AVariable
-         ("mettereaposto",id,abo,aty, params)
-    | C.CurrentProof (id,conjectures,bo,ty,params) ->
+         ("mettereaposto",id,abo,aty,params,attrs)
+    | C.CurrentProof (id,conjectures,bo,ty,params,attrs) ->
        let conjectures' =
         List.map
          (function (i,canonical_context,term) ->
@@ -556,8 +556,8 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
         ("++++++++++ Numero di iterazioni della acic_of_cic: " ^ string_of_int !seed) ;
 *)
         C.ACurrentProof
-         ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params)
-    | C.InductiveDefinition (tys,params,paramsno) ->
+         ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params,attrs)
+    | C.InductiveDefinition (tys,params,paramsno,attrs) ->
        let context =
         List.map
          (fun (name,_,arity,_) -> Some (C.Name name, C.Decl arity)) tys in
@@ -575,7 +575,7 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
             (id,name,inductive,acic_term_of_cic_term' ty None,acons)
          ) (List.rev idrefs) tys
        in
-        C.AInductiveDefinition ("mettereaposto",atys,params,paramsno)
+        C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)
    in
     aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
      ids_to_conjectures,ids_to_hypotheses

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index ef6999ca0887e65f5ad4036ca7320763d6693cda..aaf4512565e3ee30b479dc6b30c62efbb5021407 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -374,10 +374,8 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                         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
                       ) in
                     let (_,_,_,constructors) = 
                       List.nth inductive_types tyno in 
@@ -548,7 +546,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
                 Cic.Constant _ -> assert false
                | Cic.Variable _ -> assert false
                | Cic.CurrentProof _ -> assert false
-               | Cic.InductiveDefinition (l,_,n) -> l,n 
+               | Cic.InductiveDefinition (l,_,n,_) -> l,n 
           ) in
         let (_,_,_,constructors) = List.nth inductive_types typeno in
         let name_and_arities = 
@@ -694,10 +692,8 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
         let inductive_types,noparams =
           (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in
             match o with
-                Cic.Constant _ -> assert false
-               | Cic.Variable _ -> assert false
-               | Cic.CurrentProof _ -> assert false
-               | Cic.InductiveDefinition (l,_,n) -> (l,n) 
+               | Cic.InductiveDefinition (l,_,n,_) -> (l,n) 
+               | _ -> assert false
           ) in
         let rec split n l =
           if n = 0 then ([],l) else
@@ -916,7 +912,7 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
   let module C2A = Cic2acic in
   let seed = ref 0 in
   function
-      C.ACurrentProof (_,_,n,conjectures,bo,ty,params) ->
+      C.ACurrentProof (_,_,n,conjectures,bo,ty,params,_) ->
         (gen_id object_prefix seed, params,
           Some
            (List.map
@@ -925,27 +921,27 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
           `Def (K.Const,ty,
             build_def_item seed (get_id bo) (C.Name n) bo 
              ~ids_to_inner_sorts ~ids_to_inner_types))
-    | C.AConstant (_,_,n,Some bo,ty,params) ->
+    | C.AConstant (_,_,n,Some bo,ty,params,_) ->
          (gen_id object_prefix seed, params, None,
            `Def (K.Const,ty,
              build_def_item seed (get_id bo) (C.Name n) bo 
                ~ids_to_inner_sorts ~ids_to_inner_types))
-    | C.AConstant (id,_,n,None,ty,params) ->
+    | C.AConstant (id,_,n,None,ty,params,_) ->
          (gen_id object_prefix seed, params, None,
            `Decl (K.Const,
              build_decl_item seed id (C.Name n) ty 
                ~ids_to_inner_sorts))
-    | C.AVariable (_,n,Some bo,ty,params) ->
+    | C.AVariable (_,n,Some bo,ty,params,_) ->
          (gen_id object_prefix seed, params, None,
            `Def (K.Var,ty,
              build_def_item seed (get_id bo) (C.Name n) bo
                ~ids_to_inner_sorts ~ids_to_inner_types))
-    | C.AVariable (id,n,None,ty,params) ->
+    | C.AVariable (id,n,None,ty,params,_) ->
          (gen_id object_prefix seed, params, None,
            `Decl (K.Var,
              build_decl_item seed id (C.Name n) ty
               ~ids_to_inner_sorts))
-    | C.AInductiveDefinition (id,l,params,nparams) ->
+    | C.AInductiveDefinition (id,l,params,nparams,_) ->
          (gen_id object_prefix seed, params, None,
             `Joint
               { K.joint_id = gen_id joint_prefix seed;

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index bf80a5939b47153dd938a84f4a4e2ca96ef65127..fdc2cea1cee300573c739dfe597ea46896c52242 100644 (file)
--- a/helm/ocaml/cic_omdoc/content2cic.ml
+++ b/helm/ocaml/cic_omdoc/content2cic.ml
@@ -227,7 +227,7 @@ let cobj2obj deannotate (id,params,metasenv,obj) =
       (match metasenv with
           None ->
            Cic.Constant
-            (id, Some (proof2cic deannotate bo), deannotate ty, params)
+            (id, Some (proof2cic deannotate bo), deannotate ty, params, [])
         | Some metasenv' ->
            let metasenv'' =
             List.map
@@ -259,7 +259,8 @@ let cobj2obj deannotate (id,params,metasenv,obj) =
              ) metasenv'
            in
             Cic.CurrentProof
-             (id, metasenv'', proof2cic deannotate bo, deannotate ty, params))
+             (id, metasenv'', proof2cic deannotate bo, deannotate ty, params,
+              []))
   | _ -> raise ToDo
 ;;
 

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
index e16aa789f2412c07af939f663478d5ac0af817e9..128da869b72a142b8cb914c80f68a02a221952ff 100644 (file)
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
@@ -272,8 +272,8 @@ let type_of_constant uri =
        raise (NotWellTyped "Reference to an unchecked constant")
   in
    match cobj with
-      C.Constant (_,_,ty,_) -> ty
-    | C.CurrentProof (_,_,_,ty,_) -> ty
+      C.Constant (_,_,ty,_,_) -> ty
+    | C.CurrentProof (_,_,_,ty,_,_) -> ty
     | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
 ;;
 
@@ -282,7 +282,7 @@ let type_of_variable uri =
  let module R = CicReduction in
  let module U = UriManager in
   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
-     CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),_) -> ty
+     CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),_) -> ty
    | CicEnvironment.UncheckedObj (C.Variable _) ->
       raise (NotWellTyped "Reference to an unchecked variable")
    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
@@ -299,7 +299,7 @@ let type_of_mutual_inductive_defs uri i =
        raise (NotWellTyped "Reference to an unchecked inductive type")
   in
    match cobj with
-      C.InductiveDefinition (dl,_,_) ->
+      C.InductiveDefinition (dl,_,_,_) ->
        let (_,_,arity,_) = List.nth dl i in
         arity
     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
@@ -316,7 +316,7 @@ let type_of_mutual_inductive_constr uri i j =
        raise (NotWellTyped "Reference to an unchecked constructor")
   in
    match cobj with
-      C.InductiveDefinition (dl,_,_) ->
+      C.InductiveDefinition (dl,_,_,_) ->
        let (_,_,_,cl) = List.nth dl i in
         let (_,ty) = List.nth cl (j-1) in
          ty
@@ -543,7 +543,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
              with Not_found -> assert false
            in
           match obj with
-             C.InductiveDefinition (tl,_,parsno) ->
+             C.InductiveDefinition (tl,_,parsno,_) ->
               let (_,_,_,cl) = List.nth tl i in (cl,parsno)
            | _ ->
              raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
@@ -645,22 +645,18 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
        with Not_found -> assert false
      in
-    match obj with
-      Cic.Constant (_,_,_,params)
-    | Cic.CurrentProof (_,_,_,_,params)
-    | Cic.Variable (_,_,_,params)
-    | Cic.InductiveDefinition (_,params,_) ->
-       List.map
-        (function uri ->
-           let obj,_ =
-             try
-               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
-             with Not_found -> assert false
-           in
-           match obj with
-             Cic.Variable (_,None,ty,_) -> uri,ty
-           | _ -> assert false (* the theorem is well-typed *)
-        ) params
+    let params = CicUtil.params_of_obj obj in
+     List.map
+      (function uri ->
+         let obj,_ =
+           try
+             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+           with Not_found -> assert false
+         in
+         match obj with
+           Cic.Variable (_,None,ty,_,_) -> uri,ty
+         | _ -> assert false (* the theorem is well-typed *)
+      ) params
   in
    let rec check uris_and_types subst =
     match uris_and_types,subst with

diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
index 41cc72738c7562e638cc146d0596bdad6eac061c..68dec37d6b04230f1468665e0a6f77516ccdb365 100644 (file)
--- a/helm/ocaml/cic_omdoc/eta_fixing.ml
+++ b/helm/ocaml/cic_omdoc/eta_fixing.ml
@@ -242,7 +242,7 @@ let eta_fix metasenv context t =
                Cic.Constant _ -> assert false
              | Cic.Variable _ -> assert false
              | Cic.CurrentProof _ -> assert false
-             | Cic.InductiveDefinition (l,_,n) -> l,n 
+             | Cic.InductiveDefinition (l,_,n,_) -> l,n 
            ) in
        let (_,_,_,constructors) = List.nth inductive_types tyno in
        let constructor_types = 
@@ -299,7 +299,7 @@ let eta_fix metasenv context t =
         let ty =
          let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
-               Cic.Variable (_,_,ty,_) -> 
+               Cic.Variable (_,_,ty,_,_) -> 
                  CicSubstitution.subst_vars newsubst ty
               | _ ->  raise ReferenceToNonVariable 
        in