X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcontent_pres%2Fcontent2pres.ml;fp=helm%2Focaml%2Fcontent_pres%2Fcontent2pres.ml;h=948eb7b9ac7c58293123397cc150de0f4705349a;hp=0000000000000000000000000000000000000000;hb=792b5d29ebae8f917043d9dd226692919b5d6ca1;hpb=a14a8c7637fd0b95e9d4deccb20c6abc98e8f953 diff --git a/helm/ocaml/content_pres/content2pres.ml b/helm/ocaml/content_pres/content2pres.ml new file mode 100644 index 000000000..948eb7b9a --- /dev/null +++ b/helm/ocaml/content_pres/content2pres.ml @@ -0,0 +1,817 @@ +(* Copyright (C) 2003-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(***************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 17/06/2003 *) +(* *) +(***************************************************************************) + +(* $Id$ *) + +module P = Mpresentation +module B = Box +module Con = Content + +let p_mtr a b = Mpresentation.Mtr(a,b) +let p_mtd a b = Mpresentation.Mtd(a,b) +let p_mtable a b = Mpresentation.Mtable(a,b) +let p_mtext a b = Mpresentation.Mtext(a,b) +let p_mi a b = Mpresentation.Mi(a,b) +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 rec split n l = + if n = 0 then [],l + else let l1,l2 = + split (n-1) (List.tl l) in + (List.hd l)::l1,l2 + +let get_xref = function + | `Declaration d + | `Hypothesis d -> d.Con.dec_id + | `Proof p -> p.Con.proof_id + | `Definition d -> d.Con.def_id + | `Joint jo -> jo.Con.joint_id + +let hv_attrs = + RenderingAttrs.spacing_attributes `BoxML + @ RenderingAttrs.indent_attributes `BoxML + +let make_row items concl = + B.b_hv hv_attrs (items @ [ concl ]) +(* match concl with + B.V _ -> |+ big! +| + B.b_v attrs [B.b_h [] items; B.b_indent concl] + | _ -> |+ small +| + B.b_h attrs (items@[B.b_space; concl]) *) + +let make_concl ?(attrs=[]) verb concl = + B.b_hv (hv_attrs @ attrs) [ B.b_kw verb; concl ] +(* match concl with + B.V _ -> |+ big! +| + B.b_v attrs [ B.b_kw verb; B.b_indent concl] + | _ -> |+ small +| + B.b_h attrs [ B.b_kw verb; B.b_space; concl ] *) + +let make_args_for_apply term2pres args = + let make_arg_for_apply is_first arg row = + let res = + match arg with + Con.Aux n -> assert false + | Con.Premise prem -> + let name = + (match prem.Con.premise_binder with + None -> "previous" + | Some s -> s) in + (B.b_object (P.Mi ([], name)))::row + | Con.Lemma lemma -> + let lemma_attrs = [ + Some "helm", "xref", lemma.Con.lemma_id; + Some "xlink", "href", lemma.Con.lemma_uri ] + in + (B.b_object (P.Mi(lemma_attrs,lemma.Con.lemma_name)))::row + | Con.Term t -> + if is_first then + (term2pres t)::row + else (B.b_object (P.Mi([],"_")))::row + | Con.ArgProof _ + | Con.ArgMethod _ -> + (B.b_object (P.Mi([],"_")))::row + in + if is_first then res else B.skip::res + in + match args with + hd::tl -> + make_arg_for_apply true hd + (List.fold_right (make_arg_for_apply false) tl []) + | _ -> assert false + +let get_name = function + | Some s -> s + | None -> "_" + +let add_xref id = function + | B.Text (attrs, t) -> B.Text (((Some "helm", "xref", id) :: attrs), t) + | _ -> assert false (* TODO, add_xref is meaningful for all boxes *) + +let rec justification term2pres p = + if ((p.Con.proof_conclude.Con.conclude_method = "Exact") or + ((p.Con.proof_context = []) & + (p.Con.proof_apply_context = []) & + (p.Con.proof_conclude.Con.conclude_method = "Apply"))) then + let pres_args = + 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([],")")]) + else proof2pres term2pres p + +and proof2pres term2pres p = + let rec proof2pres p = + let indent = + let is_decl e = + (match e with + `Declaration _ + | `Hypothesis _ -> true + | _ -> false) in + ((List.filter is_decl p.Con.proof_context) != []) in + let omit_conclusion = (not indent) && (p.Con.proof_context != []) in + let concl = + (match p.Con.proof_conclude.Con.conclude_conclusion with + None -> None + | Some t -> Some (term2pres t)) in + let body = + let presconclude = + conclude2pres p.Con.proof_conclude indent omit_conclusion in + let presacontext = + acontext2pres p.Con.proof_apply_context presconclude indent in + context2pres p.Con.proof_context presacontext in + match p.Con.proof_name with + None -> body + | Some name -> + let action = + match concl with + None -> body + | Some ac -> + B.Action + ([None,"type","toggle"], + [(make_concl ~attrs:[Some "helm", "xref", p.Con.proof_id] + "proof of" ac); body]) + in + B.V ([], + [B.Text ([],"(" ^ name ^ ")"); + B.indent action]) + + and context2pres 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; + the whole context-proof is already selectable *) + match c with + [] -> continuation + | hd::tl -> + let continuation' = + List.fold_right + (fun ce continuation -> + 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]); + 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]); + continuation']) + + and ce2pres_in_joint_context_element = 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 + + and ce2pres_in_proof_context_element = 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 + + 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) + | `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) + | `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) + + and acontext2pres ac continuation indent = + List.fold_right + (fun p continuation -> + let hd = + if indent then + B.indent (proof2pres p) + else + proof2pres p in + B.V([Some "helm","xref",p.Con.proof_id], + [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]); + continuation])) ac continuation + + and conclude2pres conclude indent omit_conclusion = + let tconclude_body = + match conclude.Con.conclude_conclusion with + Some t when + not omit_conclusion or + (* CSC: I ignore the omit_conclusion flag in this case. *) + (* CSC: Is this the correct behaviour? In the stylesheets *) + (* CSC: we simply generated nothing (i.e. the output type *) + (* CSC: of the function should become an option. *) + conclude.Con.conclude_method = "BU_Conversion" -> + let concl = (term2pres t) in + if conclude.Con.conclude_method = "BU_Conversion" then + make_concl "that is equivalent to" concl + else if conclude.Con.conclude_method = "FalseInd" then + (* false ind is in charge to add the conclusion *) + falseind conclude + else + let conclude_body = conclude_aux conclude in + let ann_concl = + if conclude.Con.conclude_method = "TD_Conversion" then + make_concl "that is equivalent to" concl + else make_concl "we conclude" concl in + B.V ([], [conclude_body; ann_concl]) + | _ -> conclude_aux conclude in + if indent then + B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id], + [tconclude_body])) + else + B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body]) + + and conclude_aux conclude = + if conclude.Con.conclude_method = "TD_Conversion" then + let expected = + (match conclude.Con.conclude_conclusion with + None -> B.Text([],"NO EXPECTED!!!") + | Some c -> term2pres c) in + let subproof = + (match conclude.Con.conclude_args with + [Con.ArgProof p] -> p + | _ -> assert false) in + let synth = + (match subproof.Con.proof_conclude.Con.conclude_conclusion with + None -> B.Text([],"NO SYNTH!!!") + | Some c -> (term2pres c)) in + B.V + ([], + [make_concl "we must prove" expected; + make_concl "or equivalently" synth; + proof2pres subproof]) + else if conclude.Con.conclude_method = "BU_Conversion" then + assert false + else if conclude.Con.conclude_method = "Exact" then + let arg = + (match conclude.Con.conclude_args with + [Con.Term t] -> term2pres t + | [Con.Premise p] -> + (match p.Con.premise_binder with + | None -> assert false; (* unnamed hypothesis ??? *) + | Some s -> B.Text([],s)) + | err -> assert false) in + (match conclude.Con.conclude_conclusion with + None -> + B.b_h [] [B.b_kw "Consider"; B.b_space; arg] + | Some c -> let conclusion = term2pres c in + make_row + [arg; B.b_space; B.b_kw "proves"] + conclusion + ) + else if conclude.Con.conclude_method = "Intros+LetTac" then + (match conclude.Con.conclude_args with + [Con.ArgProof p] -> proof2pres p + | _ -> assert false) +(* OLD CODE + let conclusion = + (match conclude.Con.conclude_conclusion with + None -> B.Text([],"NO Conclusion!!!") + | Some c -> term2pres c) in + (match conclude.Con.conclude_args with + [Con.ArgProof p] -> + B.V + ([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], + [B.H([],[B.Object([],proof2pres p)]); + B.H([],[B.Object([], + (make_concl "we proved 1" conclusion))])]); + | _ -> assert false) +*) + else if (conclude.Con.conclude_method = "Case") then + case conclude + else if (conclude.Con.conclude_method = "ByInduction") then + byinduction conclude + else if (conclude.Con.conclude_method = "Exists") then + exists conclude + else if (conclude.Con.conclude_method = "AndInd") then + andind conclude + else if (conclude.Con.conclude_method = "FalseInd") then + falseind conclude + else if (conclude.Con.conclude_method = "Rewrite") then + let justif = + (match (List.nth conclude.Con.conclude_args 6) with + Con.ArgProof p -> justification term2pres p + | _ -> assert false) in + let term1 = + (match List.nth conclude.Con.conclude_args 2 with + Con.Term t -> term2pres t + | _ -> assert false) in + let term2 = + (match List.nth conclude.Con.conclude_args 5 with + Con.Term t -> term2pres t + | _ -> assert false) in + B.V ([], + [B.H ([],[ + (B.b_kw "rewrite"); + B.b_space; term1; + B.b_space; (B.b_kw "with"); + B.b_space; term2; + B.indent justif])]) + else if conclude.Con.conclude_method = "Apply" then + let pres_args = + make_args_for_apply term2pres conclude.Con.conclude_args in + B.H([], + (B.b_kw "by"):: + B.b_space:: + B.Text([],"(")::pres_args@[B.Text([],")")]) + else + B.V ([], [ + B.b_kw ("Apply method" ^ conclude.Con.conclude_method ^ " to"); + (B.indent (B.V ([], args2pres conclude.Con.conclude_args)))]) + + and args2pres l = List.map arg2pres l + + and arg2pres = + 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 p + | Con.ArgMethod s -> B.b_kw "method" + + and case conclude = + let proof_conclusion = + (match conclude.Con.conclude_conclusion with + None -> B.b_kw "No conclusion???" + | Some t -> term2pres t) in + let arg,args_for_cases = + (match conclude.Con.conclude_args with + Con.Aux(_)::Con.Aux(_)::Con.Term(_)::arg::tl -> + arg,tl + | _ -> assert false) in + let case_on = + let case_arg = + (match arg with + Con.Aux n -> B.b_kw "an aux???" + | Con.Premise prem -> + (match prem.Con.premise_binder with + None -> B.b_kw "the previous result" + | Some n -> B.Object ([], P.Mi([],n))) + | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name)) + | Con.Term t -> + term2pres t + | Con.ArgProof p -> B.b_kw "a proof???" + | Con.ArgMethod s -> B.b_kw "a method???") + in + (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)) + + and byinduction conclude = + let proof_conclusion = + (match conclude.Con.conclude_conclusion with + None -> B.b_kw "No conclusion???" + | Some t -> term2pres t) in + let inductive_arg,args_for_cases = + (match conclude.Con.conclude_args with + Con.Aux(n)::_::tl -> + let l1,l2 = split (int_of_string n) tl in + let last_pos = (List.length l2)-1 in + List.nth l2 last_pos,l1 + | _ -> assert false) in + let induction_on = + let arg = + (match inductive_arg with + Con.Aux n -> B.b_kw "an aux???" + | Con.Premise prem -> + (match prem.Con.premise_binder with + None -> B.b_kw "the previous result" + | Some n -> B.Object ([], P.Mi([],n))) + | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name)) + | Con.Term t -> + term2pres t + | Con.ArgProof p -> B.b_kw "a proof???" + | Con.ArgMethod s -> B.b_kw "a method???") in + (make_concl "we proceed by induction on" arg) in + let to_prove = + (make_concl "to prove" proof_conclusion) in + B.V ([], induction_on::to_prove:: (make_cases args_for_cases)) + + and make_cases l = List.map make_case l + + and make_case = + function + Con.ArgProof p -> + let name = + (match p.Con.proof_name with + None -> B.b_kw "no name for case!!" + | Some n -> B.Object ([], P.Mi([],n))) in + let indhyps,args = + List.partition + (function + `Hypothesis h -> h.Con.dec_inductive + | _ -> false) p.Con.proof_context in + let pattern_aux = + List.fold_right + (fun e p -> + let dec = + (match e with + `Declaration h + | `Hypothesis h -> + let name = + (match h.Con.dec_name with + None -> "NO NAME???" + | Some n ->n) in + [B.b_space; + B.Object ([], P.Mi ([],name)); + B.Text([],":"); + (term2pres h.Con.dec_type)] + | _ -> [B.Text ([],"???")]) in + dec@p) args [] in + let pattern = + B.H ([], + (B.b_kw "Case"::B.b_space::name::pattern_aux)@ + [B.b_space; + B.Text([], Utf8Macro.unicode_of_tex "\\Rightarrow")]) in + let subconcl = + (match p.Con.proof_conclude.Con.conclude_conclusion with + None -> B.b_kw "No conclusion!!!" + | Some t -> term2pres t) in + let asubconcl = B.indent (make_concl "the thesis becomes" subconcl) in + let induction_hypothesis = + (match indhyps with + [] -> [] + | _ -> + let text = B.indent (B.b_kw "by induction hypothesis we know") in + let make_hyp = + function + `Hypothesis h -> + let name = + (match h.Con.dec_name with + None -> "no name" + | Some s -> s) in + B.indent (B.H ([], + [B.Text([],"("); + B.Object ([], P.Mi ([],name)); + B.Text([],")"); + B.b_space; + term2pres h.Con.dec_type])) + | _ -> assert false in + let hyps = List.map make_hyp indhyps in + text::hyps) in + (* let acontext = + acontext2pres_old p.Con.proof_apply_context true in *) + let body = conclude2pres p.Con.proof_conclude true false in + let presacontext = + let acontext_id = + match p.Con.proof_apply_context with + [] -> p.Con.proof_conclude.Con.conclude_id + | {Con.proof_id = id}::_ -> id + in + B.Action([None,"type","toggle"], + [ B.indent (add_xref acontext_id (B.b_kw "Proof")); + acontext2pres p.Con.proof_apply_context body true]) in + B.V ([], pattern::asubconcl::induction_hypothesis@[presacontext]) + | _ -> assert false + + and falseind conclude = + let proof_conclusion = + (match conclude.Con.conclude_conclusion with + None -> B.b_kw "No conclusion???" + | Some t -> term2pres t) in + let case_arg = + (match conclude.Con.conclude_args with + [Con.Aux(n);_;case_arg] -> case_arg + | _ -> assert false; + (* + List.map (ContentPp.parg 0) conclude.Con.conclude_args; + assert false *)) in + let arg = + (match case_arg with + Con.Aux n -> assert false + | Con.Premise prem -> + (match prem.Con.premise_binder with + None -> [B.b_kw "Contradiction, hence"] + | Some n -> + [ B.Object ([],P.Mi([],n)); B.skip; + B.b_kw "is contradictory, hence"]) + | Con.Lemma lemma -> + [ B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip; + B.b_kw "is contradictory, hence" ] + | _ -> assert false) in + (* let body = proof2pres {proof with Con.proof_context = tl} in *) + make_row arg proof_conclusion + + and andind conclude = + let proof,case_arg = + (match conclude.Con.conclude_args with + [Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg + | _ -> assert false; + (* + List.map (ContentPp.parg 0) conclude.Con.conclude_args; + assert false *)) in + let arg = + (match case_arg with + Con.Aux n -> assert false + | Con.Premise prem -> + (match prem.Con.premise_binder with + None -> [] + | Some n -> [(B.b_kw "by"); B.b_space; B.Object([], P.Mi([],n))]) + | Con.Lemma lemma -> + [(B.b_kw "by");B.skip; + B.Object([], P.Mi([],lemma.Con.lemma_name))] + | _ -> 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.Text([],")"); + B.skip; + term2pres hyp1.Con.dec_type]) in + let preshyp2 = + B.H ([], + [B.Text([],"("); + B.Object ([], P.Mi([],get_name hyp2)); + B.Text([],")"); + B.skip; + term2pres hyp2.Con.dec_type]) in + (* let body = proof2pres {proof with Con.proof_context = tl} in *) + let body = conclude2pres proof.Con.proof_conclude false true in + let presacontext = + acontext2pres proof.Con.proof_apply_context body false in + B.V + ([], + [B.H ([],arg@[B.skip; B.b_kw "we have"]); + preshyp1; + B.b_kw "and"; + preshyp2; + presacontext]); + | _ -> assert false + + and exists conclude = + let proof = + (match conclude.Con.conclude_args with + [Con.Aux(n);_;Con.ArgProof proof;_] -> proof + | _ -> assert false; + (* + List.map (ContentPp.parg 0) conclude.Con.conclude_args; + assert false *)) 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.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.Text([],")"); + B.skip; + term2pres hyp.Con.dec_type]) in + (* let body = proof2pres {proof with Con.proof_context = tl} in *) + let body = conclude2pres proof.Con.proof_conclude false true in + let presacontext = + acontext2pres proof.Con.proof_apply_context body false in + B.V + ([], + [presdecl; + suchthat; + presacontext]); + | _ -> assert false + + in + proof2pres p + +exception ToDo + +let counter = ref 0 + +let conjecture2pres term2pres (id, n, context, ty) = + (B.b_h [Some "helm", "xref", id] + (((List.map + (function + | None -> + B.b_h [] + [ B.b_object (p_mi [] "_") ; + B.b_object (p_mo [] ":?") ; + B.b_object (p_mi [] "_")] + | Some (`Declaration d) + | Some (`Hypothesis d) -> + let { Content.dec_name = + dec_name ; Content.dec_type = ty } = d + in + B.b_h [] + [ B.b_object + (p_mi [] + (match dec_name with + None -> "_" + | Some n -> n)); + B.b_text [] ":"; + term2pres ty ] + | Some (`Definition d) -> + let + { Content.def_name = def_name ; + Content.def_term = bo } = d + in + B.b_h [] + [ B.b_object (p_mi [] + (match def_name with + None -> "_" + | Some n -> n)) ; + B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign"); + term2pres bo] + | Some (`Proof p) -> + let proof_name = p.Content.proof_name in + B.b_h [] + [ B.b_object (p_mi [] + (match proof_name with + None -> "_" + | Some n -> n)) ; + B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign"); + proof2pres term2pres p]) + (List.rev context)) @ + [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash"); + B.b_object (p_mi [] (string_of_int n)) ; + B.b_text [] ":" ; + term2pres ty ]))) + +let metasenv2pres term2pres = function + | None -> [] + | Some metasenv' -> + (* Conjectures are in their own table to make *) + (* diffing the DOM trees easier. *) + [B.b_v [] + ((B.b_kw ("Conjectures:" ^ + (let _ = incr counter; in (string_of_int !counter)))) :: + (List.map (conjecture2pres term2pres) metasenv'))] + +let params2pres params = + let param2pres uri = + B.b_text [Some "xlink", "href", UriManager.string_of_uri uri] + (UriManager.name_of_uri uri) + in + let rec spatiate = function + | [] -> [] + | hd :: [] -> [hd] + | hd :: tl -> hd :: B.b_text [] ", " :: spatiate tl + in + match params with + | [] -> [] + | p -> + let params = spatiate (List.map param2pres p) in + [B.b_space; + B.b_h [] (B.b_text [] "[" :: params @ [ B.b_text [] "]" ])] + +let recursion_kind2pres params kind = + let kind = + match kind with + | `Recursive _ -> "Recursive definition" + | `CoRecursive -> "CoRecursive definition" + | `Inductive _ -> "Inductive definition" + | `CoInductive _ -> "CoInductive definition" + in + B.b_h [] (B.b_kw kind :: params2pres params) + +let inductive2pres term2pres ind = + let constructor2pres decl = + B.b_h [] [ + B.b_text [] ("| " ^ get_name decl.Content.dec_name ^ ":"); + B.b_space; + term2pres decl.Content.dec_type + ] + in + B.b_v [] + (B.b_h [] [ + B.b_kw (ind.Content.inductive_name ^ " of arity"); + B.smallskip; + term2pres ind.Content.inductive_type ] + :: List.map constructor2pres ind.Content.inductive_constructors) + +let joint_def2pres term2pres def = + match def with + | `Inductive ind -> inductive2pres term2pres ind + | _ -> assert false (* ZACK or raise ToDo? *) + +let content2pres term2pres (id,params,metasenv,obj) = + match obj with + | `Def (Content.Const, thesis, `Proof p) -> + let name = get_name p.Content.proof_name in + B.b_v + [Some "helm","xref","id"] + ([ B.b_h [] (B.b_kw ("Proof " ^ name) :: params2pres params); + B.b_kw "Thesis:"; + B.indent (term2pres thesis) ] @ + metasenv2pres term2pres metasenv @ + [proof2pres term2pres p]) + | `Def (_, ty, `Definition body) -> + let name = get_name body.Content.def_name in + B.b_v + [Some "helm","xref","id"] + ([B.b_h [] (B.b_kw ("Definition " ^ name) :: params2pres params); + B.b_kw "Type:"; + B.indent (term2pres ty)] @ + metasenv2pres term2pres metasenv @ + [B.b_kw "Body:"; term2pres body.Content.def_term]) + | `Decl (_, `Declaration decl) + | `Decl (_, `Hypothesis decl) -> + let name = get_name decl.Content.dec_name in + B.b_v + [Some "helm","xref","id"] + ([B.b_h [] (B.b_kw ("Axiom " ^ name) :: params2pres params); + B.b_kw "Type:"; + B.indent (term2pres decl.Content.dec_type)] @ + metasenv2pres term2pres metasenv) + | `Joint joint -> + B.b_v [] + (recursion_kind2pres params joint.Content.joint_kind + :: List.map (joint_def2pres term2pres) joint.Content.joint_defs) + | _ -> raise ToDo + +let content2pres ~ids_to_inner_sorts = + content2pres + (fun annterm -> + let ast, ids_to_uris = + TermAcicContent.ast_of_acic ids_to_inner_sorts annterm + in + CicNotationPres.box_of_mpres + (CicNotationPres.render ids_to_uris + (TermContentPres.pp_ast ast))) +