diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:22:59 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:22:59 +0100 |
commit | a40fb961c8ffeeb03769404cacda8bd6cff17417 (patch) | |
tree | 7105d621bc16f825c1f309e3d5b7720b1b1513ec /engine | |
parent | 3875a525ee1e075be9f0eb1f17c74726e9f38b43 (diff) | |
parent | 66973ce17e32a3c692a5b0032f38300ec8cc36d3 (diff) |
Merge PR #6893: Cleanup UState API usage
Diffstat (limited to 'engine')
-rw-r--r-- | engine/evarutil.ml | 6 | ||||
-rw-r--r-- | engine/evd.ml | 77 | ||||
-rw-r--r-- | engine/evd.mli | 19 | ||||
-rw-r--r-- | engine/termops.ml | 3 | ||||
-rw-r--r-- | engine/uState.ml | 12 | ||||
-rw-r--r-- | engine/uState.mli | 5 |
6 files changed, 72 insertions, 50 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 7674cf67a..6b3ce048f 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -89,15 +89,15 @@ let nf_evars_universes evm = (Evd.universe_subst evm) let nf_evars_and_universes evm = - let evm = Evd.nf_constraints evm in + let evm = Evd.minimize_universes evm in evm, nf_evars_universes evm let e_nf_evars_and_universes evdref = - evdref := Evd.nf_constraints !evdref; + evdref := Evd.minimize_universes !evdref; nf_evars_universes !evdref, Evd.universe_subst !evdref let nf_evar_map_universes evm = - let evm = Evd.nf_constraints evm in + let evm = Evd.minimize_universes evm in let subst = Evd.universe_subst evm in if Univ.LMap.is_empty subst then evm, nf_evar0 evm else diff --git a/engine/evd.ml b/engine/evd.ml index e7d542d12..185cab101 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 minimize_universes evd = + let subst, uctx' = UState.normalize_variables evd.universes in + let uctx' = UState.minimize 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,25 @@ 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.minimize +let nf_constraints = minimize_universes diff --git a/engine/evd.mli b/engine/evd.mli index ed3316c16..49c953f6d 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -493,22 +493,31 @@ val univ_flexible_alg : rigid type 'a in_evar_universe_context = 'a * UState.t val evar_universe_context_set : UState.t -> Univ.ContextSet.t +[@@ocaml.deprecated "Alias of UState.context_set"] val evar_universe_context_constraints : UState.t -> Univ.Constraint.t +[@@ocaml.deprecated "Alias of UState.constraints"] val evar_context_universe_context : UState.t -> Univ.UContext.t [@@ocaml.deprecated "alias of UState.context"] val evar_universe_context_of : Univ.ContextSet.t -> UState.t +[@@ocaml.deprecated "Alias of UState.of_context_set"] val empty_evar_universe_context : UState.t +[@@ocaml.deprecated "Alias of UState.empty"] val union_evar_universe_context : UState.t -> UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.union"] val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst +[@@ocaml.deprecated "Alias of UState.subst"] val constrain_variables : Univ.LSet.t -> UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.constrain_variables"] val evar_universe_context_of_binders : Universes.universe_binders -> UState.t +[@@ocaml.deprecated "Alias of UState.of_binders"] val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t +[@@ocaml.deprecated "Use UState.make or UState.make_with_initial_binders"] val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map (** Raises Not_found if not a name for a universe in this map. *) val universe_of_name : evar_map -> Id.t -> Univ.Level.t @@ -516,13 +525,15 @@ val universe_of_name : evar_map -> Id.t -> Univ.Level.t val universe_binders : evar_map -> Universes.universe_binders val add_constraints_context : UState.t -> Univ.Constraint.t -> UState.t +[@@ocaml.deprecated "Alias of UState.add_constraints"] val normalize_evar_universe_context_variables : UState.t -> Univ.universe_subst in_evar_universe_context +[@@ocaml.deprecated "Alias of UState.normalize_variables"] -val normalize_evar_universe_context : UState.t -> - UState.t +val normalize_evar_universe_context : UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.minimize"] val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t @@ -581,12 +592,16 @@ val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_co val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst val abstract_undefined_variables : UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.abstract_undefined_variables"] val fix_undefined_variables : evar_map -> evar_map val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst +(** Universe minimization *) +val minimize_universes : evar_map -> evar_map val nf_constraints : evar_map -> evar_map +[@@ocaml.deprecated "Alias of Evd.minimize_universes"] val update_sigma_env : evar_map -> env -> evar_map diff --git a/engine/termops.ml b/engine/termops.ml index c615155d1..35258762a 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -294,12 +294,11 @@ let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_cont let pr_evar_universe_context ctx = let open UState in - let open Evd in let prl = pr_uctx_level ctx in if UState.is_empty ctx then mt () else (str"UNIVERSES:"++brk(0,1)++ - h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set ctx)) ++ fnl () ++ + h 0 (Univ.pr_universe_context_set prl (UState.context_set ctx)) ++ fnl () ++ str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ diff --git a/engine/uState.ml b/engine/uState.ml index 00825208b..e57afd743 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -476,6 +476,13 @@ let new_univ_variable ?loc rigid name uctx_initial_universes = initial} in uctx', u +let make_with_initial_binders e us = + let uctx = make e in + List.fold_left + (fun uctx { CAst.loc; v = id } -> + fst (new_univ_variable ?loc univ_rigid (Some id) uctx)) + uctx us + let add_global_univ uctx u = let initial = UGraph.add_universe u true uctx.uctx_initial_universes @@ -578,7 +585,7 @@ let refresh_undefined_univ_variables uctx = uctx_initial_universes = initial } in uctx', subst -let normalize uctx = +let minimize uctx = let ((vars',algs'), us') = Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic @@ -606,3 +613,6 @@ let update_sigma_env uctx env = uctx_universes = univs } in merge true univ_rigid eunivs eunivs.uctx_local + +(** Deprecated *) +let normalize = minimize diff --git a/engine/uState.mli b/engine/uState.mli index 68fe350c0..9a2bc706b 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -26,6 +26,8 @@ val empty : t val make : UGraph.t -> t +val make_with_initial_binders : UGraph.t -> Misctypes.lident list -> t + val is_empty : t -> bool val union : t -> t -> t @@ -131,7 +133,10 @@ val fix_undefined_variables : t -> t val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst +(** Universe minimization *) +val minimize : t -> t val normalize : t -> t +[@@ocaml.deprecated "Alias of UState.minimize"] type universe_decl = (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl |