From 001b43beae9e912a921da426d23c1e437328bb9e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 2 Jan 2007 18:03:59 +0000 Subject: [PATCH] added oblivion_universe and used it in paxck_coercions --- components/cic/cicUniv.ml | 92 +++++++++++-------- components/cic/cicUniv.mli | 3 + components/cic/cicUtil.ml | 16 ++++ components/cic/cicUtil.mli | 2 + .../cic_proof_checking/cicEnvironment.ml | 20 ++-- .../cic_proof_checking/freshNamesGenerator.ml | 3 +- components/cic_unification/cicRefine.ml | 4 +- 7 files changed, 91 insertions(+), 49 deletions(-) diff --git a/components/cic/cicUniv.ml b/components/cic/cicUniv.ml index d48772c27..fae784d36 100644 --- a/components/cic/cicUniv.ml +++ b/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 "\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 (*****************************************************************************) @@ -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/components/cic/cicUniv.mli b/components/cic/cicUniv.mli index 288efe616..7a4331905 100644 --- a/components/cic/cicUniv.mli +++ b/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/components/cic/cicUtil.ml b/components/cic/cicUtil.ml index 31b47f672..496452a87 100644 --- a/components/cic/cicUtil.ml +++ b/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/components/cic/cicUtil.mli b/components/cic/cicUtil.mli index 422bb130b..9b1fecf0c 100644 --- a/components/cic/cicUtil.mli +++ b/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/components/cic_proof_checking/cicEnvironment.ml b/components/cic_proof_checking/cicEnvironment.ml index 314abf4eb..e64370bf1 100644 --- a/components/cic_proof_checking/cicEnvironment.ml +++ b/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/components/cic_proof_checking/freshNamesGenerator.ml b/components/cic_proof_checking/freshNamesGenerator.ml index 1edb35b04..4838623c2 100755 --- a/components/cic_proof_checking/freshNamesGenerator.ml +++ b/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/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 95651c49f..9cb0a04a4 100644 --- a/components/cic_unification/cicRefine.ml +++ b/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, _ = -- 2.39.2