X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicUniv.ml;h=05e0a99a1e9f7435902328ce7f988d06894f1cdc;hb=0c6a5aadb1a7746681a8e26fc0b009f847c10557;hp=d76fde47a535c3582f26e81e26ef57e0c0a96ca1;hpb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;p=helm.git diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml index d76fde47a..05e0a99a1 100644 --- a/helm/ocaml/cic/cicUniv.ml +++ b/helm/ocaml/cic/cicUniv.ml @@ -34,312 +34,508 @@ (* *) (******************************************************************************) -(* +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 -> ()