From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 5 Oct 2005 16:10:13 +0000 (+0000)
Subject: added metadata "commands"
X-Git-Tag: V_0_7_2_3~244
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=22bc6da37df76df92c51165880ba5e0c5065c6ec;p=helm.git

added metadata "commands"
---

diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml
index 53cbc353f..d3c9d0e95 100644
--- a/helm/ocaml/cic_notation/grafiteAst.ml
+++ b/helm/ocaml/cic_notation/grafiteAst.ml
@@ -124,8 +124,7 @@ type obj =
   | Inductive of (string * Ast.term) list *
       Ast.term inductive_type list
       (** parameters, list of loc * mutual inductive types *)
-  | Theorem of thm_flavour * string * Ast.term *
-      Ast.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
@@ -136,9 +135,17 @@ type obj =
       (string * Ast.term) list
       (** left parameters, name, type, fields *)
 
+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 = 1
+let magic = 2
 
 type ('term,'obj) command =
   | Default of loc * string * UriManager.uri list
@@ -161,6 +168,8 @@ type ('term,'obj) command =
         Ast.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 *)
diff --git a/helm/ocaml/cic_notation/grafiteAstPp.ml b/helm/ocaml/cic_notation/grafiteAstPp.ml
index 6a8e79bc1..9e4d63271 100644
--- a/helm/ocaml/cic_notation/grafiteAstPp.ml
+++ b/helm/ocaml/cic_notation/grafiteAstPp.ml
@@ -270,6 +270,11 @@ let pp_dir_opt = function
   | Some `LeftToRight -> "> "
   | Some `RightToLeft -> "< "
 
+let pp_metadata =
+  function
+  | Dependency buri -> sprintf "dependency %s" buri
+  | Baseuri buri -> sprintf "baseuri %s" buri
+
 let pp_command = function
   | Include (_,path) -> "include " ^ path
   | Qed _ -> "qed"
@@ -293,6 +298,7 @@ let pp_command = function
         (pp_associativity assoc)
         (pp_precedence prec)
         (pp_l2_pattern l2_pattern)
+  | Metadata (_, m) -> sprintf "metadata %s" (pp_metadata m)
   | Render _
   | Dump _ -> assert false  (* ZACK: debugging *)
 
@@ -338,6 +344,7 @@ let pp_cic_command = function
   | Render _
   | Dump _
   | Interpretation _
+  | Metadata _
   | Notation _
   | Obj _ -> assert false (* not implemented *)
 
diff --git a/helm/ocaml/cic_notation/grafiteAstPp.mli b/helm/ocaml/cic_notation/grafiteAstPp.mli
index bd7b23adb..b8445095f 100644
--- a/helm/ocaml/cic_notation/grafiteAstPp.mli
+++ b/helm/ocaml/cic_notation/grafiteAstPp.mli
@@ -30,6 +30,7 @@ val pp_tactic:
 
 val pp_obj: GrafiteAst.obj -> string
 val pp_command: (CicNotationPt.term,GrafiteAst.obj) GrafiteAst.command -> string
+val pp_metadata: GrafiteAst.metadata -> string
 val pp_macro: ('a -> string) -> 'a GrafiteAst.macro -> string
 
 val pp_comment:
diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index c3a4b7f01..3438e2c33 100644
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -472,6 +472,10 @@ EXTEND
     | IDENT "interpretation"; id = QSTRING;
       (symbol, args, l3) = interpretation ->
         GrafiteAst.Interpretation (loc, id, (symbol, args), l3)
+    | IDENT "metadata"; [IDENT "dependency" | IDENT "baseuri" ] ; URI ->
+        (** metadata commands lives only in .moo, where they are in marshalled
+         * form *)
+        raise (CicNotationParser.Parse_error (loc, "metadata not allowed here"))
 
     | IDENT "dump" -> GrafiteAst.Dump loc
     | IDENT "render"; u = URI ->