X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=c4ec503c797a2418b66ea0dcfc8c39359f747b80;hb=489639a3c319d0349a9c864fd0eeaf659daa3d3f;hp=2d55e8634fd73bd88b44ee9ede5ae07e158ad84e;hpb=91d21783f8ef99251f1868ea286c395d7f653ac5;p=helm.git

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index 2d55e8634..c4ec503c7 100644
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -36,6 +36,8 @@ type npattern =
 
 type auto_params = nterm list option * (string*string) list
 
+type just = [`Term of nterm | `Auto of auto_params]
+
 type ntactic =
    | NApply of loc * nterm
    | NSmartApply of loc * nterm
@@ -75,6 +77,37 @@ type ntactic =
    | NAssumption of loc
    | NRepeat of loc * ntactic
    | NBlock of loc * ntactic list
+   (* Declarative langauge *)
+   (* Not the best idea to use a string directly, an abstract type for identifiers would be better *)
+   | Assume of loc * string * nterm * nterm option (* loc, identifier, type, eqty *)
+   | Suppose of loc * nterm *string * nterm option (* loc, assumption, identifier, eqass *)
+   | By_just_we_proved of loc * just * nterm * string option * nterm option (* loc,
+   justification, conclusion, identifier, eqconcl *)
+   | We_need_to_prove of loc * nterm * string option * nterm option (* loc, newconclusion,
+   identifier, equivnewcon *)
+   | Bydone of loc * just
+   | ExistsElim of loc * just * string * nterm * nterm * string
+   | AndElim of loc * just * nterm * string * nterm * string
+                (*
+   | RewritingStep of
+      loc * (string option * nterm) option * nterm *
+       [ `Term of nterm | `Auto of auto_params
+       | `Proof | `SolveWith of nterm ] *
+       bool (* last step*)
+                   *)
+   | RewritingStep of
+      loc * nterm * [ `Term of nterm | `Auto of auto_params | `Proof | `SolveWith of nterm ] * bool (* last step*)
+   | Obtain of
+      loc * string * nterm
+   | Conclude of
+      loc * nterm
+   | Thesisbecomes of loc * nterm * nterm option
+   | We_proceed_by_induction_on of loc * nterm * nterm
+   | We_proceed_by_cases_on of loc * nterm * nterm
+   | Byinduction of loc * nterm * string
+   | Case of loc * string * (string * nterm) list 
+    (* This is a debug tactic to print the stack to stdout, can be safely removed *)
+   | PrintStack of loc 
 
 type nmacro =
   | NCheck of loc * nterm
@@ -84,7 +117,7 @@ type nmacro =
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 36
+let magic = 37
 
 (* composed magic: term + command magics. No need to change this value *)
 let magic = magic + 10000 * NotationPt.magic
@@ -99,10 +132,10 @@ type inclusion_mode = WithPreferences | WithoutPreferences | OnlyPreferences (*
 type command =
   | Include of loc * inclusion_mode * string (* _,buri,_,path *)
   | UnificationHint of loc * nterm * int (* term, precedence *)
-  | NObj of loc * nterm NotationPt.obj
+  | NObj of loc * nterm NotationPt.obj * bool
   | NDiscriminator of loc * nterm
   | NInverter of loc * string * nterm * bool list option * nterm option
-  | NUnivConstraint of loc * NUri.uri * NUri.uri
+  | NUnivConstraint of loc * bool * NUri.uri * NUri.uri
   | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
   | NCoercion of loc * string * bool * 
       (nterm * nterm * (string * nterm) * nterm) option