diff options
| -rw-r--r-- | src/CHAD.hs | 11 |
1 files changed, 2 insertions, 9 deletions
diff --git a/src/CHAD.hs b/src/CHAD.hs index 222617b..cb48816 100644 --- a/src/CHAD.hs +++ b/src/CHAD.hs @@ -35,7 +35,6 @@ module CHAD ( import Data.Functor.Const import Data.Some import Data.Type.Equality (type (==), testEquality) -import GHC.Stack (HasCallStack) import Analysis.Identity (ValId(..), validSplitEither) import AST @@ -485,11 +484,6 @@ expandSubenvZeros w (SCons t ts) (SENo sub) e = (expandSubenvZeros (WPop w) ts sub e) (EZero ext (d2M t) (d2zeroInfo t (EVar ext (d1 t) (w @> IZ)))) -assertSubenvEmpty :: HasCallStack => Subenv' s env env' -> env' :~: '[] -assertSubenvEmpty (SENo sub) | Refl <- assertSubenvEmpty sub = Refl -assertSubenvEmpty SETop = Refl -assertSubenvEmpty SEYes{} = error "assertSubenvEmpty: not empty" - --------------------------------- ACCUMULATORS --------------------------------- @@ -1058,8 +1052,7 @@ drev des accumMap sd = \case subDescr des usedSub $ \(usedDes :: Descr env' _) subMergeUsed subAccumUsed subD1eUsed -> accumPromote sdElt usedDes $ \prodes (envPro :: SList _ envPro) proSub proAccRevSub accumMapProPart wPro -> let accumMapPro = VarMap.disjointUnion (VarMap.superMap proAccRevSub (VarMap.subMap subAccumUsed accumMap)) accumMapProPart in - case drev (prodes `DPush` (shty, Nothing, SDiscr)) accumMapPro sdElt e of { Ret (e0 :: Bindings _ _ e_binds) (subtapeE :: Subenv _ e_tape) e1 sub e2 -> - case assertSubenvEmpty sub of { Refl -> + case drev (prodes `DPush` (shty, Nothing, SDiscr)) accumMapPro sdElt e of { Ret (e0 :: Bindings _ _ e_binds) (subtapeE :: Subenv _ e_tape) e1 SETop e2 -> case lemAppendNil @e_binds of { Refl -> let tapety = tapeTy (subList (bindingsBinds e0) subtapeE) in let collectexpr = bindingsCollectTape (bindingsBinds e0) subtapeE in @@ -1120,7 +1113,7 @@ drev des accumMap sd = \case ((#etape :++: #prerebinds) :++: #tape :++: #d :++: #ix :++: #pro :++: #darr :++: #tapearr :++: #sh :++: #propr :++: #d2acEnv) .> wPro (subList (bindingsBinds e0) subtapeE)) e2) - }}} + }} EUnit _ e | SpArr sdElt <- sd |