From: Stefano Zacchiroli Date: Fri, 8 Jul 2005 16:03:44 +0000 (+0000) Subject: snapshot X-Git-Tag: pre_notation~66 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5d5e328a05ed70fcf565aef8f92b7ec87b2740f2;p=helm.git snapshot - added hyperlink handling on all notation literals --- diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 1c1532548..204e945fc 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -201,7 +201,7 @@ struct Pt.Variable (Pt.TermVar name) in let rec aux = function - | Pt.AttributedTerm (_, t) -> aux t + | Pt.AttributedTerm (_, t) -> assert false | Pt.Literal _ | Pt.Layout _ -> assert false | Pt.Variable v -> Pt.Variable v @@ -330,7 +330,7 @@ struct Hashtbl.hash mask, tl let mask_of_appl_pattern = function - | Pt.UriPattern s -> Uri (UriManager.uri_of_string s), [] + | Pt.UriPattern uri -> Uri uri, [] | Pt.VarPattern _ -> Blob, [] | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index ba12b49da..4dcc77297 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -543,7 +543,7 @@ EXTEND ] ]; level3_term: [ - [ u = URI -> UriPattern u + [ u = URI -> UriPattern (UriManager.uri_of_string u) | id = IDENT -> VarPattern id | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" -> (match terms with diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index a3e4f4621..cb67202a5 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -44,6 +44,8 @@ let pp_literal l = | `Number s -> s) let rec pp_term = function + | AttributedTerm (`Href _, term) when print_attributes -> + sprintf "#[%s]" (pp_term term) | AttributedTerm (_, term) when print_attributes -> sprintf "@[%s]" (pp_term term) | AttributedTerm (_, term) -> pp_term term diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index 97659b763..790bb3785 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -168,9 +168,17 @@ 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 = - let uri = lookup_uri xref in - make_attributes [Some "helm","xref"; Some "xlink","href"] [xref;uri] + let make_href xref uris = + let xref_uri = lookup_uri xref in + let raw_uris = List.map UriManager.string_of_uri uris in + let uri = + match xref_uri, raw_uris with + | None, [] -> None + | Some uri, [] -> Some uri + | 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] in let make_xref xref = make_attributes [Some "helm","xref"] [xref] in let make_box = function @@ -179,38 +187,40 @@ let render ids_to_uris = box | m -> Box.Object ([], m) in - let make_hv xref children = - let attrs = indent_attributes @ make_href xref in - P.Mobject ([], Box.HV (indent_attributes, List.map make_box children)) - in (* when mathonly is true no boxes should be generated, only mrows *) - let rec aux mathonly xref pos prec t = + let rec aux mathonly xref pos prec uris t = match t with - | A.AttributedTerm (`Loc _, t) -> aux mathonly xref pos prec t - | A.AttributedTerm (`Level (child_prec, child_assoc), t) -> - let t' = aux mathonly xref pos child_prec t in - add_parens child_prec child_assoc pos prec t' - | A.AttributedTerm (`IdRef xref, t) -> aux mathonly (Some xref) pos prec t - | 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,to_unicode literal) - | A.Uri (literal, _) -> P.Mi (make_href xref, to_unicode literal) - | A.Literal l -> aux_literal xref prec l - | A.Layout l -> aux_layout mathonly xref pos prec l + | 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 + | 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_literal xref prec l = - let attrs = make_href xref in + and aux_attribute mathonly xref pos prec uris t = + function + | `Loc _ -> aux mathonly xref pos prec uris t + | `Level (child_prec, child_assoc) -> + let t' = aux 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 + | _ -> assert false + and aux_literal xref prec uris l = + let attrs = make_href xref uris in match l with | `Symbol s | `Keyword s -> P.Mo (attrs, to_unicode s) | `Number s -> P.Mn (attrs, to_unicode s) - and aux_layout mathonly xref pos prec l = + and aux_layout mathonly xref pos prec uris l = let attrs = make_xref xref in - let invoke' t = aux true None pos prec 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) @@ -223,9 +233,9 @@ let render ids_to_uris = | A.Sqrt t -> P.Msqrt (attrs, invoke' t) | A.Root (t1, t2) -> P.Mroot (attrs, invoke' t1, invoke' t2) | A.Box (kind, terms) -> - let children = aux_children mathonly xref pos prec terms in + let children = aux_children mathonly xref pos prec uris terms in box_of mathonly kind attrs children - and aux_children mathonly xref pos prec terms = + and aux_children mathonly xref pos prec uris terms = let rec aux_list first = function [] -> [] @@ -238,7 +248,7 @@ let render ids_to_uris = | `Right -> `Right | `Left -> `Inner in - [aux mathonly xref pos' prec t] + [aux mathonly xref pos' prec uris t] | t :: tl -> let pos' = match pos, first with @@ -249,13 +259,13 @@ let render ids_to_uris = | `Right, _ -> `Inner | `Inner, _ -> `Inner in - (aux mathonly xref pos' prec 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 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 c702f5115..ab484c3eb 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -39,6 +39,7 @@ let loc_of_floc = function type term_attribute = [ `Loc of location (* source file location *) | `IdRef of string (* ACic pointer *) + | `Href of UriManager.uri list (* hyperlinks for literals *) | `Level of int * Gramext.g_assoc (* precedence, associativity *) ] @@ -133,7 +134,7 @@ type argument_pattern = | IdentArg of int * string (* eta-depth, name *) type cic_appl_pattern = - | UriPattern of string + | UriPattern of UriManager.uri | VarPattern of string | ApplPattern of cic_appl_pattern list diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 3af28fddd..dac2b4c73 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -82,6 +82,8 @@ let resolve_binder = function | `Exists -> "\\exists" 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 rec aux = function | Ast.Appl ts -> Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc), @@ -92,21 +94,22 @@ let pp_ast0 t k = Ast.Layout (Ast.Box ((Ast.HV, false, true), [ aux_ty ty; Ast.Layout (Ast.Box ((Ast.H, false, false), [ - Ast.Literal (`Symbol "\\to"); k body]))]))) + builtin_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), [ - Ast.Literal (`Symbol (resolve_binder binder_kind)); + builtin_symbol (resolve_binder binder_kind); k id; - Ast.Literal (`Symbol ":"); + builtin_symbol ":"; aux_ty ty ])); Ast.Layout (Ast.Box ((Ast.H, false, false), [ - Ast.Literal (`Symbol "."); + builtin_symbol "."; k body ]))]))) | t -> CicNotationUtil.visit_ast ~special_k k t and aux_ty = function - | None -> Ast.Literal (`Symbol "?") + | None -> builtin_symbol "?" | Some ty -> k ty and special_k = function | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t) @@ -340,16 +343,19 @@ let rec pp_ast1 term = let ast_env_of_env env = List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env in - match (get_compiled21 ()) term with - | None -> pp_ast0 term pp_ast1 - | Some (env, pid) -> - let precedence, associativity, l1 = - try - Hashtbl.find level1_patterns21 pid - with Not_found -> assert false - in - Ast.AttributedTerm (`Level (precedence, associativity), - (instantiate21 (ast_env_of_env env) (* precedence associativity *) l1)) + match term with + | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, pp_ast1 t) + | _ -> + (match (get_compiled21 ()) term with + | None -> pp_ast0 term pp_ast1 + | Some (env, pid) -> + let precedence, associativity, l1 = + try + Hashtbl.find level1_patterns21 pid + with Not_found -> assert false + in + Ast.AttributedTerm (`Level (precedence, associativity), + (instantiate21 (ast_env_of_env env) l1))) let instantiate32 term_info env symbol args = let rec instantiate_arg = function @@ -379,12 +385,15 @@ let rec ast_of_acic1 term_info annterm = let env' = List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env in - let symbol, args = + let symbol, args, uris = try Hashtbl.find level2_patterns32 pid with Not_found -> assert false in - instantiate32 term_info env' symbol args + let ast = instantiate32 term_info env' symbol args in + match uris with + | [] -> ast + | _ -> Ast.AttributedTerm (`Href uris, ast) let load_patterns32 t = set_compiled32 (CicNotationMatcher.Matcher32.compiler t) @@ -407,7 +416,8 @@ let fresh_id = let add_interpretation (symbol, args) appl_pattern = let id = fresh_id () in - Hashtbl.add level2_patterns32 id (symbol, args); + let uris = CicNotationUtil.find_appl_pattern_uris appl_pattern in + Hashtbl.add level2_patterns32 id (symbol, args, uris); pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix; load_patterns32 !pattern32_matrix; id diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index 964c303ee..630fb4361 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -311,3 +311,16 @@ let boxify = function | [ a ] -> a | l -> Layout (Box ((H, false, false), l)) +let find_appl_pattern_uris ap = + let rec aux acc = + function + | UriPattern uri -> + (try + ignore (List.find (fun uri' -> UriManager.eq uri uri') acc); + acc + with Not_found -> uri :: acc) + | VarPattern _ -> acc + | ApplPattern apl -> List.fold_left aux acc apl + in + aux [] ap + diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli index f35fbb3d3..1a7d7d6f4 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.mli +++ b/helm/ocaml/cic_notation/cicNotationUtil.mli @@ -48,3 +48,6 @@ val string_of_literal: CicNotationPt.literal -> string val boxify: CicNotationPt.term list -> CicNotationPt.term +val find_appl_pattern_uris: + CicNotationPt.cic_appl_pattern -> UriManager.uri list + diff --git a/helm/ocaml/cic_notation/doc/samples.ma b/helm/ocaml/cic_notation/doc/samples.ma index abd8b7866..d724ac4eb 100644 --- a/helm/ocaml/cic_notation/doc/samples.ma +++ b/helm/ocaml/cic_notation/doc/samples.ma @@ -25,6 +25,7 @@ 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 \[ \TERM a \OVER \TERM b : \TERM c \SQRT \TERM d \] for 'megacoso \TERM a \TERM b \TERM c \TERM d. interpretation 'megacoso x y z w = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) (cic:/Coq/Init/Peano/plus.con x y) (cic:/Coq/Init/Peano/plus.con z w)). render cic:/Coq/Arith/Plus/plus_comm.con. diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 1585f43e2..ce87368bf 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -107,17 +107,16 @@ let _ = CicNotationRew.ast_of_acic id_to_sort annterm in let time2 = Unix.gettimeofday () in - printf "ast creation took %f seconds\n" (time2 -. time1); - prerr_endline "===="; - print_endline (CicNotationPp.pp_term t); flush stdout; + prerr_endline (sprintf "ast creation took %f seconds\n" (time2 -. time1)); + prerr_endline "AST"; + prerr_endline (CicNotationPp.pp_term t); flush stdout; let time3 = Unix.gettimeofday () in let t' = CicNotationRew.pp_ast t in let time4 = Unix.gettimeofday () in - printf "pretty printing took %f seconds\n" (time4 -. time3); - dump_xml t' id_to_uri "out.xml"; - print_endline (CicNotationPp.pp_term t'); flush stdout - ) + prerr_endline (sprintf "pretty printing took %f seconds\n" (time4 -. time3)); + prerr_endline (CicNotationPp.pp_term t'); + dump_xml t' id_to_uri "out.xml") (* CicNotationParser.print_l2_pattern ()) *) | 1 -> ignore (CicNotationParser.parse_syntax_pattern istream) | 2 ->