(* *)
(******************************************************************************)
-(*
+open Printf
- todo:
- - in add_eq there is probably no need of add_gt, simple @ the gt lists
- - the problem of duplicates in the 1steg gt/ge list if two of them are
- add_eq may be "fixed" in some ways:
- - lazy, do nothing on add_eq and eventually update the ge list
- on closure
- - add a check_duplicates_after_eq function called by add_eq
- - do something like rmap, add a list of canonical that point to us
- so when we collapse we have the list of the canonical we may update
- - don't use failure but another exception
-
-*)
+(******************************************************************************)
+(** Types and default values **)
+(******************************************************************************)
-(* ************************************************************************** *)
-(* TYPES *)
-(* ************************************************************************** *)
-type universe = int
-
-type canonical_repr = {
- mutable ge:universe list;
- mutable gt:universe list;
- (* since we collapse we may need the reverse map *)
- mutable eq:universe list;
- (* the canonical representer *)
- u:universe
-}
+type universe = int
module UniverseType = struct
type t = universe
let compare = Pervasives.compare
end
-module MapUC = Map.Make(UniverseType)
+module SOF = Set.Make(UniverseType)
-(* ************************************************************************** *)
-(* Globals *)
-(* ************************************************************************** *)
+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;
+}
-let map = ref MapUC.empty
-let used = ref (-1)
+module MAL = Map.Make(UniverseType)
-(* ************************************************************************** *)
-(* Helpers *)
-(* ************************************************************************** *)
+type arc_type = GE | GT | EQ
-(* create a canonical for [u] *)
-let mk_canonical u =
- {u = u ; gt = [] ; ge = [] ; eq = [u] }
+type arc = arc_type * universe * universe
-(* give a new universe *)
-let fresh () =
- used := !used + 1;
- map := MapUC.add !used (mk_canonical !used) !map;
- !used
-
-let reset () =
- map := MapUC.empty;
- used := -1
+type bag = entry MAL.t * (arc list)
+
+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;
+}
+
+let empty_bag = (MAL.empty, [])
+
+let env_bag = ref empty_bag
+
+(******************************************************************************)
+(** Pretty printings **)
+(******************************************************************************)
+
+let string_of_universe u = string_of_int u
+
+let string_of_arc_type 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) ^ "; "
+;;
+
+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"
-(* ************************************************************************** *)
-(* Pretty printing *)
-(* ************************************************************************** *)
-(* pp *)
-let string_of_universe = string_of_int
-
-(* pp *)
-let canonical_to_string c =
- let s_gt =
- List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.gt in
- let s_ge =
- List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.ge in
- let s_eq =
- List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.eq in
- let s_u = (string_of_universe c.u) in
- "{ u:" ^ s_u ^ " ; gt:" ^ s_gt ^ " ; ge:" ^ s_ge ^ " ; eq: " ^ s_eq ^ "}"
-
-(* print the content of map *)
-let print_map () =
- MapUC.iter (fun u c ->
- prerr_endline
- (" " ^ (string_of_universe u) ^ " -> " ^ (canonical_to_string c)))
- !map;
- prerr_endline ""
-
-(* ************************************************************************** *)
-(* The way we fail *)
-(* ************************************************************************** *)
-(* we are doing bad *)
-let error s =
- (*prerr_endline " ======= Universe Inconsistency =========";
- print_map ();*)
- prerr_endline (" " ^ s ^ "\n");
- failwith s
-
-(* ************************************************************************** *)
-(* The real code *)
-(* ************************************************************************** *)
-(* <--------> *)
-
-(* the canonical representer of the [u] equaliti class *)
-let repr u =
+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;
+ !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
+*)
+let repr u m =
try
- MapUC.find u !map
+ MAL.find u m
with
- Not_found -> error ("map inconsistency, unbound " ^ (string_of_universe u))
-
-(* all the nodes we can ifer in the ge list of u *)
-let close_ge u =
- let repr_u = repr u in
- let rec close_ge_aux tofollow bag =
- match tofollow with
- [] -> bag
- | v::tl -> let repr_v = repr v in
- if List.mem repr_v bag then (* avoid loops *)
- (close_ge_aux tl bag )
- else
- (close_ge_aux (tl @ repr_v.ge) (repr_v::bag))
- (* we assume that v==u -> v \notin (repr u).ge *)
- in
- close_ge_aux repr_u.ge []
+ Not_found ->
+ try
+ let m',_ = !env_bag in
+ MAL.find u m'
+ with
+ Not_found -> empty_entry
+
+(*
+ 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
-(* all the nodes we can ifer in the gt list of u,
- we must follow bot gt and ge arcs, but we must put in bag only
- the nodes that have a gt in theys path
+(******************************************************************************)
+(** Real stuff GT **)
+(******************************************************************************)
+
+(*
+ todo is the SOF of nodes that needs to be recomputed,
+ m is the MAL map, s is the already touched nodes
*)
-let close_gt u =
- let repr_u = repr u in
- let rec close_gt_aux bag todo inspected =
- (*print_all bag todo;Unix.sleep 1;*)
- match todo with
- [],[] -> bag
- | [],p::may -> let repr_p = repr p in
- if List.mem repr_p.u inspected then (* avoid loops *)
- close_gt_aux bag ([],may) inspected
- else
- close_gt_aux bag (repr_p.gt,repr_p.ge @ may)
- (repr_p.u::inspected)
- | s::secure,may -> let repr_s = repr s in
- if List.mem repr_s.u inspected then (* avoid loops *)
- if List.mem repr_s bag then
- close_gt_aux bag (secure,may) inspected
- else
- (* even if we ave already inspected the node, now
- it is in the secure list so we want it in the bag
- *)
- close_gt_aux (repr_s::bag) (secure,may) inspected
- else
- close_gt_aux ((repr_s)::bag)
- (repr_s.gt @ repr_s.ge,may) (repr_s.u::inspected)
- in
- close_gt_aux [] (repr_u.gt,repr_u.ge) []
-
-(* when we add an eq we have to change the mapping of u to c*)
-let remap u c =
- let repr_u = repr u in
- List.iter (fun u' -> if u <> u' then map := MapUC.remove u' !map) repr_u.eq;
- List.iter (fun u' -> map := MapUC.add u' c !map) repr_u.eq
-
-(* we suspect that u and v are connected by a == implyed by two >= *)
-let rec collapse u v =
- let repr_u = repr u in
- let repr_v = repr v in
- let ge_v = close_ge v in
- let ge_u = close_ge u in
- if List.mem repr_u ge_v && List.mem repr_v ge_u then
- add_eq u v
-
-(* we have to add u == v *)
-and add_eq u v =
- let repr_u = repr u in
- let repr_v = repr v in
- (* if we already have u == v then do nothing *)
- if repr_u = repr_v then
- ()
+let rec redo_gt_closure todo m s =
+ if SOF.is_empty todo then m
else
- (* if we already have v > u then fail *)
- let gt_v = close_gt v in
- if List.mem repr_u gt_v then
- error ("Asking for " ^ (string_of_universe u) ^ " == " ^
- (string_of_universe v) ^ " but " ^
- (string_of_universe v) ^ " > " ^ (string_of_universe u))
- else
- (* if we already have u > v then fail *)
- let gt_u = close_gt u in
- if List.mem repr_v gt_u then
- error ("Asking for " ^ (string_of_universe u) ^ " == " ^
- (string_of_universe v) ^ " but " ^
- (string_of_universe u) ^ " > " ^ (string_of_universe v))
- else
- (* add the inherited > constraints *)
- List.iter (fun v -> add_gt u v ) (*gt_v*) repr_v.gt;
- (* add the inherited >= constraints *)
- (* close_ge assumes that v==u -> v \notin (repr u).ge *)
- repr_u.ge <- List.filter (fun x -> x <> u && x <> v)
- (repr_v.ge @ repr_u.ge);
- (* mege the eq list, we assume they are disjuncted *)
- repr_u.eq <- repr_u.eq @ repr_v.eq;
- (* we have to remap all node represented by repr_v to repr_u *)
- remap v repr_u;
- (* FIXME: not sure this is what we have to do
- think more to the list of suspected cicles
- *)
- List.iter (fun x -> collapse u x) repr_u.ge
-
-(* we have to add u >= v *)
-and add_ge u v =
- let repr_u = repr u in
- let repr_v = repr v in
- (* if we already have u == v then do nothing *)
- if repr_u = repr_v then
- ()
- else
- (* if we already have v > u then fail *)
- let gt = close_gt v in
- if List.memq repr_u gt then
- error ("Asking for " ^ (string_of_universe u) ^ " >= " ^
- (string_of_universe v) ^ " but " ^
- (string_of_universe v) ^ " > " ^ (string_of_universe u))
+ 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'
else
- (* it is now safe to add u >= v *)
- repr_u.ge <- v::repr_u.ge;
- (* but we may have introduced a cicle *)
- collapse u v (* FIXME: not sure it is from u to v, think more. *)
-
-(* we have to add u > v *)
-and add_gt u v =
- let repr_u = repr u in
- let repr_v = repr v in
- (* if we already have u == v then fail *)
- if repr_u = repr_v then
- error ("Asking for " ^ (string_of_universe u) ^ " > " ^
- (string_of_universe v) ^ " but " ^
- (string_of_universe u) ^ " == " ^ (string_of_universe v))
- else
- (* if we already have u > v do nothing *)
- let gt_u = close_gt u in
- if List.memq repr_v gt_u then
- ()
+ (* 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
+
+(*
+ 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 =
+ 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 m' = MAL.add u ru' m 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')
+
+(******************************************************************************)
+(** Real stuff GE **)
+(******************************************************************************)
+
+(*
+ 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
else
- (* if we already have v > u then fail *)
- let gt = close_gt v in
- if List.memq repr_u gt then
- error ("Asking for " ^ (string_of_universe u) ^ " > " ^
- (string_of_universe v) ^ " but " ^
- (string_of_universe v) ^ " > " ^ (string_of_universe u))
+ redo_ge_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_ge_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 m' = MAL.add u ru' m 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
+
+(*
+ 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
+
+(*
+ 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')
+
+(******************************************************************************)
+(** Oyther 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" ^
+ " ===== 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 add_eq u v b =
+ (* should we check to no add twice the same?? *)
+ 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
+ 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
+ else
+ add_eq u v b
+ end
+
+let add_ge u v b =
+ (* should we check to no add twice the same?? *)
+ 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
+ else
+ add_ge u v b
+
+let add_gt u v b =
+ (* should we check to no add twice the same?? *)
+ 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
+ else
+ begin
+ if SOF.mem u rv.ge_closure then
+ error (GT,u,v) u GE v rv.ge_closure
else
- (* if we already have v >= u then fail *)
- let ge = close_ge v in
- if List.memq repr_u ge then
- error ("Asking for " ^ (string_of_universe u) ^ " > " ^
- (string_of_universe v) ^ " but " ^
- (string_of_universe v) ^ " >= " ^ (string_of_universe u))
- else
- (* it is safe to add u > v *)
- repr_u.gt <- v::repr_u.gt
+ 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
+
+let fresh () =
+ current_index := !current_index + 1;
+ !current_index
+
+let qed () =
+ qed !work_bag
+
+let print_global_graph () =
+ let s = string_of_bag !env_bag in
+ prerr_endline s
+
+let print_working_graph () =
+ let s = string_of_bag !work_bag in
+ prerr_endline s
+
+type history_ticket = int
+
+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
+ []
+ else
+ begin
+ match l with
+ [] -> failwith "erroer, lista piu' corta della history"
+ | h::tl -> h::(get_history tl (n - 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
- add_gt u v; true
+ work_bag := add_gt u v !work_bag; true
with
- exn -> false
+ UniverseInconsistency s -> false
+ (*| _ -> failwith "Unexpected exception"*)
-let add_ge u v =
+let add_ge u v =
try
- add_ge u v; true
+ work_bag := add_ge u v !work_bag;true
with
- exn -> false
+ UniverseInconsistency s -> false
+ (*| _ -> failwith "Unexpected exception"*)
let add_eq u v =
try
- add_eq u v; true
+ work_bag := add_eq u v !work_bag;true
with
- exn -> false
-
-(* <--------> *)
+ UniverseInconsistency s -> false
+ (*| _ -> failwith "Unexpected exception"*)
-(* ************************************************************************** *)
-(* To make tests *)
-(* ************************************************************************** *)
+let saved_data = ref (empty_bag,0)
-(*
-let check_status_eq l =
- let s = List.fold_left (fun s u -> s^(string_of_universe u) ^ ";") "" l in
- let repr_u = repr (List.hd l) in
- let rec check_status_eq_aux c =
- match c with
- [] -> print_endline (" Result check_status_eq["^s^"] = OK");true
- | u::tl -> if repr u != repr_u then
- (print_endline (" Result check_status_eq["^s^"] = FAILED");
- print_endline ((string_of_universe u) ^ " != " ^
- (string_of_universe repr_u.u));
- print_map ();false)
- else
- check_status_eq_aux tl
- in
- check_status_eq_aux (List.tl l)
-*)
+let directly_to_env_begin () =
+ saved_data := (!work_bag, get_history_ticket !env_bag);
+ work_bag := empty_bag
+
+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 implementation *)
-(* ************************************************************************** *)
+(******************************************************************************)
+(** Fake implementatoin **)
+(******************************************************************************)
-(* <--------> *
-let add_ge u v = true
-let add_gt u v = true
-let add_eq u v = true
-* <--------> *)
+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 -> ()
projects / helm.git / blobdiff