X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2FapplyTransformation.ml;h=ad51250d8dc87f3d1576d0aca8136df179cd5213;hb=907f919aba0f21b18acff8a8e1c266ab92d10baf;hp=700c2e1be425395156c36aa4369244cba23e392d;hpb=a22f5e32e698c3874ded926bd7dabc19719098f3;p=helm.git

diff --git a/matita/matita/applyTransformation.ml b/matita/matita/applyTransformation.ml
index 700c2e1be..ad51250d8 100644
--- a/matita/matita/applyTransformation.ml
+++ b/matita/matita/applyTransformation.ml
@@ -44,9 +44,7 @@ module G  = GrafiteAst
 module GE = GrafiteEngine
 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)
@@ -159,44 +157,6 @@ let txt_of_cic_term ~map_unicode_to_tex size metasenv context t =
    metasenv fake_sequent 
 ;;
 
-ignore (
- CicMetaSubst.set_ppterm_in_context
-  (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
-       ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
-       30 metasenv context' term' in
-      if String.contains res '\n' then
-       "\n" ^ res ^ "\n"
-      else
-       res
-    with
-       Sys.Break as exn -> raise exn
-     | exn ->
-        "[[ Exception raised during pretty-printing: " ^
-         (try
-           Printexc.to_string exn
-          with
-             Sys.Break as exn -> raise exn
-           | _ -> "<<exception raised pretty-printing the exception>>"
-         ) ^ " ]] " ^
-        (CicMetaSubst.use_low_level_ppterm_in_context := true;
-         try
-          let res =
-           CicMetaSubst.ppterm_in_context ~metasenv subst term context
-          in
-           CicMetaSubst.use_low_level_ppterm_in_context := false;
-           res
-         with
-          exc -> 
-           CicMetaSubst.use_low_level_ppterm_in_context := false;
-           raise exc))
-);;
-
 (****************************************************************************)
 (* txt_of_cic_object: IMPROVE ME *)
 
@@ -352,97 +312,6 @@ let discharge_uri params uri =
 
 let discharge_name s = s ^ "_discharged"
 
-let txt_of_inline_uri ~map_unicode_to_tex params suri =
-(*   
-   Ds.debug := true;
-*)
-   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 error uri e =
-      let msg  = 
-         Printf.sprintf 
-            "ERROR IN THE GENERATION OF %s\nEXCEPTION: %s" 
-            (UM.string_of_uri uri) e
-      in
-      Printf.eprintf "%s\n" msg;
-      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 =
-	   let r = txt_of_cic_object ~map_unicode_to_tex 78 params 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 params) uri
-	in
-	if real then do_it obj else
-	let newuri = discharge_uri params uri in
-	let _lemmas = LS.add_obj ~pack_coercion_obj:CicRefine.pack_coercion_obj newuri obj in
-	do_it obj
-      with
-         | TC.TypeCheckerFailure s ->
-	    error uri ("failure  : " ^ Lazy.force s)
-         | TC.AssertFailure s      ->
-	    error uri ("assert   : " ^ Lazy.force s)
-         | E.Object_not_found u    ->
-	    error uri ("not found: " ^ UM.string_of_uri u)
-	 | e                       -> error uri (print_exc e)
-   in
-   String.concat "" (List.map map sorted_uris)
-
-let txt_of_inline_macro ~map_unicode_to_tex params name =
-   let suri = 
-      if Librarian.is_uri name then name else
-      let include_paths = 
-         Helm_registry.get_list Helm_registry.string "matita.includes"
-      in
-      let _, baseuri, _, _ = 
-         Librarian.baseuri_of_script ~include_paths name
-      in
-      baseuri ^ "/"
-   in
-   txt_of_inline_uri ~map_unicode_to_tex params suri
-
-(****************************************************************************)
-(* procedural_txt_of_cic_term *)
-
-let procedural_txt_of_cic_term ~map_unicode_to_tex n params 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 -> 
-        let msg = "procedural_txt_of_cic_term: " ^ Printexc.to_string e in
-        failwith msg
-  in
-  let term_pp = term2pres ~map_unicode_to_tex (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
-     ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in
-  let script = 
-     A2P.procedural_of_acic_term 
-        ~ids_to_inner_sorts ~ids_to_inner_types params 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)