content: {-|
  Module: Ski
  Description: Ski expressions and bracket abstraction.
  License: GPL-3
  
  This module implements a representation of the SKI subset of the
  calculus of combinators. It provides a lambda abstraction algorithm
  writing lambda expressions as combinators.
  -}
  
  module Ski
    ( Ski (S, K, I, Comb, Cte,
           Spair, Spi1, Spi2, Sinl, Sinr, Scase, Sunit, Sabort, Sabsurd)
    , skiabs
    )
  where
  
  import NamedLambda
  
  -- | A SKI combinator expression
  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
  
  -- | Shows a SKI expression
  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]"
  
  -- | SKI abstraction of a named lambda term. From a lambda expression
  -- creates a SKI equivalent expression. The following algorithm is a
  -- version of the algorithm 9.10 on the Hindley-Seldin book.
  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)
  
  
  -- | Bracket abstraction of a SKI term, as defined in Hindley-Seldin
  -- (2.18).
  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
  
  -- | Checks if a given variable is used on a SKI expression.
  freein :: String -> Ski -> Bool
  freein x (Cte y)    = x /= y
  freein x (Comb u v) = freein x u && freein x v
  freein _ _ = True
  