From 8f86320e1ee981e2a8ad6c56b031a0394c8c1ad3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 3 Oct 2005 08:10:18 +0000 Subject: [PATCH] moved to fast implementation and fixed a bug in the clean_ugraph function --- helm/ocaml/cic/cicUniv.ml | 32 ++++++++++++++++++++++---------- helm/ocaml/cic/cicUniv.mli | 3 +++ 2 files changed, 25 insertions(+), 10 deletions(-) diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml index 0ea97404e..3d92f3335 100644 --- a/helm/ocaml/cic/cicUniv.ml +++ b/helm/ocaml/cic/cicUniv.ml @@ -38,7 +38,7 @@ (** switch implementation **) (*****************************************************************************) -let fast_implementation = ref false ;; +let fast_implementation = ref true ;; (*****************************************************************************) (** open **) @@ -272,7 +272,7 @@ and add_ge_arc_fast u v m = let rv = repr v m' in let rv' = {rv with in_gegt_of = SOF.add u rv.in_gegt_of} in let m'' = MAL.add v rv' m' in - adjust_fast u m'' + adjust_fast u m'' and add_eq_arc_fast u v m = let ru = repr u m in @@ -420,7 +420,7 @@ let fill_empty_nodes_with_uri g l uri = let fill_empty_set s = SOF.fold (fun e s -> SOF.add (fill_empty_universe e) s) s SOF.empty in - let fill_empty_entry e = { + let fill_empty_entry e = { e with eq_closure = (fill_empty_set e.eq_closure) ; ge_closure = (fill_empty_set e.ge_closure) ; gt_closure = (fill_empty_set e.gt_closure) ; @@ -465,6 +465,11 @@ let fresh ?uri ?id () = in (i,uri) +let name_universe u uri = + match u with + | (i, None) -> (i, Some uri) + | _ -> u + let print_ugraph g = prerr_endline (string_of_bag g) @@ -558,16 +563,19 @@ let merge_ugraphs u v = fun k v x -> (SOF.fold ( fun u x -> - let m = add_gt k u x in m) v.one_s_gt + let m = add_gt k u x in m) + (SOF.union v.one_s_gt v.gt_closure) (SOF.fold ( fun u x -> - let m = add_ge k u x in m) v.one_s_ge + let m = add_ge k u x in m) + (SOF.union v.one_s_ge v.ge_closure) (SOF.fold ( - fun u x -> - let m = add_eq k u x in m) v.one_s_eq x))) + fun u x -> + let m = add_eq k u x in m) + (SOF.union v.one_s_eq v.eq_closure) x))) ) m1 m2 in - merge_brutal u v + merge_brutal u v (*****************************************************************************) @@ -650,12 +658,16 @@ let rec clean_ugraph m f = } in MAL.add k v' x ) m' MAL.empty in let e_l = - MAL.fold (fun k v l -> if v = empty_entry then k::l else l) m'' [] + MAL.fold (fun k v l -> if v = empty_entry && not(f k) then + begin + k::l end else l) m'' [] in if e_l != [] then clean_ugraph m'' (fun u -> (f u) && not (List.mem u e_l)) else - m'' + MAL.fold + (fun k v x -> if v <> empty_entry then MAL.add k v x else x) + m'' MAL.empty let clean_ugraph g l = clean_ugraph g (fun u -> List.mem u l) diff --git a/helm/ocaml/cic/cicUniv.mli b/helm/ocaml/cic/cicUniv.mli index 219513012..be8c28bf3 100644 --- a/helm/ocaml/cic/cicUniv.mli +++ b/helm/ocaml/cic/cicUniv.mli @@ -48,6 +48,9 @@ val fresh: unit -> universe + (* names a universe if unnamed *) +val name_universe: universe -> UriManager.uri -> universe + (* really useful at the begin and in all the functions that don't care of universes -- 2.39.2