make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in
B.H([],
(B.b_kw "by")::B.b_space::
- B.Text([],"(")::pres_args@[B.Text([],")")]), None
- else
- (B.b_kw "by"),
+ B.Text([],"(")::pres_args@[B.Text([],")")]), None
+ else (B.b_kw "by"),
Some (B.b_toggle [B.b_kw "proof";proof2pres term2pres p])
and proof2pres term2pres p =
and ce2pres =
function
`Declaration d ->
- (match d.Con.dec_name with
- Some s ->
- let ty = term2pres d.Con.dec_type in
- B.H ([],
- [(B.b_kw "Assume");
- B.b_space;
- B.Object ([], P.Mi([],s));
- B.Text([],":");
- ty])
- | None ->
- prerr_endline "NO NAME!!"; assert false)
+ let ty = term2pres d.Con.dec_type in
+ B.H ([],
+ [(B.b_kw "Assume");
+ B.b_space;
+ B.Object ([], P.Mi([],get_name d.Con.dec_name));
+ B.Text([],":");
+ ty])
| `Hypothesis h ->
- (match h.Con.dec_name with
- Some s ->
- let ty = term2pres h.Con.dec_type in
- B.H ([],
- [(B.b_kw "Suppose");
- B.b_space;
- B.Text([],"(");
- B.Object ([], P.Mi ([],s));
- B.Text([],")");
- B.b_space;
- ty])
- | None ->
- prerr_endline "NO NAME!!"; assert false)
+ let ty = term2pres h.Con.dec_type in
+ B.H ([],
+ [(B.b_kw "Suppose");
+ B.b_space;
+ B.Text([],"(");
+ B.Object ([], P.Mi ([],get_name h.Con.dec_name));
+ B.Text([],")");
+ B.b_space;
+ ty])
| `Proof p ->
proof2pres p
| `Definition d ->
- (match d.Con.def_name with
- Some s ->
- let term = term2pres d.Con.def_term in
- B.H ([],
- [ B.b_kw "Let"; B.b_space;
- B.Object ([], P.Mi([],s));
- B.Text([]," = ");
- term])
- | None ->
- prerr_endline "NO NAME!!"; assert false)
+ let term = term2pres d.Con.def_term in
+ B.H ([],
+ [ B.b_kw "Let"; B.b_space;
+ B.Object ([], P.Mi([],get_name d.Con.def_name));
+ B.Text([]," = ");
+ term])
and acontext2pres ac continuation indent =
List.fold_right
else if (conclude.Con.conclude_method = "FalseInd") then
falseind conclude
else if (conclude.Con.conclude_method = "Rewrite") then
- let justif1, justif2 =
+ let justif1,justif2 =
(match (List.nth conclude.Con.conclude_args 6) with
Con.ArgProof p -> justification term2pres p
| _ -> assert false) in
(B.b_kw "rewrite");
B.b_space; term1;
B.b_space; (B.b_kw "with");
- B.b_space; term2;
- B.b_space; justif1]) ::
- match justif2 with None -> [] | Some j -> [B.indent j])
+ B.b_space; term2;
+ B.b_space; justif1])::
+ match justif2 with None -> [] | Some j -> [B.indent j])
+ else if conclude.Con.conclude_method = "Eq_chain" then
+ let justification p =
+ let j1,j2 = justification term2pres p in
+ j1 :: B.b_space :: (match j2 with Some j -> [j] | None -> [])
+ in
+ let rec aux args =
+ match args with
+ | [] -> []
+ | (Con.ArgProof p)::(Con.Term t)::tl ->
+ B.HOV(RenderingAttrs.indent_attributes `BoxML,([B.b_kw "=";B.b_space;term2pres t;B.b_space]@justification p))::(aux tl)
+ | _ -> assert false
+ in
+ let hd =
+ match List.hd conclude.Con.conclude_args with
+ | Con.Term t -> t
+ | _ -> assert false
+ in
+ B.HOV([],[term2pres hd; (* B.b_space; *)
+ B.V ([],aux (List.tl conclude.Con.conclude_args))])
else if conclude.Con.conclude_method = "Apply" then
let pres_args =
make_args_for_apply term2pres conclude.Con.conclude_args in
(match e with
`Declaration h
| `Hypothesis h ->
- let name =
- (match h.Con.dec_name with
- None -> "NO NAME???"
- | Some n ->n) in
+ let name = get_name h.Con.dec_name in
[B.b_space;
B.Object ([], P.Mi ([],name));
B.Text([],":");
| _ -> assert false) in
match proof.Con.proof_context with
`Hypothesis hyp1::`Hypothesis hyp2::tl ->
- let get_name hyp =
- (match hyp.Con.dec_name with
- None -> "_"
- | Some s -> s) in
let preshyp1 =
B.H ([],
[B.Text([],"(");
- B.Object ([], P.Mi([],get_name hyp1));
+ B.Object ([], P.Mi([],get_name hyp1.Con.dec_name));
B.Text([],")");
B.skip;
term2pres hyp1.Con.dec_type]) in
let preshyp2 =
B.H ([],
[B.Text([],"(");
- B.Object ([], P.Mi([],get_name hyp2));
+ B.Object ([], P.Mi([],get_name hyp2.Con.dec_name));
B.Text([],")");
B.skip;
term2pres hyp2.Con.dec_type]) in
match proof.Con.proof_context with
`Declaration decl::`Hypothesis hyp::tl
| `Hypothesis decl::`Hypothesis hyp::tl ->
- let get_name decl =
- (match decl.Con.dec_name with
- None -> "_"
- | Some s -> s) in
let presdecl =
B.H ([],
[(B.b_kw "let");
B.skip;
- B.Object ([], P.Mi([],get_name decl));
+ B.Object ([], P.Mi([],get_name decl.Con.dec_name));
B.Text([],":"); term2pres decl.Con.dec_type]) in
let suchthat =
B.H ([],
[(B.b_kw "such that");
B.skip;
B.Text([],"(");
- B.Object ([], P.Mi([],get_name hyp));
+ B.Object ([], P.Mi([],get_name hyp.Con.dec_name));
B.Text([],")");
B.skip;
term2pres hyp.Con.dec_type]) in