X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst.ml;h=191323599638b3937ec47bd79adf7a07e58c2b5c;hb=bc9cc53fbb0cb8676106e0c4d74053bbe1ac1a8e;hp=d4e94b28bea16ce511ca4341b6489378becedde4;hpb=e937a197c1123e9adc6b2036ae47c7952ebbf138;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index d4e94b28b..191323599 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -24,51 +24,48 @@
  *)
 
 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 reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ]
 
 type loc = CicAst.location
 
+type ('term, 'ident) pattern =
+  ('ident * 'term) list * 'term option
+
 type ('term, 'ident) tactic =
   | Absurd of loc * 'term
   | Apply of loc * 'term
-  | Auto of loc
   | 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 * 'term * ('term,'ident) pattern (* what, with what, where *)
+  | 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
+  | Cut of loc * 'ident option * 'term
+  | DecideEquality of loc
+  | Decompose of loc * 'term
+  | Discriminate of loc * 'term
   | Elim of loc * 'term * 'term option (* what to elim, which principle to use *)
   | ElimType of loc * 'term
   | 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 * 'term
+  | Generalize of loc * 'term * 'ident option * ('term, 'ident) pattern
   | 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 * 'term option * '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
@@ -92,14 +89,20 @@ type search_kind = [ `Locate | `Hint | `Match | `Elim ]
 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 
   | 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 *)
@@ -109,29 +112,35 @@ type alias_spec =
   | 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 =
+  | 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
@@ -139,11 +148,20 @@ type ('term, 'ident) tactical =
       (* try a sequence of loc * tacticals until one succeeds, fail otherwise *)
   | Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *)
 
-type ('term, 'ident) statement =
-  | 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, 'obj, 'ident) comment =
+  | Note of loc * string
+  | Code of loc * ('term, 'obj, 'ident) code
+             
+type ('term, 'obj, 'ident) statement =
+  | Executable of loc * ('term, 'obj, 'ident) code
+  | Comment of loc * ('term, 'obj, 'ident) comment