From 0a9e6dfc1accf9dc0254f0c720f633dab6e71f42 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Sun, 6 Apr 2025 17:07:22 +0200 Subject: Populate accumMap --- src/CHAD/Top.hs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src/CHAD/Top.hs') 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) -- cgit v1.2.3-70-g09d2