From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- kernel/univ.ml | 235 ++++++++++++++++++++++++++++----------------------------- 1 file changed, 117 insertions(+), 118 deletions(-) (limited to 'kernel/univ.ml') diff --git a/kernel/univ.ml b/kernel/univ.ml index 763c0822..6c231698 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -270,8 +270,10 @@ module Level = struct let is_small x = match data x with | Level _ -> false - | _ -> true - + | Var _ -> false + | Prop -> true + | Set -> true + let is_prop x = match data x with | Prop -> true @@ -551,6 +553,10 @@ struct | Cons (l, _, Nil) -> Expr.is_level l | _ -> false + let rec is_levels l = match l with + | Cons (l, _, r) -> Expr.is_level l && is_levels r + | Nil -> true + let level l = match l with | Cons (l, _, Nil) -> Expr.level l | _ -> None @@ -577,7 +583,7 @@ struct let is_type0m x = equal type0m x let is_type0 x = equal type0 x - (* Returns the formal universe that lies juste above the universe variable u. + (* Returns the formal universe that lies just above the universe variable u. Used to type the sort u. *) let super l = if is_small l then type1 @@ -655,7 +661,6 @@ type canonical_arc = lt: Level.t list; le: Level.t list; rank : int; - predicative : bool; mutable status : status; (** Guaranteed to be unset out of the [compare_neq] functions. It is used to do an imperative traversal of the graph, ensuring a O(1) check that @@ -670,7 +675,7 @@ let arc_is_lt arc = match arc.status with | Unset | SetLe -> false | SetLt -> true -let terminal u = {univ=u; lt=[]; le=[]; rank=0; predicative=false; status = Unset} +let terminal u = {univ=u; lt=[]; le=[]; rank=0; status = Unset} module UMap : sig @@ -720,35 +725,51 @@ let enter_arc ca g = (* Every Level.t has a unique canonical arc representative *) +(** The graph always contains nodes for Prop and Set. *) + +let terminal_lt u v = + {(terminal u) with lt=[v]} + +let empty_universes = + let g = enter_arc (terminal Level.set) UMap.empty in + let g = enter_arc (terminal_lt Level.prop Level.set) g in + g + (* repr : universes -> Level.t -> canonical_arc *) (* canonical representative : we follow the Equiv links *) -let repr g u = - let rec repr_rec u = - let a = - try UMap.find u g - with Not_found -> anomaly ~label:"Univ.repr" - (str"Universe " ++ Level.pr u ++ str" undefined") - in - match a with - | Equiv v -> repr_rec v - | Canonical arc -> arc +let rec repr g u = + let a = + try UMap.find u g + with Not_found -> anomaly ~label:"Univ.repr" + (str"Universe " ++ Level.pr u ++ str" undefined") in - repr_rec u + match a with + | Equiv v -> repr g v + | Canonical arc -> arc -(* [safe_repr] also search for the canonical representative, but - if the graph doesn't contain the searched universe, we add it. *) +let get_prop_arc g = repr g Level.prop +let get_set_arc g = repr g Level.set +let is_set_arc u = Level.is_set u.univ +let is_prop_arc u = Level.is_prop u.univ -let safe_repr g u = - let rec safe_repr_rec u = - match UMap.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 +exception AlreadyDeclared + +let add_universe vlev strict g = + try + let _arcv = UMap.find vlev g in + raise AlreadyDeclared + with Not_found -> + let v = terminal vlev in + let arc = + let arc = get_set_arc g in + if strict then + { arc with lt=vlev::arc.lt} + else + { arc with le=vlev::arc.le} + in + let g = enter_arc arc g in + enter_arc v g (* reprleq : canonical_arc -> canonical_arc list *) (* All canonical arcv such that arcu<=arcv with arcv#arcu *) @@ -792,7 +813,6 @@ let between g arcu arcv = in let good,_,_ = explore ([arcv],[],false) arcu 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 = [] @@ -903,8 +923,9 @@ let get_explanation strict g arcu arcv = in find [] arc.lt in + let start = (* if is_prop_arc arcu then [Le, make arcv.univ] else *) [] in try - let (to_revert, c) = cmp [] [] [] [(arcu, [])] in + let (to_revert, c) = cmp start [] [] [(arcu, [])] in (** Reset all the touched arcs. *) let () = List.iter (fun arc -> arc.status <- Unset) to_revert in List.rev c @@ -928,25 +949,8 @@ let fast_compare_neq strict g arcu arcv = if arc_is_lt arc then cmp c to_revert lt_todo le_todo else - let rec find lt_todo lt le = match le with - | [] -> - begin match lt with - | [] -> - let () = arc.status <- SetLt in - cmp c (arc :: to_revert) lt_todo le_todo - | u :: lt -> - let arc = repr g u in - if arc == arcv then - if strict then (to_revert, FastLT) else (to_revert, FastLE) - else find (arc :: lt_todo) lt le - end - | u :: le -> - let arc = repr g u in - if arc == arcv then - if strict then (to_revert, FastLT) else (to_revert, FastLE) - else find (arc :: lt_todo) lt le - in - find lt_todo arc.lt arc.le + let () = arc.status <- SetLt in + process_lt c (arc :: to_revert) lt_todo le_todo arc.lt arc.le | [], arc::le_todo -> if arc == arcv then (* No need to continue inspecting universes above arc: @@ -958,22 +962,39 @@ let fast_compare_neq strict g arcu arcv = if arc_is_le arc then cmp c to_revert [] le_todo else - let rec find lt_todo lt = match lt with - | [] -> - let fold accu u = - let node = repr g u in - node :: accu - in - let le_new = List.fold_left fold le_todo arc.le in - let () = arc.status <- SetLe in - cmp c (arc :: to_revert) lt_todo le_new - | u :: lt -> - let arc = repr g u in - if arc == arcv then - if strict then (to_revert, FastLT) else (to_revert, FastLE) - else find (arc :: lt_todo) lt - in - find [] arc.lt + let () = arc.status <- SetLe in + process_le c (arc :: to_revert) [] le_todo arc.lt arc.le + + and process_lt c to_revert lt_todo le_todo lt le = match le with + | [] -> + begin match lt with + | [] -> cmp c to_revert lt_todo le_todo + | u :: lt -> + let arc = repr g u in + if arc == arcv then + if strict then (to_revert, FastLT) else (to_revert, FastLE) + else process_lt c to_revert (arc :: lt_todo) le_todo lt le + end + | u :: le -> + let arc = repr g u in + if arc == arcv then + if strict then (to_revert, FastLT) else (to_revert, FastLE) + else process_lt c to_revert (arc :: lt_todo) le_todo lt le + + and process_le c to_revert lt_todo le_todo lt le = match lt with + | [] -> + let fold accu u = + let node = repr g u in + node :: accu + in + let le_new = List.fold_left fold le_todo le in + cmp c to_revert lt_todo le_new + | u :: lt -> + let arc = repr g u in + if arc == arcv then + if strict then (to_revert, FastLT) else (to_revert, FastLE) + else process_le c to_revert (arc :: lt_todo) le_todo lt le + in try let (to_revert, c) = cmp FastNLE [] [] [arcu] in @@ -1017,24 +1038,18 @@ let is_lt g arcu arcv = (** First, checks on universe levels *) let check_equal g u v = - let g, arcu = safe_repr g u in - let _, arcv = safe_repr g v in - arcu == arcv + let arcu = repr g u and arcv = repr g v in + arcu == arcv let check_eq_level g u v = u == v || check_equal g u v -let is_set_arc u = Level.is_set u.univ -let is_prop_arc u = Level.is_prop u.univ -let get_prop_arc g = snd (safe_repr g Level.prop) - let check_smaller g strict u v = - let g, arcu = safe_repr g u in - let g, arcv = safe_repr g v in + let arcu = repr g u and arcv = repr g v in if strict then is_lt g arcu arcv else is_prop_arc arcu - || (is_set_arc arcu && arcv.predicative) + || (is_set_arc arcu && not (is_prop_arc arcv)) || is_leq g arcu arcv (** Then, checks on universes *) @@ -1076,19 +1091,11 @@ let check_leq g u v = (** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *) -(** To speed up tests of Set Level.t -> reason -> unit *) (* forces u > v *) (* 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 - let g = - if is_set_arc arcu then set_predicative g arcv - else g - in enter_arc arcu' g, arcu' (* checks that non-redundant *) @@ -1102,11 +1109,6 @@ let setlt_if (g,arcu) v = (* 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 - let g = - if is_set_arc arcu' then - set_predicative g arcv - else g - in enter_arc arcu' g, arcu' (* checks that non-redundant *) @@ -1122,7 +1124,8 @@ let merge g arcu arcv = (* we find the arc with the biggest rank, and we redirect all others to it *) let arcu, g, v = let best_ranked (max_rank, old_max_rank, best_arc, rest) arc = - if Level.is_small arc.univ || arc.rank >= max_rank + if Level.is_small arc.univ || + (arc.rank >= max_rank && not (Level.is_small best_arc.univ)) then (arc.rank, max_rank, arc, best_arc::rest) else (max_rank, old_max_rank, best_arc, arc::rest) in @@ -1152,7 +1155,7 @@ let merge g arcu arcv = (* 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 arc1 arc2 = - let arcu, arcv = if arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in + let arcu, arcv = if Level.is_small arc2.univ || arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in let arcu, g = if not (Int.equal arc1.rank arc2.rank) then arcu, g else @@ -1175,12 +1178,11 @@ exception UniverseInconsistency of univ_inconsistency let error_inconsistency o u v (p:explanation option) = raise (UniverseInconsistency (o,make u,make v,p)) -(* enforc_univ_eq : Level.t -> Level.t -> unit *) -(* enforc_univ_eq u v will force u=v if possible, will fail otherwise *) +(* enforce_univ_eq : Level.t -> Level.t -> unit *) +(* enforce_univ_eq u v will force u=v if possible, will fail otherwise *) let enforce_univ_eq u v g = - let g,arcu = safe_repr g u in - let g,arcv = safe_repr g v in + let arcu = repr g u and arcv = repr g v in match fast_compare g arcu arcv with | FastEQ -> g | FastLT -> @@ -1199,8 +1201,7 @@ let enforce_univ_eq u v g = (* enforce_univ_leq : Level.t -> Level.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,arcu = safe_repr g u in - let g,arcv = safe_repr g v in + let arcu = repr g u and arcv = repr g v in if is_leq g arcu arcv then g else match fast_compare g arcv arcu with @@ -1213,8 +1214,7 @@ let enforce_univ_leq u v g = (* enforce_univ_lt u v will force u g | FastLE -> fst (setlt g arcu arcv) @@ -1227,18 +1227,10 @@ let enforce_univ_lt u v g = let p = get_explanation false g arcv arcu in error_inconsistency Lt u v p -let empty_universes = UMap.empty - (* Prop = Set is forbidden here. *) -let initial_universes = enforce_univ_lt Level.prop Level.set UMap.empty +let initial_universes = empty_universes let is_initial_universes g = UMap.equal (==) g initial_universes - -let add_universe vlev g = - let v = terminal vlev in - let proparc = get_prop_arc g in - enter_arc {proparc with le=vlev::proparc.le} - (enter_arc v g) (* Constraints and sets of constraints. *) @@ -1372,10 +1364,12 @@ let check_univ_leq u v = let enforce_leq u v c = let open Universe.Huniv in + let rec aux acc v = match v with - | Cons (v, _, Nil) -> - fold (fun u -> constraint_add_leq u v) u c - | _ -> anomaly (Pp.str"A universe bound can only be a variable") + | Cons (v, _, l) -> + aux (fold (fun u -> constraint_add_leq u v) u c) l + | Nil -> acc + in aux c v let enforce_leq u v c = if check_univ_leq u v then c @@ -1446,7 +1440,6 @@ let normalize_universes g = lt = LSet.elements lt; le = LSet.elements le; rank = rank; - predicative = false; status = Unset; } in @@ -1589,9 +1582,9 @@ let sort_universes orig = let sorted = LMap.fold fold compact UMap.empty in (** Add all [Type.n] nodes *) let fold i accu u = - if 0 < i then - let pred = types.(i - 1) in - let arc = {univ = u; lt = [pred]; le = []; rank = 0; predicative = false; status = Unset; } in + if i < max then + let pred = types.(i + 1) in + let arc = {univ = u; lt = [pred]; le = []; rank = 0; status = Unset; } in UMap.add u (Canonical arc) accu else accu in @@ -1761,7 +1754,7 @@ let eq_puniverses f (x, u) (y, u') = f x y && Instance.equal u u' (** A context of universe levels with universe constraints, - representiong local universe variables and constraints *) + representing local universe variables and constraints *) module UContext = struct @@ -1775,7 +1768,7 @@ struct let pr prl (univs, cst as ctx) = if is_empty ctx then mt() else - Instance.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst) + h 0 (Instance.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) let hcons (univs, cst) = (Instance.hcons univs, hcons_constraints cst) @@ -1785,8 +1778,11 @@ struct let union (univs, cst) (univs', cst') = Instance.append univs univs', Constraint.union cst cst' - + let dest x = x + + let size (x,_) = Instance.length x + end type universe_context = UContext.t @@ -1804,6 +1800,9 @@ struct let empty = (LSet.empty, Constraint.empty) let is_empty (univs, cst) = LSet.is_empty univs && Constraint.is_empty cst + let equal (univs, cst as x) (univs', cst' as y) = + x == y || (LSet.equal univs univs' && Constraint.equal cst cst') + let of_set s = (s, Constraint.empty) let singleton l = of_set (LSet.singleton l) let of_instance i = of_set (Instance.levels i) @@ -1843,7 +1842,7 @@ struct let pr prl (univs, cst as ctx) = if is_empty ctx then mt() else - LSet.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst) + h 0 (LSet.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) let constraints (univs, cst) = cst let levels (univs, cst) = univs -- cgit v1.2.3