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 #320.

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

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 ::

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