module DDC.Source.Tetra.Transform.Expand
( Config (..)
, configDefault
, Expand (..))
where
import DDC.Source.Tetra.Compounds
import DDC.Source.Tetra.Predicates
import DDC.Source.Tetra.DataDef
import DDC.Source.Tetra.Module
import DDC.Source.Tetra.Prim
import DDC.Source.Tetra.Exp
import DDC.Type.Collect
import DDC.Type.Env (KindEnv, TypeEnv)
import qualified DDC.Type.Env as Env
import qualified Data.Set as Set
data Config l
= Config
{
configMakeTypeHole :: Kind (GName l) -> Type (GName l) }
configDefault :: GName l ~ Name => Config l
configDefault
= Config
{ configMakeTypeHole = \k -> TVar (UPrim NameHole k)}
type ExpandLanguage l
= ( Ord (GName l)
, GBind l ~ Bind (GName l)
, GBound l ~ Bound (GName l))
class ExpandLanguage l => Expand (c :: * -> *) l where
expand
:: Ord (GName l)
=> Config l
-> KindEnv (GName l) -> TypeEnv (GName l)
-> c l -> c l
instance ExpandLanguage l => Expand Module l where
expand = expandM
expandM config kenv tenv mm
= let
preTop p
= case p of
TopClause a (SLet _ b [] [GExp x])
-> let (b', x') = expandQuant a config kenv (b, x)
in ( TopClause a (SLet a b' [] [GExp x'])
, Env.singleton b')
TopData _ def
-> (p, typeEnvOfDataDef def)
_ -> error "source-tetra.expand: can't expand sugared TopClause."
(tops_quant, tenvs)
= unzip $ map preTop $ moduleTops mm
tenv' = Env.unions $ tenv : tenvs
tops' = map (expand config kenv tenv')
$ tops_quant
in mm { moduleTops = tops' }
instance ExpandLanguage l => Expand Top l where
expand = expandT
expandT config kenv tenv top
= case top of
TopClause a1 (SLet a2 b [] [GExp x])
-> let tenv' = Env.extend b tenv
x' = expand config kenv tenv' x
in TopClause a1 (SLet a2 b [] [GExp x'])
TopData{} -> top
_ -> error "source-tetra.expand: can't expand sugared TopClause."
instance ExpandLanguage l => Expand GExp l where
expand = downX
downX config kenv tenv xx
= case xx of
XVar{}
-> expandApp config kenv tenv xx []
XCon{}
-> expandApp config kenv tenv xx []
XPrim{}
-> expandApp config kenv tenv xx []
XApp{}
| (x1, xas) <- takeXAppsWithAnnots xx
-> if isXVar x1 || isXCon x1
then let xas' = [ (expand config kenv tenv x, a) | (x, a) <- xas ]
in expandApp config kenv tenv x1 xas'
else let x1' = expand config kenv tenv x1
xas' = [ (expand config kenv tenv x, a) | (x, a) <- xas ]
in makeXAppsWithAnnots x1' xas'
XLet a (LLet b x1) x2
-> let
(b_quant, x1_quant)
= expandQuant a config kenv (b, x1)
tenv' = Env.extend b_quant tenv
x1' = expand config kenv tenv' x1_quant
x2' = expand config kenv tenv' x2
in XLet a (LLet b x1') x2'
XLet a (LRec bxs) x2
-> let
(bs_quant, xs_quant)
= unzip
$ [expandQuant a config kenv (b, x) | (b, x) <- bxs]
tenv' = Env.extends bs_quant tenv
xs' = map (expand config kenv tenv') xs_quant
x2' = expand config kenv tenv' x2
in XLet a (LRec (zip bs_quant xs')) x2'
XLet a (LGroup [SLet _ b [] [GExp x1]]) x2
-> expand config kenv tenv (XLet a (LLet b x1) x2)
XLet _ (LGroup{}) _
-> error $ "ddc-source-tetra.expand: can't expand sugared LGroup."
XLAM a b x
-> let kenv' = Env.extend b kenv
x' = expand config kenv' tenv x
in XLAM a b x'
XLam a b x
-> let tenv' = Env.extend b tenv
x' = expand config kenv tenv' x
in XLam a b x'
XLet a (LPrivate bts mR bxs) x2
-> let tenv' = Env.extends bts kenv
kenv' = Env.extends bxs tenv
x2' = expand config kenv' tenv' x2
in XLet a (LPrivate bts mR bxs) x2'
XCase a x alts -> XCase a (downX config kenv tenv x)
(map (downA config kenv tenv) alts)
XCast a c x -> XCast a c (downX config kenv tenv x)
XType{} -> xx
XWitness{} -> xx
XDefix a xs -> XDefix a (map (downX config kenv tenv) xs)
XInfixOp{} -> xx
XInfixVar{} -> xx
instance ExpandLanguage l => Expand GAlt l where
expand = downA
downA config kenv tenv alt
= case alt of
AAlt p gsx
-> let tenv' = extendPat p tenv
gsx' = map (expand config kenv tenv') gsx
in AAlt p gsx'
instance ExpandLanguage l => Expand GGuardedExp l where
expand = downGX
downGX config kenv tenv (GGuard g x)
= let g' = expand config kenv tenv g
tenv' = extendGuard g' tenv
in GGuard g' (expand config kenv tenv' x)
downGX config kenv tenv (GExp x)
= let x' = expand config kenv tenv x
in GExp x'
instance ExpandLanguage l => Expand GGuard l where
expand = downG
downG config kenv tenv gg
= case gg of
GPat p x
-> let tenv' = extendPat p tenv
x' = expand config kenv tenv' x
in GPat p x'
GPred x
-> let x' = expand config kenv tenv x
in GPred x'
GDefault
-> GDefault
extendPat
:: ExpandLanguage l
=> GPat l -> TypeEnv (GName l) -> TypeEnv (GName l)
extendPat ww tenv
= case ww of
PDefault -> tenv
PData _ bs -> Env.extends bs tenv
extendGuard
:: ExpandLanguage l
=> GGuard l -> TypeEnv (GName l) -> TypeEnv (GName l)
extendGuard gg tenv
= case gg of
GPat w _ -> extendPat w tenv
_ -> tenv
expandQuant
:: ExpandLanguage l
=> GAnnot l
-> Config l
-> KindEnv (GName l)
-> (GBind l, GExp l)
-> (GBind l, GExp l)
expandQuant a config kenv (b, x)
| fvs <- freeVarsT kenv (typeOfBind b)
, not $ Set.null fvs
= let
kHole = configMakeTypeHole config sComp
makeBind u
= case u of
UName n -> Just $ BName n kHole
UIx{} -> Just $ BAnon kHole
_ -> Nothing
Just bsNew = sequence $ map makeBind $ Set.toList fvs
t' = foldr TForall (typeOfBind b) bsNew
b' = replaceTypeOfBind t' b
x' = foldr (XLAM a) x bsNew
in (b', x')
| otherwise
= (b, x)
expandApp
:: ExpandLanguage l
=> Config l
-> KindEnv (GName l)
-> TypeEnv (GName l)
-> GExp l
-> [(GExp l, GAnnot l)]
-> GExp l
expandApp config _kenv tenv x0 xas0
| Just (a, u) <- slurpVarConBound x0
, Just tt <- Env.lookup u tenv
, not $ isBot tt
= let
go t xas
= case (t, xas) of
(TForall _b t2, (x1@(XType _ _t1'), a1) : xas')
-> (x1, a1) : go t2 xas'
(TForall b t2, xas')
-> let k = typeOfBind b
Just a0 = takeAnnotOfExp x0
xh = XType a0 (configMakeTypeHole config k)
in (xh, a) : go t2 xas'
_ -> xas
xas_expanded
= go tt xas0
in makeXAppsWithAnnots x0 xas_expanded
| otherwise
= makeXAppsWithAnnots x0 xas0
slurpVarConBound
:: GBound l ~ Bound (GName l)
=> GExp l
-> Maybe (GAnnot l, GBound l)
slurpVarConBound xx
= case xx of
XVar a u -> Just (a, u)
XCon a dc
| DaConBound n <- dc -> Just (a, UName n)
| DaConPrim n t <- dc -> Just (a, UPrim n t)
_ -> Nothing