    -- |
    -- Module      :  Cryptol.Symbolic
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE ImplicitParams #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE RecordWildCards #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TupleSections #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE ViewPatterns #-}

    module Cryptol.Symbolic
     ( ProverCommand(..)
     , QueryType(..)
     , SatNum(..)
     , ProverResult(..)
     , ProverStats
     , CounterExampleType(..)
       -- * FinType
     , FinType(..)
     , finType
     , unFinType
     , predArgTypes
       -- * VarShape
     , VarShape(..)
     , varShapeToValue
     , freshVar
     , computeModel
     , FreshVarFns(..)
     , modelPred
     , varModelPred
     , varToExpr
     , flattenShape
     , flattenShapes
     ) where

    import Control.Monad (foldM)
    import Data.IORef(IORef)
    import Data.List (genericReplicate)
    import Data.Ratio
    import qualified LibBF as FP

    import           Cryptol.Backend
    import           Cryptol.Backend.FloatHelpers(bfValue)
    import           Cryptol.Backend.SeqMap (finiteSeqMap)
    import           Cryptol.Backend.WordValue (wordVal)

    import qualified Cryptol.Eval.Concrete as Concrete
    import           Cryptol.Eval.Value
    import           Cryptol.TypeCheck.AST
    import           Cryptol.TypeCheck.Solver.InfNat
    import           Cryptol.Eval.Type (TValue(..), evalType,tValTy,tNumValTy)
    import           Cryptol.Utils.Ident (Ident,prelPrim,floatPrim)
    import           Cryptol.Utils.RecordMap
    import           Cryptol.Utils.Panic
    import           Cryptol.Utils.PP

    import Prelude ()
    import Prelude.Compat
    import Data.Time (NominalDiffTime)

    type SatResult = [(TValue, Expr, Concrete.Value)]

    data SatNum = AllSat | SomeSat Int
      deriving (Int -> SatNum -> ShowS
    [SatNum] -> ShowS
    SatNum -> [Char]
    (Int -> SatNum -> ShowS)
    -> (SatNum -> [Char]) -> ([SatNum] -> ShowS) -> Show SatNum
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> SatNum -> ShowS
    showsPrec :: Int -> SatNum -> ShowS
    $cshow :: SatNum -> [Char]
    show :: SatNum -> [Char]
    $cshowList :: [SatNum] -> ShowS
    showList :: [SatNum] -> ShowS
    Show)

    data QueryType = SatQuery SatNum | ProveQuery | SafetyQuery
      deriving (Int -> QueryType -> ShowS
    [QueryType] -> ShowS
    QueryType -> [Char]
    (Int -> QueryType -> ShowS)
    -> (QueryType -> [Char])
    -> ([QueryType] -> ShowS)
    -> Show QueryType
    forall a.
    (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> QueryType -> ShowS
    showsPrec :: Int -> QueryType -> ShowS
    $cshow :: QueryType -> [Char]
    show :: QueryType -> [Char]
    $cshowList :: [QueryType] -> ShowS
    showList :: [QueryType] -> ShowS
    Show)

    data ProverCommand = ProverCommand {
        ProverCommand -> QueryType
    pcQueryType :: QueryType
        -- ^ The type of query to run
      , ProverCommand -> [Char]
    pcProverName :: String
        -- ^ Which prover to use (one of the strings in 'proverConfigs')
      , ProverCommand -> Bool
    pcVerbose :: Bool
        -- ^ Verbosity flag passed to SBV
      , ProverCommand -> Bool
    pcValidate :: Bool
        -- ^ Model validation flag passed to SBV
      , ProverCommand -> IORef ProverStats
    pcProverStats :: !(IORef ProverStats)
        -- ^ Record timing information here
      , ProverCommand -> [DeclGroup]
    pcExtraDecls :: [DeclGroup]
        -- ^ Extra declarations to bring into scope for symbolic
        -- simulation
      , ProverCommand -> Maybe [Char]
    pcSmtFile :: Maybe FilePath
        -- ^ Optionally output the SMTLIB query to a file
      , ProverCommand -> Expr
    pcExpr :: Expr
        -- ^ The typechecked expression to evaluate
      , ProverCommand -> Schema
    pcSchema :: Schema
        -- ^ The 'Schema' of @pcExpr@
      , ProverCommand -> Bool
    pcIgnoreSafety :: Bool
        -- ^ Should we ignore safety predicates?
      }

    type ProverStats = NominalDiffTime

    -- | A @:prove@ command can fail either because some
    --   input causes the predicate to violate a safety assertion,
    --   or because the predicate returns false for some input.
    data CounterExampleType = SafetyViolation | PredicateFalsified

    -- | A prover result is either an error message, an empty result (eg
    -- for the offline prover), a counterexample or a lazy list of
    -- satisfying assignments.
    data ProverResult = AllSatResult [SatResult] -- LAZY
                      | ThmResult    [TValue]
                      | CounterExample CounterExampleType SatResult
                      | EmptyResult
                      | ProverError  String

    predArgTypes :: QueryType -> Schema -> Either String [FinType]
    predArgTypes :: QueryType -> Schema -> Either [Char] [FinType]
    predArgTypes QueryType
    qtype schema :: Schema
    schema@(Forall [TParam]
    ts [Prop]
    ps Prop
    ty)
      | [TParam] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [TParam]
    ts Bool -> Bool -> Bool
    && [Prop] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Prop]
    ps =
          case TValue -> Maybe [FinType]
    go (TValue -> Maybe [FinType])
    -> Either Nat' TValue -> Either Nat' (Maybe [FinType])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TypeEnv -> Prop -> Either Nat' TValue
    evalType TypeEnv
    forall a. Monoid a => a
    mempty Prop
    ty) of
            Right (Just [FinType]
    fts) -> [FinType] -> Either [Char] [FinType]
    forall a b. b -> Either a b
    Right [FinType]
    fts
            Either Nat' (Maybe [FinType])
    _ | QueryType
    SafetyQuery <- QueryType
    qtype -> [Char] -> Either [Char] [FinType]
    forall a b. a -> Either a b
    Left ([Char] -> Either [Char] [FinType])
    -> [Char] -> Either [Char] [FinType]
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Expected finite result type:\n" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Doc -> [Char]
    forall a. Show a => a -> [Char]
    show (Schema -> Doc
    forall a. PP a => a -> Doc
    pp Schema
    schema)
              | Bool
    otherwise -> [Char] -> Either [Char] [FinType]
    forall a b. a -> Either a b
    Left ([Char] -> Either [Char] [FinType])
    -> [Char] -> Either [Char] [FinType]
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Not a valid predicate type:\n" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Doc -> [Char]
    forall a. Show a => a -> [Char]
    show (Schema -> Doc
    forall a. PP a => a -> Doc
    pp Schema
    schema)
      | Bool
    otherwise = [Char] -> Either [Char] [FinType]
    forall a b. a -> Either a b
    Left ([Char] -> Either [Char] [FinType])
    -> [Char] -> Either [Char] [FinType]
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Not a monomorphic type:\n" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Doc -> [Char]
    forall a. Show a => a -> [Char]
    show (Schema -> Doc
    forall a. PP a => a -> Doc
    pp Schema
    schema)
      where
        go :: TValue -> Maybe [FinType]
        go :: TValue -> Maybe [FinType]
    go TValue
    TVBit             = [FinType] -> Maybe [FinType]
    forall a. a -> Maybe a
    Just []
        go (TVFun TValue
    ty1 TValue
    ty2)   = (:) (FinType -> [FinType] -> [FinType])
    -> Maybe FinType -> Maybe ([FinType] -> [FinType])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TValue -> Maybe FinType
    finType TValue
    ty1 Maybe ([FinType] -> [FinType])
    -> Maybe [FinType] -> Maybe [FinType]
    forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TValue -> Maybe [FinType]
    go TValue
    ty2
        go TValue
    tv
          | Just FinType
    _ <- TValue -> Maybe FinType
    finType TValue
    tv
          , QueryType
    SafetyQuery <- QueryType
    qtype
          = [FinType] -> Maybe [FinType]
    forall a. a -> Maybe a
    Just []

          | Bool
    otherwise
          = Maybe [FinType]
    forall a. Maybe a
    Nothing

    data FinType
        = FTBit
        | FTInteger
        | FTIntMod Integer
        | FTRational
        | FTFloat Integer Integer
        | FTSeq Integer FinType
        | FTTuple [FinType]
        | FTRecord (RecordMap Ident FinType)
        | FTNewtype Newtype [Either Nat' TValue] (RecordMap Ident FinType)

    finType :: TValue -> Maybe FinType
    finType :: TValue -> Maybe FinType
    finType TValue
    ty =
      case TValue
    ty of
        TValue
    TVBit               -> FinType -> Maybe FinType
    forall a. a -> Maybe a
    Just FinType
    FTBit
        TValue
    TVInteger           -> FinType -> Maybe FinType
    forall a. a -> Maybe a
    Just FinType
    FTInteger
        TVIntMod Integer
    n          -> FinType -> Maybe FinType
    forall a. a -> Maybe a
    Just (Integer -> FinType
    FTIntMod Integer
    n)
        TValue
    TVRational          -> FinType -> Maybe FinType
    forall a. a -> Maybe a
    Just FinType
    FTRational
        TVFloat Integer
    e Integer
    p         -> FinType -> Maybe FinType
    forall a. a -> Maybe a
    Just (Integer -> Integer -> FinType
    FTFloat Integer
    e Integer
    p)
        TVSeq Integer
    n TValue
    t           -> Integer -> FinType -> FinType
    FTSeq Integer
    n (FinType -> FinType) -> Maybe FinType -> Maybe FinType
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TValue -> Maybe FinType
    finType TValue
    t
        TVTuple [TValue]
    ts          -> [FinType] -> FinType
    FTTuple ([FinType] -> FinType) -> Maybe [FinType] -> Maybe FinType
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TValue -> Maybe FinType) -> [TValue] -> Maybe [FinType]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse TValue -> Maybe FinType
    finType [TValue]
    ts
        TVRec RecordMap Ident TValue
    fields        -> RecordMap Ident FinType -> FinType
    FTRecord (RecordMap Ident FinType -> FinType)
    -> Maybe (RecordMap Ident FinType) -> Maybe FinType
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TValue -> Maybe FinType)
    -> RecordMap Ident TValue -> Maybe (RecordMap Ident FinType)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
    traverse TValue -> Maybe FinType
    finType RecordMap Ident TValue
    fields
        TVNewtype Newtype
    u [Either Nat' TValue]
    ts RecordMap Ident TValue
    body -> Newtype
    -> [Either Nat' TValue] -> RecordMap Ident FinType -> FinType
    FTNewtype Newtype
    u [Either Nat' TValue]
    ts (RecordMap Ident FinType -> FinType)
    -> Maybe (RecordMap Ident FinType) -> Maybe FinType
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TValue -> Maybe FinType)
    -> RecordMap Ident TValue -> Maybe (RecordMap Ident FinType)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
    traverse TValue -> Maybe FinType
    finType RecordMap Ident TValue
    body
        TVAbstract {}       -> Maybe FinType
    forall a. Maybe a
    Nothing
        TVArray{}           -> Maybe FinType
    forall a. Maybe a
    Nothing
        TVStream{}          -> Maybe FinType
    forall a. Maybe a
    Nothing
        TVFun{}             -> Maybe FinType
    forall a. Maybe a
    Nothing

    finTypeToType :: FinType -> Type
    finTypeToType :: FinType -> Prop
    finTypeToType FinType
    fty =
      case FinType
    fty of
        FinType
    FTBit             -> Prop
    tBit
        FinType
    FTInteger         -> Prop
    tInteger
        FTIntMod Integer
    n        -> Prop -> Prop
    tIntMod (Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum Integer
    n)
        FinType
    FTRational        -> Prop
    tRational
        FTFloat Integer
    e Integer
    p       -> Prop -> Prop -> Prop
    tFloat (Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum Integer
    e) (Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum Integer
    p)
        FTSeq Integer
    l FinType
    ety       -> Prop -> Prop -> Prop
    tSeq (Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum Integer
    l) (FinType -> Prop
    finTypeToType FinType
    ety)
        FTTuple [FinType]
    ftys      -> [Prop] -> Prop
    tTuple (FinType -> Prop
    finTypeToType (FinType -> Prop) -> [FinType] -> [Prop]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [FinType]
    ftys)
        FTRecord RecordMap Ident FinType
    fs       -> RecordMap Ident Prop -> Prop
    tRec (FinType -> Prop
    finTypeToType (FinType -> Prop)
    -> RecordMap Ident FinType -> RecordMap Ident Prop
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> RecordMap Ident FinType
    fs)
        FTNewtype Newtype
    u [Either Nat' TValue]
    ts RecordMap Ident FinType
    _  -> Newtype -> [Prop] -> Prop
    tNewtype Newtype
    u ((Either Nat' TValue -> Prop) -> [Either Nat' TValue] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map Either Nat' TValue -> Prop
    unArg [Either Nat' TValue]
    ts)
     where
      unArg :: Either Nat' TValue -> Prop
    unArg (Left Nat'
    Inf)     = Prop
    tInf
      unArg (Left (Nat Integer
    n)) = Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum Integer
    n
      unArg (Right TValue
    t)      = TValue -> Prop
    tValTy TValue
    t

    unFinType :: FinType -> TValue
    unFinType :: FinType -> TValue
    unFinType FinType
    fty =
      case FinType
    fty of
        FinType
    FTBit             -> TValue
    TVBit
        FinType
    FTInteger         -> TValue
    TVInteger
        FTIntMod Integer
    n        -> Integer -> TValue
    TVIntMod Integer
    n
        FinType
    FTRational        -> TValue
    TVRational
        FTFloat Integer
    e Integer
    p       -> Integer -> Integer -> TValue
    TVFloat Integer
    e Integer
    p
        FTSeq Integer
    n FinType
    ety       -> Integer -> TValue -> TValue
    TVSeq Integer
    n (FinType -> TValue
    unFinType FinType
    ety)
        FTTuple [FinType]
    ftys      -> [TValue] -> TValue
    TVTuple (FinType -> TValue
    unFinType (FinType -> TValue) -> [FinType] -> [TValue]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [FinType]
    ftys)
        FTRecord RecordMap Ident FinType
    fs       -> RecordMap Ident TValue -> TValue
    TVRec   (FinType -> TValue
    unFinType (FinType -> TValue)
    -> RecordMap Ident FinType -> RecordMap Ident TValue
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> RecordMap Ident FinType
    fs)
        FTNewtype Newtype
    u [Either Nat' TValue]
    ts RecordMap Ident FinType
    fs -> Newtype -> [Either Nat' TValue] -> RecordMap Ident TValue -> TValue
    TVNewtype Newtype
    u [Either Nat' TValue]
    ts (FinType -> TValue
    unFinType (FinType -> TValue)
    -> RecordMap Ident FinType -> RecordMap Ident TValue
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> RecordMap Ident FinType
    fs)

    data VarShape sym
      = VarBit (SBit sym)
      | VarInteger (SInteger sym)
      | VarRational (SInteger sym) (SInteger sym)
      | VarFloat (SFloat sym)
      | VarWord (SWord sym)
      | VarFinSeq Integer [VarShape sym]
      | VarTuple [VarShape sym]
      | VarRecord (RecordMap Ident (VarShape sym))

    ppVarShape :: Backend sym => sym -> VarShape sym -> Doc
    ppVarShape :: forall sym. Backend sym => sym -> VarShape sym -> Doc
    ppVarShape sym
    _sym (VarBit SBit sym
    _b) = [Char] -> Doc
    text [Char]
    "<bit>"
    ppVarShape sym
    _sym (VarInteger SInteger sym
    _i) = [Char] -> Doc
    text [Char]
    "<integer>"
    ppVarShape sym
    _sym (VarFloat SFloat sym
    _f) = [Char] -> Doc
    text [Char]
    "<float>"
    ppVarShape sym
    _sym (VarRational SInteger sym
    _n SInteger sym
    _d) = [Char] -> Doc
    text [Char]
    "<rational>"
    ppVarShape sym
    sym (VarWord SWord sym
    w) = [Char] -> Doc
    text [Char]
    "<word:" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Integer -> Doc
    integer (sym -> SWord sym -> Integer
    forall sym. Backend sym => sym -> SWord sym -> Integer
    wordLen sym
    sym SWord sym
    w) Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> [Char] -> Doc
    text [Char]
    ">"
    ppVarShape sym
    sym (VarFinSeq Integer
    _ [VarShape sym]
    xs) =
      [Doc] -> Doc
    ppList ((VarShape sym -> Doc) -> [VarShape sym] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (sym -> VarShape sym -> Doc
    forall sym. Backend sym => sym -> VarShape sym -> Doc
    ppVarShape sym
    sym) [VarShape sym]
    xs)
    ppVarShape sym
    sym (VarTuple [VarShape sym]
    xs) =
      [Doc] -> Doc
    ppTuple ((VarShape sym -> Doc) -> [VarShape sym] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (sym -> VarShape sym -> Doc
    forall sym. Backend sym => sym -> VarShape sym -> Doc
    ppVarShape sym
    sym) [VarShape sym]
    xs)
    ppVarShape sym
    sym (VarRecord RecordMap Ident (VarShape sym)
    fs) =
      [Doc] -> Doc
    ppRecord (((Ident, VarShape sym) -> Doc) -> [(Ident, VarShape sym)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Ident, VarShape sym) -> Doc
    forall {a}. PP a => (a, VarShape sym) -> Doc
    ppField (RecordMap Ident (VarShape sym) -> [(Ident, VarShape sym)]
    forall a b. (Show a, Ord a) => RecordMap a b -> [(a, b)]
    displayFields RecordMap Ident (VarShape sym)
    fs))
     where
      ppField :: (a, VarShape sym) -> Doc
    ppField (a
    f,VarShape sym
    v) = a -> Doc
    forall a. PP a => a -> Doc
    pp a
    f Doc -> Doc -> Doc
    <+> Char -> Doc
    char Char
    '=' Doc -> Doc -> Doc
    <+> sym -> VarShape sym -> Doc
    forall sym. Backend sym => sym -> VarShape sym -> Doc
    ppVarShape sym
    sym VarShape sym
    v

    -- | Flatten structured shapes (like tuples and sequences), leaving only
    --   a sequence of variable shapes of base type.
    flattenShapes :: [VarShape sym] -> [VarShape sym] -> [VarShape sym]
    flattenShapes :: forall sym. [VarShape sym] -> [VarShape sym] -> [VarShape sym]
    flattenShapes []     [VarShape sym]
    tl = [VarShape sym]
    tl
    flattenShapes (VarShape sym
    x:[VarShape sym]
    xs) [VarShape sym]
    tl = VarShape sym -> [VarShape sym] -> [VarShape sym]
    forall sym. VarShape sym -> [VarShape sym] -> [VarShape sym]
    flattenShape VarShape sym
    x ([VarShape sym] -> [VarShape sym] -> [VarShape sym]
    forall sym. [VarShape sym] -> [VarShape sym] -> [VarShape sym]
    flattenShapes [VarShape sym]
    xs [VarShape sym]
    tl)

    flattenShape :: VarShape sym -> [VarShape sym] -> [VarShape sym]
    flattenShape :: forall sym. VarShape sym -> [VarShape sym] -> [VarShape sym]
    flattenShape VarShape sym
    x [VarShape sym]
    tl =
      case VarShape sym
    x of
        VarBit{}       -> VarShape sym
    x VarShape sym -> [VarShape sym] -> [VarShape sym]
    forall a. a -> [a] -> [a]
    : [VarShape sym]
    tl
        VarInteger{}   -> VarShape sym
    x VarShape sym -> [VarShape sym] -> [VarShape sym]
    forall a. a -> [a] -> [a]
    : [VarShape sym]
    tl
        VarRational{}  -> VarShape sym
    x VarShape sym -> [VarShape sym] -> [VarShape sym]
    forall a. a -> [a] -> [a]
    : [VarShape sym]
    tl
        VarWord{}      -> VarShape sym
    x VarShape sym -> [VarShape sym] -> [VarShape sym]
    forall a. a -> [a] -> [a]
    : [VarShape sym]
    tl
        VarFloat{}     -> VarShape sym
    x VarShape sym -> [VarShape sym] -> [VarShape sym]
    forall a. a -> [a] -> [a]
    : [VarShape sym]
    tl
        VarFinSeq Integer
    _ [VarShape sym]
    vs -> [VarShape sym] -> [VarShape sym] -> [VarShape sym]
    forall sym. [VarShape sym] -> [VarShape sym] -> [VarShape sym]
    flattenShapes [VarShape sym]
    vs [VarShape sym]
    tl
        VarTuple [VarShape sym]
    vs    -> [VarShape sym] -> [VarShape sym] -> [VarShape sym]
    forall sym. [VarShape sym] -> [VarShape sym] -> [VarShape sym]
    flattenShapes [VarShape sym]
    vs [VarShape sym]
    tl
        VarRecord RecordMap Ident (VarShape sym)
    fs   -> [VarShape sym] -> [VarShape sym] -> [VarShape sym]
    forall sym. [VarShape sym] -> [VarShape sym] -> [VarShape sym]
    flattenShapes (RecordMap Ident (VarShape sym) -> [VarShape sym]
    forall a b. RecordMap a b -> [b]
    recordElements RecordMap Ident (VarShape sym)
    fs) [VarShape sym]
    tl

    varShapeToValue :: Backend sym => sym -> VarShape sym -> GenValue sym
    varShapeToValue :: forall sym. Backend sym => sym -> VarShape sym -> GenValue sym
    varShapeToValue sym
    sym VarShape sym
    var =
      case VarShape sym
    var of
        VarBit SBit sym
    b     -> SBit sym -> GenValue sym
    forall sym. SBit sym -> GenValue sym
    VBit SBit sym
    b
        VarInteger SInteger sym
    i -> SInteger sym -> GenValue sym
    forall sym. SInteger sym -> GenValue sym
    VInteger SInteger sym
    i
        VarRational SInteger sym
    n SInteger sym
    d -> SRational sym -> GenValue sym
    forall sym. SRational sym -> GenValue sym
    VRational (SInteger sym -> SInteger sym -> SRational sym
    forall sym. SInteger sym -> SInteger sym -> SRational sym
    SRational SInteger sym
    n SInteger sym
    d)
        VarWord SWord sym
    w    -> Integer -> WordValue sym -> GenValue sym
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord (sym -> SWord sym -> Integer
    forall sym. Backend sym => sym -> SWord sym -> Integer
    wordLen sym
    sym SWord sym
    w) (SWord sym -> WordValue sym
    forall sym. SWord sym -> WordValue sym
    wordVal SWord sym
    w)
        VarFloat SFloat sym
    f   -> SFloat sym -> GenValue sym
    forall sym. SFloat sym -> GenValue sym
    VFloat SFloat sym
    f
        VarFinSeq Integer
    n [VarShape sym]
    vs -> Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    VSeq Integer
    n (sym -> [SEval sym (GenValue sym)] -> SeqMap sym (GenValue sym)
    forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
    finiteSeqMap sym
    sym ((VarShape sym -> SEval sym (GenValue sym))
    -> [VarShape sym] -> [SEval sym (GenValue sym)]
    forall a b. (a -> b) -> [a] -> [b]
    map (GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (GenValue sym -> SEval sym (GenValue sym))
    -> (VarShape sym -> GenValue sym)
    -> VarShape sym
    -> SEval sym (GenValue sym)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . sym -> VarShape sym -> GenValue sym
    forall sym. Backend sym => sym -> VarShape sym -> GenValue sym
    varShapeToValue sym
    sym) [VarShape sym]
    vs))
        VarTuple [VarShape sym]
    vs  -> [SEval sym (GenValue sym)] -> GenValue sym
    forall sym. [SEval sym (GenValue sym)] -> GenValue sym
    VTuple ((VarShape sym -> SEval sym (GenValue sym))
    -> [VarShape sym] -> [SEval sym (GenValue sym)]
    forall a b. (a -> b) -> [a] -> [b]
    map (GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (GenValue sym -> SEval sym (GenValue sym))
    -> (VarShape sym -> GenValue sym)
    -> VarShape sym
    -> SEval sym (GenValue sym)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . sym -> VarShape sym -> GenValue sym
    forall sym. Backend sym => sym -> VarShape sym -> GenValue sym
    varShapeToValue sym
    sym) [VarShape sym]
    vs)
        VarRecord RecordMap Ident (VarShape sym)
    fs -> RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
    forall sym.
    RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
    VRecord ((VarShape sym -> SEval sym (GenValue sym))
    -> RecordMap Ident (VarShape sym)
    -> RecordMap Ident (SEval sym (GenValue sym))
    forall a b. (a -> b) -> RecordMap Ident a -> RecordMap Ident b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (GenValue sym -> SEval sym (GenValue sym)
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (GenValue sym -> SEval sym (GenValue sym))
    -> (VarShape sym -> GenValue sym)
    -> VarShape sym
    -> SEval sym (GenValue sym)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . sym -> VarShape sym -> GenValue sym
    forall sym. Backend sym => sym -> VarShape sym -> GenValue sym
    varShapeToValue sym
    sym) RecordMap Ident (VarShape sym)
    fs)

    data FreshVarFns sym =
      FreshVarFns
      { forall sym. FreshVarFns sym -> IO (SBit sym)
    freshBitVar     :: IO (SBit sym)
      , forall sym. FreshVarFns sym -> Integer -> IO (SWord sym)
    freshWordVar    :: Integer -> IO (SWord sym)
      , forall sym.
    FreshVarFns sym
    -> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
    freshIntegerVar :: Maybe Integer -> Maybe Integer -> IO (SInteger sym)
      , forall sym.
    FreshVarFns sym -> Integer -> Integer -> IO (SFloat sym)
    freshFloatVar   :: Integer -> Integer -> IO (SFloat sym)
      }

    freshVar :: Backend sym => FreshVarFns sym -> FinType -> IO (VarShape sym)
    freshVar :: forall sym.
    Backend sym =>
    FreshVarFns sym -> FinType -> IO (VarShape sym)
    freshVar FreshVarFns sym
    fns FinType
    tp =
      case FinType
    tp of
        FinType
    FTBit         -> SBit sym -> VarShape sym
    forall sym. SBit sym -> VarShape sym
    VarBit      (SBit sym -> VarShape sym) -> IO (SBit sym) -> IO (VarShape sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> FreshVarFns sym -> IO (SBit sym)
    forall sym. FreshVarFns sym -> IO (SBit sym)
    freshBitVar FreshVarFns sym
    fns
        FinType
    FTInteger     -> SInteger sym -> VarShape sym
    forall sym. SInteger sym -> VarShape sym
    VarInteger  (SInteger sym -> VarShape sym)
    -> IO (SInteger sym) -> IO (VarShape sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> FreshVarFns sym
    -> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
    forall sym.
    FreshVarFns sym
    -> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
    freshIntegerVar FreshVarFns sym
    fns Maybe Integer
    forall a. Maybe a
    Nothing Maybe Integer
    forall a. Maybe a
    Nothing
        FinType
    FTRational    -> SInteger sym -> SInteger sym -> VarShape sym
    forall sym. SInteger sym -> SInteger sym -> VarShape sym
    VarRational
                            (SInteger sym -> SInteger sym -> VarShape sym)
    -> IO (SInteger sym) -> IO (SInteger sym -> VarShape sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> FreshVarFns sym
    -> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
    forall sym.
    FreshVarFns sym
    -> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
    freshIntegerVar FreshVarFns sym
    fns Maybe Integer
    forall a. Maybe a
    Nothing Maybe Integer
    forall a. Maybe a
    Nothing
                            IO (SInteger sym -> VarShape sym)
    -> IO (SInteger sym) -> IO (VarShape sym)
    forall a b. IO (a -> b) -> IO a -> IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> FreshVarFns sym
    -> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
    forall sym.
    FreshVarFns sym
    -> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
    freshIntegerVar FreshVarFns sym
    fns (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    1) Maybe Integer
    forall a. Maybe a
    Nothing
        FTIntMod Integer
    0    -> [Char] -> [[Char]] -> IO (VarShape sym)
    forall a. HasCallStack => [Char] -> [[Char]] -> a
    panic [Char]
    "freshVariable" [[Char]
    "0 modulus not allowed"]
        FTIntMod Integer
    m    -> SInteger sym -> VarShape sym
    forall sym. SInteger sym -> VarShape sym
    VarInteger  (SInteger sym -> VarShape sym)
    -> IO (SInteger sym) -> IO (VarShape sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> FreshVarFns sym
    -> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
    forall sym.
    FreshVarFns sym
    -> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
    freshIntegerVar FreshVarFns sym
    fns (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    0) (Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just (Integer
    mInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1))
        FTFloat Integer
    e Integer
    p   -> SFloat sym -> VarShape sym
    forall sym. SFloat sym -> VarShape sym
    VarFloat    (SFloat sym -> VarShape sym)
    -> IO (SFloat sym) -> IO (VarShape sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> FreshVarFns sym -> Integer -> Integer -> IO (SFloat sym)
    forall sym.
    FreshVarFns sym -> Integer -> Integer -> IO (SFloat sym)
    freshFloatVar FreshVarFns sym
    fns Integer
    e Integer
    p
        FTSeq Integer
    n FinType
    FTBit -> SWord sym -> VarShape sym
    forall sym. SWord sym -> VarShape sym
    VarWord     (SWord sym -> VarShape sym) -> IO (SWord sym) -> IO (VarShape sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> FreshVarFns sym -> Integer -> IO (SWord sym)
    forall sym. FreshVarFns sym -> Integer -> IO (SWord sym)
    freshWordVar FreshVarFns sym
    fns (Integer -> Integer
    forall a. Integral a => a -> Integer
    toInteger Integer
    n)
        FTSeq Integer
    n FinType
    t     -> Integer -> [VarShape sym] -> VarShape sym
    forall sym. Integer -> [VarShape sym] -> VarShape sym
    VarFinSeq (Integer -> Integer
    forall a. Integral a => a -> Integer
    toInteger Integer
    n) ([VarShape sym] -> VarShape sym)
    -> IO [VarShape sym] -> IO (VarShape sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [IO (VarShape sym)] -> IO [VarShape sym]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence (Integer -> IO (VarShape sym) -> [IO (VarShape sym)]
    forall i a. Integral i => i -> a -> [a]
    genericReplicate Integer
    n (FreshVarFns sym -> FinType -> IO (VarShape sym)
    forall sym.
    Backend sym =>
    FreshVarFns sym -> FinType -> IO (VarShape sym)
    freshVar FreshVarFns sym
    fns FinType
    t))
        FTTuple [FinType]
    ts    -> [VarShape sym] -> VarShape sym
    forall sym. [VarShape sym] -> VarShape sym
    VarTuple    ([VarShape sym] -> VarShape sym)
    -> IO [VarShape sym] -> IO (VarShape sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (FinType -> IO (VarShape sym)) -> [FinType] -> IO [VarShape sym]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (FreshVarFns sym -> FinType -> IO (VarShape sym)
    forall sym.
    Backend sym =>
    FreshVarFns sym -> FinType -> IO (VarShape sym)
    freshVar FreshVarFns sym
    fns) [FinType]
    ts
        FTRecord RecordMap Ident FinType
    fs   -> RecordMap Ident (VarShape sym) -> VarShape sym
    forall sym. RecordMap Ident (VarShape sym) -> VarShape sym
    VarRecord   (RecordMap Ident (VarShape sym) -> VarShape sym)
    -> IO (RecordMap Ident (VarShape sym)) -> IO (VarShape sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (FinType -> IO (VarShape sym))
    -> RecordMap Ident FinType -> IO (RecordMap Ident (VarShape sym))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
    traverse (FreshVarFns sym -> FinType -> IO (VarShape sym)
    forall sym.
    Backend sym =>
    FreshVarFns sym -> FinType -> IO (VarShape sym)
    freshVar FreshVarFns sym
    fns) RecordMap Ident FinType
    fs
        FTNewtype Newtype
    _ [Either Nat' TValue]
    _ RecordMap Ident FinType
    fs -> RecordMap Ident (VarShape sym) -> VarShape sym
    forall sym. RecordMap Ident (VarShape sym) -> VarShape sym
    VarRecord (RecordMap Ident (VarShape sym) -> VarShape sym)
    -> IO (RecordMap Ident (VarShape sym)) -> IO (VarShape sym)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (FinType -> IO (VarShape sym))
    -> RecordMap Ident FinType -> IO (RecordMap Ident (VarShape sym))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
    traverse (FreshVarFns sym -> FinType -> IO (VarShape sym)
    forall sym.
    Backend sym =>
    FreshVarFns sym -> FinType -> IO (VarShape sym)
    freshVar FreshVarFns sym
    fns) RecordMap Ident FinType
    fs

    computeModel ::
      PrimMap ->
      [FinType] ->
      [VarShape Concrete.Concrete] ->
      [(TValue, Expr, Concrete.Value)]
    computeModel :: PrimMap
    -> [FinType] -> [VarShape Concrete] -> [(TValue, Expr, Value)]
    computeModel PrimMap
    _ [] [] = []
    computeModel PrimMap
    primMap (FinType
    t:[FinType]
    ts) (VarShape Concrete
    v:[VarShape Concrete]
    vs) =
      do let v' :: Value
    v' = Concrete -> VarShape Concrete -> Value
    forall sym. Backend sym => sym -> VarShape sym -> GenValue sym
    varShapeToValue Concrete
    Concrete.Concrete VarShape Concrete
    v
         let t' :: TValue
    t' = FinType -> TValue
    unFinType FinType
    t
         let e :: Expr
    e  = PrimMap -> FinType -> VarShape Concrete -> Expr
    varToExpr PrimMap
    primMap FinType
    t VarShape Concrete
    v
         let zs :: [(TValue, Expr, Value)]
    zs = PrimMap
    -> [FinType] -> [VarShape Concrete] -> [(TValue, Expr, Value)]
    computeModel PrimMap
    primMap [FinType]
    ts [VarShape Concrete]
    vs
          in ((TValue
    t',Expr
    e,Value
    v')(TValue, Expr, Value)
    -> [(TValue, Expr, Value)] -> [(TValue, Expr, Value)]
    forall a. a -> [a] -> [a]
    :[(TValue, Expr, Value)]
    zs)
    computeModel PrimMap
    _ [FinType]
    _ [VarShape Concrete]
    _ = [Char] -> [[Char]] -> [(TValue, Expr, Value)]
    forall a. HasCallStack => [Char] -> [[Char]] -> a
    panic [Char]
    "computeModel" [[Char]
    "type/value list mismatch"]

    modelPred  ::
      Backend sym =>
      sym ->
      [VarShape sym] ->
      [VarShape Concrete.Concrete] ->
      SEval sym (SBit sym)
    modelPred :: forall sym.
    Backend sym =>
    sym
    -> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym)
    modelPred sym
    sym [VarShape sym]
    vs [VarShape Concrete]
    xs =
      do [SBit sym]
    ps <- ((VarShape sym, VarShape Concrete) -> SEval sym (SBit sym))
    -> [(VarShape sym, VarShape Concrete)] -> SEval sym [SBit sym]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (sym -> (VarShape sym, VarShape Concrete) -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> (VarShape sym, VarShape Concrete) -> SEval sym (SBit sym)
    varModelPred sym
    sym) ([VarShape sym]
    -> [VarShape Concrete] -> [(VarShape sym, VarShape Concrete)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [VarShape sym]
    vs [VarShape Concrete]
    xs)
         (SBit sym -> SBit sym -> SEval sym (SBit sym))
    -> SBit sym -> [SBit sym] -> SEval sym (SBit sym)
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM (sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
    bitAnd sym
    sym) (sym -> Bool -> SBit sym
    forall sym. Backend sym => sym -> Bool -> SBit sym
    bitLit sym
    sym Bool
    True) [SBit sym]
    ps

    varModelPred ::
      Backend sym =>
      sym ->
      (VarShape sym, VarShape Concrete.Concrete) ->
      SEval sym (SBit sym)
    varModelPred :: forall sym.
    Backend sym =>
    sym -> (VarShape sym, VarShape Concrete) -> SEval sym (SBit sym)
    varModelPred sym
    sym (VarShape sym, VarShape Concrete)
    vx =
      case (VarShape sym, VarShape Concrete)
    vx of
        (VarBit SBit sym
    b, VarBit SBit Concrete
    blit) ->
          sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
    bitEq sym
    sym SBit sym
    b (sym -> Bool -> SBit sym
    forall sym. Backend sym => sym -> Bool -> SBit sym
    bitLit sym
    sym Bool
    SBit Concrete
    blit)

        (VarInteger SInteger sym
    i, VarInteger SInteger Concrete
    ilit) ->
          sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
    intEq sym
    sym SInteger sym
    i (SInteger sym -> SEval sym (SBit sym))
    -> SEval sym (SInteger sym) -> SEval sym (SBit sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    SInteger Concrete
    ilit

        (VarRational SInteger sym
    n SInteger sym
    d, VarRational SInteger Concrete
    nlit SInteger Concrete
    dlit) ->
          do SInteger sym
    n' <- sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    SInteger Concrete
    nlit
             SInteger sym
    d' <- sym -> Integer -> SEval sym (SInteger sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit sym
    sym Integer
    SInteger Concrete
    dlit
             sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
    rationalEq sym
    sym (SInteger sym -> SInteger sym -> SRational sym
    forall sym. SInteger sym -> SInteger sym -> SRational sym
    SRational SInteger sym
    n SInteger sym
    d) (SInteger sym -> SInteger sym -> SRational sym
    forall sym. SInteger sym -> SInteger sym -> SRational sym
    SRational SInteger sym
    n' SInteger sym
    d')

        (VarWord SWord sym
    w, VarWord (Concrete.BV Integer
    len Integer
    wlit)) ->
          sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
    wordEq sym
    sym SWord sym
    w (SWord sym -> SEval sym (SBit sym))
    -> SEval sym (SWord sym) -> SEval sym (SBit sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> Integer -> Integer -> SEval sym (SWord sym)
    forall sym.
    Backend sym =>
    sym -> Integer -> Integer -> SEval sym (SWord sym)
    wordLit sym
    sym Integer
    len Integer
    wlit

        (VarFloat SFloat sym
    f, VarFloat SFloat Concrete
    flit) ->
          sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
    fpLogicalEq sym
    sym SFloat sym
    f (SFloat sym -> SEval sym (SBit sym))
    -> SEval sym (SFloat sym) -> SEval sym (SBit sym)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< sym -> BF -> SEval sym (SFloat sym)
    forall sym. Backend sym => sym -> BF -> SEval sym (SFloat sym)
    fpExactLit sym
    sym BF
    SFloat Concrete
    flit

        (VarFinSeq Integer
    _n [VarShape sym]
    vs, VarFinSeq Integer
    _ [VarShape Concrete]
    xs) -> sym
    -> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym
    -> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym)
    modelPred sym
    sym [VarShape sym]
    vs [VarShape Concrete]
    xs
        (VarTuple [VarShape sym]
    vs, VarTuple [VarShape Concrete]
    xs) -> sym
    -> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym
    -> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym)
    modelPred sym
    sym [VarShape sym]
    vs [VarShape Concrete]
    xs
        (VarRecord RecordMap Ident (VarShape sym)
    vs, VarRecord RecordMap Ident (VarShape Concrete)
    xs) -> sym
    -> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym)
    forall sym.
    Backend sym =>
    sym
    -> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym)
    modelPred sym
    sym (RecordMap Ident (VarShape sym) -> [VarShape sym]
    forall a b. RecordMap a b -> [b]
    recordElements RecordMap Ident (VarShape sym)
    vs) (RecordMap Ident (VarShape Concrete) -> [VarShape Concrete]
    forall a b. RecordMap a b -> [b]
    recordElements RecordMap Ident (VarShape Concrete)
    xs)
        (VarShape sym, VarShape Concrete)
    _ -> [Char] -> [[Char]] -> SEval sym (SBit sym)
    forall a. HasCallStack => [Char] -> [[Char]] -> a
    panic [Char]
    "varModelPred" [[Char]
    "variable shape mismatch!"]

    varToExpr :: PrimMap -> FinType -> VarShape Concrete.Concrete -> Expr
    varToExpr :: PrimMap -> FinType -> VarShape Concrete -> Expr
    varToExpr PrimMap
    prims = FinType -> VarShape Concrete -> Expr
    go
      where

      prim :: Text -> Expr
    prim Text
    n = PrimMap -> PrimIdent -> Expr
    ePrim PrimMap
    prims (Text -> PrimIdent
    prelPrim Text
    n)

      go :: FinType -> VarShape Concrete.Concrete -> Expr
      go :: FinType -> VarShape Concrete -> Expr
    go FinType
    ty VarShape Concrete
    val =
        case (FinType
    ty,VarShape Concrete
    val) of
          (FTNewtype Newtype
    nt [Either Nat' TValue]
    ts RecordMap Ident FinType
    tfs, VarRecord RecordMap Ident (VarShape Concrete)
    vfs) ->
            let res :: Either (Either Ident Ident) (RecordMap Ident Expr)
    res = (Ident -> VarShape Concrete -> FinType -> Expr)
    -> RecordMap Ident (VarShape Concrete)
    -> RecordMap Ident FinType
    -> Either (Either Ident Ident) (RecordMap Ident Expr)
    forall a b c d.
    Ord a =>
    (a -> b -> c -> d)
    -> RecordMap a b
    -> RecordMap a c
    -> Either (Either a a) (RecordMap a d)
    zipRecords (\Ident
    _lbl VarShape Concrete
    v FinType
    t -> FinType -> VarShape Concrete -> Expr
    go FinType
    t VarShape Concrete
    v) RecordMap Ident (VarShape Concrete)
    vfs RecordMap Ident FinType
    tfs
             in case Either (Either Ident Ident) (RecordMap Ident Expr)
    res of
                  Left Either Ident Ident
    _ -> Expr
    forall {a}. a
    mismatch -- different fields
                  Right RecordMap Ident Expr
    efs ->
                    let f :: Expr
    f = (Expr -> Either Nat' TValue -> Expr)
    -> Expr -> [Either Nat' TValue] -> Expr
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (\Expr
    x Either Nat' TValue
    t -> Expr -> Prop -> Expr
    ETApp Expr
    x (Either Nat' TValue -> Prop
    tNumValTy Either Nat' TValue
    t)) (Name -> Expr
    EVar (Newtype -> Name
    ntConName Newtype
    nt)) [Either Nat' TValue]
    ts
                     in Expr -> Expr -> Expr
    EApp Expr
    f (RecordMap Ident Expr -> Expr
    ERec RecordMap Ident Expr
    efs)

          (FTRecord RecordMap Ident FinType
    tfs, VarRecord RecordMap Ident (VarShape Concrete)
    vfs) ->
            let res :: Either (Either Ident Ident) (RecordMap Ident Expr)
    res = (Ident -> VarShape Concrete -> FinType -> Expr)
    -> RecordMap Ident (VarShape Concrete)
    -> RecordMap Ident FinType
    -> Either (Either Ident Ident) (RecordMap Ident Expr)
    forall a b c d.
    Ord a =>
    (a -> b -> c -> d)
    -> RecordMap a b
    -> RecordMap a c
    -> Either (Either a a) (RecordMap a d)
    zipRecords (\Ident
    _lbl VarShape Concrete
    v FinType
    t -> FinType -> VarShape Concrete -> Expr
    go FinType
    t VarShape Concrete
    v) RecordMap Ident (VarShape Concrete)
    vfs RecordMap Ident FinType
    tfs
             in case Either (Either Ident Ident) (RecordMap Ident Expr)
    res of
                  Left Either Ident Ident
    _ -> Expr
    forall {a}. a
    mismatch -- different fields
                  Right RecordMap Ident Expr
    efs -> RecordMap Ident Expr -> Expr
    ERec RecordMap Ident Expr
    efs
          (FTTuple [FinType]
    ts, VarTuple [VarShape Concrete]
    tvs) ->
            [Expr] -> Expr
    ETuple ((FinType -> VarShape Concrete -> Expr)
    -> [FinType] -> [VarShape Concrete] -> [Expr]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith FinType -> VarShape Concrete -> Expr
    go [FinType]
    ts [VarShape Concrete]
    tvs)

          (FinType
    FTBit, VarBit SBit Concrete
    b) ->
            Text -> Expr
    prim (if Bool
    SBit Concrete
    b then Text
    "True" else Text
    "False")

          (FinType
    FTInteger, VarInteger SInteger Concrete
    i) ->
            -- This works uniformly for values of type Integer or Z n
            Expr -> Prop -> Expr
    ETApp (Expr -> Prop -> Expr
    ETApp (Text -> Expr
    prim Text
    "number") (Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum Integer
    SInteger Concrete
    i)) (FinType -> Prop
    finTypeToType FinType
    ty)

          (FTIntMod Integer
    _, VarInteger SInteger Concrete
    i) ->
            -- This works uniformly for values of type Integer or Z n
            Expr -> Prop -> Expr
    ETApp (Expr -> Prop -> Expr
    ETApp (Text -> Expr
    prim Text
    "number") (Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum Integer
    SInteger Concrete
    i)) (FinType -> Prop
    finTypeToType FinType
    ty)

          (FinType
    FTRational, VarRational SInteger Concrete
    n SInteger Concrete
    d) ->
            let n' :: Expr
    n' = Expr -> Prop -> Expr
    ETApp (Expr -> Prop -> Expr
    ETApp (Text -> Expr
    prim Text
    "number") (Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum Integer
    SInteger Concrete
    n)) Prop
    tInteger
                d' :: Expr
    d' = Expr -> Prop -> Expr
    ETApp (Expr -> Prop -> Expr
    ETApp (Text -> Expr
    prim Text
    "number") (Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum Integer
    SInteger Concrete
    d)) Prop
    tInteger
             in Expr -> Expr -> Expr
    EApp (Expr -> Expr -> Expr
    EApp (Text -> Expr
    prim Text
    "ratio") Expr
    n') Expr
    d'

          (FTFloat Integer
    e Integer
    p, VarFloat SFloat Concrete
    f) ->
            PrimMap -> Integer -> Integer -> BigFloat -> Expr
    floatToExpr PrimMap
    prims Integer
    e Integer
    p (BF -> BigFloat
    bfValue BF
    SFloat Concrete
    f)

          (FTSeq Integer
    _ FinType
    FTBit, VarWord (Concrete.BV Integer
    _ Integer
    v)) ->
            Expr -> Prop -> Expr
    ETApp (Expr -> Prop -> Expr
    ETApp (Text -> Expr
    prim Text
    "number") (Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum Integer
    v)) (FinType -> Prop
    finTypeToType FinType
    ty)

          (FTSeq Integer
    _ FinType
    t, VarFinSeq Integer
    _ [VarShape Concrete]
    svs) ->
            [Expr] -> Prop -> Expr
    EList ((VarShape Concrete -> Expr) -> [VarShape Concrete] -> [Expr]
    forall a b. (a -> b) -> [a] -> [b]
    map (FinType -> VarShape Concrete -> Expr
    go FinType
    t) [VarShape Concrete]
    svs) (FinType -> Prop
    finTypeToType FinType
    t)

          (FinType, VarShape Concrete)
    _ -> Expr
    forall {a}. a
    mismatch
        where
          mismatch :: a
    mismatch =
               [Char] -> [[Char]] -> a
    forall a. HasCallStack => [Char] -> [[Char]] -> a
    panic [Char]
    "Cryptol.Symbolic.varToExpr"
                 [[Char]
    "type mismatch:"
                 , Doc -> [Char]
    forall a. Show a => a -> [Char]
    show (Prop -> Doc
    forall a. PP a => a -> Doc
    pp (FinType -> Prop
    finTypeToType FinType
    ty))
                 , Doc -> [Char]
    forall a. Show a => a -> [Char]
    show (Concrete -> VarShape Concrete -> Doc
    forall sym. Backend sym => sym -> VarShape sym -> Doc
    ppVarShape Concrete
    Concrete.Concrete VarShape Concrete
    val)
                 ]

    floatToExpr :: PrimMap -> Integer -> Integer -> FP.BigFloat -> Expr
    floatToExpr :: PrimMap -> Integer -> Integer -> BigFloat -> Expr
    floatToExpr PrimMap
    prims Integer
    e Integer
    p BigFloat
    f =
      case BigFloat -> BFRep
    FP.bfToRep BigFloat
    f of
        BFRep
    FP.BFNaN -> Text -> Expr
    mkP Text
    "fpNaN"
        FP.BFRep Sign
    sign BFNum
    num ->
          case (Sign
    sign,BFNum
    num) of
            (Sign
    FP.Pos, BFNum
    FP.Zero)   -> Text -> Expr
    mkP Text
    "fpPosZero"
            (Sign
    FP.Neg, BFNum
    FP.Zero)   -> Text -> Expr
    mkP Text
    "fpNegZero"
            (Sign
    FP.Pos, BFNum
    FP.Inf)    -> Text -> Expr
    mkP Text
    "fpPosInf"
            (Sign
    FP.Neg, BFNum
    FP.Inf)    -> Text -> Expr
    mkP Text
    "fpNegInf"
            (Sign
    _, FP.Num Integer
    m Int64
    ex) ->
                let r :: Rational
    r = Integer -> Rational
    forall a. Real a => a -> Rational
    toRational Integer
    m Rational -> Rational -> Rational
    forall a. Num a => a -> a -> a
    * (Rational
    2 Rational -> Int64 -> Rational
    forall a b. (Fractional a, Integral b) => a -> b -> a
    ^^ Int64
    ex)
                in Expr -> Expr
    EProofApp (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ PrimMap -> PrimIdent -> Expr
    ePrim PrimMap
    prims (Text -> PrimIdent
    prelPrim Text
    "fraction")
                              Expr -> Prop -> Expr
    `ETApp` Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum (Rational -> Integer
    forall a. Ratio a -> a
    numerator Rational
    r)
                              Expr -> Prop -> Expr
    `ETApp` Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum (Rational -> Integer
    forall a. Ratio a -> a
    denominator Rational
    r)
                              Expr -> Prop -> Expr
    `ETApp` Int -> Prop
    forall a. Integral a => a -> Prop
    tNum (Int
    0 :: Int)
                              Expr -> Prop -> Expr
    `ETApp` Prop -> Prop -> Prop
    tFloat (Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum Integer
    e) (Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum Integer
    p)
      where
      mkP :: Text -> Expr
    mkP Text
    n = Expr -> Expr
    EProofApp (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ PrimMap -> PrimIdent -> Expr
    ePrim PrimMap
    prims (Text -> PrimIdent
    floatPrim Text
    n) Expr -> Prop -> Expr
    `ETApp` (Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum Integer
    e) Expr -> Prop -> Expr
    `ETApp` (Integer -> Prop
    forall a. Integral a => a -> Prop
    tNum Integer
    p)