1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground_2/arith.ma".
17 (* 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 *)
26 (* binary binding items *)
27 inductive bind2: Type[0] ≝
28 | Abbr: bind2 (* abbreviation *)
29 | Abst: bind2 (* abstraction *)
32 (* binary non-binding items *)
33 inductive flat2: Type[0] ≝
34 | Appl: flat2 (* application *)
35 | Cast: flat2 (* explicit type annotation *)
39 inductive item2: Type[0] ≝
40 | Bind2: bool → bind2 → item2 (* polarized binding item *)
41 | Flat2: flat2 → item2 (* non-binding item *)
44 (* TERMS ********************************************************************)
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".
66 inductive term: Type[0] ≝
67 | TAtom: item0 → term (* atomic item construction *)
68 | TPair: item2 → term → term → term (* binary item construction *)
71 interpretation "term construction (atomic)"
74 interpretation "term construction (binary)"
75 'SnItem2 I T1 T2 = (TPair I T1 T2).
77 interpretation "term binding construction (binary)"
78 'SnBind2 a I T1 T2 = (TPair (Bind2 a I) T1 T2).
80 interpretation "term positive binding construction (binary)"
81 'SnBind2Pos I T1 T2 = (TPair (Bind2 true I) T1 T2).
83 interpretation "term negative binding construction (binary)"
84 'SnBind2Neg I T1 T2 = (TPair (Bind2 false I) T1 T2).
86 interpretation "term flat construction (binary)"
87 'SnFlat2 I T1 T2 = (TPair (Flat2 I) T1 T2).
89 interpretation "sort (term)"
90 'Star k = (TAtom (Sort k)).
92 interpretation "local reference (term)"
93 'LRef i = (TAtom (LRef i)).
95 interpretation "global reference (term)"
96 'GRef p = (TAtom (GRef p)).
98 interpretation "abbreviation (term)"
99 'SnAbbr a T1 T2 = (TPair (Bind2 a Abbr) T1 T2).
101 interpretation "positive abbreviation (term)"
102 'SnAbbrPos T1 T2 = (TPair (Bind2 true Abbr) T1 T2).
104 interpretation "negative abbreviation (term)"
105 'SnAbbrNeg T1 T2 = (TPair (Bind2 false Abbr) T1 T2).
107 interpretation "abstraction (term)"
108 'SnAbst a T1 T2 = (TPair (Bind2 a Abst) T1 T2).
110 interpretation "positive abstraction (term)"
111 'SnAbstPos T1 T2 = (TPair (Bind2 true Abst) T1 T2).
113 interpretation "negative abstraction (term)"
114 'SnAbstNeg T1 T2 = (TPair (Bind2 false Abst) T1 T2).
116 interpretation "application (term)"
117 'SnAppl T1 T2 = (TPair (Flat2 Appl) T1 T2).
119 interpretation "native type annotation (term)"
120 'SnCast T1 T2 = (TPair (Flat2 Cast) T1 T2).
122 (* WEIGHT OF A TERM *********************************************************)
124 include "basic_2/notation/functions/weight_1.ma".
126 let rec tw T ≝ match T with
128 | TPair _ V T ⇒ tw V + tw T + 1
131 interpretation "weight (term)" 'Weight T = (tw T).
133 (* LOCAL ENVIRONMENTS *******************************************************)
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".
140 (* local environments *)
141 inductive lenv: Type[0] ≝
142 | LAtom: lenv (* empty *)
143 | LPair: lenv → bind2 → term → lenv (* binary binding construction *)
146 interpretation "sort (local environment)"
149 interpretation "environment binding construction (binary)"
150 'DxBind2 L I T = (LPair L I T).
152 interpretation "abbreviation (local environment)"
153 'DxAbbr L T = (LPair L Abbr T).
155 interpretation "abstraction (local environment)"
156 'DxAbst L T = (LPair L Abst T).
158 (* WEIGHT OF A LOCAL ENVIRONMENT ********************************************)
160 let rec lw L ≝ match L with
162 | LPair L _ V ⇒ lw L + ♯{V}
165 interpretation "weight (local environment)" 'Weight L = (lw L).
167 (* GLOBAL ENVIRONMENTS ******************************************************)
169 include "ground_2/list.ma".
171 (* global environments *)
172 definition genv ≝ list2 bind2 term.
174 interpretation "sort (global environment)"
175 'Star = (nil2 bind2 term).
177 interpretation "environment binding construction (binary)"
178 'DxBind2 L I T = (cons2 bind2 term I T L).
180 interpretation "abbreviation (global environment)"
181 'DxAbbr L T = (cons2 bind2 term Abbr T L).
183 interpretation "abstraction (global environment)"
184 'DxAbst L T = (cons2 bind2 term Abst T L).
186 (* WEIGHT OF A CLOSURE ******************************************************)
188 include "basic_2/notation/functions/weight_3.ma".
191 definition fw: genv → lenv → term → ? ≝ λG,L,T. ♯{L} + ♯{T}.
193 interpretation "weight (closure)" 'Weight G L T = (fw G L T).
195 (* Basic properties *********************************************************)
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}.