Big commit and major code clean-up:

[helm.git] / helm / ocaml / cic_transformations / tacticAst.ml

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index d4e94b28bea16ce511ca4341b6489378becedde4..fab264d0798748b842c00733245074af5930cc33 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -24,7 +24,7 @@
  *)
 
 type direction = [ `Left | `Right ]
-type reduction_kind = [ `Reduce | `Simpl | `Whd ]
+type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ]
 (* type 'term pattern = Pattern of 'term *)
 
   (* everywhere includes goal and hypotheses *)
@@ -38,7 +38,7 @@ type loc = CicAst.location
 type ('term, 'ident) tactic =
   | Absurd of loc * 'term
   | Apply of loc * 'term
-  | Auto of loc
+  | 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
@@ -60,6 +60,7 @@ type ('term, 'ident) tactic =
   | 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,
@@ -92,14 +93,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,23 +116,30 @@ 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
+  | 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
@@ -139,11 +153,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