]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_transformations/content2pres.ml
Reindentation
[helm.git] / helm / ocaml / cic_transformations / content2pres.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (***************************************************************************)
27 (*                                                                         *)
28 (*                            PROJECT HELM                                 *)
29 (*                                                                         *)
30 (*                Andrea Asperti <asperti@cs.unibo.it>                     *)
31 (*                              17/06/2003                                 *)
32 (*                                                                         *)
33 (***************************************************************************)
34
35 let rec split n l =
36   if n = 0 then [],l
37   else let l1,l2 = 
38     split (n-1) (List.tl l) in
39     (List.hd l)::l1,l2
40 ;;
41   
42
43 let is_big_general countterm p =
44   let maxsize = Cexpr2pres.maxsize in
45   let module Con = Content in
46   let rec countp current_size p =
47     if current_size > maxsize then current_size
48     else 
49       let c1 = (countcontext current_size p.Con.proof_context) in
50       if c1 > maxsize then c1
51     else 
52       let c2 = (countapplycontext c1 p.Con.proof_apply_context) in
53       if c2 > maxsize then c2
54     else 
55       countconclude c2 p.Con.proof_conclude
56
57   and 
58     countcontext current_size c =
59       List.fold_left countcontextitem current_size c
60   and
61     countcontextitem current_size e =
62       if current_size > maxsize then maxsize
63       else 
64         (match e with
65           `Declaration d -> 
66             (match d.Con.dec_name with
67                Some s -> current_size + 4 + (String.length s)
68              | None -> prerr_endline "NO NAME!!"; assert false)
69         | `Hypothesis h ->
70             (match h.Con.dec_name with
71                 Some s -> current_size + 4 + (String.length s)
72               | None -> prerr_endline "NO NAME!!"; assert false) 
73         | `Proof p -> countp current_size p
74         | `Definition d -> 
75             (match d.Con.def_name with
76                 Some s -> 
77                   let c1 = (current_size + 4 + (String.length s)) in
78                   (countterm c1 d.Con.def_term)
79               | None -> 
80                   prerr_endline "NO NAME!!"; assert false) 
81         | `Joint ho -> maxsize + 1) (* we assume is big *)
82   and 
83     countapplycontext current_size ac =
84       List.fold_left countp current_size ac
85   and 
86     countconclude current_size co =
87       if current_size > maxsize then current_size
88       else
89         let c1 = countargs current_size co.Con.conclude_args in
90         if c1 > maxsize then c1 
91       else 
92         (match co.Con.conclude_conclusion with
93            Some concl ->  countterm c1 concl
94         | None -> c1)
95   and 
96     countargs current_size args =
97       List.fold_left countarg current_size args
98   and
99     countarg current_size arg =
100       if current_size > maxsize then current_size
101       else 
102         (match arg with 
103            Con.Aux _ -> current_size
104          | Con.Premise prem -> 
105              (match prem.Con.premise_binder with
106                 Some s -> current_size + (String.length s)
107               | None -> current_size + 7) 
108          | Con.Lemma lemma -> 
109              current_size + (String.length lemma.Con.lemma_name)
110          | Con.Term t -> countterm current_size t
111          | Con.ArgProof p -> countp current_size p
112          | Con.ArgMethod s -> (maxsize + 1)) in
113   let size = (countp 0 p) in
114   (size > maxsize)
115 ;;
116
117 let is_big = is_big_general (Cexpr2pres.countterm)
118 ;;
119
120 let get_xref =
121     let module Con = Content in
122       function
123         `Declaration d  
124       | `Hypothesis d -> d.Con.dec_id
125       | `Proof p -> p.Con.proof_id
126       | `Definition d -> d.Con.def_id
127       | `Joint jo -> jo.Con.joint_id
128 ;;
129
130 let make_row ?(attrs=[]) items concl =
131   let module P = Mpresentation in
132     (match concl with 
133        P.Mtable _ -> (* big! *)
134          P.Mtable (attrs@[None,"align","baseline 1"; None,"equalrows","false";
135           None,"columnalign","left"],
136            [P.Mtr([],[P.Mtd ([],P.Mrow([],items))]);
137             P.Mtr ([],[P.Mtd ([],P.indented concl)])])
138      | _ ->  (* small *)
139        P.Mrow(attrs,items@[P.Mspace([None,"width","0.1cm"]);concl]))
140 ;;
141
142 let make_concl ?(attrs=[]) verb concl =
143   let module P = Mpresentation in
144     (match concl with 
145        P.Mtable _ -> (* big! *)
146          P.Mtable (attrs@[None,"align","baseline 1"; None,"equalrows","false";
147           None,"columnalign","left"],
148            [P.Mtr([],[P.Mtd ([],P.Mtext([None,"mathcolor","Red"],verb))]);
149             P.Mtr ([],[P.Mtd ([],P.indented concl)])])
150      | _ ->  (* small *)
151        P.Mrow(attrs,
152         [P.Mtext([None,"mathcolor","Red"],verb); 
153          P.Mspace([None,"width","0.1cm"]);
154          concl]))
155 ;;
156
157 let make_args_for_apply term2pres args =
158  let module Con = Content in
159  let module P = Mpresentation in
160  let make_arg_for_apply is_first arg row = 
161   let res =
162    match arg with 
163       Con.Aux n -> assert false
164     | Con.Premise prem -> 
165         let name = 
166           (match prem.Con.premise_binder with
167              None -> "previous"
168            | Some s -> s) in
169         P.Mi([],name)::row
170     | Con.Lemma lemma -> 
171          P.Mi([],lemma.Con.lemma_name)::row 
172     | Con.Term t -> 
173         if is_first then
174           (term2pres t)::row
175         else P.Mi([],"_")::row
176     | Con.ArgProof _ 
177     | Con.ArgMethod _ -> 
178        P.Mi([],"_")::row
179   in
180    if is_first then res else P.smallskip::res
181  in
182   match args with 
183     hd::tl -> 
184       make_arg_for_apply true hd 
185         (List.fold_right (make_arg_for_apply false) tl [])
186   | _ -> assert false
187 ;;
188
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
196     let pres_args = 
197       make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in
198     P.Mrow([],
199       P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"])::
200       P.Mo([],"(")::pres_args@[P.Mo([],")")]) 
201   else proof2pres term2pres p 
202      
203 and proof2pres term2pres p =
204   let rec proof2pres p =
205     let module Con = Content in
206     let module P = Mpresentation in
207       let indent = 
208         let is_decl e = 
209           (match e with 
210              `Declaration _
211            | `Hypothesis _ -> true
212            | _ -> false) in
213         ((List.filter is_decl p.Con.proof_context) != []) in 
214       let omit_conclusion = (not indent) && (p.Con.proof_context != []) in
215       let concl = 
216         (match p.Con.proof_conclude.Con.conclude_conclusion with
217            None -> None
218          | Some t -> Some (term2pres t)) in
219       let body =
220           let presconclude = 
221             conclude2pres p.Con.proof_conclude indent omit_conclusion in
222           let presacontext = 
223             acontext2pres p.Con.proof_apply_context presconclude indent in
224           context2pres p.Con.proof_context presacontext in
225       match p.Con.proof_name with
226         None -> body
227       | Some name ->
228           let action = 
229            match concl with
230               None -> body
231 (*
232                P.Maction
233                  ([None,"actiontype","toggle" ; None,"selection","1"],
234                   [P.Mtext [] "proof" ; body])
235 *)
236             | Some ac ->
237                P.Maction
238                  ([None,"actiontype","toggle" ; None,"selection","1"],
239                   [(make_concl ~attrs:[Some "helm", "xref", p.Con.proof_id]
240                      "proof of" ac); body])
241           in
242           P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
243               None,"columnalign","left"],
244             [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]);
245              P.Mtr ([],[P.Mtd ([], P.indented action)])])
246 (*
247           P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
248               None,"columnalign","left";Some "helm", "xref", p.Con.proof_id],
249             [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]);
250              P.Mtr ([],[P.Mtd ([], P.indented action)])]) *)
251
252   and context2pres c continuation =
253     (* we generate a subtable for each context element, for selection
254        purposes 
255        The table generated by the head-element does not have an xref;
256        the whole context-proof is already selectable *)
257     let module P = Mpresentation in
258     match c with
259       [] -> continuation
260     | hd::tl -> 
261         let continuation' =
262           List.fold_right
263             (fun ce continuation ->
264               let xref = get_xref ce in
265               P.Mtable([None,"align","baseline 1"; None,"equalrows","false";
266                None,"columnalign","left"; Some "helm", "xref", xref ],
267                 [P.Mtr([Some "helm", "xref", "ce_"^xref],[P.Mtd ([],ce2pres ce)]);
268                  P.Mtr([],[P.Mtd ([], continuation)])])) tl continuation in
269          let hd_xref= get_xref hd in
270          P.Mtable([None,"align","baseline 1"; None,"equalrows","false";
271            None,"columnalign","left"],
272              [P.Mtr([Some "helm", "xref", "ce_"^hd_xref],
273                [P.Mtd ([],ce2pres hd)]);
274              P.Mtr([],[P.Mtd ([], continuation')])])
275          
276   and ce2pres =
277     let module P = Mpresentation in
278     let module Con = Content in
279       function
280         `Declaration d -> 
281           (match d.Con.dec_name with
282               Some s ->
283                 let ty = term2pres d.Con.dec_type in
284                 P.Mrow ([],
285                   [P.Mtext([None,"mathcolor","Red"],"Assume");
286                    P.Mspace([None,"width","0.1cm"]);
287                    P.Mi([],s);
288                    P.Mtext([],":");
289                    ty])
290             | None -> 
291                 prerr_endline "NO NAME!!"; assert false)
292       | `Hypothesis h ->
293           (match h.Con.dec_name with
294               Some s ->
295                 let ty = term2pres h.Con.dec_type in
296                 P.Mrow ([],
297                   [P.Mtext([None,"mathcolor","Red"],"Suppose");
298                    P.Mspace([None,"width","0.1cm"]);
299                    P.Mo([],"(");
300                    P.Mi ([],s);
301                    P.Mo([],")");
302                    P.Mspace([None,"width","0.1cm"]);
303                    ty])
304             | None -> 
305                 prerr_endline "NO NAME!!"; assert false) 
306       | `Proof p -> 
307            proof2pres p 
308       | `Definition d -> 
309            (match d.Con.def_name with
310               Some s ->
311                 let term = term2pres d.Con.def_term in
312                 P.Mrow ([],
313                   [P.Mtext([],"Let ");
314                    P.Mi([],s);
315                    P.Mtext([]," = ");
316                    term])
317             | None -> 
318                 prerr_endline "NO NAME!!"; assert false) 
319       | `Joint ho -> 
320             P.Mtext ([],"jointdef")
321
322   and acontext2pres ac continuation indent =
323     let module Con = Content in
324     let module P = Mpresentation in
325     List.fold_right
326       (fun p continuation ->
327          let hd = 
328            if indent then
329              P.indented (proof2pres p)
330            else 
331              proof2pres p in
332          P.Mtable([None,"align","baseline 1"; None,"equalrows","false";
333           None,"columnalign","left"; Some "helm","xref",p.Con.proof_id],
334            [P.Mtr([Some "helm","xref","ace_"^p.Con.proof_id],[P.Mtd ([],hd)]);
335             P.Mtr([],[P.Mtd ([], continuation)])])) ac continuation 
336
337   and conclude2pres conclude indent omit_conclusion =
338     let module Con = Content in
339     let module P = Mpresentation in
340     let tconclude_body = 
341       match conclude.Con.conclude_conclusion with
342         Some t when
343          not omit_conclusion or
344          (* CSC: I ignore the omit_conclusion flag in this case.   *)
345          (* CSC: Is this the correct behaviour? In the stylesheets *)
346          (* CSC: we simply generated nothing (i.e. the output type *)
347          (* CSC: of the function should become an option.          *)
348          conclude.Con.conclude_method = "BU_Conversion" ->
349           let concl = (term2pres t) in 
350           if conclude.Con.conclude_method = "BU_Conversion" then
351             make_concl "that is equivalent to" concl
352           else if conclude.Con.conclude_method = "FalseInd" then
353            (* false ind is in charge to add the conclusion *)
354            falseind conclude
355           else  
356             let conclude_body = conclude_aux conclude in
357             let ann_concl = 
358               if conclude.Con.conclude_method = "TD_Conversion" then
359                  make_concl "that is equivalent to" concl 
360               else make_concl "we conclude" concl in
361             P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
362               None,"columnalign","left"],
363                 [P.Mtr ([],[P.Mtd ([],conclude_body)]);
364                  P.Mtr ([],[P.Mtd ([],ann_concl)])])
365       | _ -> conclude_aux conclude in
366     if indent then 
367       P.indented (P.Mrow ([Some "helm", "xref", conclude.Con.conclude_id],
368                     [tconclude_body]))
369     else 
370       P.Mrow ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body])
371
372
373   and conclude_aux conclude =
374     let module Con = Content in
375     let module P = Mpresentation in
376     if conclude.Con.conclude_method = "TD_Conversion" then
377       let expected = 
378         (match conclude.Con.conclude_conclusion with 
379            None -> P.Mtext([],"NO EXPECTED!!!")
380          | Some c -> term2pres c) in
381       let subproof = 
382         (match conclude.Con.conclude_args with
383           [Con.ArgProof p] -> p
384          | _ -> assert false) in
385       let synth = 
386         (match subproof.Con.proof_conclude.Con.conclude_conclusion with
387            None -> P.Mtext([],"NO SYNTH!!!")
388          | Some c -> (term2pres c)) in
389       P.Mtable 
390         ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"],
391         [P.Mtr([],[P.Mtd([],make_concl "we must prove" expected)]);
392          P.Mtr([],[P.Mtd([],make_concl "or equivalently" synth)]);
393          P.Mtr([],[P.Mtd([],proof2pres subproof)])])
394     else if conclude.Con.conclude_method = "BU_Conversion" then
395       assert false
396     else if conclude.Con.conclude_method = "Exact" then
397       let arg = 
398         (match conclude.Con.conclude_args with 
399            [Con.Term t] -> term2pres t
400          | _ -> assert false) in
401       (match conclude.Con.conclude_conclusion with 
402          None ->
403           P.Mrow []
404            [P.Mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg]
405        | Some c -> let conclusion = term2pres c in
406           make_row 
407             [arg; P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")]
408             conclusion
409        )
410     else if conclude.Con.conclude_method = "Intros+LetTac" then
411       (match conclude.Con.conclude_args with
412          [Con.ArgProof p] -> proof2pres p
413        | _ -> assert false)
414 (* OLD CODE 
415       let conclusion = 
416       (match conclude.Con.conclude_conclusion with 
417          None -> P.Mtext([],"NO Conclusion!!!")
418        | Some c -> term2pres c) in
419       (match conclude.Con.conclude_args with
420          [Con.ArgProof p] -> 
421            P.Mtable 
422             ([None,"align","baseline 1"; None,"equalrows","false";
423               None,"columnalign","left"],
424               [P.Mtr([],[P.Mtd([],proof2pres p)]);
425                P.Mtr([],[P.Mtd([],
426                 (make_concl "we proved 1" conclusion))])]);
427        | _ -> assert false)
428 *)
429     else if (conclude.Con.conclude_method = "ByInduction") then
430       byinduction conclude
431     else if (conclude.Con.conclude_method = "Exists") then
432       exists conclude
433     else if (conclude.Con.conclude_method = "AndInd") then
434       andind conclude
435     else if (conclude.Con.conclude_method = "FalseInd") then
436       falseind conclude
437     else if (conclude.Con.conclude_method = "Rewrite") then
438       let justif = 
439         (match (List.nth conclude.Con.conclude_args 6) with
440            Con.ArgProof p -> justification term2pres p
441          | _ -> assert false) in
442       let term1 = 
443         (match List.nth conclude.Con.conclude_args 2 with
444            Con.Term t -> term2pres t
445          | _ -> assert false) in 
446       let term2 = 
447         (match List.nth conclude.Con.conclude_args 5 with
448            Con.Term t -> term2pres t
449          | _ -> assert false) in
450       P.Mtable ([None,"align","baseline 1";None,"equalrows","false";
451         None,"columnalign","left"], 
452          [P.Mtr ([],[P.Mtd ([],P.Mrow([],[
453           P.Mtext([None,"mathcolor","Red"],"rewrite");
454           P.Mspace([None,"width","0.1cm"]);term1;
455           P.Mspace([None,"width","0.1cm"]);
456           P.Mtext([None,"mathcolor","Red"],"with");
457           P.Mspace([None,"width","0.1cm"]);term2]))]);
458           P.Mtr ([],[P.Mtd ([],P.indented justif)])]);
459     else if conclude.Con.conclude_method = "Apply" then
460       let pres_args = 
461         make_args_for_apply term2pres conclude.Con.conclude_args in
462       P.Mrow([],
463         P.Mtext([None,"mathcolor","Red"],"by")::
464         P.Mspace([None,"width","0.1cm"])::
465         P.Mo([],"(")::pres_args@[P.Mo([],")")])
466     else 
467       P.Mtable 
468         ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"],
469          [P.Mtr ([],[P.Mtd ([],P.Mtext([],"Apply method" ^ conclude.Con.conclude_method ^ " to"))]);
470           P.Mtr ([],
471            [P.Mtd ([], 
472              (P.indented 
473                (P.Mtable 
474                  ([None,"align","baseline 1"; None,"equalrows","false";
475                    None,"columnalign","left"],
476                   args2pres conclude.Con.conclude_args))))])]) 
477
478   and args2pres l =
479     let module P = Mpresentation in
480     List.map 
481      (function a -> P.Mtr ([], [P.Mtd ([], arg2pres a)])) l
482
483   and arg2pres =
484     let module P = Mpresentation in
485     let module Con = Content in
486     function
487         Con.Aux n -> 
488           P.Mtext ([],"aux " ^ n)
489       | Con.Premise prem -> 
490           P.Mtext ([],"premise")
491       | Con.Lemma lemma ->
492           P.Mtext ([],"lemma")
493       | Con.Term t -> 
494           term2pres t
495       | Con.ArgProof p ->
496         proof2pres p 
497       | Con.ArgMethod s -> 
498          P.Mtext ([],"method") 
499  
500    and byinduction conclude =
501      let module P = Mpresentation in
502      let module Con = Content in
503      let proof_conclusion = 
504        (match conclude.Con.conclude_conclusion with
505           None -> P.Mtext([],"No conclusion???")
506         | Some t -> term2pres t) in
507      let inductive_arg,args_for_cases = 
508        (match conclude.Con.conclude_args with
509            Con.Aux(n)::_::tl ->
510              let l1,l2 = split (int_of_string n) tl in
511              let last_pos = (List.length l2)-1 in
512              List.nth l2 last_pos,l1
513          | _ -> assert false) in
514      let induction_on =
515        let arg = 
516          (match inductive_arg with
517             Con.Aux n -> 
518               P.Mtext ([],"an aux???")
519            | Con.Premise prem ->
520               (match prem.Con.premise_binder with
521                  None -> P.Mtext ([],"the previous result")
522                | Some n -> P.Mi([],n))
523            | Con.Lemma lemma -> P.Mi([],lemma.Con.lemma_name)
524            | Con.Term t -> 
525                term2pres t
526            | Con.ArgProof p ->
527                P.Mtext ([],"a proof???")
528            | Con.ArgMethod s -> 
529                P.Mtext ([],"a method???")) in
530         (make_concl "we proceede by induction on" arg) in
531      let to_prove =
532         (make_concl "to prove" proof_conclusion) in
533      P.Mtable 
534        ([None,"align","baseline 1"; None,"equalrows","false"; 
535          None,"columnalign","left"],
536           P.Mtr ([],[P.Mtd ([],induction_on)])::
537           P.Mtr ([],[P.Mtd ([],to_prove)])::
538           (make_cases args_for_cases))
539
540     and make_cases args_for_cases =
541     let module P = Mpresentation in
542     List.map 
543       (fun p -> P.Mtr ([],[P.Mtd ([],make_case p)])) args_for_cases
544
545     and make_case =  
546       let module P = Mpresentation in
547       let module Con = Content in
548       function 
549         Con.ArgProof p ->
550           let name =
551             (match p.Con.proof_name with
552                None -> P.Mtext([],"no name for case!!")
553              | Some n -> P.Mi([],n)) in
554           let indhyps,args =
555              List.partition 
556                (function
557                    `Hypothesis h -> h.Con.dec_inductive
558                  | _ -> false) p.Con.proof_context in
559           let pattern_aux =
560              List.fold_right
561                (fun e p -> 
562                   let dec  = 
563                     (match e with 
564                        `Declaration h 
565                      | `Hypothesis h -> 
566                          let name = 
567                            (match h.Con.dec_name with
568                               None -> "NO NAME???"
569                            | Some n ->n) in
570                          [P.Mspace([None,"width","0.1cm"]);
571                           P.Mi ([],name);
572                           P.Mtext([],":");
573                           (term2pres h.Con.dec_type)]
574                      | _ -> [P.Mtext ([],"???")]) in
575                   dec@p) args [] in
576           let pattern = 
577             P.Mtr ([],[P.Mtd ([],P.Mrow([],
578                P.Mtext([],"Case")::P.Mspace([None,"width","0.1cm"])::name::pattern_aux@
579                 [P.Mspace([None,"width","0.1cm"]);
580                  P.Mtext([],"->")]))]) in
581           let subconcl = 
582             (match p.Con.proof_conclude.Con.conclude_conclusion with
583                None -> P.Mtext([],"No conclusion!!!") 
584              | Some t -> term2pres t) in
585           let asubconcl =
586              P.Mtr([],[P.Mtd([],
587               P.indented (make_concl "the thesis becomes" subconcl))]) in
588           let induction_hypothesis = 
589             (match indhyps with
590               [] -> []
591             | _ -> 
592                let text =
593                  P.Mtr([],[P.Mtd([], P.indented 
594                  (P.Mtext([],"by induction hypothesis we know:")))]) in
595                let make_hyp =
596                  function 
597                    `Hypothesis h ->
598                      let name = 
599                        (match h.Con.dec_name with
600                           None -> "no name"
601                         | Some s -> s) in
602                      P.indented (P.Mrow ([],
603                        [P.Mo([],"(");
604                         P.Mi ([],name);
605                         P.Mo([],")");
606                         P.Mspace([None,"width","0.1cm"]);
607                         term2pres h.Con.dec_type]))
608                    | _ -> assert false in
609                let hyps = 
610                  List.map 
611                    (function ce -> P.Mtr ([], [P.Mtd ([], make_hyp ce)])) 
612                     indhyps in
613                text::hyps) in          
614           (* let acontext = 
615                acontext2pres_old p.Con.proof_apply_context true in *)
616           let body = conclude2pres p.Con.proof_conclude true false in
617           let presacontext = 
618            let acontext_id =
619             match p.Con.proof_apply_context with
620                [] -> p.Con.proof_conclude.Con.conclude_id
621              | {Con.proof_id = id}::_ -> id
622            in
623             P.Maction([None,"actiontype","toggle" ; None,"selection","1"],
624               [P.indented
625                (P.Mtext
626                  ([None,"mathcolor","Red" ;
627                    Some "helm", "xref", acontext_id],"Proof")) ;
628                acontext2pres p.Con.proof_apply_context body true]) in
629           P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
630              None,"columnalign","left"],
631              pattern::asubconcl::induction_hypothesis@
632               [P.Mtr([],[P.Mtd([],presacontext)])])
633        | _ -> assert false 
634
635      and falseind conclude =
636        let module P = Mpresentation in
637        let module Con = Content in
638        let proof_conclusion = 
639          (match conclude.Con.conclude_conclusion with
640             None -> P.Mtext([],"No conclusion???")
641           | Some t -> term2pres t) in
642        let case_arg = 
643          (match conclude.Con.conclude_args with
644              [Con.Aux(n);_;case_arg] -> case_arg
645            | _ -> assert false;
646              (* 
647              List.map (ContentPp.parg 0) conclude.Con.conclude_args;
648              assert false *)) in
649        let arg = 
650          (match case_arg with
651              Con.Aux n -> assert false
652            | Con.Premise prem ->
653               (match prem.Con.premise_binder with
654                  None -> [P.Mtext([],"Contradiction, hence")]
655                | Some n -> 
656                   [P.Mi([],n);P.smallskip;P.Mtext([],"is contradictory, hence")])
657            | Con.Lemma lemma -> 
658                [P.Mi([],lemma.Con.lemma_name);P.smallskip;P.Mtext([],"is contradictory, hence")]
659            | _ -> assert false) in
660             (* let body = proof2pres {proof with Con.proof_context = tl} in *)
661        make_row arg proof_conclusion
662
663      and andind conclude =
664        let module P = Mpresentation in
665        let module Con = Content in
666        let proof_conclusion = 
667          (match conclude.Con.conclude_conclusion with
668             None -> P.Mtext([],"No conclusion???")
669           | Some t -> term2pres t) in
670        let proof,case_arg = 
671          (match conclude.Con.conclude_args with
672              [Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg
673            | _ -> assert false;
674              (* 
675              List.map (ContentPp.parg 0) conclude.Con.conclude_args;
676              assert false *)) in
677        let arg = 
678          (match case_arg with
679              Con.Aux n -> assert false
680            | Con.Premise prem ->
681               (match prem.Con.premise_binder with
682                  None -> []
683                | Some n -> [P.Mtext([],"by");P.smallskip;P.Mi([],n)])
684            | Con.Lemma lemma -> 
685                [P.Mtext([],"by");P.smallskip;P.Mi([],lemma.Con.lemma_name)]
686            | _ -> assert false) in
687        match proof.Con.proof_context with
688          `Hypothesis hyp1::`Hypothesis hyp2::tl ->
689             let get_name hyp =
690               (match hyp.Con.dec_name with
691                 None -> "_"
692               | Some s -> s) in
693             let preshyp1 = 
694               P.Mrow ([],
695                [P.Mtext([],"(");
696                 P.Mi([],get_name hyp1);
697                 P.Mtext([],")");
698                 P.smallskip;
699                 term2pres hyp1.Con.dec_type]) in
700             let preshyp2 = 
701               P.Mrow ([],
702                [P.Mtext([],"(");
703                 P.Mi([],get_name hyp2);
704                 P.Mtext([],")");
705                 P.smallskip;
706                 term2pres hyp2.Con.dec_type]) in
707             (* let body = proof2pres {proof with Con.proof_context = tl} in *)
708             let body = conclude2pres proof.Con.proof_conclude false true in
709             let presacontext = 
710               acontext2pres proof.Con.proof_apply_context body false in
711             P.Mtable 
712               ([None,"align","baseline 1"; None,"equalrows","false"; 
713                 None,"columnalign","left"],
714                [P.Mtr ([],[P.Mtd ([],
715                  P.Mrow([],arg@[P.smallskip;P.Mtext([],"we have")]))]);
716                 P.Mtr ([],[P.Mtd ([],preshyp1)]);
717                 P.Mtr ([],[P.Mtd ([],P.Mtext([],"and"))]);
718                 P.Mtr ([],[P.Mtd ([],preshyp2)]);
719                 P.Mtr ([],[P.Mtd ([],presacontext)])]);
720          | _ -> assert false
721
722      and exists conclude =
723        let module P = Mpresentation in
724        let module Con = Content in
725        let proof_conclusion = 
726          (match conclude.Con.conclude_conclusion with
727             None -> P.Mtext([],"No conclusion???")
728           | Some t -> term2pres t) in
729        let proof = 
730          (match conclude.Con.conclude_args with
731              [Con.Aux(n);_;Con.ArgProof proof;_] -> proof
732            | _ -> assert false;
733              (* 
734              List.map (ContentPp.parg 0) conclude.Con.conclude_args;
735              assert false *)) in
736        match proof.Con.proof_context with
737            `Declaration decl::`Hypothesis hyp::tl
738          | `Hypothesis decl::`Hypothesis hyp::tl ->
739            let get_name decl =
740              (match decl.Con.dec_name with
741                 None -> "_"
742               | Some s -> s) in
743            let presdecl = 
744              P.Mrow ([],
745                [P.Mtext([None,"mathcolor","Red"],"let");
746                 P.smallskip;
747                 P.Mi([],get_name decl);
748                 P.Mtext([],":"); term2pres decl.Con.dec_type]) in
749            let suchthat =
750              P.Mrow ([],
751                [P.Mtext([None,"mathcolor","Red"],"such that");
752                 P.smallskip;
753                 P.Mtext([],"(");
754                 P.Mi([],get_name hyp);
755                 P.Mtext([],")");
756                 P.smallskip;
757                 term2pres hyp.Con.dec_type]) in
758             (* let body = proof2pres {proof with Con.proof_context = tl} in *)
759             let body = conclude2pres proof.Con.proof_conclude false true in
760             let presacontext = 
761               acontext2pres proof.Con.proof_apply_context body false in
762             P.Mtable 
763               ([None,"align","baseline 1"; None,"equalrows","false"; 
764                 None,"columnalign","left"],
765                [P.Mtr ([],[P.Mtd ([],presdecl)]);
766                 P.Mtr ([],[P.Mtd ([],suchthat)]);
767                 P.Mtr ([],[P.Mtd ([],presacontext)])]);
768          | _ -> assert false in
769
770 proof2pres p
771 ;;
772
773 exception ToDo;;
774
775 let content2pres term2pres (id,params,metasenv,obj) =
776  let module K = Content in
777  let module P = Mpresentation in
778   match obj with
779      `Def (K.Const,thesis,`Proof p) ->
780        P.Mtable
781         [None,"align","baseline 1";
782          None,"equalrows","false";
783          None,"columnalign","left";
784          None,"helm:xref","id"]
785         ([P.Mtr []
786            [P.Mtd []
787             (P.Mrow []
788              [P.Mtext []
789                ("UNFINISHED PROOF" ^ id ^"(" ^
790                  String.concat " ; " (List.map UriManager.string_of_uri params)^
791                 ")")])] ;
792          P.Mtr []
793           [P.Mtd []
794             (P.Mrow []
795               [P.Mtext [] "THESIS:"])] ;
796          P.Mtr []
797           [P.Mtd []
798             (P.Mrow []
799               [P.Mphantom []
800                 (P.Mtext [] "__") ;
801               term2pres thesis])]] @
802          (match metasenv with
803              None -> []
804            | Some metasenv' ->
805               [P.Mtr []
806                 [P.Mtd []
807                   (* Conjectures are in their own table to make *)
808                   (* diffing the DOM trees easier.              *)
809                   (P.Mtable
810                     [None,"align","baseline 1";
811                      None,"equalrows","false";
812                      None,"columnalign","left"]
813                    ((P.Mtr []
814                       [P.Mtd []
815                        (P.Mrow []
816                          [P.Mtext [] "CONJECTURES:"])])::
817                     List.map
818                      (function
819                        (id,n,context,ty) ->
820                          P.Mtr []
821                           [P.Mtd []
822                            (P.Mrow [Some "helm", "xref", id]
823                              (List.map
824                                (function
825                                    None ->
826                                      P.Mrow []
827                                       [ P.Mi [] "_" ;
828                                         P.Mo [] ":?" ;
829                                         P.Mi [] "_"]
830                                  | Some (`Declaration d)
831                                  | Some (`Hypothesis d) ->
832                                     let
833                                      { K.dec_name = dec_name ;
834                                        K.dec_type = ty } = d
835                                      in
836                                       P.Mrow []
837                                        [ P.Mi []
838                                           (match dec_name with
839                                               None -> "_"
840                                             | Some n -> n) ;
841                                          P.Mo [] ":" ;
842                                          term2pres ty]
843                                  | Some (`Definition d) ->
844                                     let
845                                      { K.def_name = def_name ;
846                                        K.def_term = bo } = d
847                                      in
848                                       P.Mrow []
849                                        [ P.Mi []
850                                           (match def_name with
851                                               None -> "_"
852                                             | Some n -> n) ;
853                                          P.Mo [] ":=" ;
854                                          term2pres bo]
855                                  | Some (`Proof p) ->
856                                     let proof_name = p.K.proof_name in
857                                      P.Mrow []
858                                       [ P.Mi []
859                                          (match proof_name with
860                                              None -> "_"
861                                            | Some n -> n) ;
862                                         P.Mo [] ":=" ;
863                                         proof2pres term2pres p]
864                                ) (List.rev context) @
865                              [ P.Mo [] "|-" ] @
866                              [ P.Mi [] (string_of_int n) ;
867                                P.Mo [] ":" ;
868                                term2pres ty ]
869                            ))
870                           ]
871                      ) metasenv'
872                   ))]]
873          )  @
874         [P.Mtr []
875           [P.Mtd []
876             (P.Mrow []
877               [proof2pres term2pres p])]])
878    | _ -> raise ToDo
879 ;;
880
881 let content2pres ~ids_to_inner_sorts =
882  content2pres 
883   (function p -> 
884    (Cexpr2pres.cexpr2pres_charcount 
885     (Content_expressions.acic2cexpr ids_to_inner_sorts p)))
886 ;;