...

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

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 2a4624c217b7531ae14bd7b42fcdd8c3a106c9cd..f58f4dae2e1cba819e7eb1795df1d74d136b8a5b 100644 (file)
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -35,7 +35,12 @@
 
 (* $Id$ *)
 
-module G = GrafiteAst
+module UM = UriManager
+module C  = Cic
+module Un = CicUniv
+module E  = CicEnvironment
+module TC = CicTypeChecker
+module G  = GrafiteAst
 
 let mpres_document pres_box =
   Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
@@ -170,9 +175,13 @@ let txt_of_cic_object
             Cic2acic.acic_object_of_cic_object obj
         in
         aobj, ids_to_inner_sorts, ids_to_inner_types
-     with e -> 
-        let msg = "txt_of_cic_object: " ^ Printexc.to_string e in
-        failwith msg
+     with 
+        | E.Object_not_found uri -> 
+             let msg = "txt_of_cic_object: object not found: " ^ UM.string_of_uri uri in
+             failwith msg
+       | e                     ->
+             let msg = "txt_of_cic_object: " ^ Printexc.to_string e in
+             failwith msg
   in
   match style with
      | G.Declarative      ->
@@ -191,7 +200,7 @@ let txt_of_cic_object
             (CicNotationPres.mpres_of_box bobj)
         )
      | G.Procedural depth ->
-        let obj = ProceduralOptimizer.optimize_obj obj in
+       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 ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in
         let lazy_term_pp = term_pp in
@@ -205,6 +214,20 @@ let txt_of_cic_object
   in
         "\n\n" ^ String.concat "" (List.map aux script)
 
+let cic_prefix = Str.regexp_string "cic:/"
+
+let matita_prefix = Str.regexp_string "cic:/matita/"
+
+let discharge_uri style uri =
+   let template = match style with
+      | G.Declarative  -> "cic:/matita/declarative/"   
+      | G.Procedural _ -> "cic:/matita/procedural/"
+   in
+   let s = UM.string_of_uri uri in
+   if Str.string_match matita_prefix s 0 then uri else
+   let s = Str.replace_first cic_prefix template s in
+   UM.uri_of_string s
+
 let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
    let print_exc = function
       | ProofEngineHelpers.Bad_pattern s as e ->
@@ -214,14 +237,26 @@ let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
    let dbd = LibraryDb.instance () in   
    let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in
    let map uri =
-      try 
-        txt_of_cic_object 
-          ~map_unicode_to_tex 78 style ?flavour prefix
-          (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
+      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
+        match CicDischarge.discharge_uri (discharge_uri style) uri with
+          | C.InductiveDefinition _ as obj', false ->
+             let uri' = discharge_uri style uri in
+             TC.typecheck_obj uri' obj';  
+             (* we loose the sharing in this case *)
+              let obj'', _ = E.get_obj Un.default_ugraph uri' in
+             let s = do_it obj'' in begin E.remove_obj uri'; s end 
+          | obj, _                                 -> do_it obj
       with
          | e -> 
-            Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" 
-            (UriManager.string_of_uri uri) (print_exc 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
    in
    String.concat "" (List.map map sorted_uris)