helm/software/components/content_pres/content2pres.ml

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