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

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}

module Cryptol.Eval.Value
  ( -- * GenericValue
    GenValue(..)
  , forceValue
  , Backend(..)
  , asciiMode

  , EvalOpts(..)
    -- ** Value introduction operations
  , word
  , lam
  , flam
  , tlam
  , nlam
  , ilam
  , mkSeq
    -- ** Value eliminators
  , fromVBit
  , fromVInteger
  , fromVRational
  , fromVFloat
  , fromVSeq
  , fromSeq
  , fromWordVal
  , asIndex
  , fromVWord
  , vWordLen
  , tryFromBits
  , fromVFun
  , fromVPoly
  , fromVNumPoly
  , fromVTuple
  , fromVRecord
  , lookupRecord
    -- ** Pretty printing
  , defaultPPOpts
  , ppValue
    -- * Merge and if/then/else
  , iteValue
  , mergeValue
  ) where

import Data.Ratio
import Numeric (showIntAtBase)

import Cryptol.Backend
import Cryptol.Backend.SeqMap
import qualified Cryptol.Backend.Arch as Arch
import Cryptol.Backend.Monad
  ( evalPanic, wordTooWide, CallStack, combineCallStacks )
import Cryptol.Backend.FloatHelpers (fpPP)
import Cryptol.Backend.WordValue

import Cryptol.Eval.Type

import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))

import Cryptol.Utils.Ident (Ident)
import Cryptol.Utils.Logger(Logger)
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.PP
import Cryptol.Utils.RecordMap

import GHC.Generics (Generic)

-- | Some options for evalutaion
data EvalOpts = EvalOpts
  { EvalOpts -> Logger
evalLogger :: Logger    -- ^ Where to print stuff (e.g., for @trace@)
  , EvalOpts -> PPOpts
evalPPOpts :: PPOpts    -- ^ How to pretty print things.
  }

-- Values ----------------------------------------------------------------------

-- | Generic value type, parameterized by bit and word types.
--
--   NOTE: we maintain an important invariant regarding sequence types.
--   'VSeq' must never be used for finite sequences of bits.
--   Always use the 'VWord' constructor instead!  Infinite sequences of bits
--   are handled by the 'VStream' constructor, just as for other types.
data GenValue sym
  = VRecord !(RecordMap Ident (SEval sym (GenValue sym))) -- ^ @ { .. } @
  | VTuple ![SEval sym (GenValue sym)]              -- ^ @ ( .. ) @
  | VBit !(SBit sym)                           -- ^ @ Bit    @
  | VInteger !(SInteger sym)                   -- ^ @ Integer @ or @ Z n @
  | VRational !(SRational sym)                 -- ^ @ Rational @
  | VFloat !(SFloat sym)
  | VSeq !Integer !(SeqMap sym (GenValue sym)) -- ^ @ [n]a   @
                                               --   Invariant: VSeq is never a sequence of bits
  | VWord !Integer !(WordValue sym)            -- ^ @ [n]Bit @
  | VStream !(SeqMap sym (GenValue sym))       -- ^ @ [inf]a @
  | VFun  CallStack (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -- ^ functions
  | VPoly CallStack (TValue -> SEval sym (GenValue sym))   -- ^ polymorphic values (kind *)
  | VNumPoly CallStack (Nat' -> SEval sym (GenValue sym))  -- ^ polymorphic values (kind #)
 deriving (forall x. GenValue sym -> Rep (GenValue sym) x)
-> (forall x. Rep (GenValue sym) x -> GenValue sym)
-> Generic (GenValue sym)
forall x. Rep (GenValue sym) x -> GenValue sym
forall x. GenValue sym -> Rep (GenValue sym) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall sym x. Rep (GenValue sym) x -> GenValue sym
forall sym x. GenValue sym -> Rep (GenValue sym) x
$cto :: forall sym x. Rep (GenValue sym) x -> GenValue sym
$cfrom :: forall sym x. GenValue sym -> Rep (GenValue sym) x
Generic


-- | Force the evaluation of a value
forceValue :: Backend sym => GenValue sym -> SEval sym ()
forceValue :: GenValue sym -> SEval sym ()
forceValue GenValue sym
v = case GenValue sym
v of
  VRecord RecordMap Ident (SEval sym (GenValue sym))
fs  -> (SEval sym (GenValue sym) -> SEval sym ())
-> RecordMap Ident (SEval sym (GenValue sym)) -> SEval sym ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (GenValue sym -> SEval sym ()
forall sym. Backend sym => GenValue sym -> SEval sym ()
forceValue (GenValue sym -> SEval sym ())
-> SEval sym (GenValue sym) -> SEval sym ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) RecordMap Ident (SEval sym (GenValue sym))
fs
  VTuple [SEval sym (GenValue sym)]
xs   -> (SEval sym (GenValue sym) -> SEval sym ())
-> [SEval sym (GenValue sym)] -> SEval sym ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (GenValue sym -> SEval sym ()
forall sym. Backend sym => GenValue sym -> SEval sym ()
forceValue (GenValue sym -> SEval sym ())
-> SEval sym (GenValue sym) -> SEval sym ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) [SEval sym (GenValue sym)]
xs
  VSeq Integer
n SeqMap sym (GenValue sym)
xs   -> (SEval sym (GenValue sym) -> SEval sym ())
-> [SEval sym (GenValue sym)] -> SEval sym ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (GenValue sym -> SEval sym ()
forall sym. Backend sym => GenValue sym -> SEval sym ()
forceValue (GenValue sym -> SEval sym ())
-> SEval sym (GenValue sym) -> SEval sym ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) (Integer -> SeqMap sym (GenValue sym) -> [SEval sym (GenValue sym)]
forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n SeqMap sym (GenValue sym)
xs)
  VBit SBit sym
b      -> SBit sym -> SEval sym () -> SEval sym ()
seq SBit sym
b (() -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  VInteger SInteger sym
i  -> SInteger sym -> SEval sym () -> SEval sym ()
seq SInteger sym
i (() -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  VRational SRational sym
q -> SRational sym -> SEval sym () -> SEval sym ()
seq SRational sym
q (() -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  VFloat SFloat sym
f    -> SFloat sym -> SEval sym () -> SEval sym ()
seq SFloat sym
f (() -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  VWord Integer
_ WordValue sym
wv  -> WordValue sym -> SEval sym ()
forall sym. Backend sym => WordValue sym -> SEval sym ()
forceWordValue WordValue sym
wv
  VStream SeqMap sym (GenValue sym)
_   -> () -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  VFun{}      -> () -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  VPoly{}     -> () -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  VNumPoly{}  -> () -> SEval sym ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()



instance Show (GenValue sym) where
  show :: GenValue sym -> String
show GenValue sym
v = case GenValue sym
v of
    VRecord RecordMap Ident (SEval sym (GenValue sym))
fs -> String
"record:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Ident] -> String
forall a. Show a => a -> String
show (RecordMap Ident (SEval sym (GenValue sym)) -> [Ident]
forall a b. RecordMap a b -> [a]
displayOrder RecordMap Ident (SEval sym (GenValue sym))
fs)
    VTuple [SEval sym (GenValue sym)]
xs  -> String
"tuple:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([SEval sym (GenValue sym)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SEval sym (GenValue sym)]
xs)
    VBit SBit sym
_     -> String
"bit"
    VInteger SInteger sym
_ -> String
"integer"
    VRational SRational sym
_ -> String
"rational"
    VFloat SFloat sym
_   -> String
"float"
    VSeq Integer
n SeqMap sym (GenValue sym)
_   -> String
"seq:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
    VWord Integer
n WordValue sym
_  -> String
"word:"  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
    VStream SeqMap sym (GenValue sym)
_  -> String
"stream"
    VFun{}     -> String
"fun"
    VPoly{}    -> String
"poly"
    VNumPoly{} -> String
"numpoly"

-- Pretty Printing -------------------------------------------------------------

ppValue :: forall sym.
  Backend sym =>
  sym ->
  PPOpts ->
  GenValue sym ->
  SEval sym Doc
ppValue :: sym -> PPOpts -> GenValue sym -> SEval sym Doc
ppValue sym
x PPOpts
opts = GenValue sym -> SEval sym Doc
loop
  where
  loop :: GenValue sym -> SEval sym Doc
  loop :: GenValue sym -> SEval sym Doc
loop GenValue sym
val = case GenValue sym
val of
    VRecord RecordMap Ident (SEval sym (GenValue sym))
fs         -> do RecordMap Ident Doc
fs' <- (SEval sym (GenValue sym) -> SEval sym Doc)
-> RecordMap Ident (SEval sym (GenValue sym))
-> SEval sym (RecordMap Ident Doc)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (SEval sym (GenValue sym)
-> (GenValue sym -> SEval sym Doc) -> SEval sym Doc
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= GenValue sym -> SEval sym Doc
loop) RecordMap Ident (SEval sym (GenValue sym))
fs
                             Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
ppRecord (((Ident, Doc) -> Doc) -> [(Ident, Doc)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Ident, Doc) -> Doc
forall a. PP a => (a, Doc) -> Doc
ppField (RecordMap Ident Doc -> [(Ident, Doc)]
fields RecordMap Ident Doc
fs'))
      where
      ppField :: (a, Doc) -> Doc
ppField (a
f,Doc
r) = a -> Doc
forall a. PP a => a -> Doc
pp a
f Doc -> Doc -> Doc
<+> Char -> Doc
char Char
'=' Doc -> Doc -> Doc
<+> Doc
r
    VTuple [SEval sym (GenValue sym)]
vals        -> do [Doc]
vals' <- (SEval sym (GenValue sym) -> SEval sym Doc)
-> [SEval sym (GenValue sym)] -> SEval sym [Doc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (SEval sym (GenValue sym)
-> (GenValue sym -> SEval sym Doc) -> SEval sym Doc
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=GenValue sym -> SEval sym Doc
loop) [SEval sym (GenValue sym)]
vals
                             Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
ppTuple [Doc]
vals'
    VBit SBit sym
b             -> sym -> SBit sym -> SEval sym Doc
forall sym. Backend sym => sym -> SBit sym -> SEval sym Doc
ppSBit sym
x SBit sym
b
    VInteger SInteger sym
i         -> sym -> SInteger sym -> SEval sym Doc
forall sym. Backend sym => sym -> SInteger sym -> SEval sym Doc
ppSInteger sym
x SInteger sym
i
    VRational SRational sym
q        -> sym -> SRational sym -> SEval sym Doc
forall sym. Backend sym => sym -> SRational sym -> SEval sym Doc
ppSRational sym
x SRational sym
q
    VFloat SFloat sym
i           -> sym -> PPOpts -> SFloat sym -> SEval sym Doc
forall sym.
Backend sym =>
sym -> PPOpts -> SFloat sym -> SEval sym Doc
ppSFloat sym
x PPOpts
opts SFloat sym
i
    VSeq Integer
sz SeqMap sym (GenValue sym)
vals       -> Integer -> SeqMap sym (GenValue sym) -> SEval sym Doc
ppWordSeq Integer
sz SeqMap sym (GenValue sym)
vals
    VWord Integer
_ WordValue sym
wv         -> WordValue sym -> SEval sym Doc
ppWordVal WordValue sym
wv
    VStream SeqMap sym (GenValue sym)
vals       -> do [Doc]
vals' <- (SEval sym (GenValue sym) -> SEval sym Doc)
-> [SEval sym (GenValue sym)] -> SEval sym [Doc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (SEval sym (GenValue sym)
-> (GenValue sym -> SEval sym Doc) -> SEval sym Doc
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=GenValue sym -> SEval sym Doc
loop) ([SEval sym (GenValue sym)] -> SEval sym [Doc])
-> [SEval sym (GenValue sym)] -> SEval sym [Doc]
forall a b. (a -> b) -> a -> b
$ Int -> SeqMap sym (GenValue sym) -> [SEval sym (GenValue sym)]
forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap (PPOpts -> Int
useInfLength PPOpts
opts) SeqMap sym (GenValue sym)
vals
                             Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
ppList ( [Doc]
vals' [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Doc
text String
"..."] )
    VFun{}             -> Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"<function>"
    VPoly{}            -> Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"<polymorphic value>"
    VNumPoly{}         -> Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"<polymorphic value>"

  fields :: RecordMap Ident Doc -> [(Ident, Doc)]
  fields :: RecordMap Ident Doc -> [(Ident, Doc)]
fields = case PPOpts -> FieldOrder
useFieldOrder PPOpts
opts of
    FieldOrder
DisplayOrder -> RecordMap Ident Doc -> [(Ident, Doc)]
forall a b. (Show a, Ord a) => RecordMap a b -> [(a, b)]
displayFields
    FieldOrder
CanonicalOrder -> RecordMap Ident Doc -> [(Ident, Doc)]
forall a b. RecordMap a b -> [(a, b)]
canonicalFields

  ppWordVal :: WordValue sym -> SEval sym Doc
  ppWordVal :: WordValue sym -> SEval sym Doc
ppWordVal WordValue sym
w = sym -> PPOpts -> SWord sym -> SEval sym Doc
forall sym.
Backend sym =>
sym -> PPOpts -> SWord sym -> SEval sym Doc
ppSWord sym
x PPOpts
opts (SWord sym -> SEval sym Doc)
-> SEval sym (SWord sym) -> SEval sym Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> WordValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
x WordValue sym
w

  ppWordSeq :: Integer -> SeqMap sym (GenValue sym) -> SEval sym Doc
  ppWordSeq :: Integer -> SeqMap sym (GenValue sym) -> SEval sym Doc
ppWordSeq Integer
sz SeqMap sym (GenValue sym)
vals = do
    [GenValue sym]
ws <- [SEval sym (GenValue sym)] -> SEval sym [GenValue sym]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (Integer -> SeqMap sym (GenValue sym) -> [SEval sym (GenValue sym)]
forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
sz SeqMap sym (GenValue sym)
vals)
    case [GenValue sym]
ws of
      GenValue sym
w : [GenValue sym]
_
        | Just Integer
l <- GenValue sym -> Maybe Integer
forall sym. Backend sym => GenValue sym -> Maybe Integer
vWordLen GenValue sym
w
        , PPOpts -> Integer -> Bool
asciiMode PPOpts
opts Integer
l
        -> do [SWord sym]
vs <- (GenValue sym -> SEval sym (SWord sym))
-> [GenValue sym] -> SEval sym [SWord sym]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (sym -> String -> GenValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
x String
"ppWordSeq") [GenValue sym]
ws
              case (SWord sym -> Maybe Char) -> [SWord sym] -> Maybe String
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (sym -> SWord sym -> Maybe Char
forall sym. Backend sym => sym -> SWord sym -> Maybe Char
wordAsChar sym
x) [SWord sym]
vs of
                Just String
str -> Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (ShowS
forall a. Show a => a -> String
show String
str)
                Maybe String
_ -> do [Doc]
vs' <- (SWord sym -> SEval sym Doc) -> [SWord sym] -> SEval sym [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (sym -> PPOpts -> SWord sym -> SEval sym Doc
forall sym.
Backend sym =>
sym -> PPOpts -> SWord sym -> SEval sym Doc
ppSWord sym
x PPOpts
opts) [SWord sym]
vs
                        Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
ppList [Doc]
vs'
      [GenValue sym]
_ -> do [Doc]
ws' <- (GenValue sym -> SEval sym Doc)
-> [GenValue sym] -> SEval sym [Doc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse GenValue sym -> SEval sym Doc
loop [GenValue sym]
ws
              Doc -> SEval sym Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> SEval sym Doc) -> Doc -> SEval sym Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
ppList [Doc]
ws'

ppSBit :: Backend sym => sym -> SBit sym -> SEval sym Doc
ppSBit :: sym -> SBit sym -> SEval sym Doc
ppSBit sym
sym SBit sym
b =
  case sym -> SBit sym -> Maybe Bool
forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
bitAsLit sym
sym SBit sym
b of
    Just Bool
True  -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"True")
    Just Bool
False -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"False")
    Maybe Bool
Nothing    -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"?")

ppSInteger :: Backend sym => sym -> SInteger sym -> SEval sym Doc
ppSInteger :: sym -> SInteger sym -> SEval sym Doc
ppSInteger sym
sym SInteger sym
x =
  case sym -> SInteger sym -> Maybe Integer
forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
sym SInteger sym
x of
    Just Integer
i  -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Doc
integer Integer
i)
    Maybe Integer
Nothing -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"[?]")

ppSFloat :: Backend sym => sym -> PPOpts -> SFloat sym -> SEval sym Doc
ppSFloat :: sym -> PPOpts -> SFloat sym -> SEval sym Doc
ppSFloat sym
sym PPOpts
opts SFloat sym
x =
  case sym -> SFloat sym -> Maybe BF
forall sym. Backend sym => sym -> SFloat sym -> Maybe BF
fpAsLit sym
sym SFloat sym
x of
    Just BF
fp -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PPOpts -> BF -> Doc
fpPP PPOpts
opts BF
fp)
    Maybe BF
Nothing -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"[?]")

ppSRational :: Backend sym => sym -> SRational sym -> SEval sym Doc
ppSRational :: sym -> SRational sym -> SEval sym Doc
ppSRational sym
sym (SRational SInteger sym
n SInteger sym
d)
  | Just Integer
ni <- sym -> SInteger sym -> Maybe Integer
forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
sym SInteger sym
n
  , Just Integer
di <- sym -> SInteger sym -> Maybe Integer
forall sym. Backend sym => sym -> SInteger sym -> Maybe Integer
integerAsLit sym
sym SInteger sym
d
  = let q :: Ratio Integer
q = Integer
ni Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% Integer
di in
      Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"(ratio" Doc -> Doc -> Doc
<+> Integer -> Doc
integer (Ratio Integer -> Integer
forall a. Ratio a -> a
numerator Ratio Integer
q) Doc -> Doc -> Doc
<+> (Integer -> Doc
integer (Ratio Integer -> Integer
forall a. Ratio a -> a
denominator Ratio Integer
q) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
")"))

  | Bool
otherwise
  = do Doc
n' <- sym -> SInteger sym -> SEval sym Doc
forall sym. Backend sym => sym -> SInteger sym -> SEval sym Doc
ppSInteger sym
sym SInteger sym
n
       Doc
d' <- sym -> SInteger sym -> SEval sym Doc
forall sym. Backend sym => sym -> SInteger sym -> SEval sym Doc
ppSInteger sym
sym SInteger sym
d
       Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"(ratio" Doc -> Doc -> Doc
<+> Doc
n' Doc -> Doc -> Doc
<+> (Doc
d' Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
")"))

ppSWord :: Backend sym => sym -> PPOpts -> SWord sym -> SEval sym Doc
ppSWord :: sym -> PPOpts -> SWord sym -> SEval sym Doc
ppSWord sym
sym PPOpts
opts SWord sym
bv
  | PPOpts -> Integer -> Bool
asciiMode PPOpts
opts Integer
width =
      case sym -> SWord sym -> Maybe (Integer, Integer)
forall sym.
Backend sym =>
sym -> SWord sym -> Maybe (Integer, Integer)
wordAsLit sym
sym SWord sym
bv of
        Just (Integer
_,Integer
i) -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text (Char -> String
forall a. Show a => a -> String
show (Int -> Char
forall a. Enum a => Int -> a
toEnum (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i) :: Char)))
        Maybe (Integer, Integer)
Nothing    -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"?")

  | Bool
otherwise =
      case sym -> SWord sym -> Maybe (Integer, Integer)
forall sym.
Backend sym =>
sym -> SWord sym -> Maybe (Integer, Integer)
wordAsLit sym
sym SWord sym
bv of
        Just (Integer
_,Integer
i) ->
          let val :: String
val = Integer -> String
value Integer
i in
          Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Doc
prefix (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
val) Doc -> Doc -> Doc
<.> String -> Doc
text String
val)
        Maybe (Integer, Integer)
Nothing
          | Int
base Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2  -> Integer -> String -> SEval sym Doc
sliceDigits Integer
1 String
"0b"
          | Int
base Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
8  -> Integer -> String -> SEval sym Doc
sliceDigits Integer
3 String
"0o"
          | Int
base Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
16 -> Integer -> String -> SEval sym Doc
sliceDigits Integer
4 String
"0x"
          | Bool
otherwise  -> Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
"[?]")

  where
  width :: Integer
width = sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
bv

  base :: Int
base = if PPOpts -> Int
useBase PPOpts
opts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
36 then Int
10 else PPOpts -> Int
useBase PPOpts
opts

  padding :: Int -> Int -> Doc
padding Int
bitsPerDigit Int
len = String -> Doc
text (Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
padLen Char
'0')
    where
    padLen :: Int
padLen | Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0     = Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
           | Bool
otherwise = Int
d

    (Int
d,Int
m) = (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
width Int -> Int -> Int
forall a. Num a => a -> a -> a
- (Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
bitsPerDigit))
                   Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
`divMod` Int
bitsPerDigit

  prefix :: Int -> Doc
prefix Int
len = case Int
base of
    Int
2  -> String -> Doc
text String
"0b" Doc -> Doc -> Doc
<.> Int -> Int -> Doc
padding Int
1 Int
len
    Int
8  -> String -> Doc
text String
"0o" Doc -> Doc -> Doc
<.> Int -> Int -> Doc
padding Int
3 Int
len
    Int
10 -> Doc
forall a. Monoid a => a
mempty
    Int
16 -> String -> Doc
text String
"0x" Doc -> Doc -> Doc
<.> Int -> Int -> Doc
padding Int
4 Int
len
    Int
_  -> String -> Doc
text String
"0"  Doc -> Doc -> Doc
<.> Char -> Doc
char Char
'<' Doc -> Doc -> Doc
<.> Int -> Doc
int Int
base Doc -> Doc -> Doc
<.> Char -> Doc
char Char
'>'

  value :: Integer -> String
value Integer
i = Integer -> (Int -> Char) -> Integer -> ShowS
forall a. (Integral a, Show a) => a -> (Int -> Char) -> a -> ShowS
showIntAtBase (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
base) (String
digits String -> Int -> Char
forall a. [a] -> Int -> a
!!) Integer
i String
""
  digits :: String
digits  = String
"0123456789abcdefghijklmnopqrstuvwxyz"

  toDigit :: SWord sym -> Char
toDigit SWord sym
w =
    case sym -> SWord sym -> Maybe (Integer, Integer)
forall sym.
Backend sym =>
sym -> SWord sym -> Maybe (Integer, Integer)
wordAsLit sym
sym SWord sym
w of
      Just (Integer
_,Integer
i) | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
36 -> String
digits String -> Int -> Char
forall a. [a] -> Int -> a
!! Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i
      Maybe (Integer, Integer)
_ -> Char
'?'

  sliceDigits :: Integer -> String -> SEval sym Doc
sliceDigits Integer
bits String
pfx =
    do [SWord sym]
ws <- Integer -> [SWord sym] -> SWord sym -> SEval sym [SWord sym]
goDigits Integer
bits [] SWord sym
bv
       let ds :: String
ds = (SWord sym -> Char) -> [SWord sym] -> String
forall a b. (a -> b) -> [a] -> [b]
map SWord sym -> Char
toDigit [SWord sym]
ws
       Doc -> SEval sym Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
pfx Doc -> Doc -> Doc
<.> String -> Doc
text String
ds)

  goDigits :: Integer -> [SWord sym] -> SWord sym -> SEval sym [SWord sym]
goDigits Integer
bits [SWord sym]
ds SWord sym
w
    | sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
bits =
        do (SWord sym
hi,SWord sym
lo) <- sym
-> Integer
-> Integer
-> SWord sym
-> SEval sym (SWord sym, SWord sym)
forall sym.
Backend sym =>
sym
-> Integer
-> Integer
-> SWord sym
-> SEval sym (SWord sym, SWord sym)
splitWord sym
sym (sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
bits) Integer
bits SWord sym
w
           Integer -> [SWord sym] -> SWord sym -> SEval sym [SWord sym]
goDigits Integer
bits (SWord sym
loSWord sym -> [SWord sym] -> [SWord sym]
forall a. a -> [a] -> [a]
:[SWord sym]
ds) SWord sym
hi

    | sym -> SWord sym -> Integer
forall sym. Backend sym => sym -> SWord sym -> Integer
wordLen sym
sym SWord sym
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 = [SWord sym] -> SEval sym [SWord sym]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SWord sym
wSWord sym -> [SWord sym] -> [SWord sym]
forall a. a -> [a] -> [a]
:[SWord sym]
ds)

    | Bool
otherwise          = [SWord sym] -> SEval sym [SWord sym]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [SWord sym]
ds

-- Value Constructors ----------------------------------------------------------

-- | Create a packed word of n bits.
word :: Backend sym => sym -> Integer -> Integer -> SEval sym (GenValue sym)
word :: sym -> Integer -> Integer -> SEval sym (GenValue sym)
word sym
sym Integer
n Integer
i
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
Arch.maxBigIntWidth = Integer -> SEval sym (GenValue sym)
forall a. Integer -> a
wordTooWide Integer
n
  | Bool
otherwise                = Integer -> WordValue sym -> GenValue sym
forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
n (WordValue sym -> GenValue sym)
-> (SWord sym -> WordValue sym) -> SWord sym -> GenValue sym
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SWord sym -> WordValue sym
forall sym. SWord sym -> WordValue sym
wordVal (SWord sym -> GenValue sym)
-> SEval sym (SWord sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Integer -> Integer -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (SWord sym)
wordLit sym
sym Integer
n Integer
i


-- | Construct a function value
lam :: Backend sym => sym -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
lam :: sym
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
lam sym
sym SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f = CallStack
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
CallStack
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
VFun (CallStack
 -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> SEval sym CallStack
-> SEval
     sym
     ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
      -> GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SEval sym CallStack
forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym SEval
  sym
  ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
   -> GenValue sym)
-> SEval sym (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
forall (f :: * -> *) a. Applicative f => a -> f a
pure SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f

-- | Functions that assume floating point inputs
flam :: Backend sym => sym ->
        (SFloat sym -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
flam :: sym
-> (SFloat sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
flam sym
sym SFloat sym -> SEval sym (GenValue sym)
f = CallStack
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
forall sym.
CallStack
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
VFun (CallStack
 -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> GenValue sym)
-> SEval sym CallStack
-> SEval
     sym
     ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
      -> GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SEval sym CallStack
forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym SEval
  sym
  ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
   -> GenValue sym)
-> SEval sym (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (\SEval sym (GenValue sym)
arg -> SEval sym (GenValue sym)
arg SEval sym (GenValue sym)
-> (GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SFloat sym -> SEval sym (GenValue sym)
f (SFloat sym -> SEval sym (GenValue sym))
-> (GenValue sym -> SFloat sym)
-> GenValue sym
-> SEval sym (GenValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenValue sym -> SFloat sym
forall sym. GenValue sym -> SFloat sym
fromVFloat)

-- | A type lambda that expects a 'Type'.
tlam :: Backend sym => sym -> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
tlam :: sym
-> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
tlam sym
sym TValue -> SEval sym (GenValue sym)
f = CallStack -> (TValue -> SEval sym (GenValue sym)) -> GenValue sym
forall sym.
CallStack -> (TValue -> SEval sym (GenValue sym)) -> GenValue sym
VPoly (CallStack -> (TValue -> SEval sym (GenValue sym)) -> GenValue sym)
-> SEval sym CallStack
-> SEval sym ((TValue -> SEval sym (GenValue sym)) -> GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SEval sym CallStack
forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym SEval sym ((TValue -> SEval sym (GenValue sym)) -> GenValue sym)
-> SEval sym (TValue -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (TValue -> SEval sym (GenValue sym))
-> SEval sym (TValue -> SEval sym (GenValue sym))
forall (f :: * -> *) a. Applicative f => a -> f a
pure TValue -> SEval sym (GenValue sym)
f

-- | A type lambda that expects a 'Type' of kind #.
nlam :: Backend sym => sym -> (Nat' -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
nlam :: sym
-> (Nat' -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
nlam sym
sym Nat' -> SEval sym (GenValue sym)
f = CallStack -> (Nat' -> SEval sym (GenValue sym)) -> GenValue sym
forall sym.
CallStack -> (Nat' -> SEval sym (GenValue sym)) -> GenValue sym
VNumPoly (CallStack -> (Nat' -> SEval sym (GenValue sym)) -> GenValue sym)
-> SEval sym CallStack
-> SEval sym ((Nat' -> SEval sym (GenValue sym)) -> GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SEval sym CallStack
forall sym. Backend sym => sym -> SEval sym CallStack
sGetCallStack sym
sym SEval sym ((Nat' -> SEval sym (GenValue sym)) -> GenValue sym)
-> SEval sym (Nat' -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Nat' -> SEval sym (GenValue sym))
-> SEval sym (Nat' -> SEval sym (GenValue sym))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nat' -> SEval sym (GenValue sym)
f

-- | A type lambda that expects a finite numeric type.
ilam :: Backend sym => sym -> (Integer -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
ilam :: sym
-> (Integer -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
ilam sym
sym Integer -> SEval sym (GenValue sym)
f =
   sym
-> (Nat' -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> (Nat' -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
nlam sym
sym (\Nat'
n -> case Nat'
n of
                     Nat Integer
i -> Integer -> SEval sym (GenValue sym)
f Integer
i
                     Nat'
Inf   -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"ilam" [ String
"Unexpected `inf`" ])

-- | Construct either a finite sequence, or a stream.  In the finite case,
-- record whether or not the elements were bits, to aid pretty-printing.
mkSeq :: Backend sym => sym -> Nat' -> TValue -> SeqMap sym (GenValue sym) -> SEval sym (GenValue sym)
mkSeq :: sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
mkSeq sym
sym Nat'
len TValue
elty SeqMap sym (GenValue sym)
vals = case Nat'
len of
  Nat Integer
n
    | TValue -> Bool
isTBit TValue
elty -> Integer -> WordValue sym -> GenValue sym
forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
n (WordValue sym -> GenValue sym)
-> SEval sym (WordValue sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> Integer -> SeqMap sym (SBit sym) -> SEval sym (WordValue sym)
bitmapWordVal sym
sym Integer
n (GenValue sym -> SBit sym
forall sym. GenValue sym -> SBit sym
fromVBit (GenValue sym -> SBit sym)
-> SeqMap sym (GenValue sym) -> SeqMap sym (SBit sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqMap sym (GenValue sym)
vals)
    | Bool
otherwise   -> GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap sym (GenValue sym) -> GenValue sym
forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
n SeqMap sym (GenValue sym)
vals
  Nat'
Inf             -> GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ SeqMap sym (GenValue sym) -> GenValue sym
forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream SeqMap sym (GenValue sym)
vals


-- Value Destructors -----------------------------------------------------------

-- | Extract a bit value.
fromVBit :: GenValue sym -> SBit sym
fromVBit :: GenValue sym -> SBit sym
fromVBit GenValue sym
val = case GenValue sym
val of
  VBit SBit sym
b -> SBit sym
b
  GenValue sym
_      -> String -> [String] -> SBit sym
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVBit" [String
"not a Bit", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

-- | Extract an integer value.
fromVInteger :: GenValue sym -> SInteger sym
fromVInteger :: GenValue sym -> SInteger sym
fromVInteger GenValue sym
val = case GenValue sym
val of
  VInteger SInteger sym
i -> SInteger sym
i
  GenValue sym
_      -> String -> [String] -> SInteger sym
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVInteger" [String
"not an Integer", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

-- | Extract a rational value.
fromVRational :: GenValue sym -> SRational sym
fromVRational :: GenValue sym -> SRational sym
fromVRational GenValue sym
val = case GenValue sym
val of
  VRational SRational sym
q -> SRational sym
q
  GenValue sym
_      -> String -> [String] -> SRational sym
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVRational" [String
"not a Rational", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

-- | Extract a finite sequence value.
fromVSeq :: GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq :: GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq GenValue sym
val = case GenValue sym
val of
  VSeq Integer
_ SeqMap sym (GenValue sym)
vs -> SeqMap sym (GenValue sym)
vs
  GenValue sym
_         -> String -> [String] -> SeqMap sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVSeq" [String
"not a sequence", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

-- | Extract a sequence.
fromSeq :: Backend sym => String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq :: String -> GenValue sym -> SEval sym (SeqMap sym (GenValue sym))
fromSeq String
msg GenValue sym
val = case GenValue sym
val of
  VSeq Integer
_ SeqMap sym (GenValue sym)
vs   -> SeqMap sym (GenValue sym) -> SEval sym (SeqMap sym (GenValue sym))
forall (m :: * -> *) a. Monad m => a -> m a
return SeqMap sym (GenValue sym)
vs
  VStream SeqMap sym (GenValue sym)
vs  -> SeqMap sym (GenValue sym) -> SEval sym (SeqMap sym (GenValue sym))
forall (m :: * -> *) a. Monad m => a -> m a
return SeqMap sym (GenValue sym)
vs
  GenValue sym
_           -> String -> [String] -> SEval sym (SeqMap sym (GenValue sym))
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromSeq" [String
"not a sequence", String
msg, GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

fromWordVal :: Backend sym => String -> GenValue sym -> WordValue sym
fromWordVal :: String -> GenValue sym -> WordValue sym
fromWordVal String
_msg (VWord Integer
_ WordValue sym
wval) = WordValue sym
wval
fromWordVal String
msg GenValue sym
val = String -> [String] -> WordValue sym
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromWordVal" [String
"not a word value", String
msg, GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

asIndex :: Backend sym =>
  sym -> String -> TValue -> GenValue sym -> Either (SInteger sym) (WordValue sym)
asIndex :: sym
-> String
-> TValue
-> GenValue sym
-> Either (SInteger sym) (WordValue sym)
asIndex sym
_sym String
_msg TValue
TVInteger (VInteger SInteger sym
i) = SInteger sym -> Either (SInteger sym) (WordValue sym)
forall a b. a -> Either a b
Left SInteger sym
i
asIndex sym
_sym String
_msg TValue
_ (VWord Integer
_ WordValue sym
wval) = WordValue sym -> Either (SInteger sym) (WordValue sym)
forall a b. b -> Either a b
Right WordValue sym
wval
asIndex sym
_sym  String
msg TValue
_ GenValue sym
val = String -> [String] -> Either (SInteger sym) (WordValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"asIndex" [String
"not an index value", String
msg, GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

-- | Extract a packed word.
fromVWord :: Backend sym => sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord :: sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym String
_msg (VWord Integer
_ WordValue sym
wval) = sym -> WordValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal sym
sym WordValue sym
wval
fromVWord sym
_ String
msg GenValue sym
val = String -> [String] -> SEval sym (SWord sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVWord" [String
"not a word", String
msg, GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

vWordLen :: Backend sym => GenValue sym -> Maybe Integer
vWordLen :: GenValue sym -> Maybe Integer
vWordLen GenValue sym
val = case GenValue sym
val of
  VWord Integer
n WordValue sym
_wv              -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n
  GenValue sym
_                        -> Maybe Integer
forall a. Maybe a
Nothing

-- | If the given list of values are all fully-evaluated thunks
--   containing bits, return a packed word built from the same bits.
--   However, if any value is not a fully-evaluated bit, return 'Nothing'.
tryFromBits :: Backend sym => sym -> [SEval sym (GenValue sym)] -> SEval sym (Maybe (SWord sym))
tryFromBits :: sym -> [SEval sym (GenValue sym)] -> SEval sym (Maybe (SWord sym))
tryFromBits sym
sym = ([SBit sym] -> [SBit sym])
-> [SEval sym (GenValue sym)] -> SEval sym (Maybe (SWord sym))
go [SBit sym] -> [SBit sym]
forall a. a -> a
id
  where
  go :: ([SBit sym] -> [SBit sym])
-> [SEval sym (GenValue sym)] -> SEval sym (Maybe (SWord sym))
go [SBit sym] -> [SBit sym]
f [] = SWord sym -> Maybe (SWord sym)
forall a. a -> Maybe a
Just (SWord sym -> Maybe (SWord sym))
-> SEval sym (SWord sym) -> SEval sym (Maybe (SWord sym))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (sym -> [SBit sym] -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> [SBit sym] -> SEval sym (SWord sym)
packWord sym
sym ([SBit sym] -> [SBit sym]
f []))
  go [SBit sym] -> [SBit sym]
f (SEval sym (GenValue sym)
v : [SEval sym (GenValue sym)]
vs) =
    sym -> SEval sym (GenValue sym) -> SEval sym (Maybe (GenValue sym))
forall sym a.
Backend sym =>
sym -> SEval sym a -> SEval sym (Maybe a)
isReady sym
sym SEval sym (GenValue sym)
v SEval sym (Maybe (GenValue sym))
-> (Maybe (GenValue sym) -> SEval sym (Maybe (SWord sym)))
-> SEval sym (Maybe (SWord sym))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just GenValue sym
v' -> ([SBit sym] -> [SBit sym])
-> [SEval sym (GenValue sym)] -> SEval sym (Maybe (SWord sym))
go ([SBit sym] -> [SBit sym]
f ([SBit sym] -> [SBit sym])
-> ([SBit sym] -> [SBit sym]) -> [SBit sym] -> [SBit sym]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((GenValue sym -> SBit sym
forall sym. GenValue sym -> SBit sym
fromVBit GenValue sym
v')SBit sym -> [SBit sym] -> [SBit sym]
forall a. a -> [a] -> [a]
:)) [SEval sym (GenValue sym)]
vs
      Maybe (GenValue sym)
Nothing -> Maybe (SWord sym) -> SEval sym (Maybe (SWord sym))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (SWord sym)
forall a. Maybe a
Nothing

-- | Extract a function from a value.
fromVFun :: Backend sym => sym -> GenValue sym -> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
fromVFun :: sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym GenValue sym
val = case GenValue sym
val of
  VFun CallStack
fnstk SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f ->
    \SEval sym (GenValue sym)
x -> sym
-> (CallStack -> CallStack)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym a.
Backend sym =>
sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
sModifyCallStack sym
sym (\CallStack
stk -> CallStack -> CallStack -> CallStack
combineCallStacks CallStack
stk CallStack
fnstk) (SEval sym (GenValue sym) -> SEval sym (GenValue sym)
f SEval sym (GenValue sym)
x)
  GenValue sym
_ -> String
-> [String] -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVFun" [String
"not a function", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

-- | Extract a polymorphic function from a value.
fromVPoly :: Backend sym => sym -> GenValue sym -> (TValue -> SEval sym (GenValue sym))
fromVPoly :: sym -> GenValue sym -> TValue -> SEval sym (GenValue sym)
fromVPoly sym
sym GenValue sym
val = case GenValue sym
val of
  VPoly CallStack
fnstk TValue -> SEval sym (GenValue sym)
f ->
    \TValue
x -> sym
-> (CallStack -> CallStack)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym a.
Backend sym =>
sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
sModifyCallStack sym
sym (\CallStack
stk -> CallStack -> CallStack -> CallStack
combineCallStacks CallStack
stk CallStack
fnstk) (TValue -> SEval sym (GenValue sym)
f TValue
x)
  GenValue sym
_ -> String -> [String] -> TValue -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVPoly" [String
"not a polymorphic value", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

-- | Extract a polymorphic function from a value.
fromVNumPoly :: Backend sym => sym -> GenValue sym -> (Nat' -> SEval sym (GenValue sym))
fromVNumPoly :: sym -> GenValue sym -> Nat' -> SEval sym (GenValue sym)
fromVNumPoly sym
sym GenValue sym
val = case GenValue sym
val of
  VNumPoly CallStack
fnstk Nat' -> SEval sym (GenValue sym)
f ->
    \Nat'
x -> sym
-> (CallStack -> CallStack)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym a.
Backend sym =>
sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
sModifyCallStack sym
sym (\CallStack
stk -> CallStack -> CallStack -> CallStack
combineCallStacks CallStack
stk CallStack
fnstk) (Nat' -> SEval sym (GenValue sym)
f Nat'
x)
  GenValue sym
_  -> String -> [String] -> Nat' -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVNumPoly" [String
"not a polymorphic value", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

-- | Extract a tuple from a value.
fromVTuple :: GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple :: GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple GenValue sym
val = case GenValue sym
val of
  VTuple [SEval sym (GenValue sym)]
vs -> [SEval sym (GenValue sym)]
vs
  GenValue sym
_         -> String -> [String] -> [SEval sym (GenValue sym)]
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVTuple" [String
"not a tuple", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

-- | Extract a record from a value.
fromVRecord :: GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
fromVRecord :: GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
fromVRecord GenValue sym
val = case GenValue sym
val of
  VRecord RecordMap Ident (SEval sym (GenValue sym))
fs -> RecordMap Ident (SEval sym (GenValue sym))
fs
  GenValue sym
_          -> String -> [String] -> RecordMap Ident (SEval sym (GenValue sym))
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVRecord" [String
"not a record", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

fromVFloat :: GenValue sym -> SFloat sym
fromVFloat :: GenValue sym -> SFloat sym
fromVFloat GenValue sym
val =
  case GenValue sym
val of
    VFloat SFloat sym
x -> SFloat sym
x
    GenValue sym
_        -> String -> [String] -> SFloat sym
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"fromVFloat" [String
"not a Float", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]

-- | Lookup a field in a record.
lookupRecord :: Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord :: Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
f GenValue sym
val =
  case Ident
-> RecordMap Ident (SEval sym (GenValue sym))
-> Maybe (SEval sym (GenValue sym))
forall a b. Ord a => a -> RecordMap a b -> Maybe b
lookupField Ident
f (GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
forall sym.
GenValue sym -> RecordMap Ident (SEval sym (GenValue sym))
fromVRecord GenValue sym
val) of
    Just SEval sym (GenValue sym)
x  -> SEval sym (GenValue sym)
x
    Maybe (SEval sym (GenValue sym))
Nothing -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"lookupRecord" [String
"malformed record", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
val]


-- Merge and if/then/else

{-# INLINE iteValue #-}
iteValue :: Backend sym =>
  sym ->
  SBit sym ->
  SEval sym (GenValue sym) ->
  SEval sym (GenValue sym) ->
  SEval sym (GenValue sym)
iteValue :: sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue sym
sym SBit sym
b SEval sym (GenValue sym)
x SEval sym (GenValue sym)
y
  | Just Bool
True  <- sym -> SBit sym -> Maybe Bool
forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
bitAsLit sym
sym SBit sym
b = SEval sym (GenValue sym)
x
  | Just Bool
False <- sym -> SBit sym -> Maybe Bool
forall sym. Backend sym => sym -> SBit sym -> Maybe Bool
bitAsLit sym
sym SBit sym
b = SEval sym (GenValue sym)
y
  | Bool
otherwise = sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
mergeValue' sym
sym SBit sym
b SEval sym (GenValue sym)
x SEval sym (GenValue sym)
y

{-# INLINE mergeValue' #-}
mergeValue' :: Backend sym =>
  sym ->
  SBit sym ->
  SEval sym (GenValue sym) ->
  SEval sym (GenValue sym) ->
  SEval sym (GenValue sym)
mergeValue' :: sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
mergeValue' sym
sym = sym
-> (SBit sym
    -> GenValue sym -> GenValue sym -> SEval sym (GenValue sym))
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym a.
Backend sym =>
sym
-> (SBit sym -> a -> a -> SEval sym a)
-> SBit sym
-> SEval sym a
-> SEval sym a
-> SEval sym a
mergeEval sym
sym (sym
-> SBit sym
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
mergeValue sym
sym)

mergeValue :: Backend sym =>
  sym ->
  SBit sym ->
  GenValue sym ->
  GenValue sym ->
  SEval sym (GenValue sym)
mergeValue :: sym
-> SBit sym
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
mergeValue sym
sym SBit sym
c GenValue sym
v1 GenValue sym
v2 =
  case (GenValue sym
v1, GenValue sym
v2) of
    (VRecord RecordMap Ident (SEval sym (GenValue sym))
fs1 , VRecord RecordMap Ident (SEval sym (GenValue sym))
fs2 ) ->
      do let res :: Either
  (Either Ident Ident) (RecordMap Ident (SEval sym (GenValue sym)))
res = (Ident
 -> SEval sym (GenValue sym)
 -> SEval sym (GenValue sym)
 -> SEval sym (GenValue sym))
-> RecordMap Ident (SEval sym (GenValue sym))
-> RecordMap Ident (SEval sym (GenValue sym))
-> Either
     (Either Ident Ident) (RecordMap Ident (SEval sym (GenValue sym)))
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 -> sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
mergeValue' sym
sym SBit sym
c) RecordMap Ident (SEval sym (GenValue sym))
fs1 RecordMap Ident (SEval sym (GenValue sym))
fs2
         case Either
  (Either Ident Ident) (RecordMap Ident (SEval sym (GenValue sym)))
res of
           Left Either Ident Ident
f -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Eval.Value" [ String
"mergeValue: incompatible record values", Either Ident Ident -> String
forall a. Show a => a -> String
show Either Ident Ident
f ]
           Right RecordMap Ident (SEval sym (GenValue sym))
r -> GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord RecordMap Ident (SEval sym (GenValue sym))
r)
    (VTuple [SEval sym (GenValue sym)]
vs1  , VTuple [SEval sym (GenValue sym)]
vs2  ) | [SEval sym (GenValue sym)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SEval sym (GenValue sym)]
vs1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [SEval sym (GenValue sym)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SEval sym (GenValue sym)]
vs2  ->
                                  GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue sym -> SEval sym (GenValue sym))
-> GenValue sym -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ [SEval sym (GenValue sym)] -> GenValue sym
forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple ([SEval sym (GenValue sym)] -> GenValue sym)
-> [SEval sym (GenValue sym)] -> GenValue sym
forall a b. (a -> b) -> a -> b
$ (SEval sym (GenValue sym)
 -> SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
-> [SEval sym (GenValue sym)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
mergeValue' sym
sym SBit sym
c) [SEval sym (GenValue sym)]
vs1 [SEval sym (GenValue sym)]
vs2
    (VBit SBit sym
b1     , VBit SBit sym
b2     ) -> SBit sym -> GenValue sym
forall sym. SBit sym -> GenValue sym
VBit (SBit sym -> GenValue sym)
-> SEval sym (SBit sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
forall sym.
Backend sym =>
sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
iteBit sym
sym SBit sym
c SBit sym
b1 SBit sym
b2
    (VInteger SInteger sym
i1 , VInteger SInteger sym
i2 ) -> SInteger sym -> GenValue sym
forall sym. SInteger sym -> GenValue sym
VInteger (SInteger sym -> GenValue sym)
-> SEval sym (SInteger sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SInteger sym
-> SInteger sym
-> SEval sym (SInteger sym)
iteInteger sym
sym SBit sym
c SInteger sym
i1 SInteger sym
i2
    (VRational SRational sym
q1, VRational SRational sym
q2) -> SRational sym -> GenValue sym
forall sym. SRational sym -> GenValue sym
VRational (SRational sym -> GenValue sym)
-> SEval sym (SRational sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SBit sym
-> SRational sym
-> SRational sym
-> SEval sym (SRational sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SRational sym
-> SRational sym
-> SEval sym (SRational sym)
iteRational sym
sym SBit sym
c SRational sym
q1 SRational sym
q2
    (VFloat SFloat sym
f1   , VFloat SFloat sym
f2)    -> SFloat sym -> GenValue sym
forall sym. SFloat sym -> GenValue sym
VFloat (SFloat sym -> GenValue sym)
-> SEval sym (SFloat sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SBit sym -> SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
forall sym.
Backend sym =>
sym
-> SBit sym -> SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
iteFloat sym
sym SBit sym
c SFloat sym
f1 SFloat sym
f2
    (VWord Integer
n1 WordValue sym
w1 , VWord Integer
n2 WordValue sym
w2 ) | Integer
n1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n2 -> Integer -> WordValue sym -> GenValue sym
forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
n1 (WordValue sym -> GenValue sym)
-> SEval sym (WordValue sym) -> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SBit sym
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> WordValue sym
-> WordValue sym
-> SEval sym (WordValue sym)
mergeWord sym
sym SBit sym
c WordValue sym
w1 WordValue sym
w2
    (VSeq Integer
n1 SeqMap sym (GenValue sym)
vs1 , VSeq Integer
n2 SeqMap sym (GenValue sym)
vs2 ) | Integer
n1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n2 -> Integer -> SeqMap sym (GenValue sym) -> GenValue sym
forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
n1 (SeqMap sym (GenValue sym) -> GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> Nat'
-> SeqMap sym (GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap sym
sym (Integer -> Nat'
Nat Integer
n1) (sym
-> SBit sym
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
mergeSeqMapVal sym
sym SBit sym
c SeqMap sym (GenValue sym)
vs1 SeqMap sym (GenValue sym)
vs2)
    (VStream SeqMap sym (GenValue sym)
vs1 , VStream SeqMap sym (GenValue sym)
vs2 ) -> SeqMap sym (GenValue sym) -> GenValue sym
forall sym. SeqMap sym (GenValue sym) -> GenValue sym
VStream (SeqMap sym (GenValue sym) -> GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
-> SEval sym (GenValue sym)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> Nat'
-> SeqMap sym (GenValue sym)
-> SEval sym (SeqMap sym (GenValue sym))
forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap sym
sym Nat'
Inf (sym
-> SBit sym
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
mergeSeqMapVal sym
sym SBit sym
c SeqMap sym (GenValue sym)
vs1 SeqMap sym (GenValue sym)
vs2)
    (f1 :: GenValue sym
f1@VFun{}   , f2 :: GenValue sym
f2@VFun{}   ) -> sym
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
lam sym
sym ((SEval sym (GenValue sym) -> SEval sym (GenValue sym))
 -> SEval sym (GenValue sym))
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ \SEval sym (GenValue sym)
x -> sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
mergeValue' sym
sym SBit sym
c (sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym GenValue sym
f1 SEval sym (GenValue sym)
x) (sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> GenValue sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
fromVFun sym
sym GenValue sym
f2 SEval sym (GenValue sym)
x)
    (f1 :: GenValue sym
f1@VPoly{}  , f2 :: GenValue sym
f2@VPoly{}  ) -> sym
-> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
tlam sym
sym ((TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym))
-> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ \TValue
x -> sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
mergeValue' sym
sym SBit sym
c (sym -> GenValue sym -> TValue -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> GenValue sym -> TValue -> SEval sym (GenValue sym)
fromVPoly sym
sym GenValue sym
f1 TValue
x) (sym -> GenValue sym -> TValue -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> GenValue sym -> TValue -> SEval sym (GenValue sym)
fromVPoly sym
sym GenValue sym
f2 TValue
x)
    (GenValue sym
_           , GenValue sym
_           ) -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Eval.Value"
                                  [ String
"mergeValue: incompatible values", GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
v1, GenValue sym -> String
forall a. Show a => a -> String
show GenValue sym
v2 ]

{-# INLINE mergeSeqMapVal #-}
mergeSeqMapVal :: Backend sym =>
  sym ->
  SBit sym ->
  SeqMap sym (GenValue sym)->
  SeqMap sym (GenValue sym)->
  SeqMap sym (GenValue sym)
mergeSeqMapVal :: sym
-> SBit sym
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
-> SeqMap sym (GenValue sym)
mergeSeqMapVal sym
sym SBit sym
c SeqMap sym (GenValue sym)
x SeqMap sym (GenValue sym)
y =
  (Integer -> SEval sym (GenValue sym)) -> SeqMap sym (GenValue sym)
forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap ((Integer -> SEval sym (GenValue sym))
 -> SeqMap sym (GenValue sym))
-> (Integer -> SEval sym (GenValue sym))
-> SeqMap sym (GenValue sym)
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
    sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue sym
sym SBit sym
c (SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
x Integer
i) (SeqMap sym (GenValue sym) -> Integer -> SEval sym (GenValue sym)
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym (GenValue sym)
y Integer
i)