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

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index e32131a06..c4ec503c7 100644
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -29,33 +29,38 @@ type direction = [ `LeftToRight | `RightToLeft ]
 
 type loc = Stdpp.location
 
+type nterm = NotationPt.term
+
 type npattern = 
- NotationPt.term option * (string * NotationPt.term) list * NotationPt.term option
+ nterm option * (string * nterm) list * nterm option
+
+type auto_params = nterm list option * (string*string) list
 
-type auto_params = NotationPt.term list option * (string*string) list
+type just = [`Term of nterm | `Auto of auto_params]
 
 type ntactic =
-   | NApply of loc * NotationPt.term
-   | NSmartApply of loc * NotationPt.term
-   | NAssert of loc * ((string * [`Decl of NotationPt.term | `Def of NotationPt.term * NotationPt.term]) list * NotationPt.term) list
-   | NCases of loc * NotationPt.term * npattern  
+   | NApply of loc * nterm
+   | NSmartApply of loc * nterm
+   | NAssert of loc * ((string * [`Decl of nterm | `Def of nterm * nterm]) list * nterm) list
+   | NCases of loc * nterm * npattern  
    | NCase1 of loc * string
-   | NChange of loc * npattern * NotationPt.term
-   | NConstructor of loc * int option * NotationPt.term list
-   | NCut of loc * NotationPt.term
-(* | NDiscriminate of loc * NotationPt.term
-   | NSubst of loc * NotationPt.term *)
+   | NChange of loc * npattern * nterm
+   | NClear of loc * string list
+   | NConstructor of loc * int option * nterm list
+   | NCut of loc * nterm
+(* | NDiscriminate of loc * nterm
+   | NSubst of loc * nterm *)
    | NDestruct of loc * string list option * string list
-   | NElim of loc * NotationPt.term * npattern  
+   | NElim of loc * nterm * npattern  
    | NGeneralize of loc * npattern
    | NId of loc
    | NIntro of loc * string
    | NIntros of loc * string list
-   | NInversion of loc * NotationPt.term * npattern  
-   | NLApply of loc * NotationPt.term
-   | NLetIn of loc * npattern * NotationPt.term * string
+   | NInversion of loc * nterm * npattern  
+   | NLApply of loc * nterm
+   | NLetIn of loc * npattern * nterm * string
    | NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern
-   | NRewrite of loc * direction * NotationPt.term * npattern
+   | NRewrite of loc * direction * nterm * npattern
    | NAuto of loc * auto_params
    | NDot of loc
    | NSemicolon of loc
@@ -72,37 +77,82 @@ 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 * NotationPt.term
+  | NCheck of loc * nterm
   | Screenshot of loc * string
   | NAutoInteractive of loc * auto_params
   | NIntroGuess of loc
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 35
+let magic = 37
+
+(* composed magic: term + command magics. No need to change this value *)
+let magic = magic + 10000 * NotationPt.magic
+
+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 inclusion_mode = WithPreferences | WithoutPreferences | OnlyPreferences (* aka aliases *)
 
 type command =
-  | Include of loc * string 
-  | Set of loc * string * string
-  | Print of loc * string
-
-type ncommand =
-  | UnificationHint of loc * NotationPt.term * int (* term, precedence *)
-  | NObj of loc * NotationPt.term NotationPt.obj
-  | NDiscriminator of loc * NotationPt.term
-  | NInverter of loc * string * NotationPt.term * bool list option * NotationPt.term option
-  | NUnivConstraint of loc * NUri.uri * NUri.uri
+  | Include of loc * inclusion_mode * string (* _,buri,_,path *)
+  | UnificationHint of loc * nterm * int (* term, precedence *)
+  | NObj of loc * nterm NotationPt.obj * bool
+  | NDiscriminator of loc * nterm
+  | NInverter of loc * string * nterm * bool list option * nterm option
+  | NUnivConstraint of loc * bool * NUri.uri * NUri.uri
   | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
-  | NCoercion of loc * string *
-      NotationPt.term * NotationPt.term *
-      (string * NotationPt.term) * NotationPt.term
-  | NQed of loc
+  | NCoercion of loc * string * bool * 
+      (nterm * nterm * (string * nterm) * nterm) option
+  | NQed of loc * bool
+  (* ex lexicon commands *)
+  | Alias of loc * alias_spec
+      (** parameters, name, type, fields *) 
+  | Notation of loc * direction option * nterm * Gramext.g_assoc *
+      int * nterm
+      (* direction, l1 pattern, associativity, precedence, l2 pattern *)
+  | Interpretation of loc *
+      string * (string * NotationPt.argument_pattern list) *
+        NotationPt.cic_appl_pattern
+      (* description (i.e. id), symbol, arg pattern, appl pattern *)
 
 type code =
-  | Command of loc * command
-  | NCommand of loc * ncommand
+  | NCommand of loc * command
   | NMacro of loc * nmacro 
   | NTactic of loc * ntactic list
              
@@ -113,3 +163,9 @@ type comment =
 type statement =
   | Executable of loc * code
   | Comment of loc * comment
+
+let description_of_alias =
+ function
+    Ident_alias (_,desc)
+  | Symbol_alias (_,_,desc)
+  | Number_alias (_,desc) -> desc