module GE = GrafiteEngine
module LS = LibrarySync
module Ds = CicDischarge
+module PO = ProceduralOptimizer
let mpres_document pres_box =
Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
(CicNotationPres.mpres_of_box bobj)
)
| G.Procedural depth ->
- let obj = ProceduralOptimizer.optimize_obj obj in
+ let obj, info = PO.optimize_obj obj in
let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in
let lazy_term_pp = term_pp in
~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in
let script =
Acic2Procedural.procedural_of_acic_object
- ~ids_to_inner_sorts ~ids_to_inner_types
+ ~ids_to_inner_sorts ~ids_to_inner_types ~info
?depth ?flavour prefix aobj
in
"\n\n" ^ String.concat "" (List.map aux script)
(* procedural_txt_of_cic_term *)
let procedural_txt_of_cic_term ~map_unicode_to_tex n ?depth context term =
+ let term, _info = PO.optimize_term context term in
let annterm, ids_to_inner_sorts, ids_to_inner_types =
try Cic2acic.acic_term_of_cic_term context term
with e ->
String.concat "" (List.map aux script)
;;
+(****************************************************************************)
+
let txt_of_macro ~map_unicode_to_tex metasenv context m =
GrafiteAstPp.pp_macro
~term_pp:(txt_of_cic_term ~map_unicode_to_tex 80 metasenv context)