X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst.ml;h=3f4d4226f96fe5f19f40cb75495cae1a7707a9a2;hb=d43002dfc61afac676ea14bc6a1418e5ec0e3e9c;hp=ae9143dabf849ed29f1d9c5c9e41b2f8114c9230;hpb=bc36fe01d5465d07ef76c445c83639e341f3eb2a;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index ae9143dab..3f4d4226f 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -23,65 +23,59 @@
  * http://helm.cs.unibo.it/
  *)
 
-type direction = [ `Left | `Right ]
-type reduction_kind = [ `Reduce | `Simpl | `Whd ]
-(* type 'term pattern = Pattern of 'term *)
+type direction = [ `LeftToRight | `RightToLeft ]
+type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ]
 
-  (* everywhere includes goal and hypotheses *)
-type 'term pattern = [ `Goal | `Everywhere ]
+type loc = CicAst.location
 
-  (* when an 'ident option is None, the default is to apply the tactic
-  to the current goal *)
+type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term
 
-type loc = CicAst.location
+type ('term, 'ident) type_spec =
+   | Ident of 'ident
+   | Type of UriManager.uri * int 
 
 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 * string option (* depth, width, paramodulation ALB *)
+  | 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, 'ident) type_spec list * 'ident * 'ident list
+  | 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
   | Symmetry of loc
   | Transitivity of loc * 'term
 
-type thm_flavour =
-  [ `Definition
-  | `Fact
-  | `Lemma
-  | `Remark
-  | `Theorem
-  ]
+type thm_flavour = Cic.object_flavour
 
   (** <name, inductive/coinductive, type, constructor list>
   * true means inductive, false coinductive *)
@@ -99,13 +93,13 @@ type 'term macro =
   | WLocate of loc * string
   | WElim of loc * 'term
   (* real macros *)
-  | Abort of loc
+(*   | Abort of loc *)
   | Print of loc * string
   | Check of loc * 'term 
   | Hint of loc
   | 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 *)
@@ -115,50 +109,59 @@ 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 =
+  | 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