matita/matita/contribs/lambdadelta/apps_2/functional/rtm.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 "basic_2/grammar/term_vector.ma".
  16 include "basic_2/grammar/genv.ma".
  17
  18 (* REDUCTION AND TYPE MACHINE ***********************************************)
  19
  20 (* machine local environment *)
  21 inductive xenv: Type[0] ≝
  22 | XAtom: xenv                                    (* empty *)
  23 | XQuad: xenv → bind2 → nat → xenv → term → xenv (* entry *)
  24 .
  25
  26 interpretation "atom (ext. local environment)"
  27    'Star = XAtom.
  28
  29 interpretation "environment construction (quad)"
  30    'DxItem4 L I u K V = (XQuad L I u K V).
  31
  32 (* machine stack *)
  33 definition stack: Type[0] ≝ list2 xenv term.
  34
  35 (* machine status *)
  36 record rtm: Type[0] ≝
  37 { rg: genv;  (* global environment *)
  38   ru: nat;   (* current de Bruijn's level *)
  39   re: xenv;  (* extended local environment *)
  40   rs: stack; (* application stack *)
  41   rt: term   (* code *)
  42 }.
  43
  44 (* initial state *)
  45 definition rtm_i: genv → term → rtm ≝
  46                   λG,T. mk_rtm G 0 (⋆) (⟠) T.
  47
  48 (* update code *)
  49 definition rtm_t: rtm → term → rtm ≝
  50                   λM,T. match M with
  51                   [ mk_rtm G u E _ _ ⇒ mk_rtm G u E (⟠) T
  52                   ].
  53
  54 (* update closure *)
  55 definition rtm_u: rtm → xenv → term → rtm ≝
  56                   λM,E,T. match M with
  57                   [ mk_rtm G u _ _ _ ⇒ mk_rtm G u E (⟠) T
  58                   ].
  59
  60 (* get global environment *)
  61 definition rtm_g: rtm → genv ≝
  62                   λM. match M with
  63                   [ mk_rtm G _ _ _ _ ⇒ G
  64                   ].
  65
  66 (* get local reference level *)
  67 definition rtm_l: rtm → nat ≝
  68                   λM. match M with
  69                   [ mk_rtm _ u E _ _ ⇒ match E with
  70                      [ XAtom           ⇒ u
  71                      | XQuad _ _ u _ _ ⇒ u
  72                      ]
  73                   ].
  74
  75 (* get stack *)
  76 definition rtm_s: rtm → stack ≝
  77                   λM. match M with
  78                   [ mk_rtm _ _ _ S _ ⇒ S
  79                   ].
  80
  81 (* get code *)
  82 definition rtm_c: rtm → term ≝
  83                   λM. match M with
  84                   [ mk_rtm _ _ _ _ T ⇒ T
  85                   ].