Prefixes introduced for the generated ids/xrefs. Example:

 "proof:" for proofs
 "decl:"  for declarations
 ...

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 0295daac326659968bb6d8637ad9956583e90afa..335296effff7b374a7a4379f3d56a86828bcfff6 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -32,12 +32,22 @@
 (*                                                                        *)
 (**************************************************************************)
 
+let object_prefix = "obj:";;
+let declaration_prefix = "decl:";;
+let definition_prefix = "def:";;
+let inductive_prefix = "ind:";;
+let joint_prefix = "joint:";;
+let proof_prefix = "proof:";;
+let conclude_prefix = "concl:";;
+let premise_prefix = "prem:";;
+let lemma_prefix = "lemma:";;
+
 (* e se mettessi la conversione di BY nell'apply_context ? *)
 (* sarebbe carino avere l'invariante che la proof2pres
 generasse sempre prove con contesto vuoto *)
  
-let gen_id seed =
- let res = "p" ^ string_of_int !seed in
+let gen_id prefix seed =
+ let res = prefix ^ string_of_int !seed in
   incr seed ;
   res
 ;;
@@ -166,47 +176,6 @@ let test_for_lifting ~ids_to_inner_types ~ids_to_inner_sorts=
           with Not_found -> false)
 ;;
 
-(*
-let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts =
-  let module C = Cic in
-  let module K = Content in
-  let rec aux l subproofs =
-    match l with
-      [] -> []
-    | t::l1 -> 
-        if (test_for_lifting t ~ids_to_inner_types) then
-          (match subproofs with
-             [] -> assert false
-           | p::tl -> 
-              let new_arg = 
-                K.Premise
-                  { K.premise_id = gen_id seed;
-                    K.premise_xref = p.K.proof_id;
-                    K.premise_binder = p.K.proof_name;
-                    K.premise_n = None
-                  }
-                in new_arg::(aux l1 tl))
-        else 
-          let hd = 
-            (match t with 
-               C.ARel (idr,idref,n,b) ->
-                 let sort = 
-                   (try Hashtbl.find ids_to_inner_sorts idr 
-                    with Not_found -> "Type") in 
-                 if sort ="Prop" then 
-                    K.Premise 
-                      { K.premise_id = gen_id seed;
-                        K.premise_xref = idr;
-                        K.premise_binder = Some b;
-                        K.premise_n = Some n
-                      }
-                 else (K.Term t)
-             | _ -> (K.Term t)) in 
-          hd::(aux l1 subproofs)
-  in aux l subproofs
-;;
-*)
-
 (* transform a proof p into a proof list, concatenating the last 
 conclude element to the apply_context list, in case context is
 empty. Otherwise, it just returns [p] *)
@@ -244,11 +213,11 @@ let generate_conversion seed top_down id inner_proof ~ids_to_inner_types =
    | Some expty ->
        if inner_proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
          { K.proof_name = inner_proof.K.proof_name;
-            K.proof_id   = gen_id seed;
+            K.proof_id   = gen_id proof_prefix seed;
             K.proof_context = [] ;
             K.proof_apply_context = [];
             K.proof_conclude = 
-              { K.conclude_id = gen_id seed; 
+              { K.conclude_id = gen_id conclude_prefix seed; 
                 K.conclude_aref = id;
                 K.conclude_method = "TD_Conversion";
                 K.conclude_args = 
@@ -258,16 +227,16 @@ let generate_conversion seed top_down id inner_proof ~ids_to_inner_types =
           }
         else
           { K.proof_name =  inner_proof.K.proof_name;
-            K.proof_id   = gen_id seed;
+            K.proof_id   = gen_id proof_prefix seed;
             K.proof_context = [] ;
             K.proof_apply_context = [{inner_proof with K.proof_name = None}];
             K.proof_conclude = 
-              { K.conclude_id = gen_id seed; 
+              { K.conclude_id = gen_id conclude_prefix seed; 
                 K.conclude_aref = id;
                 K.conclude_method = "BU_Conversion";
                 K.conclude_args =  
                  [K.Premise 
-                  { K.premise_id = gen_id seed;
+                  { K.premise_id = gen_id premise_prefix seed;
                     K.premise_xref = inner_proof.K.proof_id; 
                     K.premise_binder = None;
                     K.premise_n = None
@@ -282,11 +251,11 @@ let generate_exact seed t id name ~ids_to_inner_types =
   let module C2A = Cic2acic in
   let module K = Content in
     { K.proof_name = name;
-      K.proof_id   = id ;
+      K.proof_id   = proof_prefix ^ id ;
       K.proof_context = [] ;
       K.proof_apply_context = [];
       K.proof_conclude = 
-        { K.conclude_id = gen_id seed; 
+        { K.conclude_id = gen_id conclude_prefix seed; 
           K.conclude_aref = id;
           K.conclude_method = "Exact";
           K.conclude_args = [K.Term t];
@@ -302,11 +271,11 @@ let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_
   let module C = Cic in
   let module K = Content in
     { K.proof_name = name;
-      K.proof_id   = id ;
+      K.proof_id  = proof_prefix ^ id ;
       K.proof_context = [] ;
       K.proof_apply_context = [];
       K.proof_conclude = 
-        { K.conclude_id = gen_id seed; 
+        { K.conclude_id = gen_id conclude_prefix seed; 
           K.conclude_aref = id;
           K.conclude_method = "Intros+LetTac";
           K.conclude_args = [K.ArgProof inner_proof];
@@ -330,7 +299,7 @@ let build_decl_item seed id n s ~ids_to_inner_sorts =
    if sort = "Prop" then
       `Hypothesis
         { K.dec_name = name_of n;
-          K.dec_id = gen_id seed; 
+          K.dec_id = gen_id declaration_prefix seed; 
           K.dec_inductive = false;
           K.dec_aref = id;
           K.dec_type = s
@@ -338,7 +307,7 @@ let build_decl_item seed id n s ~ids_to_inner_sorts =
    else 
       `Declaration
         { K.dec_name = name_of n;
-          K.dec_id = gen_id seed; 
+          K.dec_id = gen_id declaration_prefix seed; 
           K.dec_inductive = false;
           K.dec_aref = id;
           K.dec_type = s
@@ -361,7 +330,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
               seed ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in
           let new_arg = 
             K.Premise
-              { K.premise_id = gen_id seed;
+              { K.premise_id = gen_id premise_prefix seed;
                 K.premise_xref = new_subproof.K.proof_id;
                 K.premise_binder = new_subproof.K.proof_name;
                 K.premise_n = None
@@ -376,7 +345,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                     with Not_found -> "Type") in 
                  if sort ="Prop" then 
                     K.Premise 
-                      { K.premise_id = gen_id seed;
+                      { K.premise_id = gen_id premise_prefix seed;
                         K.premise_xref = idr;
                         K.premise_binder = Some b;
                         K.premise_n = Some n
@@ -388,7 +357,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                     with Not_found -> "Type") in 
                  if sort ="Prop" then 
                     K.Lemma 
-                      { K.lemma_id = gen_id seed;
+                      { K.lemma_id = gen_id lemma_prefix seed;
                         K.lemma_name = UriManager.name_of_uri uri;
                         K.lemma_uri = UriManager.string_of_uri uri
                       }
@@ -409,7 +378,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                       List.nth inductive_types tyno in 
                     let name,_ = List.nth constructors (consno - 1) in
                     K.Lemma 
-                      { K.lemma_id = gen_id seed;
+                      { K.lemma_id = gen_id lemma_prefix seed;
                         K.lemma_name = name;
                         K.lemma_uri = 
                           UriManager.string_of_uri uri ^ "#xpointer(1/" ^
@@ -453,7 +422,7 @@ build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
       (prerr_endline ("siamo qui???");
       `Definition
         { K.def_name = name_of n;
-          K.def_id = gen_id seed; 
+          K.def_id = gen_id definition_prefix seed; 
           K.def_aref = id;
           K.def_term = t
         })
@@ -551,11 +520,11 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
           let args = build_args seed li subproofs 
                  ~ids_to_inner_types ~ids_to_inner_sorts in *)
             { K.proof_name = name;
-              K.proof_id   = gen_id seed;
+              K.proof_id   = gen_id proof_prefix seed;
               K.proof_context = [];
               K.proof_apply_context = serialize seed subproofs;
               K.proof_conclude = 
-                { K.conclude_id = gen_id seed;
+                { K.conclude_id = gen_id conclude_prefix seed;
                   K.conclude_aref = id;
                   K.conclude_method = "Apply";
                   K.conclude_args = args;
@@ -597,11 +566,11 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
              l,[t] -> l,t
            | _ -> assert false) in
         { K.proof_name = name;
-          K.proof_id   = gen_id seed;
+          K.proof_id   = gen_id proof_prefix seed;
           K.proof_context = []; 
           K.proof_apply_context = serialize seed context;
           K.proof_conclude = 
-            { K.conclude_id = gen_id seed; 
+            { K.conclude_id = gen_id conclude_prefix seed; 
               K.conclude_aref = id;
               K.conclude_method = "Case";
               K.conclude_args = 
@@ -620,22 +589,22 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
         let decreasing_args = 
           List.map (function (_,_,n,_,_) -> n) funs in
         let jo = 
-          { K.joint_id = gen_id seed;
+          { K.joint_id = gen_id joint_prefix seed;
             K.joint_kind = `Recursive decreasing_args;
             K.joint_defs = proofs
           } 
         in
           { K.proof_name = name;
-            K.proof_id   = gen_id seed;
+            K.proof_id  = gen_id proof_prefix seed;
             K.proof_context = [`Joint jo]; 
             K.proof_apply_context = [];
             K.proof_conclude = 
-              { K.conclude_id = gen_id seed; 
+              { K.conclude_id = gen_id conclude_prefix seed; 
                 K.conclude_aref = id;
                 K.conclude_method = "Exact";
                 K.conclude_args =
                 [ K.Premise
-                  { K.premise_id = gen_id seed; 
+                  { K.premise_id = gen_id premise_prefix seed; 
                     K.premise_xref = jo.K.joint_id;
                     K.premise_binder = Some "tiralo fuori";
                     K.premise_n = Some no;
@@ -652,22 +621,22 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
           List.map 
             (function (_,name,_,bo) -> `Proof (aux ~name bo)) funs in
         let jo = 
-          { K.joint_id = gen_id seed;
+          { K.joint_id = gen_id joint_prefix seed;
             K.joint_kind = `CoRecursive;
             K.joint_defs = proofs
           } 
         in
           { K.proof_name = name;
-            K.proof_id   = gen_id seed;
+            K.proof_id   = gen_id proof_prefix seed;
             K.proof_context = [`Joint jo]; 
             K.proof_apply_context = [];
             K.proof_conclude = 
-              { K.conclude_id = gen_id seed; 
+              { K.conclude_id = gen_id conclude_prefix seed; 
                 K.conclude_aref = id;
                 K.conclude_method = "Exact";
                 K.conclude_args =
                 [ K.Premise
-                  { K.premise_id = gen_id seed; 
+                  { K.premise_id = gen_id premise_prefix seed; 
                     K.premise_xref = jo.K.joint_id;
                     K.premise_binder = Some "tiralo fuori";
                     K.premise_n = Some no;
@@ -764,7 +733,8 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                                      let inductive_hyp =
                                        `Hypothesis
                                          { K.dec_name = name_of n2;
-                                           K.dec_id = gen_id seed; 
+                                           K.dec_id =
+                                            gen_id declaration_prefix seed; 
                                            K.dec_inductive = true;
                                            K.dec_aref = id2;
                                            K.dec_type = s2
@@ -788,11 +758,11 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
               | _ -> assert false in
           build_method_args (constructors1,args_for_cases) in
           { K.proof_name = name;
-            K.proof_id   = gen_id seed;
+            K.proof_id   = gen_id proof_prefix seed;
             K.proof_context = []; 
             K.proof_apply_context = serialize seed subproofs;
             K.proof_conclude = 
-              { K.conclude_id = gen_id seed; 
+              { K.conclude_id = gen_id conclude_prefix seed; 
                 K.conclude_aref = id;
                 K.conclude_method = method_name;
                 K.conclude_args =
@@ -840,11 +810,11 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                 hd::(ma_aux (n-1) tl) in
           (ma_aux 3 args) in 
           { K.proof_name = name;
-            K.proof_id   = gen_id seed;
+            K.proof_id  = gen_id proof_prefix seed;
             K.proof_context = []; 
             K.proof_apply_context = serialize seed subproofs;
             K.proof_conclude = 
-              { K.conclude_id = gen_id seed; 
+              { K.conclude_id = gen_id conclude_prefix seed; 
                 K.conclude_aref = id;
                 K.conclude_method = "Rewrite";
                 K.conclude_args = 
@@ -874,7 +844,7 @@ let map_conjectures
            (* the inner-types ==> we always produce a declaration      *)
            (`Declaration
              { K.dec_name = name_of name;
-               K.dec_id = gen_id seed; 
+               K.dec_id = gen_id declaration_prefix seed; 
                K.dec_inductive = false;
                K.dec_aref = get_id t;
                K.dec_type = t
@@ -886,7 +856,7 @@ let map_conjectures
            (* the inner-types ==> we always produce a declaration     *)
            (`Definition
               { K.def_name = name_of name;
-                K.def_id = gen_id seed; 
+                K.def_id = gen_id definition_prefix seed; 
                 K.def_aref = get_id t;
                 K.def_term = t
               })
@@ -902,7 +872,7 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
   let seed = ref 0 in
   function
       C.ACurrentProof (_,_,n,conjectures,bo,ty,params) ->
-        (gen_id seed, params,
+        (gen_id object_prefix seed, params,
           Some
            (List.map
              (map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types)
@@ -911,29 +881,29 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
             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) ->
-         (gen_id seed, params, None,
+         (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) ->
-         (gen_id seed, params, None,
+         (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) ->
-         (gen_id seed, params, None,
+         (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) ->
-         (gen_id seed, params, None,
+         (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) ->
-         (gen_id seed, params, None,
+         (gen_id object_prefix seed, params, None,
             `Joint
-              { K.joint_id = gen_id seed;
+              { K.joint_id = gen_id joint_prefix seed;
                 K.joint_kind = `Inductive nparams;
                 K.joint_defs = List.map (build_inductive seed) l
               }) 
@@ -943,7 +913,7 @@ and
      let module K = Content in
       fun (_,n,b,ty,l) ->
         `Inductive
-          { K.inductive_id = gen_id seed;
+          { K.inductive_id = gen_id inductive_prefix seed;
             K.inductive_kind = b;
             K.inductive_type = ty;
             K.inductive_constructors = build_constructors seed l
@@ -955,7 +925,7 @@ and
       List.map 
        (fun (n,t) ->
            { K.dec_name = Some n;
-             K.dec_id = gen_id seed;
+             K.dec_id = gen_id declaration_prefix seed;
              K.dec_inductive = false;
              K.dec_aref = "";
              K.dec_type = t