module DDC.Core.Lite.Convert
( saltOfLiteModule
, Error(..))
where
import DDC.Core.Lite.Convert.Data
import DDC.Core.Lite.Convert.Type
import DDC.Core.Lite.Convert.Base
import DDC.Core.Salt.Convert.Init
import DDC.Core.Salt.Platform
import DDC.Core.Module
import DDC.Core.Compounds
import DDC.Core.Predicates
import DDC.Core.Exp
import DDC.Type.Universe
import DDC.Type.DataDef
import DDC.Control.Monad.Check (throw, result)
import DDC.Core.Check (AnTEC(..))
import DDC.Type.Env (KindEnv, TypeEnv)
import qualified DDC.Core.Lite.Name as L
import qualified DDC.Core.Salt.Runtime as S
import qualified DDC.Core.Salt.Name as S
import qualified DDC.Core.Salt.Compounds as S
import qualified DDC.Type.Env as Env
import qualified Data.Map as Map
import Control.Monad
import Data.Maybe
saltOfLiteModule
:: Show a
=> Platform
-> S.Config
-> DataDefs L.Name
-> KindEnv L.Name
-> TypeEnv L.Name
-> Module (AnTEC a L.Name) L.Name
-> Either (Error a) (Module a S.Name)
saltOfLiteModule platform runConfig defs kenv tenv mm
=
result $ convertM platform runConfig defs kenv tenv mm
convertM
:: Show a
=> Platform
-> S.Config
-> DataDefs L.Name
-> KindEnv L.Name
-> TypeEnv L.Name
-> Module (AnTEC a L.Name) L.Name
-> ConvertM a (Module a S.Name)
convertM pp runConfig defs kenv tenv mm
= do
tsExports'
<- liftM Map.fromList
$ mapM convertExportM
$ Map.toList
$ moduleExportTypes mm
tsImports'
<- liftM Map.fromList
$ mapM convertImportM
$ Map.toList
$ moduleImportTypes mm
let ntsImports = [(BName n t) | (n, (_, t)) <- Map.toList $ moduleImportTypes mm]
let tenv' = Env.extends ntsImports tenv
x1 <- convertExpX ExpTop pp defs kenv tenv' $ moduleBody mm
let Just a = takeAnnotOfExp x1
let (lts', _) = splitXLets x1
let x2 = xLets a lts' (xUnit a)
let mm_salt
= ModuleCore
{ moduleName = moduleName mm
, moduleExportKinds = Map.empty
, moduleExportTypes = tsExports'
, moduleImportKinds = S.runtimeImportKinds
, moduleImportTypes = Map.union S.runtimeImportTypes tsImports'
, moduleBody = x2 }
mm_init <- case initRuntime runConfig mm_salt of
Nothing -> throw ErrorMainHasNoMain
Just mm' -> return mm'
return $ mm_init
convertExportM
:: (L.Name, Type L.Name)
-> ConvertM a (S.Name, Type S.Name)
convertExportM (n, t)
= do n' <- convertBindNameM n
t' <- convertT Env.empty t
return (n', t')
convertImportM
:: (L.Name, (QualName L.Name, Type L.Name))
-> ConvertM a (S.Name, (QualName S.Name, Type S.Name))
convertImportM (n, (qn, t))
= do n' <- convertBindNameM n
qn' <- convertQualNameM qn
t' <- convertT Env.empty t
return (n', (qn', t'))
convertQualNameM
:: QualName L.Name
-> ConvertM a (QualName S.Name)
convertQualNameM (QualName mn n)
= do n' <- convertBindNameM n
return $ QualName mn n'
data ExpContext
= ExpTop
| ExpFun
| ExpBody
| ExpBind
| ExpArg
deriving (Show, Eq, Ord)
convertExpX
:: Show a
=> ExpContext
-> Platform
-> DataDefs L.Name
-> KindEnv L.Name
-> TypeEnv L.Name
-> Exp (AnTEC a L.Name) L.Name
-> ConvertM a (Exp a S.Name)
convertExpX ctx pp defs kenv tenv xx
= let downArgX = convertExpX ExpArg pp defs kenv tenv
downCtorAppX = convertCtorAppX pp defs kenv tenv
in case xx of
XVar _ UIx{}
-> throw $ ErrorMalformed
$ "Cannot convert program with anonymous value binders."
XVar a u
-> do let a' = annotTail a
u' <- convertU u
return $ XVar a' u'
XCon a u
-> do let a' = annotTail a
xx' <- convertCtor pp defs kenv tenv a' u
return xx'
XLAM a b x
| ExpFun <- ctx
, (isRegionKind $ typeOfBind b)
|| (isDataKind $ typeOfBind b)
-> do let a' = annotTail a
b' <- convertB kenv b
let kenv' = Env.extend b kenv
x' <- convertExpX ctx pp defs kenv' tenv x
return $ XLAM a' b' x'
| ExpFun <- ctx
-> do let kenv' = Env.extend b kenv
convertExpX ctx pp defs kenv' tenv x
| otherwise
-> throw $ ErrorMalformed
$ "Cannot convert XLAM in this context " ++ show ctx
XLam a b x
| ExpFun <- ctx
-> let tenv' = Env.extend b tenv
in case universeFromType1 kenv (typeOfBind b) of
Just UniverseData
-> liftM3 XLam
(return $ annotTail a)
(convertB kenv b)
(convertExpX ctx pp defs kenv tenv' x)
Just UniverseWitness
-> liftM3 XLam
(return $ annotTail a)
(convertB kenv b)
(convertExpX ctx pp defs kenv tenv' x)
_ -> throw $ ErrorMalformed
$ "Invalid universe for XLam binder: " ++ show b
| otherwise
-> throw $ ErrorMalformed
$ "Cannot convert XLam in this context " ++ show ctx
XApp a xa xb
| (x1, xsArgs) <- takeXApps1 xa xb
, XCon _ dc <- x1
-> downCtorAppX a dc xsArgs
XApp a xa xb
| (x1, xsArgs) <- takeXApps1 xa xb
, XVar _ UPrim{} <- x1
-> do x1' <- downArgX x1
xsArgs' <- mapM downArgX xsArgs
return $ xApps (annotTail a) x1' xsArgs'
XApp (AnTEC _t _ _ a') xa xb
| (x1, xsArgs) <- takeXApps1 xa xb
-> do x1' <- downArgX x1
xsArgs' <- mapM downArgX xsArgs
return $ xApps a' x1' xsArgs'
XLet a lts x2
| ctx <= ExpBind
-> do
lts' <- convertLetsX pp defs kenv tenv lts
let (bs1, bs0) = bindsOfLets lts
let kenv' = Env.extends bs1 kenv
let tenv' = Env.extends bs0 tenv
x2' <- convertExpX ExpBody pp defs kenv' tenv' x2
return $ XLet (annotTail a) lts' x2'
XLet{}
-> throw $ ErrorNotNormalized "Unexpected let-expression."
XCase (AnTEC _ _ _ a') xScrut@(XVar (AnTEC tScrut _ _ _) uScrut) alts
| TCon (TyConBound (UPrim nType _) _) <- tScrut
, L.NamePrimTyCon _ <- nType
-> do xScrut' <- convertExpX ExpArg pp defs kenv tenv xScrut
alts' <- mapM (convertAlt (min ctx ExpBody) pp defs kenv tenv a' uScrut tScrut)
alts
return $ XCase a' xScrut' alts'
XCase (AnTEC tX _ _ a') xScrut@(XVar (AnTEC tScrut _ _ _) uScrut) alts
| TCon _ : _ <- takeTApps tScrut
-> do x' <- convertExpX ExpArg pp defs kenv tenv xScrut
tX' <- convertT kenv tX
alts' <- mapM (convertAlt (min ctx ExpBody) pp defs kenv tenv a' uScrut tScrut)
alts
let asDefault
| any isPDefault [p | AAlt p _ <- alts]
= []
| otherwise
= [AAlt PDefault (S.xFail a' tX')]
tScrut' <- convertT kenv tScrut
let tPrime = fromMaybe S.rTop
$ takePrimeRegion tScrut'
return $ XCase a' (S.xGetTag a' tPrime x')
$ alts' ++ asDefault
XCase{}
-> throw $ ErrorNotNormalized ("Invalid case expression.")
XCast _ _ x
-> convertExpX (min ctx ExpBody) pp defs kenv tenv x
XType t
| ExpArg <- ctx -> liftM XType (convertT kenv t)
| otherwise -> throw $ ErrorNotNormalized ("Unexpected type expresison.")
XWitness w
| ExpArg <- ctx -> liftM XWitness (convertWitnessX kenv w)
| otherwise -> throw $ ErrorNotNormalized ("Unexpected witness expression.")
convertLetsX
:: Show a
=> Platform
-> DataDefs L.Name
-> KindEnv L.Name
-> TypeEnv L.Name
-> Lets (AnTEC a L.Name) L.Name
-> ConvertM a (Lets a S.Name)
convertLetsX pp defs kenv tenv lts
= case lts of
LRec bxs
-> do let tenv' = Env.extends (map fst bxs) tenv
let (bs, xs) = unzip bxs
bs' <- mapM (convertB kenv) bs
xs' <- mapM (convertExpX ExpFun pp defs kenv tenv') xs
return $ LRec $ zip bs' xs'
LLet LetStrict b x1
-> do let tenv' = Env.extend b tenv
b' <- convertB kenv b
x1' <- convertExpX ExpBind pp defs kenv tenv' x1
return $ LLet LetStrict b' x1'
LLet LetLazy{} _ _
-> throw $ ErrorMalformed "XLet lazy not handled yet"
LLetRegions b bs
-> do b' <- mapM (convertB kenv) b
let kenv' = Env.extends b kenv
bs' <- mapM (convertB kenv') bs
return $ LLetRegions b' bs'
LWithRegion{}
-> throw $ ErrorMalformed "LWithRegion should not appear in Lite code."
convertWitnessX
:: Show a
=> KindEnv L.Name
-> Witness L.Name
-> ConvertM a (Witness S.Name)
convertWitnessX kenv ww
= let down = convertWitnessX kenv
in case ww of
WVar n -> liftM WVar (convertU n)
WCon wc -> liftM WCon (convertWiConX kenv wc)
WApp w1 w2 -> liftM2 WApp (down w1) (down w2)
WJoin w1 w2 -> liftM2 WApp (down w1) (down w2)
WType t -> liftM WType (convertT kenv t)
convertWiConX
:: Show a
=> KindEnv L.Name
-> WiCon L.Name
-> ConvertM a (WiCon S.Name)
convertWiConX kenv wicon
= case wicon of
WiConBuiltin w
-> return $ WiConBuiltin w
WiConBound n t
-> liftM2 WiConBound
(convertU n)
(convertT kenv t)
convertCtorAppX
:: Show a
=> Platform
-> DataDefs L.Name
-> KindEnv L.Name
-> TypeEnv L.Name
-> AnTEC a L.Name
-> DaCon L.Name
-> [Exp (AnTEC a L.Name) L.Name]
-> ConvertM a (Exp a S.Name)
convertCtorAppX pp defs kenv tenv (AnTEC _ _ _ a) dc xsArgs
| Just (L.NameLitBool b) <- takeNameOfDaCon dc
, [] <- xsArgs
= return $ S.xBool a b
| Just (L.NameLitNat i) <- takeNameOfDaCon dc
, [] <- xsArgs
= return $ S.xNat a i
| Just (L.NameLitInt i) <- takeNameOfDaCon dc
, [] <- xsArgs
= return $ S.xInt a i
| Just (L.NameLitWord i bits) <- takeNameOfDaCon dc
, [] <- xsArgs
= return $ S.xWord a i bits
| DaConUnit <- daConName dc
= do return $ S.xAllocBoxed a S.rTop 0 (S.xNat a 0)
| Just nCtor <- takeNameOfDaCon dc
, Just ctorDef <- Map.lookup nCtor $ dataDefsCtors defs
, Just dataDef <- Map.lookup (dataCtorTypeName ctorDef) $ dataDefsTypes defs
= do
rPrime
<- case xsArgs of
[]
-> return S.rTop
XType (TVar u) : _
| Just tu <- Env.lookup u kenv
-> if isRegionKind tu
then do u' <- convertU u
return $ TVar u'
else return S.rTop
_ -> throw $ ErrorMalformed "Prime region variable is not in scope."
let makeFieldType x
= case takeAnnotOfExp x of
Nothing -> return Nothing
Just a' -> liftM Just $ convertT kenv (annotType a')
xsArgs' <- mapM (convertExpX ExpArg pp defs kenv tenv) xsArgs
tsArgs' <- mapM makeFieldType xsArgs
constructData pp kenv tenv a
dataDef ctorDef
rPrime xsArgs' tsArgs'
convertCtorAppX _ _ _ _ _ _nCtor _xsArgs
= throw $ ErrorMalformed "Invalid constructor application."
convertAlt
:: Show a
=> ExpContext
-> Platform
-> DataDefs L.Name
-> KindEnv L.Name
-> TypeEnv L.Name
-> a
-> Bound L.Name
-> Type L.Name
-> Alt (AnTEC a L.Name) L.Name
-> ConvertM a (Alt a S.Name)
convertAlt ctx pp defs kenv tenv a uScrut tScrut alt
= case alt of
AAlt PDefault x
-> do x' <- convertExpX ctx pp defs kenv tenv x
return $ AAlt PDefault x'
AAlt (PData dc []) x
| Just nCtor <- takeNameOfDaCon dc
, case nCtor of
L.NameLitInt{} -> True
L.NameLitWord{} -> True
L.NameLitBool{} -> True
_ -> False
-> do dc' <- convertDC kenv dc
xBody1 <- convertExpX ctx pp defs kenv tenv x
return $ AAlt (PData dc' []) xBody1
AAlt (PData dc []) x
| DaConUnit <- daConName dc
-> do xBody <- convertExpX ctx pp defs kenv tenv x
let dcTag = mkDaConAlg (S.NameLitTag 0) S.tTag
return $ AAlt (PData dcTag []) xBody
AAlt (PData dc bsFields) x
| Just nCtor <- takeNameOfDaCon dc
, Just ctorDef <- Map.lookup nCtor $ dataDefsCtors defs
-> do
let tenv' = Env.extends bsFields tenv
uScrut' <- convertU uScrut
let iTag = fromIntegral $ dataCtorTag ctorDef
let dcTag = mkDaConAlg (S.NameLitTag iTag) S.tTag
bsFields' <- mapM (convertB kenv) bsFields
xBody1 <- convertExpX ctx pp defs kenv tenv' x
tScrut' <- convertT kenv tScrut
let Just trPrime = takePrimeRegion tScrut'
xBody2 <- destructData pp a uScrut' ctorDef trPrime
bsFields' xBody1
return $ AAlt (PData dcTag []) xBody2
AAlt{}
-> throw ErrorInvalidAlt
convertCtor
:: Show a
=> Platform
-> DataDefs L.Name
-> KindEnv L.Name
-> TypeEnv L.Name
-> a
-> DaCon L.Name
-> ConvertM a (Exp a S.Name)
convertCtor pp defs kenv tenv a dc
| DaConUnit <- daConName dc
= return $ S.xAllocBoxed a S.rTop 0 (S.xNat a 0)
| Just n <- takeNameOfDaCon dc
= case n of
L.NameLitBool v -> return $ S.xBool a v
L.NameLitNat i -> return $ S.xNat a i
L.NameLitInt i -> return $ S.xInt a i
L.NameLitWord i bits -> return $ S.xWord a i bits
nCtor
| Just ctorDef <- Map.lookup nCtor $ dataDefsCtors defs
, Just dataDef <- Map.lookup (dataCtorTypeName ctorDef)
$ dataDefsTypes defs
-> do
let rPrime = S.rTop
constructData pp kenv tenv a dataDef ctorDef rPrime [] []
_ -> throw $ ErrorMalformed "Invalid constructor."
| otherwise
= throw $ ErrorMalformed "Invalid constructor."