From: Stefano Zacchiroli 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 ->