with Not_found -> assert false)
module Ast = CicNotationPt
+module Parser = CicNotationParser
let string_of_name = function
| Cic.Name s -> s
let idref id t = Ast.AttributedTerm (`IdRef id, t)
+let resolve_binder = function
+ | `Lambda -> "\\lambda"
+ | `Pi -> "\\Pi"
+ | `Forall -> "\\forall"
+ | `Exists -> "\\exists"
+
let pp_ast0 t k =
- prerr_endline "pp_ast0";
- let rec aux t = CicNotationUtil.visit_ast ~special_k k t
+ 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), [
+ Ast.Literal (`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));
+ k id;
+ Ast.Literal (`Symbol ":");
+ aux_ty ty ]));
+ Ast.Layout (Ast.Box ((Ast.H, false, false), [
+ Ast.Literal (`Symbol ".");
+ k body ]))])))
+ | t -> CicNotationUtil.visit_ast ~special_k k t
+ and aux_ty = function
+ | None -> Ast.Literal (`Symbol "?")
+ | Some ty -> k ty
and special_k = function
- | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, aux t)
+ | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t)
| _ -> assert false
in
aux t
let set_compiled32 f = compiled32 := Some f
let instantiate21 env precedence associativity l1 =
- prerr_endline "instantiate21";
- let rec subst last_box env = function
- | Ast.AttributedTerm (_, t) -> subst last_box env t
+ let rec subst_singleton env t =
+ CicNotationUtil.boxify (subst 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
let ty, value =
(* following assertion should be a conditional that makes this
* instantiation fail *)
assert (CicNotationEnv.well_typed expected_ty value);
- CicNotationEnv.term_of_value value
- | Ast.Magic m -> subst_magic last_box env m
- | Ast.Literal _ as t -> t
- | Ast.Layout l -> Ast.Layout (subst_layout last_box env l)
- | t -> CicNotationUtil.visit_ast (subst last_box env) t
- and subst_magic last_box env = function
+ [ 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 ]
+ and subst_magic env = function
| Ast.List0 (p, sep_opt)
| Ast.List1 (p, sep_opt) ->
let rec_decls = CicNotationEnv.declarations_of_term p in
in
let rec instantiate_list acc = function
| [] -> List.rev acc
+ | value_set :: [] ->
+ let env = CicNotationEnv.combine rec_decls value_set in
+ instantiate_list
+ ((CicNotationUtil.boxify (subst env p)) :: acc) []
| value_set :: tl ->
let env = CicNotationEnv.combine rec_decls value_set in
- instantiate_list ([subst last_box env p] @ sep @ acc) tl
+ instantiate_list
+ ((CicNotationUtil.boxify (subst env p @ sep)) :: acc) tl
in
- let children = instantiate_list [] values in
- CicNotationPt.Layout (CicNotationPt.Box (last_box, children))
+ instantiate_list [] values
| Ast.Opt p ->
let opt_decls = CicNotationEnv.declarations_of_term p in
let env =
in
try build_env opt_decls with Exit -> []
in
- let children =
- if env = [] then []
- else [subst last_box env p]
- in
- CicNotationPt.Layout (CicNotationPt.Box (last_box, children))
+ begin
+ match env with
+ | [] -> []
+ | _ -> subst env p
+ end
| _ -> assert false (* impossible *)
- and subst_layout last_box env l =
- CicNotationUtil.visit_layout (subst last_box env) l
- (* TODO ZACK here we need to remember the last box traversed, but
- * visit_layout is opaque :-((( *)
+ and subst_layout env = function
+ | Ast.Box (kind, tl) -> Ast.Box (kind, List.concat (List.map (subst env) tl))
+ | l -> CicNotationUtil.visit_layout (subst_singleton env) l
in
- subst CicNotationPt.H env l1
+ subst_singleton env l1
let rec pp_ast1 term =
let rec pp_value = function