X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent2pres.ml;h=ee3e64bd5456d873e0af5f74ca00f2c6213ab5b9;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=fdffe82760b840622a2f33829903e7d13abee456;hpb=bc36fe01d5465d07ef76c445c83639e341f3eb2a;p=helm.git diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index fdffe8276..ee3e64bd5 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000, HELM Team. +(* Copyright (C) 2003-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -34,6 +34,7 @@ module P = Mpresentation module B = Box +module Con = Content let p_mtr a b = Mpresentation.Mtr(a,b) let p_mtd a b = Mpresentation.Mtd(a,b) @@ -49,114 +50,35 @@ let rec split n 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 = Ast2pres.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.Lemma lemma -> - current_size + (String.length lemma.Con.lemma_name) - | 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 (Ast2pres.countterm) -;; - -let get_xref = - let module Con = Content in - function - `Declaration d - | `Hypothesis d -> d.Con.dec_id - | `Proof p -> p.Con.proof_id - | `Definition d -> d.Con.def_id - | `Joint jo -> jo.Con.joint_id -;; - -let make_row ?(attrs=[]) items concl = - match concl with - B.V _ -> (* big! *) +let get_xref = function + | `Declaration d + | `Hypothesis d -> d.Con.dec_id + | `Proof p -> p.Con.proof_id + | `Definition d -> d.Con.def_id + | `Joint jo -> jo.Con.joint_id + +let hv_attrs = + RenderingAttrs.spacing_attributes `BoxML + @ RenderingAttrs.indent_attributes `BoxML + +let make_row items concl = + B.b_hv hv_attrs (items @ [ concl ]) +(* match concl with + B.V _ -> |+ big! +| B.b_v attrs [B.b_h [] items; B.b_indent concl] - | _ -> (* small *) - B.b_h attrs (items@[B.b_space; concl]) -;; + | _ -> |+ small +| + B.b_h attrs (items@[B.b_space; concl]) *) let make_concl ?(attrs=[]) verb concl = - match concl with - B.V _ -> (* big! *) + B.b_hv (hv_attrs @ attrs) [ B.b_kw verb; concl ] +(* match concl with + B.V _ -> |+ big! +| B.b_v attrs [ B.b_kw verb; B.b_indent concl] - | _ -> (* small *) - B.b_h attrs [ B.b_kw verb; B.b_space; concl ] -;; + | _ -> |+ small +| + B.b_h attrs [ B.b_kw verb; B.b_space; concl ] *) let make_args_for_apply term2pres args = - let module Con = Content in let make_arg_for_apply is_first arg row = let res = match arg with @@ -168,7 +90,11 @@ let make_args_for_apply term2pres args = | Some s -> s) in (B.b_object (P.Mi ([], name)))::row | Con.Lemma lemma -> - (B.b_object (P.Mi([],lemma.Con.lemma_name)))::row + let lemma_attrs = [ + Some "helm", "xref", lemma.Con.lemma_id; + Some "xlink", "href", lemma.Con.lemma_uri ] + in + (B.b_object (P.Mi(lemma_attrs,lemma.Con.lemma_name)))::row | Con.Term t -> if is_first then (term2pres t)::row @@ -184,15 +110,16 @@ let make_args_for_apply term2pres args = make_arg_for_apply true hd (List.fold_right (make_arg_for_apply false) tl []) | _ -> assert false -;; let get_name = function | Some s -> s | None -> "_" +let add_xref id = function + | B.Text (attrs, t) -> B.Text (((Some "helm", "xref", id) :: attrs), t) + | _ -> assert false (* TODO, add_xref is meaningful for all boxes *) + 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 = []) & @@ -206,40 +133,39 @@ let rec justification term2pres p = and proof2pres term2pres p = let rec proof2pres p = - let module Con = Content 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 omit_conclusion = (not indent) && (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 omit_conclusion in - let presacontext = - acontext2pres p.Con.proof_apply_context presconclude indent in - context2pres p.Con.proof_context presacontext in - match p.Con.proof_name with - None -> body - | Some name -> - let action = - match concl with - None -> body - | Some ac -> - B.Action - ([None,"type","toggle"], - [(make_concl ~attrs:[Some "helm", "xref", p.Con.proof_id] - "proof of" ac); body]) - in - B.V ([], - [B.Text ([],"(" ^ name ^ ")"); - B.indent action]) + let indent = + let is_decl e = + (match e with + `Declaration _ + | `Hypothesis _ -> true + | _ -> false) in + ((List.filter is_decl p.Con.proof_context) != []) in + let omit_conclusion = (not indent) && (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 omit_conclusion in + let presacontext = + acontext2pres p.Con.proof_apply_context presconclude indent in + context2pres p.Con.proof_context presacontext in + match p.Con.proof_name with + None -> body + | Some name -> + let action = + match concl with + None -> body + | Some ac -> + B.Action + ([None,"type","toggle"], + [(make_concl ~attrs:[Some "helm", "xref", p.Con.proof_id] + "proof of" ac); body]) + in + B.V ([], + [B.Text ([],"(" ^ name ^ ")"); + B.indent action]) and context2pres c continuation = (* we generate a subtable for each context element, for selection @@ -254,17 +180,32 @@ and proof2pres term2pres p = (fun ce continuation -> let xref = get_xref ce in B.V([Some "helm", "xref", xref ], - [B.H([Some "helm", "xref", "ce_"^xref],[ce2pres ce]); + [B.H([Some "helm", "xref", "ce_"^xref], + [ce2pres_in_proof_context_element ce]); continuation])) tl continuation in let hd_xref= get_xref hd in B.V([], [B.H([Some "helm", "xref", "ce_"^hd_xref], - [ce2pres hd]); + [ce2pres_in_proof_context_element hd]); continuation']) - and ce2pres = - let module Con = Content in - function + and ce2pres_in_joint_context_element = function + | `Inductive _ -> assert false (* TODO *) + | (`Declaration _) as x -> ce2pres x + | (`Hypothesis _) as x -> ce2pres x + | (`Proof _) as x -> ce2pres x + | (`Definition _) as x -> ce2pres x + + and ce2pres_in_proof_context_element = function + | `Joint ho -> + B.H ([],(List.map ce2pres_in_joint_context_element ho.Content.joint_defs)) + | (`Declaration _) as x -> ce2pres x + | (`Hypothesis _) as x -> ce2pres x + | (`Proof _) as x -> ce2pres x + | (`Definition _) as x -> ce2pres x + + and ce2pres = + function `Declaration d -> (match d.Con.dec_name with Some s -> @@ -298,19 +239,14 @@ and proof2pres term2pres p = Some s -> let term = term2pres d.Con.def_term in B.H ([], - [B.Text([],"Let "); - B.Object ([], P.Mi([],s)); - B.Text([]," = "); - term]) + [ B.b_kw "Let"; B.b_space; + B.Object ([], P.Mi([],s)); + B.Text([]," = "); + term]) | None -> prerr_endline "NO NAME!!"; assert false) - | `Joint ho -> assert false (* - B.H ([], - (B.Text ([],"JOINT ") - :: List.map ce2pres ho.Content.joint_defs)) *) and acontext2pres ac continuation indent = - let module Con = Content in List.fold_right (fun p continuation -> let hd = @@ -323,8 +259,6 @@ and proof2pres term2pres p = continuation])) ac continuation and conclude2pres conclude indent omit_conclusion = - let module Con = Content in - let module P = Mpresentation in let tconclude_body = match conclude.Con.conclude_conclusion with Some t when @@ -354,10 +288,7 @@ and proof2pres term2pres p = else B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body]) - 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 @@ -392,7 +323,7 @@ and proof2pres term2pres p = B.b_h [] [B.b_kw "Consider"; B.b_space; arg] | Some c -> let conclusion = term2pres c in make_row - [arg; B.b_space; B.Text([],"proves")] + [arg; B.b_space; B.b_kw "proves"] conclusion ) else if conclude.Con.conclude_method = "Intros+LetTac" then @@ -452,37 +383,25 @@ and proof2pres term2pres p = B.b_space:: B.Text([],"(")::pres_args@[B.Text([],")")]) else - B.V - ([], - [B.Text([],"Apply method" ^ conclude.Con.conclude_method ^ " to"); - (B.indent - (B.V - ([], - args2pres conclude.Con.conclude_args)))]) + B.V ([], [ + B.b_kw ("Apply method" ^ conclude.Con.conclude_method ^ " to"); + (B.indent (B.V ([], args2pres conclude.Con.conclude_args)))]) and args2pres l = List.map arg2pres l and arg2pres = - let module Con = Content in function - Con.Aux n -> - B.Text ([],"aux " ^ n) - | Con.Premise prem -> - B.Text ([],"premise") - | Con.Lemma lemma -> - B.Text ([],"lemma") - | Con.Term t -> - term2pres t - | Con.ArgProof p -> - proof2pres p - | Con.ArgMethod s -> - B.Text ([],"method") + Con.Aux n -> B.b_kw ("aux " ^ n) + | Con.Premise prem -> B.b_kw "premise" + | Con.Lemma lemma -> B.b_kw "lemma" + | Con.Term t -> term2pres t + | Con.ArgProof p -> proof2pres p + | Con.ArgMethod s -> B.b_kw "method" and case conclude = - let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with - None -> B.Text([],"No conclusion???") + None -> B.b_kw "No conclusion???" | Some t -> term2pres t) in let arg,args_for_cases = (match conclude.Con.conclude_args with @@ -492,31 +411,26 @@ and proof2pres term2pres p = let case_on = let case_arg = (match arg with - Con.Aux n -> - B.Text ([],"an aux???") + Con.Aux n -> B.b_kw "an aux???" | Con.Premise prem -> (match prem.Con.premise_binder with - None -> B.Text ([],"the previous result") + None -> B.b_kw "the previous result" | Some n -> B.Object ([], P.Mi([],n))) | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name)) | Con.Term t -> term2pres t - | Con.ArgProof p -> - B.Text ([],"a proof???") - | Con.ArgMethod s -> - B.Text ([],"a method???")) in - (make_concl "we proceede by cases on" case_arg) in + | Con.ArgProof p -> B.b_kw "a proof???" + | Con.ArgMethod s -> B.b_kw "a method???") + in + (make_concl "we proceed by cases on" case_arg) in let to_prove = (make_concl "to prove" proof_conclusion) in - B.V - ([], - case_on::to_prove::(make_cases args_for_cases)) + B.V ([], case_on::to_prove::(make_cases args_for_cases)) and byinduction conclude = - let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with - None -> B.Text([],"No conclusion???") + None -> B.b_kw "No conclusion???" | Some t -> term2pres t) in let inductive_arg,args_for_cases = (match conclude.Con.conclude_args with @@ -528,36 +442,29 @@ and proof2pres term2pres p = let induction_on = let arg = (match inductive_arg with - Con.Aux n -> - B.Text ([],"an aux???") + Con.Aux n -> B.b_kw "an aux???" | Con.Premise prem -> (match prem.Con.premise_binder with - None -> B.Text ([],"the previous result") + None -> B.b_kw "the previous result" | Some n -> B.Object ([], P.Mi([],n))) | Con.Lemma lemma -> B.Object ([], P.Mi([],lemma.Con.lemma_name)) | Con.Term t -> term2pres t - | Con.ArgProof p -> - B.Text ([],"a proof???") - | Con.ArgMethod s -> - B.Text ([],"a method???")) in - (make_concl "we proceede by induction on" arg) in + | Con.ArgProof p -> B.b_kw "a proof???" + | Con.ArgMethod s -> B.b_kw "a method???") in + (make_concl "we proceed by induction on" arg) in let to_prove = (make_concl "to prove" proof_conclusion) in - B.V - ([], - induction_on::to_prove:: - (make_cases args_for_cases)) + B.V ([], induction_on::to_prove:: (make_cases args_for_cases)) and make_cases l = List.map make_case l and make_case = - let module Con = Content in function Con.ArgProof p -> let name = (match p.Con.proof_name with - None -> B.Text([],"no name for case!!") + None -> B.b_kw "no name for case!!" | Some n -> B.Object ([], P.Mi([],n))) in let indhyps,args = List.partition @@ -583,20 +490,19 @@ and proof2pres term2pres p = dec@p) args [] in let pattern = B.H ([], - (B.Text([],"Case")::B.b_space::name::pattern_aux)@ + (B.b_kw "Case"::B.b_space::name::pattern_aux)@ [B.b_space; - B.Text([],"->")]) in + B.Text([], Utf8Macro.unicode_of_tex "\\Rightarrow")]) in let subconcl = (match p.Con.proof_conclude.Con.conclude_conclusion with - None -> B.Text([],"No conclusion!!!") + None -> B.b_kw "No conclusion!!!" | Some t -> term2pres t) in let asubconcl = B.indent (make_concl "the thesis becomes" subconcl) in let induction_hypothesis = (match indhyps with [] -> [] | _ -> - let text = - B.indent (B.Text([],"by induction hypothesis we know:")) in + let text = B.indent (B.b_kw "by induction hypothesis we know") in let make_hyp = function `Hypothesis h -> @@ -623,20 +529,15 @@ and proof2pres term2pres p = | {Con.proof_id = id}::_ -> id in B.Action([None,"type","toggle"], - [B.indent - (B.Text - ([None,"color","red" ; - Some "helm", "xref", acontext_id],"Proof")) ; - acontext2pres p.Con.proof_apply_context body true]) in + [ B.indent (add_xref acontext_id (B.b_kw "Proof")); + acontext2pres p.Con.proof_apply_context body true]) in B.V ([], pattern::asubconcl::induction_hypothesis@[presacontext]) | _ -> assert false and falseind conclude = - let module P = Mpresentation in - let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with - None -> B.Text([],"No conclusion???") + None -> B.b_kw "No conclusion???" | Some t -> term2pres t) in let case_arg = (match conclude.Con.conclude_args with @@ -650,21 +551,21 @@ and proof2pres term2pres p = Con.Aux n -> assert false | Con.Premise prem -> (match prem.Con.premise_binder with - None -> [B.Text([],"Contradiction, hence")] + None -> [B.b_kw "Contradiction, hence"] | Some n -> - [B.Object ([],P.Mi([],n)); B.skip;B.Text([],"is contradictory, hence")]) + [ B.Object ([],P.Mi([],n)); B.skip; + B.b_kw "is contradictory, hence"]) | Con.Lemma lemma -> - [B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip; B.Text([],"is contradictory, hence")] + [ B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip; + B.b_kw "is contradictory, hence" ] | _ -> assert false) in (* let body = proof2pres {proof with Con.proof_context = tl} in *) make_row arg proof_conclusion and andind conclude = - let module P = Mpresentation in - let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with - None -> B.Text([],"No conclusion???") + None -> B.b_kw "No conclusion???" | Some t -> term2pres t) in let proof,case_arg = (match conclude.Con.conclude_args with @@ -681,7 +582,8 @@ and proof2pres term2pres p = None -> [] | Some n -> [(B.b_kw "by"); B.b_space; B.Object([], P.Mi([],n))]) | Con.Lemma lemma -> - [(B.b_kw "by");B.skip; B.Object([], P.Mi([],lemma.Con.lemma_name))] + [(B.b_kw "by");B.skip; + B.Object([], P.Mi([],lemma.Con.lemma_name))] | _ -> assert false) in match proof.Con.proof_context with `Hypothesis hyp1::`Hypothesis hyp2::tl -> @@ -709,19 +611,17 @@ and proof2pres term2pres p = acontext2pres proof.Con.proof_apply_context body false in B.V ([], - [B.H ([],arg@[B.skip; B.Text([],"we have")]); + [B.H ([],arg@[B.skip; B.b_kw "we have"]); preshyp1; - B.Text([],"and"); + B.b_kw "and"; preshyp2; presacontext]); | _ -> assert false and exists conclude = - let module P = Mpresentation in - let module Con = Content in let proof_conclusion = (match conclude.Con.conclude_conclusion with - None -> B.Text([],"No conclusion???") + None -> B.b_kw "No conclusion???" | Some t -> term2pres t) in let proof = (match conclude.Con.conclude_args with @@ -761,12 +661,12 @@ and proof2pres term2pres p = [presdecl; suchthat; presacontext]); - | _ -> assert false in + | _ -> assert false -proof2pres p -;; + in + proof2pres p -exception ToDo;; +exception ToDo let counter = ref 0 @@ -802,7 +702,7 @@ let conjecture2pres term2pres (id, n, context, ty) = (match def_name with None -> "_" | Some n -> n)) ; - B.b_text [] ":=" ; + B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign"); term2pres bo] | Some (`Proof p) -> let proof_name = p.Content.proof_name in @@ -811,10 +711,10 @@ let conjecture2pres term2pres (id, n, context, ty) = (match proof_name with None -> "_" | Some n -> n)) ; - B.b_text [] ":=" ; + B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign"); proof2pres term2pres p]) (List.rev context)) @ - [ B.b_text [] "|-" ; + [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash"); B.b_object (p_mi [] (string_of_int n)) ; B.b_text [] ":" ; term2pres ty ]))) @@ -825,9 +725,8 @@ let metasenv2pres term2pres = function (* Conjectures are in their own table to make *) (* diffing the DOM trees easier. *) [B.b_v [] - ((B.b_text [] - ("Conjectures:" ^ - (let _ = incr counter; in (string_of_int !counter)))) :: + ((B.b_kw ("Conjectures:" ^ + (let _ = incr counter; in (string_of_int !counter)))) :: (List.map (conjecture2pres term2pres) metasenv'))] let params2pres params = @@ -855,7 +754,7 @@ let recursion_kind2pres params kind = | `Inductive _ -> "Inductive definition" | `CoInductive _ -> "CoInductive definition" in - B.b_h [] (B.b_text [] kind :: params2pres params) + B.b_h [] (B.b_kw kind :: params2pres params) let inductive2pres term2pres ind = let constructor2pres decl = @@ -867,7 +766,8 @@ let inductive2pres term2pres ind = in B.b_v [] (B.b_h [] [ - B.b_text [] (ind.Content.inductive_name ^ " of arity "); + B.b_kw (ind.Content.inductive_name ^ " of arity"); + B.smallskip; term2pres ind.Content.inductive_type ] :: List.map constructor2pres ind.Content.inductive_constructors) @@ -882,8 +782,8 @@ let content2pres term2pres (id,params,metasenv,obj) = let name = get_name p.Content.proof_name in B.b_v [Some "helm","xref","id"] - ([ B.b_h [] (B.b_text [] ("Proof " ^ name) :: params2pres params); - B.b_text [] "Thesis:"; + ([ B.b_h [] (B.b_kw ("Proof " ^ name) :: params2pres params); + B.b_kw "Thesis:"; B.indent (term2pres thesis) ] @ metasenv2pres term2pres metasenv @ [proof2pres term2pres p]) @@ -891,18 +791,18 @@ let content2pres term2pres (id,params,metasenv,obj) = let name = get_name body.Content.def_name in B.b_v [Some "helm","xref","id"] - ([B.b_h [] (B.b_text [] ("Definition " ^ name) :: params2pres params); - B.b_text [] "Type:"; + ([B.b_h [] (B.b_kw ("Definition " ^ name) :: params2pres params); + B.b_kw "Type:"; B.indent (term2pres ty)] @ metasenv2pres term2pres metasenv @ - [term2pres body.Content.def_term]) + [B.b_kw "Body:"; term2pres body.Content.def_term]) | `Decl (_, `Declaration decl) | `Decl (_, `Hypothesis decl) -> let name = get_name decl.Content.dec_name in B.b_v [Some "helm","xref","id"] - ([B.b_h [] (B.b_text [] ("Axiom " ^ name) :: params2pres params); - B.b_text [] "Type:"; + ([B.b_h [] (B.b_kw ("Axiom " ^ name) :: params2pres params); + B.b_kw "Type:"; B.indent (term2pres decl.Content.dec_type)] @ metasenv2pres term2pres metasenv) | `Joint joint -> @@ -910,23 +810,14 @@ let content2pres term2pres (id,params,metasenv,obj) = (recursion_kind2pres params joint.Content.joint_kind :: List.map (joint_def2pres term2pres) joint.Content.joint_defs) | _ -> raise ToDo -;; - -(* -let content2pres ~ids_to_inner_sorts = - content2pres - (function p -> - (Cexpr2pres.cexpr2pres_charcount - (Content_expressions.acic2cexpr ids_to_inner_sorts p))) -;; -*) let content2pres ~ids_to_inner_sorts = content2pres (fun annterm -> - let (ast, ids_to_uris) as arg = - Acic2Ast.ast_of_acic ids_to_inner_sorts annterm + let ast, ids_to_uris = + CicNotationRew.ast_of_acic ids_to_inner_sorts annterm in - let astBox = Ast2pres.ast2astBox arg in - Box.map (fun ast -> Ast2pres.ast2mpres (ast, ids_to_uris)) astBox) + CicNotationPres.box_of_mpres + (CicNotationPres.render ids_to_uris + (CicNotationRew.pp_ast ast)))