+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 pp_ast0 t k =
let reset_href t = Ast.AttributedTerm (`Href [], t) in
let builtin_symbol s = reset_href (Ast.Literal (`Symbol s)) in
Ast.Layout (Ast.Box ((Ast.HV, false, true), [
aux_ty ty;
Ast.Layout (Ast.Box ((Ast.H, false, false), [
Ast.Layout (Ast.Box ((Ast.HV, false, true), [
aux_ty ty;
Ast.Layout (Ast.Box ((Ast.H, false, false), [
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), [
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.AttributedTerm (_, t) -> subst env t
| Ast.Variable var ->
let name, expected_ty = CicNotationEnv.declaration_of_var var in
| Ast.AttributedTerm (_, t) -> subst env t
| Ast.Variable var ->
let name, expected_ty = CicNotationEnv.declaration_of_var var in
assert (CicNotationEnv.well_typed expected_ty value);
[ CicNotationEnv.term_of_value value ]
| Ast.Magic m -> subst_magic env m
assert (CicNotationEnv.well_typed expected_ty value);
[ CicNotationEnv.term_of_value value ]
| Ast.Magic m -> subst_magic env m
| Ast.Literal _ as t -> [ t ]
| Ast.Layout l -> [ Ast.Layout (subst_layout env l) ]
| t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ]
| Ast.Literal _ as t -> [ t ]
| Ast.Layout l -> [ Ast.Layout (subst_layout env l) ]
| t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ]
- | Ast.Box (kind, tl) -> Ast.Box (kind, List.concat (List.map (subst env) tl))
+ | Ast.Box (kind, tl) ->
+ Ast.Box (kind, List.concat (List.map (subst env) tl))
- prerr_endline ("IN " ^ CicNotationPp.pp_term term);
- (* LUCA: il termine legato e' lo stesso termine di partenza per cui si innesca il loop infinito *)
- let res = Ast.AttributedTerm (`Level (precedence, associativity),
- (instantiate21 (ast_env_of_env env) l1))
- in
- prerr_endline "OUT";
- res
+ Ast.AttributedTerm (`Level (precedence, associativity),
+ (instantiate21 (ast_env_of_env env) l1))