From 15999903f875f4b5dbb3d5240d2ca39acc3cd777 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 26 May 2014 13:58:56 +0200 Subject: - Fix in kernel conversion not folding the universe constraints correctly when comparing stacks. - Disallow Type i <= Prop/Set constraints, that would otherwise allow constraints that make a universe lower than Prop. - Fix stm/lemmas that was pushing constraints to the global context, it is done depending on the constant/variable polymorphic status now. - Adapt generalized rewriting in Type code to these fixes. --- kernel/reduction.ml | 58 ++++++++++++----------------------------------------- kernel/univ.ml | 47 ++++++++++++++++++++++++------------------- 2 files changed, 39 insertions(+), 66 deletions(-) (limited to 'kernel') diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 8773f4f34..a820e337e 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -221,47 +221,23 @@ type conv_pb = let is_cumul = function CUMUL -> true | CONV -> false let is_pos = function Pos -> true | Null -> false -(* let sort_cmp env pb s0 s1 cuniv = *) -(* match (s0,s1) with *) -(* | (Prop c1, Prop c2) when is_cumul pb -> *) -(* begin match c1, c2 with *) -(* | Null, _ | _, Pos -> cuniv (\* Prop <= Set *\) *) -(* | _ -> raise NotConvertible *) -(* end *) -(* | (Prop c1, Prop c2) -> *) -(* if c1 == c2 then cuniv else raise NotConvertible *) -(* | (Prop c1, Type u) when is_cumul pb -> *) -(* enforce_leq (if is_pos c1 then Universe.type0 else Universe.type0m) u cuniv *) -(* | (Type u, Prop c) when is_cumul pb -> *) -(* enforce_leq u (if is_pos c then Universe.type0 else Universe.type0m) cuniv *) -(* | (Type u1, Type u2) -> *) -(* (match pb with *) -(* | CONV -> Univ.enforce_eq u1 u2 cuniv *) -(* | CUMUL -> enforce_leq u1 u2 cuniv) *) -(* | (_, _) -> raise NotConvertible *) - -(* let conv_sort env s0 s1 = sort_cmp CONV s0 s1 Constraint.empty *) -(* let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 Constraint.empty *) - let check_eq (univs, cstrs as cuniv) u u' = match cstrs with | None -> if check_eq univs u u' then cuniv else raise NotConvertible | Some cstrs -> univs, Some (Univ.enforce_eq u u' cstrs) - (* let cstr = Univ.enforce_eq u u' Univ.Constraint.empty in *) - (* try let univs' = Univ.enforce_constraint cstr univs in *) - (* univs', Some (Univ.enforce_eq u u' cstrs) *) - (* with UniverseInconsistency _ -> raise NotConvertible *) -let check_leq (univs, cstrs as cuniv) u u' = +let check_leq ?(record=false) (univs, cstrs as cuniv) u u' = match cstrs with | None -> if check_leq univs u u' then cuniv else raise NotConvertible | Some cstrs -> - univs, Some (Univ.enforce_leq u u' cstrs) - (* let cstr = Univ.enforce_leq u u' Univ.Constraint.empty in *) - (* try let univs' = Univ.enforce_constraint cstr univs in *) - (* univs', Some (Univ.enforce_leq u u' cstrs) *) - (* with UniverseInconsistency _ -> raise NotConvertible *) + let cstrs' = Univ.enforce_leq u u' cstrs in + let cstrs' = if record then + Univ.Constraint.add (Option.get (Univ.Universe.level u),Univ.Le, + Option.get (Univ.Universe.level u')) cstrs' + else cstrs' + in + univs, Some cstrs' let sort_cmp_universes pb s0 s1 univs = match (s0,s1) with @@ -274,23 +250,14 @@ let sort_cmp_universes pb s0 s1 univs = | (Prop c1, Type u) -> let u0 = univ_of_sort s0 in (match pb with - | CUMUL -> check_leq univs u0 u + | CUMUL -> check_leq ~record:true univs u0 u | CONV -> check_eq univs u0 u) - | (Type u, Prop c) -> - let u1 = univ_of_sort s1 in - (match pb with - | CUMUL -> check_leq univs u u1 - | CONV -> check_eq univs u u1) + | (Type u, Prop c) -> raise NotConvertible | (Type u1, Type u2) -> (match pb with | CUMUL -> check_leq univs u1 u2 | CONV -> check_eq univs u1 u2) -(* let sort_cmp _ _ _ cuniv = cuniv *) - -(* let conv_sort env s0 s1 = sort_cmp CONV s0 s1 empty_constraint *) -(* let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 empty_constraint *) - let rec no_arg_available = function | [] -> true | Zupdate _ :: stk -> no_arg_available stk @@ -594,7 +561,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = compare_stacks - (fun (l1,t1) (l2,t2) c -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv) + (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv) (eq_ind) lft1 stk1 lft2 stk2 cuniv @@ -665,7 +632,8 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2 else Constr.eq_constr_univs_infer univs t1 t2 in - if b && Univ.check_constraints cstrs univs then cstrs + if b && (try ignore(Univ.merge_constraints cstrs univs); true with _ -> false) then + cstrs else let (u, cstrs) = clos_fconv reds cv_pb l2r evars env (univs, Some Constraint.empty) t1 t2 diff --git a/kernel/univ.ml b/kernel/univ.ml index 8a48eb5db..7ab0aa93c 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1341,7 +1341,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 arc.rank >= max_rank + if Level.is_small arc.univ || arc.rank >= max_rank then (arc.rank, max_rank, arc, best_arc::rest) else (max_rank, old_max_rank, best_arc, arc::rest) in @@ -1394,27 +1394,13 @@ exception UniverseInconsistency of univ_inconsistency let error_inconsistency o u v (p:explanation) = raise (UniverseInconsistency (o,make u,make v,p)) -(* 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 - if is_leq g arcu arcv then g - else match fast_compare g arcv arcu with - | FastLT -> - (match compare g arcv arcu with - | LT p -> error_inconsistency Le u v (List.rev (Lazy.force p)) - | _ -> anomaly (Pp.str "Univ.fast_compare")) - | FastLE -> merge g arcv arcu - | FastNLE -> fst (setleq g arcu arcv) - | FastEQ -> anomaly (Pp.str "Univ.compare") - (* enforc_univ_eq : Level.t -> Level.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,arcu = safe_repr g u in let g,arcv = safe_repr g v in - match fast_compare g arcu arcv with + match fast_compare g arcu arcv with | FastEQ -> g | FastLT -> (match compare g arcu arcv with @@ -1431,11 +1417,27 @@ let enforce_univ_eq u v g = | FastNLE -> merge_disc g arcu arcv | FastEQ -> anomaly (Pp.str "Univ.compare")) +(* 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 + if is_leq g arcu arcv then g + else + match fast_compare g arcv arcu with + | FastLT -> + (match compare g arcv arcu with + | LT p -> error_inconsistency Le u v (List.rev (Lazy.force p)) + | _ -> anomaly (Pp.str "Univ.fast_compare")) + | FastLE -> merge g arcv arcu + | FastNLE -> fst (setleq g arcu arcv) + | FastEQ -> anomaly (Pp.str "Univ.compare") + (* enforce_univ_lt u v will force u g | FastLE -> fst (setlt g arcu arcv) | FastEQ -> @@ -1452,7 +1454,10 @@ let enforce_univ_lt u v g = | _ -> anomaly (Pp.str "Univ.fast_compare")) let empty_universes = LMap.empty -let initial_universes = enforce_univ_leq Level.prop Level.set LMap.empty + +(* Prop = Set is forbidden here. *) +let initial_universes = enforce_univ_lt Level.prop Level.set LMap.empty + let is_initial_universes g = LMap.equal (==) g initial_universes (* Constraints and sets of constraints. *) @@ -2176,7 +2181,7 @@ let normalize_universes g = univ = v; lt = LSet.elements lt; le = LSet.elements le; - rank = rank + rank = rank; } in LMap.mapi canonicalize g @@ -2321,7 +2326,7 @@ let sort_universes orig = let fold i accu u = if 0 < i then let pred = types.(i - 1) in - let arc = {univ = u; lt = [pred]; le = []; rank = 0; } in + let arc = {univ = u; lt = [pred]; le = []; rank = 0} in LMap.add u (Canonical arc) accu else accu in -- cgit v1.2.3