diff options
Diffstat (limited to 'dev/doc/proof-engine.md')
| -rw-r--r-- | dev/doc/proof-engine.md | 31 |
1 files changed, 13 insertions, 18 deletions
diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md index 8f96ac22..77455223 100644 --- a/dev/doc/proof-engine.md +++ b/dev/doc/proof-engine.md @@ -42,8 +42,8 @@ goal holes thanks to the `Refine` module, and in particular to the `Refine.refine` primitive. ```ocaml -val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic -(** In [refine typecheck t], [t] is a term with holes under some +val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic +(** In [refine ~typecheck t], [t] is a term with holes under some [evar_map] context. The term [t] is used as a partial solution for the current goal (refine is a goal-dependent tactic), the new holes created by [t] become the new subgoals. Exceptions @@ -51,12 +51,11 @@ val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) ``` -In a first approximation, we can think of `'a Sigma.run` as -`evar_map -> 'a * evar_map`. What the function does is first evaluate the -`Constr.t Sigma.run` argument in the current proof state, and then use the -resulting term as a filler for the proof under focus. All evars that have been -created by the invocation of this thunk are then turned into new goals added in -the order of their creation. +What the function does is first evaluate the `t` argument in the +current proof state, and then use the resulting term as a filler for +the proof under focus. All evars that have been created by the +invocation of this thunk are then turned into new goals added in the +order of their creation. To see how we can use it, let us have a look at an idealized example, the `cut` tactic. Assuming `X` is a type, `cut X` fills the current goal `[Γ ⊢ _ : A]` @@ -66,8 +65,7 @@ two new holes `[e1, e2]` are added to the goal state in this order. ```ocaml let cut c = - let open Sigma in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> (** In this block, we focus on one goal at a time indicated by gl *) let env = Proofview.Goal.env gl in (** Get the context of the goal, essentially [Γ] *) @@ -80,25 +78,22 @@ let cut c = let t = mkArrow c (Vars.lift 1 concl) in (** Build [X -> A]. Note the lifting of [A] due to being on the right hand side of the arrow. *) - Refine.refine { run = begin fun sigma -> + Refine.refine begin fun sigma -> (** All evars generated by this block will be added as goals *) - let Sigma (f, sigma, p) = Evarutil.new_evar env sigma t in + let sigma, f = Evarutil.new_evar env sigma t in (** Generate ?e1 : [Γ ⊢ _ : X -> A], add it to sigma, and return the term [f := Γ ⊢ ?e1{Γ} : X -> A] with the updated sigma. The identity substitution for [Γ] is extracted from the [env] argument, so that one must be careful to pass the correct context here in order for the resulting term to be well-typed. The [p] return value is a proof term used to enforce sigma monotonicity. *) - let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c in + let sigma, x = Evarutil.new_evar env sigma c in (** Generate ?e2 : [Γ ⊢ _ : X] in sigma and return [x := Γ ⊢ ?e2{Γ} : X]. *) let r = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 r, [|mkRel 1|])) in (** Build [r := Γ ⊢ let id : X := ?e2{Γ} in ?e1{Γ} id : A] *) - Sigma (r, sigma, p +> q) - (** Fills the current hole with [r]. The [p +> q] thingy ensures - monotonicity of sigma. *) - end } - end } + end + end ``` The `Evarutil.new_evar` function is the preferred way to generate evars in |