-- |
-- 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(..)
 , FinNominalType(..)
 , finType
 , unFinType
 , predArgTypes
   -- * VarShape
 , VarShape(..)
 , varShapeToValue
 , freshVar
 , computeModel
 , FreshVarFns(..)
 , modelPred
 , varModelPred
 , varToExpr
 , flattenShape
 , flattenShapes
 ) where


import Control.Monad (foldM)
import qualified Data.IntMap.Strict as IntMap
import Data.IORef(IORef)
import Data.List (genericReplicate)
import Data.Ratio
import Data.Vector(Vector)
import qualified Data.Vector as Vector
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(..), TNominalTypeValue(..), evalType,tValTy,tNumValTy,ConInfo(..))
import           Cryptol.Utils.Ident (Ident,prelPrim,floatPrim)
import           Cryptol.Utils.RecordMap
import           Cryptol.Utils.Panic
import           Cryptol.Utils.PP


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

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

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

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

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

type ProverStats = NominalDiffTime

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

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

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

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

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

data FinNominalType =
    FStruct (RecordMap Ident FinType)
  | FEnum (Vector (ConInfo FinType))

finType :: TValue -> Maybe FinType
finType :: TValue -> Maybe FinType
finType TValue
ty =
  case TValue
ty of
    TValue
TVBit               -> FinType -> Maybe FinType
forall a. a -> Maybe a
Just FinType
FTBit
    TValue
TVInteger           -> FinType -> Maybe FinType
forall a. a -> Maybe a
Just FinType
FTInteger
    TVIntMod Integer
n          -> FinType -> Maybe FinType
forall a. a -> Maybe a
Just (Integer -> FinType
FTIntMod Integer
n)
    TValue
TVRational          -> FinType -> Maybe FinType
forall a. a -> Maybe a
Just FinType
FTRational
    TVFloat Integer
e Integer
p         -> FinType -> Maybe FinType
forall a. a -> Maybe a
Just (Integer -> Integer -> FinType
FTFloat Integer
e Integer
p)
    TVSeq Integer
n TValue
t           -> Integer -> FinType -> FinType
FTSeq Integer
n (FinType -> FinType) -> Maybe FinType -> Maybe FinType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TValue -> Maybe FinType
finType TValue
t
    TVTuple [TValue]
ts          -> [FinType] -> FinType
FTTuple ([FinType] -> FinType) -> Maybe [FinType] -> Maybe FinType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TValue -> Maybe FinType) -> [TValue] -> Maybe [FinType]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse TValue -> Maybe FinType
finType [TValue]
ts
    TVRec RecordMap Ident TValue
fields        -> RecordMap Ident FinType -> FinType
FTRecord (RecordMap Ident FinType -> FinType)
-> Maybe (RecordMap Ident FinType) -> Maybe FinType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TValue -> Maybe FinType)
-> RecordMap Ident TValue -> Maybe (RecordMap Ident FinType)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
traverse TValue -> Maybe FinType
finType RecordMap Ident TValue
fields
    TVNominal NominalType
u [Either Nat' TValue]
ts TNominalTypeValue
nv   -> NominalType -> [Either Nat' TValue] -> FinNominalType -> FinType
FTNominal NominalType
u [Either Nat' TValue]
ts (FinNominalType -> FinType)
-> Maybe FinNominalType -> Maybe FinType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      case TNominalTypeValue
nv of
        TVStruct RecordMap Ident TValue
body -> RecordMap Ident FinType -> FinNominalType
FStruct (RecordMap Ident FinType -> FinNominalType)
-> Maybe (RecordMap Ident FinType) -> Maybe FinNominalType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TValue -> Maybe FinType)
-> RecordMap Ident TValue -> Maybe (RecordMap Ident FinType)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
traverse TValue -> Maybe FinType
finType RecordMap Ident TValue
body
        TVEnum Vector (ConInfo TValue)
cs     -> Vector (ConInfo FinType) -> FinNominalType
FEnum   (Vector (ConInfo FinType) -> FinNominalType)
-> Maybe (Vector (ConInfo FinType)) -> Maybe FinNominalType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ConInfo TValue -> Maybe (ConInfo FinType))
-> Vector (ConInfo TValue) -> Maybe (Vector (ConInfo FinType))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse ((TValue -> Maybe FinType)
-> ConInfo TValue -> Maybe (ConInfo FinType)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ConInfo a -> f (ConInfo b)
traverse TValue -> Maybe FinType
finType) Vector (ConInfo TValue)
cs
        TNominalTypeValue
TVAbstract    -> Maybe FinNominalType
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)
    FTNominal NominalType
u [Either Nat' TValue]
ts FinNominalType
_  -> NominalType -> [Prop] -> Prop
tNominal NominalType
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)

    FTNominal NominalType
u [Either Nat' TValue]
ts FinNominalType
nv -> NominalType -> [Either Nat' TValue] -> TNominalTypeValue -> TValue
TVNominal NominalType
u [Either Nat' TValue]
ts (TNominalTypeValue -> TValue) -> TNominalTypeValue -> TValue
forall a b. (a -> b) -> a -> b
$
       case FinNominalType
nv of
          FStruct RecordMap Ident FinType
fs  -> RecordMap Ident TValue -> TNominalTypeValue
TVStruct (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)
          FEnum Vector (ConInfo FinType)
cs    -> Vector (ConInfo TValue) -> TNominalTypeValue
TVEnum ((FinType -> TValue) -> ConInfo FinType -> ConInfo TValue
forall a b. (a -> b) -> ConInfo a -> ConInfo b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FinType -> TValue
unFinType (ConInfo FinType -> ConInfo TValue)
-> Vector (ConInfo FinType) -> Vector (ConInfo TValue)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector (ConInfo FinType)
cs)

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))
  | VarEnum (SInteger sym) (Vector (ConInfo (VarShape sym)))

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


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

flattenShape :: VarShape sym -> [VarShape sym] -> [VarShape sym]
flattenShape :: forall sym. VarShape sym -> [VarShape sym] -> [VarShape sym]
flattenShape VarShape sym
x [VarShape sym]
tl =
  case VarShape sym
x of
    VarBit{}       -> VarShape sym
x VarShape sym -> [VarShape sym] -> [VarShape sym]
forall a. a -> [a] -> [a]
: [VarShape sym]
tl
    VarInteger{}   -> VarShape sym
x VarShape sym -> [VarShape sym] -> [VarShape sym]
forall a. a -> [a] -> [a]
: [VarShape sym]
tl
    VarRational{}  -> VarShape sym
x VarShape sym -> [VarShape sym] -> [VarShape sym]
forall a. a -> [a] -> [a]
: [VarShape sym]
tl
    VarWord{}      -> VarShape sym
x VarShape sym -> [VarShape sym] -> [VarShape sym]
forall a. a -> [a] -> [a]
: [VarShape sym]
tl
    VarFloat{}     -> VarShape sym
x VarShape sym -> [VarShape sym] -> [VarShape sym]
forall a. a -> [a] -> [a]
: [VarShape sym]
tl
    VarFinSeq Integer
_ [VarShape sym]
vs -> [VarShape sym] -> [VarShape sym] -> [VarShape sym]
forall sym. [VarShape sym] -> [VarShape sym] -> [VarShape sym]
flattenShapes [VarShape sym]
vs [VarShape sym]
tl
    VarTuple [VarShape sym]
vs    -> [VarShape sym] -> [VarShape sym] -> [VarShape sym]
forall sym. [VarShape sym] -> [VarShape sym] -> [VarShape sym]
flattenShapes [VarShape sym]
vs [VarShape sym]
tl
    VarRecord RecordMap Ident (VarShape sym)
fs   -> [VarShape sym] -> [VarShape sym] -> [VarShape sym]
forall sym. [VarShape sym] -> [VarShape sym] -> [VarShape sym]
flattenShapes (RecordMap Ident (VarShape sym) -> [VarShape sym]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident (VarShape sym)
fs) [VarShape sym]
tl
    VarEnum SInteger sym
_ Vector (ConInfo (VarShape sym))
cs   -> VarShape sym
x VarShape sym -> [VarShape sym] -> [VarShape sym]
forall a. a -> [a] -> [a]
: [VarShape sym] -> [VarShape sym] -> [VarShape sym]
forall sym. [VarShape sym] -> [VarShape sym] -> [VarShape sym]
flattenShapes [VarShape sym]
allCons [VarShape sym]
tl
      where
      allCons :: [VarShape sym]
allCons = (ConInfo (VarShape sym) -> [VarShape sym])
-> [ConInfo (VarShape sym)] -> [VarShape sym]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Vector (VarShape sym) -> [VarShape sym]
forall a. Vector a -> [a]
Vector.toList (Vector (VarShape sym) -> [VarShape sym])
-> (ConInfo (VarShape sym) -> Vector (VarShape sym))
-> ConInfo (VarShape sym)
-> [VarShape sym]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConInfo (VarShape sym) -> Vector (VarShape sym)
forall a. ConInfo a -> Vector a
conFields) (Vector (ConInfo (VarShape sym)) -> [ConInfo (VarShape sym)]
forall a. Vector a -> [a]
Vector.toList Vector (ConInfo (VarShape sym))
cs)

varShapeToValue :: Backend sym => sym -> VarShape sym -> GenValue sym
varShapeToValue :: forall sym. Backend sym => sym -> VarShape sym -> GenValue sym
varShapeToValue sym
sym VarShape sym
var =
  case VarShape sym
var of
    VarBit SBit sym
b     -> SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit SBit sym
b
    VarInteger SInteger sym
i -> SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger SInteger sym
i
    VarRational SInteger sym
n SInteger sym
d -> SRational sym -> GenValue sym
forall sym. SRational sym -> GenValue sym
VRational (SInteger sym -> SInteger sym -> SRational sym
forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational SInteger sym
n SInteger sym
d)
    VarWord SWord sym
w    -> Integer -> WordValue sym -> GenValue sym
forall sym. Integer -> WordValue sym -> GenValue sym
VWord (sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w) (SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
wordVal SWord sym
w)
    VarFloat SFloat sym
f   -> SFloat sym -> GenValue sym
forall sym. SFloat sym -> GenValue sym
VFloat SFloat sym
f
    VarFinSeq Integer
n [VarShape sym]
vs -> Integer -> SeqMap sym (GenValue sym) -> GenValue sym
forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
n (sym -> [SEval sym (GenValue sym)] -> SeqMap sym (GenValue sym)
forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
finiteSeqMap sym
sym ((VarShape sym -> SEval sym (GenValue sym))
-> [VarShape sym] -> [SEval sym (GenValue sym)]
forall a b. (a -> b) -> [a] -> [b]
map (GenValue sym -> SEval sym (GenValue sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> (VarShape sym -> GenValue sym)
-> VarShape sym
-> SEval sym (GenValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sym -> VarShape sym -> GenValue sym
forall sym. Backend sym => sym -> VarShape sym -> GenValue sym
varShapeToValue sym
sym) [VarShape sym]
vs))
    VarTuple [VarShape sym]
vs  -> [SEval sym (GenValue sym)] -> GenValue sym
forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple ((VarShape sym -> SEval sym (GenValue sym))
-> [VarShape sym] -> [SEval sym (GenValue sym)]
forall a b. (a -> b) -> [a] -> [b]
map (GenValue sym -> SEval sym (GenValue sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> (VarShape sym -> GenValue sym)
-> VarShape sym
-> SEval sym (GenValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sym -> VarShape sym -> GenValue sym
forall sym. Backend sym => sym -> VarShape sym -> GenValue sym
varShapeToValue sym
sym) [VarShape sym]
vs)
    VarRecord RecordMap Ident (VarShape sym)
fs -> RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord ((VarShape sym -> SEval sym (GenValue sym))
-> RecordMap Ident (VarShape sym)
-> RecordMap Ident (SEval sym (GenValue sym))
forall a b. (a -> b) -> RecordMap Ident a -> RecordMap Ident b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (GenValue sym -> SEval sym (GenValue sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> (VarShape sym -> GenValue sym)
-> VarShape sym
-> SEval sym (GenValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sym -> VarShape sym -> GenValue sym
forall sym. Backend sym => sym -> VarShape sym -> GenValue sym
varShapeToValue sym
sym) RecordMap Ident (VarShape sym)
fs)
    VarEnum SInteger sym
tag Vector (ConInfo (VarShape sym))
cons ->
      SInteger sym -> IntMap (ConValue sym) -> GenValue sym
forall sym. SInteger sym -> IntMap (ConValue sym) -> GenValue sym
VEnum SInteger sym
tag ([(Int, ConValue sym)] -> IntMap (ConValue sym)
forall a. [(Int, a)] -> IntMap a
IntMap.fromList
                   ([Int] -> [ConValue sym] -> [(Int, ConValue sym)]
forall a b. [a] -> [b] -> [(a, b)]
zip [ Int
0 .. ] [ GenValue sym -> SEval sym (GenValue sym)
forall a. a -> SEval sym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> (VarShape sym -> GenValue sym)
-> VarShape sym
-> SEval sym (GenValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sym -> VarShape sym -> GenValue sym
forall sym. Backend sym => sym -> VarShape sym -> GenValue sym
varShapeToValue sym
sym (VarShape sym -> SEval sym (GenValue sym))
-> ConInfo (VarShape sym) -> ConValue sym
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConInfo (VarShape sym)
c
                                 | ConInfo (VarShape sym)
c <- Vector (ConInfo (VarShape sym)) -> [ConInfo (VarShape sym)]
forall a. Vector a -> [a]
Vector.toList Vector (ConInfo (VarShape sym))
cons ]))

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

freshVar :: Backend sym => FreshVarFns sym -> FinType -> IO (VarShape sym)
freshVar :: forall sym.
Backend sym =>
FreshVarFns sym -> FinType -> IO (VarShape sym)
freshVar FreshVarFns sym
fns FinType
tp =
  case FinType
tp of
    FinType
FTBit         -> SBit sym -> VarShape sym
forall sym. SBit sym -> VarShape sym
VarBit      (SBit sym -> VarShape sym) -> IO (SBit sym) -> IO (VarShape sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FreshVarFns sym -> IO (SBit sym)
forall sym. FreshVarFns sym -> IO (SBit sym)
freshBitVar FreshVarFns sym
fns
    FinType
FTInteger     -> SInteger sym -> VarShape sym
forall sym. SInteger sym -> VarShape sym
VarInteger  (SInteger sym -> VarShape sym)
-> IO (SInteger sym) -> IO (VarShape sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FreshVarFns sym
-> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
forall sym.
FreshVarFns sym
-> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
freshIntegerVar FreshVarFns sym
fns Maybe Integer
forall a. Maybe a
Nothing Maybe Integer
forall a. Maybe a
Nothing
    FinType
FTRational    -> SInteger sym -> SInteger sym -> VarShape sym
forall sym. SInteger sym -> SInteger sym -> VarShape sym
VarRational
                        (SInteger sym -> SInteger sym -> VarShape sym)
-> IO (SInteger sym) -> IO (SInteger sym -> VarShape sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FreshVarFns sym
-> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
forall sym.
FreshVarFns sym
-> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
freshIntegerVar FreshVarFns sym
fns Maybe Integer
forall a. Maybe a
Nothing Maybe Integer
forall a. Maybe a
Nothing
                        IO (SInteger sym -> VarShape sym)
-> IO (SInteger sym) -> IO (VarShape sym)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FreshVarFns sym
-> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
forall sym.
FreshVarFns sym
-> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
freshIntegerVar FreshVarFns sym
fns (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1) Maybe Integer
forall a. Maybe a
Nothing
    FTIntMod Integer
0    -> [Char] -> [[Char]] -> IO (VarShape sym)
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"freshVariable" [[Char]
"0 modulus not allowed"]
    FTIntMod Integer
m    -> SInteger sym -> VarShape sym
forall sym. SInteger sym -> VarShape sym
VarInteger  (SInteger sym -> VarShape sym)
-> IO (SInteger sym) -> IO (VarShape sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FreshVarFns sym
-> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
forall sym.
FreshVarFns sym
-> Maybe Integer -> Maybe Integer -> IO (SInteger sym)
freshIntegerVar FreshVarFns sym
fns (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0) (Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
mInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1))
    FTFloat Integer
e Integer
p   -> SFloat sym -> VarShape sym
forall sym. SFloat sym -> VarShape sym
VarFloat    (SFloat sym -> VarShape sym)
-> IO (SFloat sym) -> IO (VarShape sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FreshVarFns sym -> Integer -> Integer -> IO (SFloat sym)
forall sym.
FreshVarFns sym -> Integer -> Integer -> IO (SFloat sym)
freshFloatVar FreshVarFns sym
fns Integer
e Integer
p
    FTSeq Integer
n FinType
FTBit -> SWord sym -> VarShape sym
forall sym. SWord sym -> VarShape sym
VarWord     (SWord sym -> VarShape sym) -> IO (SWord sym) -> IO (VarShape sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FreshVarFns sym -> Integer -> IO (SWord sym)
forall sym. FreshVarFns sym -> Integer -> IO (SWord sym)
freshWordVar FreshVarFns sym
fns (Integer -> Integer
forall a. Integral a => a -> Integer
toInteger Integer
n)
    FTSeq Integer
n FinType
t     -> Integer -> [VarShape sym] -> VarShape sym
forall sym. Integer -> [VarShape sym] -> VarShape sym
VarFinSeq (Integer -> Integer
forall a. Integral a => a -> Integer
toInteger Integer
n) ([VarShape sym] -> VarShape sym)
-> IO [VarShape sym] -> IO (VarShape sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [IO (VarShape sym)] -> IO [VarShape sym]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence (Integer -> IO (VarShape sym) -> [IO (VarShape sym)]
forall i a. Integral i => i -> a -> [a]
genericReplicate Integer
n (FreshVarFns sym -> FinType -> IO (VarShape sym)
forall sym.
Backend sym =>
FreshVarFns sym -> FinType -> IO (VarShape sym)
freshVar FreshVarFns sym
fns FinType
t))
    FTTuple [FinType]
ts    -> [VarShape sym] -> VarShape sym
forall sym. [VarShape sym] -> VarShape sym
VarTuple    ([VarShape sym] -> VarShape sym)
-> IO [VarShape sym] -> IO (VarShape sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FinType -> IO (VarShape sym)) -> [FinType] -> IO [VarShape sym]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (FreshVarFns sym -> FinType -> IO (VarShape sym)
forall sym.
Backend sym =>
FreshVarFns sym -> FinType -> IO (VarShape sym)
freshVar FreshVarFns sym
fns) [FinType]
ts
    FTRecord RecordMap Ident FinType
fs   -> RecordMap Ident (VarShape sym) -> VarShape sym
forall sym. RecordMap Ident (VarShape sym) -> VarShape sym
VarRecord   (RecordMap Ident (VarShape sym) -> VarShape sym)
-> IO (RecordMap Ident (VarShape sym)) -> IO (VarShape sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FinType -> IO (VarShape sym))
-> RecordMap Ident FinType -> IO (RecordMap Ident (VarShape sym))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
traverse (FreshVarFns sym -> FinType -> IO (VarShape sym)
forall sym.
Backend sym =>
FreshVarFns sym -> FinType -> IO (VarShape sym)
freshVar FreshVarFns sym
fns) RecordMap Ident FinType
fs
    FTNominal NominalType
_ [Either Nat' TValue]
_ FinNominalType
nv ->
      case FinNominalType
nv of
        FStruct RecordMap Ident FinType
fs -> RecordMap Ident (VarShape sym) -> VarShape sym
forall sym. RecordMap Ident (VarShape sym) -> VarShape sym
VarRecord (RecordMap Ident (VarShape sym) -> VarShape sym)
-> IO (RecordMap Ident (VarShape sym)) -> IO (VarShape sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FinType -> IO (VarShape sym))
-> RecordMap Ident FinType -> IO (RecordMap Ident (VarShape sym))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
traverse (FreshVarFns sym -> FinType -> IO (VarShape sym)
forall sym.
Backend sym =>
FreshVarFns sym -> FinType -> IO (VarShape sym)
freshVar FreshVarFns sym
fns) RecordMap Ident FinType
fs
        FEnum Vector (ConInfo FinType)
conTs ->
          do let maxCon :: Integer
maxCon = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Vector (ConInfo FinType) -> Int
forall a. Vector a -> Int
Vector.length Vector (ConInfo FinType)
conTs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
             SInteger sym
tag <- 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
maxCon)
             Vector (ConInfo (VarShape sym))
cons <- (ConInfo FinType -> IO (ConInfo (VarShape sym)))
-> Vector (ConInfo FinType) -> IO (Vector (ConInfo (VarShape sym)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse ((FinType -> IO (VarShape sym))
-> ConInfo FinType -> IO (ConInfo (VarShape sym))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ConInfo a -> f (ConInfo b)
traverse (FreshVarFns sym -> FinType -> IO (VarShape sym)
forall sym.
Backend sym =>
FreshVarFns sym -> FinType -> IO (VarShape sym)
freshVar FreshVarFns sym
fns)) Vector (ConInfo FinType)
conTs
             VarShape sym -> IO (VarShape sym)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SInteger sym -> Vector (ConInfo (VarShape sym)) -> VarShape sym
forall sym.
SInteger sym -> Vector (ConInfo (VarShape sym)) -> VarShape sym
VarEnum SInteger sym
tag Vector (ConInfo (VarShape sym))
cons)


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



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

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

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

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

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

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

    (VarFinSeq Integer
_n [VarShape sym]
vs, VarFinSeq Integer
_ [VarShape Concrete]
xs) -> sym
-> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym)
modelPred sym
sym [VarShape sym]
vs [VarShape Concrete]
xs
    (VarTuple [VarShape sym]
vs, VarTuple [VarShape Concrete]
xs) -> sym
-> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym)
modelPred sym
sym [VarShape sym]
vs [VarShape Concrete]
xs
    (VarRecord RecordMap Ident (VarShape sym)
vs, VarRecord RecordMap Ident (VarShape Concrete)
xs) -> sym
-> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym
-> [VarShape sym] -> [VarShape Concrete] -> SEval sym (SBit sym)
modelPred sym
sym (RecordMap Ident (VarShape sym) -> [VarShape sym]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident (VarShape sym)
vs) (RecordMap Ident (VarShape Concrete) -> [VarShape Concrete]
forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident (VarShape Concrete)
xs)
    (VarEnum SInteger sym
vi Vector (ConInfo (VarShape sym))
vcons,  VarEnum SInteger Concrete
i Vector (ConInfo (VarShape Concrete))
cons) ->
      do SInteger sym
tag     <- sym -> Integer -> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit sym
sym Integer
SInteger Concrete
i
         SBit sym
sameTag <- 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
tag SInteger sym
vi
         let i' :: Int
i' = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
SInteger Concrete
i
             flds :: ConInfo a -> [a]
flds = Vector a -> [a]
forall a. Vector a -> [a]
Vector.toList (Vector a -> [a]) -> (ConInfo a -> Vector a) -> ConInfo a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConInfo a -> Vector a
forall a. ConInfo a -> Vector a
conFields
         SBit sym
sameFs  <- case (Vector (ConInfo (VarShape sym))
vcons Vector (ConInfo (VarShape sym))
-> Int -> Maybe (ConInfo (VarShape sym))
forall a. Vector a -> Int -> Maybe a
Vector.!? Int
i', Vector (ConInfo (VarShape Concrete))
cons Vector (ConInfo (VarShape Concrete))
-> Int -> Maybe (ConInfo (VarShape Concrete))
forall a. Vector a -> Int -> Maybe a
Vector.!? Int
i') of
                      (Just ConInfo (VarShape sym)
con1, Just ConInfo (VarShape Concrete)
con2) ->
                         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 (ConInfo (VarShape sym) -> [VarShape sym]
forall {a}. ConInfo a -> [a]
flds ConInfo (VarShape sym)
con1) (ConInfo (VarShape Concrete) -> [VarShape Concrete]
forall {a}. ConInfo a -> [a]
flds ConInfo (VarShape Concrete)
con2)
                      (Maybe (ConInfo (VarShape sym)),
 Maybe (ConInfo (VarShape Concrete)))
_ -> [Char] -> [[Char]] -> SEval sym (SBit sym)
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"varModelPred" [[Char]
"malformed constructor"]
         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 SBit sym
sameTag SBit sym
sameFs

    (VarShape sym, VarShape Concrete)
_ -> [Char] -> [[Char]] -> SEval sym (SBit sym)
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"varModelPred" [[Char]
"variable shape mismatch!"]


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

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

  go :: FinType -> VarShape Concrete.Concrete -> Expr
  go :: FinType -> VarShape Concrete -> Expr
go FinType
ty VarShape Concrete
val =
    case (FinType
ty,VarShape Concrete
val) of
      (FTNominal NominalType
nt [Either Nat' TValue]
ts (FStruct 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 con :: Name
con = case NominalType -> NominalTypeDef
ntDef NominalType
nt of
                            Struct StructCon
c -> StructCon -> Name
ntConName StructCon
c
                            Enum {} -> [Char] -> [[Char]] -> Name
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"varToExpr" [[Char]
"Enum, expected Struct"]
                            Abstract {} -> [Char] -> [[Char]] -> Name
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"varToExpr"
                              [[Char]
"Abstract, expected Struct"]
                    f :: Expr
f = (Expr -> Either Nat' TValue -> Expr)
-> Expr -> [Either Nat' TValue] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Expr
x Either Nat' TValue
t -> Expr -> Prop -> Expr
ETApp Expr
x (Either Nat' TValue -> Prop
tNumValTy Either Nat' TValue
t)) (Name -> Expr
EVar Name
con) [Either Nat' TValue]
ts
                 in Expr -> Expr -> Expr
EApp Expr
f (RecordMap Ident Expr -> Expr
ERec RecordMap Ident Expr
efs)

      (FTNominal NominalType
nt [Either Nat' TValue]
ts (FEnum Vector (ConInfo FinType)
cons), VarEnum SInteger Concrete
tag Vector (ConInfo (VarShape Concrete))
conVs) ->
         (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
EApp Expr
conName [Expr]
args
         where
         tag' :: Int
tag' = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
SInteger Concrete
tag
         args :: [Expr]
args = case (Vector (ConInfo FinType)
cons Vector (ConInfo FinType) -> Int -> Maybe (ConInfo FinType)
forall a. Vector a -> Int -> Maybe a
Vector.!? Int
tag', Vector (ConInfo (VarShape Concrete))
conVs Vector (ConInfo (VarShape Concrete))
-> Int -> Maybe (ConInfo (VarShape Concrete))
forall a. Vector a -> Int -> Maybe a
Vector.!? Int
tag') of
                 (Just ConInfo FinType
conT, Just ConInfo (VarShape Concrete)
conV) ->
                    Vector Expr -> [Expr]
forall a. Vector a -> [a]
Vector.toList
                       ((FinType -> VarShape Concrete -> Expr)
-> Vector FinType -> Vector (VarShape Concrete) -> Vector Expr
forall a b c. (a -> b -> c) -> Vector a -> Vector b -> Vector c
Vector.zipWith FinType -> VarShape Concrete -> Expr
go (ConInfo FinType -> Vector FinType
forall a. ConInfo a -> Vector a
conFields ConInfo FinType
conT) (ConInfo (VarShape Concrete) -> Vector (VarShape Concrete)
forall a. ConInfo a -> Vector a
conFields ConInfo (VarShape Concrete)
conV))
                 (Maybe (ConInfo FinType), Maybe (ConInfo (VarShape Concrete)))
_ -> [Char] -> [[Char]] -> [Expr]
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"varToExpr" [[Char]
"Malformed constructor"]

         conName :: Expr
conName =
           case NominalType -> NominalTypeDef
ntDef NominalType
nt of
             Enum [EnumCon]
cs | EnumCon
c : [EnumCon]
_ <- (EnumCon -> Bool) -> [EnumCon] -> [EnumCon]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int
tag' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) (Int -> Bool) -> (EnumCon -> Int) -> EnumCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EnumCon -> Int
ecNumber ) [EnumCon]
cs ->
                (Expr -> Either Nat' TValue -> Expr)
-> Expr -> [Either Nat' TValue] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Expr
x Either Nat' TValue
t -> Expr -> Prop -> Expr
ETApp Expr
x (Either Nat' TValue -> Prop
tNumValTy Either Nat' TValue
t)) (Name -> Expr
EVar (EnumCon -> Name
ecName EnumCon
c)) [Either Nat' TValue]
ts

             NominalTypeDef
_ -> [Char] -> [[Char]] -> Expr
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"varToExpr" [[Char]
"Missing constructor"]

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

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

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

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

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

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

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

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

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

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