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 "basic_2/grammar/term_vector.ma".
16 include "basic_2/grammar/genv.ma".
17 include "apps_2/functional/notation.ma".
19 (* REDUCTION AND TYPE MACHINE ***********************************************)
21 (* machine local environment *)
22 inductive xenv: Type[0] ≝
23 | XAtom: xenv (* empty *)
24 | XQuad: xenv → bind2 → nat → xenv → term → xenv (* entry *)
27 interpretation "atom (ext. local environment)"
30 interpretation "environment construction (quad)"
31 'DxItem4 L I u K V = (XQuad L I u K V).
34 definition stack: Type[0] ≝ list2 xenv term.
38 { rg: genv; (* global environment *)
39 ru: nat; (* current de Bruijn's level *)
40 re: xenv; (* extended local environment *)
41 rs: stack; (* application stack *)
46 definition rtm_i: genv → term → rtm ≝
47 λG,T. mk_rtm G 0 (⋆) (◊) T.
50 definition rtm_t: rtm → term → rtm ≝
52 [ mk_rtm G u E _ _ ⇒ mk_rtm G u E (◊) T
56 definition rtm_u: rtm → xenv → term → rtm ≝
58 [ mk_rtm G u _ _ _ ⇒ mk_rtm G u E (◊) T
61 (* get global environment *)
62 definition rtm_g: rtm → genv ≝
64 [ mk_rtm G _ _ _ _ ⇒ G
67 (* get local reference level *)
68 definition rtm_l: rtm → nat ≝
70 [ mk_rtm _ u E _ _ ⇒ match E with
77 definition rtm_s: rtm → stack ≝
79 [ mk_rtm _ _ _ S _ ⇒ S
83 definition rtm_c: rtm → term ≝
85 [ mk_rtm _ _ _ _ T ⇒ T