{-# 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
, unFinType
, predArgTypes
, 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]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [SatNum] -> ShowS
$cshowList :: [SatNum] -> ShowS
show :: SatNum -> [Char]
$cshow :: SatNum -> [Char]
showsPrec :: Int -> SatNum -> ShowS
$cshowsPrec :: Int -> SatNum -> ShowS
Show)
data QueryType = SatQuery SatNum | ProveQuery | SafetyQuery
deriving (Int -> QueryType -> ShowS
[QueryType] -> ShowS
QueryType -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [QueryType] -> ShowS
$cshowList :: [QueryType] -> ShowS
show :: QueryType -> [Char]
$cshow :: QueryType -> [Char]
showsPrec :: Int -> QueryType -> ShowS
$cshowsPrec :: Int -> QueryType -> ShowS
Show)
data ProverCommand = ProverCommand {
ProverCommand -> QueryType
pcQueryType :: QueryType
, ProverCommand -> [Char]
pcProverName :: String
, ProverCommand -> Bool
pcVerbose :: Bool
, ProverCommand -> Bool
pcValidate :: Bool
, ProverCommand -> IORef ProverStats
pcProverStats :: !(IORef ProverStats)
, :: [DeclGroup]
, ProverCommand -> Maybe [Char]
pcSmtFile :: Maybe FilePath
, ProverCommand -> Expr
pcExpr :: Expr
, ProverCommand -> Schema
pcSchema :: Schema
, ProverCommand -> Bool
pcIgnoreSafety :: Bool
}
type ProverStats = NominalDiffTime
data CounterExampleType = SafetyViolation | PredicateFalsified
data ProverResult = AllSatResult [SatResult]
| 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)
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TParam]
ts Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Prop]
ps =
case TValue -> Maybe [FinType]
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TypeEnv -> Prop -> Either Nat' TValue
evalType forall a. Monoid a => a
mempty Prop
ty) of
Right (Just [FinType]
fts) -> forall a b. b -> Either a b
Right [FinType]
fts
Either Nat' (Maybe [FinType])
_ | QueryType
SafetyQuery <- QueryType
qtype -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ [Char]
"Expected finite result type:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. PP a => a -> Doc
pp Schema
schema)
| Bool
otherwise -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ [Char]
"Not a valid predicate type:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. PP a => a -> Doc
pp Schema
schema)
| Bool
otherwise = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ [Char]
"Not a monomorphic type:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. PP a => a -> Doc
pp Schema
schema)
where
go :: TValue -> Maybe [FinType]
go :: TValue -> Maybe [FinType]
go TValue
TVBit = forall a. a -> Maybe a
Just []
go (TVFun TValue
ty1 TValue
ty2) = (:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TValue -> Maybe FinType
finType TValue
ty1 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
= forall a. a -> Maybe a
Just []
| Bool
otherwise
= 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 -> forall a. a -> Maybe a
Just FinType
FTBit
TValue
TVInteger -> forall a. a -> Maybe a
Just FinType
FTInteger
TVIntMod Integer
n -> forall a. a -> Maybe a
Just (Integer -> FinType
FTIntMod Integer
n)
TValue
TVRational -> forall a. a -> Maybe a
Just FinType
FTRational
TVFloat Integer
e Integer
p -> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TValue -> Maybe FinType
finType TValue
t
TVTuple [TValue]
ts -> [FinType] -> FinType
FTTuple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 {} -> forall a. Maybe a
Nothing
TVArray{} -> forall a. Maybe a
Nothing
TVStream{} -> forall a. Maybe a
Nothing
TVFun{} -> 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 (forall a. Integral a => a -> Prop
tNum Integer
n)
FinType
FTRational -> Prop
tRational
FTFloat Integer
e Integer
p -> Prop -> Prop -> Prop
tFloat (forall a. Integral a => a -> Prop
tNum Integer
e) (forall a. Integral a => a -> Prop
tNum Integer
p)
FTSeq Integer
l FinType
ety -> Prop -> Prop -> Prop
tSeq (forall a. Integral a => a -> Prop
tNum Integer
l) (FinType -> Prop
finTypeToType FinType
ety)
FTTuple [FinType]
ftys -> [Prop] -> Prop
tTuple (FinType -> Prop
finTypeToType 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 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 (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)) = 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 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 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 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:" forall a. Semigroup a => a -> a -> a
<> Integer -> Doc
integer (forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w) forall a. Semigroup a => a -> a -> a
<> [Char] -> Doc
text [Char]
">"
ppVarShape sym
sym (VarFinSeq Integer
_ [VarShape sym]
xs) =
[Doc] -> Doc
ppList (forall a b. (a -> b) -> [a] -> [b]
map (forall sym. Backend sym => sym -> VarShape sym -> Doc
ppVarShape sym
sym) [VarShape sym]
xs)
ppVarShape sym
sym (VarTuple [VarShape sym]
xs) =
[Doc] -> Doc
ppTuple (forall a b. (a -> b) -> [a] -> [b]
map (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 (forall a b. (a -> b) -> [a] -> [b]
map forall {a}. PP a => (a, VarShape sym) -> Doc
ppField (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) = forall a. PP a => a -> Doc
pp a
f Doc -> Doc -> Doc
<+> Char -> Doc
char Char
'=' Doc -> Doc -> Doc
<+> forall sym. Backend sym => sym -> VarShape sym -> Doc
ppVarShape sym
sym VarShape sym
v
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 = forall sym. VarShape sym -> [VarShape sym] -> [VarShape sym]
flattenShape VarShape sym
x (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 forall a. a -> [a] -> [a]
: [VarShape sym]
tl
VarInteger{} -> VarShape sym
x forall a. a -> [a] -> [a]
: [VarShape sym]
tl
VarRational{} -> VarShape sym
x forall a. a -> [a] -> [a]
: [VarShape sym]
tl
VarWord{} -> VarShape sym
x forall a. a -> [a] -> [a]
: [VarShape sym]
tl
VarFloat{} -> VarShape sym
x forall a. a -> [a] -> [a]
: [VarShape sym]
tl
VarFinSeq Integer
_ [VarShape sym]
vs -> forall sym. [VarShape sym] -> [VarShape sym] -> [VarShape sym]
flattenShapes [VarShape sym]
vs [VarShape sym]
tl
VarTuple [VarShape sym]
vs -> forall sym. [VarShape sym] -> [VarShape sym] -> [VarShape sym]
flattenShapes [VarShape sym]
vs [VarShape sym]
tl
VarRecord RecordMap Ident (VarShape sym)
fs -> forall sym. [VarShape sym] -> [VarShape sym] -> [VarShape sym]
flattenShapes (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 -> forall sym. SBit sym -> GenValue sym
VBit SBit sym
b
VarInteger SInteger sym
i -> forall sym. SInteger sym -> GenValue sym
VInteger SInteger sym
i
VarRational SInteger sym
n SInteger sym
d -> forall sym. SRational sym -> GenValue sym
VRational (forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational SInteger sym
n SInteger sym
d)
VarWord SWord sym
w -> forall sym. Integer -> WordValue sym -> GenValue sym
VWord (forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w) (forall sym. SWord sym -> WordValue sym
wordVal SWord sym
w)
VarFloat SFloat sym
f -> forall sym. SFloat sym -> GenValue sym
VFloat SFloat sym
f
VarFinSeq Integer
n [VarShape sym]
vs -> forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
n (forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
finiteSeqMap sym
sym (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. Backend sym => sym -> VarShape sym -> GenValue sym
varShapeToValue sym
sym) [VarShape sym]
vs))
VarTuple [VarShape sym]
vs -> forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. Backend sym => sym -> VarShape sym -> GenValue sym
varShapeToValue sym
sym) [VarShape sym]
vs)
VarRecord RecordMap Ident (VarShape sym)
fs -> forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> forall sym. SBit sym -> VarShape sym
VarBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. FreshVarFns sym -> IO (SBit sym)
freshBitVar FreshVarFns sym
fns
FinType
FTInteger -> forall sym. SInteger sym -> VarShape sym
VarInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
FreshVarFns sym
-> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
freshIntegerVar FreshVarFns sym
fns forall a. Maybe a
Nothing forall a. Maybe a
Nothing
FinType
FTRational -> forall sym. SInteger sym -> SInteger sym -> VarShape sym
VarRational
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
FreshVarFns sym
-> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
freshIntegerVar FreshVarFns sym
fns forall a. Maybe a
Nothing forall a. Maybe a
Nothing
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall sym.
FreshVarFns sym
-> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
freshIntegerVar FreshVarFns sym
fns (forall a. a -> Maybe a
Just Integer
1) forall a. Maybe a
Nothing
FTIntMod Integer
0 -> forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"freshVariable" [[Char]
"0 modulus not allowed"]
FTIntMod Integer
m -> forall sym. SInteger sym -> VarShape sym
VarInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
FreshVarFns sym
-> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
freshIntegerVar FreshVarFns sym
fns (forall a. a -> Maybe a
Just Integer
0) (forall a. a -> Maybe a
Just (Integer
mforall a. Num a => a -> a -> a
-Integer
1))
FTFloat Integer
e Integer
p -> forall sym. SFloat sym -> VarShape sym
VarFloat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
FreshVarFns sym -> Integer -> Integer -> IO (SFloat sym)
freshFloatVar FreshVarFns sym
fns Integer
e Integer
p
FTSeq Integer
n FinType
FTBit -> forall sym. SWord sym -> VarShape sym
VarWord forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. FreshVarFns sym -> Integer -> IO (SWord sym)
freshWordVar FreshVarFns sym
fns (forall a. Integral a => a -> Integer
toInteger Integer
n)
FTSeq Integer
n FinType
t -> forall sym. Integer -> [VarShape sym] -> VarShape sym
VarFinSeq (forall a. Integral a => a -> Integer
toInteger Integer
n) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall i a. Integral i => i -> a -> [a]
genericReplicate Integer
n (forall sym.
Backend sym =>
FreshVarFns sym -> FinType -> IO (VarShape sym)
freshVar FreshVarFns sym
fns FinType
t))
FTTuple [FinType]
ts -> forall sym. [VarShape sym] -> VarShape sym
VarTuple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym.
Backend sym =>
FreshVarFns sym -> FinType -> IO (VarShape sym)
freshVar FreshVarFns sym
fns) [FinType]
ts
FTRecord RecordMap Ident FinType
fs -> forall sym. RecordMap Ident (VarShape sym) -> VarShape sym
VarRecord forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (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 -> forall sym. RecordMap Ident (VarShape sym) -> VarShape sym
VarRecord forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (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' = 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')forall a. a -> [a] -> [a]
:[(TValue, Expr, Value)]
zs)
computeModel PrimMap
_ [FinType]
_ [VarShape Concrete]
_ = 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym.
Backend sym =>
sym -> (VarShape sym, VarShape Concrete) -> SEval sym (SBit sym)
varModelPred sym
sym) (forall a b. [a] -> [b] -> [(a, b)]
zip [VarShape sym]
vs [VarShape Concrete]
xs)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitAnd sym
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) ->
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
bitEq sym
sym SBit sym
b (forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit sym
sym SBit Concrete
blit)
(VarInteger SInteger sym
i, VarInteger SInteger Concrete
ilit) ->
forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intEq sym
sym SInteger sym
i forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym SInteger Concrete
ilit
(VarRational SInteger sym
n SInteger sym
d, VarRational SInteger Concrete
nlit SInteger Concrete
dlit) ->
do SInteger sym
n' <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym SInteger Concrete
nlit
SInteger sym
d' <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym SInteger Concrete
dlit
forall sym.
Backend sym =>
sym -> SRational sym -> SRational sym -> SEval sym (SBit sym)
rationalEq sym
sym (forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational SInteger sym
n SInteger sym
d) (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)) ->
forall sym.
Backend sym =>
sym -> SWord sym -> SWord sym -> SEval sym (SBit sym)
wordEq sym
sym SWord sym
w forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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) ->
forall sym.
Backend sym =>
sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
fpLogicalEq sym
sym SFloat sym
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym. Backend sym => sym -> BF -> SEval sym (SFloat sym)
fpExactLit sym
sym SFloat Concrete
flit
(VarFinSeq Integer
_n [VarShape sym]
vs, VarFinSeq Integer
_ [VarShape Concrete]
xs) -> 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) -> 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) -> forall sym.
Backend sym =>
sym
-> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym)
modelPred sym
sym (forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident (VarShape sym)
vs) (forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident (VarShape Concrete)
xs)
(VarShape sym, VarShape Concrete)
_ -> 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 = 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
_ -> forall {a}. a
mismatch
Right RecordMap Ident Expr
efs ->
let f :: Expr
f = 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 = 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
_ -> forall {a}. a
mismatch
Right RecordMap Ident Expr
efs -> RecordMap Ident Expr -> Expr
ERec RecordMap Ident Expr
efs
(FTTuple [FinType]
ts, VarTuple [VarShape Concrete]
tvs) ->
[Expr] -> Expr
ETuple (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 SBit Concrete
b then Text
"True" else Text
"False")
(FinType
FTInteger, VarInteger SInteger Concrete
i) ->
Expr -> Prop -> Expr
ETApp (Expr -> Prop -> Expr
ETApp (Text -> Expr
prim Text
"number") (forall a. Integral a => a -> Prop
tNum SInteger Concrete
i)) (FinType -> Prop
finTypeToType FinType
ty)
(FTIntMod Integer
_, VarInteger SInteger Concrete
i) ->
Expr -> Prop -> Expr
ETApp (Expr -> Prop -> Expr
ETApp (Text -> Expr
prim Text
"number") (forall a. Integral a => a -> Prop
tNum 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") (forall a. Integral a => a -> Prop
tNum SInteger Concrete
n)) Prop
tInteger
d' :: Expr
d' = Expr -> Prop -> Expr
ETApp (Expr -> Prop -> Expr
ETApp (Text -> Expr
prim Text
"number") (forall a. Integral a => a -> Prop
tNum 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 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") (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 (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)
_ -> forall {a}. a
mismatch
where
mismatch :: a
mismatch =
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"Cryptol.Symbolic.varToExpr"
[[Char]
"type mismatch:"
, forall a. Show a => a -> [Char]
show (forall a. PP a => a -> Doc
pp (FinType -> Prop
finTypeToType FinType
ty))
, forall a. Show a => a -> [Char]
show (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 = forall a. Real a => a -> Rational
toRational Integer
m forall a. Num a => a -> a -> a
* (Rational
2 forall a b. (Fractional a, Integral b) => a -> b -> a
^^ Int64
ex)
in Expr -> Expr
EProofApp forall a b. (a -> b) -> a -> b
$ PrimMap -> PrimIdent -> Expr
ePrim PrimMap
prims (Text -> PrimIdent
prelPrim Text
"fraction")
Expr -> Prop -> Expr
`ETApp` forall a. Integral a => a -> Prop
tNum (forall a. Ratio a -> a
numerator Rational
r)
Expr -> Prop -> Expr
`ETApp` forall a. Integral a => a -> Prop
tNum (forall a. Ratio a -> a
denominator Rational
r)
Expr -> Prop -> Expr
`ETApp` forall a. Integral a => a -> Prop
tNum (Int
0 :: Int)
Expr -> Prop -> Expr
`ETApp` Prop -> Prop -> Prop
tFloat (forall a. Integral a => a -> Prop
tNum Integer
e) (forall a. Integral a => a -> Prop
tNum Integer
p)
where
mkP :: Text -> Expr
mkP Text
n = Expr -> Expr
EProofApp forall a b. (a -> b) -> a -> b
$ PrimMap -> PrimIdent -> Expr
ePrim PrimMap
prims (Text -> PrimIdent
floatPrim Text
n) Expr -> Prop -> Expr
`ETApp` (forall a. Integral a => a -> Prop
tNum Integer
e) Expr -> Prop -> Expr
`ETApp` (forall a. Integral a => a -> Prop
tNum Integer
p)