-- |
-- 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]
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
    -- ^ 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)
  | 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


-- | 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 = 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 -- different fields
              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 -- 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 (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) ->
        -- This works uniformly for values of type Integer or Z n
        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) ->
        -- This works uniformly for values of type Integer or Z n
        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)