module Lang.LamIf.Val where
import FP
import Lang.LamIf.StateSpace
import Lang.LamIf.Syntax
data CVal lτ dτ = LitC Lit | CloC (Clo lτ dτ) | TupC (PicoVal lτ dτ, PicoVal lτ dτ) | BotC
deriving (Eq, Ord)
makePrisms ''CVal
instance (Eq lτ, Eq dτ) => PartialOrder (CVal lτ dτ) where
pcompare BotC _ = PLT
pcompare _ BotC = PGT
pcompare v1 v2 | v1 == v2 = PEQ
| otherwise = PUN
instance (Ord lτ, Ord dτ) => Val lτ dτ (CVal lτ dτ) where
lit :: Lit -> CVal lτ dτ
lit = LitC
clo :: Clo lτ dτ -> CVal lτ dτ
clo = CloC
binop :: BinOp -> CVal lτ dτ -> CVal lτ dτ -> CVal lτ dτ
binop Add (LitC (I n1)) (LitC (I n2)) = LitC $ I $ n1 + n2
binop Sub (LitC (I n1)) (LitC (I n2)) = LitC $ I $ n1 n2
binop GTE (LitC (I n1)) (LitC (I n2)) = LitC $ B $ n1 >= n2
binop _ _ _ = BotC
tup :: (PicoVal lτ dτ, PicoVal lτ dτ) -> CVal lτ dτ
tup = TupC
elimBool :: CVal lτ dτ -> Set Bool
elimBool (LitC (B b)) = single b
elimBool _ = empty
elimClo :: CVal lτ dτ -> Set (Clo lτ dτ)
elimClo (CloC c) = single c
elimClo _ = empty
elimTup :: CVal lτ dτ -> Set (PicoVal lτ dτ, PicoVal lτ dτ)
elimTup (TupC t) = single t
elimTup _ = empty
data AVal lτ dτ = LitA Lit | IA | BA | CloA (Clo lτ dτ) | TupA (PicoVal lτ dτ, PicoVal lτ dτ) | BotA
deriving (Eq, Ord)
makePrisms ''AVal
instance (Eq lτ, Eq dτ) => PartialOrder (AVal lτ dτ) where
pcompare BotA _ = PLT
pcompare _ BotA = PGT
pcompare (LitA (I _)) IA = PLT
pcompare IA (LitA (I _)) = PGT
pcompare (LitA (B _)) BA = PLT
pcompare BA (LitA (B _)) = PGT
pcompare v1 v2 | v1 == v2 = PEQ
| otherwise = PUN
instance (Ord lτ, Ord dτ) => Val lτ dτ (AVal lτ dτ) where
lit :: Lit -> AVal lτ dτ
lit = LitA
clo :: Clo lτ dτ -> AVal lτ dτ
clo = CloA
binop :: BinOp -> AVal lτ dτ -> AVal lτ dτ -> AVal lτ dτ
binop Add v1 v2 | v1 ⊑ IA && v2 ⊑ IA = IA
binop Sub v1 v2 | v1 ⊑ IA && v2 ⊑ IA = IA
binop GTE v1 v2 | v1 ⊑ IA && v2 ⊑ IA = BA
binop _ _ _ = BotA
tup :: (PicoVal lτ dτ, PicoVal lτ dτ) -> AVal lτ dτ
tup = TupA
elimBool :: AVal lτ dτ -> Set Bool
elimBool (LitA (B b)) = single b
elimBool BA = fromList [True, False]
elimBool _ = empty
elimClo :: AVal lτ dτ -> Set (Clo lτ dτ)
elimClo (CloA c) = single c
elimClo _ = empty
elimTup :: AVal lτ dτ -> Set (PicoVal lτ dτ, PicoVal lτ dτ)
elimTup (TupA t) = single t
elimTup _ = empty
newtype Power val lτ dτ = Power { runPower :: Set (val lτ dτ) }
deriving
( Eq, Ord, PartialOrder, Bot, Join, JoinLattice, Difference
, Iterable (val lτ dτ), Container (val lτ dτ), Buildable (val lτ dτ)
)
instance (Ord lτ, Ord dτ) => Val lτ dτ (Power CVal lτ dτ) where
lit = Power . single . lit
clo = Power . single . clo
binop o vP1 vP2 = Power $ do
v1 <- runPower vP1
v2 <- runPower vP2
single $ binop o v1 v2
tup = Power . single . tup
elimBool = extend elimBool . runPower
elimClo = extend elimClo . runPower
elimTup = extend elimTup . runPower
instance (Ord lτ, Ord dτ) => Val lτ dτ (Power AVal lτ dτ) where
lit = Power . single . lit
clo = Power . single . clo
binop o vP1 vP2 = Power $ do
v1 <- runPower vP1
v2 <- runPower vP2
single $ binop o v1 v2
tup = Power . single . tup
elimBool = extend elimBool . runPower
elimClo = extend elimClo . runPower
elimTup = extend elimTup . runPower