IMDP.hs

{-# LANGUAGE QualifiedDo, RebindableSyntax #-}
-- | Interval MDP: robot navigation on a line.
module Imp.Examples.IMDP
  ( Position(..)
  , step
  , simpleRobot
  , simpleRobot3
  , Move(..)
  , step3
  , robotDynamics
  , complexRobot
  ) where

import Imp

-- | Robot position.
data Position = P0 | P1 | P2 deriving stock (Eq, Ord, Show)

-- | Move right on True with 'P2' absorbing.
step :: Position -> Bool -> Position
step P2 _     = P2
step P1 True  = P2
step P1 False = P1
step P0 True  = P1
step P0 False = P0

-- | 2-step IMDP from position 0.
simpleRobot :: Imp '["move1", "move2"] Position
simpleRobot = Imp.do
  move1 <- interval @"move1" 0.6 0.9
  let pos1 = step P0 move1
  move2 <- interval @"move2" 0.6 0.9
  Imp.return (step pos1 move2)

-- | 3-step IMDP from position 0.
simpleRobot3 :: Imp '["move1", "move2", "move3"] Position
simpleRobot3 = Imp.do
  move1 <- interval @"move1" 0.6 0.9
  let pos1 = step P0 move1
  move2 <- interval @"move2" 0.6 0.9
  let pos2 = step pos1 move2
  move3 <- interval @"move3" 0.6 0.9
  Imp.return (step pos2 move3)

-- ---------------------------------------------------------------------------
-- Compositional robot: reusable dynamics with 'tag'
-- ---------------------------------------------------------------------------

-- | Three-way movement outcome.
data Move = Backwards | Stationary | Forwards
  deriving stock (Eq, Ord, Show)

-- | Step function with three-way movement: the robot can now  move backwards.
step3 :: Position -> Move -> Position
step3 P0 Backwards  = P0
step3 P0 Stationary = P0
step3 P0 Forwards   = P1
step3 P1 Backwards  = P0
step3 P1 Stationary = P1
step3 P1 Forwards   = P2
step3 P2 _          = P2   -- goal is absorbing

-- | Imprecise robot dynamics as a reusable subprogram.
robotDynamics :: Imp '["b", "f"] Move
robotDynamics = Imp.do
  goForward <- interval @"f" 0.5 0.8
  goBack    <- interval @"b" 0.0 0.2
  Imp.return $ if goForward then Forwards
               else if goBack then Backwards
               else Stationary

-- | Compositional 2-step robot using 'tag' to reuse 'robotDynamics'.
complexRobot :: Imp '["move1.b", "move1.f", "move2.b", "move2.f"] Position
complexRobot = Imp.do
  move1 <- tag @"move1" robotDynamics
  let pos1 = step3 P0 move1
  move2 <- tag @"move2" robotDynamics
  Imp.return (step3 pos1 move2)