sbreese

#!/usr/bin/env                 runhaskell
-- sam breese, λ enthusiast. contact me @
{-# Language ViewPatterns #-} -- sbree.se
data T=V Int|A T T|L T T|P T T|Y deriving
 (Show,Read,Eq);m f i(V j)=f i j; m f i(A
 x y)=A(m f i x)$m f i y;m f i(L t x)=L(m
 f i t)$m f(i+1)x; m f i(P t x)=P(m f i t
 )$m f(i+1)x;m _ _ x=x; ifm True x=Just x
 ; ifm _ _=Nothing;mb f g (g->Just v) y =
 Just$f v y;mb f g x (g->Just v)=Just$f x
 v;mb _ _ _ _=Nothing;up i=m$ \j k->if k-
 j>=0then V$k+i else V k;dn=m$ \i j->if j
 <i then V$j-1else V j;su v=m$ \i j->if i
 ==j then up i 0 v else V j;e1(A(L _ x)y)
 =Just$su(dn 0 x)0y;e1(A x y)=mb A e1 x y
 ;e1(L t x)=mb L e1 t x;e1(P t x)=mb P e1
 t x;e1 _=Nothing;n x=case e1 x of{ --sjb
 Nothing->x;Just y->n y};teq(fmap n->Just
 t)(n->y)=t==y;teq _ _=False; inf c(V i)=
 ifm(i<length c)$c!!i;inf c(A x y)=do{P i
 o<-n<$>inf c x;u<-inf c y;ifm(teq(Just i
 )u)$su y 0o}; inf c(L t x)=ifm(teq(inf c
 t)Y)=<<P t<$>inf(up 1 0t:c)x;inf c(P t x
 )=ifm(teq(inf c t)Y&&teq(inf(up 1 0t:c)x
 )Y)Y;inf c Y=Just Y;main=do {putStr"λ ";
 t <- readLn; case inf[] t of {Nothing ->
 print "err";Just y->print(n t,y);};main}