diff options
Diffstat (limited to 'src/CHAD')
| -rw-r--r-- | src/CHAD/EnvDescr.hs | 33 | ||||
| -rw-r--r-- | src/CHAD/Top.hs | 12 |
2 files changed, 23 insertions, 22 deletions
diff --git a/src/CHAD/EnvDescr.hs b/src/CHAD/EnvDescr.hs index fcd91f7..de615a1 100644 --- a/src/CHAD/EnvDescr.hs +++ b/src/CHAD/EnvDescr.hs @@ -11,6 +11,7 @@ module CHAD.EnvDescr where import Data.Kind (Type) import GHC.TypeLits (Symbol) +import Analysis.Identity (ValId(..)) import AST.Env import AST.Types import CHAD.Types @@ -27,12 +28,12 @@ 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) + 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 +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' @@ -43,13 +44,13 @@ subDescr :: Descr env sto -> Subenv env env' -> r) -> r subDescr DTop SETop k = k DTop SETop SETop SETop -subDescr (des `DPush` (t, sto)) (SEYes sub) k = +subDescr (des `DPush` (t, vid, 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 = + SMerge -> k (des' `DPush` (t, vid, sto)) (SEYes submerge) subaccum (SEYes subd1e) + SAccum -> k (des' `DPush` (t, vid, sto)) submerge (SEYes subaccum) (SEYes subd1e) + SDiscr -> k (des' `DPush` (t, vid, 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) @@ -64,12 +65,12 @@ type family Select env sto s where 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) +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) diff --git a/src/CHAD/Top.hs b/src/CHAD/Top.hs index ea7449d..2c01178 100644 --- a/src/CHAD/Top.hs +++ b/src/CHAD/Top.hs @@ -28,7 +28,7 @@ type family MergeEnv env where mergeDescr :: SList STy env -> Descr env (MergeEnv env) mergeDescr SNil = DTop -mergeDescr (t `SCons` env) = mergeDescr env `DPush` (t, SMerge) +mergeDescr (t `SCons` env) = mergeDescr env `DPush` (t, Nothing, SMerge) mergeEnvNoAccum :: SList f env -> Select env (MergeEnv env) "accum" :~: '[] mergeEnvNoAccum SNil = Refl @@ -41,8 +41,8 @@ mergeEnvOnlyMerge (_ `SCons` env) | Refl <- mergeEnvOnlyMerge env = Refl accumDescr :: SList STy env -> (forall sto. Descr env sto -> r) -> r accumDescr SNil k = k DTop accumDescr (t `SCons` env) k = accumDescr env $ \des -> - if hasArrays t then k (des `DPush` (t, SAccum)) - else k (des `DPush` (t, SMerge)) + if hasArrays t then k (des `DPush` (t, Nothing, SAccum)) + else k (des `DPush` (t, Nothing, SMerge)) d1Identity :: STy t -> D1 t :~: t d1Identity = \case @@ -62,17 +62,17 @@ reassembleD2E :: Descr env sto -> Ex env' (TPair (Tup (D2E (Select env sto "accum"))) (Tup (D2E (Select env sto "merge")))) -> Ex env' (Tup (D2E env)) reassembleD2E DTop _ = ENil ext -reassembleD2E (des `DPush` (_, SAccum)) e = +reassembleD2E (des `DPush` (_, _, SAccum)) e = ELet ext e $ EPair ext (reassembleD2E des (EPair ext (EFst ext (EFst ext (EVar ext (typeOf e) IZ))) (ESnd ext (EVar ext (typeOf e) IZ)))) (ESnd ext (EFst ext (EVar ext (typeOf e) IZ))) -reassembleD2E (des `DPush` (_, SMerge)) e = +reassembleD2E (des `DPush` (_, _, SMerge)) e = ELet ext e $ EPair ext (reassembleD2E des (EPair ext (EFst ext (EVar ext (typeOf e) IZ)) (EFst ext (ESnd ext (EVar ext (typeOf e) IZ))))) (ESnd ext (ESnd ext (EVar ext (typeOf e) IZ))) -reassembleD2E (des `DPush` (t, SDiscr)) e = EPair ext (reassembleD2E des e) (EZero ext t) +reassembleD2E (des `DPush` (t, _, SDiscr)) e = EPair ext (reassembleD2E des e) (EZero ext t) chad :: CHADConfig -> SList STy env -> Ex env t -> Ex (D2 t : D1E env) (TPair (D1 t) (Tup (D2E env))) chad config env (term :: Ex env t) |