imp-ppl-0.1.0.0: bench/Robot.hs

{-# LANGUAGE AllowAmbiguousTypes #-}

-- | An n-step robot IMDP benchmark.

module Main where

import GHC.TypeLits (Nat)

import Imp.DSL (Imp, interval)
import Imp.DSL.Combinators (ConcatMapTag, GenNames, TagFoldM, foldN)
import Imp.Examples.IMDP (Position(..), step)

import Bench
  ( BenchCase(..)
  , BenchConfig(..)
  , defaultConfig
  , runAll
  )

robotStep :: Imp '["d"] Bool
robotStep = interval @"d" 0.6 0.9

mkRobot :: forall (n :: Nat). TagFoldM (GenNames n "t") '["d"]
        => Imp (ConcatMapTag (GenNames n "t") '["d"]) Position
mkRobot = foldN @n @"t" robotStep P0 step

benchCases :: [BenchCase]
benchCases =
  [ BenchCase 1 (mkRobot @1) (== P2)
  , BenchCase 2 (mkRobot @2) (== P2)
  , BenchCase 3 (mkRobot @3) (== P2)
  , BenchCase 4 (mkRobot @4) (== P2)
  , BenchCase 5 (mkRobot @5) (== P2)
  , BenchCase 6 (mkRobot @6) (== P2)
  , BenchCase 7 (mkRobot @7) (== P2)
  , BenchCase 8 (mkRobot @8) (== P2)
  ]

robotConfig :: BenchConfig
robotConfig = defaultConfig
  { bcGradSteps  = 10
  , bcGradLR     = 0.1
  , bcGradBounds = False
  }

main :: IO ()
main = runAll robotConfig benchCases