diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 22 | ||||
| -rw-r--r-- | proofs/proofview.mli | 68 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 2 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 45 |
4 files changed, 75 insertions, 62 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index b8a58daeb2..826b4772a0 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -908,17 +908,17 @@ let catchable_exception = function module Goal = struct - type 'a t = { + type ('a, 'r) t = { env : Environ.env; sigma : Evd.evar_map; concl : Term.constr ; self : Evar.t ; (* for compatibility with old-style definitions *) } - type 'a enter = - { enter : 'a t -> unit tactic } + type ('a, 'b) enter = + { enter : 'r. ('a, 'r) t -> 'b } - let assume (gl : 'a t) = (gl :> [ `NF ] t) + let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t) let env { env=env } = env let sigma { sigma=sigma } = sigma @@ -977,8 +977,8 @@ module Goal = struct end end - type 'a s_enter = - { s_enter : 'r. 'a t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma } + type ('a, 'b) s_enter = + { s_enter : 'r. ('a, 'r) t -> 'r Sigma.t -> ('b, 'r) Sigma.sigma } let s_enter f = InfoL.tag (Info.Dispatch) begin @@ -1033,6 +1033,8 @@ module Goal = struct (* compatibility *) let goal { self=self } = self + let lift (gl : ('a, 'r) t) _ = (gl :> ('a, 's) t) + end @@ -1257,8 +1259,8 @@ module Notations = struct let (>>=) = tclBIND let (<*>) = tclTHEN let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) - type 'a enter = 'a Goal.enter = - { enter : 'a Goal.t -> unit tactic } - type 'a s_enter = 'a Goal.s_enter = - { s_enter : 'r. 'a Goal.t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma } + type ('a, 'b) enter = ('a, 'b) Goal.enter = + { enter : 'r. ('a, 'r) Goal.t -> 'b } + type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter = + { s_enter : 'r. ('a, 'r) Goal.t -> 'r Sigma.t -> ('b, 'r) Sigma.sigma } end diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 1616782e54..5c97ada344 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -418,61 +418,71 @@ end module Goal : sig - (** 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 + (** Type of goals. + + The first 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. + + The second parameter is a stage indicating where the goal belongs. See + module {!Sigma}. + *) + type ('a, 'r) t (** Assume that you do not need the goal to be normalized. *) - val assume : 'a t -> [ `NF ] t + val assume : ('a, 'r) t -> ([ `NF ], 'r) t (** Normalises the argument goal. *) - val normalize : 'a t -> [ `NF ] t tactic + val normalize : ('a, 'r) t -> ([ `NF ], 'r) t tactic (** [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 : [ `NF ] t -> Term.constr - val hyps : [ `NF ] t -> Context.named_context - val env : 'a t -> Environ.env - val sigma : 'a t -> Evd.evar_map - val extra : 'a t -> Evd.Store.t + val concl : ([ `NF ], 'r) t -> Term.constr + val hyps : ([ `NF ], 'r) t -> Context.named_context + val env : ('a, 'r) t -> Environ.env + val sigma : ('a, 'r) t -> Evd.evar_map + val extra : ('a, 'r) t -> Evd.Store.t (** Returns the goal's conclusion even if the goal is not normalised. *) - val raw_concl : 'a t -> Term.constr + val raw_concl : ('a, 'r) t -> Term.constr - type 'a enter = - { enter : 'a t -> unit tactic } + type ('a, 'b) enter = + { enter : 'r. ('a, 'r) t -> 'b } (** [nf_enter t] applies the goal-dependent tactic [t] in each goal independently, in the manner of {!tclINDEPENDENT} except that the current goal is also given as an argument to [t]. The goal is normalised with respect to evars. *) - val nf_enter : [ `NF ] enter -> unit tactic + val nf_enter : ([ `NF ], unit tactic) enter -> unit tactic (** Like {!nf_enter}, but does not normalize the goal beforehand. *) - val enter : [ `LZ ] enter -> unit tactic + val enter : ([ `LZ ], unit tactic) enter -> unit tactic - type 'a s_enter = - { s_enter : 'r. 'a t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma } + type ('a, 'b) s_enter = + { s_enter : 'r. ('a, 'r) t -> 'r Sigma.t -> ('b, 'r) Sigma.sigma } (** A variant of {!enter} allows to work with a monotonic state. The evarmap returned by the argument is put back into the current state before firing the returned tactic. *) - val s_enter : [ `LZ ] s_enter -> unit tactic + val s_enter : ([ `LZ ], unit tactic) s_enter -> unit tactic (** Like {!s_enter}, but normalizes the goal beforehand. *) - val nf_s_enter : [ `NF ] s_enter -> unit tactic + val nf_s_enter : ([ `NF ], unit tactic) s_enter -> unit tactic - (** Recover the list of current goals under focus, without evar-normalization *) - val goals : [ `LZ ] t tactic list tactic + (** Recover the list of current goals under focus, without evar-normalization. + FIXME: encapsulate the level in an existential type. *) + val goals : ([ `LZ ], 'r) t tactic list tactic (** Compatibility: avoid if possible *) - val goal : [ `NF ] t -> Evar.t + val goal : ([ `NF ], 'r) t -> Evar.t + + (** Every goal is valid at a later stage. FIXME: take a later evarmap *) + val lift : ('a, 'r) t -> ('r, 's) Sigma.le -> ('a, 's) t end @@ -595,8 +605,8 @@ module Notations : sig (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *) val (<+>) : 'a tactic -> 'a tactic -> 'a tactic - type 'a enter = 'a Goal.enter = - { enter : 'a Goal.t -> unit tactic } - type 'a s_enter = 'a Goal.s_enter = - { s_enter : 'r. 'a Goal.t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma } + type ('a, 'b) enter = ('a, 'b) Goal.enter = + { enter : 'r. ('a, 'r) Goal.t -> 'b } + type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter = + { s_enter : 'r. ('a, 'r) Goal.t -> 'r Sigma.t -> ('b, 'r) Sigma.sigma } end diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 4238d1e372..8af28b6ab1 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -212,7 +212,7 @@ 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 : ([ `LZ ], 'r) Proofview.Goal.t) = (** We normalize the conclusion just after *) let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index a0e1a01577..3ed6a2eeb1 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -106,36 +106,37 @@ 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) -> '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_apply : (env -> evar_map -> 'a) -> ('b, 'r) Proofview.Goal.t -> 'a + val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> constr + (** FIXME: encapsulate the level in an existential type. *) + val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a - val pf_env : 'a Proofview.Goal.t -> Environ.env - val pf_concl : [ `NF ] Proofview.Goal.t -> types + val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env + val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types - val pf_unsafe_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types - val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> evar_map * Term.types - val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool + val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types + val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.types + val pf_conv_x : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.constr -> bool - val pf_get_new_id : identifier -> [ `NF ] Proofview.Goal.t -> identifier - val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list - val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list + val pf_get_new_id : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier + val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list + val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list - 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 + val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> named_declaration + val pf_get_hyp_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types + val pf_last_hyp : ([ `NF ], 'r) 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 -> pinductive * types + val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types + val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * 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 : ('a, 'r) Proofview.Goal.t -> constr -> types + val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types - val pf_whd_betadeltaiota : 'a Proofview.Goal.t -> constr -> constr - val pf_compute : 'a Proofview.Goal.t -> constr -> constr + val pf_whd_betadeltaiota : ('a, 'r) Proofview.Goal.t -> constr -> constr + val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr - val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map + val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map - val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr + val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr end |