X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst.ml;h=fab264d0798748b842c00733245074af5930cc33;hb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;hp=f0dad83e23b828372be01a031e8f1eeb71fac101;hpb=511f0c1672e0db4cf577afc9b79f12dea39469ad;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index f0dad83e2..fab264d07 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -24,84 +24,149 @@
  *)
 
 type direction = [ `Left | `Right ]
-type reduction_kind = [ `Reduce | `Simpl | `Whd ]
-type 'term pattern = Pattern of 'term
+type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ]
+(* 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 ('term, 'ident) tactic =
-  | LocatedTactic of CicAst.location * ('term, 'ident) tactic
+type loc = CicAst.location
 
-  | Absurd
-  | Apply of 'term
-  | Assumption
-  | Change of 'term * 'term * 'ident option (* what, with what, where *)
-  | Change_pattern of 'term pattern * 'term * 'ident option
+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 *)
-  | 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
-  | 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 *)
-  | 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
+  | 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
+  | Exact of loc * 'term
+  | Exists of loc
+  | Fold of loc * reduction_kind * 'term
+  | Fourier of loc
+  | Goal of loc * int (* change current goal, argument is goal number 1-based *)
+  | Injection of loc * 'ident
+  | Intros of loc * int option * 'ident list
+  | 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 *) *)
+  | ReduceAt of loc * reduction_kind * 'ident * 'term
+  | 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 *)
+  | 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
+  | Right of loc
+  | Ring of loc
+  | Split of loc
+  | Symmetry of loc
+  | Transitivity of loc * 'term
 
 type thm_flavour =
   [ `Definition
   | `Fact
-  | `Goal
   | `Lemma
   | `Remark
   | `Theorem
   ]
 
-type 'term command =
-  | Proof
-  | Theorem of thm_flavour * string option * 'term * 'term option
-      (* flavour, name, type, body
+  (** <name, inductive/coinductive, type, constructor list>
+  * true means inductive, false coinductive *)
+type 'term inductive_type = string * bool * 'term * (string * 'term) list
+
+type search_kind = [ `Locate | `Hint | `Match | `Elim ]
+
+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
        *)
-  | Qed of string option
-      (* name.
+  | Record of
+     (string * CicAst.term) list * string * CicAst.term *
+      (string * CicAst.term) list
+
+type ('term,'obj) command =
+  | Set of loc * string * string
+  | Qed of loc
+      (** name.
        * Name is needed when theorem was started without providing a name
        *)
-  | Quit
+  | 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
+  | 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
+      (* 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, '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