X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicUniv.ml;h=3d92f33358f1b76929027eb0366da95bea03d7ec;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=05e0a99a1e9f7435902328ce7f988d06894f1cdc;hpb=655906d74521fa49de332f54ec34bfc9d9744151;p=helm.git diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml index 05e0a99a1..3d92f3335 100644 --- a/helm/ocaml/cic/cicUniv.ml +++ b/helm/ocaml/cic/cicUniv.ml @@ -23,519 +23,925 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Enrico Tassi *) -(* 23/04/2004 *) -(* *) -(* This module implements the aciclic graph of universes. *) -(* *) -(******************************************************************************) +(*****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Enrico Tassi *) +(* 23/04/2004 *) +(* *) +(* This module implements the aciclic graph of universes. *) +(* *) +(*****************************************************************************) + +(*****************************************************************************) +(** switch implementation **) +(*****************************************************************************) + +let fast_implementation = ref true ;; + +(*****************************************************************************) +(** open **) +(*****************************************************************************) open Printf -(******************************************************************************) -(** Types and default values **) -(******************************************************************************) - -type universe = int +(*****************************************************************************) +(** Types and default values **) +(*****************************************************************************) +type universe = int * UriManager.uri option + module UniverseType = struct type t = universe let compare = Pervasives.compare end - + module SOF = Set.Make(UniverseType) - + type entry = { - eq_closure : SOF.t; - ge_closure : SOF.t; - gt_closure : SOF.t; - in_eq_of : SOF.t; - in_ge_of : SOF.t; - in_gt_of : SOF.t; - one_s_eq : SOF.t; - one_s_ge : SOF.t; - one_s_gt : SOF.t; + eq_closure : SOF.t; + ge_closure : SOF.t; + gt_closure : SOF.t; + in_gegt_of : SOF.t; + one_s_eq : SOF.t; + one_s_ge : SOF.t; + one_s_gt : SOF.t; } - + module MAL = Map.Make(UniverseType) - + type arc_type = GE | GT | EQ - -type arc = arc_type * universe * universe - -type bag = entry MAL.t * (arc list) - + +type bag = entry MAL.t + let empty_entry = { - eq_closure=SOF.empty; - ge_closure=SOF.empty; - gt_closure=SOF.empty; - in_eq_of=SOF.empty; - in_ge_of=SOF.empty; - in_gt_of=SOF.empty; - one_s_eq=SOF.empty; - one_s_ge=SOF.empty; - one_s_gt=SOF.empty; + eq_closure=SOF.empty; + ge_closure=SOF.empty; + gt_closure=SOF.empty; + in_gegt_of=SOF.empty; + one_s_eq=SOF.empty; + one_s_ge=SOF.empty; + one_s_gt=SOF.empty; } +let empty_bag = MAL.empty -let empty_bag = (MAL.empty, []) +let are_set_eq s1 s2 = + SOF.equal s1 s2 -let env_bag = ref empty_bag +let are_entry_eq v1 v2 = + (are_set_eq v1.gt_closure v2.gt_closure ) && + (are_set_eq v1.ge_closure v2.ge_closure ) && + (are_set_eq v1.eq_closure v2.eq_closure ) && + (*(are_set_eq v1.in_gegt_of v2.in_gegt_of ) &&*) + (are_set_eq v1.one_s_ge v2.one_s_ge ) && + (are_set_eq v1.one_s_gt v2.one_s_gt ) && + (are_set_eq v1.one_s_eq v2.one_s_eq ) -(******************************************************************************) -(** Pretty printings **) -(******************************************************************************) +let are_ugraph_eq = MAL.equal are_entry_eq -let string_of_universe u = string_of_int u +(*****************************************************************************) +(** Pretty printings **) +(*****************************************************************************) -let string_of_arc_type u = +let string_of_universe (i,u) = match u with - EQ -> "EQ" - | GT -> "GT" - | GE -> "EQ" - -let string_of_arc u = - let atype,a,b = u in - (string_of_arc_type atype) ^ " " ^ - (string_of_universe a) ^ " " ^ (string_of_universe b) ^ "; " -;; + Some u -> + "(" ^ ((string_of_int i) ^ "," ^ (UriManager.string_of_uri u) ^ ")") + | None -> "(" ^ (string_of_int i) ^ ",None)" let string_of_universe_set l = SOF.fold (fun x s -> s ^ (string_of_universe x) ^ " ") l "" -let string_of_arc_list l = - List.fold_left (fun s x -> s ^ (string_of_arc x) ^ " ") "" l - let string_of_node n = "{"^ "eq_c: " ^ (string_of_universe_set n.eq_closure) ^ "; " ^ "ge_c: " ^ (string_of_universe_set n.ge_closure) ^ "; " ^ "gt_c: " ^ (string_of_universe_set n.gt_closure) ^ "; " ^ - "i_eq: " ^ (string_of_universe_set n.in_eq_of) ^ "; " ^ - "i_ge: " ^ (string_of_universe_set n.in_ge_of) ^ "; " ^ - "i_gt: " ^ (string_of_universe_set n.in_gt_of) ^ "}\n" + "i_gegt: " ^ (string_of_universe_set n.in_gegt_of) ^ "}\n" + +let string_of_arc (a,u,v) = + (string_of_universe u) ^ " " ^ a ^ " " ^ (string_of_universe v) let string_of_mal m = let rc = ref "" in - MAL.iter (fun k v -> rc := !rc ^ sprintf "%d --> %s" k (string_of_node v)) m; + MAL.iter (fun k v -> + rc := !rc ^ sprintf "%s --> %s" (string_of_universe k) + (string_of_node v)) m; !rc let string_of_bag b = - let (m,l) = b in - let s_m = string_of_mal m in - let s_l = string_of_arc_list l in - s_m ^"["^s_l^"]" - -(******************************************************************************) -(** Helpers **) -(******************************************************************************) - -(* - we need to merge the 2 graphs... here the code -*) + string_of_mal b + +(*****************************************************************************) +(** Helpers **) +(*****************************************************************************) + +(* find the repr *) let repr u m = try MAL.find u m with - Not_found -> - try - let m',_ = !env_bag in - MAL.find u m' - with - Not_found -> empty_entry + Not_found -> empty_entry -(* - FIXME: May be faster if we make it by hand -*) +(* FIXME: May be faster if we make it by hand *) let merge_closures f nodes m = SOF.fold (fun x i -> SOF.union (f (repr x m)) i ) nodes SOF.empty -(******************************************************************************) -(** Real stuff GT **) -(******************************************************************************) +(*****************************************************************************) +(** Benchmarking **) +(*****************************************************************************) +let time_spent = ref 0.0;; +let partial = ref 0.0 ;; + +let reset_spent_time () = time_spent := 0.0;; +let get_spent_time () = !time_spent ;; +let begin_spending () = + (*assert (!partial = 0.0);*) + partial := Unix.gettimeofday () +;; -(* - todo is the SOF of nodes that needs to be recomputed, - m is the MAL map, s is the already touched nodes -*) -let rec redo_gt_closure todo m s = - if SOF.is_empty todo then m - else - begin - (* we choose the node to recompute *) - let u = SOF.choose todo in - if not (SOF.mem u s) then - let ru = repr u m in - let ru' = {ru with gt_closure = - (* the new gt closure is the gt-closures + ge-closures + eq-closures - of the one step gt-connected nodes *) - SOF.union ru.one_s_gt (merge_closures - (fun x -> SOF.union x.eq_closure - (SOF.union x.gt_closure x.ge_closure)) ru.one_s_gt m) } in - let m' = MAL.add u ru' m in - let s' = SOF.add u s in - redo_gt_closure (SOF.union (SOF.remove u todo) ru'.in_gt_of) m' s' +let end_spending () = + assert (!partial > 0.0); + let interval = (Unix.gettimeofday ()) -. !partial in + partial := 0.0; + time_spent := !time_spent +. interval +;; + + +(*****************************************************************************) +(** _fats implementation **) +(*****************************************************************************) + +let rec closure_of_fast ru m = + let eq_c = closure_eq_fast ru m in + let ge_c = closure_ge_fast ru m in + let gt_c = closure_gt_fast ru m in + { + eq_closure = eq_c; + ge_closure = ge_c; + gt_closure = gt_c; + in_gegt_of = ru.in_gegt_of; + one_s_eq = ru.one_s_eq; + one_s_ge = ru.one_s_ge; + one_s_gt = ru.one_s_gt + } + +and closure_eq_fast ru m = + let eq_c = + let j = ru.one_s_eq in + let _Uj = merge_closures (fun x -> x.eq_closure) j m in + let one_step_eq = ru.one_s_eq in + (SOF.union one_step_eq _Uj) + in + eq_c + +and closure_ge_fast ru m = + let ge_c = + let j = SOF.union ru.one_s_ge (SOF.union ru.one_s_gt ru.one_s_eq) in + let _Uj = merge_closures (fun x -> x.ge_closure) j m in + let _Ux = j in + (SOF.union _Uj _Ux) + in + ge_c + +and closure_gt_fast ru m = + let gt_c = + let j = ru.one_s_gt in + let k = ru.one_s_ge in + let l = ru.one_s_eq in + let _Uj = merge_closures (fun x -> x.ge_closure) j m in + let _Uk = merge_closures (fun x -> x.gt_closure) k m in + let _Ul = merge_closures (fun x -> x.gt_closure) l m in + let one_step_gt = ru.one_s_gt in + (SOF.union (SOF.union (SOF.union _Ul one_step_gt) _Uk) _Uj) + in + gt_c + +and print_rec_status u ru = + print_endline ("Aggiusto " ^ (string_of_universe u) ^ + "e ottengo questa chiusura\n " ^ (string_of_node ru)) + +and adjust_fast u m = + let ru = repr u m in + let gt_c = closure_gt_fast ru m in + let ge_c = closure_ge_fast ru m in + let eq_c = closure_eq_fast ru m in + let changed_eq = not (are_set_eq eq_c ru.eq_closure) in + let changed_gegt = + (not (are_set_eq gt_c ru.gt_closure)) || + (not (are_set_eq ge_c ru.ge_closure)) + in + if ((not changed_gegt) && (not changed_eq)) then + m else - (* if already done go next. FIXME: think if it is right - maybe we should check if we changed something or not *) - redo_gt_closure (SOF.remove u todo) m s - end + begin + let ru' = { + eq_closure = eq_c; + ge_closure = ge_c; + gt_closure = gt_c; + in_gegt_of = ru.in_gegt_of; + one_s_eq = ru.one_s_eq; + one_s_ge = ru.one_s_ge; + one_s_gt = ru.one_s_gt} + in + let m = MAL.add u ru' m in + let m = + SOF.fold (fun x m -> adjust_fast x m) + (SOF.union ru'.eq_closure ru'.in_gegt_of) m + (* TESI: + ru'.in_gegt_of m + *) + in + m (*adjust_fast u m*) + end + +and add_gt_arc_fast u v m = + let ru = repr u m in + let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in + let m' = MAL.add u ru' m in + 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'' + +and add_ge_arc_fast u v m = + let ru = repr u m in + let ru' = { ru with one_s_ge = SOF.add v ru.one_s_ge} in + let m' = MAL.add u ru' m in + 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'' -(* - calculates the closures of u and adjusts the in_*_of of v, then - starts redo_*_closure to adjust the colure of nodew thet have - (clusure u) in theyr closures -*) -let add_gt_arc u v m = +and add_eq_arc_fast u v m = let ru = repr u m in let rv = repr v m in - let ru' = { - (* new node: we add the v gt-closure and v to our gt-closure *) - eq_closure = ru.eq_closure; - ge_closure = ru.ge_closure; - gt_closure = SOF.add v - (SOF.union ru.gt_closure - (SOF.union rv.ge_closure - (SOF.union rv.eq_closure rv.gt_closure))); - in_eq_of = ru.in_eq_of; - in_ge_of = ru.in_ge_of; - in_gt_of = ru.in_gt_of; - one_s_eq = ru.one_s_eq; - one_s_ge = ru.one_s_ge; - one_s_gt = SOF.add v ru.one_s_gt; - } in - (* may add the sanity check *) - let rv' = { rv with in_gt_of = SOF.add u rv.in_gt_of } in + let ru' = {ru with one_s_eq = SOF.add v ru.one_s_eq} in + (*TESI: let ru' = {ru' with in_gegt_of = SOF.add v ru.in_gegt_of} in *) let m' = MAL.add u ru' m in + let rv' = {rv with one_s_eq = SOF.add u rv.one_s_eq} in + (*TESI: let rv' = {rv' with in_gegt_of = SOF.add u rv.in_gegt_of} in *) let m'' = MAL.add v rv' m' in - redo_gt_closure ru'.in_gt_of m'' SOF.empty - -(* - given the 2 nodes plus the current bag, adds the arc, recomputes the - closures and returns the new map -*) -let add_gt u v b = - let m,l = b in - let m' = add_gt_arc u v m in - let l' = (GT,u,v)::l in - (m',l') + adjust_fast v (*(adjust_fast u*) m'' (* ) *) +;; -(******************************************************************************) -(** Real stuff GE **) -(******************************************************************************) + +(*****************************************************************************) +(** safe implementation **) +(*****************************************************************************) -(* - todo is the SOF of nodes that needs to be recomputed, - m is the MAL map, s is the already touched nodes -*) -let rec redo_ge_closure todo m s = - if SOF.is_empty todo then m,s - else - begin - let u = SOF.choose todo in - if not (SOF.mem u s) then - begin - let ru = repr u m in - (* the ge-closure is recomputed as the ge-closures of - ge connected nodes plus theys eq-closure *) - let ru' = {ru with ge_closure = merge_closures - (fun x -> SOF.union x.eq_closure x.ge_closure) ru.one_s_ge m } in - let m' = MAL.add u ru' m in - let s' = SOF.add u s in - redo_ge_closure (SOF.union (SOF.remove u todo) ru'.in_ge_of) m' s' - end +let closure_of u m = + let ru = repr u m in + let eq_c = + let j = ru.one_s_eq in + let _Uj = merge_closures (fun x -> x.eq_closure) j m in + let one_step_eq = ru.one_s_eq in + (SOF.union one_step_eq _Uj) + in + let ge_c = + let j = SOF.union ru.one_s_ge (SOF.union ru.one_s_gt ru.one_s_eq) in + let _Uj = merge_closures (fun x -> x.ge_closure) j m in + let _Ux = j in + (SOF.union _Uj _Ux) + in + let gt_c = + let j = ru.one_s_gt in + let k = ru.one_s_ge in + let l = ru.one_s_eq in + let _Uj = merge_closures (fun x -> x.ge_closure) j m in + let _Uk = merge_closures (fun x -> x.gt_closure) k m in + let _Ul = merge_closures (fun x -> x.gt_closure) l m in + let one_step_gt = ru.one_s_gt in + (SOF.union (SOF.union (SOF.union _Ul one_step_gt) _Uk) _Uj) + in + { + eq_closure = eq_c; + ge_closure = ge_c; + gt_closure = gt_c; + in_gegt_of = ru.in_gegt_of; + one_s_eq = ru.one_s_eq; + one_s_ge = ru.one_s_ge; + one_s_gt = ru.one_s_gt + } + +let rec simple_adjust m = + let m' = + MAL.mapi (fun x _ -> closure_of x m) m + in + if not (are_ugraph_eq m m') then( + simple_adjust m') else - redo_ge_closure (SOF.remove u todo) m s - end + m' -(* - calculates the closures of u and adjusts the in_*_of of v, then - starts redo_*_closure to adjust the colure of nodew thet have - (clusure u) in theyr closures -*) -let add_ge_arc u v m = +let add_eq_arc u v m = let ru = repr u m in - let rv = repr v m in - let ru' = { - eq_closure = ru.eq_closure; - ge_closure = SOF.add v - (SOF.union ru.ge_closure - (SOF.union rv.eq_closure rv.ge_closure)); - gt_closure = ru.gt_closure; - in_eq_of = ru.in_eq_of; - in_ge_of = ru.in_ge_of; - in_gt_of = ru.in_gt_of; - one_s_eq = ru.one_s_eq; - one_s_ge = SOF.add v ru.one_s_ge; - one_s_gt = ru.one_s_gt; - } in - let rv' = { rv with in_gt_of = SOF.add u rv.in_ge_of } in + let rv = repr v m in + let ru' = {ru with one_s_eq = SOF.add v ru.one_s_eq} in let m' = MAL.add u ru' m in + let rv' = {rv with one_s_eq = SOF.add u rv.one_s_eq} in let m'' = MAL.add v rv' m' in - let m''',td = redo_ge_closure ru'.in_ge_of m'' SOF.empty in - (* closing ge may provoke aome changes in gt-closures *) - redo_gt_closure (SOF.union ru'.in_gt_of - (SOF.fold (fun u s -> SOF.union s ((repr u m''').in_gt_of)) - td SOF.empty )) m''' SOF.empty + simple_adjust m'' + +let add_ge_arc u v m = + let ru = repr u m in + let ru' = { ru with one_s_ge = SOF.add v ru.one_s_ge} in + let m' = MAL.add u ru' m in + simple_adjust m' + +let add_gt_arc u v m = + let ru = repr u m in + let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in + let m' = MAL.add u ru' m in + simple_adjust m' + + +(*****************************************************************************) +(** Outhern interface, that chooses between _fast and safe **) +(*****************************************************************************) (* given the 2 nodes plus the current bag, adds the arc, recomputes the closures and returns the new map *) -let add_ge u v b = - let m,l = b in - let m' = add_ge_arc u v m in - let l' = (GE,u,v)::l in - (m',l') - -(******************************************************************************) -(** Real stuff EQ **) -(******************************************************************************) - -let rec redo_eq_closure todo m s = - if SOF.is_empty todo then m,s - else begin - let u = SOF.choose todo in - if not (SOF.mem u s) then - begin - let ru = repr u m in - let eq_closure = merge_closures - (fun x -> x.eq_closure) ru.one_s_eq m in - let ru' = {ru with eq_closure = eq_closure - ; in_eq_of = eq_closure ; one_s_eq = eq_closure } in - let m' = MAL.add u ru' m in - let s' = SOF.add u s in - redo_eq_closure (SOF.union (SOF.remove u todo) ru'.in_eq_of) m' s' - end - else - redo_eq_closure (SOF.remove u todo) m s - end - -(* - calculates the closures of u and adjusts the in_*_of of v, then - starts redo_*_closure to adjust the colure of nodew thet have - (clusure u) in theyr closures -*) -let add_eq_arc u v m = - let ru = repr u m in - let rv = repr v m in - (* since eq is symmetric we have to chage more *) - let eq_closure = SOF.add u (SOF.add v - (SOF.union ru.eq_closure rv.eq_closure)) in - let ru' = { - eq_closure = eq_closure; - ge_closure = SOF.union ru.ge_closure rv.ge_closure; - gt_closure = SOF.union ru.gt_closure rv.gt_closure; - in_eq_of = eq_closure; - in_ge_of = SOF.union ru.in_ge_of rv.in_ge_of; - in_gt_of = SOF.union ru.in_gt_of rv.in_gt_of; - one_s_eq = eq_closure; - one_s_ge = SOF.union ru.one_s_ge rv.one_s_ge; - one_s_gt = SOF.union ru.one_s_gt rv.one_s_gt; - } in - (* this is a collapse *) - let rv' = ru' in - let m' = MAL.add u ru' m in - let m'' = MAL.add v rv' m' in - let m''',td = redo_eq_closure ru'.in_eq_of m'' SOF.empty in - (* redoing a eq may change some ge and some gt *) - let m'''',td' = redo_ge_closure - (SOF.union ru'.in_ge_of - (SOF.fold (fun u s -> SOF.union s ((repr u m''').in_ge_of)) - td SOF.empty)) m''' SOF.empty in - redo_gt_closure (SOF.union ru'.in_gt_of - (SOF.fold (fun u s -> SOF.union s ((repr u m'''').in_gt_of)) - td' SOF.empty)) m'''' SOF.empty +let add_eq fast u v b = + if fast then + add_eq_arc_fast u v b + else + add_eq_arc u v b (* given the 2 nodes plus the current bag, adds the arc, recomputes the closures and returns the new map *) -let add_eq u v b = - let m,l = b in - let m' = add_eq_arc u v m in - let l' = (EQ,u,v)::l in - (m',l') +let add_ge fast u v b = + if fast then + add_ge_arc_fast u v b + else + add_ge_arc u v b +(* + given the 2 nodes plus the current bag, adds the arc, recomputes the + closures and returns the new map +*) +let add_gt fast u v b = + if fast then + add_gt_arc_fast u v b + else + add_gt_arc u v b + -(******************************************************************************) -(** Oyther real code **) -(******************************************************************************) +(*****************************************************************************) +(** Other real code **) +(*****************************************************************************) exception UniverseInconsistency of string let error arc node1 closure_type node2 closure = - let s = " ===== Universe Inconsistency detected =====\n\n" ^ - "\tUnable to add ("^ (string_of_arc arc) ^ ") cause " ^ - (string_of_universe node1) ^ " is in the " ^ - (string_of_arc_type closure_type) ^ " closure {" ^ - (string_of_universe_set closure) ^ "} of " ^ - (string_of_universe node2) ^ "\n\n" ^ + let s = "\n ===== Universe Inconsistency detected =====\n\n" ^ + " Unable to add\n" ^ + "\t" ^ (string_of_arc arc) ^ "\n" ^ + " cause\n" ^ + "\t" ^ (string_of_universe node1) ^ "\n" ^ + " is in the " ^ closure_type ^ " closure\n" ^ + "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^ + " of\n" ^ + "\t" ^ (string_of_universe node2) ^ "\n\n" ^ " ===== Universe Inconsistency detected =====\n" in prerr_endline s; raise (UniverseInconsistency s) -(* - we merge the env_bag with b -*) -let qed b = - let m,l = b in - let m',l' = !env_bag in - let m'' = ref m' in - MAL.iter (fun k v -> m'':= MAL.add k v !m'') m; - let l'' = l @ l' in - env_bag := (!m'',l'') + +let fill_empty_nodes_with_uri g l uri = + let fill_empty_universe u = + match u with + (i,None) -> (i,Some uri) + | (i,Some _) as u -> u + in + 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 = { 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) ; + in_gegt_of = (fill_empty_set e.in_gegt_of) ; + one_s_eq = (fill_empty_set e.one_s_eq) ; + one_s_ge = (fill_empty_set e.one_s_ge) ; + one_s_gt = (fill_empty_set e.one_s_gt) ; + } in + let m = g in + let m' = MAL.fold ( + fun k v m -> + 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',l' + + +(*****************************************************************************) +(** World interface **) +(*****************************************************************************) + +type universe_graph = bag + +let empty_ugraph = empty_bag + +let current_index_anon = ref (-1) +let current_index_named = ref (-1) + +let restart_numbering () = current_index_named := (-1) + +let fresh ?uri ?id () = + let i = + match uri,id with + | None,None -> + current_index_anon := !current_index_anon + 1; + !current_index_anon + | None, Some _ -> assert false + | Some _, None -> + current_index_named := !current_index_named + 1; + !current_index_named + | Some _, Some id -> id + in + (i,uri) + +let name_universe u uri = + match u with + | (i, None) -> (i, Some uri) + | _ -> u -let add_eq u v b = +let print_ugraph g = + prerr_endline (string_of_bag g) + +let add_eq ?(fast=(!fast_implementation)) u v b = (* should we check to no add twice the same?? *) - let m,_ = b in + let m = b in let ru = repr u m in if SOF.mem v ru.gt_closure then - error (EQ,u,v) v GT u ru.gt_closure + error ("EQ",u,v) v "GT" u ru.gt_closure else begin let rv = repr v m in if SOF.mem u rv.gt_closure then - error (EQ,u,v) u GT v rv.gt_closure + error ("EQ",u,v) u "GT" v rv.gt_closure else - add_eq u v b + add_eq fast u v b end -let add_ge u v b = +let add_ge ?(fast=(!fast_implementation)) u v b = (* should we check to no add twice the same?? *) - let m,_ = b in + let m = b in let rv = repr v m in if SOF.mem u rv.gt_closure then - error (GE,u,v) u GT v rv.gt_closure + error ("GE",u,v) u "GT" v rv.gt_closure else - add_ge u v b + add_ge fast u v b -let add_gt u v b = +let add_gt ?(fast=(!fast_implementation)) u v b = (* should we check to no add twice the same?? *) - let m,_ = b in + (* + FIXME : check the thesis... no need to check GT and EQ closure since the + GE is a superset of both + *) + let m = b in let rv = repr v m in - if SOF.mem u rv.gt_closure then - error (GT,u,v) u GT v rv.gt_closure + + if u = v then + error ("GT",u,v) u "==" v SOF.empty else - begin + + (*if SOF.mem u rv.gt_closure then + error ("GT",u,v) u "GT" v rv.gt_closure + else + begin*) if SOF.mem u rv.ge_closure then - error (GT,u,v) u GE v rv.ge_closure + error ("GT",u,v) u "GE" v rv.ge_closure else - begin +(* begin if SOF.mem u rv.eq_closure then - error (GT,u,v) u EQ v rv.eq_closure - else - add_gt u v b - end - end - - - -(******************************************************************************) -(** World interface **) -(******************************************************************************) - -type universe_graph = bag - -let work_bag = ref empty_bag -let current_index = ref (-1) - -let get_working () = !work_bag -let get_global () = !env_bag -let set_working b = work_bag := b + error ("GT",u,v) u "EQ" v rv.eq_closure + else*) + add_gt fast u v b +(* end + end*) + +(*****************************************************************************) +(** START: Decomment this for performance comparisons **) +(*****************************************************************************) + +let add_eq ?(fast=(!fast_implementation)) u v b = + begin_spending (); + let rc = add_eq ~fast u v b in + end_spending(); + rc + +let add_ge ?(fast=(!fast_implementation)) u v b = + begin_spending (); + let rc = add_ge ~fast u v b in + end_spending(); + rc + +let add_gt ?(fast=(!fast_implementation)) u v b = + begin_spending (); + let rc = add_gt ~fast u v b in + end_spending(); + rc + +(*****************************************************************************) +(** END: Decomment this for performance comparisons **) +(*****************************************************************************) + +let merge_ugraphs u v = + (* this sucks *) + let merge_brutal u v = + if u = empty_bag then v + else if v = empty_bag then u + else + let m1 = u in + let m2 = v in + MAL.fold ( + fun k v x -> + (SOF.fold ( + fun u x -> + 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) + (SOF.union v.one_s_ge v.ge_closure) + (SOF.fold ( + 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 -let fresh () = - current_index := !current_index + 1; - !current_index -let qed () = - qed !work_bag +(*****************************************************************************) +(** Xml sesialization and parsing **) +(*****************************************************************************) -let print_global_graph () = - let s = string_of_bag !env_bag in - prerr_endline s +let xml_of_universe name u = + match u with + | (i,Some u) -> + Xml.xml_empty name [ + None,"id",(string_of_int i) ; + None,"uri",(UriManager.string_of_uri u)] + | (_,None) -> + raise (Failure "we can serialize only universes with uri") + +let xml_of_set s = + let l = + List.map (xml_of_universe "node") (SOF.elements s) + in + List.fold_left (fun s x -> [< s ; x >] ) [<>] l + +let xml_of_entry_content e = + let stream_of_field f name = + let eq_c = xml_of_set f in + if eq_c != [<>] then + Xml.xml_nempty name [] eq_c + else + [<>] + in + [< + (stream_of_field e.eq_closure "eq_closure"); + (stream_of_field e.gt_closure "gt_closure"); + (stream_of_field e.ge_closure "ge_closure"); + (stream_of_field e.in_gegt_of "in_gegt_of"); + (stream_of_field e.one_s_eq "one_s_eq"); + (stream_of_field e.one_s_gt "one_s_gt"); + (stream_of_field e.one_s_ge "one_s_ge") + >] + +let xml_of_entry u e = + let (i,u') = u in + let u'' = + match u' with + Some x -> x + | None -> + raise (Failure "we can serialize only universes (entry) with uri") + in + let ent = Xml.xml_nempty "entry" [ + None,"id",(string_of_int i) ; + None,"uri",(UriManager.string_of_uri u'')] in + let content = xml_of_entry_content e in + ent content + +let write_xml_of_ugraph filename m l = + let tokens = + [< + Xml.xml_cdata "\n"; + Xml.xml_nempty "ugraph" [] + ([< (MAL.fold ( fun k v s -> [< s ; (xml_of_entry k v) >]) m [<>]) ; + (List.fold_left + (fun s u -> [< s ; xml_of_universe "owned_node" u >]) [<>] l) >])>] + in + Xml.pp ~gzip:true tokens (Some filename) + +let univno = fst -let print_working_graph () = - let s = string_of_bag !work_bag in - prerr_endline s + +let rec clean_ugraph m 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 -> + let v' = { + eq_closure = SOF.filter f v.eq_closure; + ge_closure = SOF.filter f v.ge_closure; + gt_closure = SOF.filter f v.gt_closure; + in_gegt_of = SOF.filter f v.in_gegt_of; + one_s_eq = SOF.filter f v.one_s_eq; + one_s_ge = SOF.filter f v.one_s_ge; + one_s_gt = SOF.filter f v.one_s_gt + } in + MAL.add k v' x ) m' MAL.empty in + let e_l = + 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 + 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) + +let assigner_of = + function + "ge_closure" -> (fun e u->{e with ge_closure=SOF.add u e.ge_closure}) + | "gt_closure" -> (fun e u->{e with gt_closure=SOF.add u e.gt_closure}) + | "eq_closure" -> (fun e u->{e with eq_closure=SOF.add u e.eq_closure}) + | "in_gegt_of" -> (fun e u->{e with in_gegt_of =SOF.add u e.in_gegt_of}) + | "one_s_ge" -> (fun e u->{e with one_s_ge =SOF.add u e.one_s_ge}) + | "one_s_gt" -> (fun e u->{e with one_s_gt =SOF.add u e.one_s_gt}) + | "one_s_eq" -> (fun e u->{e with one_s_eq =SOF.add u e.one_s_eq}) + | s -> raise (Failure ("unsupported tag " ^ s)) +;; -type history_ticket = int +let cb_factory m l = + let module XPP = XmlPushParser in + let current_node = ref (0,None) in + let current_entry = ref empty_entry in + let current_assign = ref (assigner_of "in_gegt_of") in + { XPP.default_callbacks with + XPP.end_element = Some( fun name -> + match name with + | "entry" -> + m := MAL.add !current_node !current_entry !m; + current_entry := empty_entry + | _ -> () + ); + XPP.start_element = Some( fun name attlist -> + match name with + | "ugraph" -> () + | "entry" -> + let id = List.assoc "id" attlist in + let uri = List.assoc "uri" attlist in + current_node := (int_of_string id,Some (UriManager.uri_of_string uri)) + | "node" -> + let id = int_of_string (List.assoc "id" attlist) in + let uri = List.assoc "uri" attlist in + current_entry := !current_assign !current_entry + (id,Some (UriManager.uri_of_string uri)) + | "owned_node" -> + let id = int_of_string (List.assoc "id" attlist) in + let uri = List.assoc "uri" attlist in + l := (id,Some (UriManager.uri_of_string uri)) :: !l + | s -> current_assign := assigner_of s + ) + } +;; + +let ugraph_and_univlist_of_xml filename = + let module XPP = XmlPushParser in + let result_map = ref MAL.empty in + let result_list = ref [] in + let cb = cb_factory result_map result_list in + let xml_parser = XPP.create_parser cb in + 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, !result_list + + +(*****************************************************************************) +(** the main, only for testing **) +(*****************************************************************************) -let get_history_ticket b = - let m,l = b in - List.length l +(* -let redo_history t b b'= - let rec get_history l n = - if n == 0 then - [] +type arc = Ge | Gt | Eq ;; + +let randomize_actionlist n m = + let ge_percent = 0.7 in + let gt_percent = 0.15 in + let random_step () = + let node1 = Random.int m in + let node2 = Random.int m in + let op = + let r = Random.float 1.0 in + if r < ge_percent then + Ge + else (if r < (ge_percent +. gt_percent) then + Gt + else + Eq) + in + op,node1,node2 + in + let rec aux n = + match n with + 0 -> [] + | n -> (random_step ())::(aux (n-1)) + in + aux n + +let print_action_list l = + let string_of_step (op,node1,node2) = + (match op with + Ge -> "Ge" + | Gt -> "Gt" + | Eq -> "Eq") ^ + "," ^ (string_of_int node1) ^ "," ^ (string_of_int node2) + in + let rec aux l = + match l with + [] -> "]" + | a::tl -> + ";" ^ (string_of_step a) ^ (aux tl) + in + let body = aux l in + let l_body = (String.length body) - 1 in + prerr_endline ("[" ^ (String.sub body 1 l_body)) + +let debug = false +let d_print_endline = if debug then print_endline else ignore +let d_print_ugraph = if debug then print_ugraph else ignore + +let _ = + (if Array.length Sys.argv < 2 then + prerr_endline ("Usage " ^ Sys.argv.(0) ^ " max_edges max_nodes")); + Random.self_init (); + let max_edges = int_of_string Sys.argv.(1) in + let max_nodes = int_of_string Sys.argv.(2) in + let action_listR = randomize_actionlist max_edges max_nodes in + + let action_list = [Ge,1,4;Ge,2,6;Ge,1,1;Eq,6,4;Gt,6,3] in + let action_list = action_listR in + + print_action_list action_list; + let prform_step ?(fast=false) (t,u,v) g = + let f,str = + match t with + Ge -> add_ge,">=" + | Gt -> add_gt,">" + | Eq -> add_eq,"=" + in + d_print_endline ( + "Aggiungo " ^ + (string_of_int u) ^ + " " ^ str ^ " " ^ + (string_of_int v)); + let g' = f ~fast (u,None) (v,None) g in + (*print_ugraph g' ;*) + g' + in + let fail = ref false in + let time1 = Unix.gettimeofday () in + let n_safe = ref 0 in + let g_safe = + try + d_print_endline "SAFE"; + List.fold_left ( + fun g e -> + n_safe := !n_safe + 1; + prform_step e g + ) empty_ugraph action_list + with + UniverseInconsistency s -> fail:=true;empty_bag + in + let time2 = Unix.gettimeofday () in + d_print_ugraph g_safe; + let time3 = Unix.gettimeofday () in + let n_test = ref 0 in + let g_test = + try + d_print_endline "FAST"; + List.fold_left ( + fun g e -> + n_test := !n_test + 1; + prform_step ~fast:true e g + ) empty_ugraph action_list + with + UniverseInconsistency s -> empty_bag + in + let time4 = Unix.gettimeofday () in + d_print_ugraph g_test; + if are_ugraph_eq g_safe g_test && !n_test = !n_safe then + begin + let num_eq = + List.fold_left ( + fun s (e,_,_) -> + if e = Eq then s+1 else s + ) 0 action_list + in + let num_gt = + List.fold_left ( + fun s (e,_,_) -> + if e = Gt then s+1 else s + ) 0 action_list + in + let num_ge = max_edges - num_gt - num_eq in + let time_fast = (time4 -. time3) in + let time_safe = (time2 -. time1) in + let gap = ((time_safe -. time_fast) *. 100.0) /. time_safe in + let fail = if !fail then 1 else 0 in + print_endline + (sprintf + "OK %d safe %1.4f fast %1.4f %% %1.2f #eq %d #gt %d #ge %d %d" + fail time_safe time_fast gap num_eq num_gt num_ge !n_safe); + exit 0 + end else begin - match l with - [] -> failwith "erroer, lista piu' corta della history" - | h::tl -> h::(get_history tl (n - 1)) + print_endline "FAIL"; + print_ugraph g_safe; + print_ugraph g_test; + exit 1 end - in - let rec redo_commands l b = - match l with - [] -> b - | (GE,u,v)::tl -> redo_commands tl (add_ge u v b) - | (GT,u,v)::tl -> redo_commands tl (add_gt u v b) - | (EQ,u,v)::tl -> redo_commands tl (add_eq u v b) - in - let (m,l) = b in - let todo = List.rev (get_history l ((List.length l) - t)) in - try - redo_commands todo b' - with - UniverseInconsistency s -> failwith s - (*| _ -> failwith "Unexpected exception"*) - -let add_gt u v = - try - work_bag := add_gt u v !work_bag; true - with - UniverseInconsistency s -> false - (*| _ -> failwith "Unexpected exception"*) - -let add_ge u v = - try - work_bag := add_ge u v !work_bag;true - with - UniverseInconsistency s -> false - (*| _ -> failwith "Unexpected exception"*) +;; -let add_eq u v = - try - work_bag := add_eq u v !work_bag;true - with - UniverseInconsistency s -> false - (*| _ -> failwith "Unexpected exception"*) + *) -let saved_data = ref (empty_bag,0) +let recons_univ u = + match u with + | i, None -> u + | i, Some uri -> + i, Some (UriManager.uri_of_string (UriManager.string_of_uri uri)) -let directly_to_env_begin () = - saved_data := (!work_bag, get_history_ticket !env_bag); - work_bag := empty_bag +let recons_entry entry = + let recons_set set = + SOF.fold (fun univ set -> SOF.add (recons_univ univ) set) set SOF.empty + in + { + eq_closure = recons_set entry.eq_closure; + ge_closure = recons_set entry.ge_closure; + gt_closure = recons_set entry.gt_closure; + in_gegt_of = recons_set entry.in_gegt_of; + one_s_eq = recons_set entry.one_s_eq; + one_s_ge = recons_set entry.one_s_ge; + one_s_gt = recons_set entry.one_s_gt; + } + +let recons_graph graph = + MAL.fold + (fun universe entry map -> + MAL.add (recons_univ universe) (recons_entry entry) map) + graph MAL.empty + +let assert_univ u = + match u with + | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole") + | _ -> () + +let assert_univs_have_uri graph univlist = + let assert_set s = + SOF.iter (fun u -> assert_univ u) s + in + let assert_entry e = + assert_set e.eq_closure; + assert_set e.ge_closure; + assert_set e.gt_closure; + assert_set e.in_gegt_of; + assert_set e.one_s_eq; + assert_set e.one_s_ge; + assert_set e.one_s_gt; + in + MAL.iter (fun k v -> assert_univ k; assert_entry v)graph; + List.iter assert_univ univlist -let directly_to_env_end () = - qed (); - let (b,t) = !saved_data in - work_bag := redo_history t !env_bag b - -let reset_working () = work_bag := empty_bag - -(******************************************************************************) -(** Fake implementatoin **) -(******************************************************************************) - -let reset_working = function _ -> () -let directly_to_env_end = function _ -> () -let directly_to_env_begin = function _ -> () -let add_eq = fun _ _ -> true -let add_ge = fun _ _ -> true -let add_gt = fun _ _ -> true -let get_working = function a -> empty_bag -let set_working = function a -> () +let eq u1 u2 = + match u1,u2 with + | (id1, Some uri1),(id2, Some uri2) -> + id1 = id2 && UriManager.eq uri1 uri2 + | (id1, None),(id2, None) -> id1 = id2 + | _ -> false + +let compare (id1, uri1) (id2, uri2) = + let cmp = id1 - id2 in + if cmp = 0 then + match uri1,uri2 with + | None, None -> 0 + | Some _, None -> 1 + | None, Some _ -> ~-1 + | Some uri1, Some uri2 -> UriManager.compare uri1 uri2 + else + cmp + +(* EOF *)