| `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