+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.HOV, true, true), List.map k ts)))
+ Ast.Layout
+ (Ast.Box ((Ast.HOV, true, true),
+ (CicNotationUtil.dress
+ (Ast.Layout Ast.Break)
+ (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.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.Binder (binder_kind, (id, ty), body) ->
Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
Ast.Layout (Ast.Box ((Ast.HV, false, true), [
| 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 ]))])))
+ binder_symbol (resolve_binder binder_kind);
+ k id;
+ builtin_symbol ":";
+ aux_ty ty;
+ Ast.Layout Ast.Break;
+ builtin_symbol ".";
+ k body ])))
-let (compiled21: (CicNotationPt.term -> (CicNotationEnv.t * int) option)
-option ref) =
- ref None
-let (compiled32: (Cic.annterm -> ((string * Cic.annterm) list * int) option)
-option ref) =
- ref None
+let compiled21 = ref None
+let compiled32 = ref None
let set_compiled21 f = compiled21 := Some f
let set_compiled32 f = compiled32 := Some f
let instantiate21 env (* precedence associativity *) l1 =
let rec subst_singleton env t =
let set_compiled21 f = compiled21 := Some f
let set_compiled32 f = compiled32 := Some f
let instantiate21 env (* precedence associativity *) l1 =
let rec subst_singleton env t =
and subst env = function
| Ast.AttributedTerm (_, t) -> subst env t
| Ast.Variable var ->
let name, expected_ty = CicNotationEnv.declaration_of_var var in
and subst env = function
| 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))
let t = (try List.assoc name env with Not_found -> assert false) in
let rec count_lambda = function
| Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body
let t = (try List.assoc name env with Not_found -> assert false) in
let rec count_lambda = function
| Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body
let ast_of_acic id_to_sort annterm =
let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
let ast_of_acic id_to_sort annterm =
let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in