let p_mo a b = Mpresentation.Mo(a,b)
let p_mrow a b = Mpresentation.Mrow(a,b)
let p_mphantom a b = Mpresentation.Mphantom(a,b)
+let b_ink a = Box.Ink a
let rec split n l =
if n = 0 then [],l
)],
Some (B.b_toggle [B.b_kw "proof";B.indent (proof2pres true term2pres p)])
-and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
- let rec proof2pres ?skip_initial_lambdas_internal is_top_down p in_bu_conversion =
+and proof2pres0 term2pres ?skip_initial_lambdas_internal is_top_down p in_bu_conversion =
let indent =
let is_decl e =
(match e with
| Some t -> Some (term2pres t)) in
let body =
let presconclude =
- conclude2pres
+ conclude2pres term2pres
?skip_initial_lambdas_internal:
(match skip_initial_lambdas_internal with
Some (`Later s) -> Some (`Now s)
is_top_down p.Con.proof_name p.Con.proof_conclude indent
omit_conclusion in_bu_conversion in
let presacontext =
- acontext2pres
+ acontext2pres term2pres
(if p.Con.proof_conclude.Con.conclude_method = "BU_Conversion" then
is_top_down
else
presconclude indent
(p.Con.proof_conclude.Con.conclude_method = "BU_Conversion")
in
- context2pres
+ context2pres term2pres
(match skip_initial_lambdas_internal with
Some (`Now n) -> snd (HExtlib.split_nth n p.Con.proof_context)
| _ -> p.Con.proof_context)
- presacontext
+ ~continuation:presacontext
in
(*
let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (if is_top_down then "(TD)" else "(NTD)") ^ "*)"); body; B.b_kw "(*>>*)"]) in
in
B.indent action
- and context2pres c continuation =
+and context2pres term2pres c ~continuation =
(* we generate a subtable for each context element, for selection
purposes
The table generated by the head-element does not have an xref;
let xref = get_xref ce in
B.V([Some "helm", "xref", xref ],
[B.H([Some "helm", "xref", "ce_"^xref],
- [ce2pres_in_proof_context_element ce]);
+ [ce2pres_in_proof_context_element term2pres ce]);
continuation])) tl continuation in
let hd_xref= get_xref hd in
B.V([],
[B.H([Some "helm", "xref", "ce_"^hd_xref],
- [ce2pres_in_proof_context_element hd]);
+ [ce2pres_in_proof_context_element term2pres hd]);
continuation'])
- and ce2pres_in_joint_context_element = function
+and ce2pres_in_joint_context_element term2pres = function
| `Inductive _ -> assert false (* TODO *)
- | (`Declaration _) as x -> ce2pres x
- | (`Hypothesis _) as x -> ce2pres x
- | (`Proof _) as x -> ce2pres x
- | (`Definition _) as x -> ce2pres x
+ | (`Declaration _)
+ | (`Hypothesis _)
+ | (`Proof _)
+ | (`Definition _) as x -> ce2pres term2pres x
- and ce2pres_in_proof_context_element = function
+and ce2pres_in_proof_context_element term2pres = function
| `Joint ho ->
- B.H ([],(List.map ce2pres_in_joint_context_element ho.Content.joint_defs))
- | (`Declaration _) as x -> ce2pres x
- | (`Hypothesis _) as x -> ce2pres x
- | (`Proof _) as x -> ce2pres x
- | (`Definition _) as x -> ce2pres x
+ B.H ([],(List.map (ce2pres_in_joint_context_element term2pres) ho.Content.joint_defs))
+ | (`Declaration _)
+ | (`Hypothesis _)
+ | (`Proof _)
+ | (`Definition _) as x -> ce2pres term2pres x
- and ce2pres =
+and ce2pres term2pres =
function
`Declaration d ->
let ty = term2pres d.Con.dec_type in
B.Text([],")");
B.Text([],".")])
| `Proof p ->
- proof2pres false p false
+ proof2pres0 term2pres false p false
| `Definition d ->
let term = term2pres d.Con.def_term in
B.H ([],
B.Text([],Utf8Macro.unicode_of_tex "\\def");
term])
- and acontext2pres is_top_down ac continuation indent in_bu_conversion =
+and acontext2pres term2pres is_top_down ac continuation indent in_bu_conversion =
let rec aux =
function
[] -> continuation
[] -> in_bu_conversion
| p::_ -> p.Con.proof_conclude.Con.conclude_method = "BU_Conversion"
in
- let hd = proof2pres is_top_down p in_bu_conversion in
+ let hd = proof2pres0 term2pres is_top_down p in_bu_conversion in
let hd = if indent then B.indent hd else hd in
B.V([Some "helm","xref",p.Con.proof_id],
[B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]);
continuation])
in aux ac
- and conclude2pres ?skip_initial_lambdas_internal is_top_down name conclude indent omit_conclusion in_bu_conversion =
+and conclude2pres term2pres ?skip_initial_lambdas_internal is_top_down name conclude indent omit_conclusion in_bu_conversion =
let tconclude_body =
match conclude.Con.conclude_conclusion with
Some t (*when not omit_conclusion or
B.Text([],".")] else [B.Text([],".")])
else if conclude.Con.conclude_method = "FalseInd" then
(* false ind is in charge to add the conclusion *)
- falseind conclude
+ falseind term2pres conclude
else
let prequel =
if
else
[] in
let conclude_body =
- conclude_aux ?skip_initial_lambdas_internal is_top_down conclude in
+ conclude_aux term2pres ?skip_initial_lambdas_internal is_top_down conclude in
let ann_concl =
if conclude.Con.conclude_method = "Intros+LetTac"
|| conclude.Con.conclude_method = "ByInduction"
) @ if not in_bu_conversion then [B.Text([],".")] else [])
in
B.V ([], prequel @ [conclude_body; ann_concl])
- | _ -> conclude_aux ?skip_initial_lambdas_internal is_top_down conclude
+ | _ -> conclude_aux term2pres ?skip_initial_lambdas_internal is_top_down conclude
in
if indent then
B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id],
else
B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body])
- and conclude_aux ?skip_initial_lambdas_internal is_top_down conclude =
+and conclude_aux term2pres ?skip_initial_lambdas_internal is_top_down conclude =
if conclude.Con.conclude_method = "TD_Conversion" then
let expected =
(match conclude.Con.conclude_conclusion with
([],
[make_concl "we need to prove" expected;
B.H ([],[make_concl "or equivalently" synth; B.Text([],".")]);
- proof2pres true subproof false])
+ proof2pres0 term2pres true subproof false])
else if conclude.Con.conclude_method = "BU_Conversion" then
assert false
else if conclude.Con.conclude_method = "Exact" then
[Con.ArgProof p] ->
(match conclude.Con.conclude_args with
[Con.ArgProof p] ->
- proof2pres ?skip_initial_lambdas_internal true p false
+ proof2pres0 term2pres ?skip_initial_lambdas_internal true p false
| _ -> assert false)
| _ -> assert false)
(* OLD CODE
B.V
([None,"align","baseline 1"; None,"equalrows","false";
None,"columnalign","left"],
- [B.H([],[B.Object([],proof2pres p false)]);
+ [B.H([],[B.Object([],proof2pres p term2pres false)]);
B.H([],[B.Object([],
(make_concl "we proved 1" conclusion))])]);
| _ -> assert false)
*)
else if (conclude.Con.conclude_method = "Case") then
- case conclude
+ case term2pres conclude
else if (conclude.Con.conclude_method = "ByInduction") then
- byinduction conclude
+ byinduction term2pres conclude
else if (conclude.Con.conclude_method = "Exists") then
- exists conclude
+ exists term2pres conclude
else if (conclude.Con.conclude_method = "AndInd") then
- andind conclude
+ andind term2pres conclude
else if (conclude.Con.conclude_method = "FalseInd") then
- falseind conclude
+ falseind term2pres conclude
else if conclude.Con.conclude_method = "RewriteLR"
|| conclude.Con.conclude_method = "RewriteRL" then
let justif1,justif2 =
else
B.V ([], [
B.b_kw ("Apply method" ^ conclude.Con.conclude_method ^ " to");
- (B.indent (B.V ([], args2pres conclude.Con.conclude_args)))])
+ (B.indent (B.V ([], args2pres term2pres conclude.Con.conclude_args)))])
- and args2pres l = List.map arg2pres l
+and args2pres term2pres l = List.map (arg2pres term2pres) l
- and arg2pres =
+and arg2pres term2pres =
function
Con.Aux n -> B.b_kw ("aux " ^ n)
| Con.Premise prem -> B.b_kw "premise"
| Con.Lemma lemma -> B.b_kw "lemma"
| Con.Term (_,t) -> term2pres t
- | Con.ArgProof p -> proof2pres true p false
+ | Con.ArgProof p -> proof2pres0 term2pres true p false
| Con.ArgMethod s -> B.b_kw "method"
- and case conclude =
+and case term2pres conclude =
let proof_conclusion =
(match conclude.Con.conclude_conclusion with
None -> B.b_kw "No conclusion???"
(make_concl "we proceed by cases on" case_arg) in
let to_prove =
(make_concl "to prove" proof_conclusion) in
- B.V ([], case_on::to_prove::(make_cases args_for_cases))
+ B.V ([], case_on::to_prove::(make_cases term2pres args_for_cases))
- and byinduction conclude =
+and byinduction term2pres conclude =
let proof_conclusion =
(match conclude.Con.conclude_conclusion with
None -> B.b_kw "No conclusion???"
(make_concl "we proceed by induction on" arg) in
let to_prove =
B.H ([], [make_concl "to prove" proof_conclusion ; B.Text([],".")]) in
- B.V ([], induction_on::to_prove::(make_cases args_for_cases))
+ B.V ([], induction_on::to_prove::(make_cases term2pres args_for_cases))
- and make_cases l = List.map make_case l
+and make_cases term2pres l = List.map (make_case term2pres) l
- and make_case =
+and make_case term2pres =
function
Con.ArgProof p ->
let name =
let hyps = List.map make_hyp indhyps in
text::hyps) in
let body =
- conclude2pres true p.Con.proof_name p.Con.proof_conclude true true false in
+ conclude2pres term2pres true p.Con.proof_name p.Con.proof_conclude true true false in
let presacontext =
let acontext_id =
match p.Con.proof_apply_context with
in
B.Action([None,"type","toggle"],
[ B.indent (add_xref acontext_id (B.b_kw "Proof"));
- acontext2pres
+ acontext2pres term2pres
(p.Con.proof_conclude.Con.conclude_method = "BU_Conversion")
p.Con.proof_apply_context body true
(p.Con.proof_conclude.Con.conclude_method = "BU_Conversion")
B.V ([], pattern::induction_hypothesis@[B.H ([],[asubconcl;B.Text([],".")]);presacontext])
| _ -> assert false
- and falseind conclude =
+and falseind term2pres conclude =
let proof_conclusion =
(match conclude.Con.conclude_conclusion with
None -> B.b_kw "No conclusion???"
| _ -> assert false) in
make_row arg proof_conclusion
- and andind conclude =
+and andind term2pres conclude =
let proof,case_arg =
(match conclude.Con.conclude_args with
[Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg
B.skip;
term2pres hyp2.Con.dec_type]) in
let body =
- conclude2pres false proof.Con.proof_name proof.Con.proof_conclude
+ conclude2pres term2pres false proof.Con.proof_name proof.Con.proof_conclude
false true false in
let presacontext =
- acontext2pres false proof.Con.proof_apply_context body false false
+ acontext2pres term2pres false proof.Con.proof_apply_context body false false
in
B.V
([],
presacontext]);
| _ -> assert false
- and exists conclude =
+and exists term2pres conclude =
let proof =
(match conclude.Con.conclude_args with
[Con.Aux(n);_;Con.ArgProof proof;_] -> proof
B.skip;
term2pres hyp.Con.dec_type]) in
let body =
- conclude2pres false proof.Con.proof_name proof.Con.proof_conclude
+ conclude2pres term2pres false proof.Con.proof_name proof.Con.proof_conclude
false true false in
let presacontext =
- acontext2pres false proof.Con.proof_apply_context body false false
+ acontext2pres term2pres false proof.Con.proof_apply_context body false false
in
B.V
([],
presacontext]);
| _ -> assert false
- in
- proof2pres
- ?skip_initial_lambdas_internal:
- (match skip_initial_lambdas with
- None -> Some (`Later 0) (* we already printed theorem: *)
- | Some n -> Some (`Later n))
- is_top_down p false
+and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
+ proof2pres0 term2pres
+ ?skip_initial_lambdas_internal:
+ (match skip_initial_lambdas with
+ None -> Some (`Later 0) (* we already printed theorem: *)
+ | Some n -> Some (`Later n))
+ is_top_down p false
exception ToDo
(List.map (njoint_def2pres term2pres) defs)))
;;
-let ncontent2pres0
+let nobj2pres0
?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres
(id,metasenv,obj : NotationPt.term Content.cobj)
=
match obj with
| `Def (Content.Const, thesis, `Proof p) ->
let name = get_name p.Content.proof_name in
- let proof = proof2pres true term2pres ?skip_initial_lambdas p in
+ let proof = proof2pres true ?skip_initial_lambdas term2pres p in
if skip_thm_and_qed then
proof
else
joint.Content.joint_kind joint.Content.joint_defs]
| _ -> raise ToDo
-let ncontent2pres status ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs =
+let nterm2pres status ~ids_to_nrefs =
let lookup_uri id =
try
let nref = Hashtbl.find ids_to_nrefs id in
Some (NReference.string_of_reference nref)
with Not_found -> None
in
- ncontent2pres0 ?skip_initial_lambdas ?skip_thm_and_qed
- (fun ?(prec=90) ast ->
- CicNotationPres.box_of_mpres
- (CicNotationPres.render ~lookup_uri ~prec
- (TermContentPres.pp_ast status ast)))
+ fun ?(prec=90) ast ->
+ CicNotationPres.box_of_mpres
+ (CicNotationPres.render status ~lookup_uri ~prec
+ (TermContentPres.pp_ast status ast))
+
+let nobj2pres status ~ids_to_nrefs =
+ nobj2pres0 ?skip_initial_lambdas:None ?skip_thm_and_qed:None
+ (nterm2pres status ~ids_to_nrefs)
+
+let nconjlist2pres0 term2pres context =
+ let rec aux accum =
+ function
+ [] -> accum
+ | None::tl -> aux accum tl
+ | (Some (`Declaration d))::tl ->
+ let
+ { Con.dec_name = dec_name ;
+ Con.dec_id = dec_id ;
+ Con.dec_type = ty } = d in
+ let r =
+ Box.b_h [Some "helm", "xref", dec_id]
+ [ Box.b_object (p_mi []
+ (match dec_name with
+ None -> "_"
+ | Some n -> n)) ;
+ Box.b_space; Box.b_text [] ":"; Box.b_space;
+ term2pres ty] in
+ aux (r::accum) tl
+ | (Some (`Definition d))::tl ->
+ let
+ { Con.def_name = def_name ;
+ Con.def_id = def_id ;
+ Con.def_term = bo } = d in
+ let r =
+ Box.b_h [Some "helm", "xref", def_id]
+ [ Box.b_object (p_mi []
+ (match def_name with
+ None -> "_"
+ | Some n -> n)) ; Box.b_space ;
+ Box.b_text [] (Utf8Macro.unicode_of_tex "\\def") ;
+ Box.b_space; term2pres bo] in
+ aux (r::accum) tl
+ | _::_ -> assert false
+ in
+ if context <> [] then [Box.b_v [] (aux [] context)] else []
+
+let sequent2pres0 term2pres (_,_,context,ty) =
+ let pres_context = nconjlist2pres0 term2pres context in
+ let pres_goal = term2pres ty in
+ (Box.b_h [] [
+ Box.b_space;
+ (Box.b_v []
+ (Box.b_space ::
+ pres_context @ [
+ b_ink [None,"width","4cm"; None,"height","2px"]; (* sequent line *)
+ Box.b_space;
+ pres_goal]))])
+
+let ncontext2pres status ~ids_to_nrefs ctx =
+ let ctx = HExtlib.filter_map (fun x -> x) ctx in
+ context2pres (nterm2pres status ~ids_to_nrefs) ~continuation:Box.smallskip
+ (ctx:>NotationPt.term Con.in_proof_context_element list)
+
+let nsequent2pres status ~ids_to_nrefs =
+ sequent2pres0 (nterm2pres status ~ids_to_nrefs)
projects / helm.git / blobdiff