-- Needed in general
{-# LANGUAGE GADTs, KindSignatures #-}

-- Needed for Show instances
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}

----------------------------------------------------------------
--                                                    2011.06.14
-- |
-- Module      :  DeBruijn_simple
-- Copyright   :  Copyright (c) 2009 wren ng thornton
-- License     :  BSD
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  non-portable (GADTs,...)
--
-- This module provides a type-safe de Bruijn GADT implementation.
--
----------------------------------------------------------------
module DeBruijn_simple
    (
    -- * Typing contexts
      Ctx(..)
    -- * Typed de Bruijn indices
    , Ix(..)
    , ixToInteger
    , eq_Ix
    -- * Variable binding environments
    , Env(..)
    , lookupEnv
    , curryEnv
    -- * Object language terms
    , DTerm(..)
    , eval
    ) where

import Control.Applicative

----------------------------------------------------------------
----------------------------------------------------------------

-- We don't actually need this anywhere...
-- | A term-level representation for typing contexts.
data Ctx :: * -> * where
    ZeroCtx  ::          Ctx ()
    SuccCtx  :: Ctx r -> Ctx (r,a)
    -- TODO: we probably want @a@ to be Typeable, or otherwise representable.


----------------------------------------------------------------
-- | Typed de Bruijn indices, aka variable names. The @a@ is the
-- type of the term that the variable represents, and the pairs are
-- a stack of types (one for each index) which serves as the typing
-- context, usually called Γ. The typing context of the index
-- and the binding environment will be unified in the evaluation
-- function. @Zero@ refers to the top element of the typing
-- context\/binding environment (which must be non-empty); and each
-- @Succ@ goes one level deeper on the stack.

data Ix    :: * -> * -> * where
    ZeroIx ::           Ix (r,a) a
    SuccIx :: Ix r a -> Ix (r,b) a

instance Show (Ix r a) where
    show = ("#"++) . show . ixToInteger

instance Eq (Ix r a) where
    (==) = eq_Ix

{-
-- | Case elimination on 'Ix'. Using this is often more trouble
-- than it's worth, since you'll generally need to use explicitly
-- named arguments so that you can give them polymorphic type
-- signatures.
elim_Ix
    :: forall r a z
    .  (forall r'.   (r ~ (r',a)) => z)
    -> (forall r' b. (r ~ (r',b)) => Ix r' a -> z)
    -> Ix r a -> z
elim_Ix z _ ZeroIx     = z
elim_Ix _ s (SuccIx n) = s n
-}


-- | Convert an 'Ix' into a plain integer.
ixToInteger :: Ix r a -> Integer
ixToInteger = go 0
    where
    -- This signature is needed to avoid the warning:
    -- "GADT pattern match in non-rigid context"
    go :: Integer -> Ix r a -> Integer
    go i ZeroIx     = i
    go i (SuccIx m) = (go $! i+1) m


-- | Heterogeneous equality for 'Ix'. Note, this only ensures that
-- the indices are equal as integers; it does not ensure that their
-- type environments are equal. (Though we do require that the types
-- of the values they're bound to to be the same, i.e. @(a ~ a)@.)
eq_Ix :: Ix l a -> Ix r a -> Bool
eq_Ix ZeroIx     ZeroIx     = True
eq_Ix (SuccIx m) (SuccIx n) = eq_Ix m n
eq_Ix _          _          = False


----------------------------------------------------------------
-- | Typed binding environments, aka heterogeneous (snoc) lists.
-- This is the stack of values that 'Ix' indexes into. The @i@ is
-- an \"idiom\" (i.e., an 'Applicative') which lets the values carry
-- arbitrary side-effects or interpretations.
--
-- N.B., the Show instance prints the environment in snoc-list order;
-- that is, with the EmptyEnv at the left and the ZeroIx element at the
-- right.

data Env     :: * -> * where
    EmptyEnv ::               Env ()
    PushEnv  :: Env r -> a -> Env (r,a)

instance Show (Env ()) where
    show = const "<>"

instance (Show (Env r), Show a) => Show (Env (r,a)) where
    show (PushEnv env v) =
        -- Can't use @case env of@ because it informs us about types too much
        ( case show env of
          "<>"    -> "<"
          showEnv -> init showEnv ++ "," ) ++ show v ++ ">"
    
    -- Older GHCs still require this branch; newer ones warn about overlap
    --show _ = absurd "cannot construct @EmptyEnv :: Env i (r,a)@"


-- | Look up an index in the binding environment.
lookupEnv :: Ix r a -> Env r -> a
lookupEnv _          EmptyEnv        = absurd "the only @Ix () a@ is bottom"
lookupEnv ZeroIx     (PushEnv _   v) = v
lookupEnv (SuccIx n) (PushEnv env _) = lookupEnv n env


-- | A variant of 'error' for pattern matches which are impossible.
absurd :: String -> a
absurd msg = error $ "Absurd: "++msg


----------------------------------------------------------------
-- | Terms are constants, variables, applications, lambda abstractions,
-- and let-bindings. Because of 'zipEnv', side-effects occur only
-- once, so let-bindings add no formal power in that regard. The
-- reason to use the @DTerm@ let-binding rather than Haskell's
-- let-binding is to share the work of 'eval'.

data DTerm :: * -> * -> * where
    DCon   :: {- Show a => -} a             -> DTerm r a
    DVar   :: Ix r a                        -> DTerm r a
    DApp   :: DTerm r (a -> b) -> DTerm r a -> DTerm r b
    DLam   :: DTerm (r, a) b                -> DTerm r (a -> b)

{-
-- Using this instance means we cannot use @DCon@ to lift Haskell
-- functions into DTerm functions, since we can't show functions.
instance Show (DTerm r a) where
    show (DCon c)     = show c
    show (DVar n)     = show n
    show (DApp e1 e2) = "("++ show e1 ++" $ "++ show e2 ++")"
    show (DLam e1)    = "(\\_ -> "++ show e1 ++")"
-}


eval :: DTerm r a -> Env r -> a
eval (DCon v)     = const v
eval (DVar n)     = lookupEnv n
eval (DApp e1 e2) = eval e1 <*> eval e2
eval (DLam e1)    = curryEnv (eval e1)


-- | A variant of `curry` if we think of Env like (,).
curryEnv :: (Env (r,a) -> b) -> (Env r -> a -> b)
curryEnv = (... PushEnv)
    where
    (...) = (.) . (.)

----------------------------------------------------------------
----------------------------------------------------------- fin.