/**
 * A transformation from the unsigned integer arithmetic language
 * to the lambda calculus.
 *
 * @author Jacob Andersen
 */

(|
  "unsignedArith.l" -> "lambda.l" 

  [ Exp -> Exp ] 

  Exp.zero   =  '\fx.x' ;
  Exp.succ   =  '(\nfx.f(nfx)) ($1)' ;
  Exp.pred   =  '(\nfx.n(\gh.h(gf))(\u.x)(\u.u)) ($1)' ;
  Exp.add    =  '(\mnfx.mf(nfx)) ($1) ($2)' ;
  Exp.sub    =  '(\mn.n(\nfx.n(\gh.h(gf))(\u.x)(\u.u))m) ($1) ($2)' ;
  Exp.mul    =  '(\mnf.n(mf)) ($1) ($2)' ;
  Exp.iszero =  '(\n.n(\x.(\xy.y))(\xy.x)) ($1)' ;
  Exp.paren  =  '($1)' ;
|)