procedural: added fwd rewrite in arbitrary proofs (not just premises)

[helm.git] / helm / software / components / content_pres / proceduralTypes.ml

diff --git a/helm/software/components/content_pres/proceduralTypes.ml b/helm/software/components/content_pres/proceduralTypes.ml
index 0ef73e2488d84b170a45f23f1edfc0e8d5c1ce9d..b7f6d3c6b68b2baf49909f448e86c5aa2f83e3e4 100644 (file)
--- a/helm/software/components/content_pres/proceduralTypes.ml
+++ b/helm/software/components/content_pres/proceduralTypes.ml
@@ -75,6 +75,7 @@ type step = Note of note
          | Rewrite of how * what * where * note
          | Elim of what * using option * note
          | Apply of what * note
+         | Whd of count * note
          | Branch of step list list * note
 
 (* annterm constructors *****************************************************)
@@ -85,6 +86,8 @@ let mk_arel i b = Cic.ARel ("", "", i, b)
 
 let floc = H.dummy_floc
 
+let hole = C.AImplicit ("", Some `Hole)
+
 let mk_note str = G.Comment (floc, G.Note (floc, str))
 
 let mk_theorem name t = 
@@ -114,7 +117,6 @@ let mk_letin name what =
    mk_tactic tactic
 
 let mk_rewrite direction what where =
-   let hole = C.AImplicit ("", Some `Hole) in
    let direction = if direction then `RightToLeft else `LeftToRight in 
    let pattern, rename = match where with
       | None                 -> (None, [], Some hole), []
@@ -131,6 +133,11 @@ let mk_apply t =
    let tactic = G.Apply (floc, t) in
    mk_tactic tactic
 
+let mk_whd i =
+   let pattern = None, [], Some hole in
+   let tactic = G.Reduce (floc, `Whd, pattern) in
+   mk_tactic tactic
+
 let mk_dot = G.Executable (floc, G.Tactical (floc, G.Dot floc, None))
 
 let mk_sc = G.Executable (floc, G.Tactical (floc, G.Semicolon floc, None))
@@ -154,6 +161,7 @@ let rec render_step sep a = function
    | Rewrite (b, t, w, s) -> mk_note s :: cont sep (mk_rewrite b t w :: a)
    | Elim (t, xu, s)      -> mk_note s :: cont sep (mk_elim t xu :: a)
    | Apply (t, s)         -> mk_note s :: cont sep (mk_apply t :: a)
+   | Whd (c, s)           -> mk_note s :: cont sep (mk_whd c :: a)
    | Branch ([], s)       -> a
    | Branch ([ps], s)     -> render_steps sep a ps
    | Branch (pss, s)      ->