diff options
Diffstat (limited to 'src/CHAD.hs')
| -rw-r--r-- | src/CHAD.hs | 23 |
1 files changed, 5 insertions, 18 deletions
diff --git a/src/CHAD.hs b/src/CHAD.hs index 6118e48..3f76922 100644 --- a/src/CHAD.hs +++ b/src/CHAD.hs @@ -309,24 +309,11 @@ conv2Idx (DPush des (_, SDiscr)) (IS i) = conv2Idx DTop i = case i of {} ------------------------------------- LEMMAS ------------------------------------ - -indexTupD1Id :: SNat n -> Tup (Replicate n TIx) :~: D1 (Tup (Replicate n TIx)) -indexTupD1Id SZ = Refl -indexTupD1Id (SS n) | Refl <- indexTupD1Id n = Refl - - ------------------------------------ MONOIDS ----------------------------------- -zero :: STy t -> Ex env (D2 t) -zero = EZero ext - -plus :: STy t -> Ex env (D2 t) -> Ex env (D2 t) -> Ex env (D2 t) -plus = EPlus ext - zeroTup :: SList STy env0 -> Ex env (Tup (D2E env0)) zeroTup SNil = ENil ext -zeroTup (SCons t env) = EPair ext (zeroTup env) (zero t) +zeroTup (SCons t env) = EPair ext (zeroTup env) (EZero ext t) ------------------------------------ SUBENVS ----------------------------------- @@ -366,7 +353,7 @@ subenvPlus (SCons t env) (SEYes sub1) (SEYes sub2) k = ELet ext (weakenExpr WSink e2) $ EPair ext (pl (EFst ext (EVar ext (typeOf e1) (IS IZ))) (EFst ext (EVar ext (typeOf e2) IZ))) - (plus t + (EPlus ext t (ESnd ext (EVar ext (typeOf e1) (IS IZ))) (ESnd ext (EVar ext (typeOf e2) IZ))) @@ -376,7 +363,7 @@ expandSubenvZeros (SCons t ts) (SEYes sub) e = ELet ext e $ let var = EVar ext (STPair (tTup (d2e (subList ts sub))) (d2 t)) IZ in EPair ext (expandSubenvZeros ts sub (EFst ext var)) (ESnd ext var) -expandSubenvZeros (SCons t ts) (SENo sub) e = EPair ext (expandSubenvZeros ts sub e) (zero t) +expandSubenvZeros (SCons t ts) (SENo sub) e = EPair ext (expandSubenvZeros ts sub e) (EZero ext t) assertSubenvEmpty :: HasCallStack => Subenv env env' -> env' :~: '[] assertSubenvEmpty (SENo sub) | Refl <- assertSubenvEmpty sub = Refl @@ -664,7 +651,7 @@ drev des = \case subtape (EFst ext e1) sub - (ELet ext (EJust ext (EPair ext (EVar ext (d2 t1) IZ) (zero t2))) $ + (ELet ext (EJust ext (EPair ext (EVar ext (d2 t1) IZ) (EZero ext t2))) $ weakenExpr (WCopy WSink) e2) ESnd _ e @@ -674,7 +661,7 @@ drev des = \case subtape (ESnd ext e1) sub - (ELet ext (EJust ext (EPair ext (zero t1) (EVar ext (d2 t2) IZ))) $ + (ELet ext (EJust ext (EPair ext (EZero ext t1) (EVar ext (d2 t2) IZ))) $ weakenExpr (WCopy WSink) e2) ENil _ -> Ret BTop SETop (ENil ext) (subenvNone (select SMerge des)) (ENil ext) |