From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- kernel/univ.ml | 171 ++++++++++++++++++++++++++++----------------------------- 1 file changed, 84 insertions(+), 87 deletions(-) (limited to 'kernel/univ.ml') diff --git a/kernel/univ.ml b/kernel/univ.ml index 3d254ce6..16544eca 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: univ.ml 11596 2008-11-16 15:34:06Z letouzey $ *) +(* $Id$ *) (* Initial Caml version originates from CoC 4.8 [Dec 1988] *) (* Extension with algebraic universes by HH [Sep 2001] *) @@ -55,40 +55,38 @@ let cmp_univ_level u v = match u,v with 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 - -module UniverseOrdered = struct - type t = universe_level - let compare = cmp_univ_level -end - -let string_of_univ_level = function - | Set -> "0" - | Level (d,n) -> Names.string_of_dirpath d^"."^string_of_int n let make_univ (m,n) = Atom (Level (m,n)) let pr_uni_level u = str (string_of_univ_level u) let pr_uni = function - | Atom u -> + | Atom u -> pr_uni_level u | Max ([],[u]) -> str "(" ++ pr_uni_level u ++ str ")+1" | Max (gel,gtl) -> str "max(" ++ hov 0 - (prlist_with_sep pr_coma pr_uni_level gel ++ - (if gel <> [] & gtl <> [] then pr_coma () else mt ()) ++ - prlist_with_sep pr_coma + (prlist_with_sep pr_comma pr_uni_level gel ++ + (if gel <> [] & gtl <> [] then pr_comma () else mt ()) ++ + prlist_with_sep pr_comma (fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl) ++ str ")" (* Returns the formal universe that lies juste above the universe variable u. Used to type the sort u. *) let super = function - | Atom u -> + | Atom u -> Max ([],[u]) | Max _ -> anomaly ("Cannot take the successor of a non variable universe:\n"^ @@ -121,18 +119,17 @@ type univ_entry = Canonical of canonical_arc | Equiv of universe_level * universe_level -module UniverseMap = Map.Make(UniverseOrdered) -type universes = univ_entry UniverseMap.t - +type universes = univ_entry UniverseLMap.t + let enter_equiv_arc u v g = - UniverseMap.add u (Equiv(u,v)) g + UniverseLMap.add u (Equiv(u,v)) g let enter_arc ca g = - UniverseMap.add ca.univ (Canonical ca) g + UniverseLMap.add ca.univ (Canonical ca) g let declare_univ u g = - if not (UniverseMap.mem u g) then + if not (UniverseLMap.mem u g) then enter_arc (terminal u) g else g @@ -162,20 +159,20 @@ let is_univ_variable = function let type1_univ = Max ([],[Set]) -let initial_universes = UniverseMap.empty +let initial_universes = UniverseLMap.empty (* Every universe_level has a unique canonical arc representative *) (* repr : universes -> universe_level -> canonical_arc *) (* canonical representative : we follow the Equiv links *) -let repr g u = +let repr g u = let rec repr_rec u = let a = - try UniverseMap.find u g + try UniverseLMap.find u g with Not_found -> anomalylabstrm "Univ.repr" - (str"Universe " ++ pr_uni_level u ++ str" undefined") + (str"Universe " ++ pr_uni_level u ++ str" undefined") in - match a with + match a with | Equiv(_,v) -> repr_rec v | Canonical arc -> arc in @@ -192,16 +189,16 @@ let collect g arcu = let rec coll_rec lt le = function | [],[] -> (lt, list_subtractq le lt) | arcv::lt', le' -> - if List.memq arcv lt then + if List.memq arcv lt then coll_rec lt le (lt',le') else coll_rec (arcv::lt) le ((can g (arcv.lt@arcv.le))@lt',le') - | [], arcw::le' -> - if (List.memq arcw lt) or (List.memq arcw le) then + | [], arcw::le' -> + if (List.memq arcw lt) or (List.memq arcw le) then coll_rec lt le ([],le') else coll_rec lt (arcw::le) (can g arcw.lt, (can g arcw.le)@le') - in + in coll_rec [] [] ([],[arcu]) (* reprleq : canonical_arc -> canonical_arc list *) @@ -211,19 +208,19 @@ let reprleq g arcu = | [] -> w | v :: vl -> let arcv = repr g v in - if List.memq arcv w || arcu==arcv then + if List.memq arcv w || arcu==arcv then searchrec w vl - else + else searchrec (arcv :: w) vl - in + in searchrec [] arcu.le (* between : universe_level -> canonical_arc -> canonical_arc list *) -(* between u v = {w|u<=w<=v, w canonical} *) +(* between u v = {w|u<=w<=v, w canonical} *) (* between is the most costly operation *) -let between g u arcv = +let between g u arcv = (* good are all w | u <= w <= v *) (* bad are all w | u <= w ~<= v *) (* find good and bad nodes in {w | u <= w} *) @@ -233,50 +230,50 @@ let between g u arcv = (good, bad, true) (* b or true *) else if List.memq arcu bad then input (* (good, bad, b or false) *) - else - let leq = reprleq g arcu in + else + let leq = reprleq g arcu in (* is some universe >= u good ? *) - let good, bad, b_leq = + let good, bad, b_leq = List.fold_left explore (good, bad, false) leq in if b_leq then arcu::good, bad, true (* b or true *) - else + else good, arcu::bad, b (* b or false *) in let good,_,_ = explore ([arcv],[],false) (repr g u) in good - + (* We assume compare(u,v) = LE with v canonical (see compare below). In this case List.hd(between g u v) = repr u - Otherwise, between g u v = [] + Otherwise, between g u v = [] *) type order = EQ | LT | LE | NLE (* compare : universe_level -> universe_level -> order *) -let compare g u v = - let arcu = repr g u +let compare g u v = + let arcu = repr g u and arcv = repr g v in - if arcu==arcv then + if arcu==arcv then EQ - else + else let (lt,leq) = collect g arcu in - if List.memq arcv lt then + if List.memq arcv lt then LT - else if List.memq arcv leq then + else if List.memq arcv leq then LE - else + else NLE (* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ compare(u,v) = LT or LE => compare(v,u) = NLE compare(u,v) = NLE => compare(v,u) = NLE or LE or LT - Adding u>=v is consistent iff compare(v,u) # LT + Adding u>=v is consistent iff compare(v,u) # LT and then it is redundant iff compare(u,v) # NLE - Adding u>v is consistent iff compare(v,u) = NLE + 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 = @@ -288,7 +285,7 @@ let compare_eq g u v = type check_function = universes -> universe -> universe -> bool let incl_list cmp l1 l2 = - List.for_all (fun x1 -> List.exists (fun x2 -> cmp x1 x2) l2) l1 + List.for_all (fun x1 -> List.exists (fun x2 -> cmp x1 x2) l2) l1 let compare_list cmp l1 l2 = incl_list cmp l1 l2 && incl_list cmp l2 l1 @@ -361,7 +358,7 @@ let merge g u v = (* redirected to it *) let redirect (g,w,w') arcv = let g' = enter_equiv_arc arcv.univ arcu.univ g in - (g',list_unionq arcv.lt w,arcv.le@w') + (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 @@ -395,7 +392,7 @@ 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 - | NLE -> + | NLE -> (match compare g v u with | LT -> error_inconsistency Le u v | LE -> merge g v u @@ -412,7 +409,7 @@ let enforce_univ_eq u v g = | EQ -> g | LT -> error_inconsistency Eq u v | LE -> merge g u v - | NLE -> + | NLE -> (match compare g v u with | LT -> error_inconsistency Eq u v | LE -> merge g v u @@ -427,13 +424,13 @@ let enforce_univ_lt u v g = | LT -> g | LE -> setlt g u v | EQ -> error_inconsistency Lt u v - | NLE -> + | NLE -> (match compare g v u with | NLE -> setlt g u v | _ -> error_inconsistency Lt u v) (* -let enforce_univ_relation g = function +let enforce_univ_relation g = function | Equiv (u,v) -> enforce_univ_eq u v g | Canonical {univ=u; lt=lt; le=le} -> let g' = List.fold_right (enforce_univ_lt u) lt g in @@ -443,7 +440,7 @@ let enforce_univ_relation g = function (* Merging 2 universe graphs *) (* let merge_universes sp u1 u2 = - UniverseMap.fold (fun _ a g -> enforce_univ_relation g a) u1 u2 + UniverseLMap.fold (fun _ a g -> enforce_univ_relation g a) u1 u2 *) @@ -461,14 +458,14 @@ let enforce_constraint cst g = module Constraint = Set.Make( - struct - type t = univ_constraint - let compare = Pervasives.compare + struct + type t = univ_constraint + let compare = Pervasives.compare end) - + type constraints = Constraint.t -type constraint_function = +type constraint_function = universe -> universe -> constraints -> constraints let constraint_add_leq v u c = @@ -515,17 +512,17 @@ let is_direct_constraint u = function | Atom u' -> u = u' | Max (le,lt) -> List.mem u le -(* +(* Solve a system of universe constraint of the form u_s11, ..., u_s1p1, w1 <= u1 ... u_sn1, ..., u_snpn, wn <= un -where +where - the ui (1 <= i <= n) are universe variables, - - the sjk select subsets of the ui for each equations, + - the sjk select subsets of the ui for each equations, - the wi are arbitrary complex universes that do not mention the ui. *) @@ -534,7 +531,7 @@ let is_direct_sort_constraint s v = match s with | None -> false let solve_constraints_system levels level_bounds = - let levels = + let levels = Array.map (Option.map (function Atom u -> u | _ -> anomaly "expects Atom")) levels in let v = Array.copy level_bounds in @@ -553,7 +550,7 @@ let solve_constraints_system levels level_bounds = v let subst_large_constraint u u' v = - match u with + match u with | Atom u -> if is_direct_constraint u v then sup u' (remove_large_constraint u v) else v @@ -571,16 +568,16 @@ let no_upper_constraints u cst = (* Pretty-printing *) let num_universes g = - UniverseMap.fold (fun _ _ -> succ) g 0 + 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 - UniverseMap.fold (fun _ a n -> n + (reln_len a)) g 0 - -let pr_arc = function + UniverseLMap.fold (fun _ a n -> n + (reln_len a)) g 0 + +let pr_arc = function | Canonical {univ=u; lt=[]; le=[]} -> mt () | Canonical {univ=u; lt=lt; le=le} -> @@ -590,43 +587,43 @@ let pr_arc = function (if lt <> [] & le <> [] then spc () else mt()) ++ prlist_with_sep pr_spc (fun v -> str "<= " ++ pr_uni_level v) le) ++ fnl () - | Equiv (u,v) -> + | Equiv (u,v) -> pr_uni_level u ++ str " = " ++ pr_uni_level v ++ fnl () let pr_universes g = - let graph = UniverseMap.fold (fun k a l -> (k,a)::l) g [] in + let graph = UniverseLMap.fold (fun k a l -> (k,a)::l) g [] in prlist (function (_,a) -> pr_arc a) graph - + let pr_constraints c = - Constraint.fold (fun (u1,op,u2) pp_std -> - let op_str = match op with + Constraint.fold (fun (u1,op,u2) pp_std -> + let op_str = match op with | Lt -> " < " | Leq -> " <= " | Eq -> " = " in pp_std ++ pr_uni_level u1 ++ str op_str ++ pr_uni_level u2 ++ fnl () ) c (str "") - -(* Dumping constrains to a file *) -let dump_universes output g = +(* Dumping constraints to a file *) + +let dump_universes output g = let dump_arc _ = function - | Canonical {univ=u; lt=lt; le=le} -> + | Canonical {univ=u; lt=lt; le=le} -> let u_str = string_of_univ_level u in - List.iter - (fun v -> + List.iter + (fun v -> Printf.fprintf output "%s < %s ;\n" u_str - (string_of_univ_level v)) + (string_of_univ_level v)) lt; - List.iter - (fun v -> + List.iter + (fun v -> Printf.fprintf output "%s <= %s ;\n" u_str - (string_of_univ_level v)) + (string_of_univ_level v)) le | Equiv (u,v) -> Printf.fprintf output "%s = %s ;\n" (string_of_univ_level u) (string_of_univ_level v) in - UniverseMap.iter dump_arc g + UniverseLMap.iter dump_arc g (* Hash-consing *) -- cgit v1.2.3