X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FapplyTransformation.ml;h=ca73e2baac10b2738622247327fec249fd903517;hb=1b9751de891efa2761cdc6cb9d019df6aaaa8514;hp=f58f4dae2e1cba819e7eb1795df1d74d136b8a5b;hpb=71cc47ca7047fdb74dca7c4d3808ccd2343ca1db;p=helm.git

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index f58f4dae2..ca73e2baa 100644
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -41,6 +41,9 @@ module Un = CicUniv
 module E  = CicEnvironment
 module TC = CicTypeChecker
 module G  = GrafiteAst
+module GE = GrafiteEngine
+module LS = LibrarySync
+module Ds = CicDischarge
 
 let mpres_document pres_box =
   Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
@@ -215,8 +218,16 @@ let txt_of_cic_object
         "\n\n" ^ String.concat "" (List.map aux script)
 
 let cic_prefix = Str.regexp_string "cic:/"
-
 let matita_prefix = Str.regexp_string "cic:/matita/"
+let suffixes = [".ind"; "_rec.con"; "_rect.con"; "_ind.con"; ".con"]
+
+let replacements = 
+   let map s = String.length s, s, Str.regexp_string s, "_discharged" ^ s in 
+   List.map map suffixes
+
+let replacement (ok, u) (l, s, x, t) =
+   if ok then ok, u else
+   if Str.last_chars u l = s then true, Str.replace_first x t u else ok, u
 
 let discharge_uri style uri =
    let template = match style with
@@ -226,8 +237,11 @@ let discharge_uri style uri =
    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
+   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 ->
@@ -236,27 +250,34 @@ 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 =
       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
+        let obj, real = 
+	   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)