(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "basic_2/syntax/term_vector.ma".
include "basic_2/syntax/genv.ma".
include "apps_2/functional/notation.ma".

(* REDUCTION AND TYPE MACHINE ***********************************************)

(* machine local environment *)
inductive xenv: Type[0] ≝
| XAtom: xenv                                    (* empty *)
| XQuad: xenv → bind2 → nat → xenv → term → xenv (* entry *)
.

interpretation "atom (ext. local environment)"
   'Star = XAtom.

interpretation "environment construction (quad)"
   'DxItem4 L I u K V = (XQuad L I u K V).

(* machine stack *)
definition stack: Type[0] ≝ list2 xenv term.

(* machine status *)
record rtm: Type[0] ≝
{ rg: genv;  (* global environment *)
  ru: nat;   (* current de Bruijn's level *)
  re: xenv;  (* extended local environment *)
  rs: stack; (* application stack *)
  rt: term   (* code *)
}.

(* initial state *)
definition rtm_i: genv → term → rtm ≝
                  λG,T. mk_rtm G 0 (⋆) (Ⓔ) T.

(* update code *)
definition rtm_t: rtm → term → rtm ≝
                  λM,T. match M with
                  [ mk_rtm G u E _ _ ⇒ mk_rtm G u E (Ⓔ) T
                  ].

(* update closure *)
definition rtm_u: rtm → xenv → term → rtm ≝
                  λM,E,T. match M with
                  [ mk_rtm G u _ _ _ ⇒ mk_rtm G u E (Ⓔ) T
                  ].

(* get global environment *)
definition rtm_g: rtm → genv ≝
                  λM. match M with
                  [ mk_rtm G _ _ _ _ ⇒ G
                  ].

(* get local reference level *)
definition rtm_l: rtm → nat ≝
                  λM. match M with
                  [ mk_rtm _ u E _ _ ⇒ match E with
                     [ XAtom           ⇒ u
                     | XQuad _ _ u _ _ ⇒ u
                     ]
                  ].

(* get stack *)
definition rtm_s: rtm → stack ≝
                  λM. match M with
                  [ mk_rtm _ _ _ S _ ⇒ S
                  ].

(* get code *)
definition rtm_c: rtm → term ≝
                  λM. match M with
                  [ mk_rtm _ _ _ _ T ⇒ T
                  ].