stringy

------------------------------------------------------------------------
-- Uppercase letters. Strings. Chars.
-- Bracket abstraction optimization.
------------------------------------------------------------------------

or f g x y = f x (g x y);
and f g x y = @C f y (g x y);
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));
append = @Y \r xs ys -> xs ys (\x xt -> @: x (r xt ys));
pair x y f = f x y;
just x f g = g x;
foldr = @Y \r c n l -> l n (\h t -> c h(r c n t));

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;

pure x inp = just (pair x inp);
bind f m = m @K (\x -> x f);
ap x y = \inp -> bind (\a t -> bind (\b u -> pure (a b) u) (y t)) (x inp);
fmap f x = ap (pure f) x;
alt x y = \inp -> (x inp) (y inp) 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;
between x y p = liftki x (liftk p y);
sat f inp = inp @K (\h t -> f h (pure h t) @K);

char c = sat (\x -> x(c(@=)));
com = liftki (char #-) (between (char #-) (char #
) (many (sat (\c -> @C (c(#
(@=)))))));
sp = many (alt (sat (\c -> or (c(# (@=))) (c(#
(@=))))) com);
spc f = liftk f sp;
spch = @B spc char;
var = spc (some (sat (\x -> or
  (and (#z(x(@L))) (x(#a(@L))))
  (and (#Z(x(@L))) (x(#A(@L))))
  )));
anyone = fmap (@C @: @K) (spc (sat (@K @K)));
pre = liftki (char #@) anyone;
lam r = liftki (spch #\) (liftaa (@C (foldr lcl)) (some var) (liftki (char #-) (liftki (spch #>) r)));
rawcom x = lcr (@: x @K);
consexpr = rawcom #:;
constexpr = rawcom #K;
listify = fmap (foldr (\h t -> lca (lca consexpr h) t) constexpr);
escchar = liftki (char #\) (alt (sat (\c -> or (c(#"(@=))) (or (c(#\(@=))) (c(#'(@=)))))) (fmap (@K #
) (char #n)));
litone delim = fmap (@B lcr (@B (@: ##) (@C @: @K))) (alt escchar (sat (\c -> @C (delim(c(@=))))));
litstr = listify (between (char #") (spch #") (many (litone #")));
litchar = between (char #') (spch #') (litone #');
lit = alt litstr litchar;
atom r = alt (alt (alt (alt (between (spch #() (spch #)) r) (lam r)) (fmap lcr pre)) (fmap lcv var)) lit;
apps = @Y \rr r -> alt (liftaa @T (atom r) (fmap (\vs v x -> vs (lca x v)) (rr 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 #;)));

ze   = \    a b c d e -> a;
su   = \x   a b c d e -> b x;
pass = \x   a b c d e -> c x;
la   = \x   a b c d e -> d x;
app  = \x y a b c d e -> e x y;

debruijn = @Y \r n e -> e
  (\s -> pass (lcr s))
  (\v -> foldr (\h m -> lsteq h v ze (su m)) (pass (lcv v)) n)
  (\x y -> app (r n x) (r n y))
  (\s t -> la (r (@: s n) t))
  ;

defer = \a b c d -> a;
closed = \t a b c d -> b t;
need = \x a b c d -> c x;
weak = \x a b c d -> d x;

ldef = \r y -> y
  (need (closed (lca (lca (rawcom #S) (rawcom #I)) (rawcom #I))))
  (\d -> need (closed (lca (rawcom #T) d)))
  (\e -> need (r (closed (lca (rawcom #S) (rawcom #I))) e))
  (\e -> need (r (closed (rawcom #T)) e))
  ;

lclo = \r d y -> y
  (need (closed d))
  (\dd -> closed (lca d dd))
  (\e -> need (r (closed (lca (rawcom #B) d)) e))
  (\e -> weak (r (closed d) e))
  ;

lnee = \r e y -> y
  (need (r (r (closed (rawcom #S)) e) (closed (rawcom #I))))
  (\d -> need (r (closed (lca (rawcom #R) d)) e))
  (\ee -> need (r (r (closed (rawcom #S)) e) ee))
  (\ee -> need (r (r (closed (rawcom #C)) e) ee))
  ;

lwea = \r e y -> y
  (need e)
  (\d -> weak (r e (closed d)))
  (\ee -> need (r (r (closed (rawcom #B)) e) ee))
  (\ee -> weak (r e ee))
  ;

babsa = @Y \r x y -> x
  (ldef r y)
  (\d -> lclo r d y)
  (\e -> lnee r e y)
  (\e -> lwea r e y)
  ;

babs = @Y \r t -> t
  defer
  (@B weak r)
  closed
  (\t -> r t
    (closed (rawcom #I))
    (\d -> closed (lca (rawcom #K) d))
    @I
    (babsa (closed (rawcom #K))))
  (\x y -> babsa (r x) (r y))
  ;

nolam x = babs (debruijn @K x) @? @I @? @?;

rank ds v = foldr (\d t -> lsteq v (d @K) (\n -> @: #@ (@: n @K)) (@B t \n -> # (#!(@-))(n(@+)) )) (@K v) ds # ;
show = @Y \r ds t -> t @I (rank ds) (\x y -> @:#`(append (r ds x) (r ds y))) @?;
dump = @Y \r tab ds -> ds @K \h t -> append (show tab (nolam (h (@K @I)))) (@: #; (r tab t));
main s = program s (@:#?@K) (@B (\ds -> dump ds ds) (@T @K));