{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

-- | Implements an effect for /evaluation/ of the 'Expr' abstraction.
module LibRISCV.Effects.Expressions.Language (
    ExprEval (..),
    eval,
    defaultEval,
    ifExprM,
    whenExprM,
    unlessExprM,
) where

import Control.Monad.Freer (Eff, Member, type (~>))
import Control.Monad.Freer.TH (makeEffect)
import Control.Monad.IO.Class (MonadIO)
import LibRISCV.Effects.Expressions.Expr (Expr)

-- TODO: Reevaluate if we really need the distinction between IsTrue / IsFalse
-- for symbolic execution or if this is just nice to have for debugging.
data ExprEval v r where
    IsTrue :: Expr v -> ExprEval v Bool
    IsFalse :: Expr v -> ExprEval v Bool
    Eval :: Expr v -> ExprEval v v

makeEffect ''ExprEval

defaultEval :: (MonadIO m) => (v -> Bool, Expr v -> v) -> ExprEval v ~> m
defaultEval :: forall (m :: * -> *) v.
MonadIO m =>
(v -> Bool, Expr v -> v) -> ExprEval v ~> m
defaultEval (v -> Bool
pred, Expr v -> v
evalE) = \case
    Eval Expr v
e -> v -> m v
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (v -> m v) -> v -> m v
forall a b. (a -> b) -> a -> b
$ Expr v -> v
evalE Expr v
e
    IsTrue Expr v
e -> x -> m x
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (x -> m x) -> x -> m x
forall a b. (a -> b) -> a -> b
$ v -> Bool
pred (v -> Bool) -> v -> Bool
forall a b. (a -> b) -> a -> b
$ Expr v -> v
evalE Expr v
e
    IsFalse Expr v
e -> x -> m x
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (x -> m x) -> x -> m x
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> (v -> Bool) -> v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> Bool
pred (v -> Bool) -> v -> Bool
forall a b. (a -> b) -> a -> b
$ Expr v -> v
evalE Expr v
e

------------------------------------------------------------------------

-- Higher-level abstraction for making use of IsTrue / IsFalse without
-- having to export the isTrue / isFalse smart constructor. The standard
-- constructor is still exported as it will need to be interpreted.

condExprM ::
    forall v r v'.
    (Member (ExprEval v) r) =>
    (Expr v -> Eff r Bool) ->
    Expr v ->
    Eff r v' ->
    Eff r v' ->
    Eff r v'
condExprM :: forall v (r :: [* -> *]) v'.
Member (ExprEval v) r =>
(Expr v -> Eff r Bool)
-> Expr v -> Eff r v' -> Eff r v' -> Eff r v'
condExprM Expr v -> Eff r Bool
p Expr v
b Eff r v'
t Eff r v'
f = do
    Bool
b <- Expr v -> Eff r Bool
p Expr v
b
    if Bool
b then Eff r v'
t else Eff r v'
f

-- | Like 'Control.Monad.Extra.ifM' but with internal expression evaluation.
ifExprM :: forall v r v'. (Member (ExprEval v) r) => Expr v -> Eff r v' -> Eff r v' -> Eff r v'
ifExprM :: forall v (r :: [* -> *]) v'.
Member (ExprEval v) r =>
Expr v -> Eff r v' -> Eff r v' -> Eff r v'
ifExprM = ((Expr v -> Eff r Bool)
-> Expr v -> Eff r v' -> Eff r v' -> Eff r v'
forall v (r :: [* -> *]) v'.
Member (ExprEval v) r =>
(Expr v -> Eff r Bool)
-> Expr v -> Eff r v' -> Eff r v' -> Eff r v'
condExprM Expr v -> Eff r Bool
forall v (effs :: [* -> *]).
Member (ExprEval v) effs =>
Expr v -> Eff effs Bool
isTrue)

-- | Like 'Control.Monad.Extra.whenM' but with internal expression evaluation.
whenExprM :: forall v r. (Member (ExprEval v) r) => Expr v -> Eff r () -> Eff r ()
whenExprM :: forall v (r :: [* -> *]).
Member (ExprEval v) r =>
Expr v -> Eff r () -> Eff r ()
whenExprM Expr v
b Eff r ()
t = ((Expr v -> Eff r Bool)
-> Expr v -> Eff r () -> Eff r () -> Eff r ()
forall v (r :: [* -> *]) v'.
Member (ExprEval v) r =>
(Expr v -> Eff r Bool)
-> Expr v -> Eff r v' -> Eff r v' -> Eff r v'
condExprM Expr v -> Eff r Bool
forall v (effs :: [* -> *]).
Member (ExprEval v) effs =>
Expr v -> Eff effs Bool
isTrue) Expr v
b Eff r ()
t (() -> Eff r ()
forall a. a -> Eff r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())

-- | Like 'Control.Monad.Extra.unlessM' but with internal expression evaluation.
unlessExprM :: forall v r. (Member (ExprEval v) r) => Expr v -> Eff r () -> Eff r ()
unlessExprM :: forall v (r :: [* -> *]).
Member (ExprEval v) r =>
Expr v -> Eff r () -> Eff r ()
unlessExprM Expr v
b Eff r ()
t = ((Expr v -> Eff r Bool)
-> Expr v -> Eff r () -> Eff r () -> Eff r ()
forall v (r :: [* -> *]) v'.
Member (ExprEval v) r =>
(Expr v -> Eff r Bool)
-> Expr v -> Eff r v' -> Eff r v' -> Eff r v'
condExprM Expr v -> Eff r Bool
forall v (effs :: [* -> *]).
Member (ExprEval v) effs =>
Expr v -> Eff effs Bool
isFalse) Expr v
b Eff r ()
t (() -> Eff r ()
forall a. a -> Eff r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())