From a489c57c99979c199cfe642f89df531ba9ae9ef3 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Mon, 19 Oct 2020 16:32:46 -0700
Subject: [PATCH] Support uninterpreted polymorphic functions in sbv/what4
 backends.

This works by declaring monomorphic uninterpreted functions at
each type instance, using a name suffix based on the type value.

Fixes GaloisInc/saw-script#320.
---
 .../src/Verifier/SAW/Simulator/SBV.hs         |  2 ++
 .../src/Verifier/SAW/Simulator/What4.hs       |  3 +++
 saw-core/src/Verifier/SAW/Simulator/Value.hs  | 25 +++++++++++++++++++
 3 files changed, 30 insertions(+)

diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
index 05f28b67c1..5ff011157a 100644
--- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
+++ b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
@@ -266,6 +266,8 @@ flattenSValue v = do
         VCtorApp i (V.toList->ts) -> do (xss, ss) <- unzip <$> traverse (force >=> flattenSValue) ts
                                         return (concat xss, "_" ++ identName i ++ concat ss)
         VNat n                    -> return ([], "_" ++ show n)
+        TValue (suffixTValue -> Just s)
+                                  -> return ([], s)
         _ -> fail $ "Could not create sbv argument for " ++ show v
 
 vWord :: SWord -> SValue
diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
index 8de7ec67b2..b9a0dbdfea 100644
--- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
+++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
@@ -826,8 +826,11 @@ applyUnintApp app0 v =
     VCtorApp i xv             -> foldM applyUnintApp app' =<< traverse force xv
                                    where app' = suffixUnintApp ("_" ++ identName i) app0
     VNat n                    -> return (suffixUnintApp ("_" ++ show n) app0)
+    TValue (suffixTValue -> Just s)
+                              -> return (suffixUnintApp s app0)
     _ -> fail $ "Could not create argument for " ++ show v
 
+
 ------------------------------------------------------------
 
 w4SolveAny ::
diff --git a/saw-core/src/Verifier/SAW/Simulator/Value.hs b/saw-core/src/Verifier/SAW/Simulator/Value.hs
index 0ba5d228e2..12c9492334 100644
--- a/saw-core/src/Verifier/SAW/Simulator/Value.hs
+++ b/saw-core/src/Verifier/SAW/Simulator/Value.hs
@@ -259,3 +259,28 @@ asFiniteTypeTValue v =
       FTRec <$> Map.fromList <$>
       mapM (\(fld,tp) -> (fld,) <$> asFiniteTypeTValue tp) elem_tps
     _ -> Nothing
+
+-- | A (partial) injective mapping from type values to strings. These
+-- are intended to be useful as suffixes for names of type instances
+-- of uninterpreted constants.
+suffixTValue :: TValue sym -> Maybe String
+suffixTValue tv =
+  case tv of
+    VVecType n a ->
+      do a' <- suffixTValue a
+         Just ("_Vec_" ++ show n ++ a')
+    VBoolType -> Just "_Bool"
+    VIntType -> Just "_Int"
+    VArrayType a b ->
+      do a' <- suffixTValue a
+         b' <- suffixTValue b
+         Just ("_Array" ++ a' ++ b')
+    VPiType _ _ -> Nothing
+    VUnitType -> Just "_Unit"
+    VPairType a b ->
+      do a' <- suffixTValue a
+         b' <- suffixTValue b
+         Just ("_Pair" ++ a' ++ b')
+    VDataType {} -> Nothing
+    VRecordType {} -> Nothing
+    VSort {} -> Nothing