applyTransformation: variable discharging in procedural/declarative script

                     reconstruction is now activated
we rebuilt the dependence files

diff --git a/helm/software/matita/.depend b/helm/software/matita/.depend
index 97149bc33cf0a656cf11acf4cc1ac07da675ddd1..a6cb0d1f36c5954c877ec3103f921586dcde2546 100644 (file)
--- a/helm/software/matita/.depend
+++ b/helm/software/matita/.depend
@@ -4,10 +4,10 @@ dump_moo.cmo: buildTimeConf.cmo
 dump_moo.cmx: buildTimeConf.cmx 
 lablGraphviz.cmo: lablGraphviz.cmi 
 lablGraphviz.cmx: lablGraphviz.cmi 
-matitaAutoGui.cmo: matitaGeneratedGui.cmo applyTransformation.cmi \
-    matitaAutoGui.cmi 
-matitaAutoGui.cmx: matitaGeneratedGui.cmx applyTransformation.cmx \
-    matitaAutoGui.cmi 
+matitaAutoGui.cmo: matitaGtkMisc.cmi matitaGeneratedGui.cmo buildTimeConf.cmo \
+    applyTransformation.cmi matitaAutoGui.cmi 
+matitaAutoGui.cmx: matitaGtkMisc.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \
+    applyTransformation.cmx matitaAutoGui.cmi 
 matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi 
 matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi 
 matitacLib.cmo: matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmo \
@@ -18,8 +18,8 @@ matitac.cmo: matitadep.cmi matitaclean.cmi matitacLib.cmi matitaWiki.cmo \
     matitaMisc.cmi matitaInit.cmi 
 matitac.cmx: matitadep.cmx matitaclean.cmx matitacLib.cmx matitaWiki.cmx \
     matitaMisc.cmx matitaInit.cmx 
-matitadep.cmo: matitaInit.cmi matitadep.cmi 
-matitadep.cmx: matitaInit.cmx matitadep.cmi 
+matitadep.cmo: matitaMisc.cmi matitaInit.cmi matitadep.cmi 
+matitadep.cmx: matitaMisc.cmx matitaInit.cmx matitadep.cmi 
 matitaEngine.cmo: matitaEngine.cmi 
 matitaEngine.cmx: matitaEngine.cmi 
 matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi 
@@ -34,10 +34,8 @@ matitaGui.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
 matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
     matitaMathView.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx \
     matitaExcPp.cmx matitaAutoGui.cmx buildTimeConf.cmx matitaGui.cmi 
-matitaInit.cmo: matitacLib.cmi matitaExcPp.cmi matitaEngine.cmi \
-    buildTimeConf.cmo matitaInit.cmi 
-matitaInit.cmx: matitacLib.cmx matitaExcPp.cmx matitaEngine.cmx \
-    buildTimeConf.cmx matitaInit.cmi 
+matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmo matitaInit.cmi 
+matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi 
 matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
     matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi lablGraphviz.cmi \
     buildTimeConf.cmo applyTransformation.cmi matitaMathView.cmi 

diff --git a/helm/software/matita/.depend.opt b/helm/software/matita/.depend.opt
index 19b605d2de31e9c862c60b5362144ac33c383d2f..386bd0727441ae90de1f48773cd5460c6627c7fa 100644 (file)
--- a/helm/software/matita/.depend.opt
+++ b/helm/software/matita/.depend.opt
@@ -4,9 +4,9 @@ dump_moo.cmo: buildTimeConf.cmx
 dump_moo.cmx: buildTimeConf.cmx 
 lablGraphviz.cmo: lablGraphviz.cmi 
 lablGraphviz.cmx: lablGraphviz.cmi 
-matitaAutoGui.cmo: matitaGeneratedGui.cmx buildTimeConf.cmx \
+matitaAutoGui.cmo: matitaGtkMisc.cmi matitaGeneratedGui.cmx buildTimeConf.cmx \
     applyTransformation.cmi matitaAutoGui.cmi 
-matitaAutoGui.cmx: matitaGeneratedGui.cmx buildTimeConf.cmx \
+matitaAutoGui.cmx: matitaGtkMisc.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \
     applyTransformation.cmx matitaAutoGui.cmi 
 matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi 
 matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi 

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 0982757b02d8b38ba933636c85e5a144cb442c32..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,16 +237,23 @@ 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 -> 
             let msg = 
               Printf.sprintf 
-                 "ERRORE IN STAMPA DI %s\nEXCEPTION: %s" 
-                  (UriManager.string_of_uri uri) (print_exc e)
+                 "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