{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE MultiWayIf #-}

-- | Normalization and equivalence checking for expressions
module What4.Serialize.Normalize
  ( normSymFn
  , normExpr
  , testEquivSymFn
  , testEquivExpr
  , ExprEquivResult(..)
  ) where

import qualified Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.TraversableFC as FC

import qualified What4.Interface as S
import qualified What4.Expr as S
import qualified What4.Expr.Builder as B
import qualified What4.Expr.WeightedSum as WSum
import           Data.Parameterized.Classes

-- | Apply some normalizations to make function call arguments more readable.  Examples include:
--
--  * Avoid wrapping single literals in a 'B.SemiRingLiteral' and just represent them as a bare integer literals
--  * Attempt to reduce function calls with constant arguments where possible
normSymFn :: forall sym st fs t args ret. sym ~ B.ExprBuilder t st fs
          => sym
          -> B.ExprSymFn t args ret
          -> Ctx.Assignment (S.Expr t) args
          -> IO (S.Expr t ret)
normSymFn :: forall sym (st :: Type -> Type) fs t (args :: Ctx BaseType)
       (ret :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym
-> ExprSymFn t args ret
-> Assignment (Expr t) args
-> IO (Expr t ret)
normSymFn sym
sym ExprSymFn t args ret
symFn Assignment (Expr t) args
argEs = case ExprSymFn t args ret -> SymFnInfo t args ret
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SymFnInfo t args ret
B.symFnInfo ExprSymFn t args ret
symFn of
  B.DefinedFnInfo Assignment (ExprBoundVar t) args
argBVs Expr t ret
expr UnfoldPolicy
_ -> do
    Assignment (Expr t) args
argEs' <- (forall (x :: BaseType). Expr t x -> IO (Expr t x))
-> forall (x :: Ctx BaseType).
   Assignment (Expr t) x -> IO (Assignment (Expr t) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: BaseType -> Type) (g :: BaseType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: BaseType). f x -> m (g x))
-> forall (x :: Ctx BaseType). Assignment f x -> m (Assignment g x)
FC.traverseFC (sym -> Expr t x -> IO (Expr t x)
forall sym (st :: Type -> Type) fs t (tp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym -> Expr t tp -> IO (Expr t tp)
normExpr sym
sym) Assignment (Expr t) args
argEs
    Expr t ret
expr' <- ExprBuilder t st fs
-> Expr t ret
-> Assignment (ExprBoundVar t) args
-> Assignment (Expr t) args
-> IO (Expr t ret)
forall t (st :: Type -> Type) fs (ret :: BaseType)
       (args :: Ctx BaseType).
ExprBuilder t st fs
-> Expr t ret
-> Assignment (ExprBoundVar t) args
-> Assignment (Expr t) args
-> IO (Expr t ret)
B.evalBoundVars sym
ExprBuilder t st fs
sym Expr t ret
expr Assignment (ExprBoundVar t) args
argBVs Assignment (Expr t) args
argEs'
    sym -> Expr t ret -> IO (Expr t ret)
forall sym (st :: Type -> Type) fs t (tp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym -> Expr t tp -> IO (Expr t tp)
normExpr sym
sym Expr t ret
expr'
  SymFnInfo t args ret
_ -> sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
forall (args :: Ctx BaseType) (ret :: BaseType).
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
S.applySymFn sym
sym SymFn sym args ret
ExprSymFn t args ret
symFn Assignment (SymExpr sym) args
Assignment (Expr t) args
argEs


normExpr :: forall sym st fs t tp
          . sym ~ B.ExprBuilder t st fs
         => sym
         -> B.Expr t tp -> IO (B.Expr t tp)
normExpr :: forall sym (st :: Type -> Type) fs t (tp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym -> Expr t tp -> IO (Expr t tp)
normExpr sym
sym Expr t tp
e = Expr t tp -> IO (Expr t tp)
go Expr t tp
e
  where go :: B.Expr t tp -> IO (B.Expr t tp)
        go :: Expr t tp -> IO (Expr t tp)
go (B.SemiRingLiteral SemiRingRepr sr
S.SemiRingIntegerRepr Coefficient sr
val ProgramLoc
_) = sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
S.intLit sym
sym Integer
Coefficient sr
val
        go (B.AppExpr AppExpr t tp
appExpr) = sym -> AppExpr t tp -> IO (Expr t tp)
forall sym (st :: Type -> Type) fs t (tp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym -> AppExpr t tp -> IO (Expr t tp)
normAppExpr sym
sym AppExpr t tp
appExpr
        go x :: Expr t tp
x@(B.NonceAppExpr NonceAppExpr t tp
nae) =
          case NonceAppExpr t tp -> NonceApp t (Expr t) tp
forall t (tp :: BaseType).
NonceAppExpr t tp -> NonceApp t (Expr t) tp
B.nonceExprApp NonceAppExpr t tp
nae of
            B.FnApp ExprSymFn t args tp
fn Assignment (Expr t) args
args -> sym
-> ExprSymFn t args tp
-> Assignment (Expr t) args
-> IO (Expr t tp)
forall sym (st :: Type -> Type) fs t (args :: Ctx BaseType)
       (ret :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym
-> ExprSymFn t args ret
-> Assignment (Expr t) args
-> IO (Expr t ret)
normSymFn sym
sym ExprSymFn t args tp
fn Assignment (Expr t) args
args
            NonceApp t (Expr t) tp
_ -> Expr t tp -> IO (Expr t tp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
x
        go Expr t tp
x = Expr t tp -> IO (Expr t tp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
x

-- | Normalize an expression by passing it back through the builder
--
-- NOTE: We may want to audit the cases here for completeness
normAppExpr :: forall sym st fs t tp
             . sym ~ S.ExprBuilder t st fs
            => sym
            -> S.AppExpr t tp
            -> IO (S.Expr t tp)
normAppExpr :: forall sym (st :: Type -> Type) fs t (tp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym -> AppExpr t tp -> IO (Expr t tp)
normAppExpr sym
sym AppExpr t tp
ae = do
  App (Expr t) tp
e' <- App (Expr t) tp -> IO (App (Expr t) tp)
forall (tp' :: BaseType). App (Expr t) tp' -> IO (App (Expr t) tp')
go (AppExpr t tp -> App (Expr t) tp
forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
S.appExprApp AppExpr t tp
ae)
  ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
B.sbMakeExpr sym
ExprBuilder t st fs
sym App (Expr t) tp
e'
  where norm2 :: forall tp' tp'' tp'''
               . (S.Expr t tp' -> S.Expr t tp'' -> IO (S.Expr t tp'''))
              -> S.Expr t tp' -> S.Expr t tp'' -> IO (S.Expr t tp''')
        norm2 :: forall (tp' :: BaseType) (tp'' :: BaseType) (tp''' :: BaseType).
(Expr t tp' -> Expr t tp'' -> IO (Expr t tp'''))
-> Expr t tp' -> Expr t tp'' -> IO (Expr t tp''')
norm2 Expr t tp' -> Expr t tp'' -> IO (Expr t tp''')
f Expr t tp'
e1 Expr t tp''
e2 = do
          Expr t tp'
e1' <- sym -> Expr t tp' -> IO (Expr t tp')
forall sym (st :: Type -> Type) fs t (tp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym -> Expr t tp -> IO (Expr t tp)
normExpr sym
sym Expr t tp'
e1
          Expr t tp''
e2' <- sym -> Expr t tp'' -> IO (Expr t tp'')
forall sym (st :: Type -> Type) fs t (tp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym -> Expr t tp -> IO (Expr t tp)
normExpr sym
sym Expr t tp''
e2
          Expr t tp' -> Expr t tp'' -> IO (Expr t tp''')
f Expr t tp'
e1' Expr t tp''
e2'

        go :: forall tp'. S.App (S.Expr t) tp' -> IO (S.App (S.Expr t) tp')
        go :: forall (tp' :: BaseType). App (Expr t) tp' -> IO (App (Expr t) tp')
go (S.BaseIte BaseTypeRepr tp'
_ Integer
_ Expr t BaseBoolType
test Expr t tp'
then_ Expr t tp'
else_) = do
          Expr t BaseBoolType
test' <- sym -> Expr t BaseBoolType -> IO (Expr t BaseBoolType)
forall sym (st :: Type -> Type) fs t (tp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym -> Expr t tp -> IO (Expr t tp)
normExpr sym
sym Expr t BaseBoolType
test
          Expr t tp'
then' <- sym -> Expr t tp' -> IO (Expr t tp')
forall sym (st :: Type -> Type) fs t (tp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym -> Expr t tp -> IO (Expr t tp)
normExpr sym
sym Expr t tp'
then_
          Expr t tp'
else' <- sym -> Expr t tp' -> IO (Expr t tp')
forall sym (st :: Type -> Type) fs t (tp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym -> Expr t tp -> IO (Expr t tp)
normExpr sym
sym Expr t tp'
else_
          Just App (Expr t) tp'
sm' <- Expr t tp' -> Maybe (App (Expr t) tp')
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
B.asApp (Expr t tp' -> Maybe (App (Expr t) tp'))
-> IO (Expr t tp') -> IO (Maybe (App (Expr t) tp'))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> Pred sym
-> SymExpr sym tp'
-> SymExpr sym tp'
-> IO (SymExpr sym tp')
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
S.baseTypeIte sym
sym Pred sym
Expr t BaseBoolType
test' SymExpr sym tp'
Expr t tp'
then' SymExpr sym tp'
Expr t tp'
else'
          App (Expr t) tp' -> IO (App (Expr t) tp')
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return App (Expr t) tp'
sm'
        go x :: App (Expr t) tp'
x@(S.SemiRingSum WeightedSum (Expr t) sr
sm) =
          case WeightedSum (Expr t) sr -> SemiRingRepr sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr -> SemiRingRepr sr
WSum.sumRepr WeightedSum (Expr t) sr
sm of
            SemiRingRepr sr
S.SemiRingIntegerRepr -> do
              let
                smul :: Integer -> Expr t BaseIntegerType -> IO (Expr t tp')
smul Integer
si Expr t BaseIntegerType
i = do
                    Expr t BaseIntegerType
i' <- sym -> Expr t BaseIntegerType -> IO (Expr t BaseIntegerType)
forall sym (st :: Type -> Type) fs t (tp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym -> Expr t tp -> IO (Expr t tp)
normExpr sym
sym Expr t BaseIntegerType
i
                    Expr t BaseIntegerType
si' <- sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
S.intLit sym
sym Integer
si
                    sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
S.intMul sym
sym SymInteger sym
Expr t BaseIntegerType
si' SymInteger sym
Expr t BaseIntegerType
i'
              Just App (Expr t) tp'
sm' <- Expr t tp' -> Maybe (App (Expr t) tp')
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
B.asApp (Expr t tp' -> Maybe (App (Expr t) tp'))
-> IO (Expr t tp') -> IO (Maybe (App (Expr t) tp'))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr t tp' -> Expr t tp' -> IO (Expr t tp'))
-> (Coefficient sr -> Expr t (SemiRingBase sr) -> IO (Expr t tp'))
-> (Coefficient sr -> IO (Expr t tp'))
-> WeightedSum (Expr t) sr
-> IO (Expr t tp')
forall (m :: Type -> Type) r (sr :: SemiRing)
       (f :: BaseType -> Type).
Monad m =>
(r -> r -> m r)
-> (Coefficient sr -> f (SemiRingBase sr) -> m r)
-> (Coefficient sr -> m r)
-> WeightedSum f sr
-> m r
WSum.evalM ((Expr t tp' -> Expr t tp' -> IO (Expr t tp'))
-> Expr t tp' -> Expr t tp' -> IO (Expr t tp')
forall (tp' :: BaseType) (tp'' :: BaseType) (tp''' :: BaseType).
(Expr t tp' -> Expr t tp'' -> IO (Expr t tp'''))
-> Expr t tp' -> Expr t tp'' -> IO (Expr t tp''')
norm2 ((Expr t tp' -> Expr t tp' -> IO (Expr t tp'))
 -> Expr t tp' -> Expr t tp' -> IO (Expr t tp'))
-> (Expr t tp' -> Expr t tp' -> IO (Expr t tp'))
-> Expr t tp'
-> Expr t tp'
-> IO (Expr t tp')
forall a b. (a -> b) -> a -> b
$ sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
S.intAdd sym
sym) Integer -> Expr t BaseIntegerType -> IO (Expr t tp')
Coefficient sr -> Expr t (SemiRingBase sr) -> IO (Expr t tp')
smul (sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
S.intLit sym
sym) WeightedSum (Expr t) sr
sm
              App (Expr t) tp' -> IO (App (Expr t) tp')
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return App (Expr t) tp'
sm'
            SemiRingRepr sr
_ -> App (Expr t) tp' -> IO (App (Expr t) tp')
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return App (Expr t) tp'
x
        go x :: App (Expr t) tp'
x@(S.SemiRingProd SemiRingProduct (Expr t) sr
pd) =
          case SemiRingProduct (Expr t) sr -> SemiRingRepr sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
SemiRingProduct f sr -> SemiRingRepr sr
WSum.prodRepr SemiRingProduct (Expr t) sr
pd of
            SemiRingRepr sr
S.SemiRingIntegerRepr -> do
                Maybe (Expr t tp')
maybeS <- (Expr t tp' -> Expr t tp' -> IO (Expr t tp'))
-> (Expr t (SemiRingBase sr) -> IO (Expr t tp'))
-> SemiRingProduct (Expr t) sr
-> IO (Maybe (Expr t tp'))
forall (m :: Type -> Type) r (f :: BaseType -> Type)
       (sr :: SemiRing).
Monad m =>
(r -> r -> m r)
-> (f (SemiRingBase sr) -> m r)
-> SemiRingProduct f sr
-> m (Maybe r)
WSum.prodEvalM ((Expr t tp' -> Expr t tp' -> IO (Expr t tp'))
-> Expr t tp' -> Expr t tp' -> IO (Expr t tp')
forall (tp' :: BaseType) (tp'' :: BaseType) (tp''' :: BaseType).
(Expr t tp' -> Expr t tp'' -> IO (Expr t tp'''))
-> Expr t tp' -> Expr t tp'' -> IO (Expr t tp''')
norm2 ((Expr t tp' -> Expr t tp' -> IO (Expr t tp'))
 -> Expr t tp' -> Expr t tp' -> IO (Expr t tp'))
-> (Expr t tp' -> Expr t tp' -> IO (Expr t tp'))
-> Expr t tp'
-> Expr t tp'
-> IO (Expr t tp')
forall a b. (a -> b) -> a -> b
$ sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
S.intMul sym
sym) Expr t tp' -> IO (Expr t tp')
Expr t (SemiRingBase sr) -> IO (Expr t tp')
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return SemiRingProduct (Expr t) sr
pd
                case Maybe (Expr t tp')
maybeS of
                  Just Expr t tp'
s | Just App (Expr t) tp'
sm' <- Expr t tp' -> Maybe (App (Expr t) tp')
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
B.asApp Expr t tp'
s -> App (Expr t) tp' -> IO (App (Expr t) tp')
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return App (Expr t) tp'
sm'
                  Maybe (Expr t tp')
_ -> App (Expr t) tp' -> IO (App (Expr t) tp')
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return App (Expr t) tp'
x
            SemiRingRepr sr
_ -> App (Expr t) tp' -> IO (App (Expr t) tp')
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return App (Expr t) tp'
x
        go x :: App (Expr t) tp'
x@(S.SemiRingLe OrderedSemiRingRepr sr
sr Expr t (SemiRingBase sr)
e1 Expr t (SemiRingBase sr)
e2) = do
          case OrderedSemiRingRepr sr
sr of
            OrderedSemiRingRepr sr
S.OrderedSemiRingIntegerRepr -> do
              Just App (Expr t) tp'
sm' <- Expr t tp' -> Maybe (App (Expr t) tp')
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
B.asApp (Expr t tp' -> Maybe (App (Expr t) tp'))
-> IO (Expr t tp') -> IO (Maybe (App (Expr t) tp'))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Expr t (SemiRingBase sr)
 -> Expr t (SemiRingBase sr) -> IO (Expr t tp'))
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t tp')
forall (tp' :: BaseType) (tp'' :: BaseType) (tp''' :: BaseType).
(Expr t tp' -> Expr t tp'' -> IO (Expr t tp'''))
-> Expr t tp' -> Expr t tp'' -> IO (Expr t tp''')
norm2 ((Expr t (SemiRingBase sr)
  -> Expr t (SemiRingBase sr) -> IO (Expr t tp'))
 -> Expr t (SemiRingBase sr)
 -> Expr t (SemiRingBase sr)
 -> IO (Expr t tp'))
-> (Expr t (SemiRingBase sr)
    -> Expr t (SemiRingBase sr) -> IO (Expr t tp'))
-> Expr t (SemiRingBase sr)
-> Expr t (SemiRingBase sr)
-> IO (Expr t tp')
forall a b. (a -> b) -> a -> b
$ sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
S.intLe sym
sym) Expr t (SemiRingBase sr)
e1 Expr t (SemiRingBase sr)
e2
              App (Expr t) tp' -> IO (App (Expr t) tp')
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return App (Expr t) tp'
sm'
            OrderedSemiRingRepr sr
_ -> App (Expr t) tp' -> IO (App (Expr t) tp')
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return App (Expr t) tp'
x
        go App (Expr t) tp'
x = App (Expr t) tp' -> IO (App (Expr t) tp')
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return App (Expr t) tp'
x



data ExprEquivResult = ExprEquivalent | ExprNormEquivalent | ExprUnequal

testEquivExpr :: forall sym st fs t tp tp'. sym ~ S.ExprBuilder t st fs => sym -> B.Expr t tp -> B.Expr t tp' -> IO (ExprEquivResult)
testEquivExpr :: forall sym (st :: Type -> Type) fs t (tp :: BaseType)
       (tp' :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym -> Expr t tp -> Expr t tp' -> IO ExprEquivResult
testEquivExpr sym
sym Expr t tp
e1 Expr t tp'
e2 = case Expr t tp -> Expr t tp' -> Maybe (tp :~: tp')
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: BaseType) (b :: BaseType).
Expr t a -> Expr t b -> Maybe (a :~: b)
testEquality Expr t tp
e1 Expr t tp'
e2 of
  Just tp :~: tp'
Refl -> ExprEquivResult -> IO ExprEquivResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExprEquivResult
ExprEquivalent
  Maybe (tp :~: tp')
_ -> do
    Expr t tp
e1' <- sym -> Expr t tp -> IO (Expr t tp)
forall sym (st :: Type -> Type) fs t (tp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym -> Expr t tp -> IO (Expr t tp)
normExpr sym
sym Expr t tp
e1
    Expr t tp'
e2' <- sym -> Expr t tp' -> IO (Expr t tp')
forall sym (st :: Type -> Type) fs t (tp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym -> Expr t tp -> IO (Expr t tp)
normExpr sym
sym Expr t tp'
e2
    case Expr t tp -> Expr t tp' -> Maybe (tp :~: tp')
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: BaseType) (b :: BaseType).
Expr t a -> Expr t b -> Maybe (a :~: b)
testEquality Expr t tp
e1' Expr t tp'
e2' of
      Just tp :~: tp'
Refl -> ExprEquivResult -> IO ExprEquivResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExprEquivResult
ExprNormEquivalent
      Maybe (tp :~: tp')
_ -> ExprEquivResult -> IO ExprEquivResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExprEquivResult
ExprUnequal

testEquivSymFn :: forall sym st fs t args ret args' ret'. sym ~ S.ExprBuilder t st fs => sym -> S.SymFn sym args ret -> S.SymFn sym args' ret' -> IO (ExprEquivResult)
testEquivSymFn :: forall sym (st :: Type -> Type) fs t (args :: Ctx BaseType)
       (ret :: BaseType) (args' :: Ctx BaseType) (ret' :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym
-> SymFn sym args ret -> SymFn sym args' ret' -> IO ExprEquivResult
testEquivSymFn sym
sym SymFn sym args ret
fn1 SymFn sym args' ret'
fn2 =
  let
    argTypes1 :: Assignment BaseTypeRepr args
argTypes1 = ExprSymFn t args ret -> Assignment BaseTypeRepr args
forall (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Assignment BaseTypeRepr args
forall (fn :: Ctx BaseType -> BaseType -> Type)
       (args :: Ctx BaseType) (ret :: BaseType).
IsSymFn fn =>
fn args ret -> Assignment BaseTypeRepr args
S.fnArgTypes SymFn sym args ret
ExprSymFn t args ret
fn1
    argTypes2 :: Assignment BaseTypeRepr args'
argTypes2 = ExprSymFn t args' ret' -> Assignment BaseTypeRepr args'
forall (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Assignment BaseTypeRepr args
forall (fn :: Ctx BaseType -> BaseType -> Type)
       (args :: Ctx BaseType) (ret :: BaseType).
IsSymFn fn =>
fn args ret -> Assignment BaseTypeRepr args
S.fnArgTypes SymFn sym args' ret'
ExprSymFn t args' ret'
fn2
    retType1 :: BaseTypeRepr ret
retType1 = ExprSymFn t args ret -> BaseTypeRepr ret
forall (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> BaseTypeRepr ret
forall (fn :: Ctx BaseType -> BaseType -> Type)
       (args :: Ctx BaseType) (ret :: BaseType).
IsSymFn fn =>
fn args ret -> BaseTypeRepr ret
S.fnReturnType SymFn sym args ret
ExprSymFn t args ret
fn1
    retType2 :: BaseTypeRepr ret'
retType2 = ExprSymFn t args' ret' -> BaseTypeRepr ret'
forall (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> BaseTypeRepr ret
forall (fn :: Ctx BaseType -> BaseType -> Type)
       (args :: Ctx BaseType) (ret :: BaseType).
IsSymFn fn =>
fn args ret -> BaseTypeRepr ret
S.fnReturnType SymFn sym args' ret'
ExprSymFn t args' ret'
fn2
  in if | Just args :~: args'
Refl <- Assignment BaseTypeRepr args
-> Assignment BaseTypeRepr args' -> Maybe (args :~: args')
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx BaseType) (b :: Ctx BaseType).
Assignment BaseTypeRepr a
-> Assignment BaseTypeRepr b -> Maybe (a :~: b)
testEquality Assignment BaseTypeRepr args
argTypes1 Assignment BaseTypeRepr args'
argTypes2
        , Just ret :~: ret'
Refl <- BaseTypeRepr ret -> BaseTypeRepr ret' -> Maybe (ret :~: ret')
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: BaseType) (b :: BaseType).
BaseTypeRepr a -> BaseTypeRepr b -> Maybe (a :~: b)
testEquality BaseTypeRepr ret
retType1 BaseTypeRepr ret'
retType2
        , ExprSymFn t args ret -> SolverSymbol
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SolverSymbol
B.symFnName SymFn sym args ret
ExprSymFn t args ret
fn1 SolverSymbol -> SolverSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprSymFn t args ret -> SolverSymbol
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SolverSymbol
B.symFnName SymFn sym args' ret'
ExprSymFn t args ret
fn2 ->
          case (ExprSymFn t args ret -> SymFnInfo t args ret
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SymFnInfo t args ret
S.symFnInfo SymFn sym args ret
ExprSymFn t args ret
fn1, ExprSymFn t args ret -> SymFnInfo t args ret
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SymFnInfo t args ret
S.symFnInfo SymFn sym args' ret'
ExprSymFn t args ret
fn2) of
           (S.DefinedFnInfo Assignment (ExprBoundVar t) args
argBVs1 Expr t ret
efn1 UnfoldPolicy
_, S.DefinedFnInfo Assignment (ExprBoundVar t) args
argBVs2 Expr t ret
efn2 UnfoldPolicy
_) -> do
             Assignment (Expr t) args
args <- (forall (x :: BaseType). ExprBoundVar t x -> IO (Expr t x))
-> forall (x :: Ctx BaseType).
   Assignment (ExprBoundVar t) x -> IO (Assignment (Expr t) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: BaseType -> Type) (g :: BaseType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: BaseType). f x -> m (g x))
-> forall (x :: Ctx BaseType). Assignment f x -> m (Assignment g x)
FC.traverseFC (\ExprBoundVar t x
bv -> sym -> SolverSymbol -> BaseTypeRepr x -> IO (SymExpr sym x)
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
S.freshConstant sym
sym (ExprBoundVar t x -> SolverSymbol
forall t (tp :: BaseType). ExprBoundVar t tp -> SolverSymbol
S.bvarName ExprBoundVar t x
bv) (ExprBoundVar t x -> BaseTypeRepr x
forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
B.bvarType ExprBoundVar t x
bv)) Assignment (ExprBoundVar t) args
argBVs1
             Expr t ret
expr1 <- ExprBuilder t st fs
-> Expr t ret
-> Assignment (ExprBoundVar t) args
-> Assignment (Expr t) args
-> IO (Expr t ret)
forall t (st :: Type -> Type) fs (ret :: BaseType)
       (args :: Ctx BaseType).
ExprBuilder t st fs
-> Expr t ret
-> Assignment (ExprBoundVar t) args
-> Assignment (Expr t) args
-> IO (Expr t ret)
B.evalBoundVars sym
ExprBuilder t st fs
sym Expr t ret
efn1 Assignment (ExprBoundVar t) args
argBVs1 Assignment (Expr t) args
args
             Expr t ret
expr2 <- ExprBuilder t st fs
-> Expr t ret
-> Assignment (ExprBoundVar t) args
-> Assignment (Expr t) args
-> IO (Expr t ret)
forall t (st :: Type -> Type) fs (ret :: BaseType)
       (args :: Ctx BaseType).
ExprBuilder t st fs
-> Expr t ret
-> Assignment (ExprBoundVar t) args
-> Assignment (Expr t) args
-> IO (Expr t ret)
B.evalBoundVars sym
ExprBuilder t st fs
sym Expr t ret
efn2 Assignment (ExprBoundVar t) args
argBVs2 Assignment (Expr t) args
args
             case Expr t ret -> Expr t ret -> Maybe (ret :~: ret)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: BaseType) (b :: BaseType).
Expr t a -> Expr t b -> Maybe (a :~: b)
testEquality Expr t ret
expr1 Expr t ret
expr2 of
               Just ret :~: ret
Refl -> ExprEquivResult -> IO ExprEquivResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExprEquivResult
ExprEquivalent
               Maybe (ret :~: ret)
Nothing -> do
                 Expr t ret
expr1' <- sym -> Expr t ret -> IO (Expr t ret)
forall sym (st :: Type -> Type) fs t (tp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym -> Expr t tp -> IO (Expr t tp)
normExpr sym
sym Expr t ret
expr1
                 Expr t ret
expr2' <- sym -> Expr t ret -> IO (Expr t ret)
forall sym (st :: Type -> Type) fs t (tp :: BaseType).
(sym ~ ExprBuilder t st fs) =>
sym -> Expr t tp -> IO (Expr t tp)
normExpr sym
sym Expr t ret
expr2
                 case Expr t ret -> Expr t ret -> Maybe (ret :~: ret)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: BaseType) (b :: BaseType).
Expr t a -> Expr t b -> Maybe (a :~: b)
testEquality Expr t ret
expr1' Expr t ret
expr2' of
                   Just ret :~: ret
Refl -> ExprEquivResult -> IO ExprEquivResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExprEquivResult
ExprNormEquivalent
                   Maybe (ret :~: ret)
Nothing -> ExprEquivResult -> IO ExprEquivResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExprEquivResult
ExprUnequal
           (S.UninterpFnInfo Assignment BaseTypeRepr args
_ BaseTypeRepr ret
_, S.UninterpFnInfo Assignment BaseTypeRepr args
_ BaseTypeRepr ret
_) -> ExprEquivResult -> IO ExprEquivResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExprEquivResult
ExprEquivalent
           (S.MatlabSolverFnInfo MatlabSolverFn (Expr t) args ret
_ Assignment (ExprBoundVar t) args
_ Expr t ret
_, SymFnInfo t args ret
_) -> String -> IO ExprEquivResult
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Unsupported function type for equivalence check."
           (SymFnInfo t args ret
_, S.MatlabSolverFnInfo MatlabSolverFn (Expr t) args ret
_ Assignment (ExprBoundVar t) args
_ Expr t ret
_) -> String -> IO ExprEquivResult
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Unsupported function type for equivalence check."
           (SymFnInfo t args ret
_, SymFnInfo t args ret
_) -> ExprEquivResult -> IO ExprEquivResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExprEquivResult
ExprUnequal
        | Bool
otherwise -> ExprEquivResult -> IO ExprEquivResult
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExprEquivResult
ExprUnequal