X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FapplyTransformation.ml;h=5d81d922496e28be36697bb59b77dd74af9f94f1;hb=f79567e3b0abcb508c94b66d69d967c4df83082a;hp=499c1705be978b97c7f9634ead475190e817e208;hpb=b11675b6c6cdeaeabd74dfd99143ea5f87db205b;p=helm.git

diff --git a/matita/applyTransformation.ml b/matita/applyTransformation.ml
index 499c1705b..5d81d9224 100644
--- a/matita/applyTransformation.ml
+++ b/matita/applyTransformation.ml
@@ -35,6 +35,8 @@
 
 (* $Id$ *)
 
+module G = GrafiteAst
+
 let mpres_document pres_box =
   Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
 
@@ -105,6 +107,7 @@ ignore (
   (fun ~metasenv subst term context ->
     try
      let context' = CicMetaSubst.apply_subst_context subst context in
+     let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
      let term' = CicMetaSubst.apply_subst subst term in
      let res = txt_of_cic_term 30 metasenv context' term' in
       if String.contains res '\n' then
@@ -147,7 +150,7 @@ let term2pres ?map_unicode_to_tex n ids_to_inner_sorts annterm =
    let bobj =
       CicNotationPres.box_of_mpres (
          CicNotationPres.render ~prec:90 ids_to_uris 
-	    (TermContentPres.pp_ast ast)
+            (TermContentPres.pp_ast ast)
       )
    in
    let render = function _::x::_ -> x | _ -> assert false in
@@ -155,40 +158,64 @@ let term2pres ?map_unicode_to_tex n ids_to_inner_sorts annterm =
    let s = BoxPp.render_to_string ?map_unicode_to_tex render n mpres in
    remove_closed_substs s
 
-let txt_of_cic_object ?map_unicode_to_tex n style prefix obj =
-  let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = 
-     try Cic2acic.acic_object_of_cic_object obj
+let txt_of_cic_object 
+ ?map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n style prefix obj 
+=
+  let get_aobj obj = 
+     try   
+        let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
+            Cic2acic.acic_object_of_cic_object obj
+        in
+        aobj, ids_to_inner_sorts, ids_to_inner_types
      with e -> 
-        let msg = "Cic2ACic: " ^ Printexc.to_string e in
-	failwith msg
+        let msg = "txt_of_cic_object: " ^ Printexc.to_string e in
+        failwith msg
   in
   match style with
-     | GrafiteAst.Declarative      ->
-        let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in
-        let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in
+     | G.Declarative      ->
+        let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
+        let cobj = 
+          Acic2content.annobj2content 
+            ids_to_inner_sorts ids_to_inner_types aobj 
+        in
+        let bobj = 
+          Content2pres.content2pres 
+            ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts cobj 
+        in
         remove_closed_substs ("\n\n" ^
-	   BoxPp.render_to_string ?map_unicode_to_tex
+           BoxPp.render_to_string ?map_unicode_to_tex
             (function _::x::_ -> x | _ -> assert false) n
             (CicNotationPres.mpres_of_box bobj)
-	)
-     | GrafiteAst.Procedural depth ->
+        )
+     | G.Procedural depth ->
+        let obj = ProceduralOptimizer.optimize_obj obj in
+        let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
         let term_pp = term2pres (n - 8) ids_to_inner_sorts in
         let lazy_term_pp = term_pp in
         let obj_pp = CicNotationPp.pp_obj term_pp in
         let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in
-        let script = Acic2Procedural.acic2procedural 
-	   ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj in
-	"\n\n" ^ String.concat "" (List.map aux script)
+        let script = 
+    Acic2Procedural.acic2procedural 
+           ~ids_to_inner_sorts ~ids_to_inner_types ?depth ?skip_thm_and_qed prefix aobj 
+  in
+        String.concat "" (List.map aux script) ^ "\n\n"
 
-let txt_of_inline_macro style suri prefix =
+let txt_of_inline_macro ?map_unicode_to_tex style suri prefix =
+   let print_exc = function
+      | ProofEngineHelpers.Bad_pattern s as e ->
+           Printexc.to_string e ^ " " ^ Lazy.force s
+      | e -> Printexc.to_string e
+   in
    let dbd = LibraryDb.instance () in   
    let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in
    let map uri =
-      try txt_of_cic_object 78 style prefix (* FG: mi pare meglio 78 *)
-                            (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
+      try 
+        txt_of_cic_object 
+          ?map_unicode_to_tex 78 style prefix
+          (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
       with
          | e -> 
-	    Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" 
-	    (UriManager.string_of_uri uri) (Printexc.to_string e)
+            Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" 
+            (UriManager.string_of_uri uri) (print_exc e)
    in
-   String.concat "\n\n" (List.map map sorted_uris)
+   String.concat "" (List.map map sorted_uris)