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
+(*
+ PO.critical := false;
+ Acic2Procedural.tex_formatter := Some Format.std_formatter;
+ let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in
+*)
+ let obj, info = PO.optimize_obj obj in
+(*
+ let _ = ProceduralTeX.tex_of_obj Format.std_formatter 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)
let discharge_name s = s ^ "_discharged"
let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
+(*
+ Ds.debug := true;
+*)
let print_exc = function
| ProofEngineHelpers.Bad_pattern s as e ->
Printexc.to_string e ^ " " ^ Lazy.force s
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 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
+ 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
- else
+ 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
- let _lemmas = LS.add_obj GE.refinement_toolkit newuri obj in
+ let _lemmas = LS.add_obj ~pack_coercion_obj:CicRefine.pack_coercion_obj newuri obj in
do_it obj
with
| TC.TypeCheckerFailure s ->
(* 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
+;;
+
+