package ResourceOneRuleFailIII(sysResourceOneRuleFailIII) where

import RegFile
import List

-- We are attempting to write to two elements of an array simultaneously
-- in one rule, but Arrays only permit five simultaneous upds.
-- Expect to fail with a resource allocation error.

type Index = Bit 8
type Value = Bit 8

lo :: Integer
lo = 0

hi :: Integer
hi = 1

sysResourceOneRuleFailIII :: Module Empty
sysResourceOneRuleFailIII =
      module
        r :: Reg Value
        r <- mkReg _
        a :: RegFile Index Value
        a <- mkRegFile (fromInteger lo) (fromInteger hi)
        rules
            "Bogus":
               when True
                ==> joinActions $ map (\i -> a.upd (fromInteger i) 1) (upto lo hi)