X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2FapplyTransformation.ml;h=f58f4dae2e1cba819e7eb1795df1d74d136b8a5b;hb=e053aaf3085a079c3125ed4666ba648a48fbb2af;hp=2a4624c217b7531ae14bd7b42fcdd8c3a106c9cd;hpb=6a5e51c1cf9a56c74a8b53a9b8bc5aa686c9780e;p=helm.git

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 2a4624c21..f58f4dae2 100644
--- 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)