diff options
| -rw-r--r-- | engine/evd.ml | 5 | ||||
| -rw-r--r-- | engine/evd.mli | 4 | ||||
| -rw-r--r-- | engine/uState.ml | 13 | ||||
| -rw-r--r-- | engine/uState.mli | 9 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5365.v | 13 | ||||
| -rw-r--r-- | toplevel/command.ml | 2 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 |
8 files changed, 39 insertions, 11 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index c2f848291..ac31728f4 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -809,8 +809,9 @@ let new_sort_variable ?loc ?name rigid d = let add_global_univ d u = { d with universes = UState.add_global_univ d.universes u } -let make_flexible_variable evd b u = - { evd with universes = UState.make_flexible_variable evd.universes b u } +let make_flexible_variable evd ~algebraic u = + { evd with universes = + UState.make_flexible_variable evd.universes ~algebraic u } let make_evar_universe_context e l = let uctx = UState.make (Environ.universes e) in diff --git a/engine/evd.mli b/engine/evd.mli index 86887f3dc..93d4a9d15 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -526,7 +526,9 @@ val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_ val add_global_univ : evar_map -> Univ.Level.t -> evar_map val universe_rigidity : evar_map -> Univ.Level.t -> rigid -val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map +val make_flexible_variable : evar_map -> algebraic:bool -> Univ.universe_level -> evar_map +(** See [UState.make_flexible_variable] *) + val is_sort_variable : evar_map -> sorts -> Univ.universe_level option (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is not a local sort variable declared in [evm] *) diff --git a/engine/uState.ml b/engine/uState.ml index c35f97b2e..146a386a2 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -381,16 +381,21 @@ let add_global_univ uctx u = uctx_initial_universes = initial; uctx_universes = univs } -let make_flexible_variable ctx b u = - let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in +let make_flexible_variable ctx ~algebraic u = + let {uctx_local = cstrs; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in let uvars' = Univ.LMap.add u None uvars in let avars' = - if b then + if algebraic then let uu = Univ.Universe.make u in let substu_not_alg u' v = Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v in - if not (Univ.LMap.exists substu_not_alg uvars) + let has_upper_constraint () = + Univ.Constraint.exists + (fun (l,d,r) -> d == Univ.Lt && Univ.Level.equal l u) + (Univ.ContextSet.constraints cstrs) + in + if not (Univ.LMap.exists substu_not_alg uvars || has_upper_constraint ()) then Univ.LSet.add u avars else avars else avars in diff --git a/engine/uState.mli b/engine/uState.mli index 0cdc6277a..3776e4c9f 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -92,7 +92,14 @@ val emit_side_effects : Safe_typing.private_constants -> t -> t val new_univ_variable : ?loc:Loc.t -> rigid -> string option -> t -> t * Univ.Level.t val add_global_univ : t -> Univ.Level.t -> t -val make_flexible_variable : t -> bool -> Univ.Level.t -> t + +(** [make_flexible_variable g algebraic l] + + Turn the variable [l] flexible, and algebraic if [algebraic] is true + and [l] can be. That is if there are no strict upper constraints on + [l] and and it does not appear in the instance of any non-algebraic + universe. Otherwise the variable is just made flexible. *) +val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t val is_sort_variable : t -> Sorts.t -> Univ.Level.t option diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4fd030845..e8380136e 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -67,7 +67,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) else t | UnivFlexible alg -> if onlyalg && alg then - (evdref := Evd.make_flexible_variable !evdref false l; t) + (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t) else t)) | Sort (Prop Pos as s) when refreshset && not direction -> (* Cannot make a universe "lower" than "Set", diff --git a/test-suite/bugs/closed/5365.v b/test-suite/bugs/closed/5365.v new file mode 100644 index 000000000..be360d24d --- /dev/null +++ b/test-suite/bugs/closed/5365.v @@ -0,0 +1,13 @@ + +Inductive TupleT : nat -> Type := +| nilT : TupleT 0 +| consT {n} A : (A -> TupleT n) -> TupleT (S n). + +Inductive Tuple : forall n, TupleT n -> Type := + nil : Tuple _ nilT +| cons {n A} (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F). + +Inductive TupleMap : forall n, TupleT n -> TupleT n -> Type := + tmNil : TupleMap _ nilT nilT +| tmCons {n} {A B : Type} (F : A -> TupleT n) (G : B -> TupleT n) + : (forall x, sigT (fun y => TupleMap _ (F x) (G y))) -> TupleMap _ (consT A F) (consT B G). diff --git a/toplevel/command.ml b/toplevel/command.ml index a9f2598e2..2d09e8e9d 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -427,7 +427,7 @@ let make_conclusion_flexible evdref ty poly = | Type u -> (match Univ.universe_level u with | Some u -> - evdref := Evd.make_flexible_variable !evdref true u + evdref := Evd.make_flexible_variable !evdref ~algebraic:true u | None -> ()) | _ -> () else () diff --git a/toplevel/record.ml b/toplevel/record.ml index 8d35e5a3d..4e5628dfd 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -124,7 +124,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = | Sort s' -> (if poly then match Evd.is_sort_variable !evars s' with - | Some l -> evars := Evd.make_flexible_variable !evars true l; + | Some l -> evars := Evd.make_flexible_variable !evars ~algebraic:true l; sred, true | None -> s, false else s, false) |