machines stuff

a-minimalistic-CEK-machine.agda

module CEK where

open import Function
open import Data.Bool.Base hiding (_≟_)
open import Data.Nat.Base
open import Data.Product
open import Data.List.Base hiding (lookup)
open import Relation.Nullary.Decidable

infixl 5 _·_

postulate undefined : {A : Set} -> A

data Term : Set where
  nat : ℕ -> Term
  var : ℕ -> Term
  lam : ℕ -> Term -> Term
  _·_ : Term -> Term -> Term

data Env : Set where
  layer : (ℕ -> Term × Env) -> Env

data Frame : Set where
  arg : Env -> Term -> Frame
  fun : Env -> Term -> Frame

lookup : ℕ -> Env -> Term × Env
lookup n (layer f) = f n

add : ℕ -> Term -> Env -> Env -> Env
add n t ρ′ ρ = layer $ λ m -> if ⌊ n ≟ m ⌋ then t , ρ′ else lookup m ρ

{-# TERMINATING #-}
ck : List Frame -> Env -> Term -> Term
ck  _                     _   (nat n) = nat n
ck  s                     ρ   (var v) = uncurry (λ x ρ′ -> ck s ρ′ x) $ lookup v ρ
ck  s                     ρ   (f · x) = ck (arg ρ x ∷ s) ρ f
ck (arg ρ₂ x ∷ s)         ρ₁   t      = ck (fun ρ₁ t ∷ s) ρ₂ x
ck (fun ρ₂ (lam n b) ∷ s) ρ₁   x      = ck s (add n x ρ₁ ρ₂) b
ck  _                      _    _      = undefined

S : Term
S = lam 1 $ lam 2 $ lam 3 $ var 1 · var 3 · (var 2 · var 3)

K : Term
K = lam 1 $ lam 2 $ var 1

I : Term
I = lam 1 $ var 1

nf : Term -> Term
nf = ck [] undefined

nat5 : Term
nat5 = nf (S · K · I · nat 5)

a-minimalistic-CK-machine.agda

-- Based on the CK machine from [AUTOMATING ABSTRACT INTERPRETATION OF ABSTRACT MACHINES (2015), James Ian Johnson](https://arxiv.org/pdf/1504.08033.pdf).
module CK where

open import Function
open import Data.Nat.Base
open import Data.List.Base

infixl 5 _·_

{-# NO_POSITIVITY_CHECK #-}
data HOAS : Set where
  lam : (HOAS -> HOAS) -> HOAS
  _·_ : HOAS -> HOAS -> HOAS

data Frame : Set where
  arg : HOAS -> Frame
  fun : HOAS -> Frame

{-# TERMINATING #-}
ck : List Frame -> HOAS -> HOAS
ck  s                (f · x) = ck (arg x ∷ s) f
ck (arg x ∷ s)        t      = ck (fun t ∷ s) x
ck (fun (lam k) ∷ s)  x      = ck s (k x)

-- []          , S K I
-- [_ I]       , S K
-- [_ K, _ I]  , S
-- [S _, _ I]  , K
-- [_ I]       , { S K }
-- [{ S K } _] , I
-- []          , { { S K } I }

-- Computing application is denoted as `{ f x }`.
-- So the idea is that we traverse a spine, collect arguments (which appear in reverse order)
-- in a stack (i.e. they are not reversed anymore) until encounter a variable or a lambda.
-- The state now looks like `(_ x : s) , f` and since `(_ x) f` is the same thing as `(f _) x`
-- and call-by-value computes arguments first, we turn this state into `(f _ : s) , s` and proceed.
-- That's basically it. I wonder how to normalize terms of non-ground types using abstract machines.

a-minimalistic-two-states-CK-machine.agda

-- Based on this rules:

-- s ▹ lam x A M ↦ s ◃ lam x A M
-- s ▹ [M N] ↦ (s , [_ N]) ▹ M

-- (s , [_ N]) ◃ M ↦ (s , [M _]) ▹ N
-- (s, [(lam x A M ) _]) ◃ V ↦ s ▹ [V / x] M
module CK2 where

open import Function
open import Data.Nat.Base
open import Data.List.Base

infixl 5 _·_
infix  4 _▹_ _◃_

{-# NO_POSITIVITY_CHECK #-}
data HOAS : Set where
  lam : (HOAS -> HOAS) -> HOAS
  _·_ : HOAS -> HOAS -> HOAS

data Frame : Set where
  arg : HOAS -> Frame
  fun : HOAS -> Frame

{-# TERMINATING #-}
mutual
  _▹_ : List Frame -> HOAS -> HOAS
  s ▹ f · x = arg x ∷ s ▹ f             -- 1.1
  s ▹ lam k = s ◃ lam k                  -- 1.2

  _◃_ : List Frame -> HOAS -> HOAS
  arg  x      ∷ s ◃ f = fun f ∷ s ▹ x  -- 2.1
  fun (lam k) ∷ s ◃ x = s ▹ k x         -- 2.2

-- []          ▹ S K I         -- by 1.1 to
-- [_ I]       ▹ S K           -- by 1.1 to
-- [_ K, _ I]  ▹ S             -- by 1.2 to
-- [_ K, _ I]  ◃ S          ✓  -- by 2.1 to
-- [S _, _ I]  ▹ K             -- by 1.2 to
-- [S _, _ I]  ◃ K          ✓  -- by 2.2 to
-- [_ I]       ▹ { S K }       -- by 1.2 to
-- [_ I]       ◃ { S K }    ✓  -- by 2.1 to
-- [{ S K } _] ▹ I             -- by 1.2 to
-- [{ S K } _] ◃ I          ✓  -- by 2.2 to
-- []          ▹ { { S K } I }

-- Lines with checkmarks are those not presented in the CK machine's list of states.
-- And those are exactly the same lines that have `_▹_` rather than `_◃_`.
-- So `_▹_` can be simply inlined in this case and we'll get the same CK machine back.
-- There are clauses in Figure 11 that can't be rewritten like that, since `_◃_` is
-- a recursive function, but it's still not clear to me what the semantics of these
-- `_▹_` and `_◃_` are.

CkPrim.agda

module CkPrim where

open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Base
open import Data.List.Base

infixl 5 _·_
infix  4 _▷_ _◁_

{-# NO_POSITIVITY_CHECK #-}
data Hoas : Set where
  nat  : ℕ -> Hoas
  plus : Hoas
  lam  : (Hoas -> Hoas) -> Hoas
  _·_  : Hoas -> Hoas -> Hoas

data Frame : Set where
  arg : Hoas -> Frame
  fun : Hoas -> Frame

postulate
  undefined : {A : Set} -> A

{-# TERMINATING #-}
mutual
  _▷_ : List Frame -> Hoas -> Hoas
  s ▷ f · x = arg x ∷ s ▷ f
  s ▷ term  = s ◁ term

  _◁_ : List Frame -> Hoas -> Hoas
  []        ◁ x = x
  arg x ∷ s ◁ f = fun f ∷ s ▷ x
  fun f ∷ s ◁ x = apply s f x

  apply : List Frame -> Hoas -> Hoas -> Hoas
  apply s (lam k)         x      = s ▷ k x
  apply s  plus           x      = s ◁ plus · x
  apply s (plus · nat x) (nat y) = s ◁ nat (x + y)
  apply s  _              _      = undefined

eval : Hoas -> Hoas
eval = [] ▷_

I : Hoas
I = lam λ x → x

A : Hoas
A = lam λ f → lam λ x → f · x

test : eval (A · (A · plus · nat 3) · (I · nat 5)) ≡ nat 8
test = refl