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
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
]
];
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
| `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
| 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
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)
| 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
[] -> []
| `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
| `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) =
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 *)
]
| 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
| `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),
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)
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
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)
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
| [ 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
+
val boxify: CicNotationPt.term list -> CicNotationPt.term
+val find_appl_pattern_uris:
+ CicNotationPt.cic_appl_pattern -> UriManager.uri list
+
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.
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 ->
projects / helm.git / commitdiff