gistfile1.hs

module Infer where

import Control.Monad.State
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap

data Var = V {-# UNPACK #-} !Int (Maybe String)

data HM = HM
    { nextVar :: {-# UNPACK #-} !Int
    , kinds :: IntMap (E Kind)
    , types :: IntMap (E Type)
--  , exprs :: IntMap (E Expr)

    -- simple constraint handling rules
    , views :: IntMap (E Type) 
    , joins :: [(Var,Var,Var)]
    }

fresh :: Maybe String -> Subst Var
fresh name = do 
    s <- get
    let !i = nextVar s + 1
    put (s { nextVar = i })
    return $! V i name

type Subst a = State HM 

data Super -- this space intentionally left blank!
data Kind  -- this space intentionally left blank!
data Type  -- this space intentionally left blank!
data Term  -- this space intentionally left blank!

type family Sort s
type instance Sort Expr = Type
type instance Sort Type = Kind
type instance Sort Kind = Super

data E s where
    Box        :: E Super
    Rho        :: E Kind
    Star       :: E Kind                     
    (:->)      :: E Kind -> E Kind -> E Kind
    ApT        :: E Type -> E Type -> E Type
    Arrow      :: E Type            -- :: Star -> Star -> Star
    Sig        :: E a -> E (Sort a) -> E a
    Var        :: Var -> E a        -- :: a
    Int        :: E Type            -- :: Star
    Relation   :: E Type            -- :: Rho -> Star
    Empty      :: E Type            -- :: Rho
    Ellipsis   :: E Type            -- :: Rho
--  Field      :: Name -> E Type  -- :: Star -> Rho -> Rho
    Field      :: Name -> E Type  -- :: Star -> Rho -> Rho
--  Fresh      :: (Name -> E Term) -> E Term  
    Lam        :: Maybe String -> Maybe Type -> (E Term -> E Term) -> E Term
    Join       :: E Term -- :: Relation a -> Relation b -> Relation (unify a b)
    View       :: E Type -> E Term  -- :: Type -> Relation a -> Relation b

class Env a where
    getEnv   :: HM -> IntMap (E a) 
    putEnv   :: HM -> IntMap (E a) -> HM 

lookup :: Env a => Var -> Subst (E a)
lookup v = do
    m <- gets getEnv
    fromMaybe (Var v) <$> IntMap.lookup (varid v) m

class Env a => Unifiable a where
    unify    :: E a -> E a -> Subst ()
    subst    :: E a -> Subst (E a)

unifyVar :: Unifiable a => Var -> E a -> Subst ()
...

instance Env Kind where
    getEnv = kinds
    putEnv hm m = hm { kinds = m }

instance Unifiable Kinds where
    unify Star Star = return ()
    unify Rho Rho = return ()
    unify (a :-> b) (a' :-> b') = do
        unify a a'
        unify b b'
    unify (Var v) x = unifyVar v x
    unify x (Var v) = unifyVar v x
    unify _ _ = fail "kind mismatch"

    subst (Var v) = subst (lookup v)
    subst Star = return Star
    subst Rho = return Rho
    subst (a :-> b) = (:->) <$> subst a <*> subst b
    

instance Env Type where
    getEnv = types
    putEnv hm m = hm { types = m }

instance Unifiable Types where
    unify = ...

-- instance Env Expr where
--    getEnv = exprs
--    putEnv hm m = hm { exprs = m } 

infer :: Env a => E a -> Subst (E (Sort a))
infer Rho = return Box
infer Star = return Box
infer (Sig e t) = do
    check e t -- flip to checking rather than inferring
    return t
infer Arrow = return (Star `KArrow` Star `KArrow` Star)
infer (ApT f x) = do
    (a :-> b) <- infer f 
    a' <- infer x
    unify a a'
    return b
infer (Lam a mt f) = do
    sigma <- fresh a
    case mt of
        Just sigma' -> unify sigma sigma'
        Nothing -> return ()
    tau <- infer (f sigma)
    return (Arrow `ApT` sigma `ApT` tau)
infer (Var v)   = subst v
infer Int       = return Star
infer Relation  = return (Rho :-> Star)
infer Empty     = return Rho
infer Ellipsis  = return Rho
infer (Field n) = return (Star :-> Rho :-> Star)
infer (View b)  = do
    a <- fresh Nothing
    check a Rho
    check b Rho
    modify $ \s -> { views = insert (varId a) b (views s) } 
    return $ Arrow `ApT` (Relation `ApT` a) `ApT` (Relation `ApT` b)
infer Join = do
    a <- fresh Nothing
    b <- fresh Nothing
    c <- fresh Nothing
    unify a Rho
    unify b Rho
    unify c Rho
    modify $ \s -> s { joins = (a,b,c) : joins s } 
    return $ Arrow `ApT` (Relation `ApT` Var a) `ApT` (Arrow `ApT` (Relation `ApT` Var b) `ApT` (Relation `ApT` Var c))

check :: Env a -> E a -> E (Sort a) -> Subst ()