+++ /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