From: Ferruccio Guidi Date: Fri, 9 Aug 2013 16:13:09 +0000 (+0000) Subject: riduced example showing disambiguation bug ... X-Git-Tag: make_still_working~1113 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=260c699033d4ec65a3e4ab0f591a2109a5a831ad;p=helm.git riduced example showing disambiguation bug ... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma index 806d3537c..1a5d4844c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma @@ -12,189 +12,90 @@ (* *) (**************************************************************************) -include "ground_2/arith.ma". +include "arithmetics/nat.ma". + +(* notations ****************************************************************) + +include "basic_2/notation/constructors/snbind2_4.ma". +include "basic_2/notation/constructors/dxbind2_3.ma". +include "basic_2/notation/functions/weight_1.ma". +include "basic_2/notation/functions/weight_3.ma". + +(* definitions **************************************************************) + +inductive list2 (A1,A2:Type[0]) : Type[0] := + | nil2 : list2 A1 A2 + | cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2. -(* 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 *) + | Sort: nat → item0 + | LRef: nat → item0 + | GRef: nat → item0 . -(* binary binding items *) inductive bind2: Type[0] ≝ - | Abbr: bind2 (* abbreviation *) - | Abst: bind2 (* abstraction *) + | Abbr: bind2 + | Abst: bind2 . -(* binary non-binding items *) inductive flat2: Type[0] ≝ - | Appl: flat2 (* application *) - | Cast: flat2 (* explicit type annotation *) + | Appl: flat2 + | Cast: flat2 . -(* binary items *) inductive item2: Type[0] ≝ - | Bind2: bool → bind2 → item2 (* polarized binding item *) - | Flat2: flat2 → item2 (* non-binding item *) + | Bind2: bool → bind2 → item2 + | Flat2: flat2 → item2 . -(* 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 *) + | TAtom: item0 → term + | TPair: item2 → term → term → term . -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 *) +| LAtom: lenv +| LPair: lenv → bind2 → term → lenv . -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} +| LPair L _ V ⇒ lw L + tw V ]. -interpretation "weight (local environment)" 'Weight L = (lw L). - -(* GLOBAL ENVIRONMENTS ******************************************************) +definition genv ≝ list2 bind2 term. -include "ground_2/list.ma". +definition fw: genv → lenv → term → ? ≝ λG,L,T. (lw L) + (tw T). -(* global environments *) -definition genv ≝ list2 bind2 term. +(* interpretations **********************************************************) -interpretation "sort (global environment)" - 'Star = (nil2 bind2 term). +interpretation "term binding construction (binary)" + 'SnBind2 a I T1 T2 = (TPair (Bind2 a I) T1 T2). -interpretation "environment binding construction (binary)" - 'DxBind2 L I T = (cons2 bind2 term I T L). +interpretation "weight (term)" 'Weight T = (tw T). -interpretation "abbreviation (global environment)" - 'DxAbbr L T = (cons2 bind2 term Abbr T L). +interpretation "weight (local environment)" 'Weight L = (lw L). -interpretation "abstraction (global environment)" - 'DxAbst L T = (cons2 bind2 term Abst T L). +interpretation "weight (closure)" 'Weight G L T = (fw G L T). -(* WEIGHT OF A CLOSURE ******************************************************) +(* first set *) -include "basic_2/notation/functions/weight_3.ma". +interpretation "environment binding construction (binary)" + 'DxBind2 L I T = (LPair L I T). -(* activate genv *) -definition fw: genv → lenv → term → ? ≝ λG,L,T. ♯{L} + ♯{T}. +(* second set *) -interpretation "weight (closure)" 'Weight G L T = (fw G L T). +interpretation "environment binding construction (binary)" + 'DxBind2 L I T = (cons2 bind2 term I T L). -(* Basic properties *********************************************************) +(* statements ***************************************************************) -(* 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.