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