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    let rec aux =
 261     function
 262        [] -> continuation
 263      | p::tl ->
 264         let continuation = aux tl in
 265         (* Applicative context get flattened and the "body" of a BU_Conversion
 266            is put in the applicative context. Thus two different situations
 267            are possible:
 268             {method = "BU_Conversion"; applicative_context=[p1; ...; pn]}
 269             {method = xxx; applicative_context =
 270               [ p1; ...; pn; {method="BU_Conversion"} ; p_{n+1}; ... ; pm ]}
 271            In both situations only pn must be processed in in_bu_conversion
 272            mode
 273         *)
 274         let in_bu_conversion =
 275          match tl with
 276             [] -> in_bu_conversion
 277           | p::_ -> p.Con.proof_conclude.Con.conclude_method = "BU_Conversion"
 278         in
 279         let hd =
 280           if indent then
 281             B.indent (proof2pres is_top_down p in_bu_conversion)
 282           else
 283             proof2pres is_top_down p in_bu_conversion
 284         in
 285         B.V([Some "helm","xref",p.Con.proof_id],
 286           [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]);
 287            continuation])
 288    in aux ac
 289
 290   and conclude2pres ?skip_initial_lambdas_internal is_top_down name conclude indent omit_conclusion omit_dot =
 291     let tconclude_body =
 292       match conclude.Con.conclude_conclusion with
 293         Some t (*when not omit_conclusion or
 294          (* CSC: I ignore the omit_conclusion flag in this case.   *)
 295          (* CSC: Is this the correct behaviour? In the stylesheets *)
 296          (* CSC: we simply generated nothing (i.e. the output type *)
 297          (* CSC: of the function should become an option.          *)
 298          conclude.Con.conclude_method = "BU_Conversion" *) ->
 299           let concl = term2pres t in
 300           if conclude.Con.conclude_method = "BU_Conversion" then
 301             B.b_hv []
 302              (make_concl "that is equivalent to" concl ::
 303                      if is_top_down then [B.b_space ; B.b_kw "done";
 304                      B.Text([],".")] else [B.Text([],".")])
 305           else if conclude.Con.conclude_method = "FalseInd" then
 306            (* false ind is in charge to add the conclusion *)
 307            falseind conclude
 308           else
 309             let prequel =
 310               if
 311                (not is_top_down) &&
 312                 conclude.Con.conclude_method = "Intros+LetTac"
 313               then
 314                 let name = get_name name in
 315                  [B.V ([],
 316                  [ B.H([],
 317                     let expected =
 318                       (match conclude.Con.conclude_conclusion with
 319                          None -> B.Text([],"NO EXPECTED!!!")
 320                        | Some c -> term2pres c)
 321                     in
 322                      [make_concl "we need to prove" expected;
 323                       B.skip;
 324                       B.Text([],"(");
 325                       B.Object ([], P.Mi ([],name));
 326                       B.Text([],")");
 327                       B.Text ([],".")
 328                      ])])]
 329               else
 330                [] in
 331             let conclude_body =
 332               conclude_aux ?skip_initial_lambdas_internal conclude in
 333             let ann_concl =
 334               if  conclude.Con.conclude_method = "Intros+LetTac"
 335                || conclude.Con.conclude_method = "ByInduction"
 336                || conclude.Con.conclude_method = "TD_Conversion"
 337               then
 338                B.Text([],"")
 339               else if omit_conclusion then
 340                 B.H([], [B.b_kw "done" ; B.Text([],".") ])
 341               else
 342                 B.b_hv []
 343                  ((if not is_top_down || omit_dot then
 344                     (make_concl "we proved" concl) ::
 345                       if not is_top_down then
 346                        [B.b_space; B.Text([],"(previous)")]
 347                       else []
 348                    else [B.b_kw "done"]
 349                   ) @ if not omit_dot then [B.Text([],".")] else [])
 350             in
 351             B.V ([], prequel @ [conclude_body; ann_concl])
 352       | _ -> conclude_aux ?skip_initial_lambdas_internal conclude
 353     in
 354      if indent then
 355        B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id],
 356                      [tconclude_body]))
 357      else
 358        B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body])
 359
 360   and conclude_aux ?skip_initial_lambdas_internal conclude =
 361     if conclude.Con.conclude_method = "TD_Conversion" then
 362       let expected =
 363         (match conclude.Con.conclude_conclusion with
 364            None -> B.Text([],"NO EXPECTED!!!")
 365          | Some c -> term2pres c) in
 366       let subproof =
 367         (match conclude.Con.conclude_args with
 368           [Con.ArgProof p] -> p
 369          | _ -> assert false) in
 370       let synth =
 371         (match subproof.Con.proof_conclude.Con.conclude_conclusion with
 372            None -> B.Text([],"NO SYNTH!!!")
 373          | Some c -> (term2pres c)) in
 374       B.V
 375         ([],
 376         [make_concl "we need to  prove" expected;
 377          B.H ([],[make_concl "or equivalently" synth; B.Text([],".")]);
 378          proof2pres true subproof false])
 379     else if conclude.Con.conclude_method = "BU_Conversion" then
 380       assert false
 381     else if conclude.Con.conclude_method = "Exact" then
 382       let arg =
 383         (match conclude.Con.conclude_args with
 384            [Con.Term (b,t)] -> assert (not b);term2pres t
 385          | [Con.Premise p] ->
 386              (match p.Con.premise_binder with
 387              | None -> assert false; (* unnamed hypothesis ??? *)
 388              | Some s -> B.Text([],s))
 389          | err -> assert false) in
 390       (match conclude.Con.conclude_conclusion with
 391          None ->
 392           B.b_h [] [B.b_kw "by"; B.b_space; arg]
 393        | Some c ->
 394           B.b_h [] [B.b_kw "by"; B.b_space; arg]
 395        )
 396     else if conclude.Con.conclude_method = "Intros+LetTac" then
 397       (match conclude.Con.conclude_args with
 398          [Con.ArgProof p] ->
 399            (match conclude.Con.conclude_args with
 400               [Con.ArgProof p] ->
 401                 proof2pres ?skip_initial_lambdas_internal true p false
 402             | _ -> assert false)
 403        | _ -> assert false)
 404 (* OLD CODE
 405       let conclusion =
 406       (match conclude.Con.conclude_conclusion with
 407          None -> B.Text([],"NO Conclusion!!!")
 408        | Some c -> term2pres c) in
 409       (match conclude.Con.conclude_args with
 410          [Con.ArgProof p] ->
 411            B.V
 412             ([None,"align","baseline 1"; None,"equalrows","false";
 413               None,"columnalign","left"],
 414               [B.H([],[B.Object([],proof2pres p false)]);
 415                B.H([],[B.Object([],
 416                 (make_concl "we proved 1" conclusion))])]);
 417        | _ -> assert false)
 418 *)
 419     else if (conclude.Con.conclude_method = "Case") then
 420       case conclude
 421     else if (conclude.Con.conclude_method = "ByInduction") then
 422       byinduction conclude
 423     else if (conclude.Con.conclude_method = "Exists") then
 424       exists conclude
 425     else if (conclude.Con.conclude_method = "AndInd") then
 426       andind conclude
 427     else if (conclude.Con.conclude_method = "FalseInd") then
 428       falseind conclude
 429     else if (conclude.Con.conclude_method = "Rewrite") then
 430       let justif1,justif2 =
 431         (match (List.nth conclude.Con.conclude_args 6) with
 432            Con.ArgProof p -> justification term2pres p
 433          | _ -> assert false) in
 434       let term1 =
 435         (match List.nth conclude.Con.conclude_args 2 with
 436            Con.Term (_,t) -> term2pres t
 437          | _ -> assert false) in
 438       let term2 =
 439         (match List.nth conclude.Con.conclude_args 5 with
 440            Con.Term (_,t) -> term2pres t
 441          | _ -> assert false) in
 442 (*
 443       B.V ([],
 444          B.H ([],[
 445           (B.b_kw "rewrite");
 446           B.b_space; term1;
 447           B.b_space; (B.b_kw "with");
 448           B.b_space; term2;
 449           B.b_space; justif1])::
 450             match justif2 with None -> [] | Some j -> [B.indent j])
 451 *) B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term2 ; B.b_kw "=" ; term1; B.b_kw ") (previous)."]); B.b_kw "by _"])
 452     else if conclude.Con.conclude_method = "Eq_chain" then
 453       let justification p =
 454 (*
 455         if skip_initial_lambdas <> None (* cheating *) then
 456           [B.b_kw "by _"]
 457         else
 458 *)
 459           let j1,j2 = justification term2pres p in
 460           j1 :: B.b_space :: (match j2 with Some j -> [j] | None -> [])
 461       in
 462       let rec aux args =
 463         match args with
 464           | [] -> []
 465           | (Con.ArgProof p)::(Con.Term (_,t))::tl ->
 466               B.HOV(RenderingAttrs.indent_attributes `BoxML,([B.b_kw
 467               "=";B.b_space;term2pres t;B.b_space]@justification p@
 468               (if tl <> [] then [B.Text ([],".")] else [])))::(aux tl)
 469           | _ -> assert false
 470       in
 471       let hd =
 472         match List.hd conclude.Con.conclude_args with
 473           | Con.Term (_,t) -> t
 474           | _ -> assert false
 475       in
 476       B.HOV([],[B.b_kw "conclude";B.b_space;term2pres hd; (* B.b_space; *)
 477               B.V ([],aux (List.tl conclude.Con.conclude_args))])
 478     else if conclude.Con.conclude_method = "Apply" then
 479       let pres_args =
 480         make_args_for_apply term2pres conclude.Con.conclude_args in
 481       B.H([],
 482         (B.b_kw "by")::
 483         B.b_space::
 484         B.Text([],"(")::pres_args@[B.Text([],")")])
 485     else
 486       B.V ([], [
 487         B.b_kw ("Apply method" ^ conclude.Con.conclude_method ^ " to");
 488         (B.indent (B.V ([], args2pres conclude.Con.conclude_args)))])
 489
 490   and args2pres l = List.map arg2pres l
 491
 492   and arg2pres =
 493     function
 494         Con.Aux n -> B.b_kw ("aux " ^ n)
 495       | Con.Premise prem -> B.b_kw "premise"
 496       | Con.Lemma lemma -> B.b_kw "lemma"
 497       | Con.Term (_,t) -> term2pres t
 498       | Con.ArgProof p -> proof2pres true p false
 499       | Con.ArgMethod s -> B.b_kw "method"
 500
 501    and case conclude =
 502      let proof_conclusion =
 503        (match conclude.Con.conclude_conclusion with
 504           None -> B.b_kw "No conclusion???"
 505         | Some t -> term2pres t) in
 506      let arg,args_for_cases =
 507        (match conclude.Con.conclude_args with
 508            Con.Aux(_)::Con.Aux(_)::Con.Term(_)::arg::tl ->
 509              arg,tl
 510          | _ -> assert false) in
 511      let case_on =
 512        let case_arg =
 513          (match arg with
 514             Con.Aux n -> B.b_kw "an aux???"
 515            | Con.Premise prem ->
 516               (match prem.Con.premise_binder with
 517                  None -> B.b_kw "the previous result"
 518                | Some n -> B.Object ([], P.Mi([],n)))
 519            | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name))
 520            | Con.Term (_,t) ->
 521                term2pres t
 522            | Con.ArgProof p -> B.b_kw "a proof???"
 523            | Con.ArgMethod s -> B.b_kw "a method???")
 524       in
 525         (make_concl "we proceed by cases on" case_arg) in
 526      let to_prove =
 527         (make_concl "to prove" proof_conclusion) in
 528      B.V ([], case_on::to_prove::(make_cases args_for_cases))
 529
 530    and byinduction conclude =
 531      let proof_conclusion =
 532        (match conclude.Con.conclude_conclusion with
 533           None -> B.b_kw "No conclusion???"
 534         | Some t -> term2pres t) in
 535      let inductive_arg,args_for_cases =
 536        (match conclude.Con.conclude_args with
 537            Con.Aux(n)::_::tl ->
 538              let l1,l2 = split (int_of_string n) tl in
 539              let last_pos = (List.length l2)-1 in
 540              List.nth l2 last_pos,l1
 541          | _ -> assert false) in
 542      let induction_on =
 543        let arg =
 544          (match inductive_arg with
 545             Con.Aux n -> B.b_kw "an aux???"
 546            | Con.Premise prem ->
 547               (match prem.Con.premise_binder with
 548                  None -> B.b_kw "the previous result"
 549                | Some n -> B.Object ([], P.Mi([],n)))
 550            | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name))
 551            | Con.Term (_,t) ->
 552                term2pres t
 553            | Con.ArgProof p -> B.b_kw "a proof???"
 554            | Con.ArgMethod s -> B.b_kw "a method???") in
 555         (make_concl "we proceed by induction on" arg) in
 556      let to_prove =
 557       B.H ([], [make_concl "to prove" proof_conclusion ; B.Text([],".")]) in
 558      B.V ([], induction_on::to_prove::(make_cases args_for_cases))
 559
 560     and make_cases l = List.map make_case l
 561
 562     and make_case =
 563       function
 564         Con.ArgProof p ->
 565           let name =
 566             (match p.Con.proof_name with
 567                None -> B.b_kw "no name for case!!"
 568              | Some n -> B.Object ([], P.Mi([],n))) in
 569           let indhyps,args =
 570              List.partition
 571                (function
 572                    `Hypothesis h -> h.Con.dec_inductive
 573                  | _ -> false) p.Con.proof_context in
 574           let pattern_aux =
 575              List.fold_right
 576                (fun e p ->
 577                   let dec  =
 578                     (match e with
 579                        `Declaration h
 580                      | `Hypothesis h ->
 581                          let name = get_name h.Con.dec_name in
 582                          [B.b_space;
 583                           B.Text([],"(");
 584                           B.Object ([], P.Mi ([],name));
 585                           B.Text([],":");
 586                           (term2pres h.Con.dec_type);
 587                           B.Text([],")")]
 588                      | _ -> assert false (*[B.Text ([],"???")]*)) in
 589                   dec@p) args [] in
 590           let pattern =
 591             B.H ([],
 592                (B.b_kw "case"::B.b_space::name::pattern_aux)@
 593                 [B.b_space;
 594                  B.Text([], ".")]) in
 595           let subconcl =
 596             (match p.Con.proof_conclude.Con.conclude_conclusion with
 597                None -> B.b_kw "No conclusion!!!"
 598              | Some t -> term2pres t) in
 599           let asubconcl = B.indent (make_concl "the thesis becomes" subconcl) in
 600           let induction_hypothesis =
 601             (match indhyps with
 602               [] -> []
 603             | _ ->
 604                let text = B.indent (B.b_kw "by induction hypothesis we know") in
 605                let make_hyp =
 606                  function
 607                    `Hypothesis h ->
 608                      let name =
 609                        (match h.Con.dec_name with
 610                           None -> "useless"
 611                         | Some s -> s) in
 612                      B.indent (B.H ([],
 613                        [term2pres h.Con.dec_type;
 614                         B.b_space;
 615                         B.Text([],"(");
 616                         B.Object ([], P.Mi ([],name));
 617                         B.Text([],")");
 618                         B.Text([],".")]))
 619                    | _ -> assert false in
 620                let hyps = List.map make_hyp indhyps in
 621                text::hyps) in
 622           let body =
 623            conclude2pres true p.Con.proof_name p.Con.proof_conclude true true false in
 624           let presacontext =
 625            let acontext_id =
 626             match p.Con.proof_apply_context with
 627                [] -> p.Con.proof_conclude.Con.conclude_id
 628              | {Con.proof_id = id}::_ -> id
 629            in
 630             B.Action([None,"type","toggle"],
 631               [ B.indent (add_xref acontext_id (B.b_kw "Proof"));
 632                 acontext2pres
 633                  (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion")
 634                  p.Con.proof_apply_context body true
 635                  (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion")
 636               ]) in
 637           B.V ([], pattern::induction_hypothesis@[B.H ([],[asubconcl;B.Text([],".")]);presacontext])
 638        | _ -> assert false
 639
 640      and falseind conclude =
 641        let proof_conclusion =
 642          (match conclude.Con.conclude_conclusion with
 643             None -> B.b_kw "No conclusion???"
 644           | Some t -> term2pres t) in
 645        let case_arg =
 646          (match conclude.Con.conclude_args with
 647              [Con.Aux(n);_;case_arg] -> case_arg
 648            | _ -> assert false;
 649              (*
 650              List.map (ContentPp.parg 0) conclude.Con.conclude_args;
 651              assert false *)) in
 652        let arg =
 653          (match case_arg with
 654              Con.Aux n -> assert false
 655            | Con.Premise prem ->
 656               (match prem.Con.premise_binder with
 657                  None -> [B.b_kw "Contradiction, hence"]
 658                | Some n ->
 659                    [ B.Object ([],P.Mi([],n)); B.skip;
 660                      B.b_kw "is contradictory, hence"])
 661            | Con.Lemma lemma ->
 662                [ B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip;
 663                  B.b_kw "is contradictory, hence" ]
 664            | _ -> assert false) in
 665        make_row arg proof_conclusion
 666
 667      and andind conclude =
 668        let proof,case_arg =
 669          (match conclude.Con.conclude_args with
 670              [Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg
 671            | _ -> assert false;
 672              (*
 673              List.map (ContentPp.parg 0) conclude.Con.conclude_args;
 674              assert false *)) in
 675        let arg =
 676          (match case_arg with
 677              Con.Aux n -> assert false
 678            | Con.Premise prem ->
 679               (match prem.Con.premise_binder with
 680                  None -> []
 681                | Some n -> [(B.b_kw "by"); B.b_space; B.Object([], P.Mi([],n))])
 682            | Con.Lemma lemma ->
 683                [(B.b_kw "by");B.skip;
 684                 B.Object([], P.Mi([],lemma.Con.lemma_name))]
 685            | _ -> assert false) in
 686        match proof.Con.proof_context with
 687          `Hypothesis hyp1::`Hypothesis hyp2::tl ->
 688             let preshyp1 =
 689               B.H ([],
 690                [B.Text([],"(");
 691                 B.Object ([], P.Mi([],get_name hyp1.Con.dec_name));
 692                 B.Text([],")");
 693                 B.skip;
 694                 term2pres hyp1.Con.dec_type]) in
 695             let preshyp2 =
 696               B.H ([],
 697                [B.Text([],"(");
 698                 B.Object ([], P.Mi([],get_name hyp2.Con.dec_name));
 699                 B.Text([],")");
 700                 B.skip;
 701                 term2pres hyp2.Con.dec_type]) in
 702             let body =
 703              conclude2pres false proof.Con.proof_name proof.Con.proof_conclude
 704               false true false in
 705             let presacontext =
 706               acontext2pres false proof.Con.proof_apply_context body false false
 707             in
 708             B.V
 709               ([],
 710                [B.H ([],arg@[B.skip; B.b_kw "we have"]);
 711                 preshyp1;
 712                 B.b_kw "and";
 713                 preshyp2;
 714                 presacontext]);
 715          | _ -> assert false
 716
 717      and exists conclude =
 718        let proof =
 719          (match conclude.Con.conclude_args with
 720              [Con.Aux(n);_;Con.ArgProof proof;_] -> proof
 721            | _ -> assert false;
 722              (*
 723              List.map (ContentPp.parg 0) conclude.Con.conclude_args;
 724              assert false *)) in
 725        match proof.Con.proof_context with
 726            `Declaration decl::`Hypothesis hyp::tl
 727          | `Hypothesis decl::`Hypothesis hyp::tl ->
 728            let presdecl =
 729              B.H ([],
 730                [(B.b_kw "let");
 731                 B.skip;
 732                 B.Object ([], P.Mi([],get_name decl.Con.dec_name));
 733                 B.Text([],":"); term2pres decl.Con.dec_type]) in
 734            let suchthat =
 735              B.H ([],
 736                [(B.b_kw "such that");
 737                 B.skip;
 738                 B.Text([],"(");
 739                 B.Object ([], P.Mi([],get_name hyp.Con.dec_name));
 740                 B.Text([],")");
 741                 B.skip;
 742                 term2pres hyp.Con.dec_type]) in
 743             let body =
 744              conclude2pres false proof.Con.proof_name proof.Con.proof_conclude
 745               false true false in
 746             let presacontext =
 747               acontext2pres false proof.Con.proof_apply_context body false false
 748             in
 749             B.V
 750               ([],
 751                [presdecl;
 752                 suchthat;
 753                 presacontext]);
 754          | _ -> assert false
 755
 756     in
 757     proof2pres
 758      ?skip_initial_lambdas_internal:
 759        (match skip_initial_lambdas with
 760            None -> Some (`Later 0) (* we already printed theorem: *)
 761          | Some n -> Some (`Later n))
 762      is_top_down p false
 763
 764 exception ToDo
 765
 766 let counter = ref 0
 767
 768 let conjecture2pres term2pres (id, n, context, ty) =
 769  B.b_indent
 770   (B.b_hv [Some "helm", "xref", id]
 771      ((B.b_toggle [
 772         B.b_h [] [B.b_text [] "{...}"; B.b_space];
 773         B.b_hv [] (List.map
 774           (function
 775              | None ->
 776                  B.b_h []
 777                    [ B.b_object (p_mi [] "_") ;
 778                      B.b_object (p_mo [] ":?") ;
 779                      B.b_object (p_mi [] "_")]
 780              | Some (`Declaration d)
 781              | Some (`Hypothesis d) ->
 782                  let { Content.dec_name =
 783                      dec_name ; Content.dec_type = ty } = d
 784                  in
 785                    B.b_h []
 786                      [ B.b_object
 787                          (p_mi []
 788                             (match dec_name with
 789                                  None -> "_"
 790                                | Some n -> n));
 791                        B.b_text [] ":";
 792                        term2pres ty ]
 793              | Some (`Definition d) ->
 794                  let
 795                      { Content.def_name = def_name ;
 796                        Content.def_term = bo } = d
 797                  in
 798                    B.b_h []
 799                      [ B.b_object (p_mi []
 800                                      (match def_name with
 801                                           None -> "_"
 802                                         | Some n -> n)) ;
 803                        B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign");
 804                        term2pres bo]
 805              | Some (`Proof p) ->
 806                  let proof_name = p.Content.proof_name in
 807                    B.b_h []
 808                      [ B.b_object (p_mi []
 809                                      (match proof_name with
 810                                           None -> "_"
 811                                         | Some n -> n)) ;
 812                        B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign");
 813                        proof2pres true term2pres p])
 814           (List.rev context)) ] ::
 815          [ B.b_h []
 816            [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash");
 817              B.b_object (p_mi [] (string_of_int n)) ;
 818              B.b_text [] ":" ;
 819              term2pres ty ]])))
 820
 821 let metasenv2pres term2pres = function
 822   | None -> []
 823   | Some metasenv' ->
 824       (* Conjectures are in their own table to make *)
 825       (* diffing the DOM trees easier.              *)
 826       [B.b_v []
 827         ((B.b_kw ("Conjectures:" ^
 828             (let _ = incr counter; in (string_of_int !counter)))) ::
 829          (List.map (conjecture2pres term2pres) metasenv'))]
 830
 831 let params2pres params =
 832   let param2pres uri =
 833     B.b_text [Some "xlink", "href", UriManager.string_of_uri uri]
 834       (UriManager.name_of_uri uri)
 835   in
 836   let rec spatiate = function
 837     | [] -> []
 838     | hd :: [] -> [hd]
 839     | hd :: tl -> hd :: B.b_text [] ", " :: spatiate tl
 840   in
 841   match params with
 842   | [] -> []
 843   | p ->
 844       let params = spatiate (List.map param2pres p) in
 845       [B.b_space;
 846        B.b_h [] (B.b_text [] "[" :: params @ [ B.b_text [] "]" ])]
 847
 848 let recursion_kind2pres params kind =
 849   let kind =
 850     match kind with
 851     | `Recursive _ -> "Recursive definition"
 852     | `CoRecursive -> "CoRecursive definition"
 853     | `Inductive _ -> "Inductive definition"
 854     | `CoInductive _ -> "CoInductive definition"
 855   in
 856   B.b_h [] (B.b_kw kind :: params2pres params)
 857
 858 let inductive2pres term2pres ind =
 859   let constructor2pres decl =
 860     B.b_h [] [
 861       B.b_text [] ("| " ^ get_name decl.Content.dec_name ^ ":");
 862       B.b_space;
 863       term2pres decl.Content.dec_type
 864     ]
 865   in
 866   B.b_v []
 867     (B.b_h [] [
 868       B.b_kw (ind.Content.inductive_name ^ " of arity");
 869       B.smallskip;
 870       term2pres ind.Content.inductive_type ]
 871     :: List.map constructor2pres ind.Content.inductive_constructors)
 872
 873 let joint_def2pres term2pres def =
 874   match def with
 875   | `Inductive ind -> inductive2pres term2pres ind
 876   | _ -> assert false (* ZACK or raise ToDo? *)
 877
 878 let content2pres
 879   ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres
 880   (id,params,metasenv,obj)
 881 =
 882   match obj with
 883   | `Def (Content.Const, thesis, `Proof p) ->
 884       let name = get_name p.Content.proof_name in
 885       let proof = proof2pres true term2pres ?skip_initial_lambdas p in
 886       if skip_thm_and_qed then
 887         proof
 888       else
 889       B.b_v
 890         [Some "helm","xref","id"]
 891         ([ B.b_h [] (B.b_kw ("theorem " ^ name) ::
 892           params2pres params @ [B.b_kw ":"]);
 893            B.H ([],[B.indent (term2pres thesis) ; B.b_kw "." ])] @
 894          metasenv2pres term2pres metasenv @
 895          [proof ; B.b_kw "qed."])
 896   | `Def (_, ty, `Definition body) ->
 897       let name = get_name body.Content.def_name in
 898       B.b_v
 899         [Some "helm","xref","id"]
 900         ([B.b_h []
 901            (B.b_kw ("definition " ^ name) :: params2pres params @ [B.b_kw ":"]);
 902           B.indent (term2pres ty)] @
 903           metasenv2pres term2pres metasenv @
 904           [B.b_kw ":=";
 905            B.indent (term2pres body.Content.def_term);
 906            B.b_kw "."])
 907   | `Decl (_, `Declaration decl)
 908   | `Decl (_, `Hypothesis decl) ->
 909       let name = get_name decl.Content.dec_name in
 910       B.b_v
 911         [Some "helm","xref","id"]
 912         ([B.b_h [] (B.b_kw ("Axiom " ^ name) :: params2pres params);
 913           B.b_kw "Type:";
 914           B.indent (term2pres decl.Content.dec_type)] @
 915           metasenv2pres term2pres metasenv)
 916   | `Joint joint ->
 917       B.b_v []
 918         (recursion_kind2pres params joint.Content.joint_kind
 919         :: List.map (joint_def2pres term2pres) joint.Content.joint_defs)
 920   | _ -> raise ToDo
 921
 922 let content2pres
 923   ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts
 924 =
 925   content2pres ?skip_initial_lambdas ?skip_thm_and_qed
 926     (fun ?(prec=90) annterm ->
 927       let ast, ids_to_uris =
 928         TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
 929       in
 930        CicNotationPres.box_of_mpres
 931         (CicNotationPres.render ids_to_uris ~prec
 932           (TermContentPres.pp_ast ast)))