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)
GrafiteTypes.command_error msg
in
let map uri =
+ Librarian.time_stamp "AT: BEGIN MAP";
try
(* FG: for now the explicit variables must be discharged *)
- let do_it obj = txt_of_cic_object ~map_unicode_to_tex 78 style ?flavour prefix obj in
- let obj, real =
- Ds.discharge_uri discharge_name (discharge_uri style) uri
+ let do_it obj =
+ let r = txt_of_cic_object ~map_unicode_to_tex 78 style ?flavour prefix obj in
+ Librarian.time_stamp "AT: END MAP "; r
+ in
+ let obj, real =
+ let s = UM.string_of_uri uri in
+ if Str.string_match matita_prefix s 0 then begin
+ Librarian.time_stamp "AT: GETTING OBJECT";
+ let obj, _ = E.get_obj Un.default_ugraph uri in
+ Librarian.time_stamp "AT: DONE ";
+ obj, true
+ end else
+ Ds.discharge_uri discharge_name (discharge_uri style) uri
in
if real then do_it obj else
let newuri = discharge_uri style uri in
(* 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 ->
~ids_to_inner_sorts ~ids_to_inner_types ?depth "" context annterm
in
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)
+ ~lazy_term_pp:(fun (f : Cic.lazy_term) ->
+ let t,metasenv,_ = f context metasenv CicUniv.empty_ugraph in
+ txt_of_cic_term ~map_unicode_to_tex 80 metasenv context t)
+ m
+;;
+
+