#
#	lambdarc
#	Startup lambda file
#	Fred Barnes, 1999
#

I = \x.x
K = \xy.x
S = \xyz.(xz(yz))
B = \xyz.(x(yz))
C = \xyz.(xzy)
Y = \f.((\x.(f(xx)))(\x.(f(xx))))
T = K
F = \xy.y

# Church numeral operations (add,mul,exp)
_CA = \mnsz.(ms(nsz))
_CM = \mns.(m(ns))
_CE = \mn.(nm)

# Some simple boolean operations
_if = \x.x
_true = T
_false = F

# Silly terms
_nonf = (\x.(xx) \y.(yy))
_explode = (\x.(xx) \q.(qqq))

# Slightly useful things when working with pairs

_swap = \f.(}(f),{(f))
_merge = \f.(( {({(f)) , {(}(f)) ),( }({(f)) , }(}(f)) ))
_apply = \f.({(f)}(f))

# Our friendly boolean functions
_and = \fg.(fgF)
_imp = \fg.(fgK)
_or = \fg.(fK(gKF))
_not = \f.(fFK)
_xor = \fg.(f(gFK)(gKF))

# Terms to help with lists
_cons = \xys.(sxy)
_nil = \x.K
_isnil = \p.(p (\xy.F))
_hd = \p.(p K)
_tl = \p.(p F)
_fix = ( (\xy.(y(xxy))) (\xy.(y(xxy))) )

# A nice list  [[a,b,c],[d,e],[f]]
_nlparta = ("cons" a ("cons" b ("cons" c "nil")))
_nlpartb = ("cons" d ("cons" e "nil"))
_nlpartc = ("cons" f "nil")
_nllist = ("cons" "nlparta" ("cons" "nlpartb" ("cons" "nlpartc" "nil")))
:"nllist"
_nicelist = "@"

_shortlist = ("cons" ("cons" a "nil") "nil")

# Numeric list of [1,2,3]
_numblist = ("cons" '1 ("cons" '2 ("cons" '3 "nil")))
:"numblist"
_numberlist = "@"

# Stuff for lists
_fst = \p.{(p)
_snd = \p.}(p)
_select = \nl.("fst" ((n "snd") l))

#
#	join [] y = y
#	join (a::x) y = a::(join x y)
#
_joining = \fxy.(("isnil" x) y ("cons" ("hd" x) (f ("tl" x) y) ))
_join = ("fix" "joining")

#
#	flatten [] = []
#	flatten (a::x) = join a (flatten x)
#
_flattening = \fl.(("isnil" l) l ("join" ("hd" l) (f ("tl" l))) )
_flatten = ("fix" "flattening")

#
#	map f [] = []
#	map f (a::x) = (fa)::(map f x)
#
_mapping = \rfl.(("isnil" l) l ("cons" (f ("hd" l)) (r f ("tl" l)) ))
_map = ("fix" "mapping")
_timestwo = \x.("CM" '2 x)

#
#	fun stuff
#

_iszero = \n.(n (KF) K)


#
#	experimental..  (turing-machine in lambda?)
#

# definition of a tape: [1,1,0] at index 0
_INturtape = ("cons" '1 ("cons" "nil" ("cons" '1 ("cons" '0 "nil"))))
:_INturtape
_turtape = @

# some handy functions
_INleftsym = \t.("hd" ("hd" ("tl" t)))
_INrightsym = \t.("hd" ("tl" ("tl" t)))
_INlefttape = \t.("hd" ("tl" t))
_INrighttape = \t.("tl" ("tl" t))

:_INleftsym
_leftsym = @
:_INrightsym
_rightsym = @
:_INlefttape
_lefttape = @
:_INrighttape
_righttape = @

_INreadsym = \t.("hd" t)
_INwritesym = \st.("cons" s ("cons" ("lefttape" t) ("righttape" t)))

:_INreadsym
_readsym = @
:_INwritesym
_writesym = @

# these take a tape and move it left or right
_INtapeleft = \t.("cons" ("rightsym" t) ("cons" ("cons" ("readsym" t) ("lefttape" t)) ("tl" ("righttape" t))))
_INtaperight = \t.("cons" ("leftsym" t) ("cons" ("tl" ("lefttape" t)) ("cons" ("readsym" t) ("righttape" t))))

:_INtapeleft
_tapeleft = @
:_INtaperight
_taperight = @

# this is the addition function for church numerals (prefix)
_churchadd = \xy.((\mnsz.(m s (n s z))) x y)

# a program that:
#   read number,
#   shift tape right,
#   read number,
#   shift tape right,
#   write sum of both numbers

_addadjacent = \t.("churchadd" ("readsym" t) ("readsym" ("tapeleft" t)))
_turprogram = \t.("writesym" ("addadjacent" t) ("tapeleft" ("tapeleft" t)))

# definition of a tape: [1,1,2] at index 2
_INresulttape = ("cons" '2 ("cons" ("cons" '1 ("cons" '1 "nil")) "nil"))
:_INresulttape
_resulttape = @

#/con
/von
/eon
#/l