/*
 * Illustration of encodings of programs in the simple functional 
 * programming language
 */

module examples.

type prog    string -> tm -> o.

prog "successor" 
  (fn x\ plus `@ x `@ (in 1)).

prog "onep" 
  (fn w\ fn u\ fn v\ cond (equal `@ (in 1) `@ w) u v).

prog "is_sym"
  (fn f\ fn x\ fn y\ equal `@ (f `@ x `@ y) `@ (f `@ y `@ x)).

prog "fib" 
  (fixpt fib\ fn n\ cond (zerop `@ n) (in 0) 
                     (cond (equal `@ n `@ (in 1)) (in 1) 
                           (plus `@ (fib `@ (minus `@ n `@ (in 1))) `@ 
                                   (fib `@ (minus `@ n `@ (in 2)))))).

prog "map" 
  (fixpt map\ fn f\ fn l\ 
     cond (nullp `@ l) empty 
          (cons `@ (f `@ (car `@ l)) `@ (map `@ f `@ (cdr `@ l)))).

prog "mem" 
  (fixpt mem\ fn x\ fn l\ 
    cond (nullp `@ l) false 
         (cond (and `@ (consp `@ l) `@ (equal `@ (car `@ l) `@ x)) 
                truth (mem `@ x `@ (cdr `@ l)))).

prog "fact" 
  (fixpt f\ fn n\ fn m\
    cond (equal `@ n `@ (in 0)) m
         (f `@ (minus `@ n `@ (in 1)) `@ (times `@ n `@ m))).

prog "app"
  (fixpt app\ fn l\ fn k\
    (cond (nullp `@ l) k (cons `@ (car `@ l) `@ (app `@ (cdr `@ l) `@ k)))).

prog "gcd" 
  (fixpt f\ fn x\ fn y\ 
    cond (equal `@ (in 1) `@ x) (in 1)
         (cond (greater `@ y `@ x) (f `@ y `@ x)
               (cond (equal `@ x `@ y) x (f `@ (minus `@ x `@ y) `@ y)))).

prog "ex1"   (cons `@ (in 1) `@ (in 2)).
prog "ex2"   (plus `@ empty `@ (in 1)).
prog "ex3"   (cond truth (in 3) empty).
prog "ex4"   (fn x\ fn x\x).
prog "ex5"   (cond truth (in 3) (in 5)).
prog "ex6"   ((fn x\x) `@ (fn y\y)).
prog "i"     (fn x\ x).
prog "k"     (fn x\ fn y\x).
prog "s"     (fn x\ fn y\ fn z\ (x `@ z) `@ (y `@ z)).
prog "comp"  (fn f\ fn g\ fn x\ f `@ (g `@ x)).

