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)
307 | `Joint ho -> assert false (*
309 (B.Text ([],"JOINT ")
310 :: List.map ce2pres ho.Content.joint_defs)) *)
312 and acontext2pres ac continuation indent =
313 let module Con = Content in
315 (fun p continuation ->
318 B.indent (proof2pres p)
321 B.V([Some "helm","xref",p.Con.proof_id],
322 [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]);
323 continuation])) ac continuation
325 and conclude2pres conclude indent omit_conclusion =
326 let module Con = Content in
327 let module P = Mpresentation in
329 match conclude.Con.conclude_conclusion with
331 not omit_conclusion or
332 (* CSC: I ignore the omit_conclusion flag in this case. *)
333 (* CSC: Is this the correct behaviour? In the stylesheets *)
334 (* CSC: we simply generated nothing (i.e. the output type *)
335 (* CSC: of the function should become an option. *)
336 conclude.Con.conclude_method = "BU_Conversion" ->
337 let concl = (term2pres t) in
338 if conclude.Con.conclude_method = "BU_Conversion" then
339 make_concl "that is equivalent to" concl
340 else if conclude.Con.conclude_method = "FalseInd" then
341 (* false ind is in charge to add the conclusion *)
344 let conclude_body = conclude_aux conclude in
346 if conclude.Con.conclude_method = "TD_Conversion" then
347 make_concl "that is equivalent to" concl
348 else make_concl "we conclude" concl in
349 B.V ([], [conclude_body; ann_concl])
350 | _ -> conclude_aux conclude in
352 B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id],
355 B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body])
358 and conclude_aux conclude =
359 let module Con = Content in
360 let module P = Mpresentation in
361 if conclude.Con.conclude_method = "TD_Conversion" then
363 (match conclude.Con.conclude_conclusion with
364 None -> B.Text([],"NO EXPECTED!!!")
365 | Some c -> term2pres c) in
367 (match conclude.Con.conclude_args with
368 [Con.ArgProof p] -> p
369 | _ -> assert false) in
371 (match subproof.Con.proof_conclude.Con.conclude_conclusion with
372 None -> B.Text([],"NO SYNTH!!!")
373 | Some c -> (term2pres c)) in
376 [make_concl "we must prove" expected;
377 make_concl "or equivalently" synth;
378 proof2pres subproof])
379 else if conclude.Con.conclude_method = "BU_Conversion" then
381 else if conclude.Con.conclude_method = "Exact" then
383 (match conclude.Con.conclude_args with
384 [Con.Term t] -> term2pres t
386 (match p.Con.premise_binder with
387 | None -> assert false; (* unnamed hypothesis ??? *)
388 | Some s -> B.Text([],s))
389 | err -> assert false) in
390 (match conclude.Con.conclude_conclusion with
392 B.b_h [] [B.b_kw "Consider"; B.b_space; arg]
393 | Some c -> let conclusion = term2pres c in
395 [arg; B.b_space; B.Text([],"proves")]
398 else if conclude.Con.conclude_method = "Intros+LetTac" then
399 (match conclude.Con.conclude_args with
400 [Con.ArgProof p] -> proof2pres p
404 (match conclude.Con.conclude_conclusion with
405 None -> B.Text([],"NO Conclusion!!!")
406 | Some c -> term2pres c) in
407 (match conclude.Con.conclude_args with
410 ([None,"align","baseline 1"; None,"equalrows","false";
411 None,"columnalign","left"],
412 [B.H([],[B.Object([],proof2pres p)]);
414 (make_concl "we proved 1" conclusion))])]);
417 else if (conclude.Con.conclude_method = "Case") then
419 else if (conclude.Con.conclude_method = "ByInduction") then
421 else if (conclude.Con.conclude_method = "Exists") then
423 else if (conclude.Con.conclude_method = "AndInd") then
425 else if (conclude.Con.conclude_method = "FalseInd") then
427 else if (conclude.Con.conclude_method = "Rewrite") then
429 (match (List.nth conclude.Con.conclude_args 6) with
430 Con.ArgProof p -> justification term2pres p
431 | _ -> assert false) in
433 (match List.nth conclude.Con.conclude_args 2 with
434 Con.Term t -> term2pres t
435 | _ -> assert false) in
437 (match List.nth conclude.Con.conclude_args 5 with
438 Con.Term t -> term2pres t
439 | _ -> assert false) in
444 B.b_space; (B.b_kw "with");
447 else if conclude.Con.conclude_method = "Apply" then
449 make_args_for_apply term2pres conclude.Con.conclude_args in
453 B.Text([],"(")::pres_args@[B.Text([],")")])
457 [B.Text([],"Apply method" ^ conclude.Con.conclude_method ^ " to");
461 args2pres conclude.Con.conclude_args)))])
463 and args2pres l = List.map arg2pres l
466 let module Con = Content in
469 B.Text ([],"aux " ^ n)
470 | Con.Premise prem ->
471 B.Text ([],"premise")
482 let module Con = Content in
483 let proof_conclusion =
484 (match conclude.Con.conclude_conclusion with
485 None -> B.Text([],"No conclusion???")
486 | Some t -> term2pres t) in
487 let arg,args_for_cases =
488 (match conclude.Con.conclude_args with
489 Con.Aux(_)::Con.Aux(_)::Con.Term(_)::arg::tl ->
491 | _ -> assert false) in
496 B.Text ([],"an aux???")
497 | Con.Premise prem ->
498 (match prem.Con.premise_binder with
499 None -> B.Text ([],"the previous result")
500 | Some n -> B.Object ([], P.Mi([],n)))
501 | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name))
505 B.Text ([],"a proof???")
507 B.Text ([],"a method???")) in
508 (make_concl "we proceede by cases on" case_arg) in
510 (make_concl "to prove" proof_conclusion) in
513 case_on::to_prove::(make_cases args_for_cases))
515 and byinduction conclude =
516 let module Con = Content in
517 let proof_conclusion =
518 (match conclude.Con.conclude_conclusion with
519 None -> B.Text([],"No conclusion???")
520 | Some t -> term2pres t) in
521 let inductive_arg,args_for_cases =
522 (match conclude.Con.conclude_args with
524 let l1,l2 = split (int_of_string n) tl in
525 let last_pos = (List.length l2)-1 in
526 List.nth l2 last_pos,l1
527 | _ -> assert false) in
530 (match inductive_arg with
532 B.Text ([],"an aux???")
533 | Con.Premise prem ->
534 (match prem.Con.premise_binder with
535 None -> B.Text ([],"the previous result")
536 | Some n -> B.Object ([], P.Mi([],n)))
537 | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name))
541 B.Text ([],"a proof???")
543 B.Text ([],"a method???")) in
544 (make_concl "we proceede by induction on" arg) in
546 (make_concl "to prove" proof_conclusion) in
549 induction_on::to_prove::
550 (make_cases args_for_cases))
552 and make_cases l = List.map make_case l
555 let module Con = Content in
559 (match p.Con.proof_name with
560 None -> B.Text([],"no name for case!!")
561 | Some n -> B.Object ([], P.Mi([],n))) in
565 `Hypothesis h -> h.Con.dec_inductive
566 | _ -> false) p.Con.proof_context in
575 (match h.Con.dec_name with
579 B.Object ([], P.Mi ([],name));
581 (term2pres h.Con.dec_type)]
582 | _ -> [B.Text ([],"???")]) in
586 (B.Text([],"Case")::B.b_space::name::pattern_aux)@
590 (match p.Con.proof_conclude.Con.conclude_conclusion with
591 None -> B.Text([],"No conclusion!!!")
592 | Some t -> term2pres t) in
593 let asubconcl = B.indent (make_concl "the thesis becomes" subconcl) in
594 let induction_hypothesis =
599 B.indent (B.Text([],"by induction hypothesis we know:")) in
604 (match h.Con.dec_name with
609 B.Object ([], P.Mi ([],name));
612 term2pres h.Con.dec_type]))
613 | _ -> assert false in
614 let hyps = List.map make_hyp indhyps in
617 acontext2pres_old p.Con.proof_apply_context true in *)
618 let body = conclude2pres p.Con.proof_conclude true false in
621 match p.Con.proof_apply_context with
622 [] -> p.Con.proof_conclude.Con.conclude_id
623 | {Con.proof_id = id}::_ -> id
625 B.Action([None,"type","toggle"],
628 ([None,"color","red" ;
629 Some "helm", "xref", acontext_id],"Proof")) ;
630 acontext2pres p.Con.proof_apply_context body true]) in
631 B.V ([], pattern::asubconcl::induction_hypothesis@[presacontext])
634 and falseind conclude =
635 let module P = Mpresentation in
636 let module Con = Content in
637 let proof_conclusion =
638 (match conclude.Con.conclude_conclusion with
639 None -> B.Text([],"No conclusion???")
640 | Some t -> term2pres t) in
642 (match conclude.Con.conclude_args with
643 [Con.Aux(n);_;case_arg] -> case_arg
646 List.map (ContentPp.parg 0) conclude.Con.conclude_args;
650 Con.Aux n -> assert false
651 | Con.Premise prem ->
652 (match prem.Con.premise_binder with
653 None -> [B.Text([],"Contradiction, hence")]
655 [B.Object ([],P.Mi([],n)); B.skip;B.Text([],"is contradictory, hence")])
657 [B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip; B.Text([],"is contradictory, hence")]
658 | _ -> assert false) in
659 (* let body = proof2pres {proof with Con.proof_context = tl} in *)
660 make_row arg proof_conclusion
662 and andind conclude =
663 let module P = Mpresentation in
664 let module Con = Content in
665 let proof_conclusion =
666 (match conclude.Con.conclude_conclusion with
667 None -> B.Text([],"No conclusion???")
668 | Some t -> term2pres t) in
670 (match conclude.Con.conclude_args with
671 [Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg
674 List.map (ContentPp.parg 0) conclude.Con.conclude_args;
678 Con.Aux n -> assert false
679 | Con.Premise prem ->
680 (match prem.Con.premise_binder with
682 | Some n -> [(B.b_kw "by"); B.b_space; B.Object([], P.Mi([],n))])
684 [(B.b_kw "by");B.skip; B.Object([], P.Mi([],lemma.Con.lemma_name))]
685 | _ -> assert false) in
686 match proof.Con.proof_context with
687 `Hypothesis hyp1::`Hypothesis hyp2::tl ->
689 (match hyp.Con.dec_name with
695 B.Object ([], P.Mi([],get_name hyp1));
698 term2pres hyp1.Con.dec_type]) in
702 B.Object ([], P.Mi([],get_name hyp2));
705 term2pres hyp2.Con.dec_type]) in
706 (* let body = proof2pres {proof with Con.proof_context = tl} in *)
707 let body = conclude2pres proof.Con.proof_conclude false true in
709 acontext2pres proof.Con.proof_apply_context body false in
712 [B.H ([],arg@[B.skip; B.Text([],"we have")]);
719 and exists conclude =
720 let module P = Mpresentation in
721 let module Con = Content in
722 let proof_conclusion =
723 (match conclude.Con.conclude_conclusion with
724 None -> B.Text([],"No conclusion???")
725 | Some t -> term2pres t) in
727 (match conclude.Con.conclude_args with
728 [Con.Aux(n);_;Con.ArgProof proof;_] -> proof
731 List.map (ContentPp.parg 0) conclude.Con.conclude_args;
733 match proof.Con.proof_context with
734 `Declaration decl::`Hypothesis hyp::tl
735 | `Hypothesis decl::`Hypothesis hyp::tl ->
737 (match decl.Con.dec_name with
744 B.Object ([], P.Mi([],get_name decl));
745 B.Text([],":"); term2pres decl.Con.dec_type]) in
748 [(B.b_kw "such that");
751 B.Object ([], P.Mi([],get_name hyp));
754 term2pres hyp.Con.dec_type]) in
755 (* let body = proof2pres {proof with Con.proof_context = tl} in *)
756 let body = conclude2pres proof.Con.proof_conclude false true in
758 acontext2pres proof.Con.proof_apply_context body false in
764 | _ -> assert false in
773 let conjecture2pres term2pres (id, n, context, ty) =
774 (B.b_h [Some "helm", "xref", id]
779 [ B.b_object (p_mi [] "_") ;
780 B.b_object (p_mo [] ":?") ;
781 B.b_object (p_mi [] "_")]
782 | Some (`Declaration d)
783 | Some (`Hypothesis d) ->
784 let { Content.dec_name =
785 dec_name ; Content.dec_type = ty } = d
795 | Some (`Definition d) ->
797 { Content.def_name = def_name ;
798 Content.def_term = bo } = d
801 [ B.b_object (p_mi []
808 let proof_name = p.Content.proof_name in
810 [ B.b_object (p_mi []
811 (match proof_name with
815 proof2pres term2pres p])
816 (List.rev context)) @
818 B.b_object (p_mi [] (string_of_int n)) ;
822 let metasenv2pres term2pres = function
825 (* Conjectures are in their own table to make *)
826 (* diffing the DOM trees easier. *)
830 (let _ = incr counter; in (string_of_int !counter)))) ::
831 (List.map (conjecture2pres term2pres) metasenv'))]
833 let params2pres params =
835 B.b_text [Some "xlink", "href", UriManager.string_of_uri uri]
836 (UriManager.name_of_uri uri)
838 let rec spatiate = function
841 | hd :: tl -> hd :: B.b_text [] ", " :: spatiate tl
846 let params = spatiate (List.map param2pres p) in
848 B.b_h [] (B.b_text [] "[" :: params @ [ B.b_text [] "]" ])]
850 let recursion_kind2pres params kind =
853 | `Recursive _ -> "Recursive definition"
854 | `CoRecursive -> "CoRecursive definition"
855 | `Inductive _ -> "Inductive definition"
856 | `CoInductive _ -> "CoInductive definition"
858 B.b_h [] (B.b_text [] kind :: params2pres params)
860 let inductive2pres term2pres ind =
861 let constructor2pres decl =
863 B.b_text [] ("| " ^ get_name decl.Content.dec_name ^ ":");
865 term2pres decl.Content.dec_type
870 B.b_text [] (ind.Content.inductive_name ^ " of arity ");
871 term2pres ind.Content.inductive_type ]
872 :: List.map constructor2pres ind.Content.inductive_constructors)
874 let joint_def2pres term2pres def =
876 | `Inductive ind -> inductive2pres term2pres ind
877 | _ -> assert false (* ZACK or raise ToDo? *)
879 let content2pres term2pres (id,params,metasenv,obj) =
881 | `Def (Content.Const, thesis, `Proof p) ->
882 let name = get_name p.Content.proof_name in
884 [Some "helm","xref","id"]
885 ([ B.b_h [] (B.b_text [] ("Proof " ^ name) :: params2pres params);
886 B.b_text [] "Thesis:";
887 B.indent (term2pres thesis) ] @
888 metasenv2pres term2pres metasenv @
889 [proof2pres term2pres p])
890 | `Def (_, ty, `Definition body) ->
891 let name = get_name body.Content.def_name in
893 [Some "helm","xref","id"]
894 ([B.b_h [] (B.b_text [] ("Definition " ^ name) :: params2pres params);
896 B.indent (term2pres ty)] @
897 metasenv2pres term2pres metasenv @
898 [term2pres body.Content.def_term])
899 | `Decl (_, `Declaration decl)
900 | `Decl (_, `Hypothesis decl) ->
901 let name = get_name decl.Content.dec_name in
903 [Some "helm","xref","id"]
904 ([B.b_h [] (B.b_text [] ("Axiom " ^ name) :: params2pres params);
906 B.indent (term2pres decl.Content.dec_type)] @
907 metasenv2pres term2pres metasenv)
910 (recursion_kind2pres params joint.Content.joint_kind
911 :: List.map (joint_def2pres term2pres) joint.Content.joint_defs)
916 let content2pres ~ids_to_inner_sorts =
919 (Cexpr2pres.cexpr2pres_charcount
920 (Content_expressions.acic2cexpr ids_to_inner_sorts p)))
924 let content2pres ~ids_to_inner_sorts =
927 let (ast, ids_to_uris) as arg =
928 Acic2Ast.ast_of_acic ids_to_inner_sorts annterm
930 let astBox = Ast2pres.ast2astBox arg in
931 Box.map (fun ast -> Ast2pres.ast2mpres (ast, ids_to_uris)) astBox)