module DDC.Core.Fragment.Compliance
( complies
, compliesWithEnvs
, Complies)
where
import DDC.Core.Fragment.Feature
import DDC.Core.Fragment.Profile
import DDC.Core.Fragment.Error
import DDC.Core.Compounds
import DDC.Core.Predicates
import DDC.Core.Module
import DDC.Core.Exp
import Control.Monad
import Control.Applicative
import Data.Maybe
import DDC.Type.Env (Env)
import Data.Set (Set)
import qualified DDC.Type.Env as Env
import qualified Data.Set as Set
complies
:: (Ord n, Show n, Complies c)
=> Profile n
-> c a n
-> Maybe (Error a n)
complies profile thing
= compliesWithEnvs profile
(profilePrimKinds profile)
(profilePrimTypes profile)
thing
compliesWithEnvs
:: (Ord n, Show n, Complies c)
=> Profile n
-> Env.KindEnv n
-> Env.TypeEnv n
-> c a n
-> Maybe (Error a n)
compliesWithEnvs profile kenv tenv thing
= let merr = result
$ compliesX profile
kenv tenv
contextTop thing
in case merr of
Left err -> Just err
Right _ -> Nothing
class Complies (c :: * -> * -> *) where
compliesX
:: (Ord n, Show n)
=> Profile n
-> Env n
-> Env n
-> Context
-> c a n
-> CheckM a n
(Set n, Set n)
instance Complies Module where
compliesX profile kenv tenv context mm
= do let bs = [ BName n (typeOfImportSource isrc)
| (n, isrc) <- moduleImportValues mm ]
let tenv' = Env.extends bs tenv
compliesX profile kenv tenv' context (moduleBody mm)
instance Complies Exp where
compliesX profile kenv tenv context xx
= let has f = f $ profileFeatures profile
ok = return (Set.empty, Set.empty)
in case xx of
XVar _ u@(UName n)
| not $ Env.member u tenv
, not $ has featuresUnboundLevel0Vars
-> throw $ ErrorUndefinedVar n
| args <- fromMaybe 0 $ contextFunArgs context
, Just t <- Env.lookup u tenv
, arity <- arityOfType t
, args < arity
, not $ has featuresPartialApplication
-> throw $ ErrorUnsupported PartialApplication
| otherwise
-> return (Set.empty, Set.singleton n)
XVar _ u@(UPrim n t)
| not $ Env.member u (profilePrimTypes profile)
-> throw $ ErrorUndefinedPrim n
| args <- fromMaybe 0 $ contextFunArgs context
, arity <- arityOfType t
, args < arity
, not $ has featuresPartialPrims
-> throw $ ErrorUnsupported PartialPrims
| otherwise
-> return (Set.empty, Set.empty)
XVar{} -> ok
XCon{} -> ok
XLAM _ b x
| contextAbsBody context
, not $ has featuresNestedFunctions
-> throw $ ErrorUnsupported NestedFunctions
| otherwise
-> do
let context'
| isXLAM x || isXLam x = context
| otherwise = setBody context
(tUsed, vUsed) <- compliesX profile
(Env.extend b kenv) tenv
context' x
tUsed' <- checkBind profile kenv b tUsed
return (tUsed', vUsed)
XLam _ b x
| contextAbsBody context
, not $ has featuresNestedFunctions
-> throw $ ErrorUnsupported NestedFunctions
| otherwise
-> do
let context'
| isXLAM x || isXLam x = context
| otherwise = setBody context
(tUsed, vUsed) <- compliesX profile
kenv (Env.extend b tenv)
context' x
vUsed' <- checkBind profile tenv b vUsed
return (tUsed, vUsed')
XApp _ x1 (XType _ t2)
| profileTypeIsUnboxed profile t2
, Nothing <- takeXPrimApps xx
-> throw $ ErrorUnsupported UnboxedInstantiation
| otherwise
-> do checkFunction profile x1
compliesX profile kenv tenv (addArg context) x1
XApp _ x1 XWitness{}
-> do checkFunction profile x1
compliesX profile kenv tenv (addArg context) x1
XApp _ x1 x2
-> do checkFunction profile x1
(tUsed1, vUsed1) <- compliesX profile kenv tenv (addArg context) x1
(tUsed2, vUsed2) <- compliesX profile kenv tenv context x2
return ( Set.union tUsed1 tUsed2
, Set.union vUsed1 vUsed2)
XLet _ (LLet b1 x1) x2
-> do let tenv' = Env.extend b1 tenv
(tUsed1, vUsed1) <- compliesX profile kenv tenv (reset context) x1
(tUsed2, vUsed2) <- compliesX profile kenv tenv' (reset context) x2
vUsed2' <- checkBind profile tenv b1 vUsed2
return ( Set.union tUsed1 tUsed2
, Set.union vUsed1 vUsed2')
XLet _ (LRec bxs) x2
-> do let (bs, xs) = unzip bxs
let tenv' = Env.extends bs tenv
(tUseds1, vUseds1)
<- liftM unzip
$ mapM (compliesX profile kenv tenv' (reset context))
xs
(tUsed2, vUsed2) <- compliesX profile kenv tenv' (reset context) x2
let tUseds = Set.unions (tUsed2 : tUseds1)
let vUseds = Set.unions (vUsed2 : vUseds1)
vUseds' <- checkBinds profile tenv bs vUseds
return (tUseds, vUseds')
XLet _ (LPrivate rs _ bs) x2
-> do (tUsed2, vUsed2)
<- compliesX profile (Env.extends rs kenv)
(Env.extends bs tenv)
(reset context) x2
return (tUsed2, vUsed2)
XLet _ (LWithRegion _) x2
-> do (tUsed2, vUsed2) <- compliesX profile kenv tenv
(reset context) x2
return (tUsed2, vUsed2)
XCase _ x1 alts
-> do (tUsed1, vUsed1)
<- compliesX profile kenv tenv (reset context) x1
(tUseds2, vUseds2) <- liftM unzip
$ mapM (compliesX profile kenv tenv (reset context)) alts
return ( Set.unions $ tUsed1 : tUseds2
, Set.unions $ vUsed1 : vUseds2)
XCast _ _ x -> compliesX profile kenv tenv (reset context) x
XType _ t -> throw $ ErrorNakedType t
XWitness _ w -> throw $ ErrorNakedWitness w
instance Complies Alt where
compliesX profile kenv tenv context aa
= case aa of
AAlt PDefault x
-> do (tUsed1, vUsed1) <- compliesX profile kenv tenv
(reset context) x
return (tUsed1, vUsed1)
AAlt (PData _ bs) x
-> do (tUsed1, vUsed1) <- compliesX profile kenv (Env.extends bs tenv)
(reset context) x
vUsed1' <- checkBinds profile tenv bs vUsed1
return (tUsed1, vUsed1')
checkBind
:: Ord n
=> Profile n
-> Env n
-> Bind n
-> Set n
-> CheckM a n (Set n)
checkBind profile env bb used
= let has f = f $ profileFeatures profile
in case bb of
BName n _
| not $ Set.member n used
, not $ has featuresUnusedBindings
-> throw $ ErrorUnusedBind n
| Env.memberBind bb env
, not $ has featuresNameShadowing
-> throw $ ErrorShadowedBind n
| otherwise
-> return $ Set.delete n used
BAnon{}
| not $ has featuresDebruijnBinders
-> throw $ ErrorUnsupported DebruijnBinders
_ -> return used
checkBinds
:: Ord n
=> Profile n
-> Env n -> [Bind n] -> Set n
-> CheckM a n (Set n)
checkBinds profile env bs used
= case bs of
[] -> return used
(b : bs')
-> do used' <- checkBinds profile env bs' used
checkBind profile env b used'
checkFunction :: Profile n -> Exp a n -> CheckM a n ()
checkFunction profile xx
= let has f = f $ profileFeatures profile
ok = return ()
in case xx of
XVar{} -> ok
XCon{} -> ok
XApp{} -> ok
XCast{} -> ok
_
| has featuresGeneralApplication -> return ()
| otherwise -> throw $ ErrorUnsupported GeneralApplication
data Context
= Context
{ contextAbsBody :: Bool
, contextFunArgs :: Maybe Int }
deriving (Eq, Show)
contextTop :: Context
contextTop
= Context
{ contextAbsBody = False
, contextFunArgs = Nothing }
setBody :: Context -> Context
setBody context = context { contextAbsBody = True }
addArg :: Context -> Context
addArg context
= case contextFunArgs context of
Nothing -> context { contextFunArgs = Just 1 }
Just args -> context { contextFunArgs = Just (args + 1) }
reset :: Context -> Context
reset context = context { contextFunArgs = Nothing }
data CheckM a n x
= CheckM (Either (Error a n) x)
instance Functor (CheckM s err) where
fmap = liftM
instance Applicative (CheckM s err) where
(<*>) = ap
pure = return
instance Monad (CheckM a n) where
return x = CheckM (Right x)
(>>=) m f
= case m of
CheckM (Left err) -> CheckM (Left err)
CheckM (Right x) -> f x
throw :: Error a n -> CheckM a n x
throw e = CheckM $ Left e
result :: CheckM a n x -> Either (Error a n) x
result (CheckM r) = r