content: {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE Rank2Types #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE TypeFamilies #-}
  
  module Ivory.Language.Loop (
      breakOut,
      upTo,
      downTo,
      for,
      times,
      arrayMap,
      forever
    ) where
  
  import Ivory.Language.IBool
  import Ivory.Language.Assert
  import Ivory.Language.Array
  import Ivory.Language.Monad
  import Ivory.Language.Proxy
  import Ivory.Language.Type
  import qualified Ivory.Language.Effects as E
  import qualified Ivory.Language.Syntax as AST
  
  --------------------------------------------------------------------------------
  
  breakOut :: (E.GetBreaks eff ~ 'E.Break) => Ivory eff ()
  breakOut = emit AST.Break
  
  -- XXX don't export.
  loop :: forall eff n a. (ANat n)
       => (AST.Expr -> AST.LoopIncr)
       -> IxRep
       -> IxRep
       -> (Ix n -> Ivory (E.AllowBreak eff) a)
       -> Ivory eff ()
  loop incr from to body = do
    let maxVal = ixSize (undefined :: Ix n)
  
    let maxSz :: IxRep
        maxSz = fromInteger maxVal
    ix        <- freshVar "ix"
    let ixVar = wrapExpr (AST.ExpVar ix)
    (_,block) <- collect (body ixVar)
    let asst v = compilerAssert (v <? maxSz .&& 0 <=? v)
    asst from
    asst to
    emit (AST.Loop maxVal ix (unwrapExpr from) (incr $ unwrapExpr to) (blockStmts block))
  
  
  -- | Loop over the range of indexes @[start, start + 1 .. end]@. If
  -- @start > end@, the loop body will never execute.
  upTo :: ANat n
       => Ix n -> Ix n -> (Ix n -> Ivory (E.AllowBreak eff) a) -> Ivory eff ()
  upTo from to = loop AST.IncrTo (fromIx from) (fromIx to)
  
  -- | Loop over the range of indexes @[end, end - 1 .. start]@. If
  -- @end > start@, the loop body will never execute.
  downTo :: ANat n
         => Ix n -> Ix n -> (Ix n -> Ivory (E.AllowBreak eff) a) -> Ivory eff ()
  downTo from to = loop AST.DecrTo (fromIx from) (fromIx to)
  
  -- | Run the computation n times, where
  -- @
  --   n :: Ix m, 0 <= n <= m.
  -- @
  -- Indexes increment from 0 to n-1 inclusively.
  --
  -- Note: The definition of `for` may change so that no index value is
  -- provided. (Consider using `upto` if you need to use the index.)
  for :: forall eff n a. ANat n
      => Ix n -> (Ix n -> Ivory (E.AllowBreak eff) a) -> Ivory eff ()
  for n f = loop AST.IncrTo 0 (fromIx n - 1) f
  
  -- | Run the computation n times, where
  -- @
  --   n :: Ix m, 0 <= n <= m.
  -- @
  -- Indexes decrement from n-1 to 0 inclusively.
  --
  -- Note: The definition of `times` may change so that no index value is
  -- provided. (Consider using `downTo` if you need to use the index.)
  times :: forall eff n a. ANat n
        => Ix n -> (Ix n -> Ivory (E.AllowBreak eff) a) -> Ivory eff ()
  times n = loop AST.DecrTo (fromIx n - 1) 0
  
  arrayMap :: forall eff n a . ANat n
           => (Ix n -> Ivory (E.AllowBreak eff) a) -> Ivory eff ()
  arrayMap = loop AST.IncrTo 0 (fromIntegral (fromTypeNat (aNat :: NatType n)) - 1)
  
  forever :: Ivory (E.AllowBreak eff) () -> Ivory eff ()
  forever body = do
    (_, block) <- collect (body)
    emit (AST.Forever (blockStmts block))
  