(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;
  
  F : symbol; Params : (list symbol); Body : ob;
  ==============================================
  [defun F Params Body] : 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;
  
  _______________________________
  (value *global*) : environment;) 
  
(set *global* [])           	

(define evaluate
  {ob --> ob}
   [defun F Params Y] -> (let Reverse (reverse Params)
                              Quote (quote-free-variables Params Y)  
                              Update (update-global-environment F Reverse Quote) 
                              F)
  X -> (secd [] [] [X] []))
  
(define quote-free-variables
  {(list symbol) --> ob --> ob}
   Bound [lambda X Y] -> [lambda X (quote-free-variables [X | Bound] Y)]
   Bound [if Test Then Else] -> [if (quote-free-variables Bound Test) 
                                    (quote-free-variables Bound Then) 
                                    (quote-free-variables Bound Else)]
   Bound [X Y] -> [X (quote-free-variables Bound Y)]   where (symbol? X)                               
   Bound [X Y] -> [(quote-free-variables Bound X) (quote-free-variables Bound Y)]
   [V | Vs] X ->  X       where (== V X)
   [_ | Vs] X -> (quote-free-variables Vs X)
   [] X -> [quote X]     where (symbol? X)
   _ X -> X)
  
(define update-global-environment
  {symbol --> (list symbol) --> ob --> environment}
   F [] Z         -> (set *global* [(@p F Z) | (value *global*)])
   F [X | Y] Z -> (update-global-environment F Y [lambda X Z]))
 
(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 [[quote X] | C] D -> (secd [[quote X] | 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 -> (cases (bnd? X E) (secd [(lookup X E) | S] E C D)        
                          (bnd? X (value *global*)) (secd S E [(lookup X (value *global*)) | C] D)
                          true  (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 lookup
  {ob --> environment --> ob}
   X [(@p Y Z) | _] -> Z  where (== X Y)
   X [_ | Y] -> (lookup X Y)) 
   
(define bnd?
  {ob --> environment --> boolean}
   X [] -> false
   X [(@p Y _) | _] -> true  where (== X Y) 
   X [_ | Y] -> (bnd? 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))
   
(evaluate [defun f [x y] [g x]])

(evaluate [defun g [x] y])