summaryrefslogtreecommitdiff
path: root/dev/doc/proof-engine.md
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
commit9ebf44d84754adc5b64fcf612c6816c02c80462d (patch)
treebf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /dev/doc/proof-engine.md
parent9043add656177eeac1491a73d2f3ab92bec0013c (diff)
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'dev/doc/proof-engine.md')
-rw-r--r--dev/doc/proof-engine.md31
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