+ 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.HOV, true, true), List.map k ts)))
+ | Ast.Binder (`Forall, (Ast.Ident ("_", _), ty), body)
+ | Ast.Binder (`Pi, (Ast.Ident ("_", _), ty), body) ->
+ Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
+ Ast.Layout (Ast.Box ((Ast.HV, false, true), [
+ aux_ty ty;
+ Ast.Layout (Ast.Box ((Ast.H, false, false), [
+ 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), [
+ builtin_symbol (resolve_binder binder_kind);
+ k id;
+ builtin_symbol ":";
+ aux_ty ty ]));
+ Ast.Layout (Ast.Box ((Ast.H, false, false), [
+ builtin_symbol ".";
+ k body ]))])))
+ | t -> CicNotationUtil.visit_ast ~special_k k t
+ and aux_ty = function
+ | None -> builtin_symbol "?"
+ | Some ty -> k ty