(* Copyright (C) 2000, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://cs.unibo.it/helm/. *) (******************************************************************************) (* *) (* PROJECT HELM *) (* *) (* Enrico Tassi *) (* 23/04/2004 *) (* *) (* This module implements the aciclic graph of universes. *) (* *) (******************************************************************************) (* 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 *) (* ************************************************************************** *) 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 } module UniverseType = struct type t = universe let compare = Pervasives.compare end module MapUC = Map.Make(UniverseType) (* ************************************************************************** *) (* Globals *) (* ************************************************************************** *) let map = ref MapUC.empty let used = ref (-1) (* ************************************************************************** *) (* Helpers *) (* ************************************************************************** *) (* create a canonical for [u] *) let mk_canonical u = {u = u ; gt = [] ; ge = [] ; eq = [u] } (* 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 (* ************************************************************************** *) (* 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 = try MapUC.find u !map 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 [] (* 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 *) 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 () 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)) 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 () 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)) 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 let add_gt u v = try add_gt u v; true with exn -> false let add_ge u v = try add_ge u v; true with exn -> false let add_eq u v = try add_eq u v; true with exn -> false (* <--------> *) (* ************************************************************************** *) (* To make tests *) (* ************************************************************************** *) (* 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) *) (* ************************************************************************** *) (* Fake implementation *) (* ************************************************************************** *) (* <--------> * let add_ge u v = true let add_gt u v = true let add_eq u v = true * <--------> *)