From c3b4f56760547940256afea8e692681dbbe21857 Mon Sep 17 00:00:00 2001
From: Tom Smeding <t.j.smeding@uu.nl>
Date: Sun, 9 Mar 2025 22:08:17 +0100
Subject: Clean up code organisation a little
---
src/CHAD.hs | 23 +++++------------------
1 file changed, 5 insertions(+), 18 deletions(-)
(limited to 'src/CHAD.hs')
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)
--
cgit v1.2.3-70-g09d2