From 68935660fbfdec2e357e123ed999073ed3b8fc26 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Feb 2018 16:00:04 +0100 Subject: [engine] Remove ghost parameter from `Proofview.Goal.t` In current code, `Proofview.Goal.t` uses a phantom type to indicate whether the goal was properly substituted wrt current `evar_map` or not. After the introduction of `EConstr`, this distinction should have become unnecessary, thus we remove the phantom parameter from `'a Proofview.Goal.t`. This may introduce some minor incompatibilities at the typing level. Code-wise, things should remain the same. We thus deprecate `assume`. In a next commit, we will remove normalization as much as possible from the code. --- proofs/clenv.mli | 8 ++++---- proofs/clenvtac.ml | 2 +- proofs/refine.ml | 2 -- proofs/refine.mli | 2 +- proofs/tacmach.ml | 6 +----- proofs/tacmach.mli | 48 ++++++++++++++++++++++++------------------------ 6 files changed, 31 insertions(+), 37 deletions(-) (limited to 'proofs') diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 9a2026dd3..c894b9dc9 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -41,10 +41,10 @@ val clenv_nf_meta : clausenv -> EConstr.constr -> EConstr.constr (** type of a meta in clenv context *) val clenv_meta_type : clausenv -> metavariable -> types -val mk_clenv_from : 'a Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv +val mk_clenv_from : Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv val mk_clenv_from_n : - 'a Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv -val mk_clenv_type_of : 'a Proofview.Goal.t -> EConstr.constr -> clausenv + Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv +val mk_clenv_type_of : Proofview.Goal.t -> EConstr.constr -> clausenv val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv (** Refresh the universes in a clenv *) @@ -66,7 +66,7 @@ val old_clenv_unique_resolver : ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv val clenv_unique_resolver : - ?flags:unify_flags -> clausenv -> 'a Proofview.Goal.t -> clausenv + ?flags:unify_flags -> clausenv -> Proofview.Goal.t -> clausenv val clenv_dependent : clausenv -> metavariable list diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 8bd5d98cb..373d60e69 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -141,7 +141,7 @@ let fail_quick_unif_flags = { let unify ?(flags=fail_quick_unif_flags) m = Proofview.Goal.enter begin fun gl -> let env = Tacmach.New.pf_env gl in - let n = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in + let n = Tacmach.New.pf_concl gl in let evd = clear_metas (Tacmach.New.project gl) in try let evd' = w_unify env evd CONV ~flags m n in diff --git a/proofs/refine.ml b/proofs/refine.ml index e3f650848..90276951b 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -70,7 +70,6 @@ let add_side_effects env effects = List.fold_left (fun env eff -> add_side_effect env eff) env effects let generic_refine ~typecheck f gl = - let gl = Proofview.Goal.assume gl in let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in @@ -159,7 +158,6 @@ let with_type env evd c t = evd , j'.Environ.uj_val let refine_casted ~typecheck f = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let f h = diff --git a/proofs/refine.mli b/proofs/refine.mli index cfdcde36e..1932a306c 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -33,7 +33,7 @@ val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr (** A variant of [refine] which assumes exactly one goal under focus *) val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic -> - [ `NF ] Proofview.Goal.t -> 'a tactic + Proofview.Goal.t -> 'a tactic (** The general version of refine. *) (** {7 Helper functions} *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index bdcb4868b..d3405b892 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -150,7 +150,6 @@ module New = struct let pf_global id gl = (** We only check for the existence of an [id] in [hyps] *) - let gl = Proofview.Goal.assume gl in let hyps = Proofview.Goal.hyps gl in Constrintern.construct_reference hyps id @@ -167,13 +166,11 @@ module New = struct let pf_ids_of_hyps gl = (** We only get the identifiers in [hyps] *) - let gl = Proofview.Goal.assume gl in let hyps = Proofview.Goal.hyps gl in ids_of_named_context hyps let pf_ids_set_of_hyps gl = (** We only get the identifiers in [hyps] *) - let gl = Proofview.Goal.assume gl in let env = Proofview.Goal.env gl in Environ.ids_of_named_context_val (Environ.named_context_val env) @@ -204,9 +201,8 @@ module New = struct let hyps = Proofview.Goal.hyps gl in List.hd hyps - let pf_nf_concl (gl : [ `LZ ] Proofview.Goal.t) = + let pf_nf_concl (gl : Proofview.Goal.t) = (** We normalize the conclusion just after *) - let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let sigma = project gl in nf_evar sigma concl diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index e0fb8fbc5..8f69358d4 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -92,46 +92,46 @@ val pr_glls : goal list sigma -> Pp.t (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig - val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a - val pf_global : Id.t -> 'a Proofview.Goal.t -> Globnames.global_reference + val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a + val pf_global : Id.t -> Proofview.Goal.t -> Globnames.global_reference (** FIXME: encapsulate the level in an existential type. *) - val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a + val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a - val project : 'a Proofview.Goal.t -> Evd.evar_map - val pf_env : 'a Proofview.Goal.t -> Environ.env - val pf_concl : 'a Proofview.Goal.t -> types + val project : Proofview.Goal.t -> Evd.evar_map + val pf_env : Proofview.Goal.t -> Environ.env + val pf_concl : Proofview.Goal.t -> types (** WRONG: To be avoided at all costs, it typechecks the term entirely but forgets the universe constraints necessary to retypecheck it *) - val pf_unsafe_type_of : 'a Proofview.Goal.t -> constr -> types + val pf_unsafe_type_of : Proofview.Goal.t -> constr -> types (** This function does no type inference and expects an already well-typed term. It recomputes its type in the fastest way possible (no conversion is ever involved) *) - val pf_get_type_of : 'a Proofview.Goal.t -> constr -> types + val pf_get_type_of : Proofview.Goal.t -> constr -> types (** This function entirely type-checks the term and computes its type and the implied universe constraints. *) - val pf_type_of : 'a Proofview.Goal.t -> constr -> evar_map * types - val pf_conv_x : 'a Proofview.Goal.t -> t -> t -> bool + val pf_type_of : Proofview.Goal.t -> constr -> evar_map * types + val pf_conv_x : Proofview.Goal.t -> t -> t -> bool - val pf_get_new_id : Id.t -> 'a Proofview.Goal.t -> Id.t - val pf_ids_of_hyps : 'a Proofview.Goal.t -> Id.t list - val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Id.Set.t - val pf_hyps_types : 'a Proofview.Goal.t -> (Id.t * types) list + val pf_get_new_id : Id.t -> Proofview.Goal.t -> Id.t + val pf_ids_of_hyps : Proofview.Goal.t -> Id.t list + val pf_ids_set_of_hyps : Proofview.Goal.t -> Id.Set.t + val pf_hyps_types : Proofview.Goal.t -> (Id.t * types) list - val pf_get_hyp : Id.t -> 'a Proofview.Goal.t -> named_declaration - val pf_get_hyp_typ : Id.t -> 'a Proofview.Goal.t -> types - val pf_last_hyp : 'a Proofview.Goal.t -> named_declaration + val pf_get_hyp : Id.t -> Proofview.Goal.t -> named_declaration + val pf_get_hyp_typ : Id.t -> Proofview.Goal.t -> types + val pf_last_hyp : Proofview.Goal.t -> named_declaration - val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types - val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> (inductive * EInstance.t) * types + val pf_nf_concl : Proofview.Goal.t -> types + val pf_reduce_to_quantified_ind : Proofview.Goal.t -> types -> (inductive * EInstance.t) * types - val pf_hnf_constr : 'a Proofview.Goal.t -> constr -> types - val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types + val pf_hnf_constr : Proofview.Goal.t -> constr -> types + val pf_hnf_type_of : Proofview.Goal.t -> constr -> types - val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr - val pf_compute : 'a Proofview.Goal.t -> constr -> constr + val pf_whd_all : Proofview.Goal.t -> constr -> constr + val pf_compute : Proofview.Goal.t -> constr -> constr - val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr + val pf_nf_evar : Proofview.Goal.t -> constr -> constr end -- cgit v1.2.3