-- |
-- 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
 ) 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 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 -> String
(Int -> SatNum -> ShowS)
-> (SatNum -> String) -> ([SatNum] -> ShowS) -> Show SatNum
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SatNum] -> ShowS
$cshowList :: [SatNum] -> ShowS
show :: SatNum -> String
$cshow :: SatNum -> String
showsPrec :: Int -> SatNum -> ShowS
$cshowsPrec :: Int -> SatNum -> ShowS
Show)

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

data ProverCommand = ProverCommand {
    ProverCommand -> QueryType
pcQueryType :: QueryType
    -- ^ The type of query to run
  , ProverCommand -> String
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 String
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 String [FinType]
predArgTypes QueryType
qtype schema :: Schema
schema@(Forall [TParam]
ts [Prop]
ps Prop
ty)
  | [TParam] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TParam]
ts Bool -> Bool -> Bool
&& [Prop] -> 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 String [FinType]
forall a b. b -> Either a b
Right [FinType]
fts
        Either Nat' (Maybe [FinType])
_ | QueryType
SafetyQuery <- QueryType
qtype -> String -> Either String [FinType]
forall a b. a -> Either a b
Left (String -> Either String [FinType])
-> String -> Either String [FinType]
forall a b. (a -> b) -> a -> b
$ String
"Expected finite result type:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
schema)
          | Bool
otherwise -> String -> Either String [FinType]
forall a b. a -> Either a b
Left (String -> Either String [FinType])
-> String -> Either String [FinType]
forall a b. (a -> b) -> a -> b
$ String
"Not a valid predicate type:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
schema)
  | Bool
otherwise = String -> Either String [FinType]
forall a b. a -> Either a b
Left (String -> Either String [FinType])
-> String -> Either String [FinType]
forall a b. (a -> b) -> a -> b
$ String
"Not a monomorphic type:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
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 (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)
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)
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)
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 :: sym -> VarShape sym -> Doc
ppVarShape sym
_sym (VarBit SBit sym
_b) = String -> Doc
text String
"<bit>"
ppVarShape sym
_sym (VarInteger SInteger sym
_i) = String -> Doc
text String
"<integer>"
ppVarShape sym
_sym (VarFloat SFloat sym
_f) = String -> Doc
text String
"<float>"
ppVarShape sym
_sym (VarRational SInteger sym
_n SInteger sym
_d) = String -> Doc
text String
"<rational>"
ppVarShape sym
sym (VarWord SWord sym
w) = String -> Doc
text String
"<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
<> String -> Doc
text String
">"
ppVarShape sym
sym (VarFinSeq Integer
_ [VarShape sym]
xs) =
  Doc -> Doc
brackets ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((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
parens ([Doc] -> Doc
sep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((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
braces ([Doc] -> Doc
sep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma (((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


varShapeToValue :: Backend sym => sym -> VarShape sym -> GenValue sym
varShapeToValue :: 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 -> SEval sym (WordValue sym) -> GenValue sym
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord (sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w) (WordValue sym -> SEval sym (WordValue sym)
forall (m :: * -> *) a. Monad m => a -> m a
return (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
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
n ([SEval sym (GenValue sym)] -> SeqMap sym
forall sym. [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap ((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 (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 (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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (GenValue sym -> SEval sym (GenValue sym)
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
  { FreshVarFns sym -> IO (SBit sym)
freshBitVar     :: IO (SBit sym)
  , FreshVarFns sym -> Integer -> IO (SWord sym)
freshWordVar    :: Integer -> IO (SWord sym)
  , FreshVarFns sym
-> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
freshIntegerVar :: Maybe Integer -> Maybe Integer -> IO (SInteger sym)
  , FreshVarFns sym -> Integer -> Integer -> IO (SFloat sym)
freshFloatVar   :: Integer -> Integer -> IO (SFloat sym)
  }

freshVar :: Backend sym => FreshVarFns sym -> FinType -> IO (VarShape sym)
freshVar :: 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 (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    -> String -> [String] -> IO (VarShape sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"freshVariable" [String
"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)
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)
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)
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)
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]
_ = String -> [String] -> [(TValue, Expr, Value)]
forall a. HasCallStack => String -> [String] -> a
panic String
"computeModel" [String
"type/value list mismatch"]



modelPred  ::
  Backend sym =>
  sym ->
  [VarShape sym] ->
  [VarShape Concrete.Concrete] ->
  SEval sym (SBit sym)
modelPred :: 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)
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 :: 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 len 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)
_ -> String -> [String] -> SEval sym (SBit sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"varModelPred" [String
"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 (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
ntName 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 _ 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 =
           String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Symbolic.varToExpr"
             [String
"type mismatch:"
             , Doc -> String
forall a. Show a => a -> String
show (Prop -> Doc
forall a. PP a => a -> Doc
pp (FinType -> Prop
finTypeToType FinType
ty))
             , Doc -> String
forall a. Show a => a -> String
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)