avoid writing in read only baseuris

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

diff --git a/helm/ocaml/grafite/grafiteAst.ml b/helm/ocaml/grafite/grafiteAst.ml
index 3d176fbe5190d721f0728c85f7b7c3b28ddbbec0..c9567155db9d8ffea4fa95e7463621c265bda743 100644 (file)
--- a/helm/ocaml/grafite/grafiteAst.ml
+++ b/helm/ocaml/grafite/grafiteAst.ml
@@ -23,12 +23,14 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 type direction = [ `LeftToRight | `RightToLeft ]
 
-type loc = CicNotationPt.location
+type loc = Token.flocation
 
 type ('term, 'lazy_term, 'ident) pattern =
-  'lazy_term option * ('ident * 'term) list * 'term
+  'lazy_term option * ('ident * 'term) list * 'term option
 
 type ('term, 'ident) type_spec =
    | Ident of 'ident
@@ -70,6 +72,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | IdTac of loc
   | Injection of loc * 'term
   | Intros of loc * int option * 'ident list
+  | Inversion of loc * 'term
   | LApply of loc * int option * 'term list * 'term * 'ident option
   | Left of loc
   | LetIn of loc * 'term * 'ident
@@ -107,43 +110,18 @@ type 'term macro =
   | 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 *)
-
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 4
+let magic = 5
 
-type ('term,'obj) command =
+type 'obj command =
   | Default of loc * string * UriManager.uri list
   | Include of loc * string
   | Set of loc * string * string
   | Drop of loc
   | Qed of loc
-      (** name.
-       * Name is needed when theorem was started without providing a name
-       *)
-  | Coercion of loc * 'term * bool (* add composites *)
-  | Alias of loc * alias_spec
-      (** parameters, name, type, fields *) 
+  | Coercion of loc * UriManager.uri * bool (* add composites *)
   | Obj of loc * 'obj
-  | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc *
-      int * CicNotationPt.term
-      (* direction, l1 pattern, associativity, precedence, l2 pattern *)
-  | Interpretation of loc *
-      string * (string * CicNotationPt.argument_pattern list) *
-        CicNotationPt.cic_appl_pattern
-      (* description (i.e. id), symbol, arg pattern, appl pattern *)
-
-    (* DEBUGGING *)
-  | Dump of loc (* dump grammar on stdout *)
-    (* DEBUGGING *)
-  | Render of loc * UriManager.uri (* render library object *)
-
-(* composed magic: term + command magics. No need to change this value *)
-let magic = magic + 10000 * CicNotationPt.magic
 
 type ('term, 'lazy_term, 'reduction, 'ident) tactical =
   | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
@@ -175,7 +153,7 @@ let is_punctuation =
   | _ -> false
 
 type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code =
-  | Command of loc * ('term,'obj) command
+  | Command of loc * 'obj command
   | Macro of loc * 'term macro 
   | Tactical of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
       * ('term, 'lazy_term, 'reduction, 'ident) tactical option(* punctuation *)
@@ -187,10 +165,3 @@ type ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment =
 type ('term, 'lazy_term, 'reduction, 'obj, 'ident) statement =
   | Executable of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code
   | Comment of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment
-
-  (* statements meaningful for matitadep *)
-type dependency =
-  | IncludeDep of string
-  | BaseuriDep of string
-  | UriDep of UriManager.uri
-