aboutsummaryrefslogtreecommitdiff
path: root/src/CHAD/EnvDescr.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/CHAD/EnvDescr.hs')
-rw-r--r--src/CHAD/EnvDescr.hs96
1 files changed, 0 insertions, 96 deletions
diff --git a/src/CHAD/EnvDescr.hs b/src/CHAD/EnvDescr.hs
deleted file mode 100644
index 49ae0e6..0000000
--- a/src/CHAD/EnvDescr.hs
+++ /dev/null
@@ -1,96 +0,0 @@
-{-# 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)