module Data.Config.Internal.Typecheck (typecheck) where
import Control.Exception
import Data.Foldable
import Data.Typeable
import Prelude
import Control.Monad.State.Strict
import qualified Data.Map.Strict as M
import Data.Text (Text, unpack)
import Data.Config.Internal.AST
import Data.Config.Internal.Scoped
import Data.Config.Internal.Typed
type TyM a = State TyState a
type Types = M.Map Text Type
data TyState
= TyState
{ _tyVarId :: !Int
, _tyConstrs :: ![Constraint]
, _tyErrors :: ![TyError]
, _tyMap :: !Types
}
data Constraint
= Equality (AST Scoped) (AST Scoped) Type Type
| Existence (AST Scoped) Text
data TyError
= Mismatch (AST Scoped) Type Type
| Undefined (AST Scoped) Text deriving Typeable
newtype TypecheckError = TypecheckError [TyError] deriving Typeable
instance Show TyError where
show (Mismatch s etyp ctyp)
= prop ++
":" ++
show pos ++
" Expecting " ++
show etyp ++
" but having " ++
show ctyp
where
prop = unpack $ scopeProp $ astTag s
pos = scopePos $ astTag s
show (Undefined s t)
= prop ++
":" ++
show pos ++
" Property " ++
unpack t ++
" is undefined"
where
prop = unpack $ scopeProp $ astTag s
pos = scopePos $ astTag s
instance Show TypecheckError where
show (TypecheckError xs)
= foldMap (\x -> show x ++ "\n") xs
instance Exception TyError
instance Exception TypecheckError
typecheck :: [Prop AST Scoped] -> Either SomeException (Types, [Prop AST Typed])
typecheck ps
= let (ps', s) = runState (typecheckProps ps) start
tys = _tyMap s in
case _tyErrors s of
errs | null errs -> Right (tys, ps')
| otherwise -> Left $ SomeException $ TypecheckError errs
where
start
= TyState
{ _tyVarId = resetVarId
, _tyConstrs = []
, _tyErrors = []
, _tyMap = M.empty
}
resetVarId :: Int
resetVarId = 1
typecheckProps :: [Prop AST Scoped] -> TyM [Prop AST Typed]
typecheckProps ps
= do ps' <- mapM typecheckProp ps
s <- get
let constrs = _tyConstrs s
typecheckConstrs constrs
return ps'
typecheckConstrs :: [Constraint] -> TyM ()
typecheckConstrs [] = return ()
typecheckConstrs (c:cs)
= do tys <- gets _tyMap
case c of
Equality a b (RefTy t) y ->
case M.lookup t tys of
Nothing ->
do tyReportError (Undefined a t)
typecheckConstrs cs
Just typ ->
do tyRegisterType t typ
typecheckConstrs (Equality a b typ y:cs)
Equality a b x y@(RefTy _) ->
typecheckConstrs (Equality b a y x:cs)
Equality a b x y ->
case checkType a b x y of
Right match
| match -> typecheckConstrs cs
| otherwise ->
do tyReportError (Mismatch a x y)
typecheckConstrs cs
_ -> error "impossible situation. typecheckConstrs"
Existence a t ->
case M.lookup t tys of
Nothing ->
do tyReportError (Undefined a t)
typecheckConstrs cs
_ -> typecheckConstrs cs
typecheckProp :: Prop AST Scoped -> TyM (Prop AST Typed)
typecheckProp (Prop n v)
= do v' <- typecheckAST v
let vtype = typedType $ astTag v'
tyRegisterType n vtype
tySetVarId resetVarId
return $ Prop n v'
typecheckAST :: AST Scoped -> TyM (AST Typed)
typecheckAST ast@(AST expr scope)
= case expr of
ID i -> return $ AST (ID i) (Typed (LitTy StringLit) scope)
STRING s -> return $ AST (STRING s) (Typed (LitTy StringLit) scope)
LIST xs -> typecheckList scope xs
SUBST s -> typecheckSubst ast s
MERGE l r -> typecheckMerge scope l r
OBJECT ps -> typecheckObject scope ps
typecheckSubst :: AST Scoped -> Text -> TyM (AST Typed)
typecheckSubst ast key
= do tyAddConstr (Existence ast key)
return $ AST (SUBST key) (Typed (RefTy key) (astTag ast))
typecheckList :: Scoped -> [AST Scoped] -> TyM (AST Typed)
typecheckList scope []
= do vid <- tyGetAndIncrVarId
let typ = ForAllTy vid (TyVarTy vid)
return $ AST (LIST []) (Typed (AppTy ListTy typ) scope)
typecheckList scope (x:xs)
= do x' <- typecheckAST x
tyxs <- typecheckList scope xs
let (LIST xs') = astExpr tyxs
xtype = typedType $ astTag x'
(AppTy _ xstype) = typedType $ astTag tyxs
typecheckType x (AST (LIST xs) scope) xtype xstype
return $ AST (LIST (x':xs')) (Typed (AppTy ListTy xtype) scope)
typecheckMerge :: Scoped -> AST Scoped -> AST Scoped -> TyM (AST Typed)
typecheckMerge scope x y
= do x' <- typecheckAST x
y' <- typecheckAST y
let xtype = typedType $ astTag x'
ytype = typedType $ astTag y'
typecheckType x y xtype ytype
return $ AST (MERGE x' y') (Typed xtype scope)
typecheckObject :: Scoped -> [Prop AST Scoped] -> TyM (AST Typed)
typecheckObject scope ps
= do ps' <- mapM typecheckProp ps
return $ AST (OBJECT ps') (Typed (LitTy ObjectLit) scope)
typecheckType :: AST Scoped -> AST Scoped -> Type -> Type -> TyM ()
typecheckType a b tyexp typ
= case checkType a b tyexp typ of
Left c -> tyAddConstr c
Right match
| match -> return ()
| otherwise -> tyReportError (Mismatch a tyexp typ)
checkType :: AST Scoped -> AST Scoped -> Type -> Type -> Either Constraint Bool
checkType a b x@(RefTy _) y = Left (Equality a b x y)
checkType a b x y@(RefTy _) = Left (Equality a b x y)
checkType _ _ (ForAllTy _ _) _ = Right True
checkType _ _ _ (ForAllTy _ _) = Right True
checkType a b (AppTy x xs) (AppTy y ys) = checkAppType a b x xs y ys
checkType _ _ x y = Right (x == y)
checkAppType :: AST Scoped
-> AST Scoped
-> Type
-> Type
-> Type
-> Type
-> Either Constraint Bool
checkAppType a b x xs y ys
| x == y = checkType a b xs ys
| otherwise = Right False
tyUpdateVarId :: (Int -> Int) -> TyState -> TyState
tyUpdateVarId k s
= let p = _tyVarId s in s { _tyVarId = k p }
tyUpdateErrors :: ([TyError] -> [TyError]) -> TyState -> TyState
tyUpdateErrors k s
= let p = _tyErrors s in s { _tyErrors = k p }
tyUpdateConstrs :: ([Constraint] -> [Constraint]) -> TyState -> TyState
tyUpdateConstrs k s
= let p = _tyConstrs s in s { _tyConstrs = k p }
tyUpdateTyMap :: (M.Map Text Type -> M.Map Text Type) -> TyState -> TyState
tyUpdateTyMap k s
= let p = _tyMap s in s { _tyMap = k p }
tyGetAndIncrVarId :: TyM Int
tyGetAndIncrVarId
= do i <- gets _tyVarId
modify (tyUpdateVarId succ)
return i
tySetVarId :: Int -> TyM ()
tySetVarId i = modify (tyUpdateVarId (const i))
tyAddConstr :: Constraint -> TyM ()
tyAddConstr c = modify (tyUpdateConstrs (c:))
tyReportError :: TyError -> TyM ()
tyReportError e = modify (tyUpdateErrors (e:))
tyRegisterType :: Text -> Type -> TyM ()
tyRegisterType k t = modify (tyUpdateTyMap (M.insert k t))