module StringSet = Set.Make (String)
type file = {
- ddeps: string list;
- rdeps: StringSet.t option
+ ddeps: string list; (* direct dependences *)
+ rdeps: StringSet.t option (* recursive dependences *)
}
let graph = Hashtbl.create 503
-let rec purge dname bdeps = match bdeps with
- | [] -> bdeps
- | hd :: tl -> if hd = dname then bdeps else purge dname tl
+let debug = ref 0
+
+let rec purge dname vdeps = match vdeps with
+ | [] -> vdeps
+ | hd :: tl -> if hd = dname then tl else hd :: purge dname tl
let add fname =
if Hashtbl.mem graph fname then () else
Hashtbl.replace graph fname {file with ddeps = dname :: file.ddeps}
let init fname dname =
+ if !debug land 1 > 0 then Printf.eprintf "init: %s: %s.\n" fname dname;
add fname; add dname; add_ddep fname dname
-let rec compute bdeps fname file = match file.rdeps with
+(* vdeps: visited dependences for loop detection *)
+let rec compute_from_file vdeps fname file = match file.rdeps with
| Some rdeps -> rdeps
- | None ->
- let bdeps = fname :: bdeps in
- let rdeps = List.fold_left (iter fname bdeps) StringSet.empty file.ddeps in
- Hashtbl.replace graph fname {file with rdeps = Some rdeps};
+ | None ->
+ if !debug land 2 > 0 then Printf.eprintf " compute file: %s\n" fname;
+ let vdeps = fname :: vdeps in
+ List.iter (redundant vdeps fname file.ddeps) file.ddeps;
+ let rdeps = compute_from_ddeps vdeps file.ddeps in
+ Hashtbl.replace graph fname {file with rdeps = Some rdeps};
rdeps
-and iter fname bdeps rdeps dname =
- if StringSet.mem dname rdeps then begin
- Printf.printf "%s: redundant %s\n" fname dname;
- rdeps
- end else if List.mem dname bdeps then begin
- let loop = purge dname (List.rev bdeps) in
+and compute_from_dname vdeps rdeps dname =
+ if List.mem dname vdeps then begin
+ let loop = purge dname (List.rev vdeps) in
Printf.printf "circular: %s\n" (String.concat " " loop);
StringSet.add dname rdeps
end else
let file = Hashtbl.find graph dname in
- StringSet.add dname (StringSet.union (compute bdeps dname file) rdeps)
+ StringSet.add dname (StringSet.union (compute_from_file vdeps dname file) rdeps)
+
+and compute_from_ddeps vdeps ddeps =
+ List.fold_left (compute_from_dname vdeps) StringSet.empty ddeps
+
+and redundant vdeps fname ddeps dname =
+ let rdeps = compute_from_ddeps vdeps (purge dname ddeps) in
+ if StringSet.mem dname rdeps then
+ Printf.printf "%s: redundant %s\n" fname dname
let check () =
- let iter fname file = ignore (compute [] fname file) in
+ let iter fname file = ignore (compute_from_file [] fname file) in
Hashtbl.iter iter graph
let get_unions () =
in
Hashtbl.fold map2 graph (StringSet.empty, StringSet.empty)
+let get_leafs () =
+ let map fname file fnames =
+ if file.ddeps = [] then StringSet.add fname fnames else fnames
+ in
+ Hashtbl.fold map graph StringSet.empty
+
let top () =
- let iter dname = Printf.printf "top: %s\n" dname in
+ let iter fname = Printf.printf "top: %s\n" fname in
let fnames, ddeps = get_unions () in
StringSet.iter iter (StringSet.diff fnames ddeps)
+let leaf () =
+ let iter fname = Printf.printf "leaf: %s\n" fname in
+ let fnames = get_leafs () in
+ StringSet.iter iter fnames
+
let rec read ich =
let _ = Scanf.sscanf (input_line ich) "%s@:include \"%s@\"." init in
read ich
let _ =
+ let show_check = ref false in
let show_top = ref false in
+ let show_leaf = ref false in
let process_file name = () in
+ let show () =
+ if !show_check then check ();
+ if !show_top then top ();
+ if !show_leaf then leaf ()
+ in
let help = "" in
+ let help_c = " Print the redundant and looping arcs of the dependences graph" in
+ let help_d = "<flags> Set these debug options" in
+ let help_l = " Print the leaf nodes of the dependences graph" in
let help_t = " Print the top nodes of the dependences graph" in
Arg.parse [
+ "-c", Arg.Set show_check, help_c;
+ "-d", Arg.Int (fun x -> debug := x), help_d;
+ "-l", Arg.Set show_leaf, help_l;
"-t", Arg.Set show_top, help_t;
] process_file help;
- try read stdin with End_of_file ->
- if !show_top then top () else check ()
+ try read stdin with End_of_file -> show ()
XOA2_TARGETS := ground_2/xoa2_notation.ma ground_2/xoa2.ma
XOA2_OPTS := ../../matita.conf.xml $(XOA2_CONF)
+DEP_INPUT := .depend
DEP_DIR := ../../../components/binaries/matitadep
DEP := matitadep.native
+DEP_OPTS :=
MAC_DIR := ../../../components/binaries/mac
MAC := mac.native
ORIG := . ./orig.sh
ORIGS := basic_2/basic_1.orig
-TAGS := all xoa xoa2 orig elim deps top stats tbls trim
+TAGS := all xoa xoa2 orig elim deps top leaf stats tbls trim
PACKAGES := ground_2 basic_2 apps_2
@echo " ORIG basic_2"
$(H)$(ORIG) basic_2 < $<
+# dep input ##################################################################
+
+$(DEP_INPUT): $(MAS)
+ @echo " GREP include"
+ $(H)grep "include \"" $^ > $(DEP_INPUT)
+
# dep ########################################################################
-deps: $(DEP_DIR)/$(DEP)
- @echo " MATITADEP"
- $(H)grep "include \"" $(MAS) | $<
+deps: $(DEP_INPUT)
+ @echo " MATITADEP -c"
+ $(H)$(DEP_DIR)/$(DEP) -c $(DEP_OPTS) < $<
# top ########################################################################
-top: $(DEP_DIR)/$(DEP)
+top: $(DEP_INPUT)
@echo " MATITADEP -t"
- $(H)grep "include \"" $(MAS) | $< -t
+ $(H)$(DEP_DIR)/$(DEP) -t $(DEP_OPTS) < $<
+
+# leaf #######################################################################
+
+leaf: $(DEP_INPUT)
+ @echo " MATITADEP -l"
+ $(H)$(DEP_DIR)/$(DEP) -l $(DEP_OPTS) < $<
# stats ######################################################################
(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
-(* Main propertis ***********************************************************)
+(* Main properties **********************************************************)
(* Basic_1: was: sc3_arity_csubc *)
theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/notation/relations/fleq_8.ma".
+include "basic_2/computation/lpxs.ma".
+
+(* EQUIVALENT "BIG TREE" NORMAL FORMS ***************************************)
+
+(* Note: this definition works but is not symmetric nor decidable *)
+definition fleq: ∀h. sd h → tri_relation genv lenv term ≝
+ λh,g,G1,L1,T1,G2,L2,T2.
+ ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 & T1 = T2.
+
+interpretation
+ "equivalent 'big tree' normal forms (closure)"
+ 'FLEq h g G1 L1 T1 G2 L2 T2 = (fleq h g G1 L1 T1 G2 L2 T2).
+
+(* Basic_properties *********************************************************)
+
+lemma fleq_refl: ∀h,g. tri_reflexive … (fleq h g).
+/2 width=1 by and3_intro/ qed.
(**************************************************************************)
include "basic_2/computation/fpbs_alt.ma".
-include "basic_2/computation/fpbs_fpbs.ma".
include "basic_2/computation/fpbg.ma".
(* GENERAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************)
/3 width=5 by cpxs_fqup_fpbs, fpbs_trans, lpxs_fpbs, cpxs_fpbs/
qed-.
+lemma fpbg_fwd_fpb_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ →
+ ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2
+[ #L2 #T2 #HT12 #H #HL12
+ elim (cpxs_neq_inv_step_sn … HT12 H) -HT12 -H
+ /4 width=9 by fpbsa_inv_fpbs, fpbc_cpx, ex3_2_intro, ex2_3_intro/
+| #G2 #L #L2 #T #T2 #HT1 #HT2 #HL2 elim (eq_term_dec T1 T) #H destruct
+ [ -HT1 elim (fqup_inv_step_sn … HT2) -HT2
+ /4 width=9 by fpbsa_inv_fpbs, fpbc_fqu, ex3_2_intro, ex2_3_intro/
+ | elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H
+ /5 width=9 by fpbsa_inv_fpbs, fpbc_cpx, fqup_fqus, ex3_2_intro, ex2_3_intro/
+ ]
+]
+qed-.
+
(* Advanced properties ******************************************************)
lemma fqu_fpbs_fpbg: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ →
include "basic_2/computation/fpbg_fpbg.ma".
include "basic_2/computation/fpbr.ma".
-(* RESTRICTED "BIG TREE" ORDER FOR CLOSURES *********************************)
+(* RESTRICTED "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES ***********)
(* Advanced forward lemmas **************************************************)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/reduction/fpbc.ma".
+include "basic_2/computation/fleq.ma".
+include "basic_2/computation/fpbs_alt.ma".
+
+(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
+
+(* Forward lemmas on equivalent "big tree" normal forms *********************)
+
+lemma fpbs_fwd_fpb_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ⋕[h, g] ⦃G2, L2, T2⦄ ∨
+ ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim(fpbs_fpbsa … H) -H
+#L #T #HT1 #HT2 #HL2 elim (eq_term_dec T1 T) #H destruct
+[ -HT1 elim (fqus_inv_gen … HT2) -HT2
+ [ #HT2 elim (fqup_inv_step_sn … HT2) -HT2
+ /5 width=9 by fpbsa_inv_fpbs, fpbc_fqu, ex3_2_intro, ex2_3_intro, or_intror/
+ | * #HG #HL #HT destruct /3 width=1 by and3_intro, or_introl/
+ ]
+| elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H
+ /5 width=9 by fpbsa_inv_fpbs, fpbc_cpx, ex3_2_intro, ex2_3_intro, or_intror/
+]
+qed-.
"'big tree' strong normalization (closure)"
'BTSN h g G L T = (fsb h g G L T).
+(* Basic eliminators ********************************************************)
+
+lemma fsb_ind_alt: ∀h,g. ∀R: relation3 …. (
+ ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h,g] T1 → (
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2
+ ) → R G1 L1 T1
+ ) →
+ ∀G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → R G L T.
+#h #g #R #IH #G #L #T #H elim H -G -L -T
+/4 width=1 by fsb_intro/
+qed-.
+
(* Basic inversion lemmas ***************************************************)
lemma fsb_inv_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
include "basic_2/computation/fpbg.ma".
include "basic_2/computation/fsb.ma".
-(* GENERAL "BIG TREE" STRONGLY NORMALIZING TERMS ****************************)
+(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************)
(* Note: alternative definition of fsb *)
inductive fsba (h) (g): relation3 genv lenv term ≝
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/computation/fpbs_fleq.ma".
+include "basic_2/computation/fpbg_fpbg.ma".
+include "basic_2/computation/fsb.ma".
+
+(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************)
+
+axiom fleq_fpbc_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⋕[h, g] ⦃G, L, T⦄ →
+ ⦃G, L, T⦄ ≻[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄.
+
+axiom fleq_fpbg_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⋕[h, g] ⦃G, L, T⦄ →
+ ⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
+
+(* Properties ******************************************************)
+
+lemma fsb_fleq_trans: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⋕[h, g] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⦥[h, g] T2.
+#h #g #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
+/4 width=5 by fsb_intro, fleq_fpbc_trans/
+qed-.
+
+(* Advanced eliminators *****************************************************)
+
+lemma fsb_ind_fpbg_fpbs: ∀h,g. ∀R:relation3 genv lenv term.
+ (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 →
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ R G1 L1 T1
+ ) →
+ ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2.
+#h #g #R #IH #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
+#G1 #L1 #T1 #H1 #IH1 #G2 #L2 #T2 #H12 elim (fpbs_fwd_fpb_sn … H12) -H12
+[ #H12 @IH -IH /2 width=5 by fsb_fleq_trans/
+ -H1 #G0 #L0 #T0 #H20 lapply (fleq_fpbg_trans … H12 H20) -G2 -L2 -T2
+ #H10 elim (fpbg_fwd_fpb_sn … H10) -H10 /2 width=5 by/
+| -H1 -IH * /2 width=5 by/
+]
+qed-.
--- /dev/null
+include "basic_2/reduction/lpx_ldrop.ma".
+
+lemma lpx_fpbc_trans: ∀h,g,G1,G2,K1,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ≻[h, g] ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #K1 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
+[ #G2 #L2 #T2 #H12 #HKL1 elim (lpx_fqu_trans … H12 … HKL1) -L1
+ /3 width=5 by fpbc_fqu, ex3_2_intro/
+| #T2 #HT12 #H #HKL1
--- /dev/null
+(* alternative proof that needs decidability of bteq to go in fpbs.ma
+ * or lpx_fpbc_trans to go in fpbs_lift.ma (possibly)
+*)
+
+axiom lpx_bteq_trans: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L1⦄ ⊢➡ [h, g] L →
+ ⦃G1, L, T1⦄ ⋕[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⋕[h, g] ⦃G2, L2, T2⦄.
+
+lemma fpbs_fwd_fpb_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, T1⦄ ⋕[h, g] ⦃G2, L2, T2⦄ ∨
+ ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1 [ /2 width=1 by or_introl/ ] (**) (* auto fails without brackets *)
+#G1 #G #L1 #L #T1 #T *
+[ #G0 #L0 #T0 #H #H02 #IH1 elim (fquq_inv_gen … H) -H
+ [ -IH1 /4 width=5 by fpbc_fqu, ex2_3_intro, or_intror/
+ | -H02 * #HG #HL #HT destruct /2 width=1 by/
+ ]
+| #T0 #HT10 #H02 #IH02 elim (eq_term_dec T1 T0) #H destruct
+ [ -H02 /2 width=1 by/
+ | -IH02 /5 width=5 by fpbc_cpx, ex2_3_intro, or_intror/
+ ]
+| #L0 #HL10 #_ * [ /3 width=3 by or_introl, lpx_bteq_trans/ ]
+ * #G3 #L3 #T3 #H13 #H32
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⋕ break [ term 46 h , break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FLEq $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
</news>
<news date="2013 March 16.">
Mutual recursive preservation of stratified native validity
- for hyper computation on closures.
+ for "big tree" computation on closures.
</news>
<news date="2012 October 16.">
Confluence for context-free parallel reduction on closures.
}
]
[ { "strongly normalizing \"big tree\" computation" * } {
- [ "fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )" "fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )" "fsb_csx" * ]
+ [ "fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )" "fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )" "fsb_fleq" + "fsb_csx" * ]
}
]
[ { "strongly normalizing extended computation" * } {
[ { "\"big tree\" parallel computation" * } {
[ "fpbr ( ⦃?,?,?⦄ ⊃≥[?,?] ⦃?,?,?⦄ )" "fpbr_fpbr" * ]
[ "fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpbg" * ]
- [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpbs" * ]
+ [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fleq" + "fpbs_fpbs" * ]
}
]
[ { "decomposed extended computation" * } {
[ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" * ]
}
]
- [ { "global env. slicing" * } {
+ [ { "lazy equivalence for closures" * } {
+ [ "fleq ( ⦃?,?,?⦄ ⋕ ⦃?,?,?⦄ )" "fleq_fleq" * ]
+ }
+ ]
+ [ { "global env. slicing" * } {
[ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ]
}
]
projects / helm.git / commitdiff