Documentation

MIPRE.TM.Interp.Repr

The tape representation of configurations #

Values as their preorder bits (S), the control (ctrlRepr), the environment (envRepr, innermost value at the right end, #-separated), the frames (frameRepr) and the stack (kontRepr), as lists of symbols; and their lengths in terms of the sizes.

source
def MIPRE.TM.Interp.S (v : Cost.Data) :
List Sym

A value: its preorder bits.

Equations
Instances For
    source
    @[simp]
    theorem MIPRE.TM.Interp.S_nil :
    S Cost.Data.nil = [Sym.zero]
    source
    theorem MIPRE.TM.Interp.S_cons (a b : Cost.Data) :
    S (a.cons b) = Sym.one :: (S a ++ S b)
    source
    @[simp]
    theorem MIPRE.TM.Interp.length_S (v : Cost.Data) :
    (S v).length = v.size
    source
    theorem MIPRE.TM.Interp.mem_S (v : Cost.Data) (s : Sym) :
    s ∈ S v → s = Sym.zero ∨ s = Sym.one

    The symbols of a value are bits.

    source
    def MIPRE.TM.Interp.ctrlRepr :
    Cost.Machine.Ctrl → List Sym

    The control: 0 · S(p.toData) for ev p, 1 · S(v) for ret v.

    Equations
    Instances For
      source
      def MIPRE.TM.Interp.envRepr :
      Cost.Env → List Sym

      The environment [v₁, …, vₙ] (v₁ innermost): S(vₙ) # … # S(v₁) #.

      Equations
      Instances For
        source
        @[simp]
        theorem MIPRE.TM.Interp.envRepr_nil :
        envRepr [] = []
        source
        @[simp]
        theorem MIPRE.TM.Interp.envRepr_cons (v : Cost.Data) (env : Cost.Env) :
        envRepr (v :: env) = envRepr env ++ S v ++ [Sym.sep]
        source
        theorem MIPRE.TM.Interp.length_envRepr (env : Cost.Env) :
        (envRepr env).length = (List.map Cost.Data.size env).sum + List.length env
        source
        theorem MIPRE.TM.Interp.mem_envRepr (env : Cost.Env) (s : Sym) :
        s ∈ envRepr env → s ≠ Sym.fr ∧ s ≠ Sym.en

        No $ and no in an environment.

        source
        def MIPRE.TM.Interp.frameTag :
        Cost.Machine.Frame → List Sym

        The two tag bits of a frame.

        Equations
        Instances For
          source
          def MIPRE.TM.Interp.frameRepr :
          Cost.Machine.Frame → List Sym

          A frame: its tag, its payload, $; a closure carries its environment after .

          Equations
          Instances For
            source
            def MIPRE.TM.Interp.frameBody :
            Cost.Machine.Frame → List Sym

            The body of a frame: the frame without its final $.

            Equations
            Instances For
              source
              theorem MIPRE.TM.Interp.frameRepr_eq (f : Cost.Machine.Frame) :
              frameRepr f = frameBody f ++ [Sym.fr]
              source
              theorem MIPRE.TM.Interp.mem_frameBody (f : Cost.Machine.Frame) (s : Sym) :
              s ∈ frameBody f → s ≠ Sym.fr

              No $ in the body of a frame.

              source
              def MIPRE.TM.Interp.kontRepr :
              List Cost.Machine.Frame → List Sym

              The stack [f₁, …, fₘ] (f₁ the top): frameRepr fₘ ++ … ++ frameRepr f₁.

              Equations
              Instances For
                source
                @[simp]
                theorem MIPRE.TM.Interp.kontRepr_nil :
                kontRepr [] = []
                source
                @[simp]
                theorem MIPRE.TM.Interp.kontRepr_cons (f : Cost.Machine.Frame) (k : List Cost.Machine.Frame) :
                kontRepr (f :: k) = kontRepr k ++ frameRepr f
                source
                theorem MIPRE.TM.Interp.length_frameRepr_le {V L P : ℕ} {f : Cost.Machine.Frame} (h : Cost.Machine.FrameBound V L P f) :
                (frameRepr f).length ≤ V + P + L * V + L + 4