From 418ad73145bb17560b66573cc60553e7ee69297c Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Thu, 13 Jun 2024 13:03:08 -0400
Subject: [PATCH] Simplify concretization code with `asGround`

---
 what4/src/What4/Concretize.hs      | 11 ++---
 what4/src/What4/Expr/GroundEval.hs | 67 +++++++-----------------------
 2 files changed, 18 insertions(+), 60 deletions(-)

diff --git a/what4/src/What4/Concretize.hs b/what4/src/What4/Concretize.hs
index 3ad5b332..65ac9818 100644
--- a/what4/src/What4/Concretize.hs
+++ b/what4/src/What4/Concretize.hs
@@ -29,9 +29,7 @@ import qualified What4.SatResult as WSat
 -- | Reasons why attempting to resolve a symbolic expression as concrete can
 -- fail.
 data ConcretizationFailure
-  = ConversionError
-    -- ^ 'WEG.fromConcrete' failed
-  | SolverUnknown
+  = SolverUnknown
     -- ^ Querying the SMT solver yielded @UNKNOWN@.
   | UnsatInitialAssumptions
     -- ^ Querying the SMT solver for an initial model of the expression failed
@@ -59,11 +57,8 @@ concretize ::
   WI.SymExpr sym tp ->
   IO (Either ConcretizationFailure (WEG.GroundValue tp))
 concretize sym sp val =
-  case WI.asConcrete val of
-    Just val' ->
-      case WEG.fromConcrete val' of
-        Just val'' -> pure (Right val'')
-        Nothing -> pure (Left ConversionError)
+  case WEG.asGround val of
+    Just gVal -> pure (Right gVal)
     Nothing -> do
       -- First, check to see if there is a model of the symbolic value.
       res <- WPO.inNewFrame sp $ do
diff --git a/what4/src/What4/Expr/GroundEval.hs b/what4/src/What4/Expr/GroundEval.hs
index e0d63302..93f61938 100644
--- a/what4/src/What4/Expr/GroundEval.hs
+++ b/what4/src/What4/Expr/GroundEval.hs
@@ -24,11 +24,9 @@
 module What4.Expr.GroundEval
   ( -- * Ground evaluation
     GroundValue
-  , fromConcrete
-  , toConcrete
+  , asGround
   , groundToSym
   , GroundValueWrapper(..)
-  , groundToSym
   , GroundArray(..)
   , lookupArray
   , GroundEvalFn(..)
@@ -89,6 +87,20 @@ type family GroundValue (tp :: BaseType) where
   GroundValue (BaseArrayType idx b) = GroundArray idx b
   GroundValue (BaseStructType ctx)  = Ctx.Assignment GroundValueWrapper ctx
 
+-- | Return a ground representation of a value, if it is ground.
+asGround :: IsExpr e => e tp -> Maybe (GroundValue tp)
+asGround x =
+  case exprType x of
+    BaseBoolRepr       -> asConstantPred x
+    BaseIntegerRepr    -> asInteger x
+    BaseRealRepr       -> asRational x
+    BaseStringRepr _si -> asString x
+    BaseComplexRepr    -> asComplex x
+    BaseBVRepr _w       -> asBV x
+    BaseFloatRepr _fpp  -> asFloat x
+    BaseStructRepr _   -> asStruct x >>= traverseFC (fmap GVW . asGround)
+    BaseArrayRepr _idx _tp -> Nothing
+
 -- | Inject a 'GroundValue' back into a 'SymExpr'.
 --
 -- c.f. 'What4.Interface.concreteToSym'.
@@ -124,55 +136,6 @@ groundToSym sym tpr val =
            x' <- groundToSym sym tpr' x
            arrayUpdate sym arr' i' x'
 
--- | Convert a 'ConcreteVal' into a 'GroundValue'
---
--- May fail if the 'ConcreteVal' contains ill-typed array indices.
-fromConcrete :: ConcreteVal tp -> Maybe (GroundValue tp)
-fromConcrete =
-  \case
-    ConcreteBool b -> Just b
-    ConcreteInteger i -> Just i
-    ConcreteReal r -> Just r
-    ConcreteFloat _fpp bf -> Just bf
-    ConcreteString  s -> Just s
-    ConcreteComplex c -> Just c
-    ConcreteBV _w bv -> Just bv
-    ConcreteStruct fs -> traverseFC (fmap GVW . fromConcrete) fs
-    ConcreteArray _idxTys def upds ->
-      let upds' =
-            fmap Map.fromList $
-              traverse (\(idxs, val) -> (,) <$> traverseFC toIndexLit idxs <*> fromConcrete val) $
-              Map.toList upds
-      in ArrayConcrete <$> fromConcrete def <*> upds'
-
--- | Convert a 'GroundValue' to a 'ConcreteVal'
---
--- Fails on 'ArrayMapping'.
-toConcrete :: BaseTypeRepr tp -> GroundValue tp -> Maybe (ConcreteVal tp)
-toConcrete tpr val =
-  case tpr of
-    BaseBoolRepr -> Just (ConcreteBool val)
-    BaseIntegerRepr -> Just (ConcreteInteger val)
-    BaseRealRepr -> Just (ConcreteReal val)
-    BaseFloatRepr fpp -> Just (ConcreteFloat fpp val)
-    BaseStringRepr {} -> Just (ConcreteString val)
-    BaseComplexRepr -> Just (ConcreteComplex val)
-    BaseBVRepr w -> Just (ConcreteBV w val)
-    BaseStructRepr xs ->
-      ConcreteStruct <$>
-        traverseFC
-          (\(Pair tpr' (GVW gv)) -> toConcrete tpr' gv)
-          (Ctx.zipWith Pair xs val)
-    BaseArrayRepr idxTys ty ->
-      case val of
-        ArrayMapping {} -> Nothing
-        ArrayConcrete def upds ->
-          ConcreteArray idxTys
-          <$> toConcrete ty def
-          <*> (fmap Map.fromList $
-                (traverse (\(idxs, gval) -> (,) <$> pure (fmapFC fromIndexLit idxs) <*> toConcrete ty gval) $
-                Map.toList upds))
-
 -- | A function that calculates ground values for elements.
 --   Clients of solvers should use the @groundEval@ function for computing
 --   values in models.