Remove dead code for converting between ConcreteVal/IndexLit

what4/src/What4/Concrete.hs

@@ -44,9 +44,6 @@ module What4.Concrete
   , fromConcreteString
   , fromConcreteBV
   , fromConcreteComplex
-
-  , fromIndexLit
-  , toIndexLit
   ) where
 
 import qualified Data.List as List
@@ -64,26 +61,6 @@ import           Data.Parameterized.TH.GADT
 import           Data.Parameterized.TraversableFC
 
 import           What4.BaseTypes
-import           What4.IndexLit
-import           What4.Utils.Complex
-import           What4.Utils.StringLiteral
-
--- | A data type for representing the concrete values of base types.
-data ConcreteVal tp where
-  ConcreteBool    :: Bool -> ConcreteVal BaseBoolType
-  ConcreteInteger :: Integer -> ConcreteVal BaseIntegerType
-  ConcreteReal    :: Rational -> ConcreteVal BaseRealType
-  ConcreteFloat   :: FloatPrecisionRepr fpp -> BigFloat -> ConcreteVal (BaseFloatType fpp)
-  ConcreteString  :: StringLiteral si -> ConcreteVal (BaseStringType si)
-  ConcreteComplex :: Complex Rational -> ConcreteVal BaseComplexType
-  ConcreteBV      ::
-    (1 <= w) =>
-    NatRepr w {- Width of the bitvector -} ->
-    BV.BV w   {- Unsigned value of the bitvector -} ->
-    ConcreteVal (BaseBVType w)
-  ConcreteStruct  :: Ctx.Assignment ConcreteVal ctx -> ConcreteVal (BaseStructType ctx)
-  ConcreteArray   ::
-    Ctx.Assignment BaseTypeRepr (idx ::> i) {- Type representatives for the index tuple -} ->
     ConcreteVal b {- A default value -} ->
     Map (Ctx.Assignment ConcreteVal (idx ::> i)) (ConcreteVal b) {- A collection of point-updates -} ->
     ConcreteVal (BaseArrayType (idx ::> i) b)
@@ -122,25 +99,6 @@ concreteType = \case
   ConcreteStruct xs         -> BaseStructRepr (fmapFC concreteType xs)
   ConcreteArray idxTy def _ -> BaseArrayRepr idxTy (concreteType def)
 
-fromIndexLit :: IndexLit tp -> ConcreteVal tp
-fromIndexLit =
-  \case
-    IntIndexLit i -> ConcreteInteger i
-    BVIndexLit w bv -> ConcreteBV w bv
-
-toIndexLit :: ConcreteVal tp -> Maybe (IndexLit tp)
-toIndexLit = \case
-  ConcreteInteger i         -> Just (IntIndexLit i)
-  ConcreteBV w bv           -> Just (BVIndexLit w bv)
-  -- Explicitly match all constructors to get a warning if we add one
-  ConcreteBool{}            -> Nothing
-  ConcreteReal{}            -> Nothing
-  ConcreteFloat{}           -> Nothing
-  ConcreteString{}          -> Nothing
-  ConcreteComplex{}         -> Nothing
-  ConcreteStruct{}          -> Nothing
-  ConcreteArray{}           -> Nothing
-
 $(return [])
 
 instance TestEquality ConcreteVal where