ddc-core-salt-0.4.3.1: DDC/Core/Salt/Exp.hs
{-# LANGUAGE TypeFamilies #-}
module DDC.Core.Salt.Exp
( module DDC.Core.Exp.Generic
, FromAnnot (..)
, ErrorFromAnnot (..)
, Annot, Bind, Bound, Prim
, Exp, Abs, Arg, Lets, Alt, Pat, Cast, Witness, WiCon
, Type)
where
import DDC.Core.Exp.Generic
import qualified DDC.Core.Exp.Generic as G
import qualified DDC.Core.Salt.Name as A
import qualified DDC.Core.Exp.Annot as N
import qualified DDC.Type.Exp as C
---------------------------------------------------------------------------------------------------
-- Type synonyms for the Salt fragment.
type instance G.GAnnot A.Name = ()
type instance G.GBind A.Name = C.Bind A.Name
type instance G.GBound A.Name = C.Bound A.Name
type instance G.GPrim A.Name = A.PrimOp
type Annot = G.GAnnot A.Name
type Bind = G.GBind A.Name
type Bound = G.GBound A.Name
type Prim = G.GPrim A.Name
type Exp = G.GExp A.Name
type Abs = G.GAbs A.Name
type Arg = G.GArg A.Name
type Lets = G.GLets A.Name
type Alt = G.GAlt A.Name
type Pat = G.GPat A.Name
type Cast = G.GCast A.Name
type Witness = G.GWitness A.Name
type WiCon = G.GWiCon A.Name
type Type = C.Type A.Name
---------------------------------------------------------------------------------------------------
-- | Convert annotated version of the Core language to the Salt fragment.
class FromAnnot c1 c2 | c1 -> c2 where
fromAnnot :: c1 -> Either ErrorFromAnnot c2
-- | Things that can go wrong when converting Salt code.
data ErrorFromAnnot
-- | Found a type that isn't part of a function application.
= ErrorFromAnnotFoundNakedType
-- | Found a witness that isn't part of a function application.
| ErrorFromAnnotFoundNakedWitness
instance FromAnnot (N.Exp a A.Name) Exp where
fromAnnot xx
= case xx of
N.XVar _ (C.UPrim (A.NamePrimVal (A.PrimValOp op)) _)
-> G.XPrim <$> pure op
N.XVar _ u
-> G.XVar <$> fromAnnot u
N.XCon _ c
-> G.XCon <$> fromAnnot c
N.XLAM _ b x
-> G.XAbs <$> (G.ALAM <$> fromAnnot b) <*> fromAnnot x
N.XLam _ b x
-> G.XAbs <$> (G.ALam <$> fromAnnot b) <*> fromAnnot x
N.XApp _ x1 (N.XType _ t)
-> G.XApp <$> fromAnnot x1 <*> (G.RType <$> fromAnnot t)
N.XApp _ x1 (N.XWitness _ w)
-> G.XApp <$> fromAnnot x1 <*> (G.RWitness <$> fromAnnot w)
N.XApp _ x1 x2
-> G.XApp <$> fromAnnot x1 <*> (G.RExp <$> fromAnnot x2)
N.XLet _ lts x
-> G.XLet <$> fromAnnot lts <*> fromAnnot x
N.XCase _ x alts
-> G.XCase <$> fromAnnot x <*> fromAnnots alts
N.XCast _ c x
-> G.XCast <$> fromAnnot c <*> fromAnnot x
N.XType{}
-> Left $ ErrorFromAnnotFoundNakedType
N.XWitness{}
-> Left $ ErrorFromAnnotFoundNakedWitness
instance FromAnnot (N.Lets a A.Name) Lets where
fromAnnot lts
= case lts of
N.LLet u x
-> G.LLet <$> fromAnnot u <*> fromAnnot x
N.LRec bxs
-> G.LRec <$> (sequence $ fmap fromAnnot2 bxs)
N.LPrivate rs mt wt
-> G.LPrivate <$> fromAnnots rs <*> fromAnnotM mt <*> fromAnnots wt
instance FromAnnot (N.Alt a A.Name) Alt where
fromAnnot aa
= case aa of
N.AAlt w x -> G.AAlt <$> fromAnnot w <*> fromAnnot x
instance FromAnnot (N.Pat A.Name) Pat where
fromAnnot pp
= case pp of
N.PDefault -> pure G.PDefault
N.PData dc bs -> G.PData <$> pure dc <*> fromAnnots bs
instance FromAnnot (N.Cast a A.Name) Cast where
fromAnnot cc
= case cc of
N.CastWeakenEffect t -> G.CastWeakenEffect <$> pure t
N.CastPurify w -> G.CastPurify <$> fromAnnot w
N.CastBox -> pure G.CastBox
N.CastRun -> pure G.CastRun
instance FromAnnot (N.Witness a A.Name) Witness where
fromAnnot ww
= case ww of
N.WVar _ u -> G.WVar <$> pure u
N.WCon _ wc -> G.WCon <$> fromAnnot wc
N.WApp _ w1 w2 -> G.WApp <$> fromAnnot w1 <*> fromAnnot w2
N.WType _ t -> G.WType <$> pure t
instance FromAnnot (N.DaCon A.Name (C.Type A.Name)) (N.DaCon A.Name (C.Type A.Name)) where
fromAnnot dc = pure dc
instance FromAnnot (N.WiCon A.Name) WiCon where
fromAnnot ww
= case ww of
N.WiConBound u t -> G.WiConBound <$> pure u <*> pure t
instance FromAnnot (C.Type A.Name) (C.Type A.Name) where
fromAnnot tt = pure tt
instance FromAnnot (N.Bind A.Name) (C.Bind A.Name) where
fromAnnot bb = pure bb
instance FromAnnot (N.Bound A.Name) (C.Bound A.Name) where
fromAnnot uu = pure uu
fromAnnot2 (x, y)
= (,) <$> fromAnnot x <*> fromAnnot y
fromAnnots xs
= sequence $ fmap fromAnnot xs
fromAnnotM Nothing = pure Nothing
fromAnnotM (Just x) = Just <$> fromAnnot x