X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;fp=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=65d33f9171eedc75b8e657ef39eb419e73ffb128;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml deleted file mode 100644 index 65d33f917..000000000 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ /dev/null @@ -1,881 +0,0 @@ -(* Copyright (C) 2000, 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 *) -(* *) -(***************************************************************************) - -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 is_big_general countterm p = - let maxsize = Cexpr2pres.maxsize in - let module Con = Content in - let rec countp current_size p = - if current_size > maxsize then current_size - else - let c1 = (countcontext current_size p.Con.proof_context) in - if c1 > maxsize then c1 - else - let c2 = (countapplycontext c1 p.Con.proof_apply_context) in - if c2 > maxsize then c2 - else - countconclude c2 p.Con.proof_conclude - - and - countcontext current_size c = - List.fold_left countcontextitem current_size c - and - countcontextitem current_size e = - if current_size > maxsize then maxsize - else - (match e with - `Declaration d -> - (match d.Con.dec_name with - Some s -> current_size + 4 + (String.length s) - | None -> prerr_endline "NO NAME!!"; assert false) - | `Hypothesis h -> - (match h.Con.dec_name with - Some s -> current_size + 4 + (String.length s) - | None -> prerr_endline "NO NAME!!"; assert false) - | `Proof p -> countp current_size p - | `Definition d -> - (match d.Con.def_name with - Some s -> - let c1 = (current_size + 4 + (String.length s)) in - (countterm c1 d.Con.def_term) - | None -> - prerr_endline "NO NAME!!"; assert false) - | `Joint ho -> maxsize + 1) (* we assume is big *) - and - countapplycontext current_size ac = - List.fold_left countp current_size ac - and - countconclude current_size co = - if current_size > maxsize then current_size - else - let c1 = countargs current_size co.Con.conclude_args in - if c1 > maxsize then c1 - else - (match co.Con.conclude_conclusion with - Some concl -> countterm c1 concl - | None -> c1) - and - countargs current_size args = - List.fold_left countarg current_size args - and - countarg current_size arg = - if current_size > maxsize then current_size - else - (match arg with - Con.Aux _ -> current_size - | Con.Premise prem -> - (match prem.Con.premise_binder with - Some s -> current_size + (String.length s) - | None -> current_size + 7) - | Con.Lemma lemma -> - current_size + (String.length lemma.Con.lemma_name) - | Con.Term t -> countterm current_size t - | Con.ArgProof p -> countp current_size p - | Con.ArgMethod s -> (maxsize + 1)) in - let size = (countp 0 p) in - (size > maxsize) -;; - -let is_big = is_big_general (Cexpr2pres.countterm) -;; - -let get_xref = - let module Con = Content in - 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 make_row ?(attrs=[]) items concl = - let module P = Mpresentation in - (match concl with - P.Mtable _ -> (* big! *) - P.Mtable (attrs@[None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr([],[P.Mtd ([],P.Mrow([],items))]); - P.Mtr ([],[P.Mtd ([],P.indented concl)])]) - | _ -> (* small *) - P.Mrow(attrs,items@[P.Mspace([None,"width","0.1cm"]);concl])) -;; - -let make_concl ?(attrs=[]) verb concl = - let module P = Mpresentation in - (match concl with - P.Mtable _ -> (* big! *) - P.Mtable (attrs@[None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr([],[P.Mtd ([],P.Mtext([None,"mathcolor","Red"],verb))]); - P.Mtr ([],[P.Mtd ([],P.indented concl)])]) - | _ -> (* small *) - P.Mrow(attrs, - [P.Mtext([None,"mathcolor","Red"],verb); - P.Mspace([None,"width","0.1cm"]); - concl])) -;; - -let make_args_for_apply term2pres args = - let module Con = Content in - let module P = Mpresentation in - 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 - P.Mi([],name)::row - | Con.Lemma lemma -> - P.Mi([],lemma.Con.lemma_name)::row - | Con.Term t -> - if is_first then - (term2pres t)::row - else P.Mi([],"_")::row - | Con.ArgProof _ - | Con.ArgMethod _ -> - P.Mi([],"_")::row - in - if is_first then res else P.smallskip::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 rec justification term2pres p = - let module Con = Content in - let module P = Mpresentation in - 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 - P.Mrow([], - P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"]):: - P.Mo([],"(")::pres_args@[P.Mo([],")")]) - else proof2pres term2pres p - -and proof2pres term2pres p = - let rec proof2pres p = - let module Con = Content in - let module P = Mpresentation in - 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 -(* - P.Maction - ([None,"actiontype","toggle" ; None,"selection","1"], - [P.Mtext [] "proof" ; body]) -*) - | Some ac -> - P.Maction - ([None,"actiontype","toggle" ; None,"selection","1"], - [(make_concl "proof of" ac); body]) - in - P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]); - P.Mtr ([],[P.Mtd ([], P.indented action)])]) -(* - P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left";Some "helm", "xref", p.Con.proof_id], - [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]); - P.Mtr ([],[P.Mtd ([], P.indented 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 *) - let module P = Mpresentation in - match c with - [] -> continuation - | hd::tl -> - let continuation' = - List.fold_right - (fun ce continuation -> - let xref = get_xref ce in - P.Mtable([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"; Some "helm", "xref", xref ], - [P.Mtr([Some "helm", "xref", "ce_"^xref],[P.Mtd ([],ce2pres ce)]); - P.Mtr([],[P.Mtd ([], continuation)])])) tl continuation in - let hd_xref= get_xref hd in - P.Mtable([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr([Some "helm", "xref", "ce_"^hd_xref], - [P.Mtd ([],ce2pres hd)]); - P.Mtr([],[P.Mtd ([], continuation')])]) - - and ce2pres = - let module P = Mpresentation in - let module Con = Content in - function - `Declaration d -> - (match d.Con.dec_name with - Some s -> - let ty = term2pres d.Con.dec_type in - P.Mrow ([], - [P.Mtext([None,"mathcolor","Red"],"Assume"); - P.Mspace([None,"width","0.1cm"]); - P.Mi([],s); - P.Mtext([],":"); - 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 - P.Mrow ([], - [P.Mtext([None,"mathcolor","Red"],"Suppose"); - P.Mspace([None,"width","0.1cm"]); - P.Mo([],"("); - P.Mi ([],s); - P.Mo([],")"); - P.Mspace([None,"width","0.1cm"]); - ty]) - | None -> - prerr_endline "NO NAME!!"; assert false) - | `Proof p -> - (match p.Con.proof_name with - Some "w" -> prerr_endline ("processing w"); - | _ -> ()); - proof2pres p - | `Definition d -> - (match d.Con.def_name with - Some s -> - let term = term2pres d.Con.def_term in - P.Mrow ([], - [P.Mtext([],"Let "); - P.Mi([],s); - P.Mtext([]," = "); - term]) - | None -> - prerr_endline "NO NAME!!"; assert false) - | `Joint ho -> - P.Mtext ([],"jointdef") - - and acontext2pres ac continuation indent = - let module Con = Content in - let module P = Mpresentation in - List.fold_right - (fun p continuation -> - let hd = - if indent then - P.indented (proof2pres p) - else - proof2pres p in - P.Mtable([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"; Some "helm","xref",p.Con.proof_id], - [P.Mtr([Some "helm","xref","ace_"^p.Con.proof_id],[P.Mtd ([],hd)]); - P.Mtr([],[P.Mtd ([], continuation)])])) ac continuation - - and conclude2pres conclude indent omit_conclusion = - let module Con = Content in - let module P = Mpresentation in - let tconclude_body = - match conclude.Con.conclude_conclusion with - Some t when not omit_conclusion -> - let concl = (term2pres t) in - if conclude.Con.conclude_method = "BU_Conversion" then - make_concl "that is equivalent to" concl - 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 - P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr ([],[P.Mtd ([],conclude_body)]); - P.Mtr ([],[P.Mtd ([],ann_concl)])]) - | _ -> conclude_aux conclude in - if indent then - P.indented (P.Mrow ([Some "helm", "xref", conclude.Con.conclude_id], - [tconclude_body])) - else - P.Mrow ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body]) - - - and conclude_aux conclude = - let module Con = Content in - let module P = Mpresentation in - if conclude.Con.conclude_method = "TD_Conversion" then - let expected = - (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"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 -> P.Mtext([],"NO SYNTH!!!") - | Some c -> (term2pres c)) in - P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], - [P.Mtr([],[P.Mtd([],make_concl "we must prove" expected)]); - P.Mtr([],[P.Mtd([],make_concl "or equivalently" synth)]); - P.Mtr([],[P.Mtd([],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 - | _ -> assert false) in - (match conclude.Con.conclude_conclusion with - None -> - P.Mrow [] - [P.Mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg] - | Some c -> let conclusion = term2pres c in - make_row - [arg; P.Mspace([None,"width","0.1cm"]);P.Mtext([],"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 -> P.Mtext([],"NO Conclusion!!!") - | Some c -> term2pres c) in - (match conclude.Con.conclude_args with - [Con.ArgProof p] -> - P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr([],[P.Mtd([],proof2pres p)]); - P.Mtr([],[P.Mtd([], - (make_concl "we proved 1" conclusion))])]); - | _ -> assert false) -*) - 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 = "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 - P.Mtable ([None,"align","baseline 1";None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr ([],[P.Mtd ([],P.Mrow([],[ - P.Mtext([None,"mathcolor","Red"],"rewrite"); - P.Mspace([None,"width","0.1cm"]);term1; - P.Mspace([None,"width","0.1cm"]); - P.Mtext([None,"mathcolor","Red"],"with"); - P.Mspace([None,"width","0.1cm"]);term2]))]); - P.Mtr ([],[P.Mtd ([],P.indented justif)])]); -(* OLD CODE - let conclusion = - (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"NO Conclusion!!!") - | Some c -> term2pres c) in - P.Mtable ([None,"align","baseline 1";None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr ([],[P.Mtd ([],P.Mrow([],[ - P.Mtext([None,"mathcolor","Red"],"rewrite"); - P.Mspace([None,"width","0.1cm"]);term1; - P.Mspace([None,"width","0.1cm"]); - P.Mtext([None,"mathcolor","Red"],"with"); - P.Mspace([None,"width","0.1cm"]);term2]))]); - P.Mtr ([],[P.Mtd ([],P.indented justif)]); - P.Mtr ([],[P.Mtd ([],make_concl "we proved 2" conclusion)])]) *) - else if conclude.Con.conclude_method = "Apply" then - let pres_args = - make_args_for_apply term2pres conclude.Con.conclude_args in - P.Mrow([], - P.Mtext([None,"mathcolor","Red"],"by"):: - P.Mspace([None,"width","0.1cm"]):: - P.Mo([],"(")::pres_args@[P.Mo([],")")]) -(* OLD CODE - let by = - P.Mrow([], - P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"]):: - P.Mo([],"(")::pres_args@[P.Mo([],")")]) in - match conclude.Con.conclude_conclusion with - None -> P.Mrow([],[P.Mtext([],"QUA");by]) - | Some t -> - let concl = (term2pres t) in - let ann_concl = make_concl "we proved 3" concl in - P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"; - Some "helm", "xref", conclude.Con.conclude_id], - [P.Mtr ([],[P.Mtd ([],by)]); - P.Mtr ([],[P.Mtd ([],ann_concl)])]) *) - else - P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], - [P.Mtr ([],[P.Mtd ([],P.Mtext([],"Apply method" ^ conclude.Con.conclude_method ^ " to"))]); - P.Mtr ([], - [P.Mtd ([], - (P.indented - (P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - args2pres conclude.Con.conclude_args))))])]) -(* OLD CODE - match conclude.Con.conclude_conclusion with - None -> body - | Some t -> - let concl = (term2pres t) in - let ann_concl = make_concl "we proved 4" concl in - P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr ([],[P.Mtd ([],body)]); - P.Mtr ([],[P.Mtd ([],ann_concl)])]) *) - - and args2pres l = - let module P = Mpresentation in - List.map - (function a -> P.Mtr ([], [P.Mtd ([], arg2pres a)])) l - - and arg2pres = - let module P = Mpresentation in - let module Con = Content in - function - Con.Aux n -> - P.Mtext ([],"aux " ^ n) - | Con.Premise prem -> - P.Mtext ([],"premise") - | Con.Lemma lemma -> - P.Mtext ([],"lemma") - | Con.Term t -> - term2pres t - | Con.ArgProof p -> - proof2pres p - | Con.ArgMethod s -> - P.Mtext ([],"method") - - and byinduction conclude = - let module P = Mpresentation in - let module Con = Content in - let proof_conclusion = - (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"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 -> - P.Mtext ([],"an aux???") - | Con.Premise prem -> - (match prem.Con.premise_binder with - None -> P.Mtext ([],"the previous result") - | Some n -> P.Mi([],n)) - | Con.Lemma lemma -> P.Mi([],lemma.Con.lemma_name) - | Con.Term t -> - term2pres t - | Con.ArgProof p -> - P.Mtext ([],"a proof???") - | Con.ArgMethod s -> - P.Mtext ([],"a method???")) in - (make_concl "we proceede by induction on" arg) in - let to_prove = - (make_concl "to prove" proof_conclusion) in - P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - P.Mtr ([],[P.Mtd ([],induction_on)]):: - P.Mtr ([],[P.Mtd ([],to_prove)]):: - (make_cases args_for_cases)) - - and make_cases args_for_cases = - let module P = Mpresentation in - List.map - (fun p -> P.Mtr ([],[P.Mtd ([],make_case p)])) args_for_cases - - and make_case = - let module P = Mpresentation in - let module Con = Content in - function - Con.ArgProof p -> - let name = - (match p.Con.proof_name with - None -> P.Mtext([],"no name for case!!") - | Some n -> 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 - [P.Mspace([None,"width","0.1cm"]); - P.Mi ([],name); - P.Mtext([],":"); - (term2pres h.Con.dec_type)] - | _ -> [P.Mtext ([],"???")]) in - dec@p) args [] in - let pattern = - P.Mtr ([],[P.Mtd ([],P.Mrow([], - P.Mtext([],"Case")::P.Mspace([None,"width","0.1cm"])::name::pattern_aux@ - [P.Mspace([None,"width","0.1cm"]); - P.Mtext([],"->")]))]) in - let subconcl = - (match p.Con.proof_conclude.Con.conclude_conclusion with - None -> P.Mtext([],"No conclusion!!!") - | Some t -> term2pres t) in - let asubconcl = - P.Mtr([],[P.Mtd([], - P.indented (make_concl "the thesis becomes" subconcl))]) in - let induction_hypothesis = - (match indhyps with - [] -> [] - | _ -> - let text = - P.Mtr([],[P.Mtd([], P.indented - (P.Mtext([],"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 - P.indented (P.Mrow ([], - [P.Mo([],"("); - P.Mi ([],name); - P.Mo([],")"); - P.Mspace([None,"width","0.1cm"]); - term2pres h.Con.dec_type])) - | _ -> assert false in - let hyps = - List.map - (function ce -> P.Mtr ([], [P.Mtd ([], make_hyp ce)])) - 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 = - P.Maction([None,"actiontype","toggle" ; None,"selection","1"], - [P.indented (P.Mtext([None,"mathcolor","Red"],"Proof")); - acontext2pres p.Con.proof_apply_context body true]) in - P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - pattern::asubconcl::induction_hypothesis@ - [P.Mtr([],[P.Mtd([],presacontext)])]) - | _ -> assert false - - and andind conclude = - let module P = Mpresentation in - let module Con = Content in - let proof_conclusion = - (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"No conclusion???") - | Some t -> term2pres t) in - 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 -> [P.Mtext([],"by");P.smallskip;P.Mi([],n)]) - | Con.Lemma lemma -> - [P.Mtext([],"by");P.smallskip;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 = - P.Mrow ([], - [P.Mtext([],"("); - P.Mi([],get_name hyp1); - P.Mtext([],")"); - P.smallskip; - term2pres hyp1.Con.dec_type]) in - let preshyp2 = - P.Mrow ([], - [P.Mtext([],"("); - P.Mi([],get_name hyp2); - P.Mtext([],")"); - P.smallskip; - 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 - P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr ([],[P.Mtd ([], - P.Mrow([],arg@[P.smallskip;P.Mtext([],"we have")]))]); - P.Mtr ([],[P.Mtd ([],preshyp1)]); - P.Mtr ([],[P.Mtd ([],P.Mtext([],"and"))]); - P.Mtr ([],[P.Mtd ([],preshyp2)]); - P.Mtr ([],[P.Mtd ([],presacontext)])]); - | _ -> assert false - - and exists conclude = - let module P = Mpresentation in - let module Con = Content in - let proof_conclusion = - (match conclude.Con.conclude_conclusion with - None -> P.Mtext([],"No conclusion???") - | Some t -> term2pres t) in - 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 = - P.Mrow ([], - [P.Mtext([None,"mathcolor","Red"],"let"); - P.smallskip; - P.Mi([],get_name decl); - P.Mtext([],":"); term2pres decl.Con.dec_type]) in - let suchthat = - P.Mrow ([], - [P.Mtext([None,"mathcolor","Red"],"such that"); - P.smallskip; - P.Mtext([],"("); - P.Mi([],get_name hyp); - P.Mtext([],")"); - P.smallskip; - 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 - P.Mtable - ([None,"align","baseline 1"; None,"equalrows","false"; - None,"columnalign","left"], - [P.Mtr ([],[P.Mtd ([],presdecl)]); - P.Mtr ([],[P.Mtd ([],suchthat)]); - P.Mtr ([],[P.Mtd ([],presacontext)])]); - | _ -> assert false in - -proof2pres p -;; - -exception ToDo;; - -let content2pres term2pres (id,params,metasenv,obj) = - let module K = Content in - let module P = Mpresentation in - match obj with - `Def (K.Const,thesis,`Proof p) -> - P.Mtable - [None,"align","baseline 1"; - None,"equalrows","false"; - None,"columnalign","left"; - None,"helm:xref","id"] - ([P.Mtr [] - [P.Mtd [] - (P.Mrow [] - [P.Mtext [] - ("UNFINISHED PROOF" ^ id ^"(" ^ - String.concat " ; " (List.map UriManager.string_of_uri params)^ - ")")])] ; - P.Mtr [] - [P.Mtd [] - (P.Mrow [] - [P.Mtext [] "THESIS:"])] ; - P.Mtr [] - [P.Mtd [] - (P.Mrow [] - [P.Mphantom [] - (P.Mtext [] "__") ; - term2pres thesis])]] @ - (match metasenv with - None -> [] - | Some metasenv' -> - [P.Mtr [] - [P.Mtd [] - (* Conjectures are in their own table to make *) - (* diffing the DOM trees easier. *) - (P.Mtable - [None,"align","baseline 1"; - None,"equalrows","false"; - None,"columnalign","left"] - ((P.Mtr [] - [P.Mtd [] - (P.Mrow [] - [P.Mtext [] "CONJECTURES:"])]):: - List.map - (function - (id,n,context,ty) -> - P.Mtr [] - [P.Mtd [] - (P.Mrow [Some "helm", "xref", id] - (List.map - (function - (_,None) -> - P.Mrow [] - [ P.Mi [] "_" ; - P.Mo [] ":?" ; - P.Mi [] "_"] - | (_,Some (`Declaration d)) - | (_,Some (`Hypothesis d)) -> - let - { K.dec_name = dec_name ; - K.dec_type = ty } = d - in - P.Mrow [] - [ P.Mi [] - (match dec_name with - None -> "_" - | Some n -> n) ; - P.Mo [] ":" ; - term2pres ty] - | (_,Some (`Definition d)) -> - let - { K.def_name = def_name ; - K.def_term = bo } = d - in - P.Mrow [] - [ P.Mi [] - (match def_name with - None -> "_" - | Some n -> n) ; - P.Mo [] ":=" ; - term2pres bo] - | (_,Some (`Proof p)) -> - let proof_name = p.K.proof_name in - P.Mrow [] - [ P.Mi [] - (match proof_name with - None -> "_" - | Some n -> n) ; - P.Mo [] ":=" ; - proof2pres term2pres p] - ) context @ - [ P.Mo [] "|-" ] @ - [ P.Mi [] (string_of_int n) ; - P.Mo [] ":" ; - term2pres ty ] - )) - ] - ) metasenv' - ))]] - ) @ - [P.Mtr [] - [P.Mtd [] - (P.Mrow [] - [proof2pres term2pres p])]]) - | _ -> raise ToDo -;; - -let content2pres ~ids_to_inner_sorts = - content2pres - (function p -> - (Cexpr2pres.cexpr2pres_charcount - (Content_expressions.acic2cexpr ids_to_inner_sorts p))) -;;