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

    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE TypeSynonymInstances #-}
    {-# OPTIONS_GHC -fno-warn-orphans #-}
    module Cryptol.Symbolic.Value
      ( SBool, SWord
      , literalSWord
      , fromBitsLE
      , forallBV_, existsBV_
      , forallSBool_, existsSBool_
      , Value
      , TValue(..), isTBit, tvSeq
      , GenValue(..), lam, tlam, nlam, toStream, toFinSeq, toSeq, finNat'
      , fromVBit, fromVFun, fromVPoly, fromVNumPoly, fromVTuple, fromVRecord
      , lookupRecord
      , fromSeq, fromVWord
      , evalPanic
      , iteValue, mergeValue
      )
      where

    import Data.List (foldl')

    import Data.SBV.Dynamic

    import Cryptol.Eval.Value (TValue(..), isTBit, tvSeq, finNat', GenValue(..),
                               BitWord(..), lam, tlam, nlam, toStream, toFinSeq, toSeq,
                               fromSeq, fromVBit, fromVWord, fromVFun, fromVPoly,
                               fromVNumPoly, fromVTuple, fromVRecord, lookupRecord)
    import Cryptol.Utils.Panic (panic)

    -- SBool and SWord -------------------------------------------------------------

    type SBool = SVal
    type SWord = SVal

    fromBitsLE :: [SBool] -> SWord
    fromBitsLE bs = foldl' f (literalSWord 0 0) bs
      where f w b = svJoin (svToWord1 b) w

    literalSWord :: Int -> Integer -> SWord
    literalSWord w i = svInteger (KBounded False w) i

    forallBV_ :: Int -> Symbolic SWord
    forallBV_ w = svMkSymVar (Just ALL) (KBounded False w) Nothing

    existsBV_ :: Int -> Symbolic SWord
    existsBV_ w = svMkSymVar (Just EX) (KBounded False w) Nothing

    forallSBool_ :: Symbolic SBool
    forallSBool_ = svMkSymVar (Just ALL) KBool Nothing

    existsSBool_ :: Symbolic SBool
    existsSBool_ = svMkSymVar (Just EX) KBool Nothing

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

    type Value = GenValue SBool SWord

    -- Symbolic Conditionals -------------------------------------------------------

    iteValue :: SBool -> Value -> Value -> Value
    iteValue c x y =
      case svAsBool c of
        Just True  -> x
        Just False -> y
        Nothing    -> mergeValue True c x y

    mergeValue :: Bool -> SBool -> Value -> Value -> Value
    mergeValue f c v1 v2 =
      case (v1, v2) of
        (VRecord fs1, VRecord fs2) -> VRecord $ zipWith mergeField fs1 fs2
        (VTuple vs1 , VTuple vs2 ) -> VTuple $ zipWith (mergeValue f c) vs1 vs2
        (VBit b1    , VBit b2    ) -> VBit $ mergeBit b1 b2
        (VWord w1   , VWord w2   ) -> VWord $ mergeWord w1 w2
        (VSeq b1 vs1, VSeq _ vs2 ) -> VSeq b1 $ zipWith (mergeValue f c) vs1 vs2
        (VStream vs1, VStream vs2) -> VStream $ mergeStream vs1 vs2
        (VFun f1    , VFun f2    ) -> VFun $ \x -> mergeValue f c (f1 x) (f2 x)
        (VPoly f1   , VPoly f2   ) -> VPoly $ \x -> mergeValue f c (f1 x) (f2 x)
        (VWord w1   , _          ) -> VWord $ mergeWord w1 (fromVWord v2)
        (_          , VWord w2   ) -> VWord $ mergeWord (fromVWord v1) w2
        (_          , _          ) -> panic "Cryptol.Symbolic.Value"
                                      [ "mergeValue: incompatible values" ]
      where
        mergeBit b1 b2 = svSymbolicMerge KBool f c b1 b2
        mergeWord w1 w2 = svSymbolicMerge (kindOf w1) f c w1 w2
        mergeField (n1, x1) (n2, x2)
          | n1 == n2  = (n1, mergeValue f c x1 x2)
          | otherwise = panic "Cryptol.Symbolic.Value"
                        [ "mergeValue.mergeField: incompatible values" ]
        mergeStream xs ys =
          mergeValue f c (head xs) (head ys) : mergeStream (tail xs) (tail ys)

    -- Big-endian Words ------------------------------------------------------------

    instance BitWord SBool SWord where
      packWord bs = fromBitsLE (reverse bs)
      unpackWord x = [ svTestBit x i | i <- reverse [0 .. intSizeOf x - 1] ]

    -- Errors ----------------------------------------------------------------------

    evalPanic :: String -> [String] -> a
    evalPanic cxt = panic ("[Symbolic]" ++ cxt)