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 rec justification term2pres p =
190 let module Con = Content in
191 let module P = Mpresentation in
192 if ((p.Con.proof_conclude.Con.conclude_method = "Exact") or
193 ((p.Con.proof_context = []) &
194 (p.Con.proof_apply_context = []) &
195 (p.Con.proof_conclude.Con.conclude_method = "Apply"))) then
197 make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in
199 (B.b_kw "by")::B.b_space::
200 B.Text([],"(")::pres_args@[B.Text([],")")])
201 else proof2pres term2pres p
203 and proof2pres term2pres p =
204 let rec proof2pres p =
205 let module Con = Content in
210 | `Hypothesis _ -> true
212 ((List.filter is_decl p.Con.proof_context) != []) in
213 let omit_conclusion = (not indent) && (p.Con.proof_context != []) in
215 (match p.Con.proof_conclude.Con.conclude_conclusion with
217 | Some t -> Some (term2pres t)) in
220 conclude2pres p.Con.proof_conclude indent omit_conclusion in
222 acontext2pres p.Con.proof_apply_context presconclude indent in
223 context2pres p.Con.proof_context presacontext in
224 match p.Con.proof_name with
232 ([None,"type","toggle"],
233 [(make_concl ~attrs:[Some "helm", "xref", p.Con.proof_id]
234 "proof of" ac); body])
237 [B.Text ([],"(" ^ name ^ ")");
240 and context2pres c continuation =
241 (* we generate a subtable for each context element, for selection
243 The table generated by the head-element does not have an xref;
244 the whole context-proof is already selectable *)
250 (fun ce continuation ->
251 let xref = get_xref ce in
252 B.V([Some "helm", "xref", xref ],
253 [B.H([Some "helm", "xref", "ce_"^xref],[ce2pres ce]);
254 continuation])) tl continuation in
255 let hd_xref= get_xref hd in
257 [B.H([Some "helm", "xref", "ce_"^hd_xref],
262 let module Con = Content in
265 (match d.Con.dec_name with
267 let ty = term2pres d.Con.dec_type in
271 B.Object ([], P.Mi([],s));
275 prerr_endline "NO NAME!!"; assert false)
277 (match h.Con.dec_name with
279 let ty = term2pres h.Con.dec_type in
284 B.Object ([], P.Mi ([],s));
289 prerr_endline "NO NAME!!"; assert false)
293 (match d.Con.def_name with
295 let term = term2pres d.Con.def_term in
298 B.Object ([], P.Mi([],s));
302 prerr_endline "NO NAME!!"; assert false)
304 B.Text ([],"jointdef")
306 and acontext2pres ac continuation indent =
307 let module Con = Content in
309 (fun p continuation ->
312 B.indent (proof2pres p)
315 B.V([Some "helm","xref",p.Con.proof_id],
316 [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]);
317 continuation])) ac continuation
319 and conclude2pres conclude indent omit_conclusion =
320 let module Con = Content in
321 let module P = Mpresentation in
323 match conclude.Con.conclude_conclusion with
325 not omit_conclusion or
326 (* CSC: I ignore the omit_conclusion flag in this case. *)
327 (* CSC: Is this the correct behaviour? In the stylesheets *)
328 (* CSC: we simply generated nothing (i.e. the output type *)
329 (* CSC: of the function should become an option. *)
330 conclude.Con.conclude_method = "BU_Conversion" ->
331 let concl = (term2pres t) in
332 if conclude.Con.conclude_method = "BU_Conversion" then
333 make_concl "that is equivalent to" concl
334 else if conclude.Con.conclude_method = "FalseInd" then
335 (* false ind is in charge to add the conclusion *)
338 let conclude_body = conclude_aux conclude in
340 if conclude.Con.conclude_method = "TD_Conversion" then
341 make_concl "that is equivalent to" concl
342 else make_concl "we conclude" concl in
343 B.V ([], [conclude_body; ann_concl])
344 | _ -> conclude_aux conclude in
346 B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id],
349 B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body])
352 and conclude_aux conclude =
353 let module Con = Content in
354 let module P = Mpresentation in
355 if conclude.Con.conclude_method = "TD_Conversion" then
357 (match conclude.Con.conclude_conclusion with
358 None -> B.Text([],"NO EXPECTED!!!")
359 | Some c -> term2pres c) in
361 (match conclude.Con.conclude_args with
362 [Con.ArgProof p] -> p
363 | _ -> assert false) in
365 (match subproof.Con.proof_conclude.Con.conclude_conclusion with
366 None -> B.Text([],"NO SYNTH!!!")
367 | Some c -> (term2pres c)) in
370 [make_concl "we must prove" expected;
371 make_concl "or equivalently" synth;
372 proof2pres subproof])
373 else if conclude.Con.conclude_method = "BU_Conversion" then
375 else if conclude.Con.conclude_method = "Exact" then
377 (match conclude.Con.conclude_args with
378 [Con.Term t] -> term2pres t
379 | _ -> assert false) in
380 (match conclude.Con.conclude_conclusion with
382 B.b_h [] [B.b_kw "Consider"; B.b_space; arg]
383 | Some c -> let conclusion = term2pres c in
385 [arg; B.b_space; B.Text([],"proves")]
388 else if conclude.Con.conclude_method = "Intros+LetTac" then
389 (match conclude.Con.conclude_args with
390 [Con.ArgProof p] -> proof2pres p
394 (match conclude.Con.conclude_conclusion with
395 None -> B.Text([],"NO Conclusion!!!")
396 | Some c -> term2pres c) in
397 (match conclude.Con.conclude_args with
400 ([None,"align","baseline 1"; None,"equalrows","false";
401 None,"columnalign","left"],
402 [B.H([],[B.Object([],proof2pres p)]);
404 (make_concl "we proved 1" conclusion))])]);
407 else if (conclude.Con.conclude_method = "Case") then
409 else if (conclude.Con.conclude_method = "ByInduction") then
411 else if (conclude.Con.conclude_method = "Exists") then
413 else if (conclude.Con.conclude_method = "AndInd") then
415 else if (conclude.Con.conclude_method = "FalseInd") then
417 else if (conclude.Con.conclude_method = "Rewrite") then
419 (match (List.nth conclude.Con.conclude_args 6) with
420 Con.ArgProof p -> justification term2pres p
421 | _ -> assert false) in
423 (match List.nth conclude.Con.conclude_args 2 with
424 Con.Term t -> term2pres t
425 | _ -> assert false) in
427 (match List.nth conclude.Con.conclude_args 5 with
428 Con.Term t -> term2pres t
429 | _ -> assert false) in
434 B.b_space; (B.b_kw "with");
437 else if conclude.Con.conclude_method = "Apply" then
439 make_args_for_apply term2pres conclude.Con.conclude_args in
443 B.Text([],"(")::pres_args@[B.Text([],")")])
447 [B.Text([],"Apply method" ^ conclude.Con.conclude_method ^ " to");
451 args2pres conclude.Con.conclude_args)))])
453 and args2pres l = List.map arg2pres l
456 let module Con = Content in
459 B.Text ([],"aux " ^ n)
460 | Con.Premise prem ->
461 B.Text ([],"premise")
472 let module Con = Content in
473 let proof_conclusion =
474 (match conclude.Con.conclude_conclusion with
475 None -> B.Text([],"No conclusion???")
476 | Some t -> term2pres t) in
477 let arg,args_for_cases =
478 (match conclude.Con.conclude_args with
479 Con.Aux(_)::Con.Aux(_)::Con.Term(_)::arg::tl ->
481 | _ -> assert false) in
486 B.Text ([],"an aux???")
487 | Con.Premise prem ->
488 (match prem.Con.premise_binder with
489 None -> B.Text ([],"the previous result")
490 | Some n -> B.Object ([], P.Mi([],n)))
491 | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name))
495 B.Text ([],"a proof???")
497 B.Text ([],"a method???")) in
498 (make_concl "we proceede by cases on" case_arg) in
500 (make_concl "to prove" proof_conclusion) in
503 case_on::to_prove::(make_cases args_for_cases))
505 and byinduction conclude =
506 let module Con = Content in
507 let proof_conclusion =
508 (match conclude.Con.conclude_conclusion with
509 None -> B.Text([],"No conclusion???")
510 | Some t -> term2pres t) in
511 let inductive_arg,args_for_cases =
512 (match conclude.Con.conclude_args with
514 let l1,l2 = split (int_of_string n) tl in
515 let last_pos = (List.length l2)-1 in
516 List.nth l2 last_pos,l1
517 | _ -> assert false) in
520 (match inductive_arg with
522 B.Text ([],"an aux???")
523 | Con.Premise prem ->
524 (match prem.Con.premise_binder with
525 None -> B.Text ([],"the previous result")
526 | Some n -> B.Object ([], P.Mi([],n)))
527 | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name))
531 B.Text ([],"a proof???")
533 B.Text ([],"a method???")) in
534 (make_concl "we proceede by induction on" arg) in
536 (make_concl "to prove" proof_conclusion) in
539 induction_on::to_prove::
540 (make_cases args_for_cases))
542 and make_cases l = List.map make_case l
545 let module Con = Content in
549 (match p.Con.proof_name with
550 None -> B.Text([],"no name for case!!")
551 | Some n -> B.Object ([], P.Mi([],n))) in
555 `Hypothesis h -> h.Con.dec_inductive
556 | _ -> false) p.Con.proof_context in
565 (match h.Con.dec_name with
569 B.Object ([], P.Mi ([],name));
571 (term2pres h.Con.dec_type)]
572 | _ -> [B.Text ([],"???")]) in
576 (B.Text([],"Case")::B.b_space::name::pattern_aux)@
580 (match p.Con.proof_conclude.Con.conclude_conclusion with
581 None -> B.Text([],"No conclusion!!!")
582 | Some t -> term2pres t) in
583 let asubconcl = B.indent (make_concl "the thesis becomes" subconcl) in
584 let induction_hypothesis =
589 B.indent (B.Text([],"by induction hypothesis we know:")) in
594 (match h.Con.dec_name with
599 B.Object ([], P.Mi ([],name));
602 term2pres h.Con.dec_type]))
603 | _ -> assert false in
604 let hyps = List.map make_hyp indhyps in
607 acontext2pres_old p.Con.proof_apply_context true in *)
608 let body = conclude2pres p.Con.proof_conclude true false in
611 match p.Con.proof_apply_context with
612 [] -> p.Con.proof_conclude.Con.conclude_id
613 | {Con.proof_id = id}::_ -> id
615 B.Action([None,"type","toggle"],
618 ([None,"color","red" ;
619 Some "helm", "xref", acontext_id],"Proof")) ;
620 acontext2pres p.Con.proof_apply_context body true]) in
621 B.V ([], pattern::asubconcl::induction_hypothesis@[presacontext])
624 and falseind conclude =
625 let module P = Mpresentation in
626 let module Con = Content in
627 let proof_conclusion =
628 (match conclude.Con.conclude_conclusion with
629 None -> B.Text([],"No conclusion???")
630 | Some t -> term2pres t) in
632 (match conclude.Con.conclude_args with
633 [Con.Aux(n);_;case_arg] -> case_arg
636 List.map (ContentPp.parg 0) conclude.Con.conclude_args;
640 Con.Aux n -> assert false
641 | Con.Premise prem ->
642 (match prem.Con.premise_binder with
643 None -> [B.Text([],"Contradiction, hence")]
645 [B.Object ([],P.Mi([],n)); B.skip;B.Text([],"is contradictory, hence")])
647 [B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip; B.Text([],"is contradictory, hence")]
648 | _ -> assert false) in
649 (* let body = proof2pres {proof with Con.proof_context = tl} in *)
650 make_row arg proof_conclusion
652 and andind conclude =
653 let module P = Mpresentation in
654 let module Con = Content in
655 let proof_conclusion =
656 (match conclude.Con.conclude_conclusion with
657 None -> B.Text([],"No conclusion???")
658 | Some t -> term2pres t) in
660 (match conclude.Con.conclude_args with
661 [Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg
664 List.map (ContentPp.parg 0) conclude.Con.conclude_args;
668 Con.Aux n -> assert false
669 | Con.Premise prem ->
670 (match prem.Con.premise_binder with
672 | Some n -> [(B.b_kw "by"); B.b_space; B.Object([], P.Mi([],n))])
674 [(B.b_kw "by");B.skip; B.Object([], P.Mi([],lemma.Con.lemma_name))]
675 | _ -> assert false) in
676 match proof.Con.proof_context with
677 `Hypothesis hyp1::`Hypothesis hyp2::tl ->
679 (match hyp.Con.dec_name with
685 B.Object ([], P.Mi([],get_name hyp1));
688 term2pres hyp1.Con.dec_type]) in
692 B.Object ([], P.Mi([],get_name hyp2));
695 term2pres hyp2.Con.dec_type]) in
696 (* let body = proof2pres {proof with Con.proof_context = tl} in *)
697 let body = conclude2pres proof.Con.proof_conclude false true in
699 acontext2pres proof.Con.proof_apply_context body false in
702 [B.H ([],arg@[B.skip; B.Text([],"we have")]);
709 and exists conclude =
710 let module P = Mpresentation in
711 let module Con = Content in
712 let proof_conclusion =
713 (match conclude.Con.conclude_conclusion with
714 None -> B.Text([],"No conclusion???")
715 | Some t -> term2pres t) in
717 (match conclude.Con.conclude_args with
718 [Con.Aux(n);_;Con.ArgProof proof;_] -> proof
721 List.map (ContentPp.parg 0) conclude.Con.conclude_args;
723 match proof.Con.proof_context with
724 `Declaration decl::`Hypothesis hyp::tl
725 | `Hypothesis decl::`Hypothesis hyp::tl ->
727 (match decl.Con.dec_name with
734 B.Object ([], P.Mi([],get_name decl));
735 B.Text([],":"); term2pres decl.Con.dec_type]) in
738 [(B.b_kw "such that");
741 B.Object ([], P.Mi([],get_name hyp));
744 term2pres hyp.Con.dec_type]) in
745 (* let body = proof2pres {proof with Con.proof_context = tl} in *)
746 let body = conclude2pres proof.Con.proof_conclude false true in
748 acontext2pres proof.Con.proof_apply_context body false in
754 | _ -> assert false in
763 let conjecture2pres term2pres (id, n, context, ty) =
764 (B.b_h [Some "helm", "xref", id]
769 [ B.b_object (p_mi [] "_") ;
770 B.b_object (p_mo [] ":?") ;
771 B.b_object (p_mi [] "_")]
772 | Some (`Declaration d)
773 | Some (`Hypothesis d) ->
774 let { Content.dec_name =
775 dec_name ; Content.dec_type = ty } = d
785 | Some (`Definition d) ->
787 { Content.def_name = def_name ;
788 Content.def_term = bo } = d
791 [ B.b_object (p_mi []
798 let proof_name = p.Content.proof_name in
800 [ B.b_object (p_mi []
801 (match proof_name with
805 proof2pres term2pres p])
806 (List.rev context)) @
808 B.b_object (p_mi [] (string_of_int n)) ;
812 let metasenv2pres term2pres = function
815 (* Conjectures are in their own table to make *)
816 (* diffing the DOM trees easier. *)
820 (let _ = incr counter; in (string_of_int !counter)))) ::
821 (List.map (conjecture2pres term2pres) metasenv'))]
823 let get_name = function
827 let pp_params = function
831 String.concat " ; " (List.map UriManager.string_of_uri params) ^
834 let content2pres term2pres (id,params,metasenv,obj) =
836 | `Def (Content.Const, thesis, `Proof p) ->
837 let name = get_name p.Content.proof_name in
839 [None,"helm:xref","id"]
840 ([ B.b_text [] ("Proof " ^ name ^ pp_params params);
841 B.b_text [] "Thesis:";
842 B.indent (term2pres thesis) ] @
843 metasenv2pres term2pres metasenv @
844 [proof2pres term2pres p])
845 | `Def (_, ty, `Definition body) ->
846 let name = get_name body.Content.def_name in
848 [None,"helm:xref","id"]
849 ([B.b_text [] ("Definition " ^ name ^ pp_params params);
851 B.indent (term2pres ty)] @
852 metasenv2pres term2pres metasenv @
853 [term2pres body.Content.def_term])
854 | `Decl (_, `Declaration decl)
855 | `Decl (_, `Hypothesis decl) ->
856 let name = get_name decl.Content.dec_name in
858 [None,"helm:xref","id"]
859 ([B.b_text [] ("Axiom " ^ name ^ pp_params params);
861 B.indent (term2pres decl.Content.dec_type)] @
862 metasenv2pres term2pres metasenv)
867 let content2pres ~ids_to_inner_sorts =
870 (Cexpr2pres.cexpr2pres_charcount
871 (Content_expressions.acic2cexpr ids_to_inner_sorts p)))
875 let content2pres ~ids_to_inner_sorts =
878 let (ast, ids_to_uris) as arg =
879 Acic2Ast.ast_of_acic ids_to_inner_sorts annterm
881 let astBox = Ast2pres.ast2astBox arg in
882 Box.map (fun ast -> Ast2pres.ast2mpres (ast, ids_to_uris)) astBox)