From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- kernel/univ.ml | 570 +++++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 408 insertions(+), 162 deletions(-) (limited to 'kernel/univ.ml') diff --git a/kernel/univ.ml b/kernel/univ.ml index 0646a501..a8934544 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1,17 +1,21 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 0 + | Set, _ -> -1 + | _, Set -> 1 + | Level (dp1, i1), Level (dp2, i2) -> + if i1 < i2 then -1 + else if i1 > i2 then 1 + else compare dp1 dp2 + + let to_string = function + | Set -> "Set" + | Level (d,n) -> Names.string_of_dirpath d^"."^string_of_int n +end + +module UniverseLMap = Map.Make (UniverseLevel) +module UniverseLSet = Set.Make (UniverseLevel) + +type universe_level = UniverseLevel.t + +let compare_levels = UniverseLevel.compare (* An algebraic universe [universe] is either a universe variable - [universe_level] or a formal universe known to be greater than some + [UniverseLevel.t] or a formal universe known to be greater than some universe variables and strictly greater than some (other) universe variables @@ -37,38 +70,21 @@ open Util universes inferred while type-checking: it is either the successor of a universe present in the initial term to type-check or the maximum of two algebraic universes - *) - -type universe_level = - | Set - | Level of Names.dir_path * int - -(* A specialized comparison function: we compare the [int] part first. - This way, most of the time, the [dir_path] part is not considered. *) - -let cmp_univ_level u v = match u,v with - | Set, Set -> 0 - | Set, _ -> -1 - | _, Set -> 1 - | Level (dp1,i1), Level (dp2,i2) -> - if i1 < i2 then -1 - else if i1 > i2 then 1 - else compare dp1 dp2 - -let string_of_univ_level = function - | Set -> "Set" - | Level (d,n) -> Names.string_of_dirpath d^"."^string_of_int n - -module UniverseLMap = - Map.Make (struct type t = universe_level let compare = cmp_univ_level end) +*) type universe = - | Atom of universe_level - | Max of universe_level list * universe_level list + | Atom of UniverseLevel.t + | Max of UniverseLevel.t list * UniverseLevel.t list + +let make_universe_level (m,n) = UniverseLevel.Level (m,n) +let make_universe l = Atom l +let make_univ c = Atom (make_universe_level c) -let make_univ (m,n) = Atom (Level (m,n)) +let universe_level = function + | Atom l -> Some l + | Max _ -> None -let pr_uni_level u = str (string_of_univ_level u) +let pr_uni_level u = str (UniverseLevel.to_string u) let pr_uni = function | Atom u -> @@ -97,7 +113,7 @@ let super = function let sup u v = match u,v with | Atom u, Atom v -> - if cmp_univ_level u v = 0 then Atom u else Max ([u;v],[]) + if UniverseLevel.compare u v = 0 then Atom u else Max ([u;v],[]) | u, Max ([],[]) -> u | Max ([],[]), v -> v | Atom u, Max (gel,gtl) -> Max (list_add_set u gel,gtl) @@ -109,16 +125,16 @@ let sup u v = (* Comparison on this type is pointer equality *) type canonical_arc = - { univ: universe_level; lt: universe_level list; le: universe_level list } + { univ: UniverseLevel.t; lt: UniverseLevel.t list; le: UniverseLevel.t list } let terminal u = {univ=u; lt=[]; le=[]} -(* A universe_level is either an alias for another one, or a canonical one, +(* A UniverseLevel.t is either an alias for another one, or a canonical one, for which we know the universes that are above *) type univ_entry = Canonical of canonical_arc - | Equiv of universe_level + | Equiv of UniverseLevel.t type universes = univ_entry UniverseLMap.t @@ -129,12 +145,6 @@ let enter_equiv_arc u v g = let enter_arc ca g = UniverseLMap.add ca.univ (Canonical ca) g -let declare_univ u g = - if not (UniverseLMap.mem u g) then - enter_arc (terminal u) g - else - g - (* The lower predicative level of the hierarchy that contains (impredicative) Prop and singleton inductive types *) let type0m_univ = Max ([],[]) @@ -144,28 +154,30 @@ let is_type0m_univ = function | _ -> false (* The level of predicative Set *) -let type0_univ = Atom Set +let type0_univ = Atom UniverseLevel.Set let is_type0_univ = function - | Atom Set -> true - | Max ([Set],[]) -> warning "Non canonical Set"; true + | Atom UniverseLevel.Set -> true + | Max ([UniverseLevel.Set], []) -> warning "Non canonical Set"; true | u -> false let is_univ_variable = function - | Atom a when a<>Set -> true + | Atom a when a<>UniverseLevel.Set -> true | _ -> false (* When typing [Prop] and [Set], there is no constraint on the level, hence the definition of [type1_univ], the type of [Prop] *) -let type1_univ = Max ([],[Set]) +let type1_univ = Max ([], [UniverseLevel.Set]) let initial_universes = UniverseLMap.empty +let is_initial_universes = UniverseLMap.is_empty -(* Every universe_level has a unique canonical arc representative *) +(* Every UniverseLevel.t has a unique canonical arc representative *) -(* repr : universes -> universe_level -> canonical_arc *) +(* repr : universes -> UniverseLevel.t -> canonical_arc *) (* canonical representative : we follow the Equiv links *) + let repr g u = let rec repr_rec u = let a = @@ -181,6 +193,20 @@ let repr g u = let can g = List.map (repr g) +(* [safe_repr] also search for the canonical representative, but + if the graph doesn't contain the searched universe, we add it. *) + +let safe_repr g u = + let rec safe_repr_rec u = + match UniverseLMap.find u g with + | Equiv v -> safe_repr_rec v + | Canonical arc -> arc + in + try g, safe_repr_rec u + with Not_found -> + let can = terminal u in + enter_arc can g, can + (* reprleq : canonical_arc -> canonical_arc list *) (* All canonical arcv such that arcu<=arcv with arcv#arcu *) let reprleq g arcu = @@ -196,11 +222,11 @@ let reprleq g arcu = searchrec [] arcu.le -(* between : universe_level -> canonical_arc -> canonical_arc list *) +(* between : UniverseLevel.t -> canonical_arc -> canonical_arc list *) (* between u v = {w|u<=w<=v, w canonical} *) (* between is the most costly operation *) -let between g u arcv = +let between g arcu arcv = (* good are all w | u <= w <= v *) (* bad are all w | u <= w ~<= v *) (* find good and bad nodes in {w | u <= w} *) @@ -221,7 +247,7 @@ let between g u arcv = else good, arcu::bad, b (* b or false *) in - let good,_,_ = explore ([arcv],[],false) (repr g u) in + let good,_,_ = explore ([arcv],[],false) arcu in good (* We assume compare(u,v) = LE with v canonical (see compare below). @@ -272,9 +298,7 @@ let compare_neq g arcu arcv = in cmp [] [] ([],[arcu]) -let compare g u v = - let arcu = repr g u - and arcv = repr g v in +let compare g arcu arcv = if arcu == arcv then EQ else compare_neq g arcu arcv (* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ @@ -286,11 +310,12 @@ let compare g u v = Adding u>v is consistent iff compare(v,u) = NLE and then it is redundant iff compare(u,v) = LT *) -let compare_eq g u v = - let g = declare_univ u g in - let g = declare_univ v g in - repr g u == repr g v +(** * Universe checks [check_eq] and [check_geq], used in coqchk *) +let compare_eq g u v = + let g, arcu = safe_repr g u in + let _, arcv = safe_repr g v in + arcu == arcv type check_function = universes -> universe -> universe -> bool @@ -310,10 +335,10 @@ let rec check_eq g u v = | _ -> anomaly "check_eq" (* not complete! (Atom(u) = Max([u],[]) *) let compare_greater g strict u v = - let g = declare_univ u g in - let g = declare_univ v g in - if not strict && compare_eq g v Set then true else - match compare g v u with + let g, arcu = safe_repr g u in + let g, arcv = safe_repr g v in + if not strict && arcv == snd (safe_repr g UniverseLevel.Set) then true else + match compare g arcv arcu with | (EQ|LE) -> not strict | LT -> true | NLE -> false @@ -323,44 +348,50 @@ let compare_greater g strict u v = ppnl(str (if b then if strict then ">" else ">=" else "NOT >=")); b *) -let rec check_greater g strict u v = +let check_geq g u v = match u, v with - | Atom ul, Atom vl -> compare_greater g strict ul vl + | Atom ul, Atom vl -> compare_greater g false ul vl | Atom ul, Max(le,lt) -> - List.for_all (fun vl -> compare_greater g strict ul vl) le && + List.for_all (fun vl -> compare_greater g false ul vl) le && List.for_all (fun vl -> compare_greater g true ul vl) lt | _ -> anomaly "check_greater" -let check_geq g = check_greater g false +(** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *) -(* setlt : universe_level -> universe_level -> unit *) +(* setlt : UniverseLevel.t -> UniverseLevel.t -> unit *) (* forces u > v *) -let setlt g u v = - let arcu = repr g u in - enter_arc {arcu with lt=v::arcu.lt} g +(* this is normally an update of u in g rather than a creation. *) +let setlt g arcu arcv = + let arcu' = {arcu with lt=arcv.univ::arcu.lt} in + enter_arc arcu' g, arcu' (* checks that non-redundant *) -let setlt_if g u v = match compare g u v with - | LT -> g - | _ -> setlt g u v +let setlt_if (g,arcu) v = + let arcv = repr g v in + match compare g arcu arcv with + | LT -> g, arcu + | _ -> setlt g arcu arcv -(* setleq : universe_level -> universe_level -> unit *) +(* setleq : UniverseLevel.t -> UniverseLevel.t -> unit *) (* forces u >= v *) -let setleq g u v = - let arcu = repr g u in - enter_arc {arcu with le=v::arcu.le} g +(* this is normally an update of u in g rather than a creation. *) +let setleq g arcu arcv = + let arcu' = {arcu with le=arcv.univ::arcu.le} in + enter_arc arcu' g, arcu' (* checks that non-redundant *) -let setleq_if g u v = match compare g u v with - | NLE -> setleq g u v - | _ -> g +let setleq_if (g,arcu) v = + let arcv = repr g v in + match compare g arcu arcv with + | NLE -> setleq g arcu arcv + | _ -> g, arcu -(* merge : universe_level -> universe_level -> unit *) +(* merge : UniverseLevel.t -> UniverseLevel.t -> unit *) (* we assume compare(u,v) = LE *) (* merge u v forces u ~ v with repr u as canonical repr *) -let merge g u v = - match between g u (repr g v) with +let merge g arcu arcv = + match between g arcu arcv with | arcu::v -> (* arcu is chosen as canonical and all others (v) are *) (* redirected to it *) let redirect (g,w,w') arcv = @@ -368,87 +399,84 @@ let merge g u v = (g',list_unionq arcv.lt w,arcv.le@w') in let (g',w,w') = List.fold_left redirect (g,[],[]) v in - let g'' = List.fold_left (fun g -> setlt_if g arcu.univ) g' w in - let g''' = List.fold_left (fun g -> setleq_if g arcu.univ) g'' w' in - g''' + let g_arcu = (g',arcu) in + let g_arcu = List.fold_left setlt_if g_arcu w in + let g_arcu = List.fold_left setleq_if g_arcu w' in + fst g_arcu | [] -> anomaly "Univ.between" -(* merge_disc : universe_level -> universe_level -> unit *) +(* merge_disc : UniverseLevel.t -> UniverseLevel.t -> unit *) (* we assume compare(u,v) = compare(v,u) = NLE *) (* merge_disc u v forces u ~ v with repr u as canonical repr *) -let merge_disc g u v = - let arcu = repr g u in - let arcv = repr g v in +let merge_disc g arcu arcv = let g' = enter_equiv_arc arcv.univ arcu.univ g in - let g'' = List.fold_left (fun g -> setlt_if g arcu.univ) g' arcv.lt in - let g''' = List.fold_left (fun g -> setleq_if g arcu.univ) g'' arcv.le in - g''' + let g_arcu = (g',arcu) in + let g_arcu = List.fold_left setlt_if g_arcu arcv.lt in + let g_arcu = List.fold_left setleq_if g_arcu arcv.le in + fst g_arcu (* Universe inconsistency: error raised when trying to enforce a relation that would create a cycle in the graph of universes. *) -type order_request = Lt | Le | Eq +type constraint_type = Lt | Le | Eq -exception UniverseInconsistency of order_request * universe * universe +exception UniverseInconsistency of constraint_type * universe * universe let error_inconsistency o u v = raise (UniverseInconsistency (o,Atom u,Atom v)) -(* enforce_univ_leq : universe_level -> universe_level -> unit *) +(* enforce_univ_leq : UniverseLevel.t -> UniverseLevel.t -> unit *) (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *) let enforce_univ_leq u v g = - let g = declare_univ u g in - let g = declare_univ v g in - match compare g u v with + let g,arcu = safe_repr g u in + let g,arcv = safe_repr g v in + match compare g arcu arcv with | NLE -> - (match compare g v u with + (match compare g arcv arcu with | LT -> error_inconsistency Le u v - | LE -> merge g v u - | NLE -> setleq g u v + | LE -> merge g arcv arcu + | NLE -> fst (setleq g arcu arcv) | EQ -> anomaly "Univ.compare") | _ -> g -(* enforc_univ_eq : universe_level -> universe_level -> unit *) +(* enforc_univ_eq : UniverseLevel.t -> UniverseLevel.t -> unit *) (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *) let enforce_univ_eq u v g = - let g = declare_univ u g in - let g = declare_univ v g in - match compare g u v with + let g,arcu = safe_repr g u in + let g,arcv = safe_repr g v in + match compare g arcu arcv with | EQ -> g | LT -> error_inconsistency Eq u v - | LE -> merge g u v + | LE -> merge g arcu arcv | NLE -> - (match compare g v u with + (match compare g arcv arcu with | LT -> error_inconsistency Eq u v - | LE -> merge g v u - | NLE -> merge_disc g u v + | LE -> merge g arcv arcu + | NLE -> merge_disc g arcu arcv | EQ -> anomaly "Univ.compare") (* enforce_univ_lt u v will force u g - | LE -> setlt g u v + | LE -> fst (setlt g arcu arcv) | EQ -> error_inconsistency Lt u v | NLE -> - (match compare g v u with - | NLE -> setlt g u v + (match compare g arcv arcu with + | NLE -> fst (setlt g arcu arcv) | _ -> error_inconsistency Lt u v) (* Constraints and sets of consrtaints. *) -type constraint_type = Lt | Leq | Eq - -type univ_constraint = universe_level * constraint_type * universe_level +type univ_constraint = UniverseLevel.t * constraint_type * UniverseLevel.t let enforce_constraint cst g = match cst with | (u,Lt,v) -> enforce_univ_lt u v g - | (u,Leq,v) -> enforce_univ_leq u v g + | (u,Le,v) -> enforce_univ_leq u v g | (u,Eq,v) -> enforce_univ_eq u v g - module Constraint = Set.Make( struct type t = univ_constraint @@ -457,11 +485,16 @@ module Constraint = Set.Make( type constraints = Constraint.t +let empty_constraint = Constraint.empty +let is_empty_constraint = Constraint.is_empty + +let union_constraints = Constraint.union + type constraint_function = universe -> universe -> constraints -> constraints let constraint_add_leq v u c = - if v = Set then c else Constraint.add (v,Leq,u) c + if v = UniverseLevel.Set then c else Constraint.add (v,Le,u) c let enforce_geq u v c = match u, v with @@ -479,13 +512,207 @@ let enforce_eq u v c = let merge_constraints c g = Constraint.fold enforce_constraint c g +(* Normalization *) + +let lookup_level u g = + try Some (UniverseLMap.find u g) with Not_found -> None + +(** [normalize_universes g] returns a graph where all edges point + directly to the canonical representent of their target. The output + graph should be equivalent to the input graph from a logical point + of view, but optimized. We maintain the invariant that the key of + a [Canonical] element is its own name, by keeping [Equiv] edges + (see the assertion)... I (Stéphane Glondu) am not sure if this + plays a role in the rest of the module. *) +let normalize_universes g = + let rec visit u arc cache = match lookup_level u cache with + | Some x -> x, cache + | None -> match Lazy.force arc with + | None -> + u, UniverseLMap.add u u cache + | Some (Canonical {univ=v; lt=_; le=_}) -> + v, UniverseLMap.add u v cache + | Some (Equiv v) -> + let v, cache = visit v (lazy (lookup_level v g)) cache in + v, UniverseLMap.add u v cache + in + let cache = UniverseLMap.fold + (fun u arc cache -> snd (visit u (Lazy.lazy_from_val (Some arc)) cache)) + g UniverseLMap.empty + in + let repr x = UniverseLMap.find x cache in + let lrepr us = List.fold_left + (fun e x -> UniverseLSet.add (repr x) e) UniverseLSet.empty us + in + let canonicalize u = function + | Equiv _ -> Equiv (repr u) + | Canonical {univ=v; lt=lt; le=le} -> + assert (u == v); + (* avoid duplicates and self-loops *) + let lt = lrepr lt and le = lrepr le in + let le = UniverseLSet.filter + (fun x -> x != u && not (UniverseLSet.mem x lt)) le + in + UniverseLSet.iter (fun x -> assert (x != u)) lt; + Canonical { + univ = v; + lt = UniverseLSet.elements lt; + le = UniverseLSet.elements le; + } + in + UniverseLMap.mapi canonicalize g + +(** [check_sorted g sorted]: [g] being a universe graph, [sorted] + being a map to levels, checks that all constraints in [g] are + satisfied in [sorted]. *) +let check_sorted g sorted = + let get u = try UniverseLMap.find u sorted with + | Not_found -> assert false + in UniverseLMap.iter (fun u arc -> let lu = get u in match arc with + | Equiv v -> assert (lu = get v) + | Canonical {univ=u'; lt=lt; le=le} -> + assert (u == u'); + List.iter (fun v -> assert (lu <= get v)) le; + List.iter (fun v -> assert (lu < get v)) lt) g + +(** + Bellman-Ford algorithm with a few customizations: + - [weight(eq|le) = 0], [weight(lt) = -1] + - a [le] edge is initially added from [bottom] to all other + vertices, and [bottom] is used as the source vertex +*) +let bellman_ford bottom g = + assert (lookup_level bottom g = None); + let ( << ) a b = match a, b with + | _, None -> true + | None, _ -> false + | Some x, Some y -> x < y + and ( ++ ) a y = match a with + | None -> None + | Some x -> Some (x-y) + and push u x m = match x with + | None -> m + | Some y -> UniverseLMap.add u y m + in + let relax u v uv distances = + let x = lookup_level u distances ++ uv in + if x << lookup_level v distances then push v x distances + else distances + in + let init = UniverseLMap.add bottom 0 UniverseLMap.empty in + let vertices = UniverseLMap.fold (fun u arc res -> + let res = UniverseLSet.add u res in + match arc with + | Equiv e -> UniverseLSet.add e res + | Canonical {univ=univ; lt=lt; le=le} -> + assert (u == univ); + let add res v = UniverseLSet.add v res in + let res = List.fold_left add res le in + let res = List.fold_left add res lt in + res) g UniverseLSet.empty + in + let g = + let node = Canonical { + univ = bottom; + lt = []; + le = UniverseLSet.elements vertices + } in UniverseLMap.add bottom node g + in + let rec iter count accu = + if count <= 0 then + accu + else + let accu = UniverseLMap.fold (fun u arc res -> match arc with + | Equiv e -> relax e u 0 (relax u e 0 res) + | Canonical {univ=univ; lt=lt; le=le} -> + assert (u == univ); + let res = List.fold_left (fun res v -> relax u v 0 res) res le in + let res = List.fold_left (fun res v -> relax u v 1 res) res lt in + res) g accu + in iter (count-1) accu + in + let distances = iter (UniverseLSet.cardinal vertices) init in + let () = UniverseLMap.iter (fun u arc -> + let lu = lookup_level u distances in match arc with + | Equiv v -> + let lv = lookup_level v distances in + assert (not (lu << lv) && not (lv << lu)) + | Canonical {univ=univ; lt=lt; le=le} -> + assert (u == univ); + List.iter (fun v -> assert (not (lu ++ 0 << lookup_level v distances))) le; + List.iter (fun v -> assert (not (lu ++ 1 << lookup_level v distances))) lt) g + in distances + +(** [sort_universes g] builds a map from universes in [g] to natural + numbers. It outputs a graph containing equivalence edges from each + level appearing in [g] to [Type.n], and [lt] edges between the + [Type.n]s. The output graph should imply the input graph (and the + implication will be strict most of the time), but is not + necessarily minimal. Note: the result is unspecified if the input + graph already contains [Type.n] nodes (calling a module Type is + probably a bad idea anyway). *) +let sort_universes orig = + let mp = Names.make_dirpath [Names.id_of_string "Type"] in + let rec make_level accu g i = + let type0 = UniverseLevel.Level (mp, i) in + let distances = bellman_ford type0 g in + let accu, continue = UniverseLMap.fold (fun u x (accu, continue) -> + let continue = continue || x < 0 in + let accu = + if x = 0 && u != type0 then UniverseLMap.add u i accu + else accu + in accu, continue) distances (accu, false) + in + let filter x = not (UniverseLMap.mem x accu) in + let push g u = + if UniverseLMap.mem u g then g else UniverseLMap.add u (Equiv u) g + in + let g = UniverseLMap.fold (fun u arc res -> match arc with + | Equiv v as x -> + begin match filter u, filter v with + | true, true -> UniverseLMap.add u x res + | true, false -> push res u + | false, true -> push res v + | false, false -> res + end + | Canonical {univ=v; lt=lt; le=le} -> + assert (u == v); + if filter u then + let lt = List.filter filter lt in + let le = List.filter filter le in + UniverseLMap.add u (Canonical {univ=u; lt=lt; le=le}) res + else + let res = List.fold_left (fun g u -> if filter u then push g u else g) res lt in + let res = List.fold_left (fun g u -> if filter u then push g u else g) res le in + res) g UniverseLMap.empty + in + if continue then make_level accu g (i+1) else i, accu + in + let max, levels = make_level UniverseLMap.empty orig 0 in + (* defensively check that the result makes sense *) + check_sorted orig levels; + let types = Array.init (max+1) (fun x -> UniverseLevel.Level (mp, x)) in + let g = UniverseLMap.map (fun x -> Equiv types.(x)) levels in + let g = + let rec aux i g = + if i < max then + let u = types.(i) in + let g = UniverseLMap.add u (Canonical { + univ = u; + le = []; + lt = [types.(i+1)] + }) g in aux (i+1) g + else g + in aux 0 g + in g + (**********************************************************************) (* Tools for sort-polymorphic inductive types *) (* Temporary inductive type levels *) let fresh_level = - let n = ref 0 in fun () -> incr n; Level (Names.make_dirpath [],!n) + let n = ref 0 in fun () -> incr n; UniverseLevel.Level (Names.make_dirpath [],!n) let fresh_local_univ () = Atom (fresh_level ()) @@ -559,16 +786,6 @@ let no_upper_constraints u cst = (* Pretty-printing *) -let num_universes g = - UniverseLMap.fold (fun _ _ -> succ) g 0 - -let num_edges g = - let reln_len = function - | Equiv _ -> 1 - | Canonical {lt=lt;le=le} -> List.length lt + List.length le - in - UniverseLMap.fold (fun _ a n -> n + (reln_len a)) g 0 - let pr_arc = function | _, Canonical {univ=u; lt=[]; le=[]} -> mt () @@ -590,7 +807,7 @@ let pr_constraints c = Constraint.fold (fun (u1,op,u2) pp_std -> let op_str = match op with | Lt -> " < " - | Leq -> " <= " + | Le -> " <= " | Eq -> " = " in pp_std ++ pr_uni_level u1 ++ str op_str ++ pr_uni_level u2 ++ fnl () ) c (str "") @@ -600,37 +817,40 @@ let pr_constraints c = let dump_universes output g = let dump_arc u = function | Canonical {univ=u; lt=lt; le=le} -> - let u_str = string_of_univ_level u in - List.iter - (fun v -> - Printf.fprintf output "%s < %s ;\n" u_str - (string_of_univ_level v)) - lt; - List.iter - (fun v -> - Printf.fprintf output "%s <= %s ;\n" u_str - (string_of_univ_level v)) - le + let u_str = UniverseLevel.to_string u in + List.iter (fun v -> output Lt u_str (UniverseLevel.to_string v)) lt; + List.iter (fun v -> output Le u_str (UniverseLevel.to_string v)) le | Equiv v -> - Printf.fprintf output "%s = %s ;\n" - (string_of_univ_level u) (string_of_univ_level v) + output Eq (UniverseLevel.to_string u) (UniverseLevel.to_string v) in UniverseLMap.iter dump_arc g (* Hash-consing *) +module Hunivlevel = + Hashcons.Make( + struct + type t = universe_level + type u = Names.dir_path -> Names.dir_path + let hash_sub hdir = function + | UniverseLevel.Set -> UniverseLevel.Set + | UniverseLevel.Level (d,n) -> UniverseLevel.Level (hdir d,n) + let equal l1 l2 = match l1,l2 with + | UniverseLevel.Set, UniverseLevel.Set -> true + | UniverseLevel.Level (d,n), UniverseLevel.Level (d',n') -> + n == n' && d == d' + | _ -> false + let hash = Hashtbl.hash + end) + module Huniv = Hashcons.Make( struct type t = universe - type u = Names.dir_path -> Names.dir_path - let hash_aux hdir = function - | Set -> Set - | Level (d,n) -> Level (hdir d,n) + type u = universe_level -> universe_level let hash_sub hdir = function - | Atom u -> Atom (hash_aux hdir u) - | Max (gel,gtl) -> - Max (List.map (hash_aux hdir) gel, List.map (hash_aux hdir) gtl) + | Atom u -> Atom (hdir u) + | Max (gel,gtl) -> Max (List.map hdir gel, List.map hdir gtl) let equal u v = match u, v with | Atom u, Atom v -> u == v @@ -641,7 +861,33 @@ module Huniv = let hash = Hashtbl.hash end) -let hcons1_univ u = - let _,_,hdir,_,_,_ = Names.hcons_names() in - Hashcons.simple_hcons Huniv.f hdir u +let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.f Names.hcons_dirpath +let hcons_univ = Hashcons.simple_hcons Huniv.f hcons_univlevel + +module Hconstraint = + Hashcons.Make( + struct + type t = univ_constraint + type u = universe_level -> universe_level + let hash_sub hul (l1,k,l2) = (hul l1, k, hul l2) + let equal (l1,k,l2) (l1',k',l2') = + l1 == l1' && k = k' && l2 == l2' + let hash = Hashtbl.hash + end) + +module Hconstraints = + Hashcons.Make( + struct + type t = constraints + type u = univ_constraint -> univ_constraint + let hash_sub huc s = + Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty + let equal s s' = + list_for_all2eq (==) + (Constraint.elements s) + (Constraint.elements s') + let hash = Hashtbl.hash + end) +let hcons_constraint = Hashcons.simple_hcons Hconstraint.f hcons_univlevel +let hcons_constraints = Hashcons.simple_hcons Hconstraints.f hcons_constraint -- cgit v1.2.3