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".
18 (* REDUCTION AND TYPE MACHINE ***********************************************)
20 (* machine local environment *)
21 inductive xenv: Type[0] ≝
22 | XAtom: xenv (* empty *)
23 | XQuad: xenv → bind2 → nat → xenv → term → xenv (* entry *)
26 interpretation "atom (ext. local environment)"
29 interpretation "environment construction (quad)"
30 'DxItem4 L I u K V = (XQuad L I u K V).
33 definition stack: Type[0] ≝ list2 xenv term.
37 { rg: genv; (* global environment *)
38 ru: nat; (* current de Bruijn's level *)
39 re: xenv; (* extended local environment *)
40 rs: stack; (* application stack *)
45 definition rtm_i: genv → term → rtm ≝
46 λG,T. mk_rtm G 0 (⋆) (⟠) T.
49 definition rtm_t: rtm → term → rtm ≝
51 [ mk_rtm G u E _ _ ⇒ mk_rtm G u E (⟠) T
55 definition rtm_u: rtm → xenv → term → rtm ≝
57 [ mk_rtm G u _ _ _ ⇒ mk_rtm G u E (⟠) T
60 (* get global environment *)
61 definition rtm_g: rtm → genv ≝
63 [ mk_rtm G _ _ _ _ ⇒ G
66 (* get local reference level *)
67 definition rtm_l: rtm → nat ≝
69 [ mk_rtm _ u E _ _ ⇒ match E with
76 definition rtm_s: rtm → stack ≝
78 [ mk_rtm _ _ _ S _ ⇒ S
82 definition rtm_c: rtm → term ≝
84 [ mk_rtm _ _ _ _ T ⇒ T