type note = string
type where = (name * name) option
type inferred = Cic.annterm
+type pattern = Cic.annterm
type step = Note of note
| Theorem of name * what * note
| Intros of count option * name list * note
| Cut of name * what * note
| LetIn of name * what * note
- | Rewrite of how * what * where * note
+ | Rewrite of how * what * where * pattern * note
| Elim of what * using option * note
| Apply of what * note
- | Change of inferred * what * where * note
+ | Change of inferred * what * where * pattern * note
| ClearBody of name * note
| Branch of step list list * note
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 =
let tactic = G.LetIn (floc, what, name) in
mk_tactic tactic
-let mk_rewrite direction what where =
+let mk_rewrite direction what where pattern =
let direction = if direction then `RightToLeft else `LeftToRight in
let pattern, rename = match where with
- | None -> (None, [], Some hole), []
- | Some (premise, name) -> (None, [premise, hole], None), [name]
+ | None -> (None, [], Some pattern), []
+ | Some (premise, name) -> (None, [premise, pattern], None), [name]
in
let tactic = G.Rewrite (floc, direction, what, pattern, rename) in
mk_tactic tactic
let tactic = G.Apply (floc, t) in
mk_tactic tactic
-let mk_change t where =
+let mk_change t where pattern =
let pattern = match where with
- | None -> None, [], Some hole
- | Some (premise, _) -> None, [premise, hole], None
+ | None -> None, [], Some pattern
+ | Some (premise, _) -> None, [premise, pattern], None
in
let tactic = G.Change (floc, pattern, t) in
mk_tactic tactic
(* rendering ****************************************************************)
let rec render_step sep a = function
- | Note s -> mk_note s :: a
- | Theorem (n, t, s) -> mk_note s :: mk_theorem n t :: a
- | Qed s -> (* mk_note s :: *) mk_qed :: a
- | Id s -> mk_note s :: cont sep (mk_id :: a)
- | Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a)
- | Cut (n, t, s) -> mk_note s :: cont sep (mk_cut n t :: a)
- | LetIn (n, t, s) -> mk_note s :: cont sep (mk_letin n t :: a)
- | 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)
- | Change (t, _, w, s) -> mk_note s :: cont sep (mk_change t w :: a)
- | ClearBody (n, s) -> mk_note s :: cont sep (mk_clearbody n :: a)
- | Branch ([], s) -> a
- | Branch ([ps], s) -> render_steps sep a ps
- | Branch (pss, s) ->
+ | Note s -> mk_note s :: a
+ | Theorem (n, t, s) -> mk_note s :: mk_theorem n t :: a
+ | Qed s -> (* mk_note s :: *) mk_qed :: a
+ | Id s -> mk_note s :: cont sep (mk_id :: a)
+ | Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a)
+ | Cut (n, t, s) -> mk_note s :: cont sep (mk_cut n t :: a)
+ | LetIn (n, t, s) -> mk_note s :: cont sep (mk_letin n t :: a)
+ | Rewrite (b, t, w, e, s) -> mk_note s :: cont sep (mk_rewrite b t w e :: 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)
+ | Change (t, _, w, e, s) -> mk_note s :: cont sep (mk_change t w e :: a)
+ | ClearBody (n, s) -> mk_note s :: cont sep (mk_clearbody n :: a)
+ | Branch ([], s) -> a
+ | Branch ([ps], s) -> render_steps sep a ps
+ | Branch (pss, s) ->
let a = mk_ob :: a in
let body = mk_cb :: list_rev_map_concat (render_steps None) mk_vb a pss in
mk_note s :: cont sep body