# lambda.sed

# All variables read in must be a sequence of one or more
# *lowercase* letters.  For example, a, b, it, this, coolvar.

# When we need to introduce a new variable, we just tack on a letter.
# I don't think we need to be completely non-ambiguous.

:beginning

# Alpha Reduction
#
#  [y/x]E
#   variables
#    [y/x]x       => y
#    [y/x]z       => z
#   abstractions
#    [y/x](\x.E)  => (\x.E)
#    [y/x](\y.E)  => (\z.[z/y]E)|[y/x]X
#    [y/x](\z.E)  => [y/x]E|(\z.X)
#   applications
#    [y/x](E1 E2)   => [y/x]E1|(X [y/x]E2)

:alpha-reduction

:variables
# [y/x]x => y
s,^\[\([[:lower:]]\+\)/\([[:lower:]]\+\)\]\2\(\(\)\|\(|.*\)\)$,\1\3,
# [y/x]z => z
s,^\[\([[:lower:]]\+\)/\([[:lower:]]\+\)\]\([[:lower:]]\+\)\(\(\)\|\(|.*\)\)$,\3\4,

:abstractions
# [y/x](\x.E)  => (\x.E)
s,^\[\([[:lower:]]\+\)/\([[:lower:]]\+\)\]\((\\\2\.\([^|]*\))\)\(\(\)\|\(|.*\)\)$,\3\4,
# [y/x](\y.E)  => (\z.[z/y]E)|[y/x]X
# for new variable z, we use yx
s,^\[\([[:lower:]]\+\)/\([[:lower:]]\+\)\](\\\1\.\([^|]*\)\(\(\)\|\(|.*\)\)$,(\\\1\2\.\[\1\2/\1\]\3)|\[\1/\2\]X\4,
t applications
# [y/x](\z.E)  => [y/x]E|(\z.X)
s,^\[\([[:lower:]]\+\)/\([[:lower:]]\+\)\](\\\([[:lower:]]\+\)\.\([^|]*\))\(\(\)\|\(|.*\)\),\[\1/\2\]\4|(\\\3\.X)\5,

:applications
# [y/x](E1 E2)   => (E1 E2)|[y/x]X  =>  E1:E2|[y/x]X  =>  [y/x]E1|(X [y/x]E2)
s,^\(\[[[:lower:]]\+/[[:lower:]]\+\]\)\(([^ |]\+ [^|]\+)\)\(.*\),\2|\1X,
s,^\([^|:]\+\):\([^|]\+\)|\(\[[[:lower:]]\+/[[:lower:]]\+\]\)X\(.*\),\3\1|(X \3\2)\4,

# Separate Application elements
# changes (E1 E2) => E1:E2
#
# =A=B=C=D=E=F=G
#  A = open parentheses from copy of proposed E1 (pE1)
#  B = close parentheses from copy of pE1
#  C = copy of pE1
#  D = pE1
#  E = proposed E2 (pE2)
#  F = E1 E2
#  G = stack
#
# move parentheses from C to A or B until C is empty
# if size of A == size of B, pE1 == E1
#
# (E1 E2)S          => ===pE1=pE1=pE2=E1 E2=S
# ===(c=dn=en=f=g   => =(==c=dn=en=f=g       ; first (
# ===)c=dn=en=f=g   => boom                  ; found ) first: shouldn't happen
# ==b=(c=dn=en=f=g  => boom                  ; found ( after ): shouldn't happen
# =a==)c=dn=en=f=g  => =a=)=c=dn=en=f=g      ; found another first )
# =a=b=(c=dn=en=f=g => =(a=b=c=dn=en=f=g     ; found another (
# =a=b=)c=dn=en=f=g => =a=)b=c=dn=en=f=g     ; found another )
# ===zc=dn=en=f=g   => ===c=dn=en=f=g        ; throw away non-parentheses
# ==b=zc=dn=en=f=g  => ==b=c=dn=en=f=g       ; throw away non-parentheses
# =a==zc=dn=en=f=g  => =a==c=dn=en=f=g       ; throw away non-parentheses
# =a=b=zc=dn=en=f=g => =a=b=c=dn=en=f=g      ; throw away non-parentheses
# =(a=)b==dn=en=f=g => =a=b==dn=en=f=g       ; throw away parens two by two
# =a===dn=en=f=g    => ===dn+1=dn+1=en+1=f=g ; odd number, try again
# ==b==dn=en=f=g    => ===dn+1=dn+1=en+1=f=g ; odd number, try again
# ====d=e=f=g       => d:eg                  ; found it!

:separate-application
# assume we know it is an application
# (E1 E2)|S => ===pE1=pE1=pE2=E1 E2=S
s/^(\([^ |]\+\) \([^|]\+\))\(.*\)/===\1=\1=\2=\1 \2=\3/
# ===(c=dn=en=f=g => =(==c=dn=en=f=g
s/^===(\([^=]\+\)=\([^=]\+\)=\([^=]\+\)=\([^=]\+\)=\(.*\)/=(==\1=\2=\3=\4=\5/
# ===)c=dn=en=f=g   => ==)=c=dn=en=f=g
/^===)\([^=]\+\)=\([^=]\+\)=\([^=]\+\)=\([^=]\+\)=\(.*\)/b end
# ==b=(c=dn=en=f=g => =(=b=c=dn=en=f=g
/^==\([^=]\+\)=(\([^=]\+\)=\([^=]\+\)=\([^=]\+\)=\([^=]\+\)=\(.*\)/b end
# =a==)c=dn=en=f=g => =a=)=c=dn=en=f=g
s/^=\([^=]\+\)==)\([^=]*\)=\([^=]\+\)=\([^=]\+\)=\([^=]\+\)=\(.*\)/=\1=)=\2=\3=\4=\5=\6/
# =a=b=(c=dn=en=f=g => =(a=b=c=dn=en=f=g
s/^=\([^=]\+\)=\([^=]\+\)=(\([^=]\+\)=\([^=]\+\)=\([^=]\+\)=\([^=]\+\)=\(.*\)/=(\1=\2=\3=\4=\5=\6=\7/
# =a=b=)c=dn=en=f=g => =a=)b=c=dn=en=f=g
s/^=\([^=]\+\)=\([^=]\+\)=)\([^=]\+\)=\([^=]\+\)=\([^=]\+\)=\([^=]\+\)=\(.*\)/=\1=)\2=\3=\4=\5=\6=\7/
# ===zc=dn=en=f=g => ===c=dn=en=f=g
s/^===[^()]\([^=]*\)=\([^=]\+\)=\([^=]\+\)=\([^=]\+\)=\(.*\)/===\1=\2=\3=\4=\5/
# =a==zc=dn=en=f=g => =a==c=dn=en=f=g
s/^=\([^=]\+\)==[^()]\([^=]*\)=\([^=]\+\)=\([^=]\+\)=\([^=]\+\)=\(.*\)/=\1==\2=\3=\4=\5=\6/
# ==b=zc=dn=en=f=g => ==b=c=dn=en=f=g
s/^==\([^=]\+\)=[^()]\([^=]*\)=\([^=]\+\)=\([^=]\+\)=\([^=]\+\)=\(.*\)/==\1=\2=\3=\4=\5=\6/
# =a=b=zc=dn=en=f=g => =a=b=c=dn=en=f=g
s/^=\([^=]\+\)=\([^=]\+\)=[^()]\([^=]*\)=\([^=]\+\)=\([^=]\+\)=\([^=]\+\)=\(.*\)/=\1=\2=\3=\4=\5=\6=\7/
# =(a=)b==dn=en=f=g => =a=b==dn=en=f=g
s/^=(\([^=]*\)=)\([^=]*\)==\([^=]\+\)=\([^=]\+\)=\([^=]\+\)=\(.*\)/=\1=\2==\3=\4=\5=\6/
# =a===dn=en=f=g => ===d=dn+1=en+1=f=g
s/^=\([^=]\+\)===\([^=]\+\)=\([^=]\+\)=\(\2 [^ =]\+\) \([^=]\+\)=\(.*\)/===\4=\4=\5=\4 \5=\6/
# ==b==dn=en=f=g => ===dn+1=dn+1=en+1=f=g
s/^==\([^=]\+\)==\([^=]\+\)=\([^=]\+\)=\(\2[^ ]\+\) \([^=]\+\)=\(.*\)/===\4=\4=\5=\4 \5=\6/
# ====d=e=f=g => d:eg
s/^====\([^=]\+\)=\([^=]\+\)=\([^=]\+\)=\(.*\)/\1:\2\4/
/.*:.*/b separated
t separate-application
:separated

#/.*/p
#b beginning

:end