--
-- Copyright (c) 2005 Lennart Augustsson
-- See LICENSE for licensing details.
--
:set +s
-- Some Prelude functions
id ? a -> a;
const ? a -> b -> a;
fst ? (a, b) -> a;
snd ? (a, b) -> b;
swap ? (a, b) -> (b, a);
compose ? (b->c) -> (a->b) -> (a->c)
curry ? ((a,b) -> c) -> (a -> b -> c)
uncurry ? (a -> b -> c) -> ((a,b) -> c)
flip ? (a -> b -> c) -> b -> a -> c
undefined ? a
either ? (a -> b) -> (c -> b) -> Either a c -> b
maybe ? b -> (a -> b) -> Maybe a -> b

-- continuation monad operations
type C a = (a -> Ans) -> Ans
returnC ? a -> C a
bindC ? C a -> (a -> C b) -> C b
callCC ? ((a -> C b) -> C a) -> C a

-- state monad operations
type S s a = (s -> (a, s))
returnS ? a -> S s a
bindS ? S s a -> (a -> S s b) -> S s b

-- The data type versions
data SD s a = SD (s -> (a, s))
returnSD ? a -> SD s a
bindSD ? SD s a -> (a -> SD s b) -> SD s b

data CD r a = CD ((a -> r) -> r)
returnCD ? a -> CD r a
bindCD ? CD r a -> (a -> CD r b) -> CD r b
callCCD ? ((a -> CD r b) -> CD r a) -> CD r a

returnM ? a -> Maybe a
bindM ? Maybe a -> (a -> Maybe b) -> Maybe b
handleM ? Maybe a -> Maybe a -> Maybe a

-- State and exceptions
type SX s a = s -> (s, Maybe a)
returnSX ? a -> SX s a
bindSX ? SX s a -> (a -> SX s b) -> SX s b
-- Note that handleSX gets totally munged :)
handleSX ? SX s a -> SX s a -> SX s a

-- Some boolean function
bool1 ? Bool-> Bool
bool2 ? Bool-> Bool -> Bool

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)

f ? Either () (a, b) -> Either () (b, a)

:set +m
f ? a->a->a
f ? Either () (a, b) -> Either () (b, a)
f ? a->(a->a)->a
f ? (a->a)->a->a

:set -m
:set -s
-- CPS of deMorgans laws
f1 ? ((((a, b) -> f) -> Either (a -> f) (b -> f)) -> f) -> f;
f2 ? ((Either (a -> f) (b -> f) -> (a, b) -> f) -> f) -> f;

:set +s

-- Lists with recursion through Fix (uninterpreted)
data ListN a as = Nil | Cons a as
type List a = Fix (ListN a)
out :: List a -> ListN a (List a)
in :: ListN a (List a) -> List a
-- Strangely, it finds the null function
null ? List a -> Bool
:d out
:d in

-- Some fun with negation
exm ? Not (Not (Either a (Not a)))
foo ? Not (c -> d) -> (Not (Not c), Not d)
peirce ? Not (Not (((a->b)->a)->a))