ctpl-0.1.0.4: Text/CTPL0n.hs

{-# LANGUAGE TupleSections, FlexibleInstances #-}

-- | The new CTPL0 virtual machine.

module Text.CTPL0n where

import Control.Applicative
import Control.Arrow
import Control.Monad
import Control.Monad.ST
import Data.Array.MArray as M
import Data.Array.ST
import Data.Array.Unboxed
import Data.Char
import Data.List
import Data.STRef

-- | The VM`s state record.
data CTPL0State s = CTPL0State {
    bufferContent :: !(Buffer s),      -- ^ Tape buffer
    programContent :: UArray Int Char, -- ^ Program buffer
    bufferPointer :: !Int,             -- ^ Tape pointer
    programPointer :: !Int,            -- ^ Program pointer
    cp :: !Bool,                       -- ^ If set, the next instruction will use the top element of CK instead of AX. (Say: ``SX is CK top'' in contrast to ``SX is AX'')
    ax :: !Int,                        -- ^ Accumulator register (AX)
    mk :: [Buffer s],                  -- ^ Tape stack (MK)
    rk :: [Int],                       -- ^ Return address stack (RK)
    ck :: [Int]                        -- ^ Number stack (CK). The top element may be used like a register.
  }

-- | The VM`s configuration. Immutable during execution.
data VMConfig = VMConfig {
    maxTime :: !Int,           -- ^ Initial time limit.
    maxConditRecurs :: !Int,   -- ^ Maximum recursion depth for `x' condition (FUTURE)
    maxBufferMeasure :: !Int,  -- ^ Maximum buffer size (FUTURE)
    initBufferMeasure :: !Int, -- ^ Initial buffer size.
    vmFeatures :: [VMFeature]  -- ^ Enabled feature instructions.
  }

-- | Optional feature instructions.
data VMFeature = RandomF        -- ^ enable `Xr' instruction for random number retrieval (FUTURE)
               | FilterF        -- ^ enable `Xfs', `Xfd', `Xff' instructions for setting predefined filters on the tape (FUTURE)
               | CustomFilterF  -- ^ enable `Xfc' instruction for setting custom filters on the tape (FUTURE; won't work without FilterF)
               | InterruptsF    -- ^ enable `Xi' instruction for setting and calling interrupts (FUTURE)

-- | Predefined VM configuration, very restrictive. Allows 10000 cycles, no recursive conditions, no feature instructions, at maximum 3000 chars on tape.
safeVM :: VMConfig
safeVM = VMConfig{ maxTime=10000, maxConditRecurs=0,
                   maxBufferMeasure=3000, initBufferMeasure=0,
                   vmFeatures=[] }

-- | Predefined VM configuration, very permissive. Allows 10 million cycles, 10 levels of recursion, all available feature instructions, at maximum 30000 chars on tape.
fullVM :: VMConfig
fullVM = VMConfig{ maxTime=10000000, maxConditRecurs=10,
                   maxBufferMeasure=30000, initBufferMeasure=0,
                   vmFeatures=[RandomF, FilterF, CustomFilterF, InterruptsF] }

-- | Monad displaying success or failure. A close relative of the 'Either' monad.
data Exec a = Succ a     -- ^ Execution succeeded :)
            | Fail !Fail -- ^ Nope. See 'Fail' type.

instance Monad Exec where
  return = Succ
  fail = Fail . Dead
  (Succ a) >>= f = f a
  (Fail e) >>= f = Fail e

instance Applicative Exec where
  pure = return
  (<*>) = ap

instance Functor Exec where
  fmap = liftM

-- | Possible errors.
data Fail = Expired     -- ^ Time has expired. Program took too long to finish. You might want to increase time limit.
          | ConfViol    -- ^ Confidence violation. This may have several reasons, e.g. popping from an empty stack, jumping out of program bounds, ...
          | SynViol     -- ^ Syntax violation. I encountered an instruction (or condition) I do not understand.
          | Dead String -- ^ Program requested abort (FUTURE)

-- | The VM's execution monad. Behaves like a 'ReaderT' carrying a 'CTPL0State' reference and a 'VMConfig' wrapped around the 'ST' and the 'Exec' monad.  Also responsible for time consumption and passing.
newtype CTPL0 s a = CTPL0 { runCTPL0 :: Int ->
                                        STRef s (CTPL0State s) ->
                                        VMConfig ->
                                        ST s (Exec (a, Int)) }

-- | A tape buffer, implemented by wrapping modifiers around a mutable array.
data Buffer s = Insertion { insPlace :: !Int,  insLength :: !Int,  insContent :: String,  insNext :: Buffer s } -- ^ Character insertion
              | Deletion { delPlace :: !Int, delLength :: !Int, delNext :: Buffer s } -- ^ Character deletion
              | MBuffer { bufArray :: STUArray s Int Char } -- ^ The core: the mutable array

instance Show Fail where
  show Expired = "<Fatal: Time expired.>"
  show ConfViol = "<Fatal: Confidence violation.>"
  show SynViol = "<Fatal: Syntax violation.>"
  show (Dead s) = "<Error: "++s++">"

instance Show (Exec String) where
  show (Succ a) = a
  show (Fail f) = show f
  
-- | Read a char from a tape buffer.
readBuffer :: Buffer s -> Int -> ST s Char
readBuffer (MBuffer a) i = readArray a i
readBuffer (Insertion p l c n) i
  | i < p = readBuffer n i
  | i >= p+l = readBuffer n (i-l)
  | otherwise = return (c !! (i-p))
readBuffer (Deletion p l n) i
  | i < p = readBuffer n i
  | otherwise = readBuffer n (i+l)

-- | Write a char to the tape buffer.
writeBuffer :: Buffer s -> Int -> Char -> ST s (Buffer s)
writeBuffer (MBuffer a) i e = writeArray a i e >> return (MBuffer a)
writeBuffer (Insertion p l c n) i e
  | i < p = Insertion p l c <$> writeBuffer n i e
  | i >= p+l = Insertion p l c <$> writeBuffer n (i-l) e
  | otherwise = return $ Insertion p l (take (i-p) c ++ [e] ++ drop (i-p+1) c) n
writeBuffer (Deletion p l n) i e
  | i < p = Deletion p l <$> writeBuffer n i e
  | otherwise = Deletion p l <$> writeBuffer n (i+l) e

-- | Is the given position accessible in the tape buffer?
accBuffer :: Buffer s -> Int -> ST s Bool
accBuffer (MBuffer a) i = do
  b <- M.getBounds a
  return (snd b >= i)
accBuffer (Insertion p l c n) i
  | i < p = accBuffer n i
  | i >= p+l = accBuffer n (i-l)
  | otherwise = return True
accBuffer (Deletion p l n) i
  | i < p = accBuffer n i
  | otherwise = accBuffer n (i+l)

-- | Join the tape buffer to a string.
joinBuffer :: Buffer s -> ST s String
joinBuffer (MBuffer a) = M.getElems a
joinBuffer (Insertion p l c n) = do
  nb <- joinBuffer n
  let (a,b) = splitAt p nb
  return (a ++ c ++ b)
joinBuffer (Deletion p l n) = do
  nb <- joinBuffer n
  let (a,b) = splitAt p nb
  return (a ++ drop l b)

-- | Insert a string into the tape buffer.
insBuffer :: Buffer s -> Int -> String -> ST s (Buffer s)
insBuffer (MBuffer a) i e = return $ Insertion i (length e) e (MBuffer a)
insBuffer (Insertion p l c n) i e
  | i < p = Insertion (p+length e) l c <$> insBuffer n i e
  | i >= p+l = Insertion p l c <$> insBuffer n (i-l) e
  | i >= p && (i+length e) <= p+l =
    return $ Insertion p (l+length e) (a++e++b) n
  | otherwise = return $ Insertion i (length e) e $ Insertion p l c n
  where (a,b) = splitAt (i-p) c
insBuffer (Deletion p l n) i e
  | i < p = Deletion (p+length e) l <$> insBuffer n i e
  | i > p = Deletion p l <$> insBuffer n (i+l) e
  | otherwise = return $ Insertion i (length e) e $ Deletion p l n

-- | Delete a char from the tape buffer.
delBuffer :: Buffer s -> Int -> ST s (Buffer s)
delBuffer (MBuffer a) i = return $ Deletion i 1 $ MBuffer a
delBuffer (Insertion p l c n) i
  | i < p = Insertion (p-1) l c <$> delBuffer n i
  | i >= p+l = Insertion p l c <$> delBuffer n (i-l)
  | otherwise = return $ Insertion p (l-1) (a++b) n
  where (a,_:b) = splitAt (i-p) c
delBuffer (Deletion p l n) i
  | i < p = Deletion (p-1) l <$> delBuffer n i
  | i > p = Deletion p l <$> delBuffer n (i+l)
  | otherwise = return $ Deletion p (l+1) n

-- | Get a list of ETX positions in the tape buffer.
etxBuffer :: Buffer s -> ST s [Int]
etxBuffer (MBuffer a) = do
  es <- M.getElems a
  return $ elemIndices '\3' es
etxBuffer (Insertion p l c n) = do
  ne <- etxBuffer n
  let ie = elemIndices '\3' c
  return $ sort (map (+p) ie ++ map (\ne' -> if ne' < p then ne' else ne' + l) ne)
etxBuffer (Deletion p l n) = do
  ne <- etxBuffer n
  return $ map (\ne -> if ne < p then ne else ne-l) $ filter (/=p) ne

-- | Clone the tape buffer (fixing all modifiers into the newly created mutable array)
cloneBuffer :: Buffer s -> ST s (Buffer s)
cloneBuffer b = do
  s <- joinBuffer b
  a <- M.newListArray (0, length s - 1) s
  return $ MBuffer a

-- | Get the tape buffer`s length.
measBuffer :: Buffer s -> ST s Int
measBuffer (MBuffer a) = snd <$> M.getBounds a
measBuffer (Insertion p l c n) = (+l) <$> measBuffer n
measBuffer (Deletion p l n) = subtract l <$> measBuffer n

instance Monad (CTPL0 s) where
  return a = CTPL0 $ \i ref cfg -> return $ Succ (a,i)
  m >>= f = CTPL0 $ \i ref cfg -> do
    r <- runCTPL0 m i ref cfg
    case r of
      Succ (a, i') -> runCTPL0 (f a) i' ref cfg
      Fail f -> return $ Fail f

instance Functor (CTPL0 s) where
  fmap = liftM

instance Applicative (CTPL0 s) where
  pure = return
  (<*>) = ap

-- | Run an 'ST' action inside a compatible 'CTPL0' block
liftST :: ST s a -> CTPL0 s a
liftST m = CTPL0 $ \i ref cfg -> Succ <$> (,i) <$> m

-- | A handy wrapper around 'procInstrs'. Arguments: program, tape, config. Results: tape, leftover time, AX, CK top.
evalCTPL0' :: String -> String -> VMConfig -> Exec (String, Int, Int, Int)
evalCTPL0' program buffer cfg = runST $ do
  let limit = maxTime cfg
      bufsize = max (initBufferMeasure cfg) (length buffer+1)
  bc <- newListArray (0, bufsize-1) (buffer ++ '\3' : replicate (bufsize-length buffer-1) '\0')
  let pc = listArray (0, length program - 1) program
      st = CTPL0State (MBuffer bc) pc 0 0 False 0 [] [length program] [0]
  ref <- newSTRef st
  r <- runCTPL0 procInstrs limit ref cfg{initBufferMeasure=bufsize}
  case r of
    Succ (_, i') -> do
      st <- readSTRef ref
      buf <- joinBuffer (bufferContent st)
      return $ Succ (takeWhile (/='\3') buf, i', ax st, if null (ck st) then 0 else head $ ck st)
    Fail f -> return $ Fail f

-- | Another handy wrapper around 'procInstrs'. Less clumsy than 'evalCTPL0'', but provides less information. Arguments: program, tape, config. Results: tape only.
evalCTPL0 :: String -> String -> VMConfig  -> Exec String
evalCTPL0 program buffer cfg =
  case evalCTPL0' program buffer cfg of
    Succ (s,_,_,_) -> Succ s
    Fail f -> Fail f

-- | Gets the carried 'CTPL0State' and runs a function on it.
getState :: (CTPL0State s -> a) -> CTPL0 s a
getState f =
  CTPL0 $ \i ref cfg -> do
    st <- readSTRef ref
    return $ Succ (f st, i)

-- | Runs a function on the carried 'CTPL0State'.
modState :: (CTPL0State s -> CTPL0State s) -> CTPL0 s ()
modState f =
  CTPL0 $ \i ref cfg -> do
    modifySTRef ref f
    return $ Succ ((), i)

-- | Consume virtual time. Raise 'Expired' if limit is reached.
consumeTime :: CTPL0 s ()
consumeTime = CTPL0 $ \i ref cfg -> if i >= 1 then return (Succ ((), i-1)) else return (Fail Expired)

-- | Raise a 'ConfViol'.
confViol :: CTPL0 s a
confViol = CTPL0 $ \_ _ _ -> return $ Fail ConfViol

-- | Raise a 'SynViol'.
synViol :: CTPL0 s a
synViol = CTPL0 $ \_ _ _ -> return $ Fail SynViol

-- | Raise a 'Dead'.
die :: String -> CTPL0 s a
die s = CTPL0 $ \_ _ _ -> return . Fail $ Dead s

-- | Fetch the next instruction.
getInstr :: CTPL0 s Char
getInstr = do
  (c,p) <- getState (programContent &&& programPointer)
  modState (\st -> st{programPointer=programPointer st+1})
  return (c ! p)

-- | Have we reached the end of the program tape?
endOfInstr :: CTPL0 s Bool
endOfInstr = do
  (m,p) <- getState (snd . bounds . programContent &&& programPointer)
  return (m < p)

-- | Fetch numeric argument (as many digits as we can get)
instrNumArg :: CTPL0 s Int
instrNumArg = do
  (c,p) <- getState (programContent &&& programPointer)
  if snd (bounds c) <= p || not (isDigit (c!p)) then synViol else
    let coll p | snd (bounds c) <= p = ""
        coll p | not (isDigit (c!p)) = ""
        coll p = (c!p) : coll (p+1)
        str = coll p
    in do
      modState $ \st -> st{programPointer=programPointer st+length str}
      return $ read str

-- | Fetch string argument (delimited by '$')
instrDelimArg :: CTPL0 s String
instrDelimArg = do
  (c,p) <- getState (programContent &&& programPointer)
  if snd (bounds c) < p then synViol else
    let coll p | snd (bounds c) < p = ""
        coll p | (c!p) == '$' = "$"
        coll p = (c!p) : coll (p+1)
        str = coll p
    in do
      modState $ \st -> st{programPointer=programPointer st+length str}
      unless (last str == '$') synViol
      return $ init str

-- | Run an action (first arg) iff the test (second arg) succeeds. Raise 'ConfViol' otherwise.
provided :: CTPL0 s a -> CTPL0 s Bool -> CTPL0 s a
provided act test = do
  b <- test
  if b
    then act
    else confViol

-- | SX is AX by default, but CK top after 'C'.
sx :: CTPL0State s -> Int
sx r | cp r = head $ ck r
sx r        = ax r

-- | Set SX (AX or CK top) value.
setSX :: Int -> CTPL0State s -> CTPL0State s
setSX i r | cp r = if null (ck r) then r{ck=[i]} else r{ck=i:tail (ck r)}
setSX i r        = r{ax=i}

-- | Run the next instruction in program.
singleInstr :: CTPL0 s ()
singleInstr = do
  i <- getInstr
  consumeTime
  case i of
    -- Walk left
    '<' -> modState (\st -> st{bufferPointer=bufferPointer st-1})
           `provided` getState (\st -> bufferPointer st > 0)
    -- Walk right
    '>' -> modState (\st -> st{bufferPointer=bufferPointer st+1})
           `provided` do
             (p,c) <- getState (bufferPointer &&& bufferContent)
             liftST $ accBuffer c (p+1)
             
    -- Inc SX
    '+' -> do
      num <- instrNumArg
      modState $ \st -> setSX (sx st + num) st
    -- Dec SX
    '-' -> do
      num <- instrNumArg
      modState $ \st -> setSX (sx st - num) st
    -- Insert char, go after
    'i' -> do
      ch <- getInstr `provided` liftM not endOfInstr
      (p,c) <- getState (bufferPointer &&& bufferContent)
      c' <- liftST $ insBuffer c p [ch]
      modState $ \st -> st{bufferContent=c',bufferPointer=bufferPointer st + 1}
    -- Insert string, go after
    'I' -> do
      str <- instrDelimArg
      (p,c) <- getState (bufferPointer &&& bufferContent)
      c' <- liftST $ insBuffer c p str
      modState $ \st -> st{bufferContent=c',bufferPointer=bufferPointer st + length str}
    -- Replace char, stay
    'r' -> do
      ch <- getInstr `provided` liftM not endOfInstr
      (p,c) <- getState (bufferPointer &&& bufferContent)
      c' <- liftST $ writeBuffer c p ch
      modState $ \st -> st{bufferContent=c'}
    -- Delete char
    'x' -> do
      (p,c) <- getState (bufferPointer &&& bufferContent)
      c' <- liftST $ delBuffer c p
      modState $ \st -> st{bufferContent=c'}
    -- Append char, don't walk
    'a' -> do
      ch <- getInstr `provided` liftM not endOfInstr
      (p,c) <- getState (bufferPointer &&& bufferContent)
      etx <- liftST $ etxBuffer c
      case etx of
        [] -> confViol
        etx:_ -> do
          c' <- liftST $ writeBuffer c etx ch
          c'' <- liftST $ writeBuffer c' (etx+1) '\3'
          modState $ \st -> st{bufferContent=c''}
          when (etx<p) $ modState $ \st -> st{bufferPointer=bufferPointer st + 1}
    -- Append string, don't walk
    'A' -> do
      str <- instrDelimArg
      (p,c) <- getState (bufferPointer &&& bufferContent)
      etx <- liftST $ etxBuffer c
      case etx of
        [] -> confViol
        etx:_ -> do
          (c',etx') <- foldl (\l r -> do (c,etx) <- l; c' <- liftST $ writeBuffer c etx r; return (c,etx+1)) (return (c,etx)) str
          c'' <- liftST $ writeBuffer c' etx' '\3'
          modState $ \st -> st{bufferContent=c''}
          when (etx<p) $ modState $ \st -> st{bufferPointer=bufferPointer st + 1}
    -- Set SX=0
    '0' -> do
      modState $ setSX 0
    -- Set SX=CP
    'Q' -> do
      modState $ \st -> setSX (bufferPointer st) st
    -- Set CP=SX
    'm' -> do
      modState (\st -> st{bufferPointer=sx st}) `provided` do
        (c,s) <- getState (bufferContent &&& sx)
        liftST $ accBuffer c s
    -- Choose CK(0) for SX
    'C' -> modState (\st -> st{cp=True}) `provided` getState (not . null . ck)
    -- Load [CP] into SX
    'l' -> do
      (p,c) <- getState (bufferPointer &&& bufferContent)
      s <- liftST $ readBuffer c p
      modState $ \st -> setSX (ord s) st
    -- Save SX into [CP]
    's' -> do
      (p,(c,s)) <- getState (bufferPointer &&& bufferContent &&& sx)
      c' <- liftST $ writeBuffer c p (chr s)
      modState $ \st -> st{bufferContent=c'}
    -- Push SX onto CK
    'd' -> modState $ \st -> st{ck=sx st : ck st}
    -- Pop AX from CK
    'D' -> modState (\st -> st{ax=head $ ck st, ck=tail $ ck st})
           `provided` getState (not . null . ck)
    -- Pop CK, discard
    'k' -> modState (\st -> st{ck=tail $ ck st})
           `provided` getState (not . null . ck)
    -- Set SX=LEN
    'L' -> do
      c <- getState bufferContent
      etx <- liftST $ etxBuffer c
      case etx of
        [] -> confViol
        etx':_ -> modState $ setSX etx'
    -- Swap tape and MK(0)
    'H' ->
      modState (\st -> st{mk=bufferContent st : tail (mk st), bufferContent=head (mk st)})
      `provided` getState (not . null . mk)
    -- Push entire tape to MK
    't' -> do
      c <- getState bufferContent
      c' <- liftST $ cloneBuffer c
      modState $ \st -> st{mk=c' : mk st}
    -- Push [CP] to MK
    'y' -> do
      (c,p) <- getState (bufferContent &&& bufferPointer)
      (ch,len,a) <- liftST $ do
        ch <- readBuffer c p
        len <- measBuffer c
        a <- newListArray (0,len) (ch : '\3' : replicate (len-1) '\0')
        return (ch,len,a)
      modState $ \st -> st{mk=MBuffer a : mk st}
    -- Pop MK, discard content
    'p' -> modState (\st -> st{mk=tail $ mk st})
           `provided` getState (not . null . mk)
    -- Append [CP] to MK(0)
    'Y' -> (do
               (c,(p,a)) <- getState (bufferContent &&& bufferPointer &&& head . mk)
               ch <- liftST $ readBuffer c p
               etx <- liftST $ etxBuffer a
               case etx of
                 [] -> confViol
                 etx':_ -> do
                   a' <- liftST $ writeBuffer a etx' ch
                   a'' <- liftST $ writeBuffer a' (etx'+1) '\3'
                   modState (\st -> st{mk=a'':tail (mk st)}))
           `provided` getState (not . null . mk)
    -- Peek MK, insert, go after
    'P' -> (do
               (c,(p,a)) <- getState (bufferContent &&& bufferPointer &&& head . mk)
               js <- liftST $ joinBuffer a
               let s = takeWhile (/='\3') js
               c' <- liftST $ insBuffer c p s
               modState $ \st -> st{bufferContent=c',bufferPointer=bufferPointer st+length s})
           `provided` getState (not . null . mk)
    -- Absolute jump to SX
    'j' -> do
      a <- getState sx
      b <- singleCond
      when b $ modState $ \st -> st{programPointer=a}
    -- Relative jump by SX
    'J' -> do
      a <- getState sx
      b <- singleCond
      when b $ modState $ \st -> st{programPointer=a+programPointer st}
    -- Call procedure at SX, push IP to RK
    'c' -> do
      a <- getState sx
      b <- singleCond
      when b $ modState $ \st -> st{rk=(programPointer st):rk st, programPointer=a}
    -- Return to RK(0), pop RK
    'f' -> (modState $ \st -> st{programPointer=head (rk st), rk=tail (rk st)})
           `provided` getState (not . null . rk)
    -- Swap MK(0) and MK(1)
    'h' ->
      modState (\st -> st{mk=(mk st !! 1):(mk st !! 0):(drop 2 $ mk st)})
      `provided` getState ((>=2) . length . mk)
    -- Catch others
    o -> synViol
      {-do
      ip <- getState programPointer
      die ("SynViol in singleInstr: " ++ [o] ++ " (pos "++ show ip++")")-}
  unless (i=='C') $ modState $ \st -> st{cp=False}


-- | Evaluate a condition.
singleCond :: CTPL0 s Bool
singleCond = do
  i <- getInstr `provided` liftM not endOfInstr
  case i of
    -- Is uppercase?
    'U' -> do
      (c, p) <- getState (bufferContent &&& bufferPointer)
      isUpper <$> liftST (readBuffer c p)
    -- Is lowercase?
    'L' -> do
      (c, p) <- getState (bufferContent &&& bufferPointer)
      isLower <$> liftST (readBuffer c p)
    -- SX = 0?
    'z' -> getState ((==0) . sx)
    -- Always true
    't' -> return True
    -- Is digit?
    'N' -> do
      (c, p) <- getState (bufferContent &&& bufferPointer)
      isDigit <$> liftST (readBuffer c p)
    -- End of buffer?
    'e' -> do
      (c, p) <- getState (bufferContent &&& bufferPointer)
      realEnd <- not <$> liftST (accBuffer c (p+1))
      etxEnd <- if realEnd then return '\3' else liftST (readBuffer c p)
      return (etxEnd == '\3')      
    -- Negation
    '!' -> not <$> singleCond
    -- Disjunction
    '|' -> (||) <$> singleCond <*> singleCond
    -- Conjunction
    '&' -> (&&) <$> singleCond <*> singleCond
    -- match char?
    'q' -> do
      ch <- getInstr `provided` liftM not endOfInstr
      (c, p) <- getState (bufferContent &&& bufferPointer)
      a <- liftST $ readBuffer c p
      return (a == ch)
    -- CP < SX ?
    'l' -> uncurry (<) <$> getState (bufferPointer &&& sx)
    -- CP > SX ?
    'g' -> uncurry (>) <$> getState (bufferPointer &&& sx)
    -- CP == SX ?
    'E' -> uncurry (==) <$> getState (bufferPointer &&& sx)
    -- toggle SX
    'C' -> modState (\st -> st{cp=not $ cp st}) >> singleCond
           `provided` getState (not . null . ck)
    -- AX == CK(0) ?
    '=' -> uncurry (==) <$> getState (ax &&& head . ck)
           `provided` getState (not . null . ck)
    -- AX < CK(0) ?
    '<' -> uncurry (<) <$> getState (ax &&& head . ck)
           `provided` getState (not . null . ck)
    -- AX > CK(0) ?
    '>' -> uncurry (>) <$> getState (ax &&& head . ck)
           `provided` getState (not . null . ck)
    -- pop CK, discard, continue
    'k' -> (modState (\st -> st{ck=tail $ ck st}) >> singleCond)
           `provided` getState (not . null . ck)
    -- Catch others
    o -> synViol

-- | Run the entire program.
procInstrs :: CTPL0 s ()
procInstrs = singleInstr `asLongAs` (not <$> endOfInstr)
  where asLongAs act test = do
          b <- test
          when b $ act >> act `asLongAs` test