singularity

------------------------------------------------------------------------
-- Supports comments, spaces, variables consisting of lowercase letters.
------------------------------------------------------------------------

pair x y f = f x y;
just x f g = g x;

pure x s = just (pair x s);
bind f m = m @K (\x -> x f);
ap x y = \s -> bind (\a t -> bind (\b u -> pure (a b) u) (y t)) (x s);
fmap f x = ap (pure f) x;
alt x y = \s -> (x s) (y s) just;
liftaa f x y = ap (fmap f x) y;
many = @Y \r p -> alt (liftaa @: p (r p)) (pure @K);
some p = liftaa @: p (many p);
liftki = liftaa (@K @I);
liftk = liftaa @K;
sat f s = s @K (\h t -> f h (pure h t) @K);
char c = sat (\x -> x(c @=));

lcr s   = \a b c d -> a s;
lcv v   = \a b c d -> b v;
lca x y = \a b c d -> c x y;
lcl x y = \a b c d -> d x y;

com = liftki (char #-) (liftki (char #-) (many (sat (\c -> @C (c(#
@=))))));
sp = many (alt (char # ) (alt (char #
) com));
spc f = liftk f sp;
spch = @B spc char;
var = spc ( some (sat (\x -> (#z(x @L)) (x(#a @L)) (@K @I) )));

foldr = @Y \r c n l -> l n (\h t -> c h(r c n t));
anyone = fmap (@:) (spc (sat (@K @K)));
pre = ap (alt (fmap (@K @I) (char #@)) (fmap (@B @B @:) (char ##))) anyone;
lam r = liftki (spch #\) (liftaa (@C (foldr lcl)) (some var) (liftki (char #-) (liftki (spch #>) r)));
atom r = alt (fmap lcv var) (alt (liftki (spch #() (liftk r (spch #)))) (alt (fmap lcr pre) (lam r)));
apps = @Y \f r -> alt (liftaa @T (atom r) (fmap (\vs v x -> vs (lca x v)) (f r))) (pure @I);
expr = @Y \r -> liftaa @T (atom r) (apps r);
def = liftaa pair var (liftaa (@C (foldr lcl)) (many var) (liftki (spch #=) expr));
program = liftki sp (some (liftk def (spch #;)));

lsteq = @Y \r xs ys a b -> xs (ys a (\u u -> b)) (\x xt -> ys b (\y yt -> x(y @=) (r xt yt a b) b));
rank ds v = foldr (\d t -> lsteq v (d @K) (\n -> @B (@:#@) (@:n)) (@B t \n -> #0(#1 @-)(n @+))) @? ds # ;
shows f = @Y \r t -> t @I f (\x y -> @B (@B (@:#`) (r x)) (r y)) @?;

isfree f = @Y \r t -> t (\x -> @K @I) f (\x y -> (r x) @K (r y)) @?;
unlam f = @Y \r t -> f t (t @? (@K (lcr (@:#I))) (\x y -> lca (lca (lcr (@:#S)) (r x)) (r y)) @?) (lca (lcr (@:#K)) t);
babs = @Y \r t -> t lcr lcv (\x y -> lca (r x) (r y)) (\x y -> unlam (isfree (lsteq x)) (r y));

dump tab = foldr (\h t -> shows (rank tab) (babs (h (@K @I))) (@:#;t)) @K tab;
main s = program s (@:#?@K) (@B dump (@T @K));