From 8509994e58db23307b45081491d35d5f7ff6ea6f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 18 Jan 2017 16:50:09 +0000 Subject: [PATCH] - improved lfpr_lfpr - improved make stats (it was still invoking mac) - hls.ml to list .ma files highligting the ones updated to basic_2A2 --- matita/matita/contribs/lambdadelta/Makefile | 85 +++++++++---------- .../basic_2/etc_new/frees/frees.etc | 5 ++ .../lambdadelta/basic_2/rt_transition/hls.ml | 41 +++++++++ .../basic_2/rt_transition/lfpr_frees.ma | 26 ++++++ .../basic_2/rt_transition/lfpr_lfpr.ma | 5 +- .../basic_2/rt_transition/lfpr_lfpx.ma | 4 - .../basic_2/rt_transition/partial.txt | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 8 files changed, 116 insertions(+), 54 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_frees.ma diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 6aa7ffbf8..9de41db0c 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -19,10 +19,6 @@ DEP_DIR := ../../../components/binaries/matitadep DEP := matitadep.native DEP_OPTS := -MAC_DIR := ../../../components/binaries/mac -MAC := mac.native -MAC_OPTS := - PRB_DIR := ../../../components/binaries/probe PRB := probe.native PRB_OPTS := $(XOA_OPTS) -g -i @@ -53,10 +49,6 @@ define MAS_TEMPLATE $(1)/$(1)_probe.txt: $$(MAS_$(1)) @echo " PROBE $(1)" $$(H)$$(PRB_DIR)/$$(PRB) $$(PRB_OPTS) $(1) -sn -sc -on -oc -f > $$@ - -$(1)/$(1)_mac.txt: $$(MAS_$(1)) - @echo " MAC $(1)" - $$(H)$$(MAC_DIR)/$$(MAC) $$(MAC_OPTS) $$^ > $$@ endef $(foreach PKG, $(PACKAGES), $(eval $(call MAS_TEMPLATE,$(PKG)))) @@ -127,51 +119,54 @@ define STATS_TEMPLATE STT_$(1) := $(1).stats STTS += $$(STT_$(1)) - $$(STT_$(1)): S0 = $$(shell cat $(1)/$(1)_probe.txt) - $$(STT_$(1)): S1 = $$(shell cat $(1)/$(1)_mac.txt) - $$(STT_$(1)): S4 = $$(shell ls $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): P1 = $$(shell grep "^theorem " $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): P2 = $$(shell grep "^lemma " $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): P3 = $$(shell grep "^fact " $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): P4 = $$(shell grep "qed[.-]" $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): C1 = $$(shell grep "^inductive \|^record " $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): C2 = $$(shell grep "^definition \|^let rec " $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): C3 = $$(shell grep "defined[.-]" $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): M1 = $$(shell grep "^axiom " $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): M2 = $$(shell grep "$$(OPEN)\*[^*:]*$$$$" $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): M3 = $$(shell grep "(\*\*)" $$(MAS_$(1)) | wc -l) - -$$(STT_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt $(1)/$(1)_mac.txt + $$(STT_$(1)): C0 = $$(shell cat $(1)/$(1)_probe.txt) + $$(STT_$(1)): C2 = $$(word 2, $$(C0)) + $$(STT_$(1)): C3 = $$(word 4, $$(C0)) + $$(STT_$(1)): O1 = $$(shell ls $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): O2 = $$(word 1, $$(C0)) + $$(STT_$(1)): O3 = $$(word 3, $$(C0)) + $$(STT_$(1)): P1 = $$(word 10, $$(C0)) + $$(STT_$(1)): P2 = $$(word 9, $$(C0)) + $$(STT_$(1)): P3 = $$(word 8, $$(C0)) + $$(STT_$(1)): P4 = $$(shell grep "qed[.-]" $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): D1 = $$(word 5, $$(C0)) + $$(STT_$(1)): D2 = $$(word 7, $$(C0)) + $$(STT_$(1)): D3 = $$(shell grep "defined[.-]" $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): M1 = $$(word 6, $$(C0)) + $$(STT_$(1)): M2 = $$(shell grep "$$(OPEN)\*[^*:]*$$$$" $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): M3 = $$(shell grep "(\*\*)" $$(MAS_$(1)) | wc -l) + +$$(STT_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt @printf '\x1B[1;40;37m' - @printf '%-15s %-47s' 'Statistics for:' $(1) + @printf '%-15s %-46s' 'Statistics for:' $(1) @printf '\x1B[0m\n' @printf '\x1B[1;40;35m' - @printf '%-8s %6i' Chars $$(word 1, $$(S1)) - @printf ' %-8s %4i' Pages $$(word 2, $$(S1)) - @printf ' %-7s %7i' Nodes $$(word 3, $$(S0)) + @printf '%-12s' '' + @printf ' %-8s %6i' Chars $$(C2) + @printf ' %-7s %7i' Nodes $$(C3) @printf ' %-11s' '' @printf '\x1B[0m\n' @printf '\x1B[1;40;36m' - @printf '%-8s %6i' Files $$(S4) - @printf ' %-8s %4i' Sources $$(word 1, $$(S0)) - @printf ' %-7s %7i' Objects $$(word 2, $$(S0)) + @printf '%-8s %3i' Files $$(O1) + @printf ' %-8s %6i' Sources $$(O2) + @printf ' %-7s %7i' Objects $$(O3) @printf ' %-11s' '' @printf '\x1B[0m\n' @printf '\x1B[1;40;32m' - @printf '%-8s %6i' Theorems $$(P1) - @printf ' %-8s %4i' Lemmas $$(P2) + @printf '%-8s %3i' Theorems $$(P1) + @printf ' %-8s %6i' Lemmas $$(P2) @printf ' %-7s %7i' Facts $$(P3) @printf ' %-6s %4i' Proofs $$(P4) @printf '\x1B[0m\n' @printf '\x1B[1;40;33m' - @printf '%-8s %6i' Declared $$(C1) - @printf ' %-8s %4i' Defined $$(C2) - @printf ' %-7s %7i' Proved $$(C3) + @printf '%-8s %3i' Declared $$(D1) + @printf ' %-8s %6i' Defined $$(D2) + @printf ' %-7s %7i' Proved $$(D3) @printf ' %-11s' '' @printf '\x1B[0m\n' @printf '\x1B[1;40;31m' - @printf '%-8s %6i' Axioms $$(M1) - @printf ' %-8s %4i' Comments $$(M2) + @printf '%-8s %3i' Axioms $$(M1) + @printf ' %-8s %6i' Comments $$(M2) @printf ' %-7s %7i' Marks $$(M3) @printf ' %-11s' '' @printf '\x1B[0m\n' @@ -191,15 +186,15 @@ define SUMMARY_TEMPLATE SUM_$(1) := $(1)/web/$(1)_sum.tbl SUMS += $$(SUM_$(1)) - $$(SUM_$(1)): S0 = $$(shell cat $(1)/$(1)_probe.txt) - $$(SUM_$(1)): S1 = $$(word 1, $$(S0)) - $$(SUM_$(1)): S2 = $$(word 2, $$(S0)) - $$(SUM_$(1)): S4 = $$(word 4, $$(S0)) - $$(SUM_$(1)): C1 = $$(word 5, $$(S0)) - $$(SUM_$(1)): C2 = $$(word 7, $$(S0)) + $$(SUM_$(1)): C0 = $$(shell cat $(1)/$(1)_probe.txt) + $$(SUM_$(1)): S1 = $$(word 1, $$(C0)) + $$(SUM_$(1)): S2 = $$(word 2, $$(C0)) + $$(SUM_$(1)): S4 = $$(word 4, $$(C0)) + $$(SUM_$(1)): C1 = $$(word 5, $$(C0)) + $$(SUM_$(1)): C2 = $$(word 7, $$(C0)) $$(SUM_$(1)): C3 = $$(shell echo "$$(C1)+$$(C2)"|bc) - $$(SUM_$(1)): P1 = $$(word 10, $$(S0)) - $$(SUM_$(1)): P2 = $$(word 9, $$(S0)) + $$(SUM_$(1)): P1 = $$(word 10, $$(C0)) + $$(SUM_$(1)): P2 = $$(word 9, $$(C0)) $$(SUM_$(1)): P3 = $$(shell echo "$$(P1)+$$(P2)"|bc) $$(SUM_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.etc new file mode 100644 index 000000000..a9349e870 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.etc @@ -0,0 +1,5 @@ +(* A Basic_A2 lemma we do not need so far *) +axiom frees_pair_flat: ∀L,T,f1,I1,V1. L.ⓑ{I1}V1 ⊢ 𝐅*⦃T⦄ ≡ f1 → + ∀f2,I2,V2. L.ⓑ{I2}V2 ⊢ 𝐅*⦃T⦄ ≡ f2 → + ∀f0. f1 ⋓ f2 ≡ f0 → + ∀I0,I. L.ⓑ{I0}ⓕ{I}V1.V2 ⊢ 𝐅*⦃T⦄ ≡ f0. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml new file mode 100644 index 000000000..9c12ae1c7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml @@ -0,0 +1,41 @@ +let cols = int_of_string (Sys.getenv "COLUMNS") + +let hl = ref [] + +let normal = "\x1B[0m" + +let color = "\x1B[32m" + +let add s = + if s = "" then false else + begin hl := s :: !hl; true end + +let rec read ich = + if Scanf.fscanf ich "%s " add then read ich + +let length l s = max l (String.length s) + +let write l c s = + let pre, post = if List.mem s !hl then color, normal else "", "" in + let spc = String.make (l - String.length s) ' ' in + let bol, ret = + if c = 0 || c = cols then "", l else + if c + l < cols then " ", c + succ l else "\n", l + in + Printf.printf "%s%s%s%s%s" bol pre s post spc; + ret + +let process fname = + let ich = open_in fname in + read ich; close_in ich + +let help = "" + +let main = + Arg.parse [] process help; + let files = Sys.readdir "." in + Array.fast_sort String.compare files; + let l = Array.fold_left length 0 files in + if cols < l then failwith "window too small"; + let c = Array.fold_left (write l) 0 files in + if 0 < c && c < cols then print_newline () diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_frees.ma new file mode 100644 index 000000000..3c204dcd1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_frees.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/lfpx_frees.ma". +include "basic_2/rt_transition/cpm_cpx.ma". + +(* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************) + +(* Properties with context-sensitive free variables *************************) + +lemma cpm_frees_conf: ∀n,h,G. R_frees_confluent (cpm n h G). +/3 width=6 by cpm_fwd_cpx, cpx_frees_conf/ qed-. + +lemma lfpr_frees_conf: ∀h,G. lexs_frees_confluent (cpm 0 h G) cfull. +/4 width=9 by cpm_fwd_cpx, lfpx_frees_conf, lexs_co/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma index fe854ea45..d05584ebf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma @@ -13,13 +13,12 @@ (**************************************************************************) include "basic_2/static/lfxs_lfxs.ma". -include "basic_2/rt_transition/lfpx_frees.ma". include "basic_2/rt_transition/cpm_lsubr.ma". include "basic_2/rt_transition/cpr.ma". include "basic_2/rt_transition/cpr_drops.ma". include "basic_2/rt_transition/lfpr_drops.ma". include "basic_2/rt_transition/lfpr_fqup.ma". -include "basic_2/rt_transition/lfpr_lfpx.ma". +include "basic_2/rt_transition/lfpr_frees.ma". (* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************) @@ -378,4 +377,4 @@ qed-. (* Main properties **********************************************************) theorem lfpr_conf: ∀h,G,T. confluent … (lfpr h G T). -/4 width=6 by cpr_conf_lfpr, lfpx_frees_conf_fwd_lfpr, lfpx_frees_conf, lfxs_conf/ qed-. +/3 width=6 by cpr_conf_lfpr, lfpr_frees_conf, lfxs_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpx.ma index aea28258e..47323a86d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpx.ma @@ -20,9 +20,5 @@ include "basic_2/rt_transition/lfpr.ma". (* Fwd. lemmas with unc. rt-transition for local env.s on referred entries **) -lemma lfpx_frees_conf_fwd_lfpr: ∀h,G. lexs_frees_confluent (cpx h G) cfull → - lexs_frees_confluent (cpm 0 h G) cfull. -/4 width=7 by cpm_fwd_cpx, lexs_co/ qed-. - lemma lfpr_fwd_lfpx: ∀h,T,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈[h, T] L2. /3 width=3 by cpm_fwd_cpx, lfxs_co/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt index 26a059fa7..fc1c009ca 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt @@ -3,4 +3,4 @@ cpx.ma cpx_simple.ma cpx_drops.ma cpx_lsubr.ma lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_cpx.ma cpr.ma cpr_drops.ma -lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fqup.ma lfpr_lfpx.ma lfpr_lfpr.ma +lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fqup.ma lfpr_frees.ma lfpr_lfpx.ma lfpr_lfpr.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index fa1bbc81a..c9380ba24 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -144,7 +144,7 @@ table { ] *) [ { "t-bound context-sensitive rt-transition" * } { - [ "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fqup" + "lfpr_lfpx" + "lfpr_lfpr" * ] + [ "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fqup" + "lfpr_frees" + "lfpr_lfpx" + "lfpr_lfpr" * ] [ "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" (* + "cpr_llpx_sn" + "cpr_cir" *) * ] [ "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_cpx" * ] } -- 2.39.2