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