    {-# 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
        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' <- B.evalBoundVars sym expr argBVs argEs'
        normExpr sym 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
      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)
      B.sbMakeExpr sym 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
              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
              e2' <- normExpr sym e2
              f e1' 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
              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
              then' <- normExpr sym then_
              else' <- normExpr sym else_
              Just sm' <- B.asApp <$> S.baseTypeIte sym test' then' else'
              return 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
                        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
                        si' <- S.intLit sym si
                        S.intMul sym si' i'
                  Just 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
                  return 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
                    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 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 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
                  return 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
        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
        e2' <- normExpr sym e2
        case testEquality e1' 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
                 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
                 expr1 <- B.evalBoundVars sym efn1 argBVs1 args
                 expr2 <- B.evalBoundVars sym efn2 argBVs2 args
                 case testEquality expr1 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
                     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
                     expr2' <- normExpr sym expr2
                     case testEquality expr1' 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