applyTransformation: added debugging information

makefiles: %.mo.opt now working
developments.txt: added Base-2 devel
acic_procedural: some improvements
 new optimization: atomic let-ins are now expanded

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 9815580b6444ef8bb31669e0fd60aaae5cebb60b..d54130a0cd75fdac58377ec0a4920660aa921852 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -249,7 +249,7 @@ let mk_fwd_rewrite st dtext name tl direction t =
    match where with
       | C.ARel (_, _, i, premise) as v ->
          let where = Some (premise, name) in
-         let _script = convert_elim st ~name:(premise, i) t v e in 
+(*         let _script = convert_elim st ~name:(premise, i) t v e in *) 
          let script = mk_arg st what @ mk_arg st v (* @ script *) in
         let st = {st with context = Cn.clear st.context premise} in 
         st, T.Rewrite (direction, what, where, e, dtext) :: script
@@ -259,7 +259,7 @@ let mk_rewrite st dtext where qs tl direction t =
    assert (List.length tl = 5);
    let predicate = List.nth tl 2 in
    let e = Cn.mk_pattern 1 predicate in
-   let script = convert_elim st t t e in
+   let script = [] (* convert_elim st t t e *) in
    script @ [T.Rewrite (direction, where, None, e, dtext); T.Branch (qs, "")]
 
 let rec proc_lambda st name v t =
@@ -350,7 +350,7 @@ and proc_appl st what hd tl =
               let predicate = List.nth tl (parsno - i) in
                let e = Cn.mk_pattern j predicate in
               let using = Some hd in
-              convert_elim st what what e @ script @ 
+              (* convert_elim st what what e @ *) script @ 
               [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
         | None        ->
            let qs = proc_bkd_proofs (next st) synth [] classes tl in

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index 0925289e250111e1921fd9d7daeadff63c6c9eb0..94ef413c1042207a4058f6429e7cc02e4c8f4e72 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -117,6 +117,8 @@ let is_not_atomic = function
    | C.MutConstruct _ -> false
    | _                -> true
 
+let is_atomic t = not (is_not_atomic t)
+
 let get_ind_type uri tyno =
    match E.get_obj Un.empty_ugraph uri with
       | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli
index 881f7e26635c192968d862c64f721ac0b3890e26..97b637d70b126cc21f0c1b80ec28e5faefcf6bbd 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralHelpers.mli
+++ b/helm/software/components/acic_procedural/proceduralHelpers.mli
@@ -43,6 +43,8 @@ val is_unsafe:
    int -> Cic.context * Cic.term -> bool
 val is_not_atomic:
    Cic.term -> bool
+val is_atomic:
+   Cic.term -> bool
 val get_ind_type:
    UriManager.uri -> int -> int * Cic.inductiveType
 val get_default_eliminator:

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index 19d96a91aa7ef042f7113656a43cb8a4ce99f4fa..9d04c2f91f89d0c78667c50f1c5076c56e333065 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -72,7 +72,10 @@ let rec opt1_letin g es c name v t =
          | C.LetIn (nname, vv, tt) when H.is_proof c v ->
            let x = C.LetIn (nname, vv, C.LetIn (name, tt, S.lift_from 2 1 t)) in
            HLog.warn "Optimizer: swap 1"; opt1_proof g true c x 
-         | v                               -> 
+         | v when H.is_proof c v && H.is_atomic v     ->
+           let x = S.subst v t in
+           HLog.warn "Optimizer: remove 5"; opt1_proof g true c x 
+        | v                                           -> 
            g (C.LetIn (name, v, t))
       in
       if es then opt1_term g es c v else g v

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 4883deaf8665ba06816412cc121d04e5fdd7b323..4ef0a5573be2b569375543e66f4c850e826f6067 100644 (file)
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -191,6 +191,11 @@ let txt_of_cic_object ?map_unicode_to_tex n style prefix obj =
        String.concat "" (List.map aux script) ^ "\n\n"
 
 let txt_of_inline_macro style suri prefix =
+   let print_exc = function
+      | ProofEngineHelpers.Bad_pattern s as e ->
+           Printexc.to_string e ^ " " ^ Lazy.force s
+      | e -> Printexc.to_string e
+   in
    let dbd = LibraryDb.instance () in   
    let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in
    let map uri =
@@ -199,6 +204,6 @@ let txt_of_inline_macro style suri prefix =
       with
          | e -> 
            Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n" 
-           (UriManager.string_of_uri uri) (Printexc.to_string e)
+           (UriManager.string_of_uri uri) (print_exc e)
    in
    String.concat "" (List.map map sorted_uris)

diff --git a/helm/software/matita/contribs/CoRN-Decl/makefile b/helm/software/matita/contribs/CoRN-Decl/makefile
index 60f15b469226c7a9bbebe39b400f061a770c1959..e5ac91fc8028e672d12df81f4aca5966d85bb718 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/makefile
+++ b/helm/software/matita/contribs/CoRN-Decl/makefile
@@ -30,7 +30,7 @@ cleanall.opt: preall.opt
 %.mo: preall
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
 %.mo.opt: preall.opt
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=)
        
 preall:
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/makefile
index d53547f4b05bd50be0068d8724c68bc0480f8053..d7a63e5f180e5b0704b0779cbac21fb9cf5700b1 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/makefile
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/makefile
@@ -30,7 +30,7 @@ cleanall.opt: preall.opt
 %.mo: preall
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
 %.mo.opt: preall.opt
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=)
        
 preall:
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/makefile b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/makefile
index d53547f4b05bd50be0068d8724c68bc0480f8053..d7a63e5f180e5b0704b0779cbac21fb9cf5700b1 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/makefile
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/makefile
@@ -30,7 +30,7 @@ cleanall.opt: preall.opt
 %.mo: preall
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
 %.mo.opt: preall.opt
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=)
        
 preall:
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile
index d53547f4b05bd50be0068d8724c68bc0480f8053..d7a63e5f180e5b0704b0779cbac21fb9cf5700b1 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile
@@ -30,7 +30,7 @@ cleanall.opt: preall.opt
 %.mo: preall
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
 %.mo.opt: preall.opt
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=)
        
 preall:
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)

diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/makefile b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/makefile
index 9ef6694eefb15187dc1d2df3cdb6f9dc1f504e43..711fba21cee4b89d9bbf211e1134e4197f623041 100644 (file)
--- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/makefile
+++ b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/makefile
@@ -26,7 +26,7 @@ cleanall.opt: preall
 %.mo: preall
        $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
 %.mo.opt: preall
-       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=)
        
 preall:
        $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)

diff --git a/helm/software/matita/contribs/RELATIONAL/makefile b/helm/software/matita/contribs/RELATIONAL/makefile
index 60f15b469226c7a9bbebe39b400f061a770c1959..e5ac91fc8028e672d12df81f4aca5966d85bb718 100644 (file)
--- a/helm/software/matita/contribs/RELATIONAL/makefile
+++ b/helm/software/matita/contribs/RELATIONAL/makefile
@@ -30,7 +30,7 @@ cleanall.opt: preall.opt
 %.mo: preall
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
 %.mo.opt: preall.opt
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=)
        
 preall:
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)

diff --git a/helm/software/matita/contribs/developments.txt b/helm/software/matita/contribs/developments.txt
index 821b61cd816f60600cdbf1f64211e0607ea40db1..ff8bf2c365140776e69eb695673a65f2c7171154 100644 (file)
--- a/helm/software/matita/contribs/developments.txt
+++ b/helm/software/matita/contribs/developments.txt
@@ -10,3 +10,4 @@ software/matita/contribs/RELATIONAL
 software/matita/contribs/LAMBDA-TYPES/Unified-Sub
 software/matita/contribs/LAMBDA-TYPES/Base-1
 software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1
+software/matita/contribs/LAMBDA-TYPES/Base-2

diff --git a/helm/software/matita/dama/makefile b/helm/software/matita/dama/makefile
index 39d64a95275a1157263b9b08297f6fdc11722911..ce86d13606c853eb26bad8f47cbadfecf4a12a3c 100644 (file)
--- a/helm/software/matita/dama/makefile
+++ b/helm/software/matita/dama/makefile
@@ -26,7 +26,7 @@ cleanall.opt: preall
 %.mo: preall
        $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
 %.mo.opt: preall
-       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=)
        
 preall:
        $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)

diff --git a/helm/software/matita/legacy/makefile b/helm/software/matita/legacy/makefile
index c4020f67386fccd4d20408c7b7d11713d827cc75..ec9f8cb26a5556242ec478a960943cdffefb5994 100644 (file)
--- a/helm/software/matita/legacy/makefile
+++ b/helm/software/matita/legacy/makefile
@@ -30,7 +30,7 @@ cleanall.opt: preall.opt
 %.mo: preall
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
 %.mo.opt: preall.opt
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=)
        
 preall:
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)

diff --git a/helm/software/matita/library/makefile b/helm/software/matita/library/makefile
index c4020f67386fccd4d20408c7b7d11713d827cc75..ec9f8cb26a5556242ec478a960943cdffefb5994 100644 (file)
--- a/helm/software/matita/library/makefile
+++ b/helm/software/matita/library/makefile
@@ -30,7 +30,7 @@ cleanall.opt: preall.opt
 %.mo: preall
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
 %.mo.opt: preall.opt
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=)
        
 preall:
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)

diff --git a/helm/software/matita/library_auto/makefile b/helm/software/matita/library_auto/makefile
index c4020f67386fccd4d20408c7b7d11713d827cc75..ec9f8cb26a5556242ec478a960943cdffefb5994 100644 (file)
--- a/helm/software/matita/library_auto/makefile
+++ b/helm/software/matita/library_auto/makefile
@@ -30,7 +30,7 @@ cleanall.opt: preall.opt
 %.mo: preall
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
 %.mo.opt: preall.opt
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=)
        
 preall:
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)

diff --git a/helm/software/matita/tests/makefile b/helm/software/matita/tests/makefile
index 4fbb0512ec5b6611cabe05fa17a877676c17d6a9..c610118b6f80d94badbb2fdf370b73283812b35f 100644 (file)
--- a/helm/software/matita/tests/makefile
+++ b/helm/software/matita/tests/makefile
@@ -30,7 +30,7 @@ cleanall.opt: preall
 %.mo: preall
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
 %.mo.opt: preall
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=)
        
 preall:
        $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)