content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE Rank2Types #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE FlexibleContexts #-}
  
  module Ivory.Language.Cond where
  
  import Prelude ()
  import Prelude.Compat
  
  import Ivory.Language.Area
  import Ivory.Language.IBool
  import Ivory.Language.Monad
  import Ivory.Language.Proc
  import Ivory.Language.Proxy
  import Ivory.Language.Ref
  import Ivory.Language.Type
  import qualified Ivory.Language.Syntax as I
  
  
  -- Effects ---------------------------------------------------------------------
  
  -- | Emit a pre-condition.
  --
  -- XXX do not export
  emitPreCond :: I.Require -> Ivory eff ()
  emitPreCond r = emits mempty { blockRequires = [r] }
  
  -- | Emit a post-condition.
  --
  -- XXX do not export
  emitPostCond :: I.Ensure -> Ivory eff ()
  emitPostCond e = emits mempty { blockEnsures = [e] }
  
  -- Condition Notation ----------------------------------------------------------
  
  newtype Cond = Cond
    { runCond :: forall eff. Ivory eff I.Cond
      -- ^ Use the naming environment from the Ivory monad.
    }
  
  -- | Checkable a boolean expression.
  check :: IBool -> Cond
  check bool = Cond (return (I.CondBool (unwrapExpr bool)))
  
  checkStored' :: forall ref s a c.
       ( CheckStored c
       , IvoryVar a
       , IvoryRef ref
       , IvoryVar (ref s ('Stored a))
       ) => (c -> Cond) -> ref s ('Stored a) -> (a -> c) -> Cond
  checkStored' c ref prop = Cond $ do
    n <- freshVar "pre"
    let ty = ivoryType (Proxy :: Proxy a)
    b <- runCond $ c $ prop $ wrapVar n
    return (I.CondDeref ty (unwrapExpr ref) n b)
  
  class CheckStored c where
    checkStored :: (IvoryVar a, IvoryRef ref, IvoryVar (ref s ('Stored a)))
                => ref s ('Stored a) -> (a -> c) -> Cond
  
  instance CheckStored IBool where
    checkStored = checkStored' check
  
  instance CheckStored Cond where
    checkStored = checkStored' id
  
  -- Pre-Conditions --------------------------------------------------------------
  
  -- | Proc bodies that have pre-conditions.  Multiple pre-conditions may be
  -- provided, for which the conjunction must hold.
  class Requires c where
    requires :: (WrapIvory m, IvoryType r) => c -> m r -> m r
  
  -- XXX Do not export
  requires' :: (WrapIvory m, Requires c, IvoryType r)
    => (c -> Cond) -> c -> m r -> m r
  requires' chk prop b = wrap $ do
    req <- runCond $ chk $ prop
    emitPreCond (I.Require req)
    unwrap b
  
  instance Requires IBool where
    requires = requires' check
  
  instance Requires Cond where
    requires = requires' id
  
  -- Post-Conditions -------------------------------------------------------------
  
  -- | Proc bodies that have post-conditions.  Multiple post-conditions may be
  -- provided, for which the conjunction must hold.
  class Ensures c where
    ensures  :: (WrapIvory m, IvoryVar r) => (r -> c) -> m r -> m r
    ensures_ :: (WrapIvory m) => c -> m () -> m ()
  
  -- XXX Do not export
  ensures' :: (WrapIvory m, Ensures c, IvoryVar r)
    => (c -> Cond) -> (r -> c) -> m r -> m r
  ensures' chk prop b = wrap $ do
    c <- runCond $ chk $ prop $ wrapVar I.retval
    emitPostCond (I.Ensure c)
    unwrap b
  
  -- XXX Do not export
  ensures_' :: (WrapIvory m, Ensures c)
    => (c -> Cond) -> c -> m () -> m ()
  ensures_' chk prop b = wrap $ do
    c <- runCond $ chk $ prop
    emitPostCond (I.Ensure c)
    unwrap b
  
  instance Ensures IBool where
    ensures = ensures' check
    ensures_ = ensures_' check
  
  instance Ensures Cond where
    ensures = ensures' id
    ensures_ = ensures_' id
  
  