(* Copyright (C) 2000, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://cs.unibo.it/helm/.
 *)

(***************************************************************************)
(*                                                                         *)
(*                            PROJECT HELM                                 *)
(*                                                                         *)
(*                Andrea Asperti <asperti@cs.unibo.it>                     *)
(*                              17/06/2003                                 *)
(*                                                                         *)
(***************************************************************************)

let rec split n l =
  if n = 0 then [],l
  else let l1,l2 = 
    split (n-1) (List.tl l) in
    (List.hd l)::l1,l2
;;
  

let is_big_general countterm p =
  let maxsize = Cexpr2pres.maxsize in
  let module Con = Content in
  let rec countp current_size p =
    if current_size > maxsize then current_size
    else 
      let c1 = (countcontext current_size p.Con.proof_context) in
      if c1 > maxsize then c1
    else 
      let c2 = (countapplycontext c1 p.Con.proof_apply_context) in
      if c2 > maxsize then c2
    else 
      countconclude c2 p.Con.proof_conclude

  and 
    countcontext current_size c =
      List.fold_left countcontextitem current_size c
  and
    countcontextitem current_size e =
      if current_size > maxsize then maxsize
      else 
        (match e with
          `Declaration d -> 
            (match d.Con.dec_name with
               Some s -> current_size + 4 + (String.length s)
             | None -> prerr_endline "NO NAME!!"; assert false)
        | `Hypothesis h ->
            (match h.Con.dec_name with
                Some s -> current_size + 4 + (String.length s)
              | None -> prerr_endline "NO NAME!!"; assert false) 
        | `Proof p -> countp current_size p
        | `Definition d -> 
            (match d.Con.def_name with
                Some s -> 
                  let c1 = (current_size + 4 + (String.length s)) in
                  (countterm c1 d.Con.def_term)
              | None -> 
                  prerr_endline "NO NAME!!"; assert false) 
        | `Joint ho -> maxsize + 1) (* we assume is big *)
  and 
    countapplycontext current_size ac =
      List.fold_left countp current_size ac
  and 
    countconclude current_size co =
      if current_size > maxsize then current_size
      else
        let c1 = countargs current_size co.Con.conclude_args in
        if c1 > maxsize then c1 
      else 
        (match co.Con.conclude_conclusion with
           Some concl ->  countterm c1 concl
        | None -> c1)
  and 
    countargs current_size args =
      List.fold_left countarg current_size args
  and
    countarg current_size arg =
      if current_size > maxsize then current_size
      else 
        (match arg with 
           Con.Aux _ -> current_size
         | Con.Premise prem -> 
             (match prem.Con.premise_binder with
                Some s -> current_size + (String.length s)
              | None -> current_size + 7) 
         | Con.Term t -> countterm current_size t
         | Con.ArgProof p -> countp current_size p
         | Con.ArgMethod s -> (maxsize + 1)) in
  let size = (countp 0 p) in
  (size > maxsize)
;;

let is_big = is_big_general (Cexpr2pres.countterm)
;;

let make_row items concl =
  let module P = Mpresentation in
    (match concl with 
       P.Mtable _ -> (* big! *)
         P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
          None,"columnalign","left"],
           [P.Mtr([],[P.Mtd ([],P.Mrow([],items))]);
            P.Mtr ([],[P.Mtd ([],P.indented concl)])])
     | _ ->  (* small *)
       P.Mrow([],items@[P.Mspace([None,"width","0.1cm"]);concl]))
;;

let make_concl verb concl =
  let module P = Mpresentation in
    (match concl with 
       P.Mtable _ -> (* big! *)
         P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
          None,"columnalign","left"],
           [P.Mtr([],[P.Mtd ([],P.Mtext([None,"mathcolor","Red"],verb))]);
            P.Mtr ([],[P.Mtd ([],P.indented concl)])])
     | _ ->  (* small *)
       P.Mrow([],
        [P.Mtext([None,"mathcolor","Red"],verb); 
         P.Mspace([None,"width","0.1cm"]);
         concl]))
;;

let make_args_for_apply term2pres args =
 let module Con = Content in
 let module P = Mpresentation in
 let rec make_arg_for_apply is_first arg row = 
   (match arg with 
      Con.Aux n -> assert false
    | Con.Premise prem -> 
        let name = 
          (match prem.Con.premise_binder with
             None -> "previous"
           | Some s -> s) in
        P.Mi([],name)::row
    | Con.Term t -> 
        if is_first then
          (term2pres t)::row
        else P.Mspace([None,"width","0.1cm"])::P.Mi([],"_")::row
    | Con.ArgProof _ 
    | Con.ArgMethod _ -> 
       P.Mspace([None,"width","0.1cm"])::P.Mi([],"_")::row) in
 match args with 
   hd::tl -> 
     make_arg_for_apply true hd 
       (List.fold_right (make_arg_for_apply false) tl [])
 | _ -> assert false;;

let rec justification term2pres p = 
  let module Con = Content in
  let module P = Mpresentation in
  if ((p.Con.proof_conclude.Con.conclude_method = "Exact") or
     ((p.Con.proof_context = []) &
      (p.Con.proof_apply_context = []) &
      (p.Con.proof_conclude.Con.conclude_method = "Apply"))) then
    let pres_args = 
      make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in
    P.Mrow([],
      P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"])::
      P.Mo([],"(")::pres_args@[P.Mo([],")")]) 
  else proof2pres term2pres p 
     
and proof2pres term2pres p =
  let rec proof2pres p =
    let module Con = Content in
    let module P = Mpresentation in
      let indent = 
        let is_decl e = 
          (match e with 
             `Declaration _
           | `Hypothesis _ -> true
           | _ -> false) in
        ((List.filter is_decl p.Con.proof_context) != []) in 
      let concl = 
        (match p.Con.proof_conclude.Con.conclude_conclusion with
           None -> None
         | Some t -> Some (term2pres t)) in
      let body =
          let presconclude = conclude2pres p.Con.proof_conclude indent in
          let presacontext = 
            acontext2pres p.Con.proof_apply_context presconclude indent in
          context2pres p.Con.proof_context presacontext in
(*
          P.Mtable ([("align","baseline 1");("equalrows","false");
            ("columnalign","left")],
            (context2pres_old p.Con.proof_context)@
            (acontext2pres_old p.Con.proof_apply_context indent)@
            [conclude2pres_old p.Con.proof_conclude indent]) in *)
      match p.Con.proof_name with
        None -> body
      | Some name ->
          let ac = 
        (match concl with
               None -> P.Mtext([],"NO PROOF!!!")
             | Some c -> c) in 
          let action = 
            P.Maction([None,"actiontype","toggle"],
              [(make_concl "proof of" ac);
                body]) in
          P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
              None,"columnalign","left"],
            [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]);
             P.Mtr ([],[P.Mtd ([], P.indented action)])])

  and context2pres c continuation =
    let module P = Mpresentation in
    List.fold_right
      (fun ce continuation ->
         P.Mtable([None,"align","baseline 1"; None,"equalrows","false";
          None,"columnalign","left"],
           [P.Mtr([],[P.Mtd ([],ce2pres ce)]);
            P.Mtr([],[P.Mtd ([], continuation)])])) c continuation

  and context2pres_old c =
    let module P = Mpresentation in
    List.map 
      (function ce -> P.Mtr ([], [P.Mtd ([], ce2pres ce)])) c

  and ce2pres =
    let module P = Mpresentation in
    let module Con = Content in
      function
        `Declaration d -> 
          (match d.Con.dec_name with
              Some s ->
                let ty = term2pres d.Con.dec_type in
                P.Mrow ([],
                  [P.Mtext([None,"mathcolor","Red"],"Assume");
                   P.Mspace([None,"width","0.1cm"]);
                   P.Mi([],s);
                   P.Mtext([],":");
                   ty])
            | None -> 
                prerr_endline "NO NAME!!"; assert false)
      | `Hypothesis h ->
          (match h.Con.dec_name with
              Some s ->
                let ty = term2pres h.Con.dec_type in
                P.Mrow ([],
                  [P.Mtext([None,"mathcolor","Red"],"Suppose");
                   P.Mspace([None,"width","0.1cm"]);
                   P.Mtext([],"(");
                   P.Mi ([],s);
                   P.Mtext([],")");
                   P.Mspace([None,"width","0.1cm"]);
                   ty])
            | None -> 
                prerr_endline "NO NAME!!"; assert false) 
      | `Proof p -> proof2pres p
      | `Definition d -> 
           (match d.Con.def_name with
              Some s ->
                let term = term2pres d.Con.def_term in
                P.Mrow ([],
                  [P.Mtext([],"Let ");
                   P.Mi([],s);
                   P.Mtext([]," = ");
                   term])
            | None -> 
                prerr_endline "NO NAME!!"; assert false) 
      | `Joint ho -> 
            P.Mtext ([],"jointdef")

  and acontext2pres ac continuation indent =
    let module P = Mpresentation in
    List.fold_right
      (fun p continuation ->
         let hd = 
           if indent then
             P.indented (proof2pres p)
           else 
             proof2pres p in
         P.Mtable([None,"align","baseline 1"; None,"equalrows","false";
          None,"columnalign","left"],
           [P.Mtr([],[P.Mtd ([],hd)]);
            P.Mtr([],[P.Mtd ([], continuation)])])) ac continuation 

  and acontext2pres_old ac indent =
    let module P = Mpresentation in
    List.map 
      (function p -> 
         if indent then
           P.Mtr ([], [P.Mtd ([], P.indented (proof2pres p))])
         else 
           P.Mtr ([], 
             [P.Mtd ([], proof2pres p)])) ac

  and conclude2pres conclude indent =
    let module P = Mpresentation in
    if indent then
      P.indented (conclude_aux conclude)
    else 
      conclude_aux conclude

  and conclude2pres_old conclude indent =
    let module P = Mpresentation in
    if indent then
      P.Mtr ([], [P.Mtd ([], P.indented (conclude_aux conclude))])
    else 
      P.Mtr ([], 
        [P.Mtd ([], conclude_aux conclude)])

  and conclude_aux conclude =
    let module Con = Content in
    let module P = Mpresentation in
    if conclude.Con.conclude_method = "TD_Conversion" then
      let expected = 
        (match conclude.Con.conclude_conclusion with 
           None -> P.Mtext([],"NO EXPECTED!!!")
         | Some c -> term2pres c) in
      let subproof = 
        (match conclude.Con.conclude_args with
          [Con.ArgProof p] -> p
         | _ -> assert false) in
      let synth = 
        (match subproof.Con.proof_conclude.Con.conclude_conclusion with
           None -> P.Mtext([],"NO SYNTH!!!")
         | Some c -> (term2pres c)) in
      P.Mtable 
        ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"],
        [P.Mtr([],[P.Mtd([],make_concl "we must prove" expected)]);
         P.Mtr([],[P.Mtd([],make_concl "or equivalently" synth)]);
         P.Mtr([],[P.Mtd([],proof2pres subproof)])])
    else if conclude.Con.conclude_method = "BU_Conversion" then
      let conclusion = 
      (match conclude.Con.conclude_conclusion with 
         None -> P.Mtext([],"NO Conclusion!!!")
       | Some c -> term2pres c) in
      make_concl "that is equivalent to" conclusion
    else if conclude.Con.conclude_method = "Exact" then
      let conclusion = 
        (match conclude.Con.conclude_conclusion with 
           None -> P.Mtext([],"NO Conclusion!!!")
         | Some c -> term2pres c) in
      let arg = 
        (match conclude.Con.conclude_args with 
           [Con.Term t] -> term2pres t
         | _ -> assert false) in
      make_row 
        [arg;P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")] conclusion
    else if conclude.Con.conclude_method = "Intros+LetTac" then
      let conclusion = 
      (match conclude.Con.conclude_conclusion with 
         None -> P.Mtext([],"NO Conclusion!!!")
       | Some c -> term2pres c) in
      (match conclude.Con.conclude_args with
         [Con.ArgProof p] -> 
           P.Mtable 
            ([None,"align","baseline 1"; None,"equalrows","false";
              None,"columnalign","left"],
              [P.Mtr([],[P.Mtd([],proof2pres p)]);
               P.Mtr([],[P.Mtd([],
                (make_concl "we proved *" conclusion))])]);
       | _ -> assert false)
    else if (conclude.Con.conclude_method = "ByInduction") then
      byinduction conclude
    else if (conclude.Con.conclude_method = "Rewrite") then
      let justif = 
        (match (List.nth conclude.Con.conclude_args 6) with
           Con.ArgProof p -> justification term2pres p
         | _ -> assert false) in
      let term1 = 
        (match List.nth conclude.Con.conclude_args 2 with
           Con.Term t -> term2pres t
         | _ -> assert false) in 
      let term2 = 
        (match List.nth conclude.Con.conclude_args 5 with
           Con.Term t -> term2pres t
         | _ -> assert false) in  
      let conclusion = 
        (match conclude.Con.conclude_conclusion with 
           None -> P.Mtext([],"NO Conclusion!!!")
         | Some c -> term2pres c) in
      P.Mtable ([None,"align","baseline 1";None,"equalrows","false";
            None,"columnalign","left"],
             [P.Mtr ([],[P.Mtd ([],P.Mrow([],[
               P.Mtext([None,"mathcolor","Red"],"rewrite");
               P.Mspace([None,"width","0.1cm"]);term1;
               P.Mspace([None,"width","0.1cm"]);
               P.Mtext([None,"mathcolor","Red"],"with");
               P.Mspace([None,"width","0.1cm"]);term2]))]);
              P.Mtr ([],[P.Mtd ([],P.indented justif)]);
              P.Mtr ([],[P.Mtd ([],make_concl "we proved" conclusion)])])
    else if conclude.Con.conclude_method = "Apply" then
      let pres_args = 
        make_args_for_apply term2pres conclude.Con.conclude_args in 
      let by = 
         P.Mrow([],
           P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"])::
           P.Mo([],"(")::pres_args@[P.Mo([],")")]) in 
      match conclude.Con.conclude_conclusion with
        None -> P.Mrow([],[P.Mtext([],"QUA");by])
      | Some t ->
         let concl = (term2pres t) in
         let ann_concl = make_concl "we proved" concl in
         P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
            None,"columnalign","left"],
             [P.Mtr ([],[P.Mtd ([],by)]);
              P.Mtr ([],[P.Mtd ([],ann_concl)])])
    else let body =
      P.Mtable 
        ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"],
         [P.Mtr ([],[P.Mtd ([],P.Mtext([],"Apply method" ^ conclude.Con.conclude_method ^ " to"))]);
          P.Mtr ([],
           [P.Mtd ([], 
             (P.indented 
               (P.Mtable 
                 ([None,"align","baseline 1"; None,"equalrows","false";
                   None,"columnalign","left"],
                  args2pres conclude.Con.conclude_args))))])]) in
     match conclude.Con.conclude_conclusion with
       None -> body
     | Some t ->
         let concl = (term2pres t) in
         let ann_concl = make_concl "we proved" concl in
         P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
            None,"columnalign","left"],
             [P.Mtr ([],[P.Mtd ([],body)]);
              P.Mtr ([],[P.Mtd ([],ann_concl)])])

  and args2pres l =
    let module P = Mpresentation in
    List.map 
     (function a -> P.Mtr ([], [P.Mtd ([], arg2pres a)])) l

  and arg2pres =
    let module P = Mpresentation in
    let module Con = Content in
    function
        Con.Aux n -> 
          P.Mtext ([],"aux " ^ n)
      | Con.Premise prem -> 
          P.Mtext ([],"premise")
      | Con.Term t -> 
          term2pres t
      | Con.ArgProof p ->
        proof2pres p 
      | Con.ArgMethod s -> 
         P.Mtext ([],"method") 
 
   and byinduction conclude =
     let module P = Mpresentation in
     let module Con = Content in
     let proof_conclusion = 
       (match conclude.Con.conclude_conclusion with
          None -> P.Mtext([],"No conclusion???")
        | Some t -> term2pres t) in
     let inductive_arg,args_for_cases = 
       (match conclude.Con.conclude_args with
           Con.Aux(n)::_::tl ->
             let l1,l2 = split (int_of_string n) tl in
             let last_pos = (List.length l2)-1 in
             List.nth l2 last_pos,l1
         | _ -> assert false) in
     let induction_on =
       let arg = 
         (match inductive_arg with
            Con.Aux n -> 
              P.Mtext ([],"an aux???")
           | Con.Premise prem ->
              (match prem.Con.premise_binder with
                 None -> P.Mtext ([],"the previous result")
               | Some n -> P.Mi([],n))
           | Con.Term t -> 
               term2pres t
           | Con.ArgProof p ->
               P.Mtext ([],"a proof???")
           | Con.ArgMethod s -> 
               P.Mtext ([],"a method???")) in
        (make_concl "we proceede by induction on" arg) in
     let to_prove =
        (make_concl "to prove" proof_conclusion) in
     let we_proved = 
        (make_concl "we proved" proof_conclusion) in
     P.Mtable 
       ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"],
          P.Mtr ([],[P.Mtd ([],induction_on)])::
          P.Mtr ([],[P.Mtd ([],to_prove)])::
          (make_cases args_for_cases) @
          [P.Mtr ([],[P.Mtd ([],we_proved)])]) 
    
    and make_cases args_for_cases =
    let module P = Mpresentation in
    List.map 
      (fun p -> P.Mtr ([],[P.Mtd ([],make_case p)])) args_for_cases

    and make_case =  
      let module P = Mpresentation in
      let module Con = Content in
      function 
        Con.ArgProof p ->
          let name =
            (match p.Con.proof_name with
               None -> P.Mtext([],"no name for case!!")
             | Some n -> P.Mi([],n)) in
          let indhyps,args =
             List.partition 
               (function
                   `Hypothesis h -> h.Con.dec_inductive
                 | _ -> false) p.Con.proof_context in
          let pattern_aux =
             List.fold_right
               (fun e p -> 
                  let dec  = 
                    (match e with 
                       `Declaration h 
                     | `Hypothesis h -> 
                         let name = 
                           (match h.Con.dec_name with
                              None -> "NO NAME???"
                           | Some n ->n) in
                         [P.Mspace([None,"width","0.1cm"]);
                          P.Mi ([],name);
                          P.Mtext([],":");
                          (term2pres h.Con.dec_type)]
                     | _ -> [P.Mtext ([],"???")]) in
                  dec@p) args [] in
          let pattern = 
            P.Mtr ([],[P.Mtd ([],P.Mrow([],
               P.Mtext([],"Case")::P.Mspace([None,"width","0.1cm"])::name::pattern_aux@
                [P.Mspace([None,"width","0.1cm"]);
                 P.Mtext([],"->")]))]) in
          let subconcl = 
            (match p.Con.proof_conclude.Con.conclude_conclusion with
               None -> P.Mtext([],"No conclusion!!!") 
             | Some t -> term2pres t) in
          let asubconcl =
             P.Mtr([],[P.Mtd([],
              make_concl "the thesis becomes" subconcl)]) in
          let induction_hypothesis = 
            (match indhyps with
              [] -> []
            | _ -> 
               let text =
                 P.Mtr([],[P.Mtd([], P.indented 
                 (P.Mtext([],"by induction hypothesis we know:")))]) in
               let make_hyp =
                 function 
                   `Hypothesis h ->
                     let name = 
                       (match h.Con.dec_name with
                          None -> "no name"
                        | Some s -> s) in
                     P.indented (P.Mrow ([],
                       [P.Mtext([],"(");
                        P.Mi ([],name);
                        P.Mtext([],")");
                        P.Mspace([None,"width","0.1cm"]);
                        term2pres h.Con.dec_type]))
                   | _ -> assert false in
               let hyps = 
                 List.map 
                   (function ce -> P.Mtr ([], [P.Mtd ([], make_hyp ce)])) 
                    indhyps in
               text::hyps) in          
          (* let acontext = 
               acontext2pres_old p.Con.proof_apply_context true in *)
          let body = conclude2pres p.Con.proof_conclude true in
          let presacontext = 
            acontext2pres p.Con.proof_apply_context body true in
          P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
             None,"columnalign","left"],
             pattern::asubconcl::induction_hypothesis@
              [P.Mtr([],[P.Mtd([],presacontext)])])
      | _ -> assert false in

proof2pres p
;;

exception ToDo;;

let content2pres term2pres (id,params,metasenv,obj) =
 let module K = Content in
 let module P = Mpresentation in
  match obj with
     `Def (K.Const,thesis,`Proof p) ->
       P.Mtable
        [None,"align","baseline 1";
         None,"equalrows","false";
         None,"columnalign","left";
         None,"helm:xref","id"]
        ([P.Mtr []
           [P.Mtd []
            (P.Mrow []
             [P.Mtext []
               ("UNFINISHED PROOF" ^ id ^"(" ^
                 String.concat " ; " (List.map UriManager.string_of_uri params)^
                ")")])] ;
         P.Mtr []
          [P.Mtd []
            (P.Mrow []
              [P.Mtext [] "THESIS:"])] ;
         P.Mtr []
          [P.Mtd []
            (P.Mrow []
              [P.Mphantom []
                (P.Mtext [] "__") ;
              term2pres thesis])]] @
         (match metasenv with
             None -> []
           | Some metasenv' ->
              (P.Mtr []
                [P.Mtd []
                  (P.Mrow []
                    [P.Mtext [] "CONJECTURES:"])]) ::
               List.map
                (function
                  (id,n,context,ty) ->
                    P.Mtr []
                     [P.Mtd []
                      (P.Mrow []
                        (List.map
                          (function
                              (_,None) ->
                                P.Mrow []
                                 [ P.Mi [] "_" ;
                                   P.Mo [] ":?" ;
                                   P.Mi [] "_"]
                            | (_,Some (`Declaration d))
                            | (_,Some (`Hypothesis d)) ->
                               let
                                { K.dec_name = dec_name ;
                                  K.dec_type = ty } = d
                                in
                                 P.Mrow []
                                  [ P.Mi []
                                     (match dec_name with
                                         None -> "_"
                                       | Some n -> n) ;
                                    P.Mo [] ":" ;
                                    term2pres ty]
                            | (_,Some (`Definition d)) ->
                               let
                                { K.def_name = def_name ;
                                  K.def_term = bo } = d
                                in
                                 P.Mrow []
                                  [ P.Mi []
                                     (match def_name with
                                         None -> "_"
                                       | Some n -> n) ;
                                    P.Mo [] ":=" ;
                                    term2pres bo]
                            | (_,Some (`Proof p)) ->
                               let proof_name = p.K.proof_name in
                                P.Mrow []
                                 [ P.Mi []
                                    (match proof_name with
                                        None -> "_"
                                      | Some n -> n) ;
                                   P.Mo [] ":=" ;
                                   proof2pres term2pres p]
                          ) context @
                        [ P.Mo [] "|-" ] @
                        [ P.Mi [] (string_of_int n) ;
                          P.Mo [] ":" ;
                          term2pres ty ]
                      ))
                     ]
                ) metasenv'
         ) @
        [P.Mtr []
          [P.Mtd []
            (P.Mrow []
              [proof2pres term2pres p])]])
   | _ -> raise ToDo
;;

let content2pres ~ids_to_inner_sorts =
 content2pres 
  (function p -> 
   (Cexpr2pres.cexpr2pres_charcount 
    (Content_expressions.acic2cexpr ids_to_inner_sorts p)))
;;