added oblivion_universe and used it in paxck_coercions

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index d48772c27a40a0bea41d14eeb0e55de644fb1976..fae784d369a9c59d295b72ba87907d66fdf395ff 100644 (file)
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -143,16 +143,18 @@ let partial = ref 0.0 ;;
 
 let reset_spent_time () = time_spent := 0.0;;
 let get_spent_time () = !time_spent ;;
-let begin_spending () =
+let begin_spending () = ()
   (*assert (!partial = 0.0);*)
-  partial := Unix.gettimeofday ()
+(*   partial := Unix.gettimeofday () *)
 ;;
 
-let end_spending () =
+let end_spending () = ()
+(*
   assert (!partial > 0.0);
   let interval = (Unix.gettimeofday ()) -. !partial in
     partial := 0.0;
     time_spent := !time_spent +. interval
+*)
 ;;
 
 
@@ -416,7 +418,7 @@ let error arc node1 closure_type node2 closure =
   raise (UniverseInconsistency s)
 
 
-let fill_empty_nodes_with_uri (g, already_contained) l uri =
+let fill_empty_nodes_with_uri (g, already_contained,o) l uri =
   let fill_empty_universe u =
     match u with
         (i,None) -> (i,Some uri)
@@ -440,17 +442,18 @@ let fill_empty_nodes_with_uri (g, already_contained) l uri =
       MAL.add (fill_empty_universe k) (fill_empty_entry v) m) m MAL.empty
   in
   let l' = List.map fill_empty_universe l in
-    (m', already_contained),l'
+    (m', already_contained,o),l'
 
 
 (*****************************************************************************)
 (** World interface                                                         **)
 (*****************************************************************************)
 
-type universe_graph = bag * UriManager.UriSet.t 
-(* the graph , the cache of already merged ugraphs *)
+type universe_graph = bag * UriManager.UriSet.t * bool
+(* the graph , the cache of already merged ugraphs, oblivion? *)
 
-let empty_ugraph = empty_bag, UriManager.UriSet.empty
+let empty_ugraph = empty_bag, UriManager.UriSet.empty, false
+let oblivion_ugraph = empty_bag, UriManager.UriSet.empty, true
 
 let current_index_anon = ref (-1)
 let current_index_named = ref (-1)
@@ -476,7 +479,8 @@ let name_universe u uri =
   | (i, None) -> (i, Some uri)
   | _ -> u
   
-let print_ugraph (g, _) = 
+let print_ugraph (g, _, o) = 
+  if o then prerr_endline "oblivion universe" else
   prerr_endline (string_of_bag g)
 
 let add_eq ?(fast=(!fast_implementation)) u v b =
@@ -535,26 +539,29 @@ let add_gt ?(fast=(!fast_implementation)) u v b =
 (** START: Decomment this for performance comparisons                       **)
 (*****************************************************************************)
 
-let add_eq ?(fast=(!fast_implementation))  u v (b,already_contained) =
+let add_eq ?(fast=(!fast_implementation))  u v (b,already_contained,oblivion) =
+        if oblivion then (b,already_contained,oblivion) else
   (*prerr_endline "add_eq";*)
-  begin_spending ();
+  (begin_spending ();
   let rc = add_eq ~fast u v b in
   end_spending ();
-    rc,already_contained
+    rc,already_contained,false)
 
-let add_ge ?(fast=(!fast_implementation)) u v (b,already_contained) =
+let add_ge ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) =
+        if oblivion then (b,already_contained,oblivion) else
 (*   prerr_endline "add_ge"; *)
-  begin_spending ();
+  (begin_spending ();
   let rc = add_ge ~fast u v b in
   end_spending ();
-    rc,already_contained
+    rc,already_contained,false)
     
-let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained) =
+let add_gt ?(fast=(!fast_implementation)) u v (b,already_contained,oblivion) =
+        if oblivion then (b,already_contained,oblivion) else
 (*   prerr_endline "add_gt"; *)
-  begin_spending ();
+  (begin_spending ();
   let rc = add_gt ~fast u v b in
   end_spending ();
-    rc,already_contained
+    rc,already_contained,false)
     
 (* profiling code
 let profiler_eq = HExtlib.profile "CicUniv.add_eq"
@@ -572,8 +579,10 @@ let add_eq ?fast u v b =
 (** END: Decomment this for performance comparisons                         **)
 (*****************************************************************************)
 
-let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment) =
-  let merge_brutal (u,_) v =
+(* TODO: uncomment l to gain a small speedup *)
+let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment(*,l*)) =
+  let merge_brutal (u,a,_) v = 
+    prerr_endline (UriManager.string_of_uri uri_of_increment);
     let m1 = u in 
     let m2 = v in 
       MAL.fold (
@@ -590,19 +599,28 @@ let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment) =
                    fun u x ->
                      let m = add_eq k u x in m) 
                       (SOF.union v.one_s_eq v.eq_closure) x)))
-          ) m1 m2
+          ) m1 m2 
   in
-  let base, already_contained = base_ugraph in
-  if MAL.is_empty base then
+  let base, already_contained, oblivion = base_ugraph in
+  let inc,_,oblivion2 = increment in
+  if oblivion then
+    base_ugraph      
+  else if oblivion2 then
+    increment
+  else if MAL.is_empty base then
     increment
   else if 
-    MAL.is_empty (fst increment) || 
+    MAL.is_empty inc || 
     UriManager.UriSet.mem uri_of_increment already_contained 
   then
     base_ugraph
-  else
-    fst (merge_brutal increment base_ugraph), 
-    UriManager.UriSet.add uri_of_increment already_contained
+  else 
+    (fun (x,_,_) -> x) (merge_brutal increment base_ugraph), 
+(*
+    List.fold_right UriManager.UriSet.add 
+    (List.map (fun (_,x) -> HExtlib.unopt x) l)
+*)
+    (UriManager.UriSet.add uri_of_increment already_contained), false
 
 (* profiling code; WARNING: the time spent during profiling can be
    greater than the profiled time
@@ -663,7 +681,7 @@ let xml_of_entry u e =
   let content = xml_of_entry_content e in
   ent content
 
-let write_xml_of_ugraph filename (m,_) l =
+let write_xml_of_ugraph filename (m,_,_) l =
     let tokens = 
       [< 
         Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n";
@@ -677,7 +695,7 @@ let write_xml_of_ugraph filename (m,_) l =
 let univno = fst
 
  
-let rec clean_ugraph (m,already_contained) f =
+let rec clean_ugraph m already_contained f =
   let m' = 
     MAL.fold (fun k v x -> if (f k) then MAL.add k v x else x ) m MAL.empty in
   let m'' =  MAL.fold (fun k v x -> 
@@ -698,15 +716,17 @@ let rec clean_ugraph (m,already_contained) f =
   in
     if e_l != [] then
       clean_ugraph 
-        (m'', already_contained) (fun u -> (f u) && not (List.mem u e_l))
+        m'' already_contained (fun u -> (f u) && not (List.mem u e_l))
     else
       MAL.fold 
         (fun k v x -> if v <> empty_entry then MAL.add k v x else x) 
         m'' MAL.empty,
       already_contained
 
-let clean_ugraph g l =
-  clean_ugraph g (fun u -> List.mem u l)
+let clean_ugraph (m,a,o) l =
+  assert(not o);
+  let m, a = clean_ugraph m a (fun u -> List.mem u l) in
+  m, a, o
 
 let assigner_of = 
   function
@@ -763,7 +783,7 @@ let ugraph_and_univlist_of_xml filename =
   let xml_source = `Gzip_file filename in
   (try XPP.parse xml_parser xml_source
    with (XPP.Parse_error err) as exn -> raise exn);
-  (!result_map,UriManager.UriSet.empty), !result_list
+  (!result_map,UriManager.UriSet.empty,false), !result_list
 
 \f
 (*****************************************************************************)
@@ -935,7 +955,7 @@ let recons_entry entry =
     one_s_gt = recons_set entry.one_s_gt;
   }
 
-let recons_graph (graph,uriset) =
+let recons_graph (graph,uriset,o) =
   MAL.fold
     (fun universe entry map ->
       MAL.add (recons_univ universe) (recons_entry entry) map)
@@ -945,7 +965,7 @@ let recons_graph (graph,uriset) =
     (fun u acc -> 
       UriManager.UriSet.add 
         (UriManager.uri_of_string (UriManager.string_of_uri u)) acc) 
-    uriset UriManager.UriSet.empty 
+    uriset UriManager.UriSet.empty, o
 
 let assert_univ u =
     match u with 
@@ -953,7 +973,7 @@ let assert_univ u =
        raise (UniverseInconsistency (lazy "This universe graph has a hole"))
     | _ -> ()
     
-let assert_univs_have_uri (graph,_) univlist =
+let assert_univs_have_uri (graph,_,_) univlist =
   let assert_set s =
     SOF.iter (fun u -> assert_univ u) s
   in

diff --git a/helm/software/components/cic/cicUniv.mli b/helm/software/components/cic/cicUniv.mli
index 288efe616885b833ceedb5984af376fda2f8b2ae..7a4331905b50ea95689302c90135011e5649ec5d 100644 (file)
--- a/helm/software/components/cic/cicUniv.mli
+++ b/helm/software/components/cic/cicUniv.mli
@@ -57,6 +57,9 @@ val name_universe: universe -> UriManager.uri -> universe
 *)
 val empty_ugraph: universe_graph
 
+(* an universe that does nothing: i.e. no constraints are kept, no merges.. *)
+val oblivion_ugraph: universe_graph
+
 (*
   These are the real functions to add eq/ge/gt constraints 
   to the passed graph, returning an updated graph or raising

diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml
index 31b47f672a4b8f7a2a7262d6159e970ed039386d..496452a87bf75f02efaa3344a3742f4592d29406 100644 (file)
--- a/helm/software/components/cic/cicUtil.ml
+++ b/helm/software/components/cic/cicUtil.ml
@@ -209,6 +209,8 @@ let attributes_of_obj = function
   | Cic.InductiveDefinition (_, _, _, attributes) ->
       attributes
 
+let is_generated obj = List.exists ((=) `Generated) (attributes_of_obj obj)
+
 let arity_of_composed_coercion obj =
   let attrs = attributes_of_obj obj in
   try
@@ -218,6 +220,20 @@ let arity_of_composed_coercion obj =
     | _-> assert false 
   with Not_found -> 0
 ;;
+
+let projections_of_record obj uri =
+  let attrs = attributes_of_obj obj in
+  try
+    let tag=List.find (function `Class (`Record _) -> true|_->false) attrs in
+    match tag with
+    |  `Class (`Record l) -> 
+         List.map (fun (name,_,_) ->
+           let buri = UriManager.buri_of_uri uri in
+           let puri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in
+           puri) l
+    | _-> assert false 
+  with Not_found -> []
+;;
       
 let rec mk_rels howmany from =
   match howmany with 

diff --git a/helm/software/components/cic/cicUtil.mli b/helm/software/components/cic/cicUtil.mli
index 422bb130b47a0f83b22659f49318c8e6e187c091..9b1fecf0c25de2218a593884d8f92d9fbd4f17b5 100644 (file)
--- a/helm/software/components/cic/cicUtil.mli
+++ b/helm/software/components/cic/cicUtil.mli
@@ -53,7 +53,9 @@ val id_of_annterm: Cic.annterm -> Cic.id
 
 val params_of_obj: Cic.obj -> UriManager.uri list
 val attributes_of_obj: Cic.obj -> Cic.attribute list
+val projections_of_record: Cic.obj -> UriManager.uri -> UriManager.uri list
 val arity_of_composed_coercion: Cic.obj -> int
+val is_generated: Cic.obj -> bool
 
 (** mk_rels [howmany] [from] 
  * creates a list of [howmany] rels starting from [from] in decreasing order *)

diff --git a/helm/software/components/cic_proof_checking/cicEnvironment.ml b/helm/software/components/cic_proof_checking/cicEnvironment.ml
index 314abf4eb99aa7a32fa4cfeeb8eeed561f3ecf60..e64370bf106af8f747ca2bd58088da7685acd2e4 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicEnvironment.ml
+++ b/helm/software/components/cic_proof_checking/cicEnvironment.ml
@@ -459,13 +459,13 @@ let get_cooked_obj_with_univlist ?(trust=true) base_ugraph uri =
   try
     (* the object should be in the cacheOfCookedObjects *)
     let o,u,l = Cache.find_cooked uri in
-      o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)),l
+      o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))),l
   with Not_found ->
     (* this should be an error case, but if we trust the uri... *)
     if trust && trust_obj uri then
       (* trusting means that we will fetch cook it on the fly *)
       let o,u,l = add_trusted_uri_to_cache uri in
-        o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)),l
+        o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))),l
     else
       (* we don't trust the uri, so we fail *)
       begin
@@ -493,14 +493,14 @@ let get_cooked_obj ?trust base_ugraph uri =
  *)
 let is_type_checked ?(trust=true) base_ugraph uri =
   try 
-    let o,u,_ = Cache.find_cooked uri in
-      CheckedObj (o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)))
+    let o,u,l = Cache.find_cooked uri in
+      CheckedObj (o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))))
   with Not_found ->
     (* this should return UncheckedObj *)
     if trust && trust_obj uri then
       (* trusting means that we will fetch cook it on the fly *)
-      let o,u,_ = add_trusted_uri_to_cache uri in
-        CheckedObj ( o, CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
+      let o,u,l = add_trusted_uri_to_cache uri in
+        CheckedObj ( o, CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*)))
     else
       let o,u,_ = find_or_add_to_unchecked uri in
       Cache.unchecked_to_frozen uri;
@@ -513,12 +513,12 @@ let is_type_checked ?(trust=true) base_ugraph uri =
 let get_obj base_ugraph uri =
   try
     (* the object should be in the cacheOfCookedObjects *)
-    let o,u,_ = Cache.find_cooked uri in
-      o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
+    let o,u,l = Cache.find_cooked uri in
+      o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*)))
   with Not_found ->
     (* this should be an error case, but if we trust the uri... *)
-      let o,u,_ = find_or_add_to_unchecked uri in
-        o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
+      let o,u,l = find_or_add_to_unchecked uri in
+        o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*)))
 ;; 
 
 let in_cache uri =

diff --git a/helm/software/components/cic_proof_checking/freshNamesGenerator.ml b/helm/software/components/cic_proof_checking/freshNamesGenerator.ml
index 1edb35b0420656b16f728623aadfd9f4d7e29098..4838623c257bed1ad15eec199c5c66a2524c64fb 100755 (executable)
--- a/helm/software/components/cic_proof_checking/freshNamesGenerator.ml
+++ b/helm/software/components/cic_proof_checking/freshNamesGenerator.ml
@@ -83,7 +83,8 @@ let mk_fresh_name ~subst metasenv context name ~typ =
        (try
         let ty,_ = 
           CicTypeChecker.type_of_aux' ~subst metasenv context typ 
-            CicUniv.empty_ugraph in 
+            CicUniv.oblivion_ugraph 
+        in 
          (match ty with
              C.Sort C.Prop
            | C.Sort C.CProp -> "H"

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 95651c49fe96ff9ebddec5eed4a8463422b5d67e..9cb0a04a43b8c5c55c34a224248e078f73f8f9ce 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1763,7 +1763,7 @@ let pack_coercion metasenv ctx t =
    | C.LetIn (name,so,dest) -> 
        let _,ty,metasenv,ugraph =
         pack_coercions := false;
-        type_of_aux' metasenv ctx so CicUniv.empty_ugraph in
+        type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
         pack_coercions := true;
        let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
        C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
@@ -1773,7 +1773,7 @@ let pack_coercion metasenv ctx t =
        let b,_,_,_,_ = is_a_double_coercion t in
        (* prerr_endline "CANDIDATO!!!!"; *)
        if b then
-         let ugraph = CicUniv.empty_ugraph in
+         let ugraph = CicUniv.oblivion_ugraph in
          let old_insert_coercions = !insert_coercions in
          insert_coercions := false;
          let newt, _, menv, _ =