diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 20 | ||||
| -rw-r--r-- | engine/evd.ml | 5 | ||||
| -rw-r--r-- | engine/evd.mli | 8 | ||||
| -rw-r--r-- | engine/uState.ml | 24 | ||||
| -rw-r--r-- | engine/uState.mli | 9 |
5 files changed, 25 insertions, 41 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 8493119ee5..8756ebfdf2 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -405,25 +405,17 @@ let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs = let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs = let open UnivProblem in - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); - cstrs - | Declarations.Polymorphic_ind _ -> - enforce_eq_instances_univs false u1 u2 cstrs - | Declarations.Cumulative_ind cumi -> + match mind.Declarations.mind_variance with + | None -> enforce_eq_instances_univs false u1 u2 cstrs + | Some variances -> let num_param_arity = Reduction.inductive_cumulativity_arguments spec in - let variances = Univ.ACumulativityInfo.variance cumi in compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs = let open UnivProblem in - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - cstrs - | Declarations.Polymorphic_ind _ -> - enforce_eq_instances_univs false u1 u2 cstrs - | Declarations.Cumulative_ind cumi -> + match mind.Declarations.mind_variance with + | None -> enforce_eq_instances_univs false u1 u2 cstrs + | Some _ -> let num_cnstr_args = Reduction.constructor_cumulativity_arguments spec in if not (Int.equal num_cnstr_args nargs) then enforce_eq_instances_univs false u1 u2 cstrs diff --git a/engine/evd.ml b/engine/evd.ml index eee2cb700c..f0433d3387 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -852,8 +852,9 @@ let universe_context_set d = UState.context_set d.universes let to_universe_context evd = UState.context evd.universes -let const_univ_entry ~poly evd = UState.const_univ_entry ~poly evd.universes -let ind_univ_entry ~poly evd = UState.ind_univ_entry ~poly evd.universes +let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes + +let const_univ_entry = univ_entry let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl diff --git a/engine/evd.mli b/engine/evd.mli index de73144895..d2d18ca486 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -597,12 +597,12 @@ val universes : evar_map -> UGraph.t [Univ.ContextSet.to_context]. *) val to_universe_context : evar_map -> Univ.UContext.t -val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry +val univ_entry : poly:bool -> evar_map -> Entries.universes_entry -(** NB: [ind_univ_entry] cannot create cumulative entries. *) -val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes +val const_univ_entry : poly:bool -> evar_map -> Entries.universes_entry +[@@ocaml.deprecated "Use [univ_entry]."] -val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.constant_universes_entry +val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.universes_entry val merge_universe_context : evar_map -> UState.t -> evar_map val set_universe_context : evar_map -> UState.t -> evar_map diff --git a/engine/uState.ml b/engine/uState.ml index 430a3a2fd9..77d1896683 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -100,24 +100,16 @@ let constraints ctx = snd ctx.uctx_local let context ctx = ContextSet.to_context ctx.uctx_local -let const_univ_entry ~poly uctx = +let univ_entry ~poly uctx = let open Entries in if poly then let (binders, _) = uctx.uctx_names in let uctx = context uctx in let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in - Polymorphic_const_entry (nas, uctx) - else Monomorphic_const_entry (context_set uctx) + Polymorphic_entry (nas, uctx) + else Monomorphic_entry (context_set uctx) -(* does not support cumulativity since you need more info *) -let ind_univ_entry ~poly uctx = - let open Entries in - if poly then - let (binders, _) = uctx.uctx_names in - let uctx = context uctx in - let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in - Polymorphic_ind_entry (nas, uctx) - else Monomorphic_ind_entry (context_set uctx) +let const_univ_entry = univ_entry let of_context_set ctx = { empty with uctx_local = ctx } @@ -422,10 +414,10 @@ let check_univ_decl ~poly uctx decl = let (binders, _) = uctx.uctx_names in let uctx = universe_context ~names ~extensible uctx in let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in - Entries.Polymorphic_const_entry (nas, uctx) + Entries.Polymorphic_entry (nas, uctx) else let () = check_universe_context_set ~names ~extensible uctx in - Entries.Monomorphic_const_entry uctx.uctx_local + Entries.Monomorphic_entry uctx.uctx_local in if not decl.univdecl_extensible_constraints then check_implication uctx @@ -458,8 +450,8 @@ let restrict ctx vars = let demote_seff_univs entry uctx = let open Entries in match entry.const_entry_universes with - | Polymorphic_const_entry _ -> uctx - | Monomorphic_const_entry (univs, _) -> + | Polymorphic_entry _ -> uctx + | Monomorphic_entry (univs, _) -> let seff = LSet.union uctx.uctx_seff_univs univs in { uctx with uctx_seff_univs = seff } diff --git a/engine/uState.mli b/engine/uState.mli index 5170184ef4..a358813825 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -64,12 +64,11 @@ val constraints : t -> Univ.Constraint.t val context : t -> Univ.UContext.t (** Shorthand for {!context_set} with {!Context_set.to_context}. *) -val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry +val univ_entry : poly:bool -> t -> Entries.universes_entry (** Pick from {!context} or {!context_set} based on [poly]. *) -val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes -(** Pick from {!context} or {!context_set} based on [poly]. - Cannot create cumulative entries. *) +val const_univ_entry : poly:bool -> t -> Entries.universes_entry +[@@ocaml.deprecated "Use [univ_entry]."] (** {5 Constraints handling} *) @@ -177,7 +176,7 @@ val default_univ_decl : universe_decl When polymorphic, the universes corresponding to [decl.univdecl_instance] come first in the order defined by that list. *) -val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.constant_universes_entry +val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.universes_entry val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t |