bugfix: avoid losing attributes on boxes which have a single children

[helm.git] / helm / ocaml / cic_notation / grafiteAst.ml

diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml
index 7d09e2d6a5933c53c59035d6be3764a219205987..82d90498989cabec1ac8209a22b6042135649e8f 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteAst.ml
+++ b/helm/ocaml/cic_notation/grafiteAst.ml
@@ -23,18 +23,25 @@
  * http://helm.cs.unibo.it/
  *)
 
+module Ast = CicNotationPt
+
 type direction = [ `LeftToRight | `RightToLeft ]
-type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ]
+type 'term reduction_kind =
+ [ `Normalize | `Reduce | `Simpl | `Unfold of 'term option | `Whd ]
 
-type loc = CicNotationPt.location
+type loc = Ast.location
 
 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 =
   | Absurd of loc * 'term
   | Apply of loc * 'term
   | Assumption of loc
-  | Auto of loc * int option * int option (* depth, width *)
+  | 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
@@ -43,14 +50,14 @@ type ('term, 'ident) tactic =
   | Contradiction of loc
   | Cut of loc * 'ident option * 'term
   | DecideEquality of loc
-  | Decompose of loc * 'term
+  | 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
+  | Fold of loc * 'term reduction_kind * 'term * ('term, 'ident) pattern
   | Fourier of loc
   | FwdSimpl of loc * string * 'ident list
   | Generalize of loc * ('term, 'ident) pattern * 'ident option
@@ -61,7 +68,7 @@ type ('term, 'ident) tactic =
   | 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 
+  | Reduce of loc * 'term reduction_kind * ('term, 'ident) pattern 
   | Reflexivity of loc
   | Replace of loc * ('term, 'ident) pattern * 'term
   | Rewrite of loc * direction * 'term * ('term, 'ident) pattern
@@ -106,19 +113,19 @@ type alias_spec =
   | Number_alias of int * string          (* instance no, description *)
 
 type obj =
-  | Inductive of (string * CicNotationPt.term) list *
-      CicNotationPt.term inductive_type list
+  | Inductive of (string * Ast.term) list *
+      Ast.term inductive_type list
       (** parameters, list of loc * mutual inductive types *)
-  | Theorem of thm_flavour * string * CicNotationPt.term *
-      CicNotationPt.term option
+  | Theorem of thm_flavour * string * Ast.term *
+      Ast.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 * CicNotationPt.term) list * string * CicNotationPt.term *
-      (string * CicNotationPt.term) list
+  | Record of (string * Ast.term) list * string * Ast.term *
+      (string * Ast.term) list
 
 type ('term,'obj) command =
   | Default of loc * string * UriManager.uri list
@@ -133,12 +140,12 @@ type ('term,'obj) command =
   | Alias of loc * alias_spec
       (** parameters, name, type, fields *) 
   | Obj of loc * 'obj
-  | Notation of loc * CicNotationPt.term * Gramext.g_assoc option * int option *
-      CicNotationPt.term
-      (* level 1 pattern, associativity, precedence, level 2 pattern *)
+  | Notation of loc * direction option * Ast.term * Gramext.g_assoc *
+      int * Ast.term
+      (* direction, l1 pattern, associativity, precedence, l2 pattern *)
   | Interpretation of loc *
-      string * (string * CicNotationPt.argument_pattern list) *
-        CicNotationPt.cic_appl_pattern
+      string * (string * Ast.argument_pattern list) *
+        Ast.cic_appl_pattern
       (* description (i.e. id), symbol, arg pattern, appl pattern *)
 
     (* DEBUGGING *)