content: 
  --------------------------------------------------------------------------------
  -- | Assert folding: add asserts expression for converting to and using indexes.
  --------------------------------------------------------------------------------
  
  module Ivory.Opts.Index
    ( ixFold
    ) where
  
  import           Ivory.Opts.AssertFold
  import           Ivory.Opts.Utils
  
  import qualified Ivory.Language.Array       as I
  import qualified Ivory.Language.Syntax.AST  as I
  import qualified Ivory.Language.Syntax.Type as I
  
  --------------------------------------------------------------------------------
  
  ixFold :: I.Proc -> I.Proc
  ixFold = procFold "ix" expFold
  
  --------------------------------------------------------------------------------
  
  -- | Default expression folder that performs the recursion for an asserter.
  -- Here we use a custom folder (and not the expFoldDefault in AssertFold) since
  -- the index checks are indepdent of control-flow (from the (x ? y : z)
  -- expression) and we want to explicitly pattern-match for Ix expressions.
  expFold :: I.Type -> I.Expr -> FolderStmt ()
  expFold ty e = case e of
    I.ExpSym{}                     -> return ()
    I.ExpExtern{}                  -> return ()
    I.ExpVar{}                     -> return ()
    I.ExpLit{}                     -> return ()
    I.ExpLabel ty' e0 _str         -> expFold ty' e0
    I.ExpIndex tIdx eIdx tArr eArr -> do expFold tIdx eIdx
                                         expFold tArr eArr
    I.ExpToIx e0 maxSz             -> do insert (toIxAssert e0 maxSz)
                                         expFold I.ixRep e0
    I.ExpSafeCast ty' e0           -> expFold ty' e0
    I.ExpOp op args                -> mapM_ (expFold $ expOpType ty op) args
    I.ExpAddrOfGlobal{}            -> return ()
    I.ExpMaxMin{}                  -> return ()
    I.ExpSizeOf{}                  -> return ()
  
  --------------------------------------------------------------------------------
  
  -- | For toIx e :: Ix maxSz, assert
  -- @
  --    0 <= e < maxSz && 0 < maxSz
  -- @
  toIxAssert :: I.Expr -> Integer -> I.Stmt
  toIxAssert e maxSz = I.CompilerAssert $ I.ExpOp I.ExpAnd
    [ I.ExpOp (I.ExpLt True I.ixRep)  [ lit 0, e ]
    , I.ExpOp (I.ExpLt False I.ixRep) [ e, lit maxSz ]
    , I.ExpOp (I.ExpLt False I.ixRep) [ lit 0, lit maxSz ]
    ]
  
  --------------------------------------------------------------------------------
  
  lit :: Integer -> I.Expr
  lit i = I.ExpLit (I.LitInteger i)
  
  --------------------------------------------------------------------------------
  