{-|
Module      : What4.Expr.App
Copyright   : (c) Galois Inc, 2015-2020
License     : BSD3
Maintainer  : jhendrix@galois.com

This module defines datastructures that encode the basic
syntax formers used in What4.ExprBuilder.
-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module What4.Expr.App where

import qualified Control.Exception as Ex
import           Control.Lens hiding (asIndex, (:>), Empty)
import           Control.Monad
import           Control.Monad.ST
import qualified Data.BitVector.Sized as BV
import           Data.Foldable
import           Data.Hashable
import qualified Data.HashTable.Class as H (toList)
import qualified Data.HashTable.ST.Basic as H
import           Data.Kind
import           Data.List.NonEmpty (NonEmpty(..))
import qualified Data.Map.Strict as Map
import           Data.Maybe
import           Data.Parameterized.Classes
import           Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.HashTable as PH
import           Data.Parameterized.NatRepr
import           Data.Parameterized.Nonce
import           Data.Parameterized.Some
import           Data.Parameterized.TH.GADT
import           Data.Parameterized.TraversableFC
import           Data.Ratio (numerator, denominator)
import qualified Data.Sequence as Seq
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.STRef
import           Data.String
import           Data.Text (Text)
import qualified Data.Text as Text
import           Data.Word (Word64)
import           GHC.Generics (Generic)
import           LibBF (BigFloat)
import qualified LibBF as BF
import           Numeric.Natural
import           Prettyprinter hiding (Unbounded)

import           What4.BaseTypes
import           What4.Concrete
import           What4.Interface
import           What4.ProgramLoc
import qualified What4.SemiRing as SR
import qualified What4.Expr.ArrayUpdateMap as AUM
import           What4.Expr.BoolMap (BoolMap, Polarity(..), BoolMapView(..), Wrap(..))
import qualified What4.Expr.BoolMap as BM
import           What4.Expr.MATLAB
import           What4.Expr.WeightedSum (WeightedSum, SemiRingProduct)
import qualified What4.Expr.WeightedSum as WSum
import qualified What4.Expr.StringSeq as SSeq
import           What4.Expr.UnaryBV (UnaryBV)
import qualified What4.Expr.UnaryBV as UnaryBV

import           What4.Utils.AbstractDomains
import           What4.Utils.Arithmetic
import qualified What4.Utils.BVDomain as BVD
import           What4.Utils.Complex
import           What4.Utils.IncrHash
import qualified What4.Utils.AnnotatedMap as AM


-- | This type represents 'Expr' values that were built from a
-- 'NonceApp'.
--
-- Parameter @t@ is a phantom type brand used to track nonces.
--
-- Selector functions are provided to destruct 'NonceAppExpr' values,
-- but the constructor is kept hidden. The preferred way to construct
-- an 'Expr' from a 'NonceApp' is to use 'sbNonceExpr'.
data NonceAppExpr t (tp :: BaseType)
   = NonceAppExprCtor { NonceAppExpr t tp -> Nonce t tp
nonceExprId  :: {-# UNPACK #-} !(Nonce t tp)
                     , NonceAppExpr t tp -> ProgramLoc
nonceExprLoc :: !ProgramLoc
                     , NonceAppExpr t tp -> NonceApp t (Expr t) tp
nonceExprApp :: !(NonceApp t (Expr t) tp)
                     , NonceAppExpr t tp -> AbstractValue tp
nonceExprAbsValue :: !(AbstractValue tp)
                     }

-- | This type represents 'Expr' values that were built from an 'App'.
--
-- Parameter @t@ is a phantom type brand used to track nonces.
--
-- Selector functions are provided to destruct 'AppExpr' values, but
-- the constructor is kept hidden. The preferred way to construct an
-- 'Expr' from an 'App' is to use 'sbMakeExpr'.
data AppExpr t (tp :: BaseType)
   = AppExprCtor { AppExpr t tp -> Nonce t tp
appExprId  :: {-# UNPACK #-} !(Nonce t tp)
                , AppExpr t tp -> ProgramLoc
appExprLoc :: !ProgramLoc
                , AppExpr t tp -> App (Expr t) tp
appExprApp :: !(App (Expr t) tp)
                , AppExpr t tp -> AbstractValue tp
appExprAbsValue :: !(AbstractValue tp)
                }

------------------------------------------------------------------------
-- Expr

-- | The main ExprBuilder expression datastructure.  The non-trivial @Expr@
-- values constructed by this module are uniquely identified by a
-- nonce value that is used to explicitly represent sub-term sharing.
-- When traversing the structure of an @Expr@ it is usually very important
-- to memoize computations based on the values of these identifiers to avoid
-- exponential blowups due to shared term structure.
--
-- Type parameter @t@ is a phantom type brand used to relate nonces to
-- a specific nonce generator (similar to the @s@ parameter of the
-- @ST@ monad). The type index @tp@ of kind 'BaseType' indicates the
-- type of the values denoted by the given expression.
--
-- Type @'Expr' t@ instantiates the type family @'SymExpr'
-- ('ExprBuilder' t st)@.
data Expr t (tp :: BaseType) where
  SemiRingLiteral :: !(SR.SemiRingRepr sr) -> !(SR.Coefficient sr) -> !ProgramLoc -> Expr t (SR.SemiRingBase sr)
  BoolExpr :: !Bool -> !ProgramLoc -> Expr t BaseBoolType
  FloatExpr :: !(FloatPrecisionRepr fpp) -> !BigFloat -> !ProgramLoc -> Expr t (BaseFloatType fpp)
  StringExpr :: !(StringLiteral si) -> !ProgramLoc -> Expr t (BaseStringType si)
  -- Application
  AppExpr :: {-# UNPACK #-} !(AppExpr t tp) -> Expr t tp
  -- An atomic predicate
  NonceAppExpr :: {-# UNPACK #-} !(NonceAppExpr t tp) -> Expr t tp
  -- A bound variable
  BoundVarExpr :: !(ExprBoundVar t tp) -> Expr t tp

-- | Destructor for the 'AppExpr' constructor.
{-# INLINE asApp #-}
asApp :: Expr t tp -> Maybe (App (Expr t) tp)
asApp :: Expr t tp -> Maybe (App (Expr t) tp)
asApp (AppExpr AppExpr t tp
a) = App (Expr t) tp -> Maybe (App (Expr t) tp)
forall a. a -> Maybe a
Just (AppExpr t tp -> App (Expr t) tp
forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
appExprApp AppExpr t tp
a)
asApp Expr t tp
_ = Maybe (App (Expr t) tp)
forall a. Maybe a
Nothing

-- | Destructor for the 'NonceAppExpr' constructor.
{-# INLINE asNonceApp #-}
asNonceApp :: Expr t tp -> Maybe (NonceApp t (Expr t) tp)
asNonceApp :: Expr t tp -> Maybe (NonceApp t (Expr t) tp)
asNonceApp (NonceAppExpr NonceAppExpr t tp
a) = NonceApp t (Expr t) tp -> Maybe (NonceApp t (Expr t) tp)
forall a. a -> Maybe a
Just (NonceAppExpr t tp -> NonceApp t (Expr t) tp
forall t (tp :: BaseType).
NonceAppExpr t tp -> NonceApp t (Expr t) tp
nonceExprApp NonceAppExpr t tp
a)
asNonceApp Expr t tp
_ = Maybe (NonceApp t (Expr t) tp)
forall a. Maybe a
Nothing

exprLoc :: Expr t tp -> ProgramLoc
exprLoc :: Expr t tp -> ProgramLoc
exprLoc (SemiRingLiteral SemiRingRepr sr
_ Coefficient sr
_ ProgramLoc
l) = ProgramLoc
l
exprLoc (BoolExpr Bool
_ ProgramLoc
l) = ProgramLoc
l
exprLoc (FloatExpr FloatPrecisionRepr fpp
_ BigFloat
_ ProgramLoc
l) = ProgramLoc
l
exprLoc (StringExpr StringLiteral si
_ ProgramLoc
l) = ProgramLoc
l
exprLoc (NonceAppExpr NonceAppExpr t tp
a)  = NonceAppExpr t tp -> ProgramLoc
forall t (tp :: BaseType). NonceAppExpr t tp -> ProgramLoc
nonceExprLoc NonceAppExpr t tp
a
exprLoc (AppExpr AppExpr t tp
a)   = AppExpr t tp -> ProgramLoc
forall t (tp :: BaseType). AppExpr t tp -> ProgramLoc
appExprLoc AppExpr t tp
a
exprLoc (BoundVarExpr ExprBoundVar t tp
v) = ExprBoundVar t tp -> ProgramLoc
forall t (tp :: BaseType). ExprBoundVar t tp -> ProgramLoc
bvarLoc ExprBoundVar t tp
v

mkExpr :: Nonce t tp
      -> ProgramLoc
      -> App (Expr t) tp
      -> AbstractValue tp
      -> Expr t tp
mkExpr :: Nonce t tp
-> ProgramLoc -> App (Expr t) tp -> AbstractValue tp -> Expr t tp
mkExpr Nonce t tp
n ProgramLoc
l App (Expr t) tp
a AbstractValue tp
v = AppExpr t tp -> Expr t tp
forall t (tp :: BaseType). AppExpr t tp -> Expr t tp
AppExpr (AppExpr t tp -> Expr t tp) -> AppExpr t tp -> Expr t tp
forall a b. (a -> b) -> a -> b
$ AppExprCtor :: forall t (tp :: BaseType).
Nonce t tp
-> ProgramLoc
-> App (Expr t) tp
-> AbstractValue tp
-> AppExpr t tp
AppExprCtor { appExprId :: Nonce t tp
appExprId  = Nonce t tp
n
                                    , appExprLoc :: ProgramLoc
appExprLoc = ProgramLoc
l
                                    , appExprApp :: App (Expr t) tp
appExprApp = App (Expr t) tp
a
                                    , appExprAbsValue :: AbstractValue tp
appExprAbsValue = AbstractValue tp
v
                                    }



type BoolExpr t = Expr t BaseBoolType
type FloatExpr t fpp = Expr t (BaseFloatType fpp)
type BVExpr t n = Expr t (BaseBVType n)
type IntegerExpr t = Expr t BaseIntegerType
type RealExpr t = Expr t BaseRealType
type CplxExpr t = Expr t BaseComplexType
type StringExpr t si = Expr t (BaseStringType si)



iteSize :: Expr t tp -> Integer
iteSize :: Expr t tp -> Integer
iteSize Expr t tp
e =
  case Expr t tp -> Maybe (App (Expr t) tp)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp Expr t tp
e of
    Just (BaseIte BaseTypeRepr tp
_ Integer
sz Expr t BaseBoolType
_ Expr t tp
_ Expr t tp
_) -> Integer
sz
    Maybe (App (Expr t) tp)
_ -> Integer
0

instance IsExpr (Expr t) where
  asConstantPred :: Expr t BaseBoolType -> Maybe Bool
asConstantPred = Expr t BaseBoolType -> Maybe Bool
forall t (tp :: BaseType). Expr t tp -> AbstractValue tp
exprAbsValue

  asInteger :: Expr t BaseIntegerType -> Maybe Integer
asInteger (SemiRingLiteral SemiRingRepr sr
SR.SemiRingIntegerRepr Coefficient sr
n ProgramLoc
_) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
Coefficient sr
n
  asInteger Expr t BaseIntegerType
_ = Maybe Integer
forall a. Maybe a
Nothing

  integerBounds :: Expr t BaseIntegerType -> ValueRange Integer
integerBounds Expr t BaseIntegerType
x = Expr t BaseIntegerType -> AbstractValue BaseIntegerType
forall t (tp :: BaseType). Expr t tp -> AbstractValue tp
exprAbsValue Expr t BaseIntegerType
x

  asRational :: Expr t BaseRealType -> Maybe Rational
asRational (SemiRingLiteral SemiRingRepr sr
SR.SemiRingRealRepr Coefficient sr
r ProgramLoc
_) = Rational -> Maybe Rational
forall a. a -> Maybe a
Just Rational
Coefficient sr
r
  asRational Expr t BaseRealType
_ = Maybe Rational
forall a. Maybe a
Nothing

  rationalBounds :: Expr t BaseRealType -> ValueRange Rational
rationalBounds Expr t BaseRealType
x = RealAbstractValue -> ValueRange Rational
ravRange (RealAbstractValue -> ValueRange Rational)
-> RealAbstractValue -> ValueRange Rational
forall a b. (a -> b) -> a -> b
$ Expr t BaseRealType -> AbstractValue BaseRealType
forall t (tp :: BaseType). Expr t tp -> AbstractValue tp
exprAbsValue Expr t BaseRealType
x

  asFloat :: Expr t (BaseFloatType fpp) -> Maybe BigFloat
asFloat (FloatExpr FloatPrecisionRepr fpp
_fpp BigFloat
bf ProgramLoc
_) = BigFloat -> Maybe BigFloat
forall a. a -> Maybe a
Just BigFloat
bf
  asFloat Expr t (BaseFloatType fpp)
_ = Maybe BigFloat
forall a. Maybe a
Nothing

  asComplex :: Expr t BaseComplexType -> Maybe (Complex Rational)
asComplex Expr t BaseComplexType
e
    | Just (Cplx Complex (Expr t BaseRealType)
c) <- Expr t BaseComplexType -> Maybe (App (Expr t) BaseComplexType)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp Expr t BaseComplexType
e = (Expr t BaseRealType -> Maybe Rational)
-> Complex (Expr t BaseRealType) -> Maybe (Complex Rational)
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr t BaseRealType -> Maybe Rational
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseRealType -> Maybe Rational
asRational Complex (Expr t BaseRealType)
c
    | Bool
otherwise = Maybe (Complex Rational)
forall a. Maybe a
Nothing

  exprType :: Expr t tp -> BaseTypeRepr tp
exprType (SemiRingLiteral SemiRingRepr sr
sr Coefficient sr
_ ProgramLoc
_) = SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
forall (sr :: SemiRing).
SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
SR.semiRingBase SemiRingRepr sr
sr
  exprType (BoolExpr Bool
_ ProgramLoc
_) = BaseTypeRepr tp
BaseTypeRepr BaseBoolType
BaseBoolRepr
  exprType (FloatExpr FloatPrecisionRepr fpp
fpp BigFloat
_ ProgramLoc
_) = FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr fpp
fpp
  exprType (StringExpr StringLiteral si
s ProgramLoc
_) = StringInfoRepr si -> BaseTypeRepr (BaseStringType si)
forall (si :: StringInfo).
StringInfoRepr si -> BaseTypeRepr (BaseStringType si)
BaseStringRepr (StringLiteral si -> StringInfoRepr si
forall (si :: StringInfo). StringLiteral si -> StringInfoRepr si
stringLiteralInfo StringLiteral si
s)
  exprType (NonceAppExpr NonceAppExpr t tp
e)  = NonceApp t (Expr t) tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) t (tp :: BaseType).
IsExpr e =>
NonceApp t e tp -> BaseTypeRepr tp
nonceAppType (NonceAppExpr t tp -> NonceApp t (Expr t) tp
forall t (tp :: BaseType).
NonceAppExpr t tp -> NonceApp t (Expr t) tp
nonceExprApp NonceAppExpr t tp
e)
  exprType (AppExpr AppExpr t tp
e) = App (Expr t) tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
App e tp -> BaseTypeRepr tp
appType (AppExpr t tp -> App (Expr t) tp
forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
appExprApp AppExpr t tp
e)
  exprType (BoundVarExpr ExprBoundVar t tp
i) = ExprBoundVar t tp -> BaseTypeRepr tp
forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
bvarType ExprBoundVar t tp
i

  asBV :: Expr t (BaseBVType w) -> Maybe (BV w)
asBV (SemiRingLiteral (SR.SemiRingBVRepr BVFlavorRepr fv
_ NatRepr w
_) Coefficient sr
i ProgramLoc
_) = BV w -> Maybe (BV w)
forall a. a -> Maybe a
Just BV w
Coefficient sr
i
  asBV Expr t (BaseBVType w)
_ = Maybe (BV w)
forall a. Maybe a
Nothing

  unsignedBVBounds :: Expr t (BaseBVType w) -> Maybe (Integer, Integer)
unsignedBVBounds Expr t (BaseBVType w)
x = (Integer, Integer) -> Maybe (Integer, Integer)
forall a. a -> Maybe a
Just ((Integer, Integer) -> Maybe (Integer, Integer))
-> (Integer, Integer) -> Maybe (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ BVDomain w -> (Integer, Integer)
forall (w :: Nat). BVDomain w -> (Integer, Integer)
BVD.ubounds (BVDomain w -> (Integer, Integer))
-> BVDomain w -> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ Expr t (BaseBVType w) -> AbstractValue (BaseBVType w)
forall t (tp :: BaseType). Expr t tp -> AbstractValue tp
exprAbsValue Expr t (BaseBVType w)
x
  signedBVBounds :: Expr t (BaseBVType w) -> Maybe (Integer, Integer)
signedBVBounds Expr t (BaseBVType w)
x = (Integer, Integer) -> Maybe (Integer, Integer)
forall a. a -> Maybe a
Just ((Integer, Integer) -> Maybe (Integer, Integer))
-> (Integer, Integer) -> Maybe (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BVDomain w -> (Integer, Integer)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BVDomain w -> (Integer, Integer)
BVD.sbounds (Expr t (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr t (BaseBVType w)
x) (BVDomain w -> (Integer, Integer))
-> BVDomain w -> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ Expr t (BaseBVType w) -> AbstractValue (BaseBVType w)
forall t (tp :: BaseType). Expr t tp -> AbstractValue tp
exprAbsValue Expr t (BaseBVType w)
x

  asAffineVar :: Expr t tp -> Maybe (ConcreteVal tp, Expr t tp, ConcreteVal tp)
asAffineVar Expr t tp
e = case Expr t tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType Expr t tp
e of
    BaseTypeRepr tp
BaseIntegerRepr
      | Just (Coefficient SemiRingInteger
a, Expr t (SemiRingBase SemiRingInteger)
x, Coefficient SemiRingInteger
b) <- WeightedSum (Expr t) SemiRingInteger
-> Maybe
     (Coefficient SemiRingInteger,
      Expr t (SemiRingBase SemiRingInteger), Coefficient SemiRingInteger)
forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr
-> Maybe (Coefficient sr, f (SemiRingBase sr), Coefficient sr)
WSum.asAffineVar (WeightedSum (Expr t) SemiRingInteger
 -> Maybe
      (Coefficient SemiRingInteger,
       Expr t (SemiRingBase SemiRingInteger),
       Coefficient SemiRingInteger))
-> WeightedSum (Expr t) SemiRingInteger
-> Maybe
     (Coefficient SemiRingInteger,
      Expr t (SemiRingBase SemiRingInteger), Coefficient SemiRingInteger)
forall a b. (a -> b) -> a -> b
$
          SemiRingRepr SemiRingInteger
-> Expr t (SemiRingBase SemiRingInteger)
-> WeightedSum (Expr t) SemiRingInteger
forall t (sr :: SemiRing).
HashableF (Expr t) =>
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
asWeightedSum SemiRingRepr SemiRingInteger
SR.SemiRingIntegerRepr Expr t tp
Expr t (SemiRingBase SemiRingInteger)
e ->
        (ConcreteVal BaseIntegerType, Expr t tp,
 ConcreteVal BaseIntegerType)
-> Maybe
     (ConcreteVal BaseIntegerType, Expr t tp,
      ConcreteVal BaseIntegerType)
forall a. a -> Maybe a
Just (Integer -> ConcreteVal BaseIntegerType
ConcreteInteger Integer
Coefficient SemiRingInteger
a, Expr t tp
Expr t (SemiRingBase SemiRingInteger)
x, Integer -> ConcreteVal BaseIntegerType
ConcreteInteger Integer
Coefficient SemiRingInteger
b)
    BaseTypeRepr tp
BaseRealRepr
      | Just (Coefficient SemiRingReal
a, Expr t (SemiRingBase SemiRingReal)
x, Coefficient SemiRingReal
b) <- WeightedSum (Expr t) SemiRingReal
-> Maybe
     (Coefficient SemiRingReal, Expr t (SemiRingBase SemiRingReal),
      Coefficient SemiRingReal)
forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr
-> Maybe (Coefficient sr, f (SemiRingBase sr), Coefficient sr)
WSum.asAffineVar (WeightedSum (Expr t) SemiRingReal
 -> Maybe
      (Coefficient SemiRingReal, Expr t (SemiRingBase SemiRingReal),
       Coefficient SemiRingReal))
-> WeightedSum (Expr t) SemiRingReal
-> Maybe
     (Coefficient SemiRingReal, Expr t (SemiRingBase SemiRingReal),
      Coefficient SemiRingReal)
forall a b. (a -> b) -> a -> b
$
          SemiRingRepr SemiRingReal
-> Expr t (SemiRingBase SemiRingReal)
-> WeightedSum (Expr t) SemiRingReal
forall t (sr :: SemiRing).
HashableF (Expr t) =>
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
asWeightedSum SemiRingRepr SemiRingReal
SR.SemiRingRealRepr Expr t tp
Expr t (SemiRingBase SemiRingReal)
e ->
        (ConcreteVal BaseRealType, Expr t tp, ConcreteVal BaseRealType)
-> Maybe
     (ConcreteVal BaseRealType, Expr t tp, ConcreteVal BaseRealType)
forall a. a -> Maybe a
Just (Rational -> ConcreteVal BaseRealType
ConcreteReal Rational
Coefficient SemiRingReal
a, Expr t tp
Expr t (SemiRingBase SemiRingReal)
x, Rational -> ConcreteVal BaseRealType
ConcreteReal Rational
Coefficient SemiRingReal
b)
    BaseBVRepr NatRepr w
w
      | Just (Coefficient (SemiRingBV BVArith w)
a, Expr t (SemiRingBase (SemiRingBV BVArith w))
x, Coefficient (SemiRingBV BVArith w)
b) <- WeightedSum (Expr t) (SemiRingBV BVArith w)
-> Maybe
     (Coefficient (SemiRingBV BVArith w),
      Expr t (SemiRingBase (SemiRingBV BVArith w)),
      Coefficient (SemiRingBV BVArith w))
forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr
-> Maybe (Coefficient sr, f (SemiRingBase sr), Coefficient sr)
WSum.asAffineVar (WeightedSum (Expr t) (SemiRingBV BVArith w)
 -> Maybe
      (Coefficient (SemiRingBV BVArith w),
       Expr t (SemiRingBase (SemiRingBV BVArith w)),
       Coefficient (SemiRingBV BVArith w)))
-> WeightedSum (Expr t) (SemiRingBV BVArith w)
-> Maybe
     (Coefficient (SemiRingBV BVArith w),
      Expr t (SemiRingBase (SemiRingBV BVArith w)),
      Coefficient (SemiRingBV BVArith w))
forall a b. (a -> b) -> a -> b
$
          SemiRingRepr (SemiRingBV BVArith w)
-> Expr t (SemiRingBase (SemiRingBV BVArith w))
-> WeightedSum (Expr t) (SemiRingBV BVArith w)
forall t (sr :: SemiRing).
HashableF (Expr t) =>
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
asWeightedSum (BVFlavorRepr BVArith
-> NatRepr w -> SemiRingRepr (SemiRingBV BVArith w)
forall (w :: Nat) (fv :: BVFlavor).
(1 <= w) =>
BVFlavorRepr fv -> NatRepr w -> SemiRingRepr (SemiRingBV fv w)
SR.SemiRingBVRepr BVFlavorRepr BVArith
SR.BVArithRepr (Expr t (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth Expr t tp
Expr t (BaseBVType w)
e)) Expr t tp
Expr t (SemiRingBase (SemiRingBV BVArith w))
e ->
        (ConcreteVal (BaseBVType w), Expr t tp, ConcreteVal (BaseBVType w))
-> Maybe
     (ConcreteVal (BaseBVType w), Expr t tp, ConcreteVal (BaseBVType w))
forall a. a -> Maybe a
Just (NatRepr w -> BV w -> ConcreteVal (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BV w -> ConcreteVal (BaseBVType w)
ConcreteBV NatRepr w
w BV w
Coefficient (SemiRingBV BVArith w)
a, Expr t tp
Expr t (SemiRingBase (SemiRingBV BVArith w))
x, NatRepr w -> BV w -> ConcreteVal (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BV w -> ConcreteVal (BaseBVType w)
ConcreteBV NatRepr w
w BV w
Coefficient (SemiRingBV BVArith w)
b)
    BaseTypeRepr tp
_ -> Maybe (ConcreteVal tp, Expr t tp, ConcreteVal tp)
forall a. Maybe a
Nothing

  asString :: Expr t (BaseStringType si) -> Maybe (StringLiteral si)
asString (StringExpr StringLiteral si
x ProgramLoc
_) = StringLiteral si -> Maybe (StringLiteral si)
forall a. a -> Maybe a
Just StringLiteral si
x
  asString Expr t (BaseStringType si)
_ = Maybe (StringLiteral si)
forall a. Maybe a
Nothing

  asConstantArray :: Expr t (BaseArrayType idx bt) -> Maybe (Expr t bt)
asConstantArray (Expr t (BaseArrayType idx bt)
-> Maybe (App (Expr t) (BaseArrayType idx bt))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (ConstantArray Assignment BaseTypeRepr (i ::> tp)
_ BaseTypeRepr b
_ Expr t b
def)) = Expr t b -> Maybe (Expr t b)
forall a. a -> Maybe a
Just Expr t b
def
  asConstantArray Expr t (BaseArrayType idx bt)
_ = Maybe (Expr t bt)
forall a. Maybe a
Nothing

  asStruct :: Expr t (BaseStructType flds) -> Maybe (Assignment (Expr t) flds)
asStruct (Expr t (BaseStructType flds)
-> Maybe (App (Expr t) (BaseStructType flds))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (StructCtor Assignment BaseTypeRepr flds
_ Assignment (Expr t) flds
flds)) = Assignment (Expr t) flds -> Maybe (Assignment (Expr t) flds)
forall a. a -> Maybe a
Just Assignment (Expr t) flds
flds
  asStruct Expr t (BaseStructType flds)
_ = Maybe (Assignment (Expr t) flds)
forall a. Maybe a
Nothing

  printSymExpr :: Expr t tp -> Doc ann
printSymExpr = Expr t tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty


asSemiRingLit :: SR.SemiRingRepr sr -> Expr t (SR.SemiRingBase sr) -> Maybe (SR.Coefficient sr)
asSemiRingLit :: SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (Coefficient sr)
asSemiRingLit SemiRingRepr sr
sr (SemiRingLiteral SemiRingRepr sr
sr' Coefficient sr
x ProgramLoc
_loc)
  | Just sr :~: sr
Refl <- SemiRingRepr sr -> SemiRingRepr sr -> Maybe (sr :~: sr)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SemiRingRepr sr
sr SemiRingRepr sr
sr'
  = Coefficient sr -> Maybe (Coefficient sr)
forall a. a -> Maybe a
Just Coefficient sr
Coefficient sr
x

  -- special case, ignore the BV ring flavor for this purpose
  | SR.SemiRingBVRepr BVFlavorRepr fv
_ NatRepr w
w  <- SemiRingRepr sr
sr
  , SR.SemiRingBVRepr BVFlavorRepr fv
_ NatRepr w
w' <- SemiRingRepr sr
sr'
  , Just w :~: w
Refl <- NatRepr w -> NatRepr w -> Maybe (w :~: w)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w NatRepr w
w'
  = BV w -> Maybe (BV w)
forall a. a -> Maybe a
Just BV w
Coefficient sr
x

asSemiRingLit SemiRingRepr sr
_ Expr t (SemiRingBase sr)
_ = Maybe (Coefficient sr)
forall a. Maybe a
Nothing

asSemiRingSum :: SR.SemiRingRepr sr -> Expr t (SR.SemiRingBase sr) -> Maybe (WeightedSum (Expr t) sr)
asSemiRingSum :: SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (WeightedSum (Expr t) sr)
asSemiRingSum SemiRingRepr sr
sr (SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (Coefficient sr)
forall (sr :: SemiRing) t.
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (Coefficient sr)
asSemiRingLit SemiRingRepr sr
sr -> Just Coefficient sr
x) = WeightedSum (Expr t) sr -> Maybe (WeightedSum (Expr t) sr)
forall a. a -> Maybe a
Just (SemiRingRepr sr -> Coefficient sr -> WeightedSum (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingRepr sr -> Coefficient sr -> WeightedSum f sr
WSum.constant SemiRingRepr sr
sr Coefficient sr
x)
asSemiRingSum SemiRingRepr sr
sr (Expr t (SemiRingBase sr) -> Maybe (App (Expr t) (SemiRingBase sr))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (SemiRingSum WeightedSum (Expr t) sr
x))
   | Just sr :~: sr
Refl <- SemiRingRepr sr -> SemiRingRepr sr -> Maybe (sr :~: sr)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SemiRingRepr sr
sr (WeightedSum (Expr t) sr -> SemiRingRepr sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr -> SemiRingRepr sr
WSum.sumRepr WeightedSum (Expr t) sr
x) = WeightedSum (Expr t) sr -> Maybe (WeightedSum (Expr t) sr)
forall a. a -> Maybe a
Just WeightedSum (Expr t) sr
x
asSemiRingSum SemiRingRepr sr
_ Expr t (SemiRingBase sr)
_ = Maybe (WeightedSum (Expr t) sr)
forall a. Maybe a
Nothing

asSemiRingProd :: SR.SemiRingRepr sr -> Expr t (SR.SemiRingBase sr) -> Maybe (SemiRingProduct (Expr t) sr)
asSemiRingProd :: SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (SemiRingProduct (Expr t) sr)
asSemiRingProd SemiRingRepr sr
sr (Expr t (SemiRingBase sr) -> Maybe (App (Expr t) (SemiRingBase sr))
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (SemiRingProd SemiRingProduct (Expr t) sr
x))
  | Just sr :~: sr
Refl <- SemiRingRepr sr -> SemiRingRepr sr -> Maybe (sr :~: sr)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SemiRingRepr sr
sr (SemiRingProduct (Expr t) sr -> SemiRingRepr sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
SemiRingProduct f sr -> SemiRingRepr sr
WSum.prodRepr SemiRingProduct (Expr t) sr
x) = SemiRingProduct (Expr t) sr -> Maybe (SemiRingProduct (Expr t) sr)
forall a. a -> Maybe a
Just SemiRingProduct (Expr t) sr
x
asSemiRingProd SemiRingRepr sr
_ Expr t (SemiRingBase sr)
_ = Maybe (SemiRingProduct (Expr t) sr)
forall a. Maybe a
Nothing

-- | This privides a view of a semiring expr as a weighted sum of values.
data SemiRingView t sr
   = SR_Constant !(SR.Coefficient sr)
   | SR_Sum  !(WeightedSum (Expr t) sr)
   | SR_Prod !(SemiRingProduct (Expr t) sr)
   | SR_General

viewSemiRing:: SR.SemiRingRepr sr -> Expr t (SR.SemiRingBase sr) -> SemiRingView t sr
viewSemiRing :: SemiRingRepr sr -> Expr t (SemiRingBase sr) -> SemiRingView t sr
viewSemiRing SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x
  | Just Coefficient sr
r <- SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (Coefficient sr)
forall (sr :: SemiRing) t.
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (Coefficient sr)
asSemiRingLit SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x  = Coefficient sr -> SemiRingView t sr
forall t (sr :: SemiRing). Coefficient sr -> SemiRingView t sr
SR_Constant Coefficient sr
r
  | Just WeightedSum (Expr t) sr
s <- SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (WeightedSum (Expr t) sr)
forall (sr :: SemiRing) t.
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (WeightedSum (Expr t) sr)
asSemiRingSum SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x  = WeightedSum (Expr t) sr -> SemiRingView t sr
forall t (sr :: SemiRing).
WeightedSum (Expr t) sr -> SemiRingView t sr
SR_Sum WeightedSum (Expr t) sr
s
  | Just SemiRingProduct (Expr t) sr
p <- SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (SemiRingProduct (Expr t) sr)
forall (sr :: SemiRing) t.
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (SemiRingProduct (Expr t) sr)
asSemiRingProd SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x = SemiRingProduct (Expr t) sr -> SemiRingView t sr
forall t (sr :: SemiRing).
SemiRingProduct (Expr t) sr -> SemiRingView t sr
SR_Prod SemiRingProduct (Expr t) sr
p
  | Bool
otherwise = SemiRingView t sr
forall t (sr :: SemiRing). SemiRingView t sr
SR_General

asWeightedSum :: HashableF (Expr t) => SR.SemiRingRepr sr -> Expr t (SR.SemiRingBase sr) -> WeightedSum (Expr t) sr
asWeightedSum :: SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
asWeightedSum SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x
  | Just Coefficient sr
r <- SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (Coefficient sr)
forall (sr :: SemiRing) t.
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (Coefficient sr)
asSemiRingLit SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x = SemiRingRepr sr -> Coefficient sr -> WeightedSum (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingRepr sr -> Coefficient sr -> WeightedSum f sr
WSum.constant SemiRingRepr sr
sr Coefficient sr
r
  | Just WeightedSum (Expr t) sr
s <- SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (WeightedSum (Expr t) sr)
forall (sr :: SemiRing) t.
SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> Maybe (WeightedSum (Expr t) sr)
asSemiRingSum SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x = WeightedSum (Expr t) sr
s
  | Bool
otherwise = SemiRingRepr sr
-> Expr t (SemiRingBase sr) -> WeightedSum (Expr t) sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
Tm f =>
SemiRingRepr sr -> f (SemiRingBase sr) -> WeightedSum f sr
WSum.var SemiRingRepr sr
sr Expr t (SemiRingBase sr)
x

asConjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)]
asConjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)]
asConjunction (BoolExpr Bool
True ProgramLoc
_) = []
asConjunction (Expr t BaseBoolType -> Maybe (App (Expr t) BaseBoolType)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (ConjPred BoolMap (Expr t)
xs)) =
 case BoolMap (Expr t) -> BoolMapView (Expr t)
forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f
BM.viewBoolMap BoolMap (Expr t)
xs of
   BoolMapView (Expr t)
BoolMapUnit     -> []
   BoolMapView (Expr t)
BoolMapDualUnit -> [(Bool -> ProgramLoc -> Expr t BaseBoolType
forall t. Bool -> ProgramLoc -> Expr t BaseBoolType
BoolExpr Bool
False ProgramLoc
initializationLoc, Polarity
Positive)]
   BoolMapTerms ((Expr t BaseBoolType, Polarity)
tm:|[(Expr t BaseBoolType, Polarity)]
tms) -> (Expr t BaseBoolType, Polarity)
tm(Expr t BaseBoolType, Polarity)
-> [(Expr t BaseBoolType, Polarity)]
-> [(Expr t BaseBoolType, Polarity)]
forall a. a -> [a] -> [a]
:[(Expr t BaseBoolType, Polarity)]
tms
asConjunction Expr t BaseBoolType
x = [(Expr t BaseBoolType
x,Polarity
Positive)]


asDisjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)]
asDisjunction :: Expr t BaseBoolType -> [(Expr t BaseBoolType, Polarity)]
asDisjunction (BoolExpr Bool
False ProgramLoc
_) = []
asDisjunction (Expr t BaseBoolType -> Maybe (App (Expr t) BaseBoolType)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (NotPred (Expr t BaseBoolType -> Maybe (App (Expr t) BaseBoolType)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (ConjPred BoolMap (Expr t)
xs)))) =
 case BoolMap (Expr t) -> BoolMapView (Expr t)
forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f
BM.viewBoolMap BoolMap (Expr t)
xs of
   BoolMapView (Expr t)
BoolMapUnit     -> []
   BoolMapView (Expr t)
BoolMapDualUnit -> [(Bool -> ProgramLoc -> Expr t BaseBoolType
forall t. Bool -> ProgramLoc -> Expr t BaseBoolType
BoolExpr Bool
True ProgramLoc
initializationLoc, Polarity
Positive)]
   BoolMapTerms ((Expr t BaseBoolType, Polarity)
tm:|[(Expr t BaseBoolType, Polarity)]
tms) -> ((Expr t BaseBoolType, Polarity)
 -> (Expr t BaseBoolType, Polarity))
-> [(Expr t BaseBoolType, Polarity)]
-> [(Expr t BaseBoolType, Polarity)]
forall a b. (a -> b) -> [a] -> [b]
map (ASetter
  (Expr t BaseBoolType, Polarity)
  (Expr t BaseBoolType, Polarity)
  Polarity
  Polarity
-> (Polarity -> Polarity)
-> (Expr t BaseBoolType, Polarity)
-> (Expr t BaseBoolType, Polarity)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (Expr t BaseBoolType, Polarity)
  (Expr t BaseBoolType, Polarity)
  Polarity
  Polarity
forall s t a b. Field2 s t a b => Lens s t a b
_2 Polarity -> Polarity
BM.negatePolarity) ((Expr t BaseBoolType, Polarity)
tm(Expr t BaseBoolType, Polarity)
-> [(Expr t BaseBoolType, Polarity)]
-> [(Expr t BaseBoolType, Polarity)]
forall a. a -> [a] -> [a]
:[(Expr t BaseBoolType, Polarity)]
tms)
asDisjunction Expr t BaseBoolType
x = [(Expr t BaseBoolType
x,Polarity
Positive)]

asPosAtom :: Expr t BaseBoolType -> (Expr t BaseBoolType, Polarity)
asPosAtom :: Expr t BaseBoolType -> (Expr t BaseBoolType, Polarity)
asPosAtom (Expr t BaseBoolType -> Maybe (App (Expr t) BaseBoolType)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (NotPred Expr t BaseBoolType
x)) = (Expr t BaseBoolType
x, Polarity
Negative)
asPosAtom Expr t BaseBoolType
x                           = (Expr t BaseBoolType
x, Polarity
Positive)

asNegAtom :: Expr t BaseBoolType -> (Expr t BaseBoolType, Polarity)
asNegAtom :: Expr t BaseBoolType -> (Expr t BaseBoolType, Polarity)
asNegAtom (Expr t BaseBoolType -> Maybe (App (Expr t) BaseBoolType)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (NotPred Expr t BaseBoolType
x)) = (Expr t BaseBoolType
x, Polarity
Positive)
asNegAtom Expr t BaseBoolType
x                           = (Expr t BaseBoolType
x, Polarity
Negative)


-- | Get abstract value associated with element.
exprAbsValue :: Expr t tp -> AbstractValue tp
exprAbsValue :: Expr t tp -> AbstractValue tp
exprAbsValue (SemiRingLiteral SemiRingRepr sr
sr Coefficient sr
x ProgramLoc
_) =
  case SemiRingRepr sr
sr of
    SemiRingRepr sr
SR.SemiRingIntegerRepr  -> Integer -> ValueRange Integer
forall tp. tp -> ValueRange tp
singleRange Integer
Coefficient sr
x
    SemiRingRepr sr
SR.SemiRingRealRepr -> Rational -> RealAbstractValue
ravSingle Rational
Coefficient sr
x
    SR.SemiRingBVRepr BVFlavorRepr fv
_ NatRepr w
w -> NatRepr w -> Integer -> BVDomain w
forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> BVDomain w
BVD.singleton NatRepr w
w (BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
Coefficient sr
x)

exprAbsValue (StringExpr StringLiteral si
l ProgramLoc
_) = StringLiteral si -> StringAbstractValue
forall (si :: StringInfo). StringLiteral si -> StringAbstractValue
stringAbsSingle StringLiteral si
l
exprAbsValue (FloatExpr FloatPrecisionRepr fpp
_ BigFloat
_ ProgramLoc
_) = ()
exprAbsValue (BoolExpr Bool
b ProgramLoc
_)   = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b
exprAbsValue (NonceAppExpr NonceAppExpr t tp
e) = NonceAppExpr t tp -> AbstractValue tp
forall t (tp :: BaseType). NonceAppExpr t tp -> AbstractValue tp
nonceExprAbsValue NonceAppExpr t tp
e
exprAbsValue (AppExpr AppExpr t tp
e)      = AppExpr t tp -> AbstractValue tp
forall t (tp :: BaseType). AppExpr t tp -> AbstractValue tp
appExprAbsValue AppExpr t tp
e
exprAbsValue (BoundVarExpr ExprBoundVar t tp
v) =
  AbstractValue tp -> Maybe (AbstractValue tp) -> AbstractValue tp
forall a. a -> Maybe a -> a
fromMaybe (BaseTypeRepr tp -> AbstractValue tp
forall (tp :: BaseType). BaseTypeRepr tp -> AbstractValue tp
unconstrainedAbsValue (ExprBoundVar t tp -> BaseTypeRepr tp
forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
bvarType ExprBoundVar t tp
v)) (ExprBoundVar t tp -> Maybe (AbstractValue tp)
forall t (tp :: BaseType).
ExprBoundVar t tp -> Maybe (AbstractValue tp)
bvarAbstractValue ExprBoundVar t tp
v)

instance HasAbsValue (Expr t) where
  getAbsValue :: Expr t tp -> AbstractValue tp
getAbsValue = Expr t tp -> AbstractValue tp
forall t (tp :: BaseType). Expr t tp -> AbstractValue tp
exprAbsValue


------------------------------------------------------------------------
-- Expr operations

{-# INLINE compareExpr #-}
compareExpr :: Expr t x -> Expr t y -> OrderingF x y

-- Special case, ignore the BV semiring flavor for this purpose
compareExpr :: Expr t x -> Expr t y -> OrderingF x y
compareExpr (SemiRingLiteral (SR.SemiRingBVRepr BVFlavorRepr fv
_ NatRepr w
wx) Coefficient sr
x ProgramLoc
_) (SemiRingLiteral (SR.SemiRingBVRepr BVFlavorRepr fv
_ NatRepr w
wy) Coefficient sr
y ProgramLoc
_) =
  case NatRepr w -> NatRepr w -> OrderingF w w
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF NatRepr w
wx NatRepr w
wy of
    OrderingF w w
LTF -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
LTF
    OrderingF w w
EQF -> Ordering -> OrderingF x x
forall k (x :: k). Ordering -> OrderingF x x
fromOrdering (BV w -> BV w -> Ordering
forall a. Ord a => a -> a -> Ordering
compare BV w
Coefficient sr
x BV w
Coefficient sr
y)
    OrderingF w w
GTF -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
GTF
compareExpr (SemiRingLiteral SemiRingRepr sr
srx Coefficient sr
x ProgramLoc
_) (SemiRingLiteral SemiRingRepr sr
sry Coefficient sr
y ProgramLoc
_) =
  case SemiRingRepr sr -> SemiRingRepr sr -> OrderingF sr sr
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF SemiRingRepr sr
srx SemiRingRepr sr
sry of
    OrderingF sr sr
LTF -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
LTF
    OrderingF sr sr
EQF -> Ordering -> OrderingF x x
forall k (x :: k). Ordering -> OrderingF x x
fromOrdering (SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Ordering
forall (sr :: SemiRing).
SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Ordering
SR.sr_compare SemiRingRepr sr
srx Coefficient sr
x Coefficient sr
Coefficient sr
y)
    OrderingF sr sr
GTF -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
GTF
compareExpr SemiRingLiteral{} Expr t y
_ = OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
LTF
compareExpr Expr t x
_ SemiRingLiteral{} = OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
GTF

compareExpr (StringExpr StringLiteral si
x ProgramLoc
_) (StringExpr StringLiteral si
y ProgramLoc
_) =
  case StringLiteral si -> StringLiteral si -> OrderingF si si
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF StringLiteral si
x StringLiteral si
y of
    OrderingF si si
LTF -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
LTF
    OrderingF si si
EQF -> OrderingF x y
forall k (x :: k). OrderingF x x
EQF
    OrderingF si si
GTF -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
GTF

compareExpr StringExpr{} Expr t y
_ = OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
LTF
compareExpr Expr t x
_ StringExpr{} = OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
GTF

compareExpr (BoolExpr Bool
x ProgramLoc
_) (BoolExpr Bool
y ProgramLoc
_) = Ordering -> OrderingF x x
forall k (x :: k). Ordering -> OrderingF x x
fromOrdering (Bool -> Bool -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Bool
x Bool
y)
compareExpr BoolExpr{} Expr t y
_ = OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
LTF
compareExpr Expr t x
_ BoolExpr{} = OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
GTF

compareExpr (FloatExpr FloatPrecisionRepr fpp
rx BigFloat
x ProgramLoc
_) (FloatExpr FloatPrecisionRepr fpp
ry BigFloat
y ProgramLoc
_) =
   case FloatPrecisionRepr fpp
-> FloatPrecisionRepr fpp -> OrderingF fpp fpp
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF FloatPrecisionRepr fpp
rx FloatPrecisionRepr fpp
ry of
     OrderingF fpp fpp
LTF -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
LTF
     OrderingF fpp fpp
EQF -> Ordering -> OrderingF x x
forall k (x :: k). Ordering -> OrderingF x x
fromOrdering (BigFloat -> BigFloat -> Ordering
BF.bfCompare BigFloat
x BigFloat
y) -- NB, don't use `compare`, which is IEEE754 comaprison
     OrderingF fpp fpp
GTF -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
GTF

compareExpr FloatExpr{} Expr t y
_ = OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
LTF
compareExpr Expr t x
_ FloatExpr{} = OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
GTF

compareExpr (NonceAppExpr NonceAppExpr t x
x) (NonceAppExpr NonceAppExpr t y
y) = NonceAppExpr t x -> NonceAppExpr t y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF NonceAppExpr t x
x NonceAppExpr t y
y
compareExpr NonceAppExpr{} Expr t y
_ = OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
LTF
compareExpr Expr t x
_ NonceAppExpr{} = OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
GTF

compareExpr (AppExpr AppExpr t x
x) (AppExpr AppExpr t y
y) = Nonce t x -> Nonce t y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF (AppExpr t x -> Nonce t x
forall t (tp :: BaseType). AppExpr t tp -> Nonce t tp
appExprId AppExpr t x
x) (AppExpr t y -> Nonce t y
forall t (tp :: BaseType). AppExpr t tp -> Nonce t tp
appExprId AppExpr t y
y)
compareExpr AppExpr{} Expr t y
_ = OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
LTF
compareExpr Expr t x
_ AppExpr{} = OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
GTF

compareExpr (BoundVarExpr ExprBoundVar t x
x) (BoundVarExpr ExprBoundVar t y
y) = ExprBoundVar t x -> ExprBoundVar t y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF ExprBoundVar t x
x ExprBoundVar t y
y

-- | A slightly more aggressive syntactic equality check than testEquality,
--   `sameTerm` will recurse through a small collection of known syntax formers.
sameTerm :: Expr t a -> Expr t b -> Maybe (a :~: b)

sameTerm :: Expr t a -> Expr t b -> Maybe (a :~: b)
sameTerm (Expr t a -> Maybe (App (Expr t) a)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (FloatToBinary FloatPrecisionRepr (FloatingPointPrecision eb sb)
fppx Expr t (BaseFloatType (FloatingPointPrecision eb sb))
x)) (Expr t b -> Maybe (App (Expr t) b)
forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (FloatToBinary FloatPrecisionRepr (FloatingPointPrecision eb sb)
fppy Expr t (BaseFloatType (FloatingPointPrecision eb sb))
y)) =
  do FloatingPointPrecision eb sb :~: FloatingPointPrecision eb sb
Refl <- FloatPrecisionRepr (FloatingPointPrecision eb sb)
-> FloatPrecisionRepr (FloatingPointPrecision eb sb)
-> Maybe
     (FloatingPointPrecision eb sb :~: FloatingPointPrecision eb sb)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality FloatPrecisionRepr (FloatingPointPrecision eb sb)
fppx FloatPrecisionRepr (FloatingPointPrecision eb sb)
fppy
     BaseFloatType (FloatingPointPrecision eb sb)
:~: BaseFloatType (FloatingPointPrecision eb sb)
Refl <- Expr t (BaseFloatType (FloatingPointPrecision eb sb))
-> Expr t (BaseFloatType (FloatingPointPrecision eb sb))
-> Maybe
     (BaseFloatType (FloatingPointPrecision eb sb)
      :~: BaseFloatType (FloatingPointPrecision eb sb))
forall t (a :: BaseType) (b :: BaseType).
Expr t a -> Expr t b -> Maybe (a :~: b)
sameTerm Expr t (BaseFloatType (FloatingPointPrecision eb sb))
x Expr t (BaseFloatType (FloatingPointPrecision eb sb))
y
     (a :~: a) -> Maybe (a :~: a)
forall (m :: Type -> Type) a. Monad m => a -> m a
return a :~: a
forall k (a :: k). a :~: a
Refl

sameTerm Expr t a
x Expr t b
y = Expr t a -> Expr t b -> Maybe (a :~: b)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Expr t a
x Expr t b
y


instance TestEquality (NonceAppExpr t) where
  testEquality :: NonceAppExpr t a -> NonceAppExpr t b -> Maybe (a :~: b)
testEquality NonceAppExpr t a
x NonceAppExpr t b
y =
    case NonceAppExpr t a -> NonceAppExpr t b -> OrderingF a b
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF NonceAppExpr t a
x NonceAppExpr t b
y of
      OrderingF a b
EQF -> (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
      OrderingF a b
_ -> Maybe (a :~: b)
forall a. Maybe a
Nothing

instance OrdF (NonceAppExpr t)  where
  compareF :: NonceAppExpr t x -> NonceAppExpr t y -> OrderingF x y
compareF NonceAppExpr t x
x NonceAppExpr t y
y = Nonce t x -> Nonce t y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF (NonceAppExpr t x -> Nonce t x
forall t (tp :: BaseType). NonceAppExpr t tp -> Nonce t tp
nonceExprId NonceAppExpr t x
x) (NonceAppExpr t y -> Nonce t y
forall t (tp :: BaseType). NonceAppExpr t tp -> Nonce t tp
nonceExprId NonceAppExpr t y
y)

instance Eq (NonceAppExpr t tp) where
  NonceAppExpr t tp
x == :: NonceAppExpr t tp -> NonceAppExpr t tp -> Bool
== NonceAppExpr t tp
y = Maybe (tp :~: tp) -> Bool
forall a. Maybe a -> Bool
isJust (NonceAppExpr t tp -> NonceAppExpr t tp -> Maybe (tp :~: tp)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NonceAppExpr t tp
x NonceAppExpr t tp
y)

instance Ord (NonceAppExpr t tp) where
  compare :: NonceAppExpr t tp -> NonceAppExpr t tp -> Ordering
compare NonceAppExpr t tp
x NonceAppExpr t tp
y = OrderingF tp tp -> Ordering
forall k (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (NonceAppExpr t tp -> NonceAppExpr t tp -> OrderingF tp tp
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF NonceAppExpr t tp
x NonceAppExpr t tp
y)

instance TestEquality (Expr t) where
  testEquality :: Expr t a -> Expr t b -> Maybe (a :~: b)
testEquality Expr t a
x Expr t b
y =
    case Expr t a -> Expr t b -> OrderingF a b
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF Expr t a
x Expr t b
y of
      OrderingF a b
EQF -> (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
      OrderingF a b
_ -> Maybe (a :~: b)
forall a. Maybe a
Nothing

instance OrdF (Expr t)  where
  compareF :: Expr t x -> Expr t y -> OrderingF x y
compareF = Expr t x -> Expr t y -> OrderingF x y
forall t (x :: BaseType) (y :: BaseType).
Expr t x -> Expr t y -> OrderingF x y
compareExpr

instance Eq (Expr t tp) where
  Expr t tp
x == :: Expr t tp -> Expr t tp -> Bool
== Expr t tp
y = Maybe (tp :~: tp) -> Bool
forall a. Maybe a -> Bool
isJust (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)
testEquality Expr t tp
x Expr t tp
y)

instance Ord (Expr t tp) where
  compare :: Expr t tp -> Expr t tp -> Ordering
compare Expr t tp
x Expr t tp
y = OrderingF tp tp -> Ordering
forall k (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (Expr t tp -> Expr t tp -> OrderingF tp tp
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF Expr t tp
x Expr t tp
y)

instance Hashable (Expr t tp) where
  hashWithSalt :: Int -> Expr t tp -> Int
hashWithSalt Int
s (BoolExpr Bool
b ProgramLoc
_) = Int -> Bool -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt (Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int
0::Int)) Bool
b
  hashWithSalt Int
s (SemiRingLiteral SemiRingRepr sr
sr Coefficient sr
x ProgramLoc
_) =
    case SemiRingRepr sr
sr of
      SemiRingRepr sr
SR.SemiRingIntegerRepr -> Int -> Integer -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt (Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int
2::Int)) Integer
Coefficient sr
x
      SemiRingRepr sr
SR.SemiRingRealRepr    -> Int -> Rational -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt (Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int
3::Int)) Rational
Coefficient sr
x
      SR.SemiRingBVRepr BVFlavorRepr fv
_ NatRepr w
w  -> Int -> BV w -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt (Int -> NatRepr w -> Int
forall k (f :: k -> Type) (tp :: k).
HashableF f =>
Int -> f tp -> Int
hashWithSaltF (Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int
4::Int)) NatRepr w
w) BV w
Coefficient sr
x

  hashWithSalt Int
s (FloatExpr FloatPrecisionRepr fpp
fr BigFloat
x ProgramLoc
_) = Int -> BigFloat -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt (Int -> FloatPrecisionRepr fpp -> Int
forall k (f :: k -> Type) (tp :: k).
HashableF f =>
Int -> f tp -> Int
hashWithSaltF (Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int
5::Int)) FloatPrecisionRepr fpp
fr) BigFloat
x
  hashWithSalt Int
s (StringExpr StringLiteral si
x ProgramLoc
_) = Int -> StringLiteral si -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt (Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int
6::Int)) StringLiteral si
x
  hashWithSalt Int
s (AppExpr AppExpr t tp
x)      = Int -> Nonce t tp -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt (Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int
7::Int)) (AppExpr t tp -> Nonce t tp
forall t (tp :: BaseType). AppExpr t tp -> Nonce t tp
appExprId AppExpr t tp
x)
  hashWithSalt Int
s (NonceAppExpr NonceAppExpr t tp
x) = Int -> Nonce t tp -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt (Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int
8::Int)) (NonceAppExpr t tp -> Nonce t tp
forall t (tp :: BaseType). NonceAppExpr t tp -> Nonce t tp
nonceExprId NonceAppExpr t tp
x)
  hashWithSalt Int
s (BoundVarExpr ExprBoundVar t tp
x) = Int -> ExprBoundVar t tp -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt (Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int
9::Int)) ExprBoundVar t tp
x

instance PH.HashableF (Expr t) where
  hashWithSaltF :: Int -> Expr t tp -> Int
hashWithSaltF = Int -> Expr t tp -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt


------------------------------------------------------------------------
-- PPIndex

data PPIndex
   = ExprPPIndex {-# UNPACK #-} !Word64
   | RatPPIndex !Rational
  deriving (PPIndex -> PPIndex -> Bool
(PPIndex -> PPIndex -> Bool)
-> (PPIndex -> PPIndex -> Bool) -> Eq PPIndex
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PPIndex -> PPIndex -> Bool
$c/= :: PPIndex -> PPIndex -> Bool
== :: PPIndex -> PPIndex -> Bool
$c== :: PPIndex -> PPIndex -> Bool
Eq, Eq PPIndex
Eq PPIndex
-> (PPIndex -> PPIndex -> Ordering)
-> (PPIndex -> PPIndex -> Bool)
-> (PPIndex -> PPIndex -> Bool)
-> (PPIndex -> PPIndex -> Bool)
-> (PPIndex -> PPIndex -> Bool)
-> (PPIndex -> PPIndex -> PPIndex)
-> (PPIndex -> PPIndex -> PPIndex)
-> Ord PPIndex
PPIndex -> PPIndex -> Bool
PPIndex -> PPIndex -> Ordering
PPIndex -> PPIndex -> PPIndex
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: PPIndex -> PPIndex -> PPIndex
$cmin :: PPIndex -> PPIndex -> PPIndex
max :: PPIndex -> PPIndex -> PPIndex
$cmax :: PPIndex -> PPIndex -> PPIndex
>= :: PPIndex -> PPIndex -> Bool
$c>= :: PPIndex -> PPIndex -> Bool
> :: PPIndex -> PPIndex -> Bool
$c> :: PPIndex -> PPIndex -> Bool
<= :: PPIndex -> PPIndex -> Bool
$c<= :: PPIndex -> PPIndex -> Bool
< :: PPIndex -> PPIndex -> Bool
$c< :: PPIndex -> PPIndex -> Bool
compare :: PPIndex -> PPIndex -> Ordering
$ccompare :: PPIndex -> PPIndex -> Ordering
$cp1Ord :: Eq PPIndex
Ord, (forall x. PPIndex -> Rep PPIndex x)
-> (forall x. Rep PPIndex x -> PPIndex) -> Generic PPIndex
forall x. Rep PPIndex x -> PPIndex
forall x. PPIndex -> Rep PPIndex x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PPIndex x -> PPIndex
$cfrom :: forall x. PPIndex -> Rep PPIndex x
Generic)

instance Hashable PPIndex

------------------------------------------------------------------------
-- countOccurrences

countOccurrences :: Expr t tp -> Map.Map PPIndex Int
countOccurrences :: Expr t tp -> Map PPIndex Int
countOccurrences Expr t tp
e0 = (forall s. ST s (Map PPIndex Int)) -> Map PPIndex Int
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (Map PPIndex Int)) -> Map PPIndex Int)
-> (forall s. ST s (Map PPIndex Int)) -> Map PPIndex Int
forall a b. (a -> b) -> a -> b
$ do
  HashTable s PPIndex Int
visited <- ST s (HashTable s PPIndex Int)
forall s k v. ST s (HashTable s k v)
H.new
  HashTable s PPIndex Int -> Expr t tp -> ST s ()
forall t (tp :: BaseType) s.
OccurrenceTable s -> Expr t tp -> ST s ()
countOccurrences' HashTable s PPIndex Int
visited Expr t tp
e0
  [(PPIndex, Int)] -> Map PPIndex Int
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(PPIndex, Int)] -> Map PPIndex Int)
-> ST s [(PPIndex, Int)] -> ST s (Map PPIndex Int)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> HashTable s PPIndex Int -> ST s [(PPIndex, Int)]
forall (h :: Type -> Type -> Type -> Type) s k v.
HashTable h =>
h s k v -> ST s [(k, v)]
H.toList HashTable s PPIndex Int
visited

type OccurrenceTable s = H.HashTable s PPIndex Int


incOccurrence :: OccurrenceTable s -> PPIndex -> ST s () -> ST s ()
incOccurrence :: OccurrenceTable s -> PPIndex -> ST s () -> ST s ()
incOccurrence OccurrenceTable s
visited PPIndex
idx ST s ()
sub = do
  Maybe Int
mv <- OccurrenceTable s -> PPIndex -> ST s (Maybe Int)
forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> ST s (Maybe v)
H.lookup OccurrenceTable s
visited PPIndex
idx
  case Maybe Int
mv of
    Just Int
i -> OccurrenceTable s -> PPIndex -> Int -> ST s ()
forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> v -> ST s ()
H.insert OccurrenceTable s
visited PPIndex
idx (Int -> ST s ()) -> Int -> ST s ()
forall a b. (a -> b) -> a -> b
$! Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1
    Maybe Int
Nothing -> ST s ()
sub ST s () -> ST s () -> ST s ()
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> OccurrenceTable s -> PPIndex -> Int -> ST s ()
forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> v -> ST s ()
H.insert OccurrenceTable s
visited PPIndex
idx Int
1

-- FIXME... why does this ignore Nat and Int literals?
countOccurrences' :: forall t tp s . OccurrenceTable s -> Expr t tp -> ST s ()
countOccurrences' :: OccurrenceTable s -> Expr t tp -> ST s ()
countOccurrences' OccurrenceTable s
visited (SemiRingLiteral SemiRingRepr sr
SR.SemiRingRealRepr Coefficient sr
r ProgramLoc
_) = do
  OccurrenceTable s -> PPIndex -> ST s () -> ST s ()
forall s. OccurrenceTable s -> PPIndex -> ST s () -> ST s ()
incOccurrence OccurrenceTable s
visited (Rational -> PPIndex
RatPPIndex Rational
Coefficient sr
r) (ST s () -> ST s ()) -> ST s () -> ST s ()
forall a b. (a -> b) -> a -> b
$
    () -> ST s ()
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
countOccurrences' OccurrenceTable s
visited (AppExpr AppExpr t tp
e) = do
  let idx :: PPIndex
idx = Word64 -> PPIndex
ExprPPIndex (Nonce t tp -> Word64
forall s k (tp :: k). Nonce s tp -> Word64
indexValue (AppExpr t tp -> Nonce t tp
forall t (tp :: BaseType). AppExpr t tp -> Nonce t tp
appExprId AppExpr t tp
e))
  OccurrenceTable s -> PPIndex -> ST s () -> ST s ()
forall s. OccurrenceTable s -> PPIndex -> ST s () -> ST s ()
incOccurrence OccurrenceTable s
visited PPIndex
idx (ST s () -> ST s ()) -> ST s () -> ST s ()
forall a b. (a -> b) -> a -> b
$ do
    (forall (x :: BaseType). Expr t x -> ST s ())
-> App (Expr t) tp -> ST s ()
forall k l (t :: (k -> Type) -> l -> Type) (m :: Type -> Type)
       (f :: k -> Type) a.
(FoldableFC t, Applicative m) =>
(forall (x :: k). f x -> m a) -> forall (x :: l). t f x -> m ()
traverseFC_ (OccurrenceTable s -> Expr t x -> ST s ()
forall t (tp :: BaseType) s.
OccurrenceTable s -> Expr t tp -> ST s ()
countOccurrences' OccurrenceTable s
visited) (AppExpr t tp -> App (Expr t) tp
forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
appExprApp AppExpr t tp
e)
countOccurrences' OccurrenceTable s
visited (NonceAppExpr NonceAppExpr t tp
e) = do
  let idx :: PPIndex
idx = Word64 -> PPIndex
ExprPPIndex (Nonce t tp -> Word64
forall s k (tp :: k). Nonce s tp -> Word64
indexValue (NonceAppExpr t tp -> Nonce t tp
forall t (tp :: BaseType). NonceAppExpr t tp -> Nonce t tp
nonceExprId NonceAppExpr t tp
e))
  OccurrenceTable s -> PPIndex -> ST s () -> ST s ()
forall s. OccurrenceTable s -> PPIndex -> ST s () -> ST s ()
incOccurrence OccurrenceTable s
visited PPIndex
idx (ST s () -> ST s ()) -> ST s () -> ST s ()
forall a b. (a -> b) -> a -> b
$ do
    (forall (x :: BaseType). Expr t x -> ST s ())
-> NonceApp t (Expr t) tp -> ST s ()
forall k l (t :: (k -> Type) -> l -> Type) (m :: Type -> Type)
       (f :: k -> Type) a.
(FoldableFC t, Applicative m) =>
(forall (x :: k). f x -> m a) -> forall (x :: l). t f x -> m ()
traverseFC_ (OccurrenceTable s -> Expr t x -> ST s ()
forall t (tp :: BaseType) s.
OccurrenceTable s -> Expr t tp -> ST s ()
countOccurrences' OccurrenceTable s
visited) (NonceAppExpr t tp -> NonceApp t (Expr t) tp
forall t (tp :: BaseType).
NonceAppExpr t tp -> NonceApp t (Expr t) tp
nonceExprApp NonceAppExpr t tp
e)
countOccurrences' OccurrenceTable s
_ Expr t tp
_ = () -> ST s ()
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()

------------------------------------------------------------------------
-- boundVars

type BoundVarMap s t = H.HashTable s PPIndex (Set (Some (ExprBoundVar t)))

cache :: (Eq k, Hashable k) => H.HashTable s k r -> k -> ST s r -> ST s r
cache :: HashTable s k r -> k -> ST s r -> ST s r
cache HashTable s k r
h k
k ST s r
m = do
  Maybe r
mr <- HashTable s k r -> k -> ST s (Maybe r)
forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> ST s (Maybe v)
H.lookup HashTable s k r
h k
k
  case Maybe r
mr of
    Just r
r -> r -> ST s r
forall (m :: Type -> Type) a. Monad m => a -> m a
return r
r
    Maybe r
Nothing -> do
      r
r <- ST s r
m
      HashTable s k r -> k -> r -> ST s ()
forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> v -> ST s ()
H.insert HashTable s k r
h k
k r
r
      r -> ST s r
forall (m :: Type -> Type) a. Monad m => a -> m a
return r
r


boundVars :: Expr t tp -> ST s (BoundVarMap s t)
boundVars :: Expr t tp -> ST s (BoundVarMap s t)
boundVars Expr t tp
e0 = do
  BoundVarMap s t
visited <- ST s (BoundVarMap s t)
forall s k v. ST s (HashTable s k v)
H.new
  Set (Some (ExprBoundVar t))
_ <- BoundVarMap s t -> Expr t tp -> ST s (Set (Some (ExprBoundVar t)))
forall s t (tp :: BaseType).
BoundVarMap s t -> Expr t tp -> ST s (Set (Some (ExprBoundVar t)))
boundVars' BoundVarMap s t
visited Expr t tp
e0
  BoundVarMap s t -> ST s (BoundVarMap s t)
forall (m :: Type -> Type) a. Monad m => a -> m a
return BoundVarMap s t
visited

boundVars' :: BoundVarMap s t
           -> Expr t tp
           -> ST s (Set (Some (ExprBoundVar t)))
boundVars' :: BoundVarMap s t -> Expr t tp -> ST s (Set (Some (ExprBoundVar t)))
boundVars' BoundVarMap s t
visited (AppExpr AppExpr t tp
e) = do
  let idx :: Word64
idx = Nonce t tp -> Word64
forall s k (tp :: k). Nonce s tp -> Word64
indexValue (AppExpr t tp -> Nonce t tp
forall t (tp :: BaseType). AppExpr t tp -> Nonce t tp
appExprId AppExpr t tp
e)
  BoundVarMap s t
-> PPIndex
-> ST s (Set (Some (ExprBoundVar t)))
-> ST s (Set (Some (ExprBoundVar t)))
forall k s r.
(Eq k, Hashable k) =>
HashTable s k r -> k -> ST s r -> ST s r
cache BoundVarMap s t
visited (Word64 -> PPIndex
ExprPPIndex Word64
idx) (ST s (Set (Some (ExprBoundVar t)))
 -> ST s (Set (Some (ExprBoundVar t))))
-> ST s (Set (Some (ExprBoundVar t)))
-> ST s (Set (Some (ExprBoundVar t)))
forall a b. (a -> b) -> a -> b
$ do
    [Set (Some (ExprBoundVar t))]
sums <- [ST s (Set (Some (ExprBoundVar t)))]
-> ST s [Set (Some (ExprBoundVar t))]
forall (t :: Type -> Type) (m :: Type -> Type) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ((forall (x :: BaseType).
 Expr t x -> ST s (Set (Some (ExprBoundVar t))))
-> App (Expr t) tp -> [ST s (Set (Some (ExprBoundVar t)))]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
toListFC (BoundVarMap s t -> Expr t x -> ST s (Set (Some (ExprBoundVar t)))
forall s t (tp :: BaseType).
BoundVarMap s t -> Expr t tp -> ST s (Set (Some (ExprBoundVar t)))
boundVars' BoundVarMap s t
visited) (AppExpr t tp -> App (Expr t) tp
forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
appExprApp AppExpr t tp
e))
    Set (Some (ExprBoundVar t)) -> ST s (Set (Some (ExprBoundVar t)))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Set (Some (ExprBoundVar t)) -> ST s (Set (Some (ExprBoundVar t))))
-> Set (Some (ExprBoundVar t))
-> ST s (Set (Some (ExprBoundVar t)))
forall a b. (a -> b) -> a -> b
$ (Set (Some (ExprBoundVar t))
 -> Set (Some (ExprBoundVar t)) -> Set (Some (ExprBoundVar t)))
-> Set (Some (ExprBoundVar t))
-> [Set (Some (ExprBoundVar t))]
-> Set (Some (ExprBoundVar t))
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Set (Some (ExprBoundVar t))
-> Set (Some (ExprBoundVar t)) -> Set (Some (ExprBoundVar t))
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (Some (ExprBoundVar t))
forall a. Set a
Set.empty [Set (Some (ExprBoundVar t))]
sums
boundVars' BoundVarMap s t
visited (NonceAppExpr NonceAppExpr t tp
e) = do
  let idx :: Word64
idx = Nonce t tp -> Word64
forall s k (tp :: k). Nonce s tp -> Word64
indexValue (NonceAppExpr t tp -> Nonce t tp
forall t (tp :: BaseType). NonceAppExpr t tp -> Nonce t tp
nonceExprId NonceAppExpr t tp
e)
  BoundVarMap s t
-> PPIndex
-> ST s (Set (Some (ExprBoundVar t)))
-> ST s (Set (Some (ExprBoundVar t)))
forall k s r.
(Eq k, Hashable k) =>
HashTable s k r -> k -> ST s r -> ST s r
cache BoundVarMap s t
visited (Word64 -> PPIndex
ExprPPIndex Word64
idx) (ST s (Set (Some (ExprBoundVar t)))
 -> ST s (Set (Some (ExprBoundVar t))))
-> ST s (Set (Some (ExprBoundVar t)))
-> ST s (Set (Some (ExprBoundVar t)))
forall a b. (a -> b) -> a -> b
$ do
    [Set (Some (ExprBoundVar t))]
sums <- [ST s (Set (Some (ExprBoundVar t)))]
-> ST s [Set (Some (ExprBoundVar t))]
forall (t :: Type -> Type) (m :: Type -> Type) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ((forall (x :: BaseType).
 Expr t x -> ST s (Set (Some (ExprBoundVar t))))
-> NonceApp t (Expr t) tp -> [ST s (Set (Some (ExprBoundVar t)))]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
toListFC (BoundVarMap s t -> Expr t x -> ST s (Set (Some (ExprBoundVar t)))
forall s t (tp :: BaseType).
BoundVarMap s t -> Expr t tp -> ST s (Set (Some (ExprBoundVar t)))
boundVars' BoundVarMap s t
visited) (NonceAppExpr t tp -> NonceApp t (Expr t) tp
forall t (tp :: BaseType).
NonceAppExpr t tp -> NonceApp t (Expr t) tp
nonceExprApp NonceAppExpr t tp
e))
    Set (Some (ExprBoundVar t)) -> ST s (Set (Some (ExprBoundVar t)))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Set (Some (ExprBoundVar t)) -> ST s (Set (Some (ExprBoundVar t))))
-> Set (Some (ExprBoundVar t))
-> ST s (Set (Some (ExprBoundVar t)))
forall a b. (a -> b) -> a -> b
$ (Set (Some (ExprBoundVar t))
 -> Set (Some (ExprBoundVar t)) -> Set (Some (ExprBoundVar t)))
-> Set (Some (ExprBoundVar t))
-> [Set (Some (ExprBoundVar t))]
-> Set (Some (ExprBoundVar t))
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Set (Some (ExprBoundVar t))
-> Set (Some (ExprBoundVar t)) -> Set (Some (ExprBoundVar t))
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (Some (ExprBoundVar t))
forall a. Set a
Set.empty [Set (Some (ExprBoundVar t))]
sums
boundVars' BoundVarMap s t
visited (BoundVarExpr ExprBoundVar t tp
v)
  | VarKind
QuantifierVarKind <- ExprBoundVar t tp -> VarKind
forall t (tp :: BaseType). ExprBoundVar t tp -> VarKind
bvarKind ExprBoundVar t tp
v = do
      let idx :: Word64
idx = Nonce t tp -> Word64
forall s k (tp :: k). Nonce s tp -> Word64
indexValue (ExprBoundVar t tp -> Nonce t tp
forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId ExprBoundVar t tp
v)
      BoundVarMap s t
-> PPIndex
-> ST s (Set (Some (ExprBoundVar t)))
-> ST s (Set (Some (ExprBoundVar t)))
forall k s r.
(Eq k, Hashable k) =>
HashTable s k r -> k -> ST s r -> ST s r
cache BoundVarMap s t
visited (Word64 -> PPIndex
ExprPPIndex Word64
idx) (ST s (Set (Some (ExprBoundVar t)))
 -> ST s (Set (Some (ExprBoundVar t))))
-> ST s (Set (Some (ExprBoundVar t)))
-> ST s (Set (Some (ExprBoundVar t)))
forall a b. (a -> b) -> a -> b
$
        Set (Some (ExprBoundVar t)) -> ST s (Set (Some (ExprBoundVar t)))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some (ExprBoundVar t) -> Set (Some (ExprBoundVar t))
forall a. a -> Set a
Set.singleton (ExprBoundVar t tp -> Some (ExprBoundVar t)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some ExprBoundVar t tp
v))
boundVars' BoundVarMap s t
_ Expr t tp
_ = Set (Some (ExprBoundVar t)) -> ST s (Set (Some (ExprBoundVar t)))
forall (m :: Type -> Type) a. Monad m => a -> m a
return Set (Some (ExprBoundVar t))
forall a. Set a
Set.empty


------------------------------------------------------------------------
-- Pretty printing

instance Show (Expr t tp) where
  show :: Expr t tp -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (Expr t tp -> Doc Any) -> Expr t tp -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr t tp -> Doc Any
forall t (tp :: BaseType) ann. Expr t tp -> Doc ann
ppExpr

instance Pretty (Expr t tp) where
  pretty :: Expr t tp -> Doc ann
pretty = Expr t tp -> Doc ann
forall t (tp :: BaseType) ann. Expr t tp -> Doc ann
ppExpr



-- | @AppPPExpr@ represents a an application, and it may be let bound.
data AppPPExpr ann
   = APE { AppPPExpr ann -> PPIndex
apeIndex :: !PPIndex
         , AppPPExpr ann -> ProgramLoc
apeLoc :: !ProgramLoc
         , AppPPExpr ann -> Text
apeName :: !Text
         , AppPPExpr ann -> [PPExpr ann]
apeExprs :: ![PPExpr ann]
         , AppPPExpr ann -> Int
apeLength :: !Int
           -- ^ Length of AppPPExpr not including parenthesis.
         }

data PPExpr ann
   = FixedPPExpr !(Doc ann) ![Doc ann] !Int
     -- ^ A fixed doc with length.
   | AppPPExpr !(AppPPExpr ann)
     -- ^ A doc that can be let bound.

-- | Pretty print a AppPPExpr
apeDoc :: AppPPExpr ann -> (Doc ann, [Doc ann])
apeDoc :: AppPPExpr ann -> (Doc ann, [Doc ann])
apeDoc AppPPExpr ann
a = (Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (AppPPExpr ann -> Text
forall ann. AppPPExpr ann -> Text
apeName AppPPExpr ann
a), Bool -> PPExpr ann -> Doc ann
forall ann. Bool -> PPExpr ann -> Doc ann
ppExprDoc Bool
True (PPExpr ann -> Doc ann) -> [PPExpr ann] -> [Doc ann]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AppPPExpr ann -> [PPExpr ann]
forall ann. AppPPExpr ann -> [PPExpr ann]
apeExprs AppPPExpr ann
a)

textPPExpr :: Text -> PPExpr ann
textPPExpr :: Text -> PPExpr ann
textPPExpr Text
t = Doc ann -> [Doc ann] -> Int -> PPExpr ann
forall ann. Doc ann -> [Doc ann] -> Int -> PPExpr ann
FixedPPExpr (Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
t) [] (Text -> Int
Text.length Text
t)

stringPPExpr :: String -> PPExpr ann
stringPPExpr :: String -> PPExpr ann
stringPPExpr String
t = Doc ann -> [Doc ann] -> Int -> PPExpr ann
forall ann. Doc ann -> [Doc ann] -> Int -> PPExpr ann
FixedPPExpr (String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
t) [] (String -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length String
t)

-- | Get length of Expr including parens.
ppExprLength :: PPExpr ann -> Int
ppExprLength :: PPExpr ann -> Int
ppExprLength (FixedPPExpr Doc ann
_ [] Int
n) = Int
n
ppExprLength (FixedPPExpr Doc ann
_ [Doc ann]
_ Int
n) = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2
ppExprLength (AppPPExpr AppPPExpr ann
a) = AppPPExpr ann -> Int
forall ann. AppPPExpr ann -> Int
apeLength AppPPExpr ann
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2

parenIf :: Bool -> Doc ann -> [Doc ann] -> Doc ann
parenIf :: Bool -> Doc ann -> [Doc ann] -> Doc ann
parenIf Bool
_ Doc ann
h [] = Doc ann
h
parenIf Bool
False Doc ann
h [Doc ann]
l = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep (Doc ann
hDoc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
:[Doc ann]
l)
parenIf Bool
True Doc ann
h [Doc ann]
l = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep (Doc ann
hDoc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
:[Doc ann]
l))

-- | Pretty print PPExpr
ppExprDoc :: Bool -> PPExpr ann -> Doc ann
ppExprDoc :: Bool -> PPExpr ann -> Doc ann
ppExprDoc Bool
b (FixedPPExpr Doc ann
d [Doc ann]
a Int
_) = Bool -> Doc ann -> [Doc ann] -> Doc ann
forall ann. Bool -> Doc ann -> [Doc ann] -> Doc ann
parenIf Bool
b Doc ann
d [Doc ann]
a
ppExprDoc Bool
b (AppPPExpr AppPPExpr ann
a) = (Doc ann -> [Doc ann] -> Doc ann)
-> (Doc ann, [Doc ann]) -> Doc ann
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Bool -> Doc ann -> [Doc ann] -> Doc ann
forall ann. Bool -> Doc ann -> [Doc ann] -> Doc ann
parenIf Bool
b) (AppPPExpr ann -> (Doc ann, [Doc ann])
forall ann. AppPPExpr ann -> (Doc ann, [Doc ann])
apeDoc AppPPExpr ann
a)

data PPExprOpts = PPExprOpts { PPExprOpts -> Int
ppExpr_maxWidth :: Int
                           , PPExprOpts -> Bool
ppExpr_useDecimal :: Bool
                           }

defaultPPExprOpts :: PPExprOpts
defaultPPExprOpts :: PPExprOpts
defaultPPExprOpts =
  PPExprOpts :: Int -> Bool -> PPExprOpts
PPExprOpts { ppExpr_maxWidth :: Int
ppExpr_maxWidth = Int
68
            , ppExpr_useDecimal :: Bool
ppExpr_useDecimal = Bool
True
            }

-- | Pretty print an 'Expr' using let bindings to create the term.
ppExpr :: Expr t tp -> Doc ann
ppExpr :: Expr t tp -> Doc ann
ppExpr Expr t tp
e
     | [Doc ann] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
Prelude.null [Doc ann]
bindings = Bool -> PPExpr ann -> Doc ann
forall ann. Bool -> PPExpr ann -> Doc ann
ppExprDoc Bool
False PPExpr ann
r
     | Bool
otherwise =
       [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep
       [ Doc ann
"let" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [Doc ann]
bindings)
       , Doc ann
" in" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (Bool -> PPExpr ann -> Doc ann
forall ann. Bool -> PPExpr ann -> Doc ann
ppExprDoc Bool
False PPExpr ann
r) ]
  where ([Doc ann]
bindings,PPExpr ann
r) = (forall s. ST s ([Doc ann], PPExpr ann)) -> ([Doc ann], PPExpr ann)
forall a. (forall s. ST s a) -> a
runST (Expr t tp -> PPExprOpts -> ST s ([Doc ann], PPExpr ann)
forall t (tp :: BaseType) s ann.
Expr t tp -> PPExprOpts -> ST s ([Doc ann], PPExpr ann)
ppExpr' Expr t tp
e PPExprOpts
defaultPPExprOpts)

instance ShowF (Expr t)

-- | Pretty print the top part of an element.
ppExprTop :: Expr t tp -> Doc ann
ppExprTop :: Expr t tp -> Doc ann
ppExprTop Expr t tp
e = Bool -> PPExpr ann -> Doc ann
forall ann. Bool -> PPExpr ann -> Doc ann
ppExprDoc Bool
False PPExpr ann
r
  where ([Doc ann]
_,PPExpr ann
r) = (forall s. ST s ([Doc ann], PPExpr ann)) -> ([Doc ann], PPExpr ann)
forall a. (forall s. ST s a) -> a
runST (Expr t tp -> PPExprOpts -> ST s ([Doc ann], PPExpr ann)
forall t (tp :: BaseType) s ann.
Expr t tp -> PPExprOpts -> ST s ([Doc ann], PPExpr ann)
ppExpr' Expr t tp
e PPExprOpts
defaultPPExprOpts)

-- | Contains the elements before, the index, doc, and width and
-- the elements after.
type SplitPPExprList ann = Maybe ([PPExpr ann], AppPPExpr ann, [PPExpr ann])

findExprToRemove :: [PPExpr ann] -> SplitPPExprList ann
findExprToRemove :: [PPExpr ann] -> SplitPPExprList ann
findExprToRemove [PPExpr ann]
exprs0 = [PPExpr ann]
-> [PPExpr ann] -> SplitPPExprList ann -> SplitPPExprList ann
forall ann.
[PPExpr ann]
-> [PPExpr ann] -> SplitPPExprList ann -> SplitPPExprList ann
go [] [PPExpr ann]
exprs0 SplitPPExprList ann
forall a. Maybe a
Nothing
  where go :: [PPExpr ann] -> [PPExpr ann] -> SplitPPExprList ann -> SplitPPExprList ann
        go :: [PPExpr ann]
-> [PPExpr ann] -> SplitPPExprList ann -> SplitPPExprList ann
go [PPExpr ann]
_ [] SplitPPExprList ann
mr = SplitPPExprList ann
mr
        go [PPExpr ann]
prev (e :: PPExpr ann
e@FixedPPExpr{} : [PPExpr ann]
exprs) SplitPPExprList ann
mr = do
          [PPExpr ann]
-> [PPExpr ann] -> SplitPPExprList ann -> SplitPPExprList ann
forall ann.
[PPExpr ann]
-> [PPExpr ann] -> SplitPPExprList ann -> SplitPPExprList ann
go (PPExpr ann
ePPExpr ann -> [PPExpr ann] -> [PPExpr ann]
forall a. a -> [a] -> [a]
:[PPExpr ann]
prev) [PPExpr ann]
exprs SplitPPExprList ann
mr
        go [PPExpr ann]
prev (AppPPExpr AppPPExpr ann
a:[PPExpr ann]
exprs) mr :: SplitPPExprList ann
mr@(Just ([PPExpr ann]
_,AppPPExpr ann
a',[PPExpr ann]
_))
          | AppPPExpr ann -> Int
forall ann. AppPPExpr ann -> Int
apeLength AppPPExpr ann
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< AppPPExpr ann -> Int
forall ann. AppPPExpr ann -> Int
apeLength AppPPExpr ann
a' = [PPExpr ann]
-> [PPExpr ann] -> SplitPPExprList ann -> SplitPPExprList ann
forall ann.
[PPExpr ann]
-> [PPExpr ann] -> SplitPPExprList ann -> SplitPPExprList ann
go (AppPPExpr ann -> PPExpr ann
forall ann. AppPPExpr ann -> PPExpr ann
AppPPExpr AppPPExpr ann
aPPExpr ann -> [PPExpr ann] -> [PPExpr ann]
forall a. a -> [a] -> [a]
:[PPExpr ann]
prev) [PPExpr ann]
exprs SplitPPExprList ann
mr
        go [PPExpr ann]
prev (AppPPExpr AppPPExpr ann
a:[PPExpr ann]
exprs) SplitPPExprList ann
_ = do
          [PPExpr ann]
-> [PPExpr ann] -> SplitPPExprList ann -> SplitPPExprList ann
forall ann.
[PPExpr ann]
-> [PPExpr ann] -> SplitPPExprList ann -> SplitPPExprList ann
go (AppPPExpr ann -> PPExpr ann
forall ann. AppPPExpr ann -> PPExpr ann
AppPPExpr AppPPExpr ann
aPPExpr ann -> [PPExpr ann] -> [PPExpr ann]
forall a. a -> [a] -> [a]
:[PPExpr ann]
prev) [PPExpr ann]
exprs (([PPExpr ann], AppPPExpr ann, [PPExpr ann]) -> SplitPPExprList ann
forall a. a -> Maybe a
Just ([PPExpr ann] -> [PPExpr ann]
forall a. [a] -> [a]
reverse [PPExpr ann]
prev, AppPPExpr ann
a, [PPExpr ann]
exprs))


ppExpr' :: forall t tp s ann. Expr t tp -> PPExprOpts -> ST s ([Doc ann], PPExpr ann)
ppExpr' :: Expr t tp -> PPExprOpts -> ST s ([Doc ann], PPExpr ann)
ppExpr' Expr t tp
e0 PPExprOpts
o = do
  let max_width :: Int
max_width = PPExprOpts -> Int
ppExpr_maxWidth PPExprOpts
o
  let use_decimal :: Bool
use_decimal = PPExprOpts -> Bool
ppExpr_useDecimal PPExprOpts
o
  -- Get map that counts number of elements.
  let m :: Map PPIndex Int
m = Expr t tp -> Map PPIndex Int
forall t (tp :: BaseType). Expr t tp -> Map PPIndex Int
countOccurrences Expr t tp
e0
  -- Return number of times a term is referred to in dag.
  let isShared :: PPIndex -> Bool
      isShared :: PPIndex -> Bool
isShared PPIndex
w = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 (PPIndex -> Map PPIndex Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PPIndex
w Map PPIndex Int
m) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1

  -- Get bounds variables.
  BoundVarMap s t
bvars <- Expr t tp -> ST s (BoundVarMap s t)
forall t (tp :: BaseType) s. Expr t tp -> ST s (BoundVarMap s t)
boundVars Expr t tp
e0

  STRef s (Seq (Doc ann))
bindingsRef <- Seq (Doc ann) -> ST s (STRef s (Seq (Doc ann)))
forall a s. a -> ST s (STRef s a)
newSTRef Seq (Doc ann)
forall a. Seq a
Seq.empty

  HashTable s PPIndex (PPExpr ann)
visited <- ST s (HashTable s PPIndex (PPExpr ann))
forall s k v. ST s (HashTable s k v)
H.new :: ST s (H.HashTable s PPIndex (PPExpr ann))
  HashTable s Word64 Text
visited_fns <- ST s (HashTable s Word64 Text)
forall s k v. ST s (HashTable s k v)
H.new :: ST s (H.HashTable s Word64 Text)

  let -- Add a binding to the list of bindings
      addBinding :: AppPPExpr ann -> ST s (PPExpr ann)
      addBinding :: AppPPExpr ann -> ST s (PPExpr ann)
addBinding AppPPExpr ann
a = do
        let idx :: PPIndex
idx = AppPPExpr ann -> PPIndex
forall ann. AppPPExpr ann -> PPIndex
apeIndex AppPPExpr ann
a
        Int
cnt <- Seq (Doc ann) -> Int
forall a. Seq a -> Int
Seq.length (Seq (Doc ann) -> Int) -> ST s (Seq (Doc ann)) -> ST s Int
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> STRef s (Seq (Doc ann)) -> ST s (Seq (Doc ann))
forall s a. STRef s a -> ST s a
readSTRef STRef s (Seq (Doc ann))
bindingsRef

        Set (Some (ExprBoundVar t))
vars <- Set (Some (ExprBoundVar t))
-> Maybe (Set (Some (ExprBoundVar t)))
-> Set (Some (ExprBoundVar t))
forall a. a -> Maybe a -> a
fromMaybe Set (Some (ExprBoundVar t))
forall a. Set a
Set.empty (Maybe (Set (Some (ExprBoundVar t)))
 -> Set (Some (ExprBoundVar t)))
-> ST s (Maybe (Set (Some (ExprBoundVar t))))
-> ST s (Set (Some (ExprBoundVar t)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> BoundVarMap s t
-> PPIndex -> ST s (Maybe (Set (Some (ExprBoundVar t))))
forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> ST s (Maybe v)
H.lookup BoundVarMap s t
bvars PPIndex
idx
        -- TODO: avoid intermediate String from 'ppBoundVar'
        let args :: [String]
            args :: [String]
args = (forall (tp :: BaseType). ExprBoundVar t tp -> String)
-> Some (ExprBoundVar t) -> String
forall k (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome forall t (tp :: BaseType). ExprBoundVar t tp -> String
forall (tp :: BaseType). ExprBoundVar t tp -> String
ppBoundVar (Some (ExprBoundVar t) -> String)
-> [Some (ExprBoundVar t)] -> [String]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (Some (ExprBoundVar t)) -> [Some (ExprBoundVar t)]
forall a. Set a -> [a]
Set.toList Set (Some (ExprBoundVar t))
vars

        let nm :: String
nm = case PPIndex
idx of
                   ExprPPIndex Word64
e -> String
"v" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall a. Show a => a -> String
show Word64
e
                   RatPPIndex Rational
_ -> String
"r" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
cnt
        let lhs :: Doc ann
lhs = Bool -> Doc ann -> [Doc ann] -> Doc ann
forall ann. Bool -> Doc ann -> [Doc ann] -> Doc ann
parenIf Bool
False (String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
nm) (String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann) -> [String] -> [Doc ann]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
args)
        let doc :: Doc ann
doc = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
                  [ Doc ann
"--" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Position -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (ProgramLoc -> Position
plSourceLoc (AppPPExpr ann -> ProgramLoc
forall ann. AppPPExpr ann -> ProgramLoc
apeLoc AppPPExpr ann
a))
                  , Doc ann
lhs Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> (Doc ann -> [Doc ann] -> Doc ann)
-> (Doc ann, [Doc ann]) -> Doc ann
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Bool -> Doc ann -> [Doc ann] -> Doc ann
forall ann. Bool -> Doc ann -> [Doc ann] -> Doc ann
parenIf Bool
False) (AppPPExpr ann -> (Doc ann, [Doc ann])
forall ann. AppPPExpr ann -> (Doc ann, [Doc ann])
apeDoc AppPPExpr ann
a) ]
        STRef s (Seq (Doc ann))
-> (Seq (Doc ann) -> Seq (Doc ann)) -> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef' STRef s (Seq (Doc ann))
bindingsRef (Seq (Doc ann) -> Doc ann -> Seq (Doc ann)
forall a. Seq a -> a -> Seq a
Seq.|> Doc ann
doc)
        let len :: Int
len = String -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length String
nm Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall (t :: Type -> Type) a. (Foldable t, Num a) => t a -> a
sum ((\String
arg_s -> String -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length String
arg_s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (String -> Int) -> [String] -> [Int]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
args)
        let nm_expr :: PPExpr ann
nm_expr = Doc ann -> [Doc ann] -> Int -> PPExpr ann
forall ann. Doc ann -> [Doc ann] -> Int -> PPExpr ann
FixedPPExpr (String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
nm) ((String -> Doc ann) -> [String] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [String]
args) Int
len
        HashTable s PPIndex (PPExpr ann)
-> PPIndex -> PPExpr ann -> ST s ()
forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> v -> ST s ()
H.insert HashTable s PPIndex (PPExpr ann)
visited PPIndex
idx (PPExpr ann -> ST s ()) -> PPExpr ann -> ST s ()
forall a b. (a -> b) -> a -> b
$! PPExpr ann
nm_expr
        PPExpr ann -> ST s (PPExpr ann)
forall (m :: Type -> Type) a. Monad m => a -> m a
return PPExpr ann
nm_expr

  let fixLength :: Int
                -> [PPExpr ann]
                -> ST s ([PPExpr ann], Int)
      fixLength :: Int -> [PPExpr ann] -> ST s ([PPExpr ann], Int)
fixLength Int
cur_width [PPExpr ann]
exprs
        | Int
cur_width Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
max_width
        , Just ([PPExpr ann]
prev_e, AppPPExpr ann
a, [PPExpr ann]
next_e) <- [PPExpr ann] -> Maybe ([PPExpr ann], AppPPExpr ann, [PPExpr ann])
forall ann. [PPExpr ann] -> SplitPPExprList ann
findExprToRemove [PPExpr ann]
exprs = do
          PPExpr ann
r <- AppPPExpr ann -> ST s (PPExpr ann)
addBinding AppPPExpr ann
a
          let exprs' :: [PPExpr ann]
exprs' = [PPExpr ann]
prev_e [PPExpr ann] -> [PPExpr ann] -> [PPExpr ann]
forall a. [a] -> [a] -> [a]
++ [PPExpr ann
r] [PPExpr ann] -> [PPExpr ann] -> [PPExpr ann]
forall a. [a] -> [a] -> [a]
++ [PPExpr ann]
next_e
          Int -> [PPExpr ann] -> ST s ([PPExpr ann], Int)
fixLength (Int
cur_width Int -> Int -> Int
forall a. Num a => a -> a -> a
- AppPPExpr ann -> Int
forall ann. AppPPExpr ann -> Int
apeLength AppPPExpr ann
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ PPExpr ann -> Int
forall ann. PPExpr ann -> Int
ppExprLength PPExpr ann
r) [PPExpr ann]
exprs'
      fixLength Int
cur_width [PPExpr ann]
exprs = do
        ([PPExpr ann], Int) -> ST s ([PPExpr ann], Int)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (([PPExpr ann], Int) -> ST s ([PPExpr ann], Int))
-> ([PPExpr ann], Int) -> ST s ([PPExpr ann], Int)
forall a b. (a -> b) -> a -> b
$! ([PPExpr ann]
exprs, Int
cur_width)

  -- Pretty print an argument.
  let renderArg :: PrettyArg (Expr t) -> ST s (PPExpr ann)
      renderArg :: PrettyArg (Expr t) -> ST s (PPExpr ann)
renderArg (PrettyArg Expr t tp
e) = Expr t tp -> ST s (PPExpr ann)
forall (u :: BaseType). Expr t u -> ST s (PPExpr ann)
getBindings Expr t tp
e
      renderArg (PrettyText Text
txt) = PPExpr ann -> ST s (PPExpr ann)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Text -> PPExpr ann
forall ann. Text -> PPExpr ann
textPPExpr Text
txt)
      renderArg (PrettyFunc Text
nm [PrettyArg (Expr t)]
args) =
        do [PPExpr ann]
exprs0 <- (PrettyArg (Expr t) -> ST s (PPExpr ann))
-> [PrettyArg (Expr t)] -> ST s [PPExpr ann]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse PrettyArg (Expr t) -> ST s (PPExpr ann)
renderArg [PrettyArg (Expr t)]
args
           let total_width :: Int
total_width = Text -> Int
Text.length Text
nm Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall (t :: Type -> Type) a. (Foldable t, Num a) => t a -> a
sum ((\PPExpr ann
e -> Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ PPExpr ann -> Int
forall ann. PPExpr ann -> Int
ppExprLength PPExpr ann
e) (PPExpr ann -> Int) -> [PPExpr ann] -> [Int]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [PPExpr ann]
exprs0)
           ([PPExpr ann]
exprs1, Int
cur_width) <- Int -> [PPExpr ann] -> ST s ([PPExpr ann], Int)
fixLength Int
total_width [PPExpr ann]
exprs0
           let exprs :: [Doc ann]
exprs = (PPExpr ann -> Doc ann) -> [PPExpr ann] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> PPExpr ann -> Doc ann
forall ann. Bool -> PPExpr ann -> Doc ann
ppExprDoc Bool
True) [PPExpr ann]
exprs1
           PPExpr ann -> ST s (PPExpr ann)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Doc ann -> [Doc ann] -> Int -> PPExpr ann
forall ann. Doc ann -> [Doc ann] -> Int -> PPExpr ann
FixedPPExpr (Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
nm) [Doc ann]
exprs Int
cur_width)

      renderApp :: PPIndex
                -> ProgramLoc
                -> Text
                -> [PrettyArg (Expr t)]
                -> ST s (AppPPExpr ann)
      renderApp :: PPIndex
-> ProgramLoc
-> Text
-> [PrettyArg (Expr t)]
-> ST s (AppPPExpr ann)
renderApp PPIndex
idx ProgramLoc
loc Text
nm [PrettyArg (Expr t)]
args = Bool -> ST s (AppPPExpr ann) -> ST s (AppPPExpr ann)
forall a. HasCallStack => Bool -> a -> a
Ex.assert (Bool -> Bool
not ([PrettyArg (Expr t)] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
Prelude.null [PrettyArg (Expr t)]
args)) (ST s (AppPPExpr ann) -> ST s (AppPPExpr ann))
-> ST s (AppPPExpr ann) -> ST s (AppPPExpr ann)
forall a b. (a -> b) -> a -> b
$ do
        [PPExpr ann]
exprs0 <- (PrettyArg (Expr t) -> ST s (PPExpr ann))
-> [PrettyArg (Expr t)] -> ST s [PPExpr ann]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse PrettyArg (Expr t) -> ST s (PPExpr ann)
renderArg [PrettyArg (Expr t)]
args
        -- Get width not including parenthesis of outer app.
        let total_width :: Int
total_width = Text -> Int
Text.length Text
nm Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall (t :: Type -> Type) a. (Foldable t, Num a) => t a -> a
sum ((\PPExpr ann
e -> Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ PPExpr ann -> Int
forall ann. PPExpr ann -> Int
ppExprLength PPExpr ann
e) (PPExpr ann -> Int) -> [PPExpr ann] -> [Int]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [PPExpr ann]
exprs0)
        ([PPExpr ann]
exprs, Int
cur_width) <- Int -> [PPExpr ann] -> ST s ([PPExpr ann], Int)
fixLength Int
total_width [PPExpr ann]
exprs0
        AppPPExpr ann -> ST s (AppPPExpr ann)
forall (m :: Type -> Type) a. Monad m => a -> m a
return APE :: forall ann.
PPIndex
-> ProgramLoc -> Text -> [PPExpr ann] -> Int -> AppPPExpr ann
APE { apeIndex :: PPIndex
apeIndex = PPIndex
idx
                   , apeLoc :: ProgramLoc
apeLoc = ProgramLoc
loc
                   , apeName :: Text
apeName = Text
nm
                   , apeExprs :: [PPExpr ann]
apeExprs = [PPExpr ann]
exprs
                   , apeLength :: Int
apeLength = Int
cur_width
                   }

      cacheResult :: PPIndex
                  -> ProgramLoc
                  -> PrettyApp (Expr t)
                  -> ST s (PPExpr ann)
      cacheResult :: PPIndex -> ProgramLoc -> PrettyApp (Expr t) -> ST s (PPExpr ann)
cacheResult PPIndex
_ ProgramLoc
_ (Text
nm,[]) = do
        PPExpr ann -> ST s (PPExpr ann)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Text -> PPExpr ann
forall ann. Text -> PPExpr ann
textPPExpr Text
nm)
      cacheResult PPIndex
idx ProgramLoc
loc (Text
nm,[PrettyArg (Expr t)]
args) = do
        Maybe (PPExpr ann)
mr <- HashTable s PPIndex (PPExpr ann)
-> PPIndex -> ST s (Maybe (PPExpr ann))
forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> ST s (Maybe v)
H.lookup HashTable s PPIndex (PPExpr ann)
visited PPIndex
idx
        case Maybe (PPExpr ann)
mr of
          Just PPExpr ann
d -> PPExpr ann -> ST s (PPExpr ann)
forall (m :: Type -> Type) a. Monad m => a -> m a
return PPExpr ann
d
          Maybe (PPExpr ann)
Nothing -> do
            AppPPExpr ann
a <- PPIndex
-> ProgramLoc
-> Text
-> [PrettyArg (Expr t)]
-> ST s (AppPPExpr ann)
renderApp PPIndex
idx ProgramLoc
loc Text
nm [PrettyArg (Expr t)]
args
            if PPIndex -> Bool
isShared PPIndex
idx then
              AppPPExpr ann -> ST s (PPExpr ann)
addBinding AppPPExpr ann
a
             else
              PPExpr ann -> ST s (PPExpr ann)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (AppPPExpr ann -> PPExpr ann
forall ann. AppPPExpr ann -> PPExpr ann
AppPPExpr AppPPExpr ann
a)

      bindFn :: ExprSymFn t idx ret -> ST s (PrettyArg (Expr t))
      bindFn :: ExprSymFn t idx ret -> ST s (PrettyArg (Expr t))
bindFn ExprSymFn t idx ret
f = do
        let idx :: Word64
idx = Nonce t (idx ::> ret) -> Word64
forall s k (tp :: k). Nonce s tp -> Word64
indexValue (ExprSymFn t idx ret -> Nonce t (idx ::> ret)
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Nonce t (args ::> ret)
symFnId ExprSymFn t idx ret
f)
        Maybe Text
mr <- HashTable s Word64 Text -> Word64 -> ST s (Maybe Text)
forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> ST s (Maybe v)
H.lookup HashTable s Word64 Text
visited_fns Word64
idx
        case Maybe Text
mr of
          Just Text
d -> PrettyArg (Expr t) -> ST s (PrettyArg (Expr t))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Text -> PrettyArg (Expr t)
forall (e :: BaseType -> Type). Text -> PrettyArg e
PrettyText Text
d)
          Maybe Text
Nothing -> do
            case ExprSymFn t idx ret -> SymFnInfo t idx ret
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SymFnInfo t args ret
symFnInfo ExprSymFn t idx ret
f of
              UninterpFnInfo{} -> do
                let def_doc :: Doc ann
def_doc = ExprSymFn t idx ret -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow ExprSymFn t idx ret
f Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"??"
                STRef s (Seq (Doc ann))
-> (Seq (Doc ann) -> Seq (Doc ann)) -> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef' STRef s (Seq (Doc ann))
bindingsRef (Seq (Doc ann) -> Doc ann -> Seq (Doc ann)
forall a. Seq a -> a -> Seq a
Seq.|> Doc ann
def_doc)
              DefinedFnInfo Assignment (ExprBoundVar t) idx
vars Expr t ret
rhs UnfoldPolicy
_ -> do
                -- TODO: avoid intermediate String from 'ppBoundVar'
                let pp_vars :: [Doc ann]
pp_vars = (forall (x :: BaseType). ExprBoundVar t x -> Doc ann)
-> Assignment (ExprBoundVar t) idx -> [Doc ann]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
toListFC (String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann)
-> (ExprBoundVar t x -> String) -> ExprBoundVar t x -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprBoundVar t x -> String
forall t (tp :: BaseType). ExprBoundVar t tp -> String
ppBoundVar) Assignment (ExprBoundVar t) idx
vars
                let def_doc :: Doc ann
def_doc = ExprSymFn t idx ret -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow ExprSymFn t idx ret
f Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep [Doc ann]
pp_vars Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Expr t ret -> Doc ann
forall t (tp :: BaseType) ann. Expr t tp -> Doc ann
ppExpr Expr t ret
rhs
                STRef s (Seq (Doc ann))
-> (Seq (Doc ann) -> Seq (Doc ann)) -> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef' STRef s (Seq (Doc ann))
bindingsRef (Seq (Doc ann) -> Doc ann -> Seq (Doc ann)
forall a. Seq a -> a -> Seq a
Seq.|> Doc ann
def_doc)
              MatlabSolverFnInfo MatlabSolverFn (Expr t) idx ret
fn_id Assignment (ExprBoundVar t) idx
_ Expr t ret
_ -> do
                let def_doc :: Doc ann
def_doc = ExprSymFn t idx ret -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow ExprSymFn t idx ret
f Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> MatlabSolverFn (Expr t) idx ret -> Doc ann
forall (f :: BaseType -> Type) (a :: Ctx BaseType) (r :: BaseType)
       ann.
IsExpr f =>
MatlabSolverFn f a r -> Doc ann
ppMatlabSolverFn MatlabSolverFn (Expr t) idx ret
fn_id
                STRef s (Seq (Doc ann))
-> (Seq (Doc ann) -> Seq (Doc ann)) -> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef' STRef s (Seq (Doc ann))
bindingsRef (Seq (Doc ann) -> Doc ann -> Seq (Doc ann)
forall a. Seq a -> a -> Seq a
Seq.|> Doc ann
def_doc)

            let d :: Text
d = String -> Text
Text.pack (ExprSymFn t idx ret -> String
forall a. Show a => a -> String
show ExprSymFn t idx ret
f)
            HashTable s Word64 Text -> Word64 -> Text -> ST s ()
forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> v -> ST s ()
H.insert HashTable s Word64 Text
visited_fns Word64
idx (Text -> ST s ()) -> Text -> ST s ()
forall a b. (a -> b) -> a -> b
$! Text
d
            PrettyArg (Expr t) -> ST s (PrettyArg (Expr t))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PrettyArg (Expr t) -> ST s (PrettyArg (Expr t)))
-> PrettyArg (Expr t) -> ST s (PrettyArg (Expr t))
forall a b. (a -> b) -> a -> b
$! Text -> PrettyArg (Expr t)
forall (e :: BaseType -> Type). Text -> PrettyArg e
PrettyText Text
d

      -- Collect definitions for all applications that occur multiple times
      -- in term.
      getBindings :: Expr t u -> ST s (PPExpr ann)
      getBindings :: Expr t u -> ST s (PPExpr ann)
getBindings (SemiRingLiteral SemiRingRepr sr
sr Coefficient sr
x ProgramLoc
l) =
        case SemiRingRepr sr
sr of
          SemiRingRepr sr
SR.SemiRingIntegerRepr ->
            PPExpr ann -> ST s (PPExpr ann)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PPExpr ann -> ST s (PPExpr ann))
-> PPExpr ann -> ST s (PPExpr ann)
forall a b. (a -> b) -> a -> b
$ String -> PPExpr ann
forall ann. String -> PPExpr ann
stringPPExpr (Integer -> String
forall a. Show a => a -> String
show Integer
Coefficient sr
x)
          SemiRingRepr sr
SR.SemiRingRealRepr -> PPIndex -> ProgramLoc -> PrettyApp (Expr t) -> ST s (PPExpr ann)
cacheResult (Rational -> PPIndex
RatPPIndex Rational
Coefficient sr
x) ProgramLoc
l PrettyApp (Expr t)
app
             where n :: Integer
n = Rational -> Integer
forall a. Ratio a -> a
numerator Rational
Coefficient sr
x
                   d :: Integer
d = Rational -> Integer
forall a. Ratio a -> a
denominator Rational
Coefficient sr
x
                   app :: PrettyApp (Expr t)
app | Integer
d Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1      = Text -> [PrettyArg (Expr t)] -> PrettyApp (Expr t)
forall (e :: BaseType -> Type).
Text -> [PrettyArg e] -> PrettyApp e
prettyApp (String -> Text
forall a. IsString a => String -> a
fromString (Integer -> String
forall a. Show a => a -> String
show Integer
n)) []
                       | Bool
use_decimal = Text -> [PrettyArg (Expr t)] -> PrettyApp (Expr t)
forall (e :: BaseType -> Type).
Text -> [PrettyArg e] -> PrettyApp e
prettyApp (String -> Text
forall a. IsString a => String -> a
fromString (Double -> String
forall a. Show a => a -> String
show (Rational -> Double
forall a. Fractional a => Rational -> a
fromRational Rational
Coefficient sr
x :: Double))) []
                       | Bool
otherwise   = Text -> [PrettyArg (Expr t)] -> PrettyApp (Expr t)
forall (e :: BaseType -> Type).
Text -> [PrettyArg e] -> PrettyApp e
prettyApp Text
"divReal"  [ Integer -> PrettyArg (Expr t)
forall a (e :: BaseType -> Type). Show a => a -> PrettyArg e
showPrettyArg Integer
n, Integer -> PrettyArg (Expr t)
forall a (e :: BaseType -> Type). Show a => a -> PrettyArg e
showPrettyArg Integer
d ]
          SR.SemiRingBVRepr BVFlavorRepr fv
_ NatRepr w
w ->
            PPExpr ann -> ST s (PPExpr ann)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PPExpr ann -> ST s (PPExpr ann))
-> PPExpr ann -> ST s (PPExpr ann)
forall a b. (a -> b) -> a -> b
$ String -> PPExpr ann
forall ann. String -> PPExpr ann
stringPPExpr (String -> PPExpr ann) -> String -> PPExpr ann
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BV w -> String
forall (w :: Nat). NatRepr w -> BV w -> String
BV.ppHex NatRepr w
w BV w
Coefficient sr
x

      getBindings (StringExpr StringLiteral si
x ProgramLoc
_) =
        PPExpr ann -> ST s (PPExpr ann)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PPExpr ann -> ST s (PPExpr ann))
-> PPExpr ann -> ST s (PPExpr ann)
forall a b. (a -> b) -> a -> b
$ String -> PPExpr ann
forall ann. String -> PPExpr ann
stringPPExpr (String -> PPExpr ann) -> String -> PPExpr ann
forall a b. (a -> b) -> a -> b
$ (StringLiteral si -> String
forall a. Show a => a -> String
show StringLiteral si
x)
      getBindings (FloatExpr FloatPrecisionRepr fpp
_ BigFloat
f ProgramLoc
_) =
        PPExpr ann -> ST s (PPExpr ann)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PPExpr ann -> ST s (PPExpr ann))
-> PPExpr ann -> ST s (PPExpr ann)
forall a b. (a -> b) -> a -> b
$ String -> PPExpr ann
forall ann. String -> PPExpr ann
stringPPExpr (BigFloat -> String
forall a. Show a => a -> String
show BigFloat
f)
      getBindings (BoolExpr Bool
b ProgramLoc
_) =
        PPExpr ann -> ST s (PPExpr ann)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PPExpr ann -> ST s (PPExpr ann))
-> PPExpr ann -> ST s (PPExpr ann)
forall a b. (a -> b) -> a -> b
$ String -> PPExpr ann
forall ann. String -> PPExpr ann
stringPPExpr (if Bool
b then String
"true" else String
"false")
      getBindings (NonceAppExpr NonceAppExpr t u
e) =
        PPIndex -> ProgramLoc -> PrettyApp (Expr t) -> ST s (PPExpr ann)
cacheResult (Word64 -> PPIndex
ExprPPIndex (Nonce t u -> Word64
forall s k (tp :: k). Nonce s tp -> Word64
indexValue (NonceAppExpr t u -> Nonce t u
forall t (tp :: BaseType). NonceAppExpr t tp -> Nonce t tp
nonceExprId NonceAppExpr t u
e))) (NonceAppExpr t u -> ProgramLoc
forall t (tp :: BaseType). NonceAppExpr t tp -> ProgramLoc
nonceExprLoc NonceAppExpr t u
e)
          (PrettyApp (Expr t) -> ST s (PPExpr ann))
-> ST s (PrettyApp (Expr t)) -> ST s (PPExpr ann)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall (ctx :: Ctx BaseType) (r :: BaseType).
 ExprSymFn t ctx r -> ST s (PrettyArg (Expr t)))
-> NonceApp t (Expr t) u -> ST s (PrettyApp (Expr t))
forall (m :: Type -> Type) t (e :: BaseType -> Type)
       (tp :: BaseType).
Applicative m =>
(forall (ctx :: Ctx BaseType) (r :: BaseType).
 ExprSymFn t ctx r -> m (PrettyArg e))
-> NonceApp t e tp -> m (PrettyApp e)
ppNonceApp forall (ctx :: Ctx BaseType) (r :: BaseType).
ExprSymFn t ctx r -> ST s (PrettyArg (Expr t))
bindFn (NonceAppExpr t u -> NonceApp t (Expr t) u
forall t (tp :: BaseType).
NonceAppExpr t tp -> NonceApp t (Expr t) tp
nonceExprApp NonceAppExpr t u
e)
      getBindings (AppExpr AppExpr t u
e) =
        PPIndex -> ProgramLoc -> PrettyApp (Expr t) -> ST s (PPExpr ann)
cacheResult (Word64 -> PPIndex
ExprPPIndex (Nonce t u -> Word64
forall s k (tp :: k). Nonce s tp -> Word64
indexValue (AppExpr t u -> Nonce t u
forall t (tp :: BaseType). AppExpr t tp -> Nonce t tp
appExprId AppExpr t u
e)))
                    (AppExpr t u -> ProgramLoc
forall t (tp :: BaseType). AppExpr t tp -> ProgramLoc
appExprLoc AppExpr t u
e)
                    (App (Expr t) u -> PrettyApp (Expr t)
forall (e :: BaseType -> Type) (u :: BaseType).
App e u -> PrettyApp e
ppApp' (AppExpr t u -> App (Expr t) u
forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
appExprApp AppExpr t u
e))
      getBindings (BoundVarExpr ExprBoundVar t u
i) =
        PPExpr ann -> ST s (PPExpr ann)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PPExpr ann -> ST s (PPExpr ann))
-> PPExpr ann -> ST s (PPExpr ann)
forall a b. (a -> b) -> a -> b
$ String -> PPExpr ann
forall ann. String -> PPExpr ann
stringPPExpr (String -> PPExpr ann) -> String -> PPExpr ann
forall a b. (a -> b) -> a -> b
$ ExprBoundVar t u -> String
forall t (tp :: BaseType). ExprBoundVar t tp -> String
ppBoundVar ExprBoundVar t u
i

  PPExpr ann
r <- Expr t tp -> ST s (PPExpr ann)
forall (u :: BaseType). Expr t u -> ST s (PPExpr ann)
getBindings Expr t tp
e0
  [Doc ann]
bindings <- Seq (Doc ann) -> [Doc ann]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList (Seq (Doc ann) -> [Doc ann])
-> ST s (Seq (Doc ann)) -> ST s [Doc ann]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> STRef s (Seq (Doc ann)) -> ST s (Seq (Doc ann))
forall s a. STRef s a -> ST s a
readSTRef STRef s (Seq (Doc ann))
bindingsRef
  ([Doc ann], PPExpr ann) -> ST s ([Doc ann], PPExpr ann)
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([Doc ann] -> [Doc ann]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList [Doc ann]
bindings, PPExpr ann
r)



------------------------------------------------------------------------
-- ExprBoundVar

-- | The Kind of a bound variable.
data VarKind
  = QuantifierVarKind
    -- ^ A variable appearing in a quantifier.
  | LatchVarKind
    -- ^ A variable appearing as a latch input.
  | UninterpVarKind
    -- ^ A variable appearing in a uninterpreted constant

-- | Information about bound variables.
-- Parameter @t@ is a phantom type brand used to track nonces.
--
-- Type @'ExprBoundVar' t@ instantiates the type family
-- @'BoundVar' ('ExprBuilder' t st)@.
--
-- Selector functions are provided to destruct 'ExprBoundVar'
-- values, but the constructor is kept hidden. The preferred way to
-- construct a 'ExprBoundVar' is to use 'freshBoundVar'.
data ExprBoundVar t (tp :: BaseType) =
  BVar { ExprBoundVar t tp -> Nonce t tp
bvarId  :: {-# UNPACK #-} !(Nonce t tp)
       , ExprBoundVar t tp -> ProgramLoc
bvarLoc :: !ProgramLoc
       , ExprBoundVar t tp -> SolverSymbol
bvarName :: !SolverSymbol
       , ExprBoundVar t tp -> BaseTypeRepr tp
bvarType :: !(BaseTypeRepr tp)
       , ExprBoundVar t tp -> VarKind
bvarKind :: !VarKind
       , ExprBoundVar t tp -> Maybe (AbstractValue tp)
bvarAbstractValue :: !(Maybe (AbstractValue tp))
       }

instance Eq (ExprBoundVar t tp) where
  ExprBoundVar t tp
x == :: ExprBoundVar t tp -> ExprBoundVar t tp -> Bool
== ExprBoundVar t tp
y = ExprBoundVar t tp -> Nonce t tp
forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId ExprBoundVar t tp
x Nonce t tp -> Nonce t tp -> Bool
forall a. Eq a => a -> a -> Bool
== ExprBoundVar t tp -> Nonce t tp
forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId ExprBoundVar t tp
y

instance TestEquality (ExprBoundVar t) where
  testEquality :: ExprBoundVar t a -> ExprBoundVar t b -> Maybe (a :~: b)
testEquality ExprBoundVar t a
x ExprBoundVar t b
y = Nonce t a -> Nonce t b -> Maybe (a :~: b)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (ExprBoundVar t a -> Nonce t a
forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId ExprBoundVar t a
x) (ExprBoundVar t b -> Nonce t b
forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId ExprBoundVar t b
y)

instance Ord (ExprBoundVar t tp) where
  compare :: ExprBoundVar t tp -> ExprBoundVar t tp -> Ordering
compare ExprBoundVar t tp
x ExprBoundVar t tp
y = Nonce t tp -> Nonce t tp -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (ExprBoundVar t tp -> Nonce t tp
forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId ExprBoundVar t tp
x) (ExprBoundVar t tp -> Nonce t tp
forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId ExprBoundVar t tp
y)

instance OrdF (ExprBoundVar t) where
  compareF :: ExprBoundVar t x -> ExprBoundVar t y -> OrderingF x y
compareF ExprBoundVar t x
x ExprBoundVar t y
y = Nonce t x -> Nonce t y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF (ExprBoundVar t x -> Nonce t x
forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId ExprBoundVar t x
x) (ExprBoundVar t y -> Nonce t y
forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId ExprBoundVar t y
y)

instance Hashable (ExprBoundVar t tp) where
  hashWithSalt :: Int -> ExprBoundVar t tp -> Int
hashWithSalt Int
s ExprBoundVar t tp
x = Int -> Nonce t tp -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (ExprBoundVar t tp -> Nonce t tp
forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId ExprBoundVar t tp
x)

instance HashableF (ExprBoundVar t) where
  hashWithSaltF :: Int -> ExprBoundVar t tp -> Int
hashWithSaltF = Int -> ExprBoundVar t tp -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt

------------------------------------------------------------------------
-- NonceApp

-- | Type @NonceApp t e tp@ encodes the top-level application of an
-- 'Expr'. It includes expression forms that bind variables (contrast
-- with 'App').
--
-- Parameter @t@ is a phantom type brand used to track nonces.
-- Parameter @e@ is used everywhere a recursive sub-expression would
-- go. Uses of the 'NonceApp' type will tie the knot through this
-- parameter. Parameter @tp@ indicates the type of the expression.
data NonceApp t (e :: BaseType -> Type) (tp :: BaseType) where
  Annotation ::
    !(BaseTypeRepr tp) ->
    !(Nonce t tp) ->
    !(e tp) ->
    NonceApp t e tp

  Forall :: !(ExprBoundVar t tp)
         -> !(e BaseBoolType)
         -> NonceApp t e BaseBoolType
  Exists :: !(ExprBoundVar t tp)
         -> !(e BaseBoolType)
         -> NonceApp t e BaseBoolType

  -- Create an array from a function
  ArrayFromFn :: !(ExprSymFn t (idx ::> itp) ret)
              -> NonceApp t e (BaseArrayType (idx ::> itp) ret)

  -- Create an array by mapping over one or more existing arrays.
  MapOverArrays :: !(ExprSymFn t (ctx::>d) r)
                -> !(Ctx.Assignment BaseTypeRepr (idx ::> itp))
                -> !(Ctx.Assignment (ArrayResultWrapper e (idx ::> itp)) (ctx::>d))
                -> NonceApp t e (BaseArrayType (idx ::> itp) r)

  -- This returns true if all the indices satisfying the given predicate equal true.
  ArrayTrueOnEntries
    :: !(ExprSymFn t (idx ::> itp) BaseBoolType)
    -> !(e (BaseArrayType (idx ::> itp) BaseBoolType))
    -> NonceApp t e BaseBoolType

  -- Apply a function to some arguments
  FnApp :: !(ExprSymFn t args ret)
        -> !(Ctx.Assignment e args)
        -> NonceApp t e ret


------------------------------------------------------------------------
-- ExprSymFn

-- | This describes information about an undefined or defined function.
-- Parameter @t@ is a phantom type brand used to track nonces.
-- The @args@ and @ret@ parameters define the types of arguments
-- and the return type of the function.
data SymFnInfo t (args :: Ctx BaseType) (ret :: BaseType)
   = UninterpFnInfo !(Ctx.Assignment BaseTypeRepr args)
                    !(BaseTypeRepr ret)
     -- ^ Information about the argument type and return type of an uninterpreted function.

   | DefinedFnInfo !(Ctx.Assignment (ExprBoundVar t) args)
                   !(Expr t ret)
                   !UnfoldPolicy
     -- ^ Information about a defined function.
     -- Includes bound variables and an expression associated to a defined function,
     -- as well as a policy for when to unfold the body.

   | MatlabSolverFnInfo !(MatlabSolverFn (Expr t) args ret)
                        !(Ctx.Assignment (ExprBoundVar t) args)
                        !(Expr t ret)
     -- ^ This is a function that corresponds to a matlab solver function.
     --   It includes the definition as a ExprBuilder expr to
     --   enable export to other solvers.

-- | This represents a symbolic function in the simulator.
-- Parameter @t@ is a phantom type brand used to track nonces.
-- The @args@ and @ret@ parameters define the types of arguments
-- and the return type of the function.
--
-- Type @'ExprSymFn' t (Expr t)@ instantiates the type family @'SymFn'
-- ('ExprBuilder' t st)@.
data ExprSymFn t (args :: Ctx BaseType) (ret :: BaseType)
   = ExprSymFn { ExprSymFn t args ret -> Nonce t (args ::> ret)
symFnId :: !(Nonce t (args ::> ret))
                 -- /\ A unique identifier for the function
                 , ExprSymFn t args ret -> SolverSymbol
symFnName :: !SolverSymbol
                 -- /\ Name of the function
                 , ExprSymFn t args ret -> SymFnInfo t args ret
symFnInfo :: !(SymFnInfo t args ret)
                 -- /\ Information about function
                 , ExprSymFn t args ret -> ProgramLoc
symFnLoc  :: !ProgramLoc
                 -- /\ Location where function was defined.
                 }

instance Show (ExprSymFn t args ret) where
  show :: ExprSymFn t args ret -> String
show ExprSymFn t args ret
f | ExprSymFn t args ret -> SolverSymbol
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SolverSymbol
symFnName ExprSymFn t args ret
f SolverSymbol -> SolverSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== SolverSymbol
emptySymbol = String
"f" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall a. Show a => a -> String
show (Nonce t (args ::> ret) -> Word64
forall s k (tp :: k). Nonce s tp -> Word64
indexValue (ExprSymFn t args ret -> Nonce t (args ::> ret)
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Nonce t (args ::> ret)
symFnId ExprSymFn t args ret
f))
         | Bool
otherwise                  = SolverSymbol -> String
forall a. Show a => a -> String
show (ExprSymFn t args ret -> SolverSymbol
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SolverSymbol
symFnName ExprSymFn t args ret
f)

symFnArgTypes :: ExprSymFn t args ret -> Ctx.Assignment BaseTypeRepr args
symFnArgTypes :: ExprSymFn t args ret -> Assignment BaseTypeRepr args
symFnArgTypes ExprSymFn t args ret
f =
  case ExprSymFn t args ret -> SymFnInfo t args ret
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SymFnInfo t args ret
symFnInfo ExprSymFn t args ret
f of
    UninterpFnInfo Assignment BaseTypeRepr args
tps BaseTypeRepr ret
_ -> Assignment BaseTypeRepr args
tps
    DefinedFnInfo Assignment (ExprBoundVar t) args
vars Expr t ret
_ UnfoldPolicy
_ -> (forall (x :: BaseType). ExprBoundVar t x -> BaseTypeRepr x)
-> Assignment (ExprBoundVar t) args -> Assignment BaseTypeRepr args
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
fmapFC forall t (tp :: BaseType). ExprBoundVar t tp -> BaseTypeRepr tp
forall (x :: BaseType). ExprBoundVar t x -> BaseTypeRepr x
bvarType Assignment (ExprBoundVar t) args
vars
    MatlabSolverFnInfo MatlabSolverFn (Expr t) args ret
fn_id Assignment (ExprBoundVar t) args
_ Expr t ret
_ -> MatlabSolverFn (Expr t) args ret -> Assignment BaseTypeRepr args
forall (f :: BaseType -> Type) (args :: Ctx BaseType)
       (ret :: BaseType).
MatlabSolverFn f args ret -> Assignment BaseTypeRepr args
matlabSolverArgTypes MatlabSolverFn (Expr t) args ret
fn_id

symFnReturnType :: ExprSymFn t args ret -> BaseTypeRepr ret
symFnReturnType :: ExprSymFn t args ret -> BaseTypeRepr ret
symFnReturnType ExprSymFn t args ret
f =
  case ExprSymFn t args ret -> SymFnInfo t args ret
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SymFnInfo t args ret
symFnInfo ExprSymFn t args ret
f of
    UninterpFnInfo Assignment BaseTypeRepr args
_ BaseTypeRepr ret
tp -> BaseTypeRepr ret
tp
    DefinedFnInfo Assignment (ExprBoundVar t) args
_ Expr t ret
r UnfoldPolicy
_ -> Expr t ret -> BaseTypeRepr ret
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType Expr t ret
r
    MatlabSolverFnInfo MatlabSolverFn (Expr t) args ret
fn_id Assignment (ExprBoundVar t) args
_ Expr t ret
_ -> MatlabSolverFn (Expr t) args ret -> BaseTypeRepr ret
forall (f :: BaseType -> Type) (args :: Ctx BaseType)
       (ret :: BaseType).
MatlabSolverFn f args ret -> BaseTypeRepr ret
matlabSolverReturnType MatlabSolverFn (Expr t) args ret
fn_id

-- | Return solver function associated with ExprSymFn if any.
asMatlabSolverFn :: ExprSymFn t args ret -> Maybe (MatlabSolverFn (Expr t) args ret)
asMatlabSolverFn :: ExprSymFn t args ret -> Maybe (MatlabSolverFn (Expr t) args ret)
asMatlabSolverFn ExprSymFn t args ret
f
  | MatlabSolverFnInfo MatlabSolverFn (Expr t) args ret
g Assignment (ExprBoundVar t) args
_ Expr t ret
_ <- ExprSymFn t args ret -> SymFnInfo t args ret
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> SymFnInfo t args ret
symFnInfo ExprSymFn t args ret
f = MatlabSolverFn (Expr t) args ret
-> Maybe (MatlabSolverFn (Expr t) args ret)
forall a. a -> Maybe a
Just MatlabSolverFn (Expr t) args ret
g
  | Bool
otherwise = Maybe (MatlabSolverFn (Expr t) args ret)
forall a. Maybe a
Nothing


instance Hashable (ExprSymFn t args tp) where
  hashWithSalt :: Int -> ExprSymFn t args tp -> Int
hashWithSalt Int
s ExprSymFn t args tp
f = Int
s Int -> Nonce t (args ::> tp) -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` ExprSymFn t args tp -> Nonce t (args ::> tp)
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Nonce t (args ::> ret)
symFnId ExprSymFn t args tp
f

testExprSymFnEq ::
  ExprSymFn t a1 r1 -> ExprSymFn t a2 r2 -> Maybe ((a1::>r1) :~: (a2::>r2))
testExprSymFnEq :: ExprSymFn t a1 r1
-> ExprSymFn t a2 r2 -> Maybe ((a1 ::> r1) :~: (a2 ::> r2))
testExprSymFnEq ExprSymFn t a1 r1
f ExprSymFn t a2 r2
g = Nonce t (a1 ::> r1)
-> Nonce t (a2 ::> r2) -> Maybe ((a1 ::> r1) :~: (a2 ::> r2))
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (ExprSymFn t a1 r1 -> Nonce t (a1 ::> r1)
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Nonce t (args ::> ret)
symFnId ExprSymFn t a1 r1
f) (ExprSymFn t a2 r2 -> Nonce t (a2 ::> r2)
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Nonce t (args ::> ret)
symFnId ExprSymFn t a2 r2
g)


instance IsSymFn (ExprSymFn t) where
  fnArgTypes :: ExprSymFn t args ret -> Assignment BaseTypeRepr args
fnArgTypes = ExprSymFn t args ret -> Assignment BaseTypeRepr args
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Assignment BaseTypeRepr args
symFnArgTypes
  fnReturnType :: ExprSymFn t args ret -> BaseTypeRepr ret
fnReturnType = ExprSymFn t args ret -> BaseTypeRepr ret
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> BaseTypeRepr ret
symFnReturnType


-------------------------------------------------------------------------------
-- BVOrSet

data BVOrNote w = BVOrNote !IncrHash !(BVD.BVDomain w)

instance Semigroup (BVOrNote w) where
  BVOrNote IncrHash
xh BVDomain w
xa <> :: BVOrNote w -> BVOrNote w -> BVOrNote w
<> BVOrNote IncrHash
yh BVDomain w
ya = IncrHash -> BVDomain w -> BVOrNote w
forall (w :: Nat). IncrHash -> BVDomain w -> BVOrNote w
BVOrNote (IncrHash
xh IncrHash -> IncrHash -> IncrHash
forall a. Semigroup a => a -> a -> a
<> IncrHash
yh) (BVDomain w -> BVDomain w -> BVDomain w
forall (w :: Nat). BVDomain w -> BVDomain w -> BVDomain w
BVD.or BVDomain w
xa BVDomain w
ya)

newtype BVOrSet e w = BVOrSet (AM.AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ())

traverseBVOrSet :: (HashableF f, HasAbsValue f, OrdF f, Applicative m) =>
  (forall tp. e tp -> m (f tp)) ->
  (BVOrSet e w -> m (BVOrSet f w))
traverseBVOrSet :: (forall (tp :: BaseType). e tp -> m (f tp))
-> BVOrSet e w -> m (BVOrSet f w)
traverseBVOrSet forall (tp :: BaseType). e tp -> m (f tp)
f (BVOrSet AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
m) =
  (f (BaseBVType w) -> BVOrSet f w -> BVOrSet f w)
-> BVOrSet f w -> [f (BaseBVType w)] -> BVOrSet f w
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr f (BaseBVType w) -> BVOrSet f w -> BVOrSet f w
forall (e :: BaseType -> Type) (w :: Nat).
(OrdF e, HashableF e, HasAbsValue e) =>
e (BaseBVType w) -> BVOrSet e w -> BVOrSet e w
bvOrInsert (AnnotatedMap (Wrap f (BaseBVType w)) (BVOrNote w) () -> BVOrSet f w
forall (e :: BaseType -> Type) (w :: Nat).
AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) () -> BVOrSet e w
BVOrSet AnnotatedMap (Wrap f (BaseBVType w)) (BVOrNote w) ()
forall k v a. (Ord k, Semigroup v) => AnnotatedMap k v a
AM.empty) ([f (BaseBVType w)] -> BVOrSet f w)
-> m [f (BaseBVType w)] -> m (BVOrSet f w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Wrap e (BaseBVType w), ()) -> m (f (BaseBVType w)))
-> [(Wrap e (BaseBVType w), ())] -> m [f (BaseBVType w)]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (e (BaseBVType w) -> m (f (BaseBVType w))
forall (tp :: BaseType). e tp -> m (f tp)
f (e (BaseBVType w) -> m (f (BaseBVType w)))
-> ((Wrap e (BaseBVType w), ()) -> e (BaseBVType w))
-> (Wrap e (BaseBVType w), ())
-> m (f (BaseBVType w))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wrap e (BaseBVType w) -> e (BaseBVType w)
forall k (f :: k -> Type) (x :: k). Wrap f x -> f x
unWrap (Wrap e (BaseBVType w) -> e (BaseBVType w))
-> ((Wrap e (BaseBVType w), ()) -> Wrap e (BaseBVType w))
-> (Wrap e (BaseBVType w), ())
-> e (BaseBVType w)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Wrap e (BaseBVType w), ()) -> Wrap e (BaseBVType w)
forall a b. (a, b) -> a
fst) (AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
-> [(Wrap e (BaseBVType w), ())]
forall k v a. AnnotatedMap k v a -> [(k, a)]
AM.toList AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
m)

bvOrInsert :: (OrdF e, HashableF e, HasAbsValue e) => e (BaseBVType w) -> BVOrSet e w -> BVOrSet e w
bvOrInsert :: e (BaseBVType w) -> BVOrSet e w -> BVOrSet e w
bvOrInsert e (BaseBVType w)
e (BVOrSet AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
m) = AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) () -> BVOrSet e w
forall (e :: BaseType -> Type) (w :: Nat).
AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) () -> BVOrSet e w
BVOrSet (AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
 -> BVOrSet e w)
-> AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
-> BVOrSet e w
forall a b. (a -> b) -> a -> b
$ Wrap e (BaseBVType w)
-> BVOrNote w
-> ()
-> AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
-> AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
forall k v a.
(Ord k, Semigroup v) =>
k -> v -> a -> AnnotatedMap k v a -> AnnotatedMap k v a
AM.insert (e (BaseBVType w) -> Wrap e (BaseBVType w)
forall k (f :: k -> Type) (x :: k). f x -> Wrap f x
Wrap e (BaseBVType w)
e) (IncrHash -> BVDomain w -> BVOrNote w
forall (w :: Nat). IncrHash -> BVDomain w -> BVOrNote w
BVOrNote (Int -> IncrHash
mkIncrHash (e (BaseBVType w) -> Int
forall k (f :: k -> Type) (tp :: k). HashableF f => f tp -> Int
hashF e (BaseBVType w)
e)) (e (BaseBVType w) -> AbstractValue (BaseBVType w)
forall (f :: BaseType -> Type) (tp :: BaseType).
HasAbsValue f =>
f tp -> AbstractValue tp
getAbsValue e (BaseBVType w)
e)) () AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
m

bvOrSingleton :: (OrdF e, HashableF e, HasAbsValue e) => e (BaseBVType w) -> BVOrSet e w
bvOrSingleton :: e (BaseBVType w) -> BVOrSet e w
bvOrSingleton e (BaseBVType w)
e = e (BaseBVType w) -> BVOrSet e w -> BVOrSet e w
forall (e :: BaseType -> Type) (w :: Nat).
(OrdF e, HashableF e, HasAbsValue e) =>
e (BaseBVType w) -> BVOrSet e w -> BVOrSet e w
bvOrInsert e (BaseBVType w)
e (AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) () -> BVOrSet e w
forall (e :: BaseType -> Type) (w :: Nat).
AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) () -> BVOrSet e w
BVOrSet AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
forall k v a. (Ord k, Semigroup v) => AnnotatedMap k v a
AM.empty)

bvOrContains :: OrdF e => e (BaseBVType w) -> BVOrSet e w -> Bool
bvOrContains :: e (BaseBVType w) -> BVOrSet e w -> Bool
bvOrContains e (BaseBVType w)
x (BVOrSet AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
m) = Maybe (BVOrNote w, ()) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (BVOrNote w, ()) -> Bool) -> Maybe (BVOrNote w, ()) -> Bool
forall a b. (a -> b) -> a -> b
$ Wrap e (BaseBVType w)
-> AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
-> Maybe (BVOrNote w, ())
forall k v a.
(Ord k, Semigroup v) =>
k -> AnnotatedMap k v a -> Maybe (v, a)
AM.lookup (e (BaseBVType w) -> Wrap e (BaseBVType w)
forall k (f :: k -> Type) (x :: k). f x -> Wrap f x
Wrap e (BaseBVType w)
x) AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
m

bvOrUnion :: OrdF e => BVOrSet e w -> BVOrSet e w -> BVOrSet e w
bvOrUnion :: BVOrSet e w -> BVOrSet e w -> BVOrSet e w
bvOrUnion (BVOrSet AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
x) (BVOrSet AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
y) = AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) () -> BVOrSet e w
forall (e :: BaseType -> Type) (w :: Nat).
AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) () -> BVOrSet e w
BVOrSet (AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
-> AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
-> AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
forall k v a.
(Ord k, Semigroup v) =>
AnnotatedMap k v a -> AnnotatedMap k v a -> AnnotatedMap k v a
AM.union AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
x AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
y)

bvOrToList :: BVOrSet e w -> [e (BaseBVType w)]
bvOrToList :: BVOrSet e w -> [e (BaseBVType w)]
bvOrToList (BVOrSet AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
m) = Wrap e (BaseBVType w) -> e (BaseBVType w)
forall k (f :: k -> Type) (x :: k). Wrap f x -> f x
unWrap (Wrap e (BaseBVType w) -> e (BaseBVType w))
-> ((Wrap e (BaseBVType w), ()) -> Wrap e (BaseBVType w))
-> (Wrap e (BaseBVType w), ())
-> e (BaseBVType w)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Wrap e (BaseBVType w), ()) -> Wrap e (BaseBVType w)
forall a b. (a, b) -> a
fst ((Wrap e (BaseBVType w), ()) -> e (BaseBVType w))
-> [(Wrap e (BaseBVType w), ())] -> [e (BaseBVType w)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
-> [(Wrap e (BaseBVType w), ())]
forall k v a. AnnotatedMap k v a -> [(k, a)]
AM.toList AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
m

bvOrAbs :: (OrdF e, 1 <= w) => NatRepr w -> BVOrSet e w -> BVD.BVDomain w
bvOrAbs :: NatRepr w -> BVOrSet e w -> BVDomain w
bvOrAbs NatRepr w
w (BVOrSet AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
m) =
  case AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
-> Maybe (BVOrNote w)
forall k v a. (Ord k, Semigroup v) => AnnotatedMap k v a -> Maybe v
AM.annotation AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
m of
    Just (BVOrNote IncrHash
_ BVDomain w
a) -> BVDomain w
a
    Maybe (BVOrNote w)
Nothing -> NatRepr w -> Integer -> BVDomain w
forall (w :: Nat).
(HasCallStack, 1 <= w) =>
NatRepr w -> Integer -> BVDomain w
BVD.singleton NatRepr w
w Integer
0

instance (OrdF e, TestEquality e) => Eq (BVOrSet e w) where
  BVOrSet AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
x == :: BVOrSet e w -> BVOrSet e w -> Bool
== BVOrSet AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
y = (() -> () -> Bool)
-> AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
-> AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
-> Bool
forall k a v.
Eq k =>
(a -> a -> Bool)
-> AnnotatedMap k v a -> AnnotatedMap k v a -> Bool
AM.eqBy (\()
_ ()
_ -> Bool
True) AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
x AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
y

instance OrdF e => Hashable (BVOrSet e w) where
  hashWithSalt :: Int -> BVOrSet e w -> Int
hashWithSalt Int
s (BVOrSet AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
m) =
    case AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
-> Maybe (BVOrNote w)
forall k v a. (Ord k, Semigroup v) => AnnotatedMap k v a -> Maybe v
AM.annotation AnnotatedMap (Wrap e (BaseBVType w)) (BVOrNote w) ()
m of
      Just (BVOrNote IncrHash
h BVDomain w
_) -> Int -> IncrHash -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s IncrHash
h
      Maybe (BVOrNote w)
Nothing -> Int
s


------------------------------------------------------------------------
-- App

-- | Type @'App' e tp@ encodes the top-level application of an 'Expr'
-- expression. It includes first-order expression forms that do not
-- bind variables (contrast with 'NonceApp').
--
-- Parameter @e@ is used everywhere a recursive sub-expression would
-- go. Uses of the 'App' type will tie the knot through this
-- parameter. Parameter @tp@ indicates the type of the expression.
data App (e :: BaseType -> Type) (tp :: BaseType) where

  ------------------------------------------------------------------------
  -- Generic operations

  BaseIte ::
    !(BaseTypeRepr tp) ->
    !Integer {- Total number of predicates in this ite tree -} ->
    !(e BaseBoolType) ->
    !(e tp) ->
    !(e tp) ->
    App e tp

  BaseEq ::
    !(BaseTypeRepr tp) ->
    !(e tp) ->
    !(e tp) ->
    App e BaseBoolType

  ------------------------------------------------------------------------
  -- Boolean operations

  -- Invariant: The argument to a NotPred must not be another NotPred.
  NotPred :: !(e BaseBoolType) -> App e BaseBoolType

  -- Invariant: The BoolMap must contain at least two elements. No
  -- element may be a NotPred; negated elements must be represented
  -- with Negative element polarity.
  ConjPred :: !(BoolMap e) -> App e BaseBoolType

  ------------------------------------------------------------------------
  -- Semiring operations

  SemiRingSum ::
    {-# UNPACK #-} !(WeightedSum e sr) ->
    App e (SR.SemiRingBase sr)

  -- A product of semiring values
  --
  -- The ExprBuilder should maintain the invariant that none of the values is
  -- a constant, and hence this denotes a non-linear expression.
  -- Multiplications by scalars should use the 'SemiRingSum' constructor.
  SemiRingProd ::
     {-# UNPACK #-} !(SemiRingProduct e sr) ->
     App e (SR.SemiRingBase sr)

  SemiRingLe
     :: !(SR.OrderedSemiRingRepr sr)
     -> !(e (SR.SemiRingBase sr))
     -> !(e (SR.SemiRingBase sr))
     -> App e BaseBoolType

  ------------------------------------------------------------------------
  -- Basic arithmetic operations

  RealIsInteger :: !(e BaseRealType) -> App e BaseBoolType

  IntDiv :: !(e BaseIntegerType)  -> !(e BaseIntegerType) -> App e BaseIntegerType
  IntMod :: !(e BaseIntegerType)  -> !(e BaseIntegerType) -> App e BaseIntegerType
  IntAbs :: !(e BaseIntegerType)  -> App e BaseIntegerType
  IntDivisible :: !(e BaseIntegerType) -> Natural -> App e BaseBoolType

  RealDiv :: !(e BaseRealType) -> !(e BaseRealType) -> App e BaseRealType

  -- Returns @sqrt(x)@, result is not defined if @x@ is negative.
  RealSqrt :: !(e BaseRealType) -> App e BaseRealType

  ------------------------------------------------------------------------
  -- Operations that introduce irrational numbers.

  Pi :: App e BaseRealType

  RealSin   :: !(e BaseRealType) -> App e BaseRealType
  RealCos   :: !(e BaseRealType) -> App e BaseRealType
  RealATan2 :: !(e BaseRealType) -> !(e BaseRealType) -> App e BaseRealType
  RealSinh  :: !(e BaseRealType) -> App e BaseRealType
  RealCosh  :: !(e BaseRealType) -> App e BaseRealType

  RealExp :: !(e BaseRealType) -> App e BaseRealType
  RealLog :: !(e BaseRealType) -> App e BaseRealType

  --------------------------------
  -- Bitvector operations

  -- Return value of bit at given index.
  BVTestBit :: (1 <= w)
            => !Natural -- Index of bit to test
                        -- (least-significant bit has index 0)
            -> !(e (BaseBVType w))
            -> App e BaseBoolType
  BVSlt :: (1 <= w)
        => !(e (BaseBVType w))
        -> !(e (BaseBVType w))
        -> App e BaseBoolType
  BVUlt :: (1 <= w)
        => !(e (BaseBVType w))
        -> !(e (BaseBVType w))
        -> App e BaseBoolType

  BVOrBits :: (1 <= w) => !(NatRepr w) -> !(BVOrSet e w) -> App e (BaseBVType w)

  -- A unary representation of terms where an integer @i@ is mapped to a
  -- predicate that is true if the unsigned encoding of the value is greater
  -- than or equal to @i@.
  --
  -- The map contains a binding (i -> p_i) when the predicate
  --
  -- As an example, we can encode the value @1@ with the assignment:
  --   { 0 => true ; 2 => false }
  BVUnaryTerm :: (1 <= n)
              => !(UnaryBV (e BaseBoolType) n)
              -> App e (BaseBVType n)

  BVConcat :: (1 <= u, 1 <= v, 1 <= (u+v))
           => !(NatRepr (u+v))
           -> !(e (BaseBVType u))
           -> !(e (BaseBVType v))
           -> App e (BaseBVType (u+v))

  BVSelect :: (1 <= n, idx + n <= w)
              -- First bit to select from (least-significant bit has index 0)
           => !(NatRepr idx)
              -- Number of bits to select, counting up toward more significant bits
           -> !(NatRepr n)
              -- Bitvector to select from.
           -> !(e (BaseBVType w))
           -> App e (BaseBVType n)

  BVFill :: (1 <= w)
         => !(NatRepr w)
         -> !(e BaseBoolType)
         -> App e (BaseBVType w)

  BVUdiv :: (1 <= w)
         => !(NatRepr w)
         -> !(e (BaseBVType w))
         -> !(e (BaseBVType w))
         -> App e (BaseBVType w)
  BVUrem :: (1 <= w)
         => !(NatRepr w)
         -> !(e (BaseBVType w))
         -> !(e (BaseBVType w))
         -> App e (BaseBVType w)
  BVSdiv :: (1 <= w)
         => !(NatRepr w)
         -> !(e (BaseBVType w))
         -> !(e (BaseBVType w))
         -> App e (BaseBVType w)
  BVSrem :: (1 <= w)
         => !(NatRepr w)
         -> !(e (BaseBVType w))
         -> !(e (BaseBVType w))
         -> App e (BaseBVType w)

  BVShl :: (1 <= w)
        => !(NatRepr w)
        -> !(e (BaseBVType w))
        -> !(e (BaseBVType w))
        -> App e (BaseBVType w)

  BVLshr :: (1 <= w)
         => !(NatRepr w)
         -> !(e (BaseBVType w))
         -> !(e (BaseBVType w))
         -> App e (BaseBVType w)

  BVAshr :: (1 <= w)
         => !(NatRepr w)
         -> !(e (BaseBVType w))
         -> !(e (BaseBVType w))
         -> App e (BaseBVType w)

  BVRol :: (1 <= w)
        => !(NatRepr w)
        -> !(e (BaseBVType w)) -- bitvector to rotate
        -> !(e (BaseBVType w)) -- rotate amount
        -> App e (BaseBVType w)

  BVRor :: (1 <= w)
        => !(NatRepr w)
        -> !(e (BaseBVType w))   -- bitvector to rotate
        -> !(e (BaseBVType w))   -- rotate amount
        -> App e (BaseBVType w)

  BVZext :: (1 <= w, w+1 <= r, 1 <= r)
         => !(NatRepr r)
         -> !(e (BaseBVType w))
         -> App e (BaseBVType r)

  BVSext :: (1 <= w, w+1 <= r, 1 <= r)
         => !(NatRepr r)
         -> !(e (BaseBVType w))
         -> App e (BaseBVType r)

  BVPopcount ::
    (1 <= w) =>
    !(NatRepr w) ->
    !(e (BaseBVType w)) ->
    App e (BaseBVType w)

  BVCountTrailingZeros ::
    (1 <= w) =>
    !(NatRepr w) ->
    !(e (BaseBVType w)) ->
    App e (BaseBVType w)

  BVCountLeadingZeros ::
    (1 <= w) =>
    !(NatRepr w) ->
    !(e (BaseBVType w)) ->
    App e (BaseBVType w)

  --------------------------------
  -- Float operations

  FloatNeg
    :: !(FloatPrecisionRepr fpp)
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatAbs
    :: !(FloatPrecisionRepr fpp)
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatSqrt
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatAdd
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatSub
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatMul
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatDiv
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatRem
    :: !(FloatPrecisionRepr fpp)
    -> !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatFMA
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatFpEq
    :: !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e BaseBoolType
  FloatLe
    :: !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e BaseBoolType
  FloatLt
    :: !(e (BaseFloatType fpp))
    -> !(e (BaseFloatType fpp))
    -> App e BaseBoolType
  FloatIsNaN :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  FloatIsInf :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  FloatIsZero :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  FloatIsPos :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  FloatIsNeg :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  FloatIsSubnorm :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  FloatIsNorm :: !(e (BaseFloatType fpp)) -> App e BaseBoolType
  FloatCast
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp'))
    -> App e (BaseFloatType fpp)
  FloatRound
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> App e (BaseFloatType fpp)
  FloatFromBinary
    :: (2 <= eb, 2 <= sb)
    => !(FloatPrecisionRepr (FloatingPointPrecision eb sb))
    -> !(e (BaseBVType (eb + sb)))
    -> App e (BaseFloatType (FloatingPointPrecision eb sb))
  FloatToBinary
    :: (2 <= eb, 2 <= sb, 1 <= eb + sb)
    => !(FloatPrecisionRepr (FloatingPointPrecision eb sb))
    -> !(e (BaseFloatType (FloatingPointPrecision eb sb)))
    -> App e (BaseBVType (eb + sb))
  BVToFloat
    :: (1 <= w)
    => !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseBVType w))
    -> App e (BaseFloatType fpp)
  SBVToFloat
    :: (1 <= w)
    => !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e (BaseBVType w))
    -> App e (BaseFloatType fpp)
  RealToFloat
    :: !(FloatPrecisionRepr fpp)
    -> !RoundingMode
    -> !(e BaseRealType)
    -> App e (BaseFloatType fpp)
  FloatToBV
    :: (1 <= w)
    => !(NatRepr w)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> App e (BaseBVType w)
  FloatToSBV
    :: (1 <= w)
    => !(NatRepr w)
    -> !RoundingMode
    -> !(e (BaseFloatType fpp))
    -> App e (BaseBVType w)
  FloatToReal :: !(e (BaseFloatType fpp)) -> App e BaseRealType

  ------------------------------------------------------------------------
  -- Array operations

  -- Partial map from concrete indices to array values over another array.
  ArrayMap :: !(Ctx.Assignment BaseTypeRepr (i ::> itp))
           -> !(BaseTypeRepr tp)
                -- /\ The type of the array.
           -> !(AUM.ArrayUpdateMap e (i ::> itp) tp)
              -- /\ Maps indices that are updated to the associated value.
           -> !(e (BaseArrayType (i::> itp) tp))
              -- /\ The underlying array that has been updated.
           -> App e (BaseArrayType (i ::> itp) tp)

  -- Constant array
  ConstantArray :: !(Ctx.Assignment BaseTypeRepr (i ::> tp))
                -> !(BaseTypeRepr b)
                -> !(e b)
                -> App e (BaseArrayType (i::>tp) b)

  UpdateArray :: !(BaseTypeRepr b)
              -> !(Ctx.Assignment BaseTypeRepr (i::>tp))
              -> !(e (BaseArrayType (i::>tp) b))
              -> !(Ctx.Assignment e (i::>tp))
              -> !(e b)
              -> App e (BaseArrayType (i::>tp) b)

  SelectArray :: !(BaseTypeRepr b)
              -> !(e (BaseArrayType (i::>tp) b))
              -> !(Ctx.Assignment e (i::>tp))
              -> App e b

  ------------------------------------------------------------------------
  -- Conversions.

  IntegerToReal :: !(e BaseIntegerType) -> App e BaseRealType

  -- Convert a real value to an integer
  --
  -- Not defined on non-integral reals.
  RealToInteger :: !(e BaseRealType) -> App e BaseIntegerType

  BVToInteger   :: (1 <= w) => !(e (BaseBVType w)) -> App e BaseIntegerType
  SBVToInteger  :: (1 <= w) => !(e (BaseBVType w)) -> App e BaseIntegerType

  -- Converts integer to a bitvector.  The number is interpreted modulo 2^n.
  IntegerToBV  :: (1 <= w) => !(e BaseIntegerType) -> NatRepr w -> App e (BaseBVType w)

  RoundReal :: !(e BaseRealType) -> App e BaseIntegerType
  RoundEvenReal :: !(e BaseRealType) -> App e BaseIntegerType
  FloorReal :: !(e BaseRealType) -> App e BaseIntegerType
  CeilReal  :: !(e BaseRealType) -> App e BaseIntegerType

  ------------------------------------------------------------------------
  -- Complex operations

  Cplx  :: {-# UNPACK #-} !(Complex (e BaseRealType)) -> App e BaseComplexType
  RealPart :: !(e BaseComplexType) -> App e BaseRealType
  ImagPart :: !(e BaseComplexType) -> App e BaseRealType

  ------------------------------------------------------------------------
  -- Strings

  StringContains :: !(e (BaseStringType si))
                 -> !(e (BaseStringType si))
                 -> App e BaseBoolType

  StringIsPrefixOf :: !(e (BaseStringType si))
                 -> !(e (BaseStringType si))
                 -> App e BaseBoolType

  StringIsSuffixOf :: !(e (BaseStringType si))
                 -> !(e (BaseStringType si))
                 -> App e BaseBoolType

  StringIndexOf :: !(e (BaseStringType si))
                -> !(e (BaseStringType si))
                -> !(e BaseIntegerType)
                -> App e BaseIntegerType

  StringSubstring :: !(StringInfoRepr si)
                  -> !(e (BaseStringType si))
                  -> !(e BaseIntegerType)
                  -> !(e BaseIntegerType)
                  -> App e (BaseStringType si)

  StringAppend :: !(StringInfoRepr si)
               -> !(SSeq.StringSeq e si)
               -> App e (BaseStringType si)

  StringLength :: !(e (BaseStringType si))
               -> App e BaseIntegerType

  ------------------------------------------------------------------------
  -- Structs

  -- A struct with its fields.
  StructCtor :: !(Ctx.Assignment BaseTypeRepr flds)
             -> !(Ctx.Assignment e flds)
             -> App e (BaseStructType flds)

  StructField :: !(e (BaseStructType flds))
              -> !(Ctx.Index flds tp)
              -> !(BaseTypeRepr tp)
              -> App e tp

------------------------------------------------------------------------
-- Types

nonceAppType :: IsExpr e => NonceApp t e tp -> BaseTypeRepr tp
nonceAppType :: NonceApp t e tp -> BaseTypeRepr tp
nonceAppType NonceApp t e tp
a =
  case NonceApp t e tp
a of
    Annotation BaseTypeRepr tp
tpr Nonce t tp
_ e tp
_ -> BaseTypeRepr tp
tpr
    Forall{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    Exists{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    ArrayFromFn   ExprSymFn t (idx ::> itp) ret
fn       -> Assignment BaseTypeRepr (idx ::> itp)
-> BaseTypeRepr ret
-> BaseTypeRepr (BaseArrayType (idx ::> itp) ret)
forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType).
Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs -> BaseTypeRepr (BaseArrayType (idx ::> tp) xs)
BaseArrayRepr (ExprSymFn t (idx ::> itp) ret
-> Assignment BaseTypeRepr (idx ::> itp)
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> Assignment BaseTypeRepr args
symFnArgTypes ExprSymFn t (idx ::> itp) ret
fn) (ExprSymFn t (idx ::> itp) ret -> BaseTypeRepr ret
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> BaseTypeRepr ret
symFnReturnType ExprSymFn t (idx ::> itp) ret
fn)
    MapOverArrays ExprSymFn t (ctx ::> d) r
fn Assignment BaseTypeRepr (idx ::> itp)
idx Assignment (ArrayResultWrapper e (idx ::> itp)) (ctx ::> d)
_ -> Assignment BaseTypeRepr (idx ::> itp)
-> BaseTypeRepr r -> BaseTypeRepr (BaseArrayType (idx ::> itp) r)
forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType).
Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs -> BaseTypeRepr (BaseArrayType (idx ::> tp) xs)
BaseArrayRepr Assignment BaseTypeRepr (idx ::> itp)
idx (ExprSymFn t (ctx ::> d) r -> BaseTypeRepr r
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> BaseTypeRepr ret
symFnReturnType ExprSymFn t (ctx ::> d) r
fn)
    ArrayTrueOnEntries ExprSymFn t (idx ::> itp) BaseBoolType
_ e (BaseArrayType (idx ::> itp) BaseBoolType)
_ -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FnApp ExprSymFn t args tp
f Assignment e args
_ ->  ExprSymFn t args tp -> BaseTypeRepr tp
forall t (args :: Ctx BaseType) (ret :: BaseType).
ExprSymFn t args ret -> BaseTypeRepr ret
symFnReturnType ExprSymFn t args tp
f

appType :: App e tp -> BaseTypeRepr tp
appType :: App e tp -> BaseTypeRepr tp
appType App e tp
a =
  case App e tp
a of
    BaseIte BaseTypeRepr tp
tp Integer
_ e BaseBoolType
_ e tp
_ e tp
_ -> BaseTypeRepr tp
tp
    BaseEq{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    NotPred{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    ConjPred{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    RealIsInteger{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BVTestBit{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BVSlt{}   -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BVUlt{}   -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    IntDiv{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IntMod{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IntAbs{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IntDivisible{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    SemiRingLe{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    SemiRingProd SemiRingProduct e sr
pd -> SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
forall (sr :: SemiRing).
SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
SR.semiRingBase (SemiRingProduct e sr -> SemiRingRepr sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
SemiRingProduct f sr -> SemiRingRepr sr
WSum.prodRepr SemiRingProduct e sr
pd)
    SemiRingSum WeightedSum e sr
s -> SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
forall (sr :: SemiRing).
SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
SR.semiRingBase (WeightedSum e sr -> SemiRingRepr sr
forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr -> SemiRingRepr sr
WSum.sumRepr WeightedSum e sr
s)

    RealDiv{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealSqrt{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    RoundReal{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RoundEvenReal{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloorReal{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    CeilReal{}  -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    App e tp
Pi -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealSin{}   -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealCos{}   -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealATan2{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealSinh{}  -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealCosh{}  -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    RealExp{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealLog{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    BVUnaryTerm UnaryBV (e BaseBoolType) n
u  -> NatRepr n -> BaseTypeRepr (BaseBVType n)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr (UnaryBV (e BaseBoolType) n -> NatRepr n
forall p (n :: Nat). UnaryBV p n -> NatRepr n
UnaryBV.width UnaryBV (e BaseBoolType) n
u)
    BVOrBits NatRepr w
w BVOrSet e w
_ -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w
    BVConcat NatRepr (u + v)
w e (BaseBVType u)
_ e (BaseBVType v)
_ -> NatRepr (u + v) -> BaseTypeRepr (BaseBVType (u + v))
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr (u + v)
w
    BVSelect NatRepr idx
_ NatRepr n
n e (BaseBVType w)
_ -> NatRepr n -> BaseTypeRepr (BaseBVType n)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr n
n
    BVUdiv NatRepr w
w e (BaseBVType w)
_ e (BaseBVType w)
_ -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w
    BVUrem NatRepr w
w e (BaseBVType w)
_ e (BaseBVType w)
_ -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w
    BVSdiv NatRepr w
w e (BaseBVType w)
_ e (BaseBVType w)
_ -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w
    BVSrem NatRepr w
w e (BaseBVType w)
_ e (BaseBVType w)
_ -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w
    BVShl  NatRepr w
w e (BaseBVType w)
_ e (BaseBVType w)
_  -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w
    BVLshr NatRepr w
w e (BaseBVType w)
_ e (BaseBVType w)
_ -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w
    BVAshr NatRepr w
w e (BaseBVType w)
_ e (BaseBVType w)
_ -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w
    BVRol NatRepr w
w e (BaseBVType w)
_ e (BaseBVType w)
_ -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w
    BVRor NatRepr w
w e (BaseBVType w)
_ e (BaseBVType w)
_ -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w
    BVPopcount NatRepr w
w e (BaseBVType w)
_ -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w
    BVCountLeadingZeros NatRepr w
w e (BaseBVType w)
_ -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w
    BVCountTrailingZeros NatRepr w
w e (BaseBVType w)
_ -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w
    BVZext  NatRepr r
w e (BaseBVType w)
_ -> NatRepr r -> BaseTypeRepr (BaseBVType r)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr r
w
    BVSext  NatRepr r
w e (BaseBVType w)
_ -> NatRepr r -> BaseTypeRepr (BaseBVType r)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr r
w
    BVFill NatRepr w
w e BaseBoolType
_ -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w

    FloatNeg FloatPrecisionRepr fpp
fpp e (BaseFloatType fpp)
_ -> FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr fpp
fpp
    FloatAbs FloatPrecisionRepr fpp
fpp e (BaseFloatType fpp)
_ -> FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr fpp
fpp
    FloatSqrt FloatPrecisionRepr fpp
fpp RoundingMode
_ e (BaseFloatType fpp)
_ -> FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr fpp
fpp
    FloatAdd FloatPrecisionRepr fpp
fpp RoundingMode
_ e (BaseFloatType fpp)
_ e (BaseFloatType fpp)
_ -> FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr fpp
fpp
    FloatSub FloatPrecisionRepr fpp
fpp RoundingMode
_ e (BaseFloatType fpp)
_ e (BaseFloatType fpp)
_ -> FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr fpp
fpp
    FloatMul FloatPrecisionRepr fpp
fpp RoundingMode
_ e (BaseFloatType fpp)
_ e (BaseFloatType fpp)
_ -> FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr fpp
fpp
    FloatDiv FloatPrecisionRepr fpp
fpp RoundingMode
_ e (BaseFloatType fpp)
_ e (BaseFloatType fpp)
_ -> FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr fpp
fpp
    FloatRem FloatPrecisionRepr fpp
fpp e (BaseFloatType fpp)
_ e (BaseFloatType fpp)
_ -> FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr fpp
fpp
    FloatFMA FloatPrecisionRepr fpp
fpp RoundingMode
_ e (BaseFloatType fpp)
_ e (BaseFloatType fpp)
_ e (BaseFloatType fpp)
_ -> FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr fpp
fpp
    FloatFpEq{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatLe{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatLt{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatIsNaN{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatIsInf{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatIsZero{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatIsPos{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatIsNeg{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatIsSubnorm{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatIsNorm{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    FloatCast FloatPrecisionRepr fpp
fpp RoundingMode
_ e (BaseFloatType fpp')
_ -> FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr fpp
fpp
    FloatRound FloatPrecisionRepr fpp
fpp RoundingMode
_ e (BaseFloatType fpp)
_ -> FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr fpp
fpp
    FloatFromBinary FloatPrecisionRepr (FloatingPointPrecision eb sb)
fpp e (BaseBVType (eb + sb))
_ -> FloatPrecisionRepr (FloatingPointPrecision eb sb)
-> BaseTypeRepr (BaseFloatType (FloatingPointPrecision eb sb))
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr (FloatingPointPrecision eb sb)
fpp
    FloatToBinary FloatPrecisionRepr (FloatingPointPrecision eb sb)
fpp e (BaseFloatType (FloatingPointPrecision eb sb))
_ -> FloatPrecisionRepr (FloatingPointPrecision eb sb)
-> BaseTypeRepr (BaseBVType (eb + sb))
forall (eb :: Nat) (sb :: Nat).
FloatPrecisionRepr (FloatingPointPrecision eb sb)
-> BaseTypeRepr (BaseBVType (eb + sb))
floatPrecisionToBVType FloatPrecisionRepr (FloatingPointPrecision eb sb)
fpp
    BVToFloat FloatPrecisionRepr fpp
fpp RoundingMode
_ e (BaseBVType w)
_ -> FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr fpp
fpp
    SBVToFloat FloatPrecisionRepr fpp
fpp RoundingMode
_ e (BaseBVType w)
_ -> FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr fpp
fpp
    RealToFloat FloatPrecisionRepr fpp
fpp RoundingMode
_ e BaseRealType
_ -> FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr (BaseFloatType fpp)
BaseFloatRepr FloatPrecisionRepr fpp
fpp
    FloatToBV NatRepr w
w RoundingMode
_ e (BaseFloatType fpp)
_ -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w
    FloatToSBV NatRepr w
w RoundingMode
_ e (BaseFloatType fpp)
_ -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w
    FloatToReal{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    ArrayMap      Assignment BaseTypeRepr (i ::> itp)
idx BaseTypeRepr tp
b ArrayUpdateMap e (i ::> itp) tp
_ e (BaseArrayType (i ::> itp) tp)
_ -> Assignment BaseTypeRepr (i ::> itp)
-> BaseTypeRepr tp -> BaseTypeRepr (BaseArrayType (i ::> itp) tp)
forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType).
Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs -> BaseTypeRepr (BaseArrayType (idx ::> tp) xs)
BaseArrayRepr Assignment BaseTypeRepr (i ::> itp)
idx BaseTypeRepr tp
b
    ConstantArray Assignment BaseTypeRepr (i ::> tp)
idx BaseTypeRepr b
b e b
_   -> Assignment BaseTypeRepr (i ::> tp)
-> BaseTypeRepr b -> BaseTypeRepr (BaseArrayType (i ::> tp) b)
forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType).
Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs -> BaseTypeRepr (BaseArrayType (idx ::> tp) xs)
BaseArrayRepr Assignment BaseTypeRepr (i ::> tp)
idx BaseTypeRepr b
b
    SelectArray BaseTypeRepr tp
b e (BaseArrayType (i ::> tp) tp)
_ Assignment e (i ::> tp)
_       -> BaseTypeRepr tp
b
    UpdateArray BaseTypeRepr b
b Assignment BaseTypeRepr (i ::> tp)
itp e (BaseArrayType (i ::> tp) b)
_ Assignment e (i ::> tp)
_ e b
_     -> Assignment BaseTypeRepr (i ::> tp)
-> BaseTypeRepr b -> BaseTypeRepr (BaseArrayType (i ::> tp) b)
forall (idx :: Ctx BaseType) (tp :: BaseType) (xs :: BaseType).
Assignment BaseTypeRepr (idx ::> tp)
-> BaseTypeRepr xs -> BaseTypeRepr (BaseArrayType (idx ::> tp) xs)
BaseArrayRepr Assignment BaseTypeRepr (i ::> tp)
itp BaseTypeRepr b
b

    IntegerToReal{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    BVToInteger{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    SBVToInteger{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    IntegerToBV e BaseIntegerType
_ NatRepr w
w -> NatRepr w -> BaseTypeRepr (BaseBVType w)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
BaseBVRepr NatRepr w
w

    RealToInteger{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    Cplx{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    RealPart{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    ImagPart{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    StringContains{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    StringIsPrefixOf{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    StringIsSuffixOf{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    StringIndexOf{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    StringSubstring StringInfoRepr si
si e (BaseStringType si)
_ e BaseIntegerType
_ e BaseIntegerType
_ -> StringInfoRepr si -> BaseTypeRepr (BaseStringType si)
forall (si :: StringInfo).
StringInfoRepr si -> BaseTypeRepr (BaseStringType si)
BaseStringRepr StringInfoRepr si
si
    StringAppend StringInfoRepr si
si StringSeq e si
_ -> StringInfoRepr si -> BaseTypeRepr (BaseStringType si)
forall (si :: StringInfo).
StringInfoRepr si -> BaseTypeRepr (BaseStringType si)
BaseStringRepr StringInfoRepr si
si
    StringLength{} -> BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

    StructCtor Assignment BaseTypeRepr flds
flds Assignment e flds
_     -> Assignment BaseTypeRepr flds -> BaseTypeRepr (BaseStructType flds)
forall (ctx :: Ctx BaseType).
Assignment BaseTypeRepr ctx -> BaseTypeRepr (BaseStructType ctx)
BaseStructRepr Assignment BaseTypeRepr flds
flds
    StructField e (BaseStructType flds)
_ Index flds tp
_ BaseTypeRepr tp
tp    -> BaseTypeRepr tp
tp


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