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 //print :: (Action i f) [String] -> [String]
  82 //print (MoveToShip _ _) s = ["Move to ship":s]
  83 //print (MoveToQuay _ _) s = ["Move to quay":s]
  84 //print (MoveUp _ _)     s = ["Move up":s]
  85 //print (MoveDown _ _)   s = ["Move down":s]
  86 //print (Lock _ _)       s = ["Lock":s]
  87 //print (Unlock _ _)     s = ["Unlock":s]
  88 //print (Wait _)         s = ["Wait":s]
  89 //print (a :. b)         s = print a ["\n":print b s]
  90 //print (WhileContainerBelow _ a) s
  91 //      = ["While container below (":indent ["\n":print a [")":s]]]
  92 //where
  93 //      indent s = map (\s->if (s.[0] == '\n') (s +++ "\t") s)
  94 //
  95
  96 print :: (Action i f) String [String] -> [String]
  97 print (MoveToShip _ _) i s = [i,"Move to ship":s]
  98 print (MoveToQuay _ _) i s = [i,"Move to quay":s]
  99 print (MoveUp _ _)     i s = [i,"Move up":s]
 100 print (MoveDown _ _)   i s = [i,"Move down":s]
 101 print (Lock _ _)       i s = [i,"Lock":s]
 102 print (Unlock _ _)     i s = [i,"Unlock":s]
 103 print (Wait _)         i s = [i,"Wait":s]
 104 print (a :. b)         i s = print a i ["\n":print b i s]
 105 print (WhileContainerBelow _ a) i s
 106         = [i,"While container below (\n":print a ("\t"+++i) ["\n",i,")":s]]
 107
 108 Start = print loadShip "" []
 109
 110 p1 = moveToShip :. moveDown
 111
 112 //p2 = moveToShip :. wait :. lock // the required type error
 113
 114 loadShip =
 115         whileContainerBelow (
 116                 moveDown:.
 117                 lock:.
 118                 moveUp:.
 119                 moveToShip:.
 120                 wait:.
 121                 moveDown:.
 122                 wait:.
 123                 unlock:.
 124                 moveUp:.
 125                 moveToQuay
 126         ) :. wait