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, evalCheck)
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
=
evalCheck () $ 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' <- mapM convertExportM $ moduleExportValues mm
tsImports' <- mapM convertImportM $ moduleImportValues mm
let ntsImports = [BName n (typeOfImportSource isrc)
| (n, isrc) <- moduleImportTypes mm]
let tenv' = Env.extends ntsImports tenv
x1 <- convertExpX ExpTop pp defs kenv tenv' $ moduleBody mm
let a = annotOfExp x1
let (lts', _) = splitXLets x1
let x2 = xLets a lts' (xUnit a)
let mm_salt
= ModuleCore
{ moduleName = moduleName mm
, moduleExportTypes = []
, moduleExportValues = tsExports'
, moduleImportTypes = Map.toList S.runtimeImportKinds
, moduleImportValues = (Map.toList S.runtimeImportTypes) ++ tsImports'
, moduleDataDefsLocal = []
, moduleBody = x2 }
mm_init <- case initRuntime runConfig mm_salt of
Nothing -> throw ErrorMainHasNoMain
Just mm' -> return mm'
return $ mm_init
convertExportM
:: (L.Name, ExportSource L.Name)
-> ConvertM a (S.Name, ExportSource S.Name)
convertExportM (n, esrc)
= do n' <- convertBindNameM n
esrc' <- convertExportSourceM esrc
return (n', esrc')
convertExportSourceM
:: ExportSource L.Name
-> ConvertM a (ExportSource S.Name)
convertExportSourceM isrc
= case isrc of
ExportSourceLocal n t
-> do n' <- convertBindNameM n
t' <- convertT Env.empty t
return $ ExportSourceLocal n' t'
ExportSourceLocalNoType n
-> do n' <- convertBindNameM n
return $ ExportSourceLocalNoType n'
convertImportM
:: (L.Name, ImportSource L.Name)
-> ConvertM a (S.Name, ImportSource S.Name)
convertImportM (n, isrc)
= do n' <- convertBindNameM n
isrc' <- convertImportSourceM isrc
return (n', isrc')
convertImportSourceM
:: ImportSource L.Name
-> ConvertM a (ImportSource S.Name)
convertImportSourceM isrc
= case isrc of
ImportSourceAbstract t
-> do t' <- convertT Env.empty t
return $ ImportSourceAbstract t'
ImportSourceModule mn n t
-> do t' <- convertT Env.empty t
n' <- convertBindNameM n
return $ ImportSourceModule mn n' t'
ImportSourceSea str t
-> do t' <- convertT Env.empty t
return $ ImportSourceSea str t'
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 (AnTEC _ _ _ a') t
| ExpArg <- ctx -> liftM (XType a') (convertT kenv t)
| otherwise -> throw $ ErrorNotNormalized ("Unexpected type expresison.")
XWitness (AnTEC _ _ _ a') w
| ExpArg <- ctx -> liftM (XWitness a') (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 b x1
-> do let tenv' = Env.extend b tenv
b' <- convertB kenv b
x1' <- convertExpX ExpBind pp defs kenv tenv' x1
return $ LLet b' x1'
LPrivate b mt bs
-> do b' <- mapM (convertB kenv) b
let kenv' = Env.extends b kenv
bs' <- mapM (convertB kenv') bs
mt' <- case mt of
Nothing -> return Nothing
Just t -> liftM Just $ convertT kenv t
return $ LPrivate b' mt' bs'
LWithRegion{}
-> throw $ ErrorMalformed "LWithRegion should not appear in Lite code."
convertWitnessX
:: Show a
=> KindEnv L.Name
-> Witness (AnTEC a L.Name) L.Name
-> ConvertM a (Witness a S.Name)
convertWitnessX kenv ww
= let down = convertWitnessX kenv
in case ww of
WVar a n -> liftM (WVar $ annotTail a) (convertU n)
WCon a wc -> liftM (WCon $ annotTail a) (convertWiConX kenv wc)
WApp a w1 w2 -> liftM2 (WApp $ annotTail a) (down w1) (down w2)
WJoin a w1 w2 -> liftM2 (WApp $ annotTail a) (down w1) (down w2)
WType a t -> liftM (WType $ annotTail a) (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 <- 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
= let a' = annotOfExp x
in 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 <- dc
-> do xBody <- convertExpX ctx pp defs kenv tenv x
let dcTag = DaConPrim (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 = DaConPrim (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 <- 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."