diff options
Diffstat (limited to 'src/CHAD/Top.hs')
| -rw-r--r-- | src/CHAD/Top.hs | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/CHAD/Top.hs b/src/CHAD/Top.hs index 2c01178..9e7e7f5 100644 --- a/src/CHAD/Top.hs +++ b/src/CHAD/Top.hs @@ -53,6 +53,7 @@ d1Identity = \case STArr _ t | Refl <- d1Identity t -> Refl STScal _ -> Refl STAccum{} -> error "Accumulators not allowed in input program" + STLEither a b | Refl <- d1Identity a, Refl <- d1Identity b -> Refl d1eIdentity :: SList STy env -> D1E env :~: env d1eIdentity SNil = Refl @@ -72,7 +73,7 @@ reassembleD2E (des `DPush` (_, _, SMerge)) 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) (ezeroD2 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) |