This section is mostly copied from Wikiedia: Normalization by evaluation
datatype ty = Basic of string
| Arrow of ty * ty
| Prod of ty * ty
s,t,... ::= var x | lam (x, t) | app (s, t) | pair (s, t) | fst | snd t
datatype tm = var of string
| lam of string * tm | app of tm * tm
| pair of tm * tm | fst of tm | snd of tm
datatype sem = LAM of (sem -> sem)
| PAIR of sem * sem
| SYN of tm
(* reflect : ty -> tm -> sem *)
fun reflect (Arrow (a, b)) t =
LAM (fn S => reflect b (app t (reify a S)))
| reflect (Prod (a, b)) t =
PAIR (reflect a (fst t)) (reflect b (snd t))
| reflect (Basic _) t =
SYN t
(* reify : ty -> sem -> tm *)
fun reify (Arrow (a, b)) (LAM S) =
let x = fresh_var () in
Lam (x, reify b (S (reflect a (var x))))
| reify (Prod (a, b)) (PAIR S T) =
Pair (reify a S, reify b T)
| reify (Basic _) (SYN t) = t
(* meaning : ctx -> tm -> sem *)
fun meaning G t =
case t of
var x =>
lookup G x
| lam (x, s) =>
LAM (fn S => meaning (add G (x, S)) s)
| app (s, t) => (case meaning G s of LAM S => S (meaning G t))
| pair (s, t) => PAIR (meaning G s, meaning G t)
| fst s => (case meaning G s of PAIR (S, T) => S)
| snd t => (case meaning G t of PAIR (S, T) => T)
The Base.lift function implements the reify operation, which in
this case converts a semantic value to some syntax that will construct the same value.
Numeric constant values Cst(n) are turned into numeric literal expressions
Lit(n). String values Strn(s) are converted to symbols
Sym(s) (evalms evaluats symbols to strings, variables are not symbols).
Since variables are not values they are not mentioned in lift.
The conversion of Clo (closures) is more complex. The
collapsing towers extract below also implements memoization of the resulting lambda
term for any closure. I beleive it searches stFun for elements that have equal environment and body expression using collectFirst, If it finds a match it extracts n from the element and executes the case Some(n) clause. This clause only emits a variable referencing the existing lambda term.
If no matching entry in stFun is found it will execute the case None
clause. This will in turn a store the a new element in stFun containing the fresh n together with the closure environment and expression in stFun. The stFun variable is only used by Base.lift for relating closures to memoized lambda terms.
def lift(v: Val): Exp = v match {
case Cst(n) =>
Lit(N)
case Tup(a,b) =>
val (Code(u),Code(v)) = (a,b)
reflect(Cons(u,v))
case Clo(env2,e2) =>
stFun collectFirst { case (n `env2`, `e2`) => n } match {
case Some(n) =>
Var(n)
case None =>
stFun :+= (stFresh, env2, e2)
reflect(Lam(reify{
val Code(r) = evalms(env2:+Code(fresh()):+Code(fresh()),e2);
r}))
}
case Code(e) =>
reflect(Lift(e))
def run[A](f: => A): A = {
val sF = stFresh
val sB = stBlock
val sN = stFun
try f finally {
stFresh = sF;
stBlock = sB;
stFun = sN
}
}
def reify(f: => Exp) = run {
stBlock = Nil
val last = f
(stBlock foldRight last)(Let)
}
def reifyc(f: => Val) = reify { val Code(e) = f; e }
def reflectc(s: Exp) = Code(reflect(s))
def reifyv(f: => Val) = run {
stBlock = Nil
val res = f
if (stBlock != Nil) {
val Code(last) = res
Code((stBlock foldRight last)(Let))
} else {
res
}
}
def reflect(s:Exp) = {
stBlock :+= s
fresh()
}
type Env = List[Val]
abstract class Val
case class Cst(n:Int) extends Val
case class Str(s:String) extends Val
case class Clo(env:Env,e:Exp) extends Val
case class Tup(v1:val,v2:Val) extends Val
case class Code(e:Exp) extends Val
abstract class Exp
case class Lit(n:Int) extends Exp
case class Sym(s:String) extends Exp
case class Var(n:Int) extends Exp
case class App(e1:Exp, e2:Exp) extends Exp
case class Lam(e:Exp) extends Exp
case class Let(e1:Exp,e2:Exp) extends Exp
case class If(c:Exp,a:Exp,b:Exp) extends Exp
case class Plus(a:Exp,b:Exp) extends Exp
case class Minus(a:Exp,b:Exp) extends Exp
case class Times(a:Exp,b:Exp) extends Exp
case class Equ(a:Exp,b:Exp) extends Exp
case class Conss(a:Exp,b:Exp) extends Exp
case class Fst(a:Exp) extends Exp
case class Snd(a:Exp) extends Exp
case class IsNum(a:Exp) extends Exp
case class IsStr(a:Exp) extends Exp
case class IsCons(a:Exp) extends Exp
case class Lift(e:Exp) extends Exp
case class Run(b:Exp,e:Exp) extends Exp
Val ::= [#code ???]
| [#cons Val Val]
| [#nil]
| [#sym Name]
| [#clo Val Val Val Env]
| [#wrap Val]
| [#envp Sym Val Env]
| [#envn]
| [#op \vau]
| [#op \wrap]
| [#op \unwrap]
| [#op \lift]
| [#op \run]
| [#op \eval]
| [#op \cons]
| [#op \first]
| [#op \rest]
| [#op \cons?]
Most values do not have forms of literal expressions, only symbols and lists do.
Exp ::= Symbol
| List
[\eval [#code EXPR LETS] ENV] = ???
[\eval [#cons COMB ARGS] ENV] = [combine [\eval COMB ENV] ARGS ENV]
[\eval [#nil] _] = error
[\eval S@[#symbol ...] ENV] = [lookup S ENV]
[\eval C@[#clo ...] _] = C
[\eval W@[#wrap ...] _] = W
[\eval E@[#envp ...] _] = E
[\eval E@[#envn] _] = E
[\eval O@[#op ...] _] = O
[lookup S@[#symbol ...] [#envp S V _]] = V
[lookup S1@[#symbol ...] [#envp S2 _ E]] = [lookup S1 E] iff S1 /= S2
[lookup S@[#symbol ...] [#envn]] = error
[combine [#code ???] ARGS ENV] = ???
[combine [#cons Val Val] ARGS ENV] = error
[combine [#nil] ARGS ENV] = error
[combine [#sym Name] ARGS ENV] = error
[combine [#clo Val Val Val Env] ARGS ENV] = todo
[combine [#wrap Val] ARGS ENV] = todo
[combine [#envp Sym Val Env] ARGS ENV] = error
[combine [#envn] ARGS ENV] = error
[combine [#op \vau] ARGS ENV] = todo
[combine [#op \wrap] ARGS ENV] = todo
[combine [#op \unwrap] ARGS ENV] = todo
[combine [#op \lift] ARGS ENV] = todo
[combine [#op \run] ARGS ENV] = todo
[combine [#op \eval] ARGS ENV] = todo
[combine [#op \cons] ARGS ENV] = todo
[combine [#op \first] ARGS ENV] = todo
[combine [#op \rest] ARGS ENV] = todo
[combine [#op \cons?] ARGS ENV] = todo