module Ast = CicNotationPt
type direction = [ `LeftToRight | `RightToLeft ]
-type 'term reduction_kind =
- [ `Normalize | `Reduce | `Simpl | `Unfold of 'term option | `Whd ]
type loc = Ast.location
-type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term
+type ('term, 'lazy_term, 'ident) pattern =
+ 'lazy_term option * ('ident * 'term) list * 'term
type ('term, 'ident) type_spec =
| Ident of 'ident
| Type of UriManager.uri * int
-type ('term, 'ident) tactic =
+type reduction =
+ [ `Normalize
+ | `Reduce
+ | `Simpl
+ | `Unfold of CicNotationPt.term option
+ | `Whd ]
+
+type ('term, 'lazy_term, 'reduction, 'ident) tactic =
| Absurd of loc * 'term
| Apply of loc * 'term
| Assumption of loc
- | Auto of loc * int option * int option * string option (* depth, width, paramodulation ALB *)
- | Change of loc * ('term,'ident) pattern * 'term
+ | Auto of loc * int option * int option * string option
+ (* depth, width, paramodulation *)
+ | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
| Clear of loc * 'ident
| ClearBody of loc * 'ident
| Compare of loc * 'term
| Exact of loc * 'term
| Exists of loc
| Fail of loc
- | Fold of loc * 'term reduction_kind * 'term * ('term, 'ident) pattern
+ | Fold of loc * 'reduction * 'lazy_term * ('term, 'lazy_term, 'ident) pattern
| Fourier of loc
| FwdSimpl of loc * string * 'ident list
- | Generalize of loc * ('term, 'ident) pattern * 'ident option
+ | Generalize of loc * ('term, 'lazy_term, 'ident) pattern * 'ident option
| Goal of loc * int (* change current goal, argument is goal number 1-based *)
| IdTac of loc
| Injection of loc * 'term
| LApply of loc * int option * 'term list * 'term * 'ident option
| Left of loc
| LetIn of loc * 'term * 'ident
- | Reduce of loc * 'term reduction_kind * ('term, 'ident) pattern
+ | Reduce of loc * 'reduction * ('term, 'lazy_term, 'ident) pattern
| Reflexivity of loc
- | Replace of loc * ('term, 'ident) pattern * 'term
- | Rewrite of loc * direction * 'term * ('term, 'ident) pattern
+ | Replace of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
+ | Rewrite of loc * direction * 'term *
+ ('term, 'lazy_term, 'ident) pattern
| Right of loc
| Ring of loc
| Split of loc
(* DEBUGGING *)
| Render of loc * UriManager.uri (* render library object *)
-type ('term, 'ident) tactical =
- | Tactic of loc * ('term, 'ident) tactic
- | Do of loc * int * ('term, 'ident) tactical
- | Repeat of loc * ('term, 'ident) tactical
- | Seq of loc * ('term, 'ident) tactical list (* sequential composition *)
- | Then of loc * ('term, 'ident) tactical * ('term, 'ident) tactical list
- | First of loc * ('term, 'ident) tactical list
+type ('term, 'lazy_term, 'reduction, 'ident) tactical =
+ | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
+ | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactical
+ | Repeat of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
+ | Seq of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list
+ (* sequential composition *)
+ | Then of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical *
+ ('term, 'lazy_term, 'reduction, 'ident) tactical list
+ | First of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list
(* try a sequence of loc * tacticals until one succeeds, fail otherwise *)
- | Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *)
- | Solve of loc * ('term, 'ident) tactical list
+ | Try of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
+ (* try a tactical and mask failures *)
+ | Solve of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list
-type ('term, 'obj, 'ident) code =
+type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code =
| Command of loc * ('term,'obj) command
| Macro of loc * 'term macro
- | Tactical of loc * ('term, 'ident) tactical
+ | Tactical of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
-type ('term, 'obj, 'ident) comment =
+type ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment =
| Note of loc * string
- | Code of loc * ('term, 'obj, 'ident) code
+ | Code of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code
-type ('term, 'obj, 'ident) statement =
- | Executable of loc * ('term, 'obj, 'ident) code
- | Comment of loc * ('term, 'obj, 'ident) comment
+type ('term, 'lazy_term, 'reduction, 'obj, 'ident) statement =
+ | Executable of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code
+ | Comment of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment