1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (***************************************************************************)
30 (* Andrea Asperti <asperti@cs.unibo.it> *)
33 (***************************************************************************)
35 module P = Mpresentation
38 let p_mtr a b = Mpresentation.Mtr(a,b)
39 let p_mtd a b = Mpresentation.Mtd(a,b)
40 let p_mtable a b = Mpresentation.Mtable(a,b)
41 let p_mtext a b = Mpresentation.Mtext(a,b)
42 let p_mi a b = Mpresentation.Mi(a,b)
43 let p_mo a b = Mpresentation.Mo(a,b)
44 let p_mrow a b = Mpresentation.Mrow(a,b)
45 let p_mphantom a b = Mpresentation.Mphantom(a,b)
50 split (n-1) (List.tl l) in
55 let is_big_general countterm p =
56 let maxsize = Ast2pres.maxsize in
57 let module Con = Content in
58 let rec countp current_size p =
59 if current_size > maxsize then current_size
61 let c1 = (countcontext current_size p.Con.proof_context) in
62 if c1 > maxsize then c1
64 let c2 = (countapplycontext c1 p.Con.proof_apply_context) in
65 if c2 > maxsize then c2
67 countconclude c2 p.Con.proof_conclude
70 countcontext current_size c =
71 List.fold_left countcontextitem current_size c
73 countcontextitem current_size e =
74 if current_size > maxsize then maxsize
78 (match d.Con.dec_name with
79 Some s -> current_size + 4 + (String.length s)
80 | None -> prerr_endline "NO NAME!!"; assert false)
82 (match h.Con.dec_name with
83 Some s -> current_size + 4 + (String.length s)
84 | None -> prerr_endline "NO NAME!!"; assert false)
85 | `Proof p -> countp current_size p
87 (match d.Con.def_name with
89 let c1 = (current_size + 4 + (String.length s)) in
90 (countterm c1 d.Con.def_term)
92 prerr_endline "NO NAME!!"; assert false)
93 | `Joint ho -> maxsize + 1) (* we assume is big *)
95 countapplycontext current_size ac =
96 List.fold_left countp current_size ac
98 countconclude current_size co =
99 if current_size > maxsize then current_size
101 let c1 = countargs current_size co.Con.conclude_args in
102 if c1 > maxsize then c1
104 (match co.Con.conclude_conclusion with
105 Some concl -> countterm c1 concl
108 countargs current_size args =
109 List.fold_left countarg current_size args
111 countarg current_size arg =
112 if current_size > maxsize then current_size
115 Con.Aux _ -> current_size
116 | Con.Premise prem ->
117 (match prem.Con.premise_binder with
118 Some s -> current_size + (String.length s)
119 | None -> current_size + 7)
121 current_size + (String.length lemma.Con.lemma_name)
122 | Con.Term t -> countterm current_size t
123 | Con.ArgProof p -> countp current_size p
124 | Con.ArgMethod s -> (maxsize + 1)) in
125 let size = (countp 0 p) in
129 let is_big = is_big_general (Ast2pres.countterm)
133 let module Con = Content in
136 | `Hypothesis d -> d.Con.dec_id
137 | `Proof p -> p.Con.proof_id
138 | `Definition d -> d.Con.def_id
139 | `Joint jo -> jo.Con.joint_id
142 let make_row ?(attrs=[]) items concl =
145 B.b_v attrs [B.b_h [] items; B.b_indent concl]
147 B.b_h attrs (items@[B.b_space; concl])
150 let make_concl ?(attrs=[]) verb concl =
153 B.b_v attrs [ B.b_kw verb; B.b_indent concl]
155 B.b_h attrs [ B.b_kw verb; B.b_space; concl ]
158 let make_args_for_apply term2pres args =
159 let module Con = Content in
160 let make_arg_for_apply is_first arg row =
163 Con.Aux n -> assert false
164 | Con.Premise prem ->
166 (match prem.Con.premise_binder with
169 (B.b_object (P.Mi ([], name)))::row
171 (B.b_object (P.Mi([],lemma.Con.lemma_name)))::row
175 else (B.b_object (P.Mi([],"_")))::row
178 (B.b_object (P.Mi([],"_")))::row
180 if is_first then res else B.skip::res
184 make_arg_for_apply true hd
185 (List.fold_right (make_arg_for_apply false) tl [])
189 let get_name = function
193 let rec justification term2pres p =
194 let module Con = Content in
195 let module P = Mpresentation in
196 if ((p.Con.proof_conclude.Con.conclude_method = "Exact") or
197 ((p.Con.proof_context = []) &
198 (p.Con.proof_apply_context = []) &
199 (p.Con.proof_conclude.Con.conclude_method = "Apply"))) then
201 make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in
203 (B.b_kw "by")::B.b_space::
204 B.Text([],"(")::pres_args@[B.Text([],")")])
205 else proof2pres term2pres p
207 and proof2pres term2pres p =
208 let rec proof2pres p =
209 let module Con = Content in
214 | `Hypothesis _ -> true
216 ((List.filter is_decl p.Con.proof_context) != []) in
217 let omit_conclusion = (not indent) && (p.Con.proof_context != []) in
219 (match p.Con.proof_conclude.Con.conclude_conclusion with
221 | Some t -> Some (term2pres t)) in
224 conclude2pres p.Con.proof_conclude indent omit_conclusion in
226 acontext2pres p.Con.proof_apply_context presconclude indent in
227 context2pres p.Con.proof_context presacontext in
228 match p.Con.proof_name with
236 ([None,"type","toggle"],
237 [(make_concl ~attrs:[Some "helm", "xref", p.Con.proof_id]
238 "proof of" ac); body])
241 [B.Text ([],"(" ^ name ^ ")");
244 and context2pres c continuation =
245 (* we generate a subtable for each context element, for selection
247 The table generated by the head-element does not have an xref;
248 the whole context-proof is already selectable *)
254 (fun ce continuation ->
255 let xref = get_xref ce in
256 B.V([Some "helm", "xref", xref ],
257 [B.H([Some "helm", "xref", "ce_"^xref],[ce2pres ce]);
258 continuation])) tl continuation in
259 let hd_xref= get_xref hd in
261 [B.H([Some "helm", "xref", "ce_"^hd_xref],
266 let module Con = Content in
269 (match d.Con.dec_name with
271 let ty = term2pres d.Con.dec_type in
275 B.Object ([], P.Mi([],s));
279 prerr_endline "NO NAME!!"; assert false)
281 (match h.Con.dec_name with
283 let ty = term2pres h.Con.dec_type in
288 B.Object ([], P.Mi ([],s));
293 prerr_endline "NO NAME!!"; assert false)
297 (match d.Con.def_name with
299 let term = term2pres d.Con.def_term in
302 B.Object ([], P.Mi([],s));
306 prerr_endline "NO NAME!!"; assert false)
308 B.Text ([],"jointdef")
310 and acontext2pres ac continuation indent =
311 let module Con = Content in
313 (fun p continuation ->
316 B.indent (proof2pres p)
319 B.V([Some "helm","xref",p.Con.proof_id],
320 [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]);
321 continuation])) ac continuation
323 and conclude2pres conclude indent omit_conclusion =
324 let module Con = Content in
325 let module P = Mpresentation in
327 match conclude.Con.conclude_conclusion with
329 not omit_conclusion or
330 (* CSC: I ignore the omit_conclusion flag in this case. *)
331 (* CSC: Is this the correct behaviour? In the stylesheets *)
332 (* CSC: we simply generated nothing (i.e. the output type *)
333 (* CSC: of the function should become an option. *)
334 conclude.Con.conclude_method = "BU_Conversion" ->
335 let concl = (term2pres t) in
336 if conclude.Con.conclude_method = "BU_Conversion" then
337 make_concl "that is equivalent to" concl
338 else if conclude.Con.conclude_method = "FalseInd" then
339 (* false ind is in charge to add the conclusion *)
342 let conclude_body = conclude_aux conclude in
344 if conclude.Con.conclude_method = "TD_Conversion" then
345 make_concl "that is equivalent to" concl
346 else make_concl "we conclude" concl in
347 B.V ([], [conclude_body; ann_concl])
348 | _ -> conclude_aux conclude in
350 B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id],
353 B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body])
356 and conclude_aux conclude =
357 let module Con = Content in
358 let module P = Mpresentation in
359 if conclude.Con.conclude_method = "TD_Conversion" then
361 (match conclude.Con.conclude_conclusion with
362 None -> B.Text([],"NO EXPECTED!!!")
363 | Some c -> term2pres c) in
365 (match conclude.Con.conclude_args with
366 [Con.ArgProof p] -> p
367 | _ -> assert false) in
369 (match subproof.Con.proof_conclude.Con.conclude_conclusion with
370 None -> B.Text([],"NO SYNTH!!!")
371 | Some c -> (term2pres c)) in
374 [make_concl "we must prove" expected;
375 make_concl "or equivalently" synth;
376 proof2pres subproof])
377 else if conclude.Con.conclude_method = "BU_Conversion" then
379 else if conclude.Con.conclude_method = "Exact" then
381 (match conclude.Con.conclude_args with
382 [Con.Term t] -> term2pres t
383 | _ -> assert false) in
384 (match conclude.Con.conclude_conclusion with
386 B.b_h [] [B.b_kw "Consider"; B.b_space; arg]
387 | Some c -> let conclusion = term2pres c in
389 [arg; B.b_space; B.Text([],"proves")]
392 else if conclude.Con.conclude_method = "Intros+LetTac" then
393 (match conclude.Con.conclude_args with
394 [Con.ArgProof p] -> proof2pres p
398 (match conclude.Con.conclude_conclusion with
399 None -> B.Text([],"NO Conclusion!!!")
400 | Some c -> term2pres c) in
401 (match conclude.Con.conclude_args with
404 ([None,"align","baseline 1"; None,"equalrows","false";
405 None,"columnalign","left"],
406 [B.H([],[B.Object([],proof2pres p)]);
408 (make_concl "we proved 1" conclusion))])]);
411 else if (conclude.Con.conclude_method = "Case") then
413 else if (conclude.Con.conclude_method = "ByInduction") then
415 else if (conclude.Con.conclude_method = "Exists") then
417 else if (conclude.Con.conclude_method = "AndInd") then
419 else if (conclude.Con.conclude_method = "FalseInd") then
421 else if (conclude.Con.conclude_method = "Rewrite") then
423 (match (List.nth conclude.Con.conclude_args 6) with
424 Con.ArgProof p -> justification term2pres p
425 | _ -> assert false) in
427 (match List.nth conclude.Con.conclude_args 2 with
428 Con.Term t -> term2pres t
429 | _ -> assert false) in
431 (match List.nth conclude.Con.conclude_args 5 with
432 Con.Term t -> term2pres t
433 | _ -> assert false) in
438 B.b_space; (B.b_kw "with");
441 else if conclude.Con.conclude_method = "Apply" then
443 make_args_for_apply term2pres conclude.Con.conclude_args in
447 B.Text([],"(")::pres_args@[B.Text([],")")])
451 [B.Text([],"Apply method" ^ conclude.Con.conclude_method ^ " to");
455 args2pres conclude.Con.conclude_args)))])
457 and args2pres l = List.map arg2pres l
460 let module Con = Content in
463 B.Text ([],"aux " ^ n)
464 | Con.Premise prem ->
465 B.Text ([],"premise")
476 let module Con = Content in
477 let proof_conclusion =
478 (match conclude.Con.conclude_conclusion with
479 None -> B.Text([],"No conclusion???")
480 | Some t -> term2pres t) in
481 let arg,args_for_cases =
482 (match conclude.Con.conclude_args with
483 Con.Aux(_)::Con.Aux(_)::Con.Term(_)::arg::tl ->
485 | _ -> assert false) in
490 B.Text ([],"an aux???")
491 | Con.Premise prem ->
492 (match prem.Con.premise_binder with
493 None -> B.Text ([],"the previous result")
494 | Some n -> B.Object ([], P.Mi([],n)))
495 | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name))
499 B.Text ([],"a proof???")
501 B.Text ([],"a method???")) in
502 (make_concl "we proceede by cases on" case_arg) in
504 (make_concl "to prove" proof_conclusion) in
507 case_on::to_prove::(make_cases args_for_cases))
509 and byinduction conclude =
510 let module Con = Content in
511 let proof_conclusion =
512 (match conclude.Con.conclude_conclusion with
513 None -> B.Text([],"No conclusion???")
514 | Some t -> term2pres t) in
515 let inductive_arg,args_for_cases =
516 (match conclude.Con.conclude_args with
518 let l1,l2 = split (int_of_string n) tl in
519 let last_pos = (List.length l2)-1 in
520 List.nth l2 last_pos,l1
521 | _ -> assert false) in
524 (match inductive_arg with
526 B.Text ([],"an aux???")
527 | Con.Premise prem ->
528 (match prem.Con.premise_binder with
529 None -> B.Text ([],"the previous result")
530 | Some n -> B.Object ([], P.Mi([],n)))
531 | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name))
535 B.Text ([],"a proof???")
537 B.Text ([],"a method???")) in
538 (make_concl "we proceede by induction on" arg) in
540 (make_concl "to prove" proof_conclusion) in
543 induction_on::to_prove::
544 (make_cases args_for_cases))
546 and make_cases l = List.map make_case l
549 let module Con = Content in
553 (match p.Con.proof_name with
554 None -> B.Text([],"no name for case!!")
555 | Some n -> B.Object ([], P.Mi([],n))) in
559 `Hypothesis h -> h.Con.dec_inductive
560 | _ -> false) p.Con.proof_context in
569 (match h.Con.dec_name with
573 B.Object ([], P.Mi ([],name));
575 (term2pres h.Con.dec_type)]
576 | _ -> [B.Text ([],"???")]) in
580 (B.Text([],"Case")::B.b_space::name::pattern_aux)@
584 (match p.Con.proof_conclude.Con.conclude_conclusion with
585 None -> B.Text([],"No conclusion!!!")
586 | Some t -> term2pres t) in
587 let asubconcl = B.indent (make_concl "the thesis becomes" subconcl) in
588 let induction_hypothesis =
593 B.indent (B.Text([],"by induction hypothesis we know:")) in
598 (match h.Con.dec_name with
603 B.Object ([], P.Mi ([],name));
606 term2pres h.Con.dec_type]))
607 | _ -> assert false in
608 let hyps = List.map make_hyp indhyps in
611 acontext2pres_old p.Con.proof_apply_context true in *)
612 let body = conclude2pres p.Con.proof_conclude true false in
615 match p.Con.proof_apply_context with
616 [] -> p.Con.proof_conclude.Con.conclude_id
617 | {Con.proof_id = id}::_ -> id
619 B.Action([None,"type","toggle"],
622 ([None,"color","red" ;
623 Some "helm", "xref", acontext_id],"Proof")) ;
624 acontext2pres p.Con.proof_apply_context body true]) in
625 B.V ([], pattern::asubconcl::induction_hypothesis@[presacontext])
628 and falseind conclude =
629 let module P = Mpresentation in
630 let module Con = Content in
631 let proof_conclusion =
632 (match conclude.Con.conclude_conclusion with
633 None -> B.Text([],"No conclusion???")
634 | Some t -> term2pres t) in
636 (match conclude.Con.conclude_args with
637 [Con.Aux(n);_;case_arg] -> case_arg
640 List.map (ContentPp.parg 0) conclude.Con.conclude_args;
644 Con.Aux n -> assert false
645 | Con.Premise prem ->
646 (match prem.Con.premise_binder with
647 None -> [B.Text([],"Contradiction, hence")]
649 [B.Object ([],P.Mi([],n)); B.skip;B.Text([],"is contradictory, hence")])
651 [B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip; B.Text([],"is contradictory, hence")]
652 | _ -> assert false) in
653 (* let body = proof2pres {proof with Con.proof_context = tl} in *)
654 make_row arg proof_conclusion
656 and andind conclude =
657 let module P = Mpresentation in
658 let module Con = Content in
659 let proof_conclusion =
660 (match conclude.Con.conclude_conclusion with
661 None -> B.Text([],"No conclusion???")
662 | Some t -> term2pres t) in
664 (match conclude.Con.conclude_args with
665 [Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg
668 List.map (ContentPp.parg 0) conclude.Con.conclude_args;
672 Con.Aux n -> assert false
673 | Con.Premise prem ->
674 (match prem.Con.premise_binder with
676 | Some n -> [(B.b_kw "by"); B.b_space; B.Object([], P.Mi([],n))])
678 [(B.b_kw "by");B.skip; B.Object([], P.Mi([],lemma.Con.lemma_name))]
679 | _ -> assert false) in
680 match proof.Con.proof_context with
681 `Hypothesis hyp1::`Hypothesis hyp2::tl ->
683 (match hyp.Con.dec_name with
689 B.Object ([], P.Mi([],get_name hyp1));
692 term2pres hyp1.Con.dec_type]) in
696 B.Object ([], P.Mi([],get_name hyp2));
699 term2pres hyp2.Con.dec_type]) in
700 (* let body = proof2pres {proof with Con.proof_context = tl} in *)
701 let body = conclude2pres proof.Con.proof_conclude false true in
703 acontext2pres proof.Con.proof_apply_context body false in
706 [B.H ([],arg@[B.skip; B.Text([],"we have")]);
713 and exists conclude =
714 let module P = Mpresentation in
715 let module Con = Content in
716 let proof_conclusion =
717 (match conclude.Con.conclude_conclusion with
718 None -> B.Text([],"No conclusion???")
719 | Some t -> term2pres t) in
721 (match conclude.Con.conclude_args with
722 [Con.Aux(n);_;Con.ArgProof proof;_] -> proof
725 List.map (ContentPp.parg 0) conclude.Con.conclude_args;
727 match proof.Con.proof_context with
728 `Declaration decl::`Hypothesis hyp::tl
729 | `Hypothesis decl::`Hypothesis hyp::tl ->
731 (match decl.Con.dec_name with
738 B.Object ([], P.Mi([],get_name decl));
739 B.Text([],":"); term2pres decl.Con.dec_type]) in
742 [(B.b_kw "such that");
745 B.Object ([], P.Mi([],get_name hyp));
748 term2pres hyp.Con.dec_type]) in
749 (* let body = proof2pres {proof with Con.proof_context = tl} in *)
750 let body = conclude2pres proof.Con.proof_conclude false true in
752 acontext2pres proof.Con.proof_apply_context body false in
758 | _ -> assert false in
767 let conjecture2pres term2pres (id, n, context, ty) =
768 (B.b_h [Some "helm", "xref", id]
773 [ B.b_object (p_mi [] "_") ;
774 B.b_object (p_mo [] ":?") ;
775 B.b_object (p_mi [] "_")]
776 | Some (`Declaration d)
777 | Some (`Hypothesis d) ->
778 let { Content.dec_name =
779 dec_name ; Content.dec_type = ty } = d
789 | Some (`Definition d) ->
791 { Content.def_name = def_name ;
792 Content.def_term = bo } = d
795 [ B.b_object (p_mi []
802 let proof_name = p.Content.proof_name in
804 [ B.b_object (p_mi []
805 (match proof_name with
809 proof2pres term2pres p])
810 (List.rev context)) @
812 B.b_object (p_mi [] (string_of_int n)) ;
816 let metasenv2pres term2pres = function
819 (* Conjectures are in their own table to make *)
820 (* diffing the DOM trees easier. *)
824 (let _ = incr counter; in (string_of_int !counter)))) ::
825 (List.map (conjecture2pres term2pres) metasenv'))]
827 let params2pres params =
829 B.b_text [Some "xlink", "href", UriManager.string_of_uri uri]
830 (UriManager.name_of_uri uri)
832 let rec spatiate = function
835 | hd :: tl -> hd :: B.b_text [] ", " :: spatiate tl
840 let params = spatiate (List.map param2pres p) in
842 B.b_h [] (B.b_text [] "[" :: params @ [ B.b_text [] "]" ])]
844 let recursion_kind2pres params kind =
847 | `Recursive _ -> "Recursive definition"
848 | `CoRecursive -> "CoRecursive definition"
849 | `Inductive _ -> "Inductive definition"
850 | `CoInductive _ -> "CoInductive definition"
852 B.b_h [] (B.b_text [] kind :: params2pres params)
854 let inductive2pres term2pres ind =
855 let constructor2pres decl =
857 B.b_text [] ("| " ^ get_name decl.Content.dec_name ^ ":");
859 term2pres decl.Content.dec_type
864 B.b_text [] (ind.Content.inductive_name ^ " of arity ");
865 term2pres ind.Content.inductive_type ]
866 :: List.map constructor2pres ind.Content.inductive_constructors)
868 let joint_def2pres term2pres def =
870 | `Inductive ind -> inductive2pres term2pres ind
871 | _ -> assert false (* ZACK or raise ToDo? *)
873 let content2pres term2pres (id,params,metasenv,obj) =
875 | `Def (Content.Const, thesis, `Proof p) ->
876 let name = get_name p.Content.proof_name in
878 [Some "helm","xref","id"]
879 ([ B.b_h [] (B.b_text [] ("Proof " ^ name) :: params2pres params);
880 B.b_text [] "Thesis:";
881 B.indent (term2pres thesis) ] @
882 metasenv2pres term2pres metasenv @
883 [proof2pres term2pres p])
884 | `Def (_, ty, `Definition body) ->
885 let name = get_name body.Content.def_name in
887 [Some "helm","xref","id"]
888 ([B.b_h [] (B.b_text [] ("Definition " ^ name) :: params2pres params);
890 B.indent (term2pres ty)] @
891 metasenv2pres term2pres metasenv @
892 [term2pres body.Content.def_term])
893 | `Decl (_, `Declaration decl)
894 | `Decl (_, `Hypothesis decl) ->
895 let name = get_name decl.Content.dec_name in
897 [Some "helm","xref","id"]
898 ([B.b_h [] (B.b_text [] ("Axiom " ^ name) :: params2pres params);
900 B.indent (term2pres decl.Content.dec_type)] @
901 metasenv2pres term2pres metasenv)
904 (recursion_kind2pres params joint.Content.joint_kind
905 :: List.map (joint_def2pres term2pres) joint.Content.joint_defs)
910 let content2pres ~ids_to_inner_sorts =
913 (Cexpr2pres.cexpr2pres_charcount
914 (Content_expressions.acic2cexpr ids_to_inner_sorts p)))
918 let content2pres ~ids_to_inner_sorts =
921 let (ast, ids_to_uris) as arg =
922 Acic2Ast.ast_of_acic ids_to_inner_sorts annterm
924 let astBox = Ast2pres.ast2astBox arg in
925 Box.map (fun ast -> Ast2pres.ast2mpres (ast, ids_to_uris)) astBox)