@@ -592,46 +592,51 @@ paydownMergeDebt :: MergeDebt -> MergeCredit -> Credit -> MergeDebtPaydown
592
592
paydownMergeDebt MergeDebt {totalDebt}
593
593
MergeCredit {spentCredits, unspentCredits}
594
594
c
595
- | assert (c >= 0 ) False = undefined
596
-
597
- | let ! suppliedCredits' = suppliedCredits + c
598
- , suppliedCredits' >= totalDebt
595
+ | suppliedCredits' >= totalDebt
599
596
, let ! leftover = suppliedCredits' - totalDebt
600
597
! perform = c - leftover
601
- = assert (perform >= 0 && leftover >= 0 ) $
602
- assert (c == perform + leftover) $
603
- assert (suppliedCredits + perform == totalDebt) $
598
+ = assert (dischargePostcondition perform leftover) $
604
599
MergeDebtDischarged perform leftover
605
600
606
- | let ! unspentCredits' = unspentCredits + c
607
- , unspentCredits' >= mergeBatchSize
601
+ | unspentCredits' >= mergeBatchSize
608
602
, let (! b, ! r) = divMod unspentCredits' mergeBatchSize
609
603
! perform = b * mergeBatchSize
610
- spentCredits' = spentCredits + perform
611
- unspentCredits'' = unspentCredits' - perform
612
- suppliedCredits' = spentCredits' + unspentCredits''
613
- = assert (unspentCredits'' == r)
614
- assert (suppliedCredits + c == suppliedCredits') $
615
- assert (suppliedCredits' < totalDebt) $
604
+ = assert (performPostcondition perform r) $
616
605
MergeDebtPaydownPerform
617
606
perform
618
607
MergeCredit {
619
- spentCredits = spentCredits' ,
620
- unspentCredits = unspentCredits''
608
+ spentCredits = spentCredits + perform ,
609
+ unspentCredits = unspentCredits' - perform
621
610
}
622
611
623
612
| otherwise
624
- , let unspentCredits' = unspentCredits + c
625
- suppliedCredits' = spentCredits + unspentCredits'
626
- = assert (suppliedCredits + c == suppliedCredits') $
627
- assert (suppliedCredits' < totalDebt) $
613
+ = assert creditedPostcondition $
628
614
MergeDebtPaydownCredited
629
615
MergeCredit {
630
616
spentCredits,
631
617
unspentCredits = unspentCredits'
632
618
}
633
619
where
634
- ! suppliedCredits = spentCredits + unspentCredits
620
+ suppliedCredits' = spentCredits + unspentCredits + c
621
+ unspentCredits' = unspentCredits + c
622
+
623
+ dischargePostcondition perform leftover =
624
+ (c >= 0 )
625
+ && (perform >= 0 && leftover >= 0 )
626
+ && (c == perform + leftover)
627
+ && (spentCredits + unspentCredits + perform == totalDebt)
628
+
629
+ performPostcondition perform r =
630
+ let spentCredits' = spentCredits + perform
631
+ unspentCredits'' = unspentCredits' - perform
632
+ in (c >= 0 )
633
+ && (unspentCredits'' == r)
634
+ && (suppliedCredits' == spentCredits' + unspentCredits'')
635
+ && (suppliedCredits' < totalDebt)
636
+
637
+ creditedPostcondition =
638
+ (c >= 0 )
639
+ && (suppliedCredits' < totalDebt)
635
640
636
641
mergeBatchSize :: Int
637
642
mergeBatchSize = 32
0 commit comments