(synonyms stack (list ob)
environment (list (symbol * ob))
control (list ob)
dump (list (stack * environment * control)))
(datatype ob
E : environment; X : symbol; Y : ob;
====================================
[closure E X Y] : ob;
X : symbol; Y : ob;
===================
[lambda X Y] : ob;
Then : ob; Else : ob; Test : ob;
================================
[if Then Else Test] : ob;
X : ob; Y : ob;
===============
[X Y] : ob;
X : boolean;
____________
X : ob;
X : symbol;
___________
X : ob;
X : number;
___________
X : ob;
X : string;
___________
X : ob;
_____________________________________
(number? X) : verified >> X : number;)
(define evaluate
{ob --> ob}
X -> (secd [] [] [X] []))
(define secd
{stack --> environment --> control --> dump --> ob}
S E C D -> (do (output "~%S = ~R~%E = ~R~%C = ~R~%D = ~R~%" S E C D)
(read-byte (stinput))
(secd-h S E C D)))
(define secd-h
{stack --> environment --> control --> dump --> ob}
[V] E [] [] -> V
[V] _ [] [(@p S E C) | D] -> (secd [V | S] E C D)
S E [[if Test Then Else] | C] D -> (secd S E [Test if Then Else @ | C] D)
[true | S] E [if Then Else @ | C] D -> (secd S E [Then | C] D)
[false | S] E [if Then Else @ | C] D -> (secd S E [Else | C] D)
S E [[lambda X Y] | C] D -> (secd [[closure E X Y] | S] E C D)
S E [[X Y] | C] D -> (secd S E [Y X @ | C] D)
[F X | S] E [@ | C] D -> (secd [(apply F X) | S] E C D) where (prim? F)
[[closure E* X Y] Z | S] E [@ | C] D -> (secd [] [(@p X Z) | E*] [Y] [(@p S E C) | D])
S E [X | C] D ->(if (bnd? X E) (secd [(lookup X E) | S] E C D) (secd [X | S] E C D))
S E C D -> (error "~%cannot compute S = ~R, E = ~R, C = ~R, D = ~R~%" S E C D))
(define bnd?
{ob --> environment --> boolean}
X [] -> false
X [(@p Y _) | _] -> true where (== X Y)
X [_ | Y] -> (bnd? X Y))
(define lookup
{ob --> environment --> ob}
X [] -> X
X [(@p Y Z) | _] -> Z where (== X Y)
X [_ | Y] -> (lookup X Y))
(define prim?
{ob --> boolean}
F -> (element? F [succ pred zero?]))
(define apply
{ob --> ob --> ob}
succ X -> (+ X 1) where (number? X)
pred X -> (- X 1) where (number? X)
zero? X -> (= X 0) where (number? X))