diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-09-11 18:07:39 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:10 +0200 |
commit | e759333a8b5c11247c4cc134fdde8c1bd85a6e17 (patch) | |
tree | 8eb43cf88b6d2367bb856f46b2a471af583e73db /kernel | |
parent | 88abc50ece70405d71777d5350ca2fa70c1ff437 (diff) |
Universes: enforce Set <= i for all Type occurrences.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/indtypes.ml | 5 | ||||
-rw-r--r-- | kernel/univ.ml | 71 | ||||
-rw-r--r-- | kernel/univ.mli | 10 |
3 files changed, 56 insertions, 30 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 8c89abe94..9c065101a 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -286,7 +286,10 @@ let typecheck_inductive env mie = let defu = Term.univ_of_sort def_level in let is_natural = type_in_type env || (check_leq (universes env') infu defu && - not (is_type0m_univ defu && not is_unit)) + not (is_type0m_univ defu && not is_unit) + (* (~ is_type0m_univ defu \/ is_unit) (\* infu <= defu && not prop or unital *\) *) + + ) in let _ = (** Impredicative sort, always allow *) diff --git a/kernel/univ.ml b/kernel/univ.ml index 336cdb653..040e9bc27 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 @@ -670,7 +672,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 ?(predicative=false) u = {univ=u; lt=[]; le=[]; rank=0; predicative; status = Unset} module UMap : sig @@ -720,6 +722,16 @@ 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 ~predicative:true 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 *) @@ -733,6 +745,22 @@ let rec repr g u = | Equiv v -> repr g v | Canonical arc -> arc +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 add_universe vlev ~predicative g = + let v = terminal ~predicative vlev in + let arc = + let arc = + if predicative then get_set_arc g else get_prop_arc g + in + { arc with le=vlev::arc.le} + in + let g = enter_arc arc g in + enter_arc v g + (* [safe_repr] also search for the canonical representative, but if the graph doesn't contain the searched universe, we add it. *) @@ -745,6 +773,8 @@ let safe_repr g u = try g, safe_repr_rec g u with Not_found -> let can = terminal u in + let setarc = get_set_arc g in + let g = enter_arc {setarc with le=u::setarc.le} g in enter_arc can g, can (* reprleq : canonical_arc -> canonical_arc list *) @@ -789,7 +819,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 = [] @@ -900,8 +929,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 @@ -972,7 +1002,6 @@ let fast_compare_neq strict g arcu arcv = else process_le c to_revert (arc :: lt_todo) le_todo lt le in - try let (to_revert, c) = cmp FastNLE [] [] [arcu] in (** Reset all the touched arcs. *) @@ -1021,10 +1050,6 @@ let check_equal g u v = 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 @@ -1120,7 +1145,7 @@ 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 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 @@ -1150,7 +1175,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 @@ -1173,8 +1198,8 @@ 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 @@ -1225,18 +1250,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. *) @@ -1370,10 +1387,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 diff --git a/kernel/univ.mli b/kernel/univ.mli index 7aaf2ffe6..76453cbb0 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -20,7 +20,11 @@ sig val is_small : t -> bool (** Is the universe set or prop? *) - + + val is_prop : t -> bool + val is_set : t -> bool + (** Is it specifically Prop or Set *) + val compare : t -> t -> int (** Comparison function *) @@ -159,8 +163,8 @@ val is_initial_universes : universes -> bool val sort_universes : universes -> universes -(** Adds a universe to the graph, ensuring it is >= Prop. *) -val add_universe : universe_level -> universes -> universes +(** Adds a universe to the graph, ensuring it is >= Prop or Set. *) +val add_universe : universe_level -> predicative:bool -> universes -> universes (** {6 Constraints. } *) |