{-# 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 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 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)
FC.traverseFC (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' <- 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
sym Expr t ret
expr Assignment (ExprBoundVar t) args
argBVs Assignment (Expr t) args
argEs'
    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
_ -> forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
S.applySymFn sym
sym ExprSymFn t args ret
symFn 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
_) = forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
S.intLit sym
sym Coefficient sr
val
        go (B.AppExpr AppExpr t tp
appExpr) = 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 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 -> 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
_ -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
x
        go Expr t tp
x = 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' <- forall (tp' :: BaseType). App (Expr t) tp' -> IO (App (Expr t) tp')
go (forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
S.appExprApp AppExpr t tp
ae)
  forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
B.sbMakeExpr sym
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' <- 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' <- 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' <- 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' <- 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' <- 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' <- forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
B.asApp forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
S.baseTypeIte sym
sym Expr t BaseBoolType
test' Expr t tp'
then' Expr t tp'
else'
          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 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' <- 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' <- forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
S.intLit sym
sym Integer
si
                    forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
S.intMul sym
sym Expr t BaseIntegerType
si' Expr t BaseIntegerType
i'
              Just App (Expr t) tp'
sm' <- forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
B.asApp forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (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 forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
S.intAdd sym
sym) Integer -> Expr t BaseIntegerType -> IO (Expr t tp')
smul (forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
S.intLit sym
sym) WeightedSum (Expr t) sr
sm
              forall (m :: Type -> Type) a. Monad m => a -> m a
return App (Expr t) tp'
sm'
            SemiRingRepr sr
_ -> 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 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 <- 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 (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 forall a b. (a -> b) -> a -> b
$ forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
S.intMul sym
sym) 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' <- forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
B.asApp Expr t tp'
s -> forall (m :: Type -> Type) a. Monad m => a -> m a
return App (Expr t) tp'
sm'
                  Maybe (Expr t tp')
_ -> forall (m :: Type -> Type) a. Monad m => a -> m a
return App (Expr t) tp'
x
            SemiRingRepr sr
_ -> 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' <- forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
B.asApp forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (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 forall a b. (a -> b) -> a -> b
$ 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
              forall (m :: Type -> Type) a. Monad m => a -> m a
return App (Expr t) tp'
sm'
            OrderedSemiRingRepr sr
_ -> forall (m :: Type -> Type) a. Monad m => a -> m a
return App (Expr t) tp'
x
        go App (Expr t) tp'
x = 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 forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Expr t tp
e1 Expr t tp'
e2 of
  Just tp :~: tp'
Refl -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ExprEquivResult
ExprEquivalent
  Maybe (tp :~: tp')
_ -> do
    Expr t tp
e1' <- 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' <- 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 forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Expr t tp
e1' Expr t tp'
e2' of
      Just tp :~: tp'
Refl -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ExprEquivResult
ExprNormEquivalent
      Maybe (tp :~: tp')
_ -> 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 = 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
fn1
    argTypes2 :: Assignment BaseTypeRepr args'
argTypes2 = 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'
fn2
    retType1 :: BaseTypeRepr ret
retType1 = forall (fn :: Ctx BaseType -> BaseType -> Type)
       (args :: Ctx BaseType) (ret :: BaseType).
IsSymFn fn =>
fn args ret -> BaseTypeRepr ret
S.fnReturnType SymFn sym args ret
fn1
    retType2 :: BaseTypeRepr ret'
retType2 = forall (fn :: Ctx BaseType -> BaseType -> Type)
       (args :: Ctx BaseType) (ret :: BaseType).
IsSymFn fn =>
fn args ret -> BaseTypeRepr ret
S.fnReturnType SymFn sym args' ret'
fn2
  in if | Just args :~: args'
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Assignment BaseTypeRepr args
argTypes1 Assignment BaseTypeRepr args'
argTypes2
        , Just ret :~: ret'
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality BaseTypeRepr ret
retType1 BaseTypeRepr ret'
retType2
        , forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SolverSymbol
B.symFnName SymFn sym args ret
fn1 forall a. Eq a => a -> a -> Bool
== forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SolverSymbol
B.symFnName SymFn sym args' ret'
fn2 ->
          case (forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SymFnInfo t args ret
S.symFnInfo SymFn sym args ret
fn1, forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SymFnInfo t args ret
S.symFnInfo SymFn sym 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 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)
FC.traverseFC (\ExprBoundVar t x
bv -> forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
S.freshConstant sym
sym (forall t (tp :: BaseType). ExprBoundVar t tp -> SolverSymbol
S.bvarName ExprBoundVar t x
bv) (forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
B.bvarType ExprBoundVar t x
bv)) Assignment (ExprBoundVar t) args
argBVs1
             Expr t ret
expr1 <- 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
sym Expr t ret
efn1 Assignment (ExprBoundVar t) args
argBVs1 Assignment (Expr t) args
args
             Expr t ret
expr2 <- 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
sym Expr t ret
efn2 Assignment (ExprBoundVar t) args
argBVs2 Assignment (Expr t) args
args
             case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Expr t ret
expr1 Expr t ret
expr2 of
               Just ret :~: ret
Refl -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ExprEquivResult
ExprEquivalent
               Maybe (ret :~: ret)
Nothing -> do
                 Expr t ret
expr1' <- 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' <- 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 forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Expr t ret
expr1' Expr t ret
expr2' of
                   Just ret :~: ret
Refl -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ExprEquivResult
ExprNormEquivalent
                   Maybe (ret :~: ret)
Nothing -> 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
_) -> 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
_) -> 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
_) -> 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
_) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ExprEquivResult
ExprUnequal
        | Bool
otherwise -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ExprEquivResult
ExprUnequal