Dependent.hs

import Control.Applicative

import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Error

import Text.Printf

data Step
    = Postulate Type
    | Definition Expr

data Expr
    = App Expr Expr
    | Universe Int
    | Var Name
    | (Name, Type) :=> Expr
    | (Name, Type) :-> Expr

    deriving (Show)

infixr 9 :->, :=>

type Type = Expr

data Name 
    = String String
    | Fresh  String Int
    | Dummy

    deriving (Eq)

instance Show Name where
    show name = case name of
        String s   ->  s
        Fresh  s n ->  s ++ show n
        Dummy      -> "_"

refresh name = case name of
    String s   -> Fresh  s  0
    Fresh  s n -> Fresh  s (n + 1)
    Dummy      -> Fresh "_" 0

type Env = [(Name, (Type, Maybe Expr))]

type C = StateT [Expr] (ErrorT String (Reader Env))

var = Var . String
name = String

test1, test2, test3 :: C Expr
test1 = return     $ (name "A", Universe 0) :-> (name "a" , var "A") :-> var "a"
test2 = typeOf     $ (name "A", Universe 0) :-> (name "a" , var "A") :-> var "a"
test3 = universeOf $ (name "A", Universe 0) :-> (name "a" , var "A") :-> var "a"

runC :: C a -> Either String a
runC ca = (`runReader` []) $ runErrorT $ ca `evalStateT` [] 

typeOf :: Expr -> C Expr
typeOf expr = case expr of
    App f x -> do
        x' <- typeOf x
        f' <- typeOf f

        case f' of 
            (a, a') :-> b' -> do
                (a' `alphaEqual` x')
                    `assert` printf "Cannot give %s to %s: %s =/=> %s"
                        (show x)
                        (show f)
                        (show x')
                        (show f')

                (a =:- x) $ normalize b'

            _ ->
                die $ printf "Cannot give %s to %s: non-functional type %s"
                    (show x)
                    (show f)
                    (show f')

    Universe k -> 
        return $ Universe (k + 1)

    Var name -> 
        lookupVarType name

    (a, a') :-> b -> do
        a'' <- typeOf a'
        b'  <- a =:- a' $ typeOf b

        return $ (a, a') :=> b'

    (a, a') :=> b -> 
        maxUniverse a' b

universeOf :: Expr -> C Expr
universeOf expr = case expr of
    App f x ->
        maxUniverse f x

    Universe k ->
        return $ Universe $ k + 1

    Var name ->
        universeOf =<< lookupVarType name

    (a, a') :-> b ->
        universeOfDep a a' b

    (a, a') :=> b ->
        universeOfDep a a' b

  where
    universeOfDep a a' b = do
        Universe a'' <- universeOf a'

        Universe b'' <- a =:- a' $ universeOf b

        return $ Universe $ max a'' b''

maxUniverse :: Expr -> Expr -> C Expr
maxUniverse x y = do
    Universe k <- universeOf x
    Universe i <- universeOf y
    
    return $ Universe $ max k i

lookupVarType :: Name -> C Type
lookupVarType name = do
    env <- ask

    case name `lookup` env of
        Just (t', _) -> 
            return t'
        
        _ -> 
            die $ printf "Variable %s unknown" (show name)
        
lookupVarValue :: Name -> C Expr
lookupVarValue name = do
    env <- ask

    case name `lookup` env of
        Just (type_, value) -> 
            case value of
                Just value -> return  value
                Nothing    -> return (Var name)
        
        _ -> 
            die $ printf "Variable %s unknown" (show name)
        
alphaEqual :: Expr -> Expr -> Bool
x `alphaEqual` y = case (x, y) of
    (App f x, App g y) -> True
        && f `alphaEqual` g 
        && x `alphaEqual` y

    (Universe k, Universe i) ->
        k == i

    (Var x, Var y) ->
        x == y

    (  (a, a') :-> b
     , (c, c') :-> d
     ) -> True
        && a' `alphaEqual` c'
        && b  `alphaEqual` (d `substantiate` (c, Var a))

    (  (a, a') :=> b
     , (c, c') :=> d
     ) -> True
        && a' `alphaEqual` c'
        && b  `alphaEqual` (d `substantiate` (c, Var a))

(=:-) :: Name -> Type -> C a -> C a
name =:- type_ = \child -> do
    env <- ask

    local ((name, (type_, Nothing)) :) $
        child

normalize :: Expr -> C Expr
normalize expr = case expr of
    App f x -> do
        modify (x :)
        normalize f

    Universe k ->
        return expr

    Var name ->
        lookupVarValue name

    (a, a') :-> b -> 
        normalizeDep a a' b

    (a, a') :=> b -> 
        normalizeDep a a' b

  where
    normalizeDep a a' b = do
        stack <- get

        case stack of
            (x : xs) -> do
                modify tail

                x' <- typeOf x

                (x' `alphaEqual` a')
                    `assert` printf "Cannot give %s to %s: %s =/= %s"
                        (show x)
                        (show expr)
                        (show x')
                        (show a')

                normalize $ b `substantiate` (a, x)

            [] ->
                normalize b

substantiate :: Expr -> (Name, Expr) -> Expr
body `substantiate` (name, value) =
    case body of
        App f x -> 
            App (recure f) (recure x)

        Universe k ->
            body

        Var name' ->
            case name == name' of
                True  -> value
                False -> body

        (a, a') :-> b ->
            substantiateDep a a' b

        (a, a') :=> b ->
            substantiateDep a a' b

  where
    substantiateDep a a' b =
        let 
            c = refresh a

            d = b `substantiate` (a, Var c)

        in recure d

    recure = (`substantiate` (name, value))

die = fail

infix 0 `assert`

assert condition message = 
    when (not condition) $ fail message