1. new expressions AND, OR, XOR

[helm.git] / helm / software / matita / applyTransformation.ml

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 58fc1920813ae09291d52d7e4285ec0eb5b2552f..ac044cefed05b15bc5810636555893e02101b5a1 100644 (file)
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -44,6 +44,7 @@ module G  = GrafiteAst
 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)
@@ -203,7 +204,7 @@ let txt_of_cic_object
             (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
@@ -212,7 +213,7 @@ let txt_of_cic_object
          ~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)
@@ -240,6 +241,8 @@ let discharge_uri style uri =
    let _, s = List.fold_left replacement (false, s) replacements in 
    UM.uri_of_string s
 
+let discharge_name s = s ^ "_discharged"
+
 let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
    let print_exc = function
       | ProofEngineHelpers.Bad_pattern s as e ->
@@ -248,24 +251,45 @@ let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
    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 = txt_of_cic_object ~map_unicode_to_tex 78 style ?flavour prefix obj in
-        let obj, real = Ds.discharge_uri (discharge_uri style) uri 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 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
        let _lemmas = LS.add_obj GE.refinement_toolkit newuri obj in
        do_it obj
       with
-         | e -> 
-            let msg = 
-              Printf.sprintf 
-                 "ERROR IN THE GENERATION OF %s\nEXCEPTION: %s" 
-                  (UM.string_of_uri uri) (print_exc e)
-           in
-           Printf.eprintf "%s\n" msg;
-           GrafiteTypes.command_error msg
+         | 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)
 
@@ -286,6 +310,7 @@ let txt_of_inline_macro ~map_unicode_to_tex style ?flavour prefix name =
 (* 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 -> 
@@ -302,3 +327,17 @@ let procedural_txt_of_cic_term ~map_unicode_to_tex n ?depth context term =
         ~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
+;;
+
+