(* 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 rec make_arg_for_apply is_first arg row = (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.smallskip::P.Mi([],name)::row | Con.Lemma lemma -> P.smallskip::P.Mi([],lemma.Con.lemma_name)::row | Con.Term t -> if is_first then (term2pres t)::row else P.smallskip::P.Mi([],"_")::row | Con.ArgProof _ | Con.ArgMethod _ -> P.smallskip::P.Mi([],"_")::row) 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 ac = (match concl with None -> P.Mtext([],"NO PROOF!!!") | Some c -> c) in let action = 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.Mtext([],"("); P.Mi ([],s); P.Mtext([],")"); P.Mspace([None,"width","0.1cm"]); 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 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 = 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 conclusion = (match conclude.Con.conclude_conclusion with None -> P.Mtext([],"NO Conclusion!!!") | Some c -> term2pres c) in let arg = (match conclude.Con.conclude_args with [Con.Term t] -> term2pres t | _ -> assert false) 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 = "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)) (* OLD CODE let we_proved = (make_concl "we proved 5" 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) @ [P.Mtr ([],[P.Mtd ([],we_proved)])]) *) 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.Mtext([],"("); P.Mi ([],name); P.Mtext([],")"); 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 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 [] (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))) ;;