{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}

{-# OPTIONS_GHC -fno-warn-unused-imports #-}

{-|
"Language.Expression" provides a way of forming strongly types expression
languages from /operators/, via 'HFree'. This module is an explanation of how
that works, via a simple example.

This module is intended to be read via Haddock.
-}
module Language.Expression.Example where

import           Data.Functor.Identity (Identity (..))

import           Control.Monad.State

import           Data.Map              (Map)
import qualified Data.Map              as Map

import           Data.SBV              (EqSymbolic (..), OrdSymbolic (..),
                                        Predicate, SBV, Symbolic, isTheorem,
                                        ite, literal, symbolic)

import           Language.Expression

--------------------------------------------------------------------------------
-- * Operators

{-$
An /operator/ is a type constructor @op@ of kind @(* -> *) -> * -> *@. @op t
a@ should be seen as a way of combining @t@-objects which has a result type
@a@.

'SimpleOp' is an example of an operator type.
-}


{-|
An operator type has two arguments. @t@ is a type constructor used to refer to
expressions. @a@ is the semantic type of the expression formed by the operator.
-}
data SimpleOp t a where
  -- | Given two int expressions, we may add them. Notice how we refer to expressions
  -- recursively with the type constructor parameter @t@.
  Add :: t Integer -> t Integer -> SimpleOp t Integer

  -- | Given two int expressions, we may compare them for equality. Notice the
  -- types of the arguments to the operator do not appear in the result type at
  -- all.
  Equal :: t Integer -> t Integer -> SimpleOp t Bool

  -- | Operator constructors can have any number of arguments, and you can mix
  -- argument types.
  IfThenElse :: t Bool -> t Integer -> t Integer -> SimpleOp t Integer

  -- | An operator does not have to actually combine expressions. It may produce an
  -- expression from a basic value, i.e. a literal int. 'HFree' itself does
  -- /not/ provide literals so they must be encoded in operators.
  Literal :: Integer -> SimpleOp t Integer

-- ** Type Classes

{-$
Most useful operators are instances of 'HFunctor' (which provides 'hmap') and
'HTraversable' (which provides 'htraverse'). These are higher-ranked analogues
of 'Functor' and 'Traversable' from @base@. Compare the type signatures of
'fmap' and 'hmap':

@
'fmap' :: ('Functor' f) => (a -> b) -> f a -> f b
'hmap' :: ('HFunctor' h) => (forall b. s b -> t b) -> h s a -> h t a
@

'fmap' transforms the @*@-kinded type argument to @f@, while 'hmap' transforms
the @(* -> *)@-kinded type constructor argument to @h@.

So in order for an operator to have an instance of 'HFunctor', it must be
possible to swap out sub-expressions inside it. This is the case for our
'SimpleOp'.

'HTraversable' has a similar relationship with 'Traversable'. 'htraverse'
adds an applicative context to 'hmap'\'s transformations:

@
'traverse' :: ('Traversable' t, 'Applicative' f) => (a -> f b) -> t a -> f (t b)
'htraverse' :: ('HTraversable' h, 'Applicative' f) => (forall b. s b -> f (t b)) -> h s a -> f (h t a)
@

There is a default implementation of 'hmap' in terms of 'htraverse'.
-}

instance HFunctor SimpleOp
instance HTraversable SimpleOp where
  htraverse :: (forall b. t b -> f (t' b)) -> SimpleOp t a -> f (SimpleOp t' a)
htraverse forall b. t b -> f (t' b)
f = \case
    Add t Integer
x t Integer
y -> t' Integer -> t' Integer -> SimpleOp t' Integer
forall (t :: * -> *). t Integer -> t Integer -> SimpleOp t Integer
Add (t' Integer -> t' Integer -> SimpleOp t' Integer)
-> f (t' Integer) -> f (t' Integer -> SimpleOp t' Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t Integer -> f (t' Integer)
forall b. t b -> f (t' b)
f t Integer
x f (t' Integer -> SimpleOp t' Integer)
-> f (t' Integer) -> f (SimpleOp t' Integer)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t Integer -> f (t' Integer)
forall b. t b -> f (t' b)
f t Integer
y
    Equal t Integer
x t Integer
y -> t' Integer -> t' Integer -> SimpleOp t' Bool
forall (t :: * -> *). t Integer -> t Integer -> SimpleOp t Bool
Equal (t' Integer -> t' Integer -> SimpleOp t' Bool)
-> f (t' Integer) -> f (t' Integer -> SimpleOp t' Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t Integer -> f (t' Integer)
forall b. t b -> f (t' b)
f t Integer
x f (t' Integer -> SimpleOp t' Bool)
-> f (t' Integer) -> f (SimpleOp t' Bool)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t Integer -> f (t' Integer)
forall b. t b -> f (t' b)
f t Integer
y
    IfThenElse t Bool
x t Integer
y t Integer
z -> t' Bool -> t' Integer -> t' Integer -> SimpleOp t' Integer
forall (t :: * -> *).
t Bool -> t Integer -> t Integer -> SimpleOp t Integer
IfThenElse (t' Bool -> t' Integer -> t' Integer -> SimpleOp t' Integer)
-> f (t' Bool)
-> f (t' Integer -> t' Integer -> SimpleOp t' Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t Bool -> f (t' Bool)
forall b. t b -> f (t' b)
f t Bool
x f (t' Integer -> t' Integer -> SimpleOp t' Integer)
-> f (t' Integer) -> f (t' Integer -> SimpleOp t' Integer)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t Integer -> f (t' Integer)
forall b. t b -> f (t' b)
f t Integer
y f (t' Integer -> SimpleOp t' Integer)
-> f (t' Integer) -> f (SimpleOp t' Integer)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t Integer -> f (t' Integer)
forall b. t b -> f (t' b)
f t Integer
z
    Literal Integer
x -> SimpleOp t' Integer -> f (SimpleOp t' Integer)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SimpleOp t' Integer
forall (t :: * -> *). Integer -> SimpleOp t Integer
Literal Integer
x)

--------------------------------------------------------------------------------
-- * Variables

{-$
As well as operators, expressions contain variables. Variables are also strongly
typed. A variable type @v@ has kind @* -> *@. The type parameter tells us the
type of the value that the variable is meant to represent.
-}


{-|
Notice that @a@ is a phantom type here (and it will be for most variable type
constructors). It is only used to restrict the type of values that are
representable by these variables. In this case, we only want to be able to store
integers so the only constructor has return type 'Integer'. It also contains a
'String' to be used as the variable name.
-}
data SimpleVar a where
  SimpleVar :: String -> SimpleVar Integer

--------------------------------------------------------------------------------
-- * Expressions

{-|
Now that we have defined our operators and variables, @'HFree' 'SimpleOp'
'SimpleVar' a@ is a syntax tree for a strongly typed expresson language.
-}
type SimpleExpr = HFree SimpleOp SimpleVar

--------------------------------------------------------------------------------
-- * A DSL

{-$
We can write simple wrapper functions to form a DSL for our expression language.
-}

{-|

@
var = 'hpure' . 'SimpleVar'
@

-}
var :: String -> SimpleExpr Integer
var :: String -> SimpleExpr Integer
var = SimpleVar Integer -> SimpleExpr Integer
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
HPointed h =>
t a -> h t a
hpure (SimpleVar Integer -> SimpleExpr Integer)
-> (String -> SimpleVar Integer) -> String -> SimpleExpr Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> SimpleVar Integer
SimpleVar

{-|

@
x ^+ y = 'HWrap' ('Add' x y)
@

-}
(^+) :: SimpleExpr Integer -> SimpleExpr Integer -> SimpleExpr Integer
SimpleExpr Integer
x ^+ :: SimpleExpr Integer -> SimpleExpr Integer -> SimpleExpr Integer
^+ SimpleExpr Integer
y = SimpleOp (HFree SimpleOp SimpleVar) Integer -> SimpleExpr Integer
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (SimpleExpr Integer
-> SimpleExpr Integer
-> SimpleOp (HFree SimpleOp SimpleVar) Integer
forall (t :: * -> *). t Integer -> t Integer -> SimpleOp t Integer
Add SimpleExpr Integer
x SimpleExpr Integer
y)

{-|

@
x ^== y = 'HWrap' ('Equal' x y)
@

-}
(^==) :: SimpleExpr Integer -> SimpleExpr Integer -> SimpleExpr Bool
SimpleExpr Integer
x ^== :: SimpleExpr Integer -> SimpleExpr Integer -> SimpleExpr Bool
^== SimpleExpr Integer
y = SimpleOp (HFree SimpleOp SimpleVar) Bool -> SimpleExpr Bool
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (SimpleExpr Integer
-> SimpleExpr Integer -> SimpleOp (HFree SimpleOp SimpleVar) Bool
forall (t :: * -> *). t Integer -> t Integer -> SimpleOp t Bool
Equal SimpleExpr Integer
x SimpleExpr Integer
y)

{-|

@
ifThenElse x y z = 'HWrap' ('IfThenElse' x y z)
@

-}
ifThenElse :: SimpleExpr Bool -> SimpleExpr Integer -> SimpleExpr Integer -> SimpleExpr Integer
ifThenElse :: SimpleExpr Bool
-> SimpleExpr Integer -> SimpleExpr Integer -> SimpleExpr Integer
ifThenElse SimpleExpr Bool
x SimpleExpr Integer
y SimpleExpr Integer
z = SimpleOp (HFree SimpleOp SimpleVar) Integer -> SimpleExpr Integer
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (SimpleExpr Bool
-> SimpleExpr Integer
-> SimpleExpr Integer
-> SimpleOp (HFree SimpleOp SimpleVar) Integer
forall (t :: * -> *).
t Bool -> t Integer -> t Integer -> SimpleOp t Integer
IfThenElse SimpleExpr Bool
x SimpleExpr Integer
y SimpleExpr Integer
z)

{-|

@
lit = 'HWrap' . 'Literal'
@

-}
lit :: Integer -> SimpleExpr Integer
lit :: Integer -> SimpleExpr Integer
lit = SimpleOp (HFree SimpleOp SimpleVar) Integer -> SimpleExpr Integer
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
h (HFree h t) a -> HFree h t a
HWrap (SimpleOp (HFree SimpleOp SimpleVar) Integer -> SimpleExpr Integer)
-> (Integer -> SimpleOp (HFree SimpleOp SimpleVar) Integer)
-> Integer
-> SimpleExpr Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> SimpleOp (HFree SimpleOp SimpleVar) Integer
forall (t :: * -> *). Integer -> SimpleOp t Integer
Literal

--------------------------------------------------------------------------------
-- ** Example Expression

{-|
Here's an example of expression written using this DSL.

@
exampleExpr = 'ifThenElse' ('var' "x" '.==' 'lit' 10) ('var' "y") ('var' "y" '.+' 'lit' 5)
exampleExpr ~ if (x = 10) then y else y + 5
@
-}
exampleExpr :: SimpleExpr Integer
exampleExpr :: SimpleExpr Integer
exampleExpr = SimpleExpr Bool
-> SimpleExpr Integer -> SimpleExpr Integer -> SimpleExpr Integer
ifThenElse (String -> SimpleExpr Integer
var String
"x" SimpleExpr Integer -> SimpleExpr Integer -> SimpleExpr Bool
^== Integer -> SimpleExpr Integer
lit Integer
10) (String -> SimpleExpr Integer
var String
"y") (String -> SimpleExpr Integer
var String
"y" SimpleExpr Integer -> SimpleExpr Integer -> SimpleExpr Integer
^+ Integer -> SimpleExpr Integer
lit Integer
5)

--------------------------------------------------------------------------------
-- * Expression Manipulation

{-$
If @op@ is an 'HFunctor', then @'HFree' op@ is an 'HMonad'. 'HMonad' defines
'hpure' (c.f. 'pure' or 'return'):

@
'hpure' :: ('HMonad' h) => t a -> h t a
'return' :: ('Monad' m) => a -> m a
@

and '^>>=' (c.f. '>>='):

@
('>>=') :: ('Monad' m) => m a -> (a -> m b) -> m b
('^>>=') :: ('HMonad' h) => h s a -> (forall b. s b -> h t b) -> h t a
@

In the case of @'HFree' op@, 'hpure' produces an expression containing a single
variable:

@
'hpure' :: v a -> 'HFree' op v a
@
-}

-- ** Substitution

{-$
'^>>=' substitutes variables inside expressions.
-}

{-|
'exampleExpr', with @x@ replaced by @z + 5@.

@
exampleExpr2 =
  exampleExpr '^>>=' \v@('SimpleVar' nm) ->
  if nm == "x" then 'var' "x" '^+' 'lit' 5 else 'hpure' v

exampleExpr2 ~ if ((z + 5) = 10) then y else y + 5
@

-}
exampleExpr2 :: SimpleExpr Integer
exampleExpr2 :: SimpleExpr Integer
exampleExpr2 =
  SimpleExpr Integer
exampleExpr SimpleExpr Integer
-> (forall b. SimpleVar b -> HFree SimpleOp SimpleVar b)
-> SimpleExpr Integer
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k)
       (t' :: k -> *).
HBind h =>
h t a -> (forall (b :: k). t b -> h t' b) -> h t' a
^>>= \v :: SimpleVar b
v@(SimpleVar String
nm) ->
  if String
nm String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"x" then String -> SimpleExpr Integer
var String
"z" SimpleExpr Integer -> SimpleExpr Integer -> SimpleExpr Integer
^+ Integer -> SimpleExpr Integer
lit Integer
5 else SimpleVar b -> HFree SimpleOp SimpleVar b
forall k (h :: (k -> *) -> k -> *) (t :: k -> *) (a :: k).
HPointed h =>
t a -> h t a
hpure SimpleVar b
v

-- ** Traversal

{-$
When @op@ is an 'HTraversable', 'HFree' is also an 'HTraversable'. This can be
used, for example, to evaluate variables in an expression.
-}

{-|
This is a function that knows the value of variables with certain names. It will
return 'Nothing' if it doesn't know how to evaluate a particular variable.

@
evalXOrY ('SimpleVar' "x") = 'Just' 1
evalXOrY ('SimpleVar' "y") = 'Just' 2
evalXOrY _ = 'Nothing'
@

It might seem strange that we can return @'Just' ('Identity' 1)@ when the
function says it returns a @'Maybe' ('Identity' a)@ for polymorphic @a@. This
works because the constructor 'SimpleVar' must be 'Integer'-valued, so when we match
on it, GHC generates the constraint @a ~ 'Integer'@ and it will happily accept an
'Integer'.

Notice that, for @s ~ 'SimpleVar'@, @t ~ 'Identity'@ and @f ~ 'Maybe'@,

@
evalXOrY :: forall a. s a -> f (t a)
@

This means that we can traverse using this function:

>>> htraverse evalXOrY exampleExpr
htraverse evalXOrY exampleExpr :: Maybe (HFree SimpleOp Identity Integer)
htraverse evalXOrY exampleExpr ~ Just (if (1 = 10) then 2 else 2 + 5)

>>> htraverse evalXOrY exampleExpr2
htraverse evalXOrY exampleExpr2 :: Maybe (HFree SimpleOp Identity Integer)
htraverse evalXOrY exampleExpr2 ~ Nothing

There was a variable (@z@) that @evalXOrY@ didn't know how to evaluate, so the
traversal resulted in 'Nothing'!

-}
evalXOrY :: SimpleVar a -> Maybe (Identity a)
evalXOrY :: SimpleVar a -> Maybe (Identity a)
evalXOrY (SimpleVar String
"x") = Identity a -> Maybe (Identity a)
forall a. a -> Maybe a
Just (a -> Identity a
forall a. a -> Identity a
Identity a
1)
evalXOrY (SimpleVar String
"y") = Identity a -> Maybe (Identity a)
forall a. a -> Maybe a
Just (a -> Identity a
forall a. a -> Identity a
Identity a
2)
evalXOrY SimpleVar a
_               = Maybe (Identity a)
forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
-- * Evaluating Expressions

{-$
The 'HFoldableAt' type class provides the mechanism for evaluating operators,
and hence expressions.

@
'hfoldMap' :: ('HFoldableAt' k h) => (forall b. t b -> k b) -> h t b -> k b
@

Implemented in terms of this is

@
'hfoldTraverse'
  :: ('HFoldableAt' k h, 'HTraversable' h, 'Applicative' f)
  => (forall b. t b -> f (k b))
  -> h t a
  -> f (k a)
'hfoldTraverse' f = 'fmap' ('hfoldMap' 'id') . 'htraverse' f
@

This function will allow us to evaluate our expressions to ground values:

>>> hfoldTraverse evalXOrY exampleExpr
Just (Identity 7)

>>> hfoldTraverse evalXOrY exampleExpr2
Nothing

-}

instance HFoldableAt Identity SimpleOp where
  hfoldMap :: (forall b. t b -> Identity b) -> SimpleOp t a -> Identity a
hfoldMap forall b. t b -> Identity b
f SimpleOp t a
s = case SimpleOp t a
s of
    Add t Integer
x t Integer
y -> Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) (Integer -> Integer -> Integer)
-> Identity Integer -> Identity (Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t Integer -> Identity Integer
forall b. t b -> Identity b
f t Integer
x Identity (Integer -> Integer)
-> Identity Integer -> Identity Integer
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t Integer -> Identity Integer
forall b. t b -> Identity b
f t Integer
y
    Equal t Integer
x t Integer
y -> Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Integer -> Integer -> Bool)
-> Identity Integer -> Identity (Integer -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t Integer -> Identity Integer
forall b. t b -> Identity b
f t Integer
x Identity (Integer -> Bool) -> Identity Integer -> Identity Bool
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t Integer -> Identity Integer
forall b. t b -> Identity b
f t Integer
y
    IfThenElse t Bool
x t Integer
y t Integer
z ->
      let ite' :: Bool -> p -> p -> p
ite' Bool
c p
a p
b = if Bool
c then p
a else p
b
      in Bool -> Integer -> Integer -> Integer
forall p. Bool -> p -> p -> p
ite' (Bool -> Integer -> Integer -> Integer)
-> Identity Bool -> Identity (Integer -> Integer -> Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t Bool -> Identity Bool
forall b. t b -> Identity b
f t Bool
x Identity (Integer -> Integer -> Integer)
-> Identity Integer -> Identity (Integer -> Integer)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t Integer -> Identity Integer
forall b. t b -> Identity b
f t Integer
y Identity (Integer -> Integer)
-> Identity Integer -> Identity Integer
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t Integer -> Identity Integer
forall b. t b -> Identity b
f t Integer
z
    Literal Integer
x -> Integer -> Identity Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
x

--------------------------------------------------------------------------------
-- ** Evaluating Variables Symbolically

{-$
With the help of @sbv@, we can evaluate expressions symbolically in order to
prove things about them.
-}

{-|
Here's a function that converts variables in 'SimpleVar' to symbolic values. It
needs a @'Map' 'String' ('SBV' 'Integer')@ stateful environment in order to
remember variables that already have symbolic values, because 'SBV' will give
you different variables on two different calls of @'symbolic' x@ for the same
@x@.
-}
evalVarSymbolic :: SimpleVar a -> StateT (Map String (SBV Integer)) Symbolic (SBV a)
evalVarSymbolic :: SimpleVar a -> StateT (Map String (SBV Integer)) Symbolic (SBV a)
evalVarSymbolic (SimpleVar String
nm) = do
  Maybe (SBV a)
existingSymbol <- (Map String (SBV a) -> Maybe (SBV a))
-> StateT (Map String (SBV Integer)) Symbolic (Maybe (SBV a))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (String -> Map String (SBV a) -> Maybe (SBV a)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
nm)
  case Maybe (SBV a)
existingSymbol of
    Just SBV a
x -> SBV a -> StateT (Map String (SBV Integer)) Symbolic (SBV a)
forall (m :: * -> *) a. Monad m => a -> m a
return SBV a
x
    Maybe (SBV a)
Nothing -> do
      SBV a
newSymbol <- SymbolicT IO (SBV a)
-> StateT (Map String (SBV Integer)) Symbolic (SBV a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (String -> SymbolicT IO (SBV a)
forall a. SymVal a => String -> Symbolic (SBV a)
symbolic String
nm)
      (Map String (SBV a) -> Map String (SBV a))
-> StateT (Map String (SBV Integer)) Symbolic ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (String -> SBV a -> Map String (SBV a) -> Map String (SBV a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
nm SBV a
newSymbol)
      SBV a -> StateT (Map String (SBV Integer)) Symbolic (SBV a)
forall (m :: * -> *) a. Monad m => a -> m a
return SBV a
newSymbol

--------------------------------------------------------------------------------
-- ** Evaluating Expressions Symbolically

{-$
We need an instance of @'HFoldableAt' 'SBV' 'SimpleOp'@ to do symbolic
evaluation, implemented like so:

@
instance 'HFoldableAt' 'SBV' 'SimpleOp' where
  'hfoldMap' = 'implHfoldMap' $ \s -> case s of
    'Add' x y          -> x '+' y
    'Equal' x y        -> x '.==' y
    'IfThenElse' x y z -> 'ite' x y z
    'Literal' x        -> 'literal' x
@
-}

instance HFoldableAt SBV SimpleOp where
  hfoldMap :: (forall b. t b -> SBV b) -> SimpleOp t a -> SBV a
hfoldMap = (SimpleOp SBV a -> SBV a)
-> (forall b. t b -> SBV b) -> SimpleOp t a -> SBV a
forall u (h :: (u -> *) -> u -> *) (k :: u -> *) (a :: u)
       (t :: u -> *).
HFunctor h =>
(h k a -> k a) -> (forall (b :: u). t b -> k b) -> h t a -> k a
implHfoldMap ((SimpleOp SBV a -> SBV a)
 -> (forall b. t b -> SBV b) -> SimpleOp t a -> SBV a)
-> (SimpleOp SBV a -> SBV a)
-> (forall b. t b -> SBV b)
-> SimpleOp t a
-> SBV a
forall a b. (a -> b) -> a -> b
$ \SimpleOp SBV a
s -> case SimpleOp SBV a
s of
    Add SBV Integer
x SBV Integer
y          -> SBV Integer
x SBV Integer -> SBV Integer -> SBV Integer
forall a. Num a => a -> a -> a
+ SBV Integer
y
    Equal SBV Integer
x SBV Integer
y        -> SBV Integer
x SBV Integer -> SBV Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Integer
y
    IfThenElse SBool
x SBV Integer
y SBV Integer
z -> SBool -> SBV Integer -> SBV Integer -> SBV Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
x SBV Integer
y SBV Integer
z
    Literal Integer
x        -> Integer -> SBV Integer
forall a. SymVal a => a -> SBV a
literal Integer
x

{-|
Now we can evaluate expressions symbolically and use @sbv@ to prove things about
them.

@
evalSimpleExprSymbolic = 'hfoldTraverse' 'evalVarSymbolic'
@
-}
evalSimpleExprSymbolic :: SimpleExpr a -> StateT (Map String (SBV Integer)) Symbolic (SBV a)
evalSimpleExprSymbolic :: SimpleExpr a -> StateT (Map String (SBV Integer)) Symbolic (SBV a)
evalSimpleExprSymbolic = (forall b.
 SimpleVar b -> StateT (Map String (SBV Integer)) Symbolic (SBV b))
-> SimpleExpr a
-> StateT (Map String (SBV Integer)) Symbolic (SBV a)
forall u (k :: u -> *) (h :: (u -> *) -> u -> *) (f :: * -> *)
       (t :: u -> *) (a :: u).
(HFoldableAt k h, HTraversable h, Applicative f) =>
(forall (b :: u). t b -> f (k b)) -> h t a -> f (k a)
hfoldTraverse forall b.
SimpleVar b -> StateT (Map String (SBV Integer)) Symbolic (SBV b)
evalVarSymbolic

{-|

Let's ask @sbv@ to prove that our expression always returns a value no less than
the variable @y@.

@
examplePredicate = 'flip' 'evalStateT' 'mempty' $ do
  expr <- 'evalSimpleExprSymbolic' 'exampleExpr'
  y <- 'evalSimpleExprSymbolic' ('var' "y")
  'return' ('expr' '.>=' y)
@

>>> isTheorem examplePredicate
True

-}
examplePredicate :: Predicate
examplePredicate :: Predicate
examplePredicate = (StateT (Map String (SBV Integer)) Symbolic SBool
 -> Map String (SBV Integer) -> Predicate)
-> Map String (SBV Integer)
-> StateT (Map String (SBV Integer)) Symbolic SBool
-> Predicate
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (Map String (SBV Integer)) Symbolic SBool
-> Map String (SBV Integer) -> Predicate
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Map String (SBV Integer)
forall a. Monoid a => a
mempty (StateT (Map String (SBV Integer)) Symbolic SBool -> Predicate)
-> StateT (Map String (SBV Integer)) Symbolic SBool -> Predicate
forall a b. (a -> b) -> a -> b
$ do
  SBV Integer
expr <- SimpleExpr Integer
-> StateT (Map String (SBV Integer)) Symbolic (SBV Integer)
forall a.
SimpleExpr a -> StateT (Map String (SBV Integer)) Symbolic (SBV a)
evalSimpleExprSymbolic SimpleExpr Integer
exampleExpr
  SBV Integer
y <- SimpleExpr Integer
-> StateT (Map String (SBV Integer)) Symbolic (SBV Integer)
forall a.
SimpleExpr a -> StateT (Map String (SBV Integer)) Symbolic (SBV a)
evalSimpleExprSymbolic (String -> SimpleExpr Integer
var String
"y")
  SBool -> StateT (Map String (SBV Integer)) Symbolic SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBV Integer
expr SBV Integer -> SBV Integer -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SBV Integer
y)