diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-09-02 21:07:06 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-09-02 21:07:06 +0200 |
| commit | 54198e8ab3be3b83507c448ffdad27c2491d2161 (patch) | |
| tree | 8cceadd80cafc88a05be8a1335b796985dc038df /src/CHAD.hs | |
| parent | 625c2c28d49dbdceb8864554acdfe1776d5333e0 (diff) | |
Code cleanup, and OverloadedLabels for LSeg
Diffstat (limited to 'src/CHAD.hs')
| -rw-r--r-- | src/CHAD.hs | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/src/CHAD.hs b/src/CHAD.hs index 97632c7..e99859c 100644 --- a/src/CHAD.hs +++ b/src/CHAD.hs @@ -2,6 +2,7 @@ {-# LANGUAGE EmptyCase #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedLabels #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} @@ -33,6 +34,7 @@ import GHC.TypeLits (Symbol) import AST import AST.Count +import AST.Weaken.Auto import Data import Lemmas @@ -591,8 +593,8 @@ rebaseRetPair descr b1 b2 (RetPair p sub d) | Refl <- lemAppendAssoc @b2 @b1 @env = RetPair p sub (weakenExpr (autoWeak (Seg' @"d" @'[D2 t] $.. Seg @"b2" b2 $.. Seg @"b1" b1 $.. Seg @"tl" (d2ace (select SAccum descr))) - (LSeg @"d" :++: (LSeg @"b2" :++: LSeg @"tl")) - (LSeg @"d" :++: ((LSeg @"b2" :++: LSeg @"b1") :++: LSeg @"tl"))) + (#d :++: (#b2 :++: #tl)) + (#d :++: ((#b2 :++: #b1) :++: #tl))) d) retConcat :: forall env0 sto list. Descr env0 sto -> SList (Ret env0 sto) list -> Rets env0 sto (D1E env0) list @@ -736,8 +738,8 @@ drev des = \case $.. Seg @"body" (bindingsBinds body0) $.. Seg @"rhs" (SCons (typeOf rhs1) (bindingsBinds rhs0)) $.. Seg @"tl" (d2ace (select SAccum des))) - (LSeg @"d" :++: LSeg @"body" :++: LSeg @"tl") - (LSeg @"d" :++: LSeg @"body" :++: LSeg @"rhs" :++: LSeg @"tl")) + (#d :++: #body :++: #tl) + (#d :++: #body :++: #rhs :++: #tl)) body2') $ ELet ext (ELet ext (ESnd ext (EVar ext bodyResType IZ)) $ @@ -846,8 +848,8 @@ drev des = \case $.. Seg @"recon" (tapeA `SCons` d2 (typeOf a) `SCons` SNil) $.. Seg @"binds" (tPrimal `SCons` bindingsBinds e0) $.. Seg @"tl" (d2ace (select SAccum des))) - (LSeg @"d" :++: LSeg @"a0" :++: LSeg @"tl") - (LSeg @"d" :++: (LSeg @"a0" :++: LSeg @"prea0") :++: LSeg @"recon" :++: LSeg @"binds" :++: LSeg @"tl")) + (#d :++: #a0 :++: #tl) + (#d :++: (#a0 :++: #prea0) :++: #recon :++: #binds :++: #tl)) a2') $ EPair ext (expandSubenvZeros (subList (select SMerge des) subAB) sAB_A $ @@ -865,8 +867,8 @@ drev des = \case $.. Seg @"recon" (tapeB `SCons` d2 (typeOf a) `SCons` SNil) $.. Seg @"binds" (tPrimal `SCons` bindingsBinds e0) $.. Seg @"tl" (d2ace (select SAccum des))) - (LSeg @"d" :++: LSeg @"b0" :++: LSeg @"tl") - (LSeg @"d" :++: (LSeg @"b0" :++: LSeg @"preb0") :++: LSeg @"recon" :++: LSeg @"binds" :++: LSeg @"tl")) + (#d :++: #b0 :++: #tl) + (#d :++: (#b0 :++: #preb0) :++: #recon :++: #binds :++: #tl)) b2') $ EPair ext (expandSubenvZeros (subList (select SMerge des) subAB) sAB_B $ @@ -922,8 +924,8 @@ drev des = \case $.. Seg' @"i" @'[TIx] $.. Seg @"ne0" (bindingsBinds ne0) $.. Seg @"tl" (sD1eEnv des)) - (LSeg @"ne0" :++: LSeg @"tl") - ((LSeg @"ve0" :++: LSeg @"i" :++: LSeg @"ne0") :++: LSeg @"tl")) + (#ne0 :++: #tl) + ((#ve0 :++: #i :++: #ne0) :++: #tl)) ne1) (subst (\_ t i -> case splitIdx @(TIx : D1E env) (bindingsBinds e0) i of Left ibind -> |