From 5d926b0279f70250db1ee54edcdb4e855ac96f0f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 2 Mar 2018 14:58:00 +0100 Subject: Deprecate UState aliases in Evd. --- engine/evd.ml | 74 ++++++++++++++++++++++++++--------------------------------- 1 file changed, 33 insertions(+), 41 deletions(-) (limited to 'engine/evd.ml') diff --git a/engine/evd.ml b/engine/evd.ml index e7d542d12..47fa48d4f 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -253,21 +253,8 @@ let instantiate_evar_array info c args = | [] -> c | _ -> replace_vars inst c -type evar_universe_context = UState.t - -type 'a in_evar_universe_context = 'a * evar_universe_context -let empty_evar_universe_context = UState.empty -let union_evar_universe_context = UState.union -let evar_universe_context_set = UState.context_set -let evar_universe_context_constraints = UState.constraints -let evar_context_universe_context = UState.context -let evar_universe_context_of = UState.of_context_set -let evar_universe_context_subst = UState.subst -let add_constraints_context = UState.add_constraints -let add_universe_constraints_context = UState.add_universe_constraints -let constrain_variables = UState.constrain_variables -let evar_universe_context_of_binders = UState.of_binders +type 'a in_evar_universe_context = 'a * UState.t (*******************************************************************) (* Metamaps *) @@ -427,7 +414,7 @@ type evar_map = { undf_evars : evar_info EvMap.t; evar_names : EvNames.t; (** Universes *) - universes : evar_universe_context; + universes : UState.t; (** Conversion problems *) conv_pbs : evar_constraint list; last_mods : Evar.Set.t; @@ -558,10 +545,10 @@ let existential_type d (n, args) = instantiate_evar_array info info.evar_concl args let add_constraints d c = - { d with universes = add_constraints_context d.universes c } + { d with universes = UState.add_constraints d.universes c } let add_universe_constraints d c = - { d with universes = add_universe_constraints_context d.universes c } + { d with universes = UState.add_universe_constraints d.universes c } (*** /Lifting... ***) @@ -586,7 +573,7 @@ let create_evar_defs sigma = { sigma with let empty = { defn_evars = EvMap.empty; undf_evars = EvMap.empty; - universes = empty_evar_universe_context; + universes = UState.empty; conv_pbs = []; last_mods = Evar.Set.empty; metas = Metamap.empty; @@ -609,14 +596,14 @@ let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d = let last_mods = if with_conv_pbs then evd.last_mods else d.last_mods in let universes = if not with_univs then evd.universes - else union_evar_universe_context evd.universes d.universes + else UState.union evd.universes d.universes in { evd with metas = d.metas; last_mods; conv_pbs; universes } let merge_universe_context evd uctx' = - { evd with universes = union_evar_universe_context evd.universes uctx' } + { evd with universes = UState.union evd.universes uctx' } let set_universe_context evd uctx' = { evd with universes = uctx' } @@ -798,16 +785,6 @@ 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 - match l with - | None -> uctx - | Some us -> - List.fold_left - (fun uctx { CAst.loc; v = id } -> - fst (UState.new_univ_variable ?loc univ_rigid (Some id) uctx)) - uctx us - (****************************************) (* Operations on constants *) (****************************************) @@ -910,10 +887,6 @@ let check_eq evd s s' = let check_leq evd s s' = UGraph.check_leq (UState.ugraph evd.universes) s s' -let normalize_evar_universe_context_variables = UState.normalize_variables - -let abstract_undefined_variables = UState.abstract_undefined_variables - let fix_undefined_variables evd = { evd with universes = UState.fix_undefined_variables evd.universes } @@ -922,16 +895,14 @@ let refresh_undefined_universes evd = let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in evd', subst -let normalize_evar_universe_context = UState.normalize - -let nf_univ_variables evd = - let subst, uctx' = normalize_evar_universe_context_variables evd.universes in +let nf_univ_variables evd = + let subst, uctx' = UState.normalize_variables evd.universes in let evd' = {evd with universes = uctx'} in evd', subst let nf_constraints evd = - let subst, uctx' = normalize_evar_universe_context_variables evd.universes in - let uctx' = normalize_evar_universe_context uctx' in + let subst, uctx' = UState.normalize_variables evd.universes in + let uctx' = UState.normalize uctx' in {evd with universes = uctx'} let universe_of_name evd s = UState.universe_of_name evd.universes s @@ -1076,7 +1047,7 @@ let clear_metas evd = {evd with metas = Metamap.empty} let meta_merge ?(with_univs = true) evd1 evd2 = let metas = Metamap.fold Metamap.add evd1.metas evd2.metas in let universes = - if with_univs then union_evar_universe_context evd2.universes evd1.universes + if with_univs then UState.union evd2.universes evd1.universes else evd2.universes in {evd2 with universes; metas; } @@ -1176,3 +1147,24 @@ module Monad = (* Failure explanation *) type unsolvability_explanation = SeveralInstancesFound of int + +(** Deprecated *) +type evar_universe_context = UState.t +let empty_evar_universe_context = UState.empty +let union_evar_universe_context = UState.union +let evar_universe_context_set = UState.context_set +let evar_universe_context_constraints = UState.constraints +let evar_context_universe_context = UState.context +let evar_universe_context_of = UState.of_context_set +let evar_universe_context_subst = UState.subst +let add_constraints_context = UState.add_constraints +let constrain_variables = UState.constrain_variables +let evar_universe_context_of_binders = UState.of_binders +let make_evar_universe_context e l = + let g = Environ.universes e in + match l with + | None -> UState.make g + | Some l -> UState.make_with_initial_binders g l +let normalize_evar_universe_context_variables = UState.normalize_variables +let abstract_undefined_variables = UState.abstract_undefined_variables +let normalize_evar_universe_context = UState.normalize -- cgit v1.2.3