- matitadep: new option -t to list the unreferenced sources

- lambdadelta: Makefile update to use matitadep -t
               redundant dependecy removed in cl_weight
	       test.ma: shows a bug in the disambiguation mechanism

diff --git a/matita/components/binaries/matitadep/matitadep.ml b/matita/components/binaries/matitadep/matitadep.ml
index de8f3d65db7a03d2f9f88b814890bb38ba00c599..0415a5111f1b02821ad8612d68dc1f43997e4fa8 100644 (file)
--- a/matita/components/binaries/matitadep/matitadep.ml
+++ b/matita/components/binaries/matitadep/matitadep.ml
@@ -46,9 +46,29 @@ let check () =
    let iter fname file = ignore (compute [] fname file) in
    Hashtbl.iter iter graph 
 
+let get_unions () =
+   let map1 ddeps dname = StringSet.add dname ddeps in 
+   let map2 fname file (fnames, ddeps) =
+      StringSet.add fname fnames, List.fold_left map1 ddeps file.ddeps
+   in
+   Hashtbl.fold map2 graph (StringSet.empty, StringSet.empty)
+
+let top () =
+   let iter dname = Printf.printf "top: %s\n" dname in
+   let fnames, ddeps = get_unions () in
+   StringSet.iter iter (StringSet.diff fnames ddeps) 
+
 let rec read ich = 
    let _ = Scanf.sscanf (input_line ich) "%s@:include \"%s@\"." init in
    read ich
    
 let _ =
-   try read stdin with End_of_file -> check ()
+   let show_top = ref false in
+   let process_file name = () in
+   let help   = "" in
+   let help_t = " Print the top nodes of the dependences graph" in
+   Arg.parse [
+      "-t", Arg.Set show_top, help_t;
+   ] process_file help;
+   try read stdin with End_of_file ->
+   if !show_top then top () else check ()

diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile
index a5502a41c1f36788fd19502d611ec170682bf4ec..db7ab3bffa53496baafa8afcd64b12bb36761494 100644 (file)
--- a/matita/matita/contribs/lambdadelta/Makefile
+++ b/matita/matita/contribs/lambdadelta/Makefile
@@ -28,7 +28,7 @@ PRB_OPTS     := $(XOA_OPTS) -g
 ORIG         := . ./orig.sh 
 ORIGS        := basic_2/basic_1.orig
 
-TAGS := all xoa xoa2 orig elim deps stats tbls trim
+TAGS := all xoa xoa2 orig elim deps top stats tbls trim
 
 PACKAGES := ground_2 basic_2 apps_2
 
@@ -89,6 +89,12 @@ deps: $(DEP_DIR)/$(DEP)
        @echo "  MATITADEP"
        $(H)grep "include \"" $(MAS) | $<
 
+# top ########################################################################
+
+top: $(DEP_DIR)/$(DEP)
+       @echo "  MATITADEP -t"
+       $(H)grep "include \"" $(MAS) | $< -t
+
 # stats ######################################################################
 
 define STATS_TEMPLATE

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
index 1188e613c4b8766242eb94456273d28531503a23..063e7b05eb03f3c719b1b3499a6b53e2fecf4f5b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
@@ -15,7 +15,6 @@
 include "basic_2/notation/functions/weight_3.ma".
 include "basic_2/grammar/genv.ma". (**) (* including genv after lenv shows a disambiguation bug: only the last interpretation is considered *)
 include "basic_2/grammar/lenv_weight.ma".
-include "basic_2/grammar/cl_shift.ma".
 
 (* WEIGHT OF A CLOSURE ******************************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma
new file mode 100644 (file)
index 0000000..806d353
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma
@@ -0,0 +1,200 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground_2/arith.ma".
+
+(* ITEMS ********************************************************************)
+
+(* atomic items *)
+inductive item0: Type[0] ≝
+   | Sort: nat → item0 (* sort: starting at 0 *)
+   | LRef: nat → item0 (* reference by index: starting at 0 *)
+   | GRef: nat → item0 (* reference by position: starting at 0 *)
+.
+
+(* binary binding items *)
+inductive bind2: Type[0] ≝
+  | Abbr: bind2 (* abbreviation *)
+  | Abst: bind2 (* abstraction *)
+.
+
+(* binary non-binding items *)
+inductive flat2: Type[0] ≝
+  | Appl: flat2 (* application *)
+  | Cast: flat2 (* explicit type annotation *)
+.
+
+(* binary items *)
+inductive item2: Type[0] ≝
+  | Bind2: bool → bind2 → item2 (* polarized binding item *)
+  | Flat2: flat2 → item2        (* non-binding item *)
+.
+
+(* TERMS ********************************************************************)
+
+include "basic_2/notation/constructors/item0_1.ma".
+include "basic_2/notation/constructors/snitem2_3.ma".
+include "basic_2/notation/constructors/snbind2_4.ma".
+include "basic_2/notation/constructors/snbind2pos_3.ma".
+include "basic_2/notation/constructors/snbind2neg_3.ma".
+include "basic_2/notation/constructors/snflat2_3.ma".
+include "basic_2/notation/constructors/star_1.ma".
+include "basic_2/notation/constructors/lref_1.ma".
+include "basic_2/notation/constructors/gref_1.ma".
+include "basic_2/notation/constructors/snabbr_3.ma".
+include "basic_2/notation/constructors/snabbrpos_2.ma".
+include "basic_2/notation/constructors/snabbrneg_2.ma".
+include "basic_2/notation/constructors/snabst_3.ma".
+include "basic_2/notation/constructors/snabstpos_2.ma".
+include "basic_2/notation/constructors/snabstneg_2.ma".
+include "basic_2/notation/constructors/snappl_2.ma".
+include "basic_2/notation/constructors/sncast_2.ma".
+include "basic_2/grammar/item.ma".
+
+(* terms *)
+inductive term: Type[0] ≝
+  | TAtom: item0 → term               (* atomic item construction *)
+  | TPair: item2 → term → term → term (* binary item construction *)
+.
+
+interpretation "term construction (atomic)"
+   'Item0 I = (TAtom I).
+
+interpretation "term construction (binary)"
+   'SnItem2 I T1 T2 = (TPair I T1 T2).
+
+interpretation "term binding construction (binary)"
+   'SnBind2 a I T1 T2 = (TPair (Bind2 a I) T1 T2).
+
+interpretation "term positive binding construction (binary)"
+   'SnBind2Pos I T1 T2 = (TPair (Bind2 true I) T1 T2).
+
+interpretation "term negative binding construction (binary)"
+   'SnBind2Neg I T1 T2 = (TPair (Bind2 false I) T1 T2).
+
+interpretation "term flat construction (binary)"
+   'SnFlat2 I T1 T2 = (TPair (Flat2 I) T1 T2).
+
+interpretation "sort (term)"
+   'Star k = (TAtom (Sort k)).
+
+interpretation "local reference (term)"
+   'LRef i = (TAtom (LRef i)).
+
+interpretation "global reference (term)"
+   'GRef p = (TAtom (GRef p)).
+
+interpretation "abbreviation (term)"
+   'SnAbbr a T1 T2 = (TPair (Bind2 a Abbr) T1 T2).
+
+interpretation "positive abbreviation (term)"
+   'SnAbbrPos T1 T2 = (TPair (Bind2 true Abbr) T1 T2).
+
+interpretation "negative abbreviation (term)"
+   'SnAbbrNeg T1 T2 = (TPair (Bind2 false Abbr) T1 T2).
+
+interpretation "abstraction (term)"
+   'SnAbst a T1 T2 = (TPair (Bind2 a Abst) T1 T2).
+
+interpretation "positive abstraction (term)"
+   'SnAbstPos T1 T2 = (TPair (Bind2 true Abst) T1 T2).
+
+interpretation "negative abstraction (term)"
+   'SnAbstNeg T1 T2 = (TPair (Bind2 false Abst) T1 T2).
+
+interpretation "application (term)"
+   'SnAppl T1 T2 = (TPair (Flat2 Appl) T1 T2).
+
+interpretation "native type annotation (term)"
+   'SnCast T1 T2 = (TPair (Flat2 Cast) T1 T2).
+
+(* WEIGHT OF A TERM *********************************************************)
+
+include "basic_2/notation/functions/weight_1.ma".
+
+let rec tw T ≝ match T with
+[ TAtom _     ⇒ 1
+| TPair _ V T ⇒ tw V + tw T + 1
+].
+
+interpretation "weight (term)" 'Weight T = (tw T).
+
+(* LOCAL ENVIRONMENTS *******************************************************)
+
+include "basic_2/notation/constructors/star_0.ma".
+include "basic_2/notation/constructors/dxbind2_3.ma".
+include "basic_2/notation/constructors/dxabbr_2.ma".
+include "basic_2/notation/constructors/dxabst_2.ma".
+
+(* local environments *)
+inductive lenv: Type[0] ≝
+| LAtom: lenv                       (* empty *)
+| LPair: lenv → bind2 → term → lenv (* binary binding construction *)
+.
+
+interpretation "sort (local environment)"
+   'Star = LAtom.
+
+interpretation "environment binding construction (binary)"
+   'DxBind2 L I T = (LPair L I T).
+
+interpretation "abbreviation (local environment)"
+   'DxAbbr L T = (LPair L Abbr T).
+
+interpretation "abstraction (local environment)"
+   'DxAbst L T = (LPair L Abst T).
+
+(* WEIGHT OF A LOCAL ENVIRONMENT ********************************************)
+
+let rec lw L ≝ match L with
+[ LAtom       ⇒ 0
+| LPair L _ V ⇒ lw L + ♯{V}
+].
+
+interpretation "weight (local environment)" 'Weight L = (lw L).
+
+(* GLOBAL ENVIRONMENTS ******************************************************)
+
+include "ground_2/list.ma".
+
+(* global environments *)
+definition genv ≝ list2 bind2 term.
+
+interpretation "sort (global environment)"
+   'Star = (nil2 bind2 term).
+
+interpretation "environment binding construction (binary)"
+   'DxBind2 L I T = (cons2 bind2 term I T L).
+
+interpretation "abbreviation (global environment)"
+   'DxAbbr L T = (cons2 bind2 term Abbr T L).
+
+interpretation "abstraction (global environment)"
+   'DxAbst L T = (cons2 bind2 term Abst T L).
+
+(* WEIGHT OF A CLOSURE ******************************************************)
+
+include "basic_2/notation/functions/weight_3.ma".
+
+(* activate genv *)
+definition fw: genv → lenv → term → ? ≝ λG,L,T. ♯{L} + ♯{T}.
+
+interpretation "weight (closure)" 'Weight G L T = (fw G L T).
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: flt_shift *)
+lemma fw_shift: ∀a,I,G,K,V,T. ♯{G, K.ⓑ{I}V, T} < ♯{G, K, ⓑ{a,I}V.T}.
+normalize //
+qed.