added metadata "commands"

diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml
index 53cbc353fa49aa676003df9ced084cd221a7fd53..d3c9d0e9581121be2ca909f97ae0a3261f2dcdcd 100644 (file)
--- 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 6a8e79bc10722535c8dff3df30ab016144ace9fe..9e4d632712a087da49db3e38813bbeac03d64af5 100644 (file)
--- 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 bd7b23adb8b272268cd6a3cd254079e61cd30ec3..b8445095ff32ada3dcb419dab62d0920ce8f4f8b 100644 (file)
--- 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 c3a4b7f01ef998e30c5debd31d5ee34a032725bb..3438e2c3314e25960bf8a4b90225e66a05b953a4 100644 (file)
--- 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 ->