X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst.ml;h=48fbc4aa2115d9800e702ba8a1515beb7bbbc93a;hb=577cd769f88edc9aa851f117df7f83909c95a06c;hp=8c678de93ba9d9fe6d0d91e2ac1d362efe03437d;hpb=9701a8bee17d66e49a5cff28dc62963c54fadc6b;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 8c678de93..48fbc4aa2 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -23,66 +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 ('term, 'ident) type_spec =
+   | Ident of 'ident
+   | Type of UriManager.uri * int 
 
 type ('term, 'ident) tactic =
-  | LocatedTactic of CicAst.location * ('term, 'ident) tactic
-
-  | Absurd of 'term
-  | Apply of 'term
-  | Auto
-  | Assumption
-  | Change of 'term * 'term * 'ident option (* what, with what, where *)
-  | Change_pattern of 'term pattern * 'term * 'ident option
-      (* what, with what, where *)
-  | Contradiction
-  | Cut of 'term
-  | Decompose of 'ident * 'ident list (* where, which principles *)
-  | Discriminate of 'ident
-  | Elim of 'term * 'term option (* what to elim, which principle to use *)
-  | ElimType of 'term
-  | Exact of 'term
-  | Exists
-  | Fold of reduction_kind * 'term
-  | Fourier
-  | Hint
-  | Injection of 'ident
-  | Intros of int option * 'ident list
-  | Left
-  | LetIn of 'term * 'ident
-(*   | Named_intros of 'ident list (* joined with Intros above *) *)
-(*   | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *) *)
-  | Reduce of 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 terms given in list occuring in term
-      * pattern *)
-  | Reflexivity
-  | Replace of 'term * 'term (* what, with what *)
-  | Replace_pattern of 'term pattern * 'term
-  | Rewrite of direction * 'term * 'ident option
-  | Right
-  | Ring
-  | Split
-  | Symmetry
-  | Transitivity of 'term
-
-type thm_flavour =
-  [ `Definition
-  | `Fact
-  | `Goal
-  | `Lemma
-  | `Remark
-  | `Theorem
-  ]
+  | Absurd of loc * 'term
+  | Apply of loc * 'term
+  | Assumption of loc
+  | 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 * '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
+  | 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 *)
+  | 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
+  | Reduce of loc * reduction_kind * ('term, 'ident) pattern 
+  | Reflexivity of loc
+  | 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 = Cic.object_flavour
 
   (** <name, inductive/coinductive, type, constructor list>
   * true means inductive, false coinductive *)
@@ -90,43 +83,85 @@ type 'term inductive_type = string * bool * 'term * (string * 'term) list
 
 type search_kind = [ `Locate | `Hint | `Match | `Elim ]
 
-type 'term command =
-  | Abort
-  | Baseuri of string option (** get/set base uri *)
-  | Check of 'term
-  | Search_pat of search_kind * string  (* searches with string pattern *)
-  | Search_term of search_kind * 'term  (* searches with term pattern *)
-  | Proof
-  | Qed of string option
-      (** name.
-       * Name is needed when theorem was started without providing a name
-       *)
-  | Quit
-  | Inductive of (string * 'term) list * 'term inductive_type list
-      (** parameters, list of mutual inductive types *)
-  | Theorem of thm_flavour * string option * 'term * 'term option
+type print_kind = [ `Env | `Coer ]
+
+type 'term macro = 
+  (* 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
+  | Quit of loc
+(*   | 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 *)
+
+type alias_spec =
+  | Ident_alias of string * string        (* identifier, uri *)
+  | Symbol_alias of string * int * string (* name, instance no, description *)
+  | Number_alias of int * string          (* instance no, description *)
+
+type obj =
+  | Inductive of (string * CicAst.term) list * CicAst.term inductive_type list
+      (** parameters, list of loc * mutual inductive types *)
+  | 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
        *)
-  | Redo of int option
-  | Undo of int option
+  | 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 =
-  | LocatedTactical of CicAst.location * ('term, 'ident) tactical
-
-  | Tactic of ('term, 'ident) tactic
-  | Command of 'term command
-
-  | Fail
-  | Do of int * ('term, 'ident) tactical
-  | IdTac
-  | Repeat of ('term, 'ident) tactical
-  | Seq of ('term, 'ident) tactical list (* sequential composition *)
-  | Then of ('term, 'ident) tactical * ('term, 'ident) tactical list
-  | Tries of ('term, 'ident) tactical list
-      (* try a sequence of tacticals until one succeeds, fail otherwise *)
-  | Try of ('term, 'ident) tactical (* try a tactical and mask failures *)
+  | 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
+      (* 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, '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