    -- |
    -- 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
    $cfrom :: forall sym x. GenValue sym -> Rep (GenValue sym) x
    from :: forall x. GenValue sym -> Rep (GenValue sym) x
    $cto :: forall sym x. Rep (GenValue sym) x -> GenValue sym
    to :: forall x. Rep (GenValue sym) x -> GenValue sym
    Generic

    -- | Force the evaluation of a value
    forceValue :: Backend sym => GenValue sym -> SEval sym ()
    forceValue :: forall sym. Backend sym => 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 ()
    forall a b. a -> b -> b
    seq SBit sym
    b (() -> SEval sym ()
    forall a. a -> SEval sym a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())
      VInteger SInteger sym
    i  -> SInteger sym -> SEval sym () -> SEval sym ()
    forall a b. a -> b -> b
    seq SInteger sym
    i (() -> SEval sym ()
    forall a. a -> SEval sym a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())
      VRational SRational sym
    q -> SRational sym -> SEval sym () -> SEval sym ()
    forall a b. a -> b -> b
    seq SRational sym
    q (() -> SEval sym ()
    forall a. a -> SEval sym a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())
      VFloat SFloat sym
    f    -> SFloat sym -> SEval sym () -> SEval sym ()
    forall a b. a -> b -> b
    seq SFloat sym
    f (() -> SEval sym ()
    forall a. a -> SEval sym a
    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 a. a -> SEval sym a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      VFun{}      -> () -> SEval sym ()
    forall a. a -> SEval sym a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      VPoly{}     -> () -> SEval sym ()
    forall a. a -> SEval sym a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      VNumPoly{}  -> () -> SEval sym ()
    forall a. a -> SEval sym a
    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 a. [a] -> 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 :: forall sym.
    Backend sym =>
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> RecordMap Ident a -> f (RecordMap Ident b)
    traverse (SEval sym (GenValue sym)
    -> (GenValue sym -> SEval sym Doc) -> SEval sym Doc
    forall a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse (SEval sym (GenValue sym)
    -> (GenValue sym -> SEval sym Doc) -> SEval sym Doc
    forall a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse (SEval sym (GenValue sym)
    -> (GenValue sym -> SEval sym Doc) -> SEval sym Doc
    forall a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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 a. a -> SEval sym a
    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 a. a -> SEval sym a
    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 a. a -> SEval sym a
    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)
    forall (m :: * -> *) a. Monad m => [m a] -> m [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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [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 a. a -> SEval sym a
    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)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> SEval sym a
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse GenValue sym -> SEval sym Doc
    loop [GenValue sym]
    ws
                  Doc -> SEval sym Doc
    forall a. a -> SEval sym a
    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 :: forall sym. Backend sym => 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 a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (String -> Doc
    text String
    "True")
        Just Bool
    False -> Doc -> SEval sym Doc
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (String -> Doc
    text String
    "False")
        Maybe Bool
    Nothing    -> Doc -> SEval sym Doc
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (String -> Doc
    text String
    "?")

    ppSInteger :: Backend sym => sym -> SInteger sym -> SEval sym Doc
    ppSInteger :: forall sym. Backend sym => 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 a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Doc
    integer Integer
    i)
        Maybe Integer
    Nothing -> Doc -> SEval sym Doc
    forall a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (String -> Doc
    text String
    "[?]")

    ppSFloat :: Backend sym => sym -> PPOpts -> SFloat sym -> SEval sym Doc
    ppSFloat :: forall sym.
    Backend sym =>
    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 a. a -> SEval sym a
    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 a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (String -> Doc
    text String
    "[?]")

    ppSRational :: Backend sym => sym -> SRational sym -> SEval sym Doc
    ppSRational :: forall sym. Backend sym => 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 a. a -> SEval sym a
    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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    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 a. a -> SEval sym a
    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 a. a -> SEval sym a
    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 a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Int -> Doc
    prefix (String -> Int
    forall a. [a] -> 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 a. a -> SEval sym a
    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 => a -> (Int -> Char) -> a -> ShowS
    showIntAtBase (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    base) (String
    digits String -> Int -> Char
    forall a. HasCallStack => [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. HasCallStack => [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 a. a -> SEval sym a
    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 a. a -> SEval sym a
    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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    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 :: 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)
    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 a b. SEval sym (a -> b) -> SEval sym a -> SEval sym b
    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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    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 a b. SEval sym (a -> b) -> SEval sym a -> SEval sym b
    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 a. a -> SEval sym a
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 :: forall sym.
    Backend sym =>
    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 a b. SEval sym (a -> b) -> SEval sym a -> SEval sym b
    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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    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 a b. SEval sym (a -> b) -> SEval sym a -> SEval sym b
    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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    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 :: forall sym.
    Backend sym =>
    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 a. a -> SEval sym a
    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 a. a -> SEval sym a
    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 :: forall sym. 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 :: forall sym. 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 :: forall sym. 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 :: forall sym. 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 :: forall sym.
    Backend sym =>
    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 a. a -> SEval sym a
    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 a. a -> SEval sym a
    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 :: forall sym. Backend sym => 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 :: forall sym.
    Backend sym =>
    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 :: forall sym.
    Backend sym =>
    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 :: forall sym. Backend sym => 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 :: forall sym.
    Backend sym =>
    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 a. sym -> SEval sym a -> SEval sym (Maybe a)
    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 a b. SEval sym a -> (a -> SEval sym b) -> SEval sym b
    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 a. a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    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 a.
    sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    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 a.
    sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    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 a.
    sym -> (CallStack -> CallStack) -> SEval sym a -> SEval sym a
    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 :: forall sym. 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 :: forall sym.
    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 :: forall sym. 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 :: forall sym. 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 :: forall sym.
    Backend sym =>
    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' :: forall sym.
    Backend sym =>
    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 a.
    sym
    -> (SBit sym -> a -> a -> SEval sym a)
    -> SBit sym
    -> SEval sym a
    -> SEval sym a
    -> SEval sym a
    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 :: forall sym.
    Backend sym =>
    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 a. a -> SEval sym a
    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 a. [a] -> 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 a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SEval sym (GenValue sym)]
    vs2  ->
                                      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))
    -> 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 :: 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)
    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)