Skip to content

Commit

Permalink
use UnitInterval type for safer guarantees
Browse files Browse the repository at this point in the history
  • Loading branch information
kostmo committed Sep 6, 2023
1 parent 0bb2952 commit 05cb68e
Show file tree
Hide file tree
Showing 4 changed files with 34 additions and 11 deletions.
10 changes: 3 additions & 7 deletions src/Swarm/TUI/View.hs
Original file line number Diff line number Diff line change
Expand Up @@ -113,6 +113,7 @@ import Swarm.TUI.View.CellDisplay
import Swarm.TUI.View.Objective qualified as GR
import Swarm.TUI.View.Util as VU
import Swarm.Util
import Swarm.Util.UnitInterval
import Swarm.Util.WindowedCounter qualified as WC
import Swarm.Version (NewReleaseFailure (..))
import System.Clock (TimeSpec (..))
Expand Down Expand Up @@ -647,20 +648,15 @@ robotsListWidget s = hCenter table
, txt rLog
]

dutyCycleAttrIdx = floor $ dutyCycleRatio * fromIntegral (length meterAttributeNames - 1)
-- Since (!!) is partial, here is "proof" that it is safe:
-- \* 'dutyCycleRatio' lies within the unit interval
-- \* If 'dutyCycleRatio' is 1, then the maximum value of 'dutyCycleAttrIdx' is
-- one less than the length of 'meterAttributeNames' (i.e., a valid index).
dutyCycleAttr = meterAttributeNames !! dutyCycleAttrIdx
dutyCycleAttr = safeIndex dutyCycleRatio meterAttributeNames
dutyCycleDisplay = withAttr dutyCycleAttr . str . flip (showFFloat (Just 1)) "%" $ dutyCyclePercentage

dutyCycleRatio =
WC.getOccupancy curTicks $
robot ^. activityCounts . activityWindow

dutyCyclePercentage :: Double
dutyCyclePercentage = 100 * dutyCycleRatio
dutyCyclePercentage = 100 * getValue dutyCycleRatio

idWidget = str $ show $ robot ^. robotID
nameWidget =
Expand Down
24 changes: 24 additions & 0 deletions src/Swarm/Util/UnitInterval.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Creation and utilities for tge unit interval
module Swarm.Util.UnitInterval (
UnitInterval,
getValue,
mkInterval,
safeIndex,
) where

newtype UnitInterval a = UnitInterval
{ getValue :: a
}

-- | Guarantees that the stored interval falls on the range
-- @[0, 1]@. It is up to clients to ensure that the promotion
-- to this type is lossless.
mkInterval :: (Ord a, Num a) => a -> UnitInterval a
mkInterval = UnitInterval . max 0 . min 1

safeIndex :: (RealFrac a, Num a) => UnitInterval a -> [b] -> b
safeIndex (UnitInterval alpha) xs =
xs !! floor (alpha * fromIntegral (length xs - 1))
10 changes: 6 additions & 4 deletions src/Swarm/Util/WindowedCounter.hs
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ module Swarm.Util.WindowedCounter (
import Data.Aeson
import Data.Set (Set)
import Data.Set qualified as Set
import Swarm.Util.UnitInterval
import Prelude hiding (length)

-- | Values that can be offset by an integral amount
Expand Down Expand Up @@ -128,11 +129,12 @@ getOccupancy ::
-- | current time
a ->
WindowedCounter a ->
Double
UnitInterval Double
getOccupancy currentTime wc@(WindowedCounter s lastLargest nominalSpan) =
if Set.null s || maybe False (< referenceTick) lastLargest
then 0
else fromIntegral (Set.size culledSet) / fromIntegral nominalSpan
mkInterval $
if Set.null s || maybe False (< referenceTick) lastLargest
then 0
else fromIntegral (Set.size culledSet) / fromIntegral nominalSpan
where
referenceTick = offsetBy (negate nominalSpan) currentTime
-- Cull the window according to the current time
Expand Down
1 change: 1 addition & 0 deletions swarm.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -202,6 +202,7 @@ library
Swarm.Util.Erasable
Swarm.Util.Lens
Swarm.Util.Parse
Swarm.Util.UnitInterval
Swarm.Util.WindowedCounter
Swarm.Util.Yaml
Swarm.Version
Expand Down

0 comments on commit 05cb68e

Please sign in to comment.