From: Ferruccio Guidi Date: Sun, 20 May 2007 10:41:12 +0000 (+0000) Subject: applyTransformation: added debugging information X-Git-Tag: make_still_working~6327 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=20c9d7116bdfefe8075dd04266836c183d66178e;p=helm.git 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 9815580b6..d54130a0c 100644 --- 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 0925289e2..94ef413c1 100644 --- 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 881f7e266..97b637d70 100644 --- 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 19d96a91a..9d04c2f91 100644 --- 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 4883deaf8..4ef0a5573 100644 --- 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 60f15b469..e5ac91fc8 100644 --- 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 d53547f4b..d7a63e5f1 100644 --- 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 d53547f4b..d7a63e5f1 100644 --- 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 d53547f4b..d7a63e5f1 100644 --- 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 9ef6694ee..711fba21c 100644 --- 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 60f15b469..e5ac91fc8 100644 --- 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 821b61cd8..ff8bf2c36 100644 --- 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 39d64a952..ce86d1360 100644 --- 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 c4020f673..ec9f8cb26 100644 --- 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 c4020f673..ec9f8cb26 100644 --- 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 c4020f673..ec9f8cb26 100644 --- 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 4fbb0512e..c610118b6 100644 --- 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)