From 915c3e1993cad4dcadefe7e6886e6cb8feefae8b Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 13 Jul 2005 17:03:04 +0000 Subject: [PATCH] added XmlAttrs attribute for specification of xml attributes directly from cicNotationRew.ml --- helm/ocaml/cic_notation/cicNotationLexer.ml | 4 +- .../cicNotationParser.expanded.ml | 4 +- helm/ocaml/cic_notation/cicNotationPres.ml | 51 +++++++++++-------- helm/ocaml/cic_notation/cicNotationPt.ml | 2 + helm/ocaml/cic_notation/cicNotationRew.ml | 16 ++++-- helm/ocaml/cic_notation/doc/samples.ma | 8 ++- 6 files changed, 54 insertions(+), 31 deletions(-) diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml index 01ef6142c..92204cfb7 100644 --- a/helm/ocaml/cic_notation/cicNotationLexer.ml +++ b/helm/ocaml/cic_notation/cicNotationLexer.ml @@ -87,9 +87,7 @@ let _ = [ "Prop"; "Type"; "Set"; "let"; "rec"; "corec"; "match"; "with"; "in"; "and"; "on" ] -let add_level2_ast_keyword k = - prerr_endline ("Adding keyword " ^ k); - Hashtbl.add level2_ast_keywords k () +let add_level2_ast_keyword k = Hashtbl.add level2_ast_keywords k () let remove_level2_ast_keyword k = Hashtbl.remove level2_ast_keywords k let regexp uri = diff --git a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml index 5d103bdaa..5c73d2b4c 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml @@ -96,7 +96,9 @@ let extract_term_production pattern = | Layout l -> aux_layout l | Magic m -> aux_magic m | Variable v -> aux_variable v - | t -> prerr_endline (CicNotationPp.pp_term t); assert false + | t -> + prerr_endline (CicNotationPp.pp_term t); + assert false and aux_literal = function `Symbol s -> [NoBinding, symbol s] diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index c3ea73f1c..a14ff349d 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -169,7 +169,7 @@ let render ids_to_uris = | None -> None | Some id -> (try Some (Hashtbl.find ids_to_uris id) with Not_found -> None) in - let make_href xref uris = + let make_href xmlattrs xref uris = let xref_uri = lookup_uri xref in let raw_uris = List.map UriManager.string_of_uri uris in let uri = @@ -179,7 +179,8 @@ let render ids_to_uris = | None, raw_uris -> Some (String.concat " " raw_uris) | Some uri, raw_uris -> Some (String.concat " " (uri :: raw_uris)) in - make_attributes [Some "helm", "xref"; Some "xlink", "href"] [xref; uri] + xmlattrs + @ make_attributes [Some "helm", "xref"; Some "xlink", "href"] [xref; uri] in let make_xref xref = make_attributes [Some "helm","xref"] [xref] in let make_box = function @@ -189,38 +190,43 @@ let render ids_to_uris = | m -> Box.Object ([], m) in (* when mathonly is true no boxes should be generated, only mrows *) - let rec aux mathonly xref pos prec uris t = + let rec aux xmlattrs mathonly xref pos prec uris t = match t with | A.AttributedTerm (attr, t) -> - aux_attribute mathonly xref pos prec uris t attr - | A.Ident (literal, _) -> P.Mi (make_href xref [], to_unicode literal) - | A.Num (literal, _) -> P.Mn (make_href xref [], to_unicode literal) - | A.Symbol (literal, _) -> P.Mo (make_href xref uris, to_unicode literal) - | A.Uri (literal, _) -> P.Mi (make_href xref [], to_unicode literal) - | A.Literal l -> aux_literal xref prec uris l + aux_attribute xmlattrs mathonly xref pos prec uris t attr + | A.Ident (literal, _) -> + P.Mi (make_href xmlattrs xref [], to_unicode literal) + | A.Num (literal, _) -> + P.Mn (make_href xmlattrs xref [], to_unicode literal) + | A.Symbol (literal, _) -> + P.Mo (make_href xmlattrs xref uris, to_unicode literal) + | A.Uri (literal, _) -> + P.Mi (make_href xmlattrs xref [], to_unicode literal) + | A.Literal l -> aux_literal xmlattrs xref prec uris l | A.Layout l -> aux_layout mathonly xref pos prec uris l | A.Magic _ | A.Variable _ -> assert false (* should have been instantiated *) | t -> prerr_endline (CicNotationPp.pp_term t); assert false - and aux_attribute mathonly xref pos prec uris t = + and aux_attribute xmlattrs mathonly xref pos prec uris t = function - | `Loc _ -> aux mathonly xref pos prec uris t + | `Loc _ -> aux xmlattrs mathonly xref pos prec uris t | `Level (child_prec, child_assoc) -> - let t' = aux mathonly xref pos child_prec uris t in + let t' = aux xmlattrs mathonly xref pos child_prec uris t in add_parens child_prec child_assoc pos prec t' - | `IdRef xref -> aux mathonly (Some xref) pos prec uris t - | `Href uris' -> aux mathonly xref pos prec uris' t - and aux_literal xref prec uris l = - let attrs = make_href xref uris in + | `IdRef xref -> aux xmlattrs mathonly (Some xref) pos prec uris t + | `Href uris' -> aux xmlattrs mathonly xref pos prec uris' t + | `XmlAttrs xmlattrs -> aux xmlattrs mathonly xref pos prec uris t + and aux_literal xmlattrs xref prec uris l = + let attrs = make_href xmlattrs xref uris in match l with | `Symbol s -> P.Mo (attrs, to_unicode s) - | `Keyword s -> P.Mo (keyword_attributes @ attrs, to_unicode s) + | `Keyword s -> P.Mo (attrs, to_unicode s) | `Number s -> P.Mn (attrs, to_unicode s) and aux_layout mathonly xref pos prec uris l = let attrs = make_xref xref in - let invoke' t = aux true None pos prec uris t in + let invoke' t = aux [] true None pos prec uris t in match l with | A.Sub (t1, t2) -> P.Msub (attrs, invoke' t1, invoke' t2) | A.Sup (t1, t2) -> P.Msup (attrs, invoke' t1, invoke' t2) @@ -235,6 +241,7 @@ let render ids_to_uris = | A.Box (kind, terms) -> let children = aux_children mathonly xref pos prec uris terms in box_of mathonly kind attrs children + | A.Break -> assert false (* TODO? *) and aux_children mathonly xref pos prec uris terms = let rec aux_list first = function @@ -248,7 +255,7 @@ let render ids_to_uris = | `Right -> `Right | `Left -> `Inner in - [aux mathonly xref pos' prec uris t] + [aux [] mathonly xref pos' prec uris t] | t :: tl -> let pos' = match pos, first with @@ -259,13 +266,13 @@ let render ids_to_uris = | `Right, _ -> `Inner | `Inner, _ -> `Inner in - (aux mathonly xref pos' prec uris t) :: aux_list false tl + (aux [] mathonly xref pos' prec uris t) :: aux_list false tl in match terms with - [t] -> [aux mathonly xref pos prec uris t] + | [t] -> [aux [] mathonly xref pos prec uris t] | tl -> aux_list true tl in - aux false None `None 0 [] + aux [] false None `None 0 [] let render_to_boxml id_to_uri t = let rec print_box (t: CicNotationPres.boxml_markup) = diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index 99b8909e5..5ad1f0b5b 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -41,6 +41,8 @@ type term_attribute = | `IdRef of string (* ACic pointer *) | `Href of UriManager.uri list (* hyperlinks for literals *) | `Level of int * Gramext.g_assoc (* precedence, associativity *) + | `XmlAttrs of (string option * string * string) list + (* list of XML attributes: namespace, name, value *) ] type literal = diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 207b26a23..e72bfacc8 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -37,8 +37,6 @@ type term_info = uri: (Cic.id, string) Hashtbl.t; } -let warning s = prerr_endline ("CicNotation WARNING: " ^ s) - let get_types uri = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with @@ -81,9 +79,17 @@ let resolve_binder = function | `Forall -> "\\forall" | `Exists -> "\\exists" +let binder_attributes = [None, "mathcolor", "blue"] +let atop_attributes = [None, "linethickness", "0pt"] +let indent_attributes = [None, "indent", "1em"] +let keyword_attributes = [None, "mathcolor", "blue"] + let pp_ast0 t k = let reset_href t = Ast.AttributedTerm (`Href [], t) in let builtin_symbol s = reset_href (Ast.Literal (`Symbol s)) in + let binder_symbol s = + Ast.AttributedTerm (`XmlAttrs binder_attributes, builtin_symbol s) + in let rec aux = function | Ast.Appl ts -> Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc), @@ -94,13 +100,13 @@ let pp_ast0 t k = Ast.Layout (Ast.Box ((Ast.HV, false, true), [ aux_ty ty; Ast.Layout (Ast.Box ((Ast.H, false, false), [ - builtin_symbol "\\to"; + binder_symbol "\\to"; k body]))]))) | Ast.Binder (binder_kind, (id, ty), body) -> Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc), Ast.Layout (Ast.Box ((Ast.HV, false, true), [ Ast.Layout (Ast.Box ((Ast.H, false, false), [ - builtin_symbol (resolve_binder binder_kind); + binder_symbol (resolve_binder binder_kind); k id; builtin_symbol ":"; aux_ty ty ])); @@ -275,6 +281,8 @@ let instantiate21 env (* precedence associativity *) l1 = assert (CicNotationEnv.well_typed expected_ty value); [ CicNotationEnv.term_of_value value ] | Ast.Magic m -> subst_magic env m + | Ast.Literal (`Keyword k) as t -> + [ Ast.AttributedTerm (`XmlAttrs keyword_attributes, t) ] | Ast.Literal _ as t -> [ t ] | Ast.Layout l -> [ Ast.Layout (subst_layout env l) ] | t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ] diff --git a/helm/ocaml/cic_notation/doc/samples.ma b/helm/ocaml/cic_notation/doc/samples.ma index 46193bf73..f8620ecec 100644 --- a/helm/ocaml/cic_notation/doc/samples.ma +++ b/helm/ocaml/cic_notation/doc/samples.ma @@ -47,11 +47,17 @@ notation "a + b" left associative for @{ 'plus $a $b }. print 1 + 2 + 3. print 1 + (2 + 3). +notation "a + b" left associative for @{ 'plus $a $b }. +notation "a * b" left associative for @{ 'mult $a $b }. +interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y). +interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y). +render cic:/Coq/Arith/Mult/mult_plus_distr_r.con. + notation "'if' a 'then' b 'else' c" for @{ 'ifthenelse $a $b $c }. -print if even then x else bump x. +print if even then \forall x:nat.x else bump x. notation "a \vee b" -- 2.39.2