* http://helm.cs.unibo.it/
*)
-type direction = [ `Left | `Right ]
-type reduction_kind = [ `Reduce | `Simpl | `Whd ]
-(* type 'term pattern = Pattern of 'term *)
-
- (* everywhere includes goal and hypotheses *)
-type 'term pattern = [ `Goal | `Everywhere ]
-
- (* when an 'ident option is None, the default is to apply the tactic
- to the current goal *)
+type direction = [ `LeftToRight | `RightToLeft ]
+type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ]
type loc = CicAst.location
+type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term
+
type ('term, 'ident) tactic =
| Absurd of loc * 'term
| Apply of loc * 'term
- | Auto of loc * int option
| Assumption of loc
- | Change of loc * 'term * 'term * 'ident option (* what, with what, where *)
- | Change_pattern of loc * 'term pattern * 'term * 'ident option
- (* what, with what, where *)
+ | Auto of loc * int option * int option (* depth, width *)
+ | Change of loc * ('term,'ident) pattern * 'term
+ | Clear of loc * 'ident
+ | ClearBody of loc * 'ident
+ | Compare of loc * 'term
+ | Constructor of loc * int
| Contradiction of loc
- | Cut of loc * 'term
- | Decompose of loc * 'ident * 'ident list (* where, which principles *)
- | Discriminate of loc * 'ident
- | Elim of loc * 'term * 'term option (* what to elim, which principle to use *)
- | ElimType of loc * 'term
+ | Cut of loc * 'ident option * 'term
+ | DecideEquality of loc
+ | Decompose of loc * 'term
+ | Discriminate of loc * 'term
+ | Elim of loc * 'term * 'term option * int option * 'ident list
+ | ElimType of loc * 'term * 'term option * int option * 'ident list
| Exact of loc * 'term
| Exists of loc
- | Fold of loc * reduction_kind * 'term
+ | Fail of loc
+ | Fold of loc * reduction_kind * 'term * ('term, 'ident) pattern
| Fourier of loc
+ | FwdSimpl of loc * string * 'ident list
+ | Generalize of loc * ('term, 'ident) pattern * 'ident option
| Goal of loc * int (* change current goal, argument is goal number 1-based *)
- | Injection of loc * 'ident
+ | IdTac of loc
+ | Injection of loc * 'term
| Intros of loc * int option * 'ident list
+ | LApply of loc * int option * 'term list * 'term * 'ident option
| Left of loc
| LetIn of loc * 'term * 'ident
-(* | Named_intros of loc * 'ident list (* joined with Intros above *) *)
-(* | Reduce of loc * reduction_kind * 'term pattern * 'ident option (* what, where *) *)
- | Reduce of loc * reduction_kind * ('term list * 'term pattern) option
- (* kind, (what, where)
- * if second argument is None, reduction is applied to the current goal,
- * otherwise to each occurrence of loc * terms given in list occuring in term
- * pattern *)
+ | Reduce of loc * reduction_kind * ('term, 'ident) pattern
| Reflexivity of loc
- | Replace of loc * 'term * 'term (* what, with what *)
- | Replace_pattern of loc * 'term pattern * 'term
- | Rewrite of loc * direction * 'term * 'ident option
+ | Replace of loc * ('term, 'ident) pattern * 'term
+ | Rewrite of loc * direction * 'term * ('term, 'ident) pattern
| Right of loc
| Ring of loc
| Split of loc
type print_kind = [ `Env | `Coer ]
type 'term macro =
- | Abort of loc
+ (* Whelp's stuff *)
+ | WHint of loc * 'term
+ | WMatch of loc * 'term
+ | WInstance of loc * 'term
+ | WLocate of loc * string
+ | WElim of loc * 'term
+ (* real macros *)
+(* | Abort of loc *)
| Print of loc * string
| Check of loc * 'term
| Hint of loc
- | Match of loc * 'term
- | Instance of loc * 'term
| Quit of loc
- | Redo of loc * int option
- | Undo of loc * int option
+(* | Redo of loc * int option
+ | Undo of loc * int option *)
(* | Print of loc * print_kind *)
| Search_pat of loc * search_kind * string (* searches with string pattern *)
| Search_term of loc * search_kind * 'term (* searches with term pattern *)
| Symbol_alias of string * int * string (* name, instance no, description *)
| Number_alias of int * string (* instance no, description *)
-type 'term command =
- | Set of loc * string * string
- | Qed of loc
- (** name.
- * Name is needed when theorem was started without providing a name
- *)
- | Inductive of loc * (string * 'term) list * 'term inductive_type list
+type obj =
+ | Inductive of (string * CicAst.term) list * CicAst.term inductive_type list
(** parameters, list of loc * mutual inductive types *)
- | Theorem of loc * thm_flavour * string option * 'term * 'term option
+ | Theorem of thm_flavour * string * CicAst.term * CicAst.term option
(** flavour, name, type, body
* - name is absent when an unnamed theorem is being proved, tipically in
* interactive usage
* - body is present when its given along with the command, otherwise it
* will be given in proof editing mode using the tactical language
*)
+ | Record of
+ (string * CicAst.term) list * string * CicAst.term *
+ (string * CicAst.term) list
+
+type ('term,'obj) command =
+ | Default of loc * string * UriManager.uri list
+ | Include of loc * string
+ | Set of loc * string * string
+ | Drop of loc
+ | Qed of loc
+ (** name.
+ * Name is needed when theorem was started without providing a name
+ *)
| Coercion of loc * 'term
| Alias of loc * alias_spec
+ (** parameters, name, type, fields *)
+ | Obj of loc * 'obj
type ('term, 'ident) tactical =
| Tactic of loc * ('term, 'ident) tactic
- | Fail of loc
| Do of loc * int * ('term, 'ident) tactical
- | IdTac of loc
| 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
- | Tries of loc * ('term, 'ident) tactical list
+ | First of loc * ('term, '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
-type ('term, 'ident) code =
- | Command of loc * 'term command
+type ('term, 'obj, 'ident) code =
+ | Command of loc * ('term,'obj) command
| Macro of loc * 'term macro
(* Macro are substantially queries, but since we are not the kind of
* peolpe that like to push "start" to turn off the computer
* we added this command *)
| Tactical of loc * ('term, 'ident) tactical
-type ('term, 'ident) comment =
+type ('term, 'obj, 'ident) comment =
| Note of loc * string
- | Code of loc * ('term, 'ident) code
+ | Code of loc * ('term, 'obj, 'ident) code
-type ('term, 'ident) statement =
- | Executable of loc * ('term, 'ident) code
- | Comment of loc * ('term, 'ident) comment
+type ('term, 'obj, 'ident) statement =
+ | Executable of loc * ('term, 'obj, 'ident) code
+ | Comment of loc * ('term, 'obj, 'ident) comment
projects / helm.git / blobdiff