--------------------------------------------------------------------------
-- |
-- Module      :  Untyped.Term
-- Copyright   :  (c) Thanos Tsouanas 2010
-- License     :  BSD
-- Maintainer  :  thanos@sians.org
-- Stability   :  experimental
--
-- Terms of the untyped system.
--
--------------------------------------------------------------------------
module Untyped.Term ( 
       -- * Data types
         Term(..)
       , Program
       -- * Relations
       , (@=)
       -- * Subterms and variables
       , subterms
       , variables
       , freeVariables
       , freeIn
       , notFreeIn
       -- * Properties of terms
       , isUnitVal
       , isNatVal
       , isBoolVal
       , isAbsVal
       , isVal
       -- * Supplamentary creators
       , natFromInt
       , abstract
       , apply
       -- ** Substitutions
       , (|->)
       , (@>)
       ) where
--------------------------------------------------------------------------
import Sidekick    ( passAny )
import List        ( union, (\\) )
--------------------------------------------------------------------------


-- | Definition of terms for this calculus.
--
-- /Beware/: this, as an instance of @Eq@, never heard of the alpha-conversion.
-- Use @(\@=)@ if you need to check for alpha-equivalence.
data Term = TmUnit               -- ^ Unit value.
          | TmTrue               -- ^ Boolean value true.
          | TmFalse              -- ^ Boolean value false.
          | TmIf Term Term Term  -- ^ Branching.
          | TmZero               -- ^ Natural number zero.
          | TmSucc Term          -- ^ Successor.
          | TmPred Term          -- ^ Predecessor.
          | TmIsZero Term        -- ^ Zero test.
          | TmVar String         -- ^ Variable.
          | TmAbs String Term    -- ^ Lambda abstraction.
          | TmApp Term Term      -- ^ Term application.
          | TmStop               -- ^ Stop of evaluation meta-term.
          | TmLoop               -- ^ A term that loops infinitely.
          deriving (Eq, Show)    -- Beware, this Eq never heard of the alpha-conversion.
                                 -- Use (@=) if you need to check for alpha-equivalence.

-- | A list of terms that represent a program.
type Program = [Term]


-- | Turn an integral number to the corresponding 'Nat' term.
natFromInt :: Integral t => t -> Term
natFromInt 0        = TmZero
natFromInt (n + 1)  = TmSucc (natFromInt n)
natFromInt _        = error "Negative nat?!"


-- | Lambda-abstract a given variable term in a given term.
abstract :: Term -> Term -> Term
abstract (TmVar x) t  = TmAbs x t
abstract _         _  = error "can only abstract variable terms"


-- | Turn a list of terms into a single application term.
-- (Like @foldr1 TmApp types@ but returns @unit@ if empty.)
apply :: [Term] -> Term
apply []  = TmUnit
apply ts  = foldl1 TmApp ts


{- Properties and relations -}

-- | alpha-conversion equivalence.
(@=) :: Term -> Term -> Bool
t @= s = if t == s then True else case (t, s) of 
    ( t1 `TmApp` t2 , s1 `TmApp` s2 )  -> t1 @= s1 && t2 @= s2
    ( TmSucc t'     , TmSucc s'     )  -> t' @= s'
    ( TmPred t'     , TmPred s'     )  -> t' @= s'
    ( TmIsZero t'   , TmPred s'     )  -> t' @= s'
    ( TmAbs x t'    , TmAbs y s'    )  -> t' @= (y @> x) s'
    _________________________________  -> False


valueChecks :: [Term -> Bool]
valueChecks  = [isUnitVal, isBoolVal, isNatVal, isAbsVal]

-- | Checks if the given term is a unit value.
isUnitVal :: Term -> Bool
isUnitVal TmUnit     = True
isUnitVal _          = False

-- | Checks if the given term is a boolean value.
isBoolVal :: Term -> Bool
isBoolVal TmTrue     = True
isBoolVal TmFalse    = True
isBoolVal _          = False

-- | Checks if the given term is a natural number value.
isNatVal :: Term -> Bool
isNatVal TmZero      = True
isNatVal (TmSucc t)  = isNatVal t
isNatVal _           = False

-- | Checks if the given term is an abstraction value.
isAbsVal :: Term -> Bool
isAbsVal TmAbs {}    = True
isAbsVal _           = False

-- | Checks if the given term is a value.
isVal :: Term -> Bool
isVal  = passAny valueChecks


{- Variables -}

-- | List of all subterms of the given term.
subterms :: Term -> [Term]
subterms term = case term of
    TmVar x        -> [term]
    TmAbs _ t      -> term : subterms t
    t1 `TmApp` t2  -> term : (foldl1 union $ map subterms [t1, t2])
    TmIf t t1 t2   -> term : (foldl1 union $ map subterms [t, t1, t2])
    TmSucc t       -> term : subterms t
    TmPred t       -> term : subterms t
    TmIsZero t     -> term : subterms t
    _____________  -> [term]


-- | All variables that occur in the given term.
variables :: Term -> [String]
variables term = case term of
    TmVar x        -> [x]
    TmAbs _ t      -> variables t
    t1 `TmApp` t2  -> foldl1 union $ map variables [t1, t2]
    TmIf t t1 t2   -> foldl1 union $ map variables [t, t1, t2]
    TmSucc t       -> variables t
    TmPred t       -> variables t
    TmIsZero t     -> variables t
    _____________  -> []


-- | All variables that occur /free/ in the given term.
freeVariables :: Term -> [String]
freeVariables term = case term of
    TmVar x        -> [x]
    TmAbs x t      -> (freeVariables t) \\ [x]
    t1 `TmApp` t2  -> foldl1 union $ map freeVariables [t1, t2]
    TmIf t t1 t2   -> foldl1 union $ map freeVariables [t, t1, t2]
    TmSucc t       -> freeVariables t
    TmPred t       -> freeVariables t
    TmIsZero t     -> freeVariables t
    _____________  -> []


-- | Handy shortcut for \"@x@ in FV(@t@)\".
freeIn :: String -> Term -> Bool
x `freeIn` t = x `elem` (freeVariables t)

-- | \"x not in FV(@t@)\".  What; this is handy too!
notFreeIn :: String -> Term -> Bool
x `notFreeIn` t = not (x `freeIn` t)


{- Variables names -}

niceNames :: [String]
niceNames = ["x", "y", "z"]

-- | A list of nice names for variables, using primes.
--
-- /BEWARE!/  Infinite list: @[x, y, z, x', y', z', x'', y'', z'', ...]@
niceNamesPrimed :: [String]
niceNamesPrimed = zipWith (++) names decorators
    where names      = cycle niceNames
          decorators = [ replicate n '\'' | n <- [0..]]

-- | A list of nice names for variables, using numeric indices.
--
-- /BEWARE!/  Infinite list: @[x0, y0, z0, x1, y1, z1, x2, y2, z2, ...]@
niceNamesIndexed :: [String]
niceNamesIndexed = zipWith (++) names decorators
    where names      = cycle niceNames
          decorators = map show [ n `div` (length niceNames) | n <- [0..] ]

-- | Something like a Hartogs operator for finding fresh variables.
hartogs :: [String] -> String
hartogs taken = head $ dropWhile (`elem` taken) niceNamesIndexed


{- Substitutions and all that Jazz -}

-- | Substitution in lambda-calculus terms.
--
-- @(x |-> s) t@ is the term we get if we replace every free occurrence
-- of @x@ in @t@ with @s@.
(|->) :: String -> Term -> Term -> Term

(x |-> s) term = case term of
    TmVar y              -> if x == y then s else term
    TmSucc t             -> TmSucc t'       where t' = (x |-> s) t
    TmPred t             -> TmPred t'       where t' = (x |-> s) t
    TmIsZero t           -> TmIsZero t'     where t' = (x |-> s) t
    t1 `TmApp` t2        -> t1' `TmApp` t2' where [t1', t2']     = map (x |-> s) [t1, t2]
    TmIf t t1 t2         -> TmIf t' t1' t2' where [t', t1', t2'] = map (x |-> s) [t, t1, t2]
    TmAbs y t
      | x == y           -> term
      | y `notFreeIn` s  -> TmAbs y ((x |-> s) t)
      | otherwise        -> (x |-> s) $ (y @> w) term
      where
        w        = hartogs usedvars
        usedvars = freeVariables s `union` variables t
    ___________________  -> term


-- | Renaming in the spirit of the alpha-conversion of lambda-calculus.
--
-- /BEWARE!/  This isn't safe: @w@ must be /correctly/ picked before-hand.
-- In fact, this is the most brain-dead substitution implementation.
(@>) :: String -> String -> Term -> Term
(x @> w) term = case term of
    TmSucc t       -> TmSucc t'        where t' = (x @> w) t
    TmPred t       -> TmPred t'        where t' = (x @> w) t
    TmIsZero t     -> TmIsZero t'      where t' = (x @> w) t
    t1 `TmApp` t2  -> t1' `TmApp` t2'  where [t1', t2']     = map (x @> w) [t1, t2]
    TmIf t t1 t2   -> TmIf t' t1' t2'  where [t', t1', t2'] = map (x @> w) [t, t1, t2]
    TmVar y        -> if (x == y) then (TmVar w) else term
    TmAbs y t      -> if (x == y) then (TmAbs w t') else (TmAbs y t')
                      where t' = (x @> w) t
    _____________  -> term