iwilare

data Lam
  = Abs Lam
  | App Lam Lam
  | Var Int

data Stack = S [(Lam, Stack)]

krivine (App a b, S e, S s)     = krivine (a, S e, S ((b, S e):s))
krivine (Abs t,   S e, S (c:s)) = krivine (t, S (c:e), S s)
krivine (Var n,   S e, S s)     = krivine (fst (e !! n), snd (e !! n), S s)

iwilare

// 1-index De Bruijn, [0,n] abstraction, [f,x] application
let repr1 = [0, [[1, [0, [0, [0, [[3, 1], [2, 1]]]]]], [0, [0, 2]]]]
// 1-index De Bruijn, {f:, x:} application, {λ:} abstraction
let repr2 = {λ:       {f: {f: 1, x: {λ:       {λ:       {λ:       {f: {f: 3, x: 1}, x: {f: 2, x: 1}}}}}}, x: {λ:       {λ:       2}}}}
// Named,             {f:, x:} application, {λ:, b:} abstraction
let repr3 = {λ: 1, b: {f: {f: 1, x: {λ: 2, b: {λ: 3, b: {λ: 4, b: {f: {f: 2, x: 4}, x: {f: 3, x: 4}}}}}}, x: {λ: 2, b: {λ: 3, b: 2}}}}
// 0-index De Bruijn, {f:, x:} application, {λ:} abstraction
let reprN = {λ:       {f: {f: 0, x: {λ:       {λ:       {λ:       {f: {f: 2, x: 0}, x: {f: 1, x: 0}}}}}}, x: {λ:       {λ:       1}}}}
// 0-index De Bruijn, {t:1, f:, x:} application, {t:0, λ:} abstraction
let repr4 = {t:0,λ: {t:1,f: {t:1,f: 0, x: {t:0,λ: {t:0,λ: {t:0,λ: {t:1,f: {t:1,f: 2, x: 0}, x: {t:1,f: 1, x: 0}}}}}}, x: {t:0,λ: {t:0,λ: 1}}}}

iwilare

E=([a,b],Γ=[])=>b?a?E(a,Γ)(E(b,Γ)):x=>E(b,[x,...Γ]):Γ[a] 

iwilare

Keybase proof

I hereby claim:

• I am iwilare on github.
• I am iwilare (https://keybase.io/iwilare) on keybase.
• I have a public key ASDBYl3y4-9VLMf8M4sTLR57d97YndrcHh09apOae5rbuwo

To claim this, I am signing this object: