module Ski
( Ski (S, K, I, Comb, Cte,
Spair, Spi1, Spi2, Sinl, Sinr, Scase, Sunit, Sabort, Sabsurd)
, skiabs
)
where
import NamedLambda
data Ski = S | K | I | Comb Ski Ski | Cte String
| Spair
| Spi1
| Spi2
| Sinl
| Sinr
| Scase
| Sunit
| Sabort
| Sabsurd
deriving (Eq, Ord)
instance Show Ski where
show = showski
showski :: Ski -> String
showski S = "S"
showski K = "K"
showski I = "I"
showski (Cte _) = "?"
showski (Comb x S) = showski x ++ showski S
showski (Comb x K) = showski x ++ showski K
showski (Comb x I) = showski x ++ showski I
showski (Comb x (Cte c)) = showski x ++ showski (Cte c)
showski (Comb x (Comb u v)) = showski x ++ "(" ++ showski (Comb u v) ++ ")"
showski (Comb x a) = showski x ++ showski a
showski Spair = "[PAIR]"
showski Spi1 = "[FST]"
showski Spi2 = "[SND]"
showski Sinl = "[INL]"
showski Sinr = "[INR]"
showski Scase = "[CASEOF]"
showski Sunit = "[UNIT]"
showski Sabort = "[ABORT]"
showski Sabsurd = "[ABSURD]"
skiabs :: NamedLambda -> Ski
skiabs (LambdaVariable x) = Cte x
skiabs (LambdaApplication m n) = Comb (skiabs m) (skiabs n)
skiabs (LambdaAbstraction x m) = bracketabs x (skiabs m)
skiabs (TypedPair a b) = Comb (Comb Spair (skiabs a)) (skiabs b)
skiabs (TypedPi1 a) = Comb Spi1 (skiabs a)
skiabs (TypedPi2 a) = Comb Spi2 (skiabs a)
skiabs (TypedInl a) = Comb Sinl (skiabs a)
skiabs (TypedInr a) = Comb Sinr (skiabs a)
skiabs (TypedCase a b c) = Comb (Comb (Comb Scase (skiabs a)) (skiabs b)) (skiabs c)
skiabs TypedUnit = Sunit
skiabs (TypedAbort a) = Comb Sabort (skiabs a)
skiabs (TypedAbsurd a) = Comb Sabsurd (skiabs a)
bracketabs :: String -> Ski -> Ski
bracketabs x (Cte y) = if x == y then I else Comb K (Cte y)
bracketabs x (Comb u (Cte y))
| freein x u && x == y = u
| freein x u = Comb K (Comb u (Cte y))
| otherwise = Comb (Comb S (bracketabs x u)) (bracketabs x (Cte y))
bracketabs x (Comb u v)
| freein x (Comb u v) = Comb K (Comb u v)
| otherwise = Comb (Comb S (bracketabs x u)) (bracketabs x v)
bracketabs _ a = Comb K a
freein :: String -> Ski -> Bool
freein x (Cte y) = x /= y
freein x (Comb u v) = freein x u && freein x v
freein _ _ = True