--- /dev/null
+(* 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 <tassi@cs.unibo.it> *)
+(* 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
+* <--------> *)
projects / helm.git / blobdiff