diff options
Diffstat (limited to 'src/CHAD/Top.hs')
| -rw-r--r-- | src/CHAD/Top.hs | 12 |
1 files changed, 6 insertions, 6 deletions
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) |