X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite%2FgrafiteAst.ml;h=e1ae5865d43e6ef1dcc0e2de060b46e9636f06e3;hb=9d4a3a25b327bb2c15bd0cff116ba6698b1a4335;hp=f3687789b4ffef162f9c341c14fae13008529b9a;hpb=785d58938cfe252fc078a2ca7d4c7d8bfc83cdc8;p=helm.git

diff --git a/helm/ocaml/grafite/grafiteAst.ml b/helm/ocaml/grafite/grafiteAst.ml
index f3687789b..e1ae5865d 100644
--- a/helm/ocaml/grafite/grafiteAst.ml
+++ b/helm/ocaml/grafite/grafiteAst.ml
@@ -23,24 +23,22 @@
  * http://helm.cs.unibo.it/
  *)
 
-module Ast = CicNotationPt
-
 type direction = [ `LeftToRight | `RightToLeft ]
 
-type loc = Ast.location
+type loc = CicNotationPt.location
 
 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
    | Type of UriManager.uri * int 
 
-type reduction =
+type 'lazy_term reduction =
   [ `Normalize
   | `Reduce
   | `Simpl
-  | `Unfold of CicNotationPt.term option
+  | `Unfold of 'lazy_term option
   | `Whd ]
 
 type ('term, 'lazy_term, 'reduction, 'ident) tactic =
@@ -114,19 +112,11 @@ type alias_spec =
   | Symbol_alias of string * int * string (* name, instance no, description *)
   | Number_alias of int * string          (* instance no, description *)
 
-type metadata =
-  | Dependency of string  (* baseuri without trailing slash *)
-  | Baseuri of string 
-
-let compare_metadata = Pervasives.compare
-
-let eq_metadata = (=)
-
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 3
+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
@@ -135,20 +125,18 @@ type ('term,'obj) command =
       (** name.
        * Name is needed when theorem was started without providing a name
        *)
-  | Coercion of loc * 'term * bool (* add composites *)
+  | Coercion of loc * UriManager.uri * bool (* add composites *)
   | Alias of loc * alias_spec
       (** parameters, name, type, fields *) 
   | Obj of loc * 'obj
-  | Notation of loc * direction option * Ast.term * Gramext.g_assoc *
-      int * Ast.term
+  | 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 * Ast.argument_pattern list) *
-        Ast.cic_appl_pattern
+      string * (string * CicNotationPt.argument_pattern list) *
+        CicNotationPt.cic_appl_pattern
       (* description (i.e. id), symbol, arg pattern, appl pattern *)
 
-  | Metadata of loc * metadata
-
     (* DEBUGGING *)
   | Dump of loc (* dump grammar on stdout *)
     (* DEBUGGING *)
@@ -157,26 +145,6 @@ type ('term,'obj) command =
 (* composed magic: term + command magics. No need to change this value *)
 let magic = magic + 10000 * CicNotationPt.magic
 
-let reash_cmd_uris =
-  let reash_uri uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in
-  function
-  | Default (loc, name, uris) ->
-      let uris = List.map reash_uri uris in
-      Default (loc, name, uris)
-  | Interpretation (loc, dsc, args, cic_appl_pattern) ->
-      let rec aux =
-        function
-        | CicNotationPt.UriPattern uri ->
-            CicNotationPt.UriPattern (reash_uri uri)
-        | CicNotationPt.ApplPattern args ->
-            CicNotationPt.ApplPattern (List.map aux args)
-        | CicNotationPt.VarPattern _
-        | CicNotationPt.ImplicitPattern as pat -> pat
-      in
-      let appl_pattern = aux cic_appl_pattern in
-      Interpretation (loc, dsc, args, appl_pattern)
-  | cmd -> cmd
-
 type ('term, 'lazy_term, 'reduction, 'ident) tactical =
   | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
   | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactical
@@ -207,7 +175,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 *)