From: Ferruccio Guidi Date: Fri, 9 Aug 2013 20:06:52 +0000 (+0000) Subject: - test.ma on the disambiguation bug moved to ONAG (just out of the way) X-Git-Tag: make_still_working~1110 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=784a534f6d969a261f45396307d0ef30f7fb2be2;p=helm.git - test.ma on the disambiguation bug moved to ONAG (just out of the way) - lambdadelta: updated interpretation descriptions fix the disambiguation bug --- diff --git a/matita/matita/contribs/ONAG/test.ma b/matita/matita/contribs/ONAG/test.ma new file mode 100644 index 000000000..1f4fac570 --- /dev/null +++ b/matita/matita/contribs/ONAG/test.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +universe constraint Type[0] < Type[1]. + +notation "hvbox(a break \to b)" + right associative with precedence 20 +for @{ \forall $_:$a.$b }. + +notation "hvbox( * )" + non associative with precedence 90 + for @{ 'B }. + +inductive l: Type[0] ≝ L: l. + +inductive g: Type[0] ≝ G: g. + +axiom f: l → Prop. + +interpretation "b" 'B = L. + +interpretation "b" 'B = G. + +(* FG: two interpretations of the same notation and with the same description + override eachother, so the description is not just informative +*) + +axiom s: f *. 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/grammar/test.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma deleted file mode 100644 index 1f4fac570..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma +++ /dev/null @@ -1,39 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -universe constraint Type[0] < Type[1]. - -notation "hvbox(a break \to b)" - right associative with precedence 20 -for @{ \forall $_:$a.$b }. - -notation "hvbox( * )" - non associative with precedence 90 - for @{ 'B }. - -inductive l: Type[0] ≝ L: l. - -inductive g: Type[0] ≝ G: g. - -axiom f: l → Prop. - -interpretation "b" 'B = L. - -interpretation "b" 'B = G. - -(* FG: two interpretations of the same notation and with the same description - override eachother, so the description is not just informative -*) - -axiom s: f *. 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 ***************************************)