X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FapplyTransformation.ml;h=bdc3b9268c799089fe34f49a7e5cb40a664ff7a6;hb=1439ced76cb62f9c5f5e638c53a005c3843870ae;hp=2988af4211fa00143d85a84b2eeaa5de2424e545;hpb=d3548c16f481b14ce94e64c790bc767c59590050;p=helm.git diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 2988af421..bdc3b9268 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -46,6 +46,7 @@ module LS = LibrarySync module Ds = CicDischarge module PO = ProceduralOptimizer module N = CicNotationPt +module A2P = Acic2Procedural let mpres_document pres_box = Xml.add_xml_declaration (CicNotationPres.print_box pres_box) @@ -65,10 +66,11 @@ let mml_of_cic_sequent metasenv sequent = (asequent, (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts))) -let nmml_of_cic_sequent metasenv subst sequent = - let content_sequent = NTermCicContent.nmap_sequent ~subst sequent in +let nmml_of_cic_sequent status metasenv subst sequent = + let content_sequent,ids_to_refs = + NTermCicContent.nmap_sequent status ~metasenv ~subst sequent in let pres_sequent = - Sequent2pres.nsequent2pres subst content_sequent in + Sequent2pres.nsequent2pres ids_to_refs subst content_sequent in let xmlpres = mpres_document pres_sequent in Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres @@ -88,6 +90,13 @@ let mml_of_cic_object obj = (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses, ids_to_inner_sorts,ids_to_inner_types))) +let nmml_of_cic_object status obj = + let cobj,ids_to_nrefs = NTermCicContent.nmap_obj status obj in + let pres_sequent = Content2pres.ncontent2pres ~ids_to_nrefs cobj in + let xmlpres = mpres_document pres_sequent in + Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres +;; + let txt_of_cic_sequent ~map_unicode_to_tex size metasenv sequent = let unsh_sequent,(asequent,ids_to_terms, ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses) @@ -111,8 +120,10 @@ let txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type size let t, ids_to_uris = TermAcicContent.ast_of_acic ~output_type ids_to_inner_sorts t in let t = TermContentPres.pp_ast t in - let t = CicNotationPres.render ids_to_uris t in - BoxPp.render_to_string ~map_unicode_to_tex + let t = + CicNotationPres.render ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) t + in + BoxPp.render_to_string ~map_unicode_to_tex (function x::_ -> x | _ -> assert false) size t let txt_of_cic_term ~map_unicode_to_tex size metasenv context t = @@ -169,9 +180,10 @@ let term2pres ~map_unicode_to_tex n ids_to_inner_sorts annterm = let ast, ids_to_uris = TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in let bobj = - CicNotationPres.box_of_mpres ( - CicNotationPres.render ~prec:90 ids_to_uris - (TermContentPres.pp_ast ast)) in + CicNotationPres.box_of_mpres ( + CicNotationPres.render ~prec:90 + ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) + (TermContentPres.pp_ast ast)) in let render = function _::x::_ -> x | _ -> assert false in let mpres = CicNotationPres.mpres_of_box bobj in let s = BoxPp.render_to_string ~map_unicode_to_tex render n mpres in @@ -202,10 +214,12 @@ let txt_of_cic_object failwith msg in if List.mem G.IPProcedural params then begin -(* - PO.debug := true; + + Procedural2.debug := A2P.is_debug 1 params; + PO.debug := A2P.is_debug 2 params; +(* PO.critical := false; - Acic2Procedural.tex_formatter := Some Format.std_formatter; + A2P.tex_formatter := Some Format.std_formatter; let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in *) let obj, info = PO.optimize_obj obj in @@ -221,15 +235,35 @@ let txt_of_cic_object ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in let aux = function - | G.Executable (_, G.Command (_, G.Obj (_, N.Inductive _))) as stm - -> + | G.Executable (_, G.Command (_, G.Obj (_, N.Inductive _))) + | G.Executable (_, G.Command (_, G.Obj (_, N.Record _))) as stm + -> + let hc = !Acic2content.hide_coercions in + if List.mem G.IPCoercions params then + Acic2content.hide_coercions := false; enable_notations false; - let str = stm_pp stm in enable_notations true; str -(* FG: we disable notation for Inductive to avoid recursive notation *) - | stm -> stm_pp stm + let str = stm_pp stm in + enable_notations true; + Acic2content.hide_coercions := hc; + str +(* FG: we disable notation for inductive types to avoid recursive notation *) + | G.Executable (_, G.Tactic _) as stm -> + let hc = !Acic2content.hide_coercions in + Acic2content.hide_coercions := false; + let str = stm_pp stm in + Acic2content.hide_coercions := hc; + str +(* FG: we show coercion because the reconstruction is not aware of them *) + | stm -> + let hc = !Acic2content.hide_coercions in + if List.mem G.IPCoercions params then + Acic2content.hide_coercions := false; + let str = stm_pp stm in + Acic2content.hide_coercions := hc; + str in let script = - Acic2Procedural.procedural_of_acic_object + A2P.procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ~info params aobj in String.concat "" (List.map aux script) ^ "\n\n" @@ -357,7 +391,7 @@ let procedural_txt_of_cic_term ~map_unicode_to_tex n params context term = let aux = GrafiteAstPp.pp_statement ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in let script = - Acic2Procedural.procedural_of_acic_term + A2P.procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types params context annterm in String.concat "" (List.map aux script)