From 784a534f6d969a261f45396307d0ef30f7fb2be2 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 9 Aug 2013 20:06:52 +0000 Subject: [PATCH] - test.ma on the disambiguation bug moved to ONAG (just out of the way) - lambdadelta: updated interpretation descriptions fix the disambiguation bug --- .../{lambdadelta/basic_2/grammar => ONAG}/test.ma | 0 .../contribs/lambdadelta/basic_2/computation/acp_cr.ma | 1 - .../contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma | 2 +- .../contribs/lambdadelta/basic_2/computation/csn_lift.ma | 2 +- .../contribs/lambdadelta/basic_2/computation/lprs.ma | 2 +- .../contribs/lambdadelta/basic_2/grammar/cl_weight.ma | 2 +- .../matita/contribs/lambdadelta/basic_2/grammar/genv.ma | 2 +- .../matita/contribs/lambdadelta/basic_2/grammar/lenv.ma | 2 +- .../matita/contribs/lambdadelta/basic_2/reduction/lpr.ma | 2 +- .../contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma | 2 +- .../contribs/lambdadelta/basic_2/relocation/ldrop.ma | 2 +- .../contribs/lambdadelta/basic_2/relocation/lift.ma | 2 +- .../matita/contribs/lambdadelta/basic_2/static/lsuba.ma | 2 +- matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma | 8 ++++---- .../contribs/lambdadelta/basic_2/static/ssta_lift.ma | 2 +- .../matita/contribs/lambdadelta/basic_2/unfold/sstas.ma | 2 +- .../matita/contribs/lambdadelta/basic_2/unfold/unfold.ma | 2 +- 17 files changed, 18 insertions(+), 19 deletions(-) rename matita/matita/contribs/{lambdadelta/basic_2/grammar => ONAG}/test.ma (100%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma b/matita/matita/contribs/ONAG/test.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma rename to matita/matita/contribs/ONAG/test.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma index 8c00d3a99..dde5b8ce5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma @@ -14,7 +14,6 @@ include "basic_2/notation/relations/ineint_5.ma". include "basic_2/grammar/aarity.ma". -include "basic_2/grammar/genv.ma". (**) (* not needed, disambiguation error *) include "basic_2/substitution/gr2_gr2.ma". include "basic_2/substitution/lifts_lift_vector.ma". include "basic_2/substitution/ldrops_ldrop.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma index f25909b75..730671630 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) +include "basic_2/reduction/lpx_ldrop.ma". include "basic_2/computation/cpxs_lift.ma". -include "basic_2/reduction/lpx_ldrop.ma". (**) (* disambiguation error *) (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma index 5658ab364..6b52e5b00 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "basic_2/computation/csn.ma". (**) (* disambiguation error *) include "basic_2/reduction/cnx_lift.ma". include "basic_2/computation/acp.ma". +include "basic_2/computation/csn.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma index b1cd89788..6e8431959 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma @@ -13,8 +13,8 @@ (**************************************************************************) include "basic_2/notation/relations/predsnstar_3.ma". -include "basic_2/reduction/lpr.ma". (**) (* disambiguation error *) include "basic_2/grammar/lpx_sn_tc.ma". +include "basic_2/reduction/lpr.ma". (* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) 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 063e7b05e..aa20d64db 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma @@ -13,8 +13,8 @@ (**************************************************************************) 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/genv.ma". (* WEIGHT OF A CLOSURE ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma index 38757ca16..3308b79ed 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma @@ -27,7 +27,7 @@ definition genv ≝ list2 bind2 term. interpretation "sort (global environment)" 'Star = (nil2 bind2 term). -interpretation "environment binding construction (binary)" +interpretation "global environment binding construction (binary)" 'DxBind2 L I T = (cons2 bind2 term I T L). interpretation "abbreviation (global environment)" diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma index a15c5309b..909231ae8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma @@ -29,7 +29,7 @@ inductive lenv: Type[0] ≝ interpretation "sort (local environment)" 'Star = LAtom. -interpretation "environment binding construction (binary)" +interpretation "local environment binding construction (binary)" 'DxBind2 L I T = (LPair L I T). interpretation "abbreviation (local environment)" diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma index 970673d2e..8aab91761 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma @@ -13,8 +13,8 @@ (**************************************************************************) include "basic_2/notation/relations/predsn_3.ma". +include "basic_2/grammar/lpx_sn.ma". include "basic_2/reduction/cpr.ma". -include "basic_2/grammar/lpx_sn.ma". (**) (* disambiguation error *) (* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma index b3e872e40..f23cca2fc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "basic_2/reduction/lpr_ldrop.ma". (**) (* disambiguation error *) include "basic_2/grammar/lpx_sn_lpx_sn.ma". include "basic_2/substitution/fsupp.ma". +include "basic_2/reduction/lpr_ldrop.ma". (* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma index d209bd4b0..6acb2858c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma @@ -20,7 +20,7 @@ include "basic_2/relocation/lift.ma". (* LOCAL ENVIRONMENT SLICING ************************************************) (* Basic_1: includes: drop_skip_bind *) -inductive ldrop: nat → nat → relation lenv ≝ +inductive ldrop: relation4 nat nat lenv lenv ≝ | ldrop_atom : ∀d. ldrop d 0 (⋆) (⋆) | ldrop_pair : ∀L,I,V. ldrop 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V) | ldrop_ldrop: ∀L1,L2,I,V,e. ldrop 0 e L1 L2 → ldrop 0 (e + 1) (L1. ⓑ{I} V) L2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma index e48d22e20..ba117d867 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma @@ -21,7 +21,7 @@ include "basic_2/grammar/term_simple.ma". (* Basic_1: includes: lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat *) -inductive lift: nat → nat → relation term ≝ +inductive lift: relation4 nat nat term term ≝ | lift_sort : ∀k,d,e. lift d e (⋆k) (⋆k) | lift_lref_lt: ∀i,d,e. i < d → lift d e (#i) (#i) | lift_lref_ge: ∀i,d,e. d ≤ i → lift d e (#i) (#(i + e)) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma index c6d4478de..eab0ff035 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma @@ -13,8 +13,8 @@ (**************************************************************************) include "basic_2/notation/relations/lrsubeqa_3.ma". -include "basic_2/static/aaa.ma". (**) (* disambiguation error *) include "basic_2/substitution/lsubr.ma". +include "basic_2/static/aaa.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma index ac9033c53..5bb8b8793 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma @@ -13,14 +13,14 @@ (**************************************************************************) include "basic_2/notation/relations/statictype_7.ma". -include "basic_2/grammar/genv.ma". (**) (* disambiguation error *) +include "basic_2/grammar/genv.ma". include "basic_2/relocation/ldrop.ma". include "basic_2/static/sd.ma". (* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************) (* activate genv *) -inductive ssta (h:sh) (g:sd h): nat → genv → lenv → relation term ≝ +inductive ssta (h:sh) (g:sd h): nat → relation4 genv lenv term term ≝ | ssta_sort: ∀G,L,k,l. deg h g k l → ssta h g l G L (⋆k) (⋆(next h k)) | ssta_ldef: ∀G,L,K,V,W,U,i,l. ⇩[0, i] L ≡ K. ⓓV → ssta h g l G K V W → ⇧[0, i + 1] W ≡ U → ssta h g l G L (#i) U @@ -36,8 +36,8 @@ inductive ssta (h:sh) (g:sd h): nat → genv → lenv → relation term ≝ interpretation "stratified static type assignment (term)" 'StaticType h g G L T U l = (ssta h g l G L T U). -definition ssta_step: ∀h. sd h → genv → lenv → relation term ≝ λh,g,G,L,T,U. - ∃l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄. +definition ssta_step: ∀h. sd h → relation4 genv lenv term term ≝ + λh,g,G,L,T,U. ∃l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄. (* Basic inversion lemmas ************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma index e51c4e805..cf969115d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/static/ssta.ma". (**) (* disambiguation error *) include "basic_2/relocation/ldrop_ldrop.ma". +include "basic_2/static/ssta.ma". (* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma index ce1aea36e..de9ca8b0d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma @@ -18,7 +18,7 @@ include "basic_2/static/ssta.ma". (* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************) (* Note: includes: stass_refl *) -definition sstas: ∀h. sd h → genv → lenv → relation term ≝ +definition sstas: ∀h. sd h → relation4 genv lenv term term ≝ λh,g,G,L. star … (ssta_step h g G L). interpretation "iterated stratified static type assignment (term)" diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma index c44939a33..160c6da76 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/unfold.ma @@ -13,8 +13,8 @@ (**************************************************************************) include "basic_2/notation/relations/unfold_4.ma". -include "basic_2/grammar/genv.ma". (**) (* disambiguation error *) include "basic_2/grammar/lenv_append.ma". +include "basic_2/grammar/genv.ma". include "basic_2/relocation/ldrop.ma". (* CONTEXT-SENSITIVE UNFOLD FOR TERMS ***************************************) -- 2.39.2