1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module CHAD.EnvDescr where
import Data.Kind (Type)
import Data.Some
import GHC.TypeLits (Symbol)
import Analysis.Identity (ValId(..))
import AST.Env
import AST.Types
import AST.Weaken
import CHAD.Types
import Data
type Storage :: Symbol -> Type
data Storage s where
SAccum :: Storage "accum" -- ^ in the monad state as a mutable accumulator
SMerge :: Storage "merge" -- ^ just return and merge
SDiscr :: Storage "discr" -- ^ we happen to know this is a discrete type and won't need any contributions
deriving instance Show (Storage s)
-- | Environment description
data Descr env sto where
DTop :: Descr '[] '[]
DPush :: Descr env sto -> (STy t, Maybe (ValId t), Storage s) -> Descr (t : env) (s : sto)
deriving instance Show (Descr env sto)
descrList :: Descr env sto -> SList STy env
descrList DTop = SNil
descrList (des `DPush` (t, _, _)) = t `SCons` descrList des
descrPrj :: Descr env sto -> Idx env t -> (STy t, Maybe (ValId t), Some Storage)
descrPrj (_ `DPush` (ty, vid, sto)) IZ = (ty, vid, Some sto)
descrPrj (des `DPush` _) (IS i) = descrPrj des i
descrPrj DTop i = case i of {}
-- | This could have more precise typing on the output storage.
subDescr :: Descr env sto -> Subenv env env'
-> (forall sto'. Descr env' sto'
-> Subenv (Select env sto "merge") (Select env' sto' "merge")
-> Subenv (D2AcE (Select env sto "accum")) (D2AcE (Select env' sto' "accum"))
-> Subenv (D1E env) (D1E env')
-> r)
-> r
subDescr DTop SETop k = k DTop SETop SETop SETop
subDescr (des `DPush` (t, vid, sto)) (SEYesR sub) k =
subDescr des sub $ \des' submerge subaccum subd1e ->
case sto of
SMerge -> k (des' `DPush` (t, vid, sto)) (SEYesR submerge) subaccum (SEYesR subd1e)
SAccum -> k (des' `DPush` (t, vid, sto)) submerge (SEYesR subaccum) (SEYesR subd1e)
SDiscr -> k (des' `DPush` (t, vid, sto)) submerge subaccum (SEYesR subd1e)
subDescr (des `DPush` (_, _, sto)) (SENo sub) k =
subDescr des sub $ \des' submerge subaccum subd1e ->
case sto of
SMerge -> k des' (SENo submerge) subaccum (SENo subd1e)
SAccum -> k des' submerge (SENo subaccum) (SENo subd1e)
SDiscr -> k des' submerge subaccum (SENo subd1e)
-- | Select only the types from the environment that have the specified storage
type family Select env sto s where
Select '[] '[] _ = '[]
Select (t : ts) (s : sto) s = t : Select ts sto s
Select (_ : ts) (_ : sto) s = Select ts sto s
select :: Storage s -> Descr env sto -> SList STy (Select env sto s)
select _ DTop = SNil
select s@SAccum (DPush des (t, _, SAccum)) = SCons t (select s des)
select s@SMerge (DPush des (_, _, SAccum)) = select s des
select s@SDiscr (DPush des (_, _, SAccum)) = select s des
select s@SAccum (DPush des (_, _, SMerge)) = select s des
select s@SMerge (DPush des (t, _, SMerge)) = SCons t (select s des)
select s@SDiscr (DPush des (_, _, SMerge)) = select s des
select s@SAccum (DPush des (_, _, SDiscr)) = select s des
select s@SMerge (DPush des (_, _, SDiscr)) = select s des
select s@SDiscr (DPush des (t, _, SDiscr)) = SCons t (select s des)
selectSub :: Storage s -> Descr env sto -> Subenv env (Select env sto s)
selectSub _ DTop = SETop
selectSub s@SAccum (DPush des (_, _, SAccum)) = SEYesR (selectSub s des)
selectSub s@SMerge (DPush des (_, _, SAccum)) = SENo (selectSub s des)
selectSub s@SDiscr (DPush des (_, _, SAccum)) = SENo (selectSub s des)
selectSub s@SAccum (DPush des (_, _, SMerge)) = SENo (selectSub s des)
selectSub s@SMerge (DPush des (_, _, SMerge)) = SEYesR (selectSub s des)
selectSub s@SDiscr (DPush des (_, _, SMerge)) = SENo (selectSub s des)
selectSub s@SAccum (DPush des (_, _, SDiscr)) = SENo (selectSub s des)
selectSub s@SMerge (DPush des (_, _, SDiscr)) = SENo (selectSub s des)
selectSub s@SDiscr (DPush des (_, _, SDiscr)) = SEYesR (selectSub s des)
|
