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
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module CHAD.EnvDescr where
import Data.Kind (Type)
import GHC.TypeLits (Symbol)
import AST.Env
import AST.Types
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, 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
-- | 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, sto)) (SEYes sub) k =
subDescr des sub $ \des' submerge subaccum subd1e ->
case sto of
SMerge -> k (des' `DPush` (t, sto)) (SEYes submerge) subaccum (SEYes subd1e)
SAccum -> k (des' `DPush` (t, sto)) submerge (SEYes subaccum) (SEYes subd1e)
SDiscr -> k (des' `DPush` (t, sto)) submerge subaccum (SEYes 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)
|
