diff options
| -rw-r--r-- | proofs/goal.ml | 5 | ||||
| -rw-r--r-- | proofs/proofview.ml | 24 | ||||
| -rw-r--r-- | proofs/proofview.mli | 26 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 4 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 20 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 4 |
7 files changed, 58 insertions, 27 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index b0fded289..64eeb69d9 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -375,10 +375,7 @@ let defs _ rdefs _ _ = let enter f = (); fun env rdefs gl info -> let sigma = !rdefs in - let concl = Reductionops.nf_evar sigma (Evd.evar_concl info) in - let map_nf c = Reductionops.nf_evar sigma c in - let hyps = Environ.map_named_val map_nf (Evd.evar_hyps info) in - f env sigma hyps concl gl + f env sigma (Evd.evar_hyps info) (Evd.evar_concl info) gl (*** Conversion in goals ***) diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 1365fe86e..67893e3b7 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -768,7 +768,7 @@ end module Goal = struct - type t = { + type 'a t = { env : Environ.env; sigma : Evd.evar_map; hyps : Environ.named_context_val; @@ -776,6 +776,8 @@ module Goal = struct self : Goal.goal ; (* for compatibility with old-style definitions *) } + let assume (gl : 'a t) = (gl :> [ `NF ] t) + let env { env=env } = env let sigma { sigma=sigma } = sigma let hyps { hyps=hyps } = Environ.named_context_of_val hyps @@ -800,8 +802,12 @@ module Goal = struct tclZERO e let enter_t f = Goal.enter begin fun env sigma hyps concl self -> + let concl = Reductionops.nf_evar sigma concl in + let map_nf c = Reductionops.nf_evar sigma c in + let hyps = Environ.map_named_val map_nf hyps in f {env=env;sigma=sigma;hyps=hyps;concl=concl;self=self} end + let enter f = list_iter_goal () begin fun goal () -> Proof.current >>= fun env -> @@ -815,6 +821,22 @@ module Goal = struct tclZERO e end + let raw_enter_t f = Goal.enter begin fun env sigma hyps concl self -> + f {env=env;sigma=sigma;hyps=hyps;concl=concl;self=self} + end + + let raw_enter f = + list_iter_goal () begin fun goal () -> + Proof.current >>= fun env -> + tclEVARMAP >>= fun sigma -> + try + (* raw_enter_t cannot modify the sigma. *) + let (t,_) = Goal.eval (raw_enter_t f) env sigma goal in + t + with e when catchable_exception e -> + let e = Errors.push e in + tclZERO e + end (* compatibility *) let goal { self=self } = self diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 7e2d374d5..7be8f6003 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -335,17 +335,24 @@ end Eventually I'll try to remove it in favour of [Proofview.Goal] *) module Goal : sig - (* The type of goals *) - type t + (** The type of goals. The parameter type is a phantom argument indicating + whether the data contained in the goal has been normalized w.r.t. the + current sigma. If it is the case, it is flagged [ `NF ]. You may still + access the un-normalized data using {!assume} if you known you do not rely + on the assumption of being normalized, at your own risk. *) + type 'a t + + (** Assume that you do not need the goal to be normalized. *) + val assume : 'a t -> [ `NF ] t (* [concl], [hyps], [env] and [sigma] given a goal [gl] return respectively the conclusion of [gl], the hypotheses of [gl], the environment of [gl] (i.e. the global environment and the hypotheses) and the current evar map. *) - val concl : t -> Term.constr - val hyps : t -> Context.named_context - val env : t -> Environ.env - val sigma : t -> Evd.evar_map + val concl : [ `NF ] t -> Term.constr + val hyps : [ `NF ] t -> Context.named_context + val env : 'a t -> Environ.env + val sigma : 'a t -> Evd.evar_map (* [lift_sensitive s k] applies [s] in each goal independently raising result [a] then continues with [k a]. *) @@ -354,15 +361,16 @@ module Goal : sig (* [enter t] execute the goal-dependent tactic [t] in each goal independently. In particular [t] need not backtrack the same way in each goal. *) - val enter : (t -> unit tactic) -> unit tactic + val enter : ([ `NF ] t -> unit tactic) -> unit tactic + val raw_enter : ([ `LZ ] t -> unit tactic) -> unit tactic (* compatibility: avoid if possible *) - val goal : t -> Goal.goal + val goal : [ `NF ] t -> Goal.goal (** [refresh g] updates the [sigma g] to the current value, may be useful with compatibility functions like [Tacmach.New.of_old] *) - val refresh_sigma : t -> t tactic + val refresh_sigma : 'a t -> 'a t tactic end (* The [NonLogical] module allows to execute side effects in tactics diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 9a03df041..adeb50741 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -212,6 +212,8 @@ module New = struct f { Evd.it = Proofview.Goal.goal gl ; sigma = Proofview.Goal.sigma gl } 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 @@ -221,6 +223,8 @@ 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 diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 10f6be1d5..07639f475 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -130,17 +130,17 @@ val pr_glls : goal list sigma -> Pp.std_ppcmds (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig - val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a - val pf_global : identifier -> Proofview.Goal.t -> constr - val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a + val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a + val pf_global : identifier -> 'a Proofview.Goal.t -> constr + val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a - val pf_type_of : Proofview.Goal.t -> Term.constr -> Term.types + val pf_type_of : 'b Proofview.Goal.t -> Term.constr -> Term.types - val pf_get_new_id : identifier -> Proofview.Goal.t -> identifier - val pf_ids_of_hyps : Proofview.Goal.t -> identifier list - val pf_hyps_types : Proofview.Goal.t -> (identifier * types) list + val pf_get_new_id : identifier -> [ `NF ] Proofview.Goal.t -> identifier + val pf_ids_of_hyps : 'b Proofview.Goal.t -> identifier list + val pf_hyps_types : 'b Proofview.Goal.t -> (identifier * types) list - val pf_get_hyp : identifier -> Proofview.Goal.t -> named_declaration - val pf_get_hyp_typ : identifier -> Proofview.Goal.t -> types - val pf_last_hyp : Proofview.Goal.t -> named_declaration + val pf_get_hyp : identifier -> [ `NF ] Proofview.Goal.t -> named_declaration + val pf_get_hyp_typ : identifier -> [ `NF ] Proofview.Goal.t -> types + val pf_last_hyp : [ `NF ] Proofview.Goal.t -> named_declaration end diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 830fbd2d4..981616246 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -944,7 +944,7 @@ let val_interp_glob ist (tac:glob_tactic_expr) : typed_generic_argument = module GenargTac = Genarg.Monadic(Proofview.Monad) (* Interprets an l-tac expression into a value *) -let rec val_interp ist (tac:glob_tactic_expr) (gl:Proofview.Goal.t) : typed_generic_argument Proofview.tactic = +let rec val_interp ist (tac:glob_tactic_expr) (gl:'a Proofview.Goal.t) : typed_generic_argument Proofview.tactic = let value_interp ist = try Proofview.tclUNIT (val_interp_glob ist tac) with NeedsAGoal -> diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 49d40db24..090fb1cca 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -66,10 +66,10 @@ val interp_genarg : interp_sign -> Environ.env -> Evd.evar_map -> Term.constr -> glob_generic_argument -> Evd.evar_map * typed_generic_argument (** Interprets any expression *) -val val_interp : interp_sign -> glob_tactic_expr -> Proofview.Goal.t -> value Proofview.tactic +val val_interp : interp_sign -> glob_tactic_expr -> [ `NF ] Proofview.Goal.t -> value Proofview.tactic (** Interprets an expression that evaluates to a constr *) -val interp_ltac_constr : interp_sign -> glob_tactic_expr -> Proofview.Goal.t -> constr Proofview.tactic +val interp_ltac_constr : interp_sign -> glob_tactic_expr -> [ `NF ] Proofview.Goal.t -> constr Proofview.tactic (** Interprets redexp arguments *) val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr |