afp/a10/a10.icl

   1 module a10
   2
   3 import StdEnv
   4
   5 import Data.Functor
   6 import Control.Applicative
   7 import Control.Monad
   8 import Data.Maybe
   9 import Data.Error
  10 import Text => qualified join
  11
  12 :: BM a b = {t :: a->b, f :: b->a, t2 :: A.c t:(t c a)->t c b, f2 :: A.c t:(t b c)->t a c}
  13 bm = {t = id, f = id, t2 = id, f2 = id}
  14
  15 :: Action b a
  16         = MoveToShip (BM b High) (BM a High)
  17         | MoveToQuay (BM b High) (BM a High)
  18         | MoveUp     (BM b Low)  (BM a High)
  19         | MoveDown   (BM b High) (BM a Low)
  20         | Lock       (BM b Low)  (BM a Low)
  21         | Unlock     (BM b Low)  (BM a Low)
  22         | Wait       (BM b a)
  23         | E.i: (:.) infixl 1 (Action b i) (Action i a)
  24         | WhileContainerBelow (BM b a) (Action a a)
  25 :: High = High
  26 :: Low = Low
  27
  28 moveToShip = MoveToShip bm bm
  29 moveToQuay = MoveToQuay bm bm
  30 moveUp     = MoveUp     bm bm
  31 moveDown   = MoveDown   bm bm
  32 lock       = Lock       bm bm
  33 unlock     = Unlock     bm bm
  34 wait       = Wait       bm
  35 whileContainerBelow = WhileContainerBelow bm
  36
  37 :: State =
  38         { onShip      :: [String]
  39         , onQuay      :: [String]
  40         , craneUp     :: Bool
  41         , craneOnQuay :: Bool
  42         , locked      :: Maybe String
  43         }
  44
  45 state0 =
  46         { onShip = []
  47         , onQuay = ["apples","beer","camera's"]
  48         , craneUp = True
  49         , craneOnQuay = True
  50         , locked = Nothing
  51         }
  52
  53 // ================
  54 eval :: (Action i f) State -> MaybeErrorString State
  55 eval (MoveToShip _ _) s = pure {s & craneOnQuay = False}
  56 eval (MoveToQuay _ _) s = pure {s & craneOnQuay = True}
  57 eval (MoveUp _ _)     s = pure {s & craneUp = True}
  58 eval (MoveDown _ _)   s = pure {s & craneUp = False}
  59 eval (Lock _ _)       s=:{locked=Nothing}
  60         | s.craneOnQuay
  61                 = case s.onQuay of
  62                         [c:r] = pure {s & onQuay = r, locked = Just c}
  63                         []    = Error "Cannot lock container on empty quay"
  64                 = case s.onShip of
  65                         [c:r] = pure {s & onShip = r, locked = Just c}
  66                         []    = Error "Cannot lock container on empty ship"
  67 eval (Lock _ _)       s=:{locked=(Just c)}
  68         = Error ("Cannot lock new container, craner contains " +++ c)
  69 eval (Unlock _ _)     s=:{locked=(Just c)}
  70         | s.craneOnQuay = pure {s & onQuay = [c:s.onQuay], locked = Nothing}
  71                         = pure {s & onShip = [c:s.onShip], locked = Nothing}
  72 eval (Unlock b1 b2)   s=:{locked=Nothing}
  73         = Error "Cannot unlock container, crane contains nothing"
  74 eval (Wait _)       s = Ok s
  75 eval (a :. b)       s = eval a s >>= eval b
  76 eval (WhileContainerBelow _ action) s
  77         | s.craneOnQuay && not (isEmpty s.onQuay) || not s.craneOnQuay && not (isEmpty s.onShip)
  78                 = eval (action :. whileContainerBelow action) s
  79         = pure s
  80
  81 opt :: (Action a b) -> Action a b
  82 opt (WhileContainerBelow b a) = WhileContainerBelow b (opt a)
  83 opt (Wait bm :. b) = opt (bm.f2 b)
  84 opt (a :. Wait bm) = opt (bm.t2 a)
  85 opt (a :. b) = opt a :. opt b
  86 opt x = x
  87
  88 Start = opt (moveToShip :. wait :. moveDown)
  89 //print :: (Action i f) [String] -> [String]
  90 //print (MoveToShip _ _) s = ["Move to ship":s]
  91 //print (MoveToQuay _ _) s = ["Move to quay":s]
  92 //print (MoveUp _ _)     s = ["Move up":s]
  93 //print (MoveDown _ _)   s = ["Move down":s]
  94 //print (Lock _ _)       s = ["Lock":s]
  95 //print (Unlock _ _)     s = ["Unlock":s]
  96 //print (Wait _)         s = ["Wait":s]
  97 //print (a :. b)         s = print a ["\n":print b s]
  98 //print (WhileContainerBelow _ a) s
  99 //      = ["While container below (":indent ["\n":print a [")":s]]]
 100 //where
 101 //      indent s = map (\s->if (s.[0] == '\n') (s +++ "\t") s)
 102 //
 103
 104 print :: (Action i f) String [String] -> [String]
 105 print (MoveToShip _ _) i s = [i,"Move to ship":s]
 106 print (MoveToQuay _ _) i s = [i,"Move to quay":s]
 107 print (MoveUp _ _)     i s = [i,"Move up":s]
 108 print (MoveDown _ _)   i s = [i,"Move down":s]
 109 print (Lock _ _)       i s = [i,"Lock":s]
 110 print (Unlock _ _)     i s = [i,"Unlock":s]
 111 print (Wait _)         i s = [i,"Wait":s]
 112 print (a :. b)         i s = print a i ["\n":print b i s]
 113 print (WhileContainerBelow _ a) i s
 114         = [i,"While container below (\n":print a ("\t"+++i) ["\n",i,")":s]]
 115
 116 Start = print loadShip "" []
 117
 118 p1 = moveToShip :. moveDown
 119
 120 //p2 = moveToShip :. wait :. lock // the required type error
 121
 122 loadShip =
 123         whileContainerBelow (
 124                 moveDown:.
 125                 lock:.
 126                 moveUp:.
 127                 moveToShip:.
 128                 wait:.
 129                 moveDown:.
 130                 wait:.
 131                 unlock:.
 132                 moveUp:.
 133                 moveToQuay
 134         ) :. wait