matita/matita/contribs/lambdadelta/basic_2/grammar/test.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "ground_2/arith.ma".
  16
  17 (* ITEMS ********************************************************************)
  18
  19 (* atomic items *)
  20 inductive item0: Type[0] ≝
  21    | Sort: nat → item0 (* sort: starting at 0 *)
  22    | LRef: nat → item0 (* reference by index: starting at 0 *)
  23    | GRef: nat → item0 (* reference by position: starting at 0 *)
  24 .
  25
  26 (* binary binding items *)
  27 inductive bind2: Type[0] ≝
  28   | Abbr: bind2 (* abbreviation *)
  29   | Abst: bind2 (* abstraction *)
  30 .
  31
  32 (* binary non-binding items *)
  33 inductive flat2: Type[0] ≝
  34   | Appl: flat2 (* application *)
  35   | Cast: flat2 (* explicit type annotation *)
  36 .
  37
  38 (* binary items *)
  39 inductive item2: Type[0] ≝
  40   | Bind2: bool → bind2 → item2 (* polarized binding item *)
  41   | Flat2: flat2 → item2        (* non-binding item *)
  42 .
  43
  44 (* TERMS ********************************************************************)
  45
  46 include "basic_2/notation/constructors/item0_1.ma".
  47 include "basic_2/notation/constructors/snitem2_3.ma".
  48 include "basic_2/notation/constructors/snbind2_4.ma".
  49 include "basic_2/notation/constructors/snbind2pos_3.ma".
  50 include "basic_2/notation/constructors/snbind2neg_3.ma".
  51 include "basic_2/notation/constructors/snflat2_3.ma".
  52 include "basic_2/notation/constructors/star_1.ma".
  53 include "basic_2/notation/constructors/lref_1.ma".
  54 include "basic_2/notation/constructors/gref_1.ma".
  55 include "basic_2/notation/constructors/snabbr_3.ma".
  56 include "basic_2/notation/constructors/snabbrpos_2.ma".
  57 include "basic_2/notation/constructors/snabbrneg_2.ma".
  58 include "basic_2/notation/constructors/snabst_3.ma".
  59 include "basic_2/notation/constructors/snabstpos_2.ma".
  60 include "basic_2/notation/constructors/snabstneg_2.ma".
  61 include "basic_2/notation/constructors/snappl_2.ma".
  62 include "basic_2/notation/constructors/sncast_2.ma".
  63 include "basic_2/grammar/item.ma".
  64
  65 (* terms *)
  66 inductive term: Type[0] ≝
  67   | TAtom: item0 → term               (* atomic item construction *)
  68   | TPair: item2 → term → term → term (* binary item construction *)
  69 .
  70
  71 interpretation "term construction (atomic)"
  72    'Item0 I = (TAtom I).
  73
  74 interpretation "term construction (binary)"
  75    'SnItem2 I T1 T2 = (TPair I T1 T2).
  76
  77 interpretation "term binding construction (binary)"
  78    'SnBind2 a I T1 T2 = (TPair (Bind2 a I) T1 T2).
  79
  80 interpretation "term positive binding construction (binary)"
  81    'SnBind2Pos I T1 T2 = (TPair (Bind2 true I) T1 T2).
  82
  83 interpretation "term negative binding construction (binary)"
  84    'SnBind2Neg I T1 T2 = (TPair (Bind2 false I) T1 T2).
  85
  86 interpretation "term flat construction (binary)"
  87    'SnFlat2 I T1 T2 = (TPair (Flat2 I) T1 T2).
  88
  89 interpretation "sort (term)"
  90    'Star k = (TAtom (Sort k)).
  91
  92 interpretation "local reference (term)"
  93    'LRef i = (TAtom (LRef i)).
  94
  95 interpretation "global reference (term)"
  96    'GRef p = (TAtom (GRef p)).
  97
  98 interpretation "abbreviation (term)"
  99    'SnAbbr a T1 T2 = (TPair (Bind2 a Abbr) T1 T2).
 100
 101 interpretation "positive abbreviation (term)"
 102    'SnAbbrPos T1 T2 = (TPair (Bind2 true Abbr) T1 T2).
 103
 104 interpretation "negative abbreviation (term)"
 105    'SnAbbrNeg T1 T2 = (TPair (Bind2 false Abbr) T1 T2).
 106
 107 interpretation "abstraction (term)"
 108    'SnAbst a T1 T2 = (TPair (Bind2 a Abst) T1 T2).
 109
 110 interpretation "positive abstraction (term)"
 111    'SnAbstPos T1 T2 = (TPair (Bind2 true Abst) T1 T2).
 112
 113 interpretation "negative abstraction (term)"
 114    'SnAbstNeg T1 T2 = (TPair (Bind2 false Abst) T1 T2).
 115
 116 interpretation "application (term)"
 117    'SnAppl T1 T2 = (TPair (Flat2 Appl) T1 T2).
 118
 119 interpretation "native type annotation (term)"
 120    'SnCast T1 T2 = (TPair (Flat2 Cast) T1 T2).
 121
 122 (* WEIGHT OF A TERM *********************************************************)
 123
 124 include "basic_2/notation/functions/weight_1.ma".
 125
 126 let rec tw T ≝ match T with
 127 [ TAtom _     ⇒ 1
 128 | TPair _ V T ⇒ tw V + tw T + 1
 129 ].
 130
 131 interpretation "weight (term)" 'Weight T = (tw T).
 132
 133 (* LOCAL ENVIRONMENTS *******************************************************)
 134
 135 include "basic_2/notation/constructors/star_0.ma".
 136 include "basic_2/notation/constructors/dxbind2_3.ma".
 137 include "basic_2/notation/constructors/dxabbr_2.ma".
 138 include "basic_2/notation/constructors/dxabst_2.ma".
 139
 140 (* local environments *)
 141 inductive lenv: Type[0] ≝
 142 | LAtom: lenv                       (* empty *)
 143 | LPair: lenv → bind2 → term → lenv (* binary binding construction *)
 144 .
 145
 146 interpretation "sort (local environment)"
 147    'Star = LAtom.
 148
 149 interpretation "environment binding construction (binary)"
 150    'DxBind2 L I T = (LPair L I T).
 151
 152 interpretation "abbreviation (local environment)"
 153    'DxAbbr L T = (LPair L Abbr T).
 154
 155 interpretation "abstraction (local environment)"
 156    'DxAbst L T = (LPair L Abst T).
 157
 158 (* WEIGHT OF A LOCAL ENVIRONMENT ********************************************)
 159
 160 let rec lw L ≝ match L with
 161 [ LAtom       ⇒ 0
 162 | LPair L _ V ⇒ lw L + ♯{V}
 163 ].
 164
 165 interpretation "weight (local environment)" 'Weight L = (lw L).
 166
 167 (* GLOBAL ENVIRONMENTS ******************************************************)
 168
 169 include "ground_2/list.ma".
 170
 171 (* global environments *)
 172 definition genv ≝ list2 bind2 term.
 173
 174 interpretation "sort (global environment)"
 175    'Star = (nil2 bind2 term).
 176
 177 interpretation "environment binding construction (binary)"
 178    'DxBind2 L I T = (cons2 bind2 term I T L).
 179
 180 interpretation "abbreviation (global environment)"
 181    'DxAbbr L T = (cons2 bind2 term Abbr T L).
 182
 183 interpretation "abstraction (global environment)"
 184    'DxAbst L T = (cons2 bind2 term Abst T L).
 185
 186 (* WEIGHT OF A CLOSURE ******************************************************)
 187
 188 include "basic_2/notation/functions/weight_3.ma".
 189
 190 (* activate genv *)
 191 definition fw: genv → lenv → term → ? ≝ λG,L,T. ♯{L} + ♯{T}.
 192
 193 interpretation "weight (closure)" 'Weight G L T = (fw G L T).
 194
 195 (* Basic properties *********************************************************)
 196
 197 (* Basic_1: was: flt_shift *)
 198 lemma fw_shift: ∀a,I,G,K,V,T. ♯{G, K.ⓑ{I}V, T} < ♯{G, K, ⓑ{a,I}V.T}.
 199 normalize //
 200 qed.