lambdabot-4.0: scripts/Djinn/examples.out
id :: a -> a
id a = a
const :: a -> b -> a
const a _ = a
fst :: (a, b) -> a
fst (a, _) = a
snd :: (a, b) -> b
snd (_, a) = a
swap :: (a, b) -> (b, a)
swap (a, b) = (b, a)
compose :: (b -> c) -> (a -> b) -> a -> c
compose a b c = a (b c)
curry :: ((a, b) -> c) -> a -> b -> c
curry a b c = a (b, c)
uncurry :: (a -> b -> c) -> (a, b) -> c
uncurry a (b, c) = a b c
flip :: (a -> b -> c) -> b -> a -> c
flip a b c = a c b
-- undefined cannot be realized.
either :: (a -> b) -> (c -> b) -> Either a c -> b
either a b c =
case c of
Left d -> a d
Right e -> b e
maybe :: b -> (a -> b) -> Maybe a -> b
maybe a b c =
case c of
Nothing -> a
Just d -> b d
returnC :: a -> C a
returnC a b = b a
bindC :: C a -> (a -> C b) -> C b
bindC a b c = a (\ d -> b d c)
callCC :: ((a -> C b) -> C a) -> C a
callCC a b = a (\ c _ -> b c) b
returnS :: a -> S s a
returnS a b = (a, b)
bindS :: S s a -> (a -> S s b) -> S s b
bindS a b c =
case a c of
(d, e) -> b d e
returnSD :: a -> SD s a
returnSD a = SD (\ b -> (a, b))
bindSD :: SD s a -> (a -> SD s b) -> SD s b
bindSD a b =
case a of
SD c -> SD (\ d ->
case c d of
(e, f) -> case b e of
SD g -> g f)
returnCD :: a -> CD r a
returnCD a = CD (\ b -> b a)
bindCD :: CD r a -> (a -> CD r b) -> CD r b
bindCD a b =
case a of
CD c -> CD (\ d ->
c (\ e ->
case b e of
CD f -> f d))
callCCD :: ((a -> CD r b) -> CD r a) -> CD r a
callCCD a =
CD (\ b ->
case a (\ c -> CD (\ _ -> b c)) of
CD d -> d b)
returnM :: a -> Maybe a
returnM = Just
bindM :: Maybe a -> (a -> Maybe b) -> Maybe b
bindM a b =
case a of
Nothing -> Nothing
Just c -> b c
handleM :: Maybe a -> Maybe a -> Maybe a
handleM a b =
case a of
Nothing -> b
Just c -> Just c
returnSX :: a -> SX s a
returnSX a b = (b, Just a)
bindSX :: SX s a -> (a -> SX s b) -> SX s b
bindSX a b c =
case a c of
(d, e) -> case e of
Nothing -> (d, Nothing)
Just f -> b f d
handleSX :: SX s a -> SX s a -> SX s a
handleSX a b c =
case b c of
(d, e) -> case e of
Nothing -> a c
Just f -> case a c of
(g, h) -> case h of
Nothing -> (g, Just f)
Just i -> (d, Just i)
bool1 :: Bool -> Bool
bool1 a = a
bool2 :: Bool -> Bool -> Bool
bool2 a b =
case a of
False -> b
True -> False
rot :: (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, aa, ab, ac) -> (z, aa, ab, ac, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y)
rot (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u,
v, w, x, y, z, x1, x2, x3) =
(z, x1, x2, x3, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q,
r, s, t, u, v, w, x, y)
f :: Either () (a, b) -> Either () (b, a)
f a =
case a of
Left _ -> Left ()
Right (b, c) -> Right (c, b)
f :: a -> a -> a
f _ a = a
-- or
f a _ = a
f :: Either () (a, b) -> Either () (b, a)
f a =
case a of
Left _ -> Left ()
Right (b, c) -> Right (c, b)
-- or
f _ = Left ()
f :: a -> (a -> a) -> a
f a b = b a
-- or
f a _ = a
f :: (a -> a) -> a -> a
f a = a
-- or
f a b = a b
-- or
f _ a = a
f1 :: ((((a, b) -> f) -> Either (a -> f) (b -> f)) -> f) -> f
f1 a =
a (\ b ->
Right (\ _ ->
a (\ _ -> Right (\ c -> a (\ _ -> Left (\ d -> b (d, c)))))))
f2 :: ((Either (a -> f) (b -> f) -> (a, b) -> f) -> f) -> f
f2 a =
a (\ b ->
case b of
Left c -> \ (d, _) -> c d
Right e -> \ (_, f) -> e f)
null :: List a -> Bool
null a =
case out a of
Nil -> False
Cons _ _ -> True
exm :: Not (Not (Either a (Not a)))
exm a = void (a (Right (\ b -> a (Left b))))
foo :: Not (c -> d) -> (Not (Not c), Not d)
foo a = (\ b -> void (a (\ c -> void (b c))), \ d -> a (\ _ -> d))
peirce :: Not (Not (((a -> b) -> a) -> a))
peirce a =
void (a (\ b -> void (a (\ _ -> b (\ c -> void (a (\ _ -> c)))))))