Merge pull request #92 from GaloisInc/unint-poly

Support uninterpreted polymorphic functions in sbv/what4 backends.

saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs

@@ -266,7 +266,10 @@ 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)
-        _ -> fail $ "Could not create sbv argument for " ++ show v
+        TValue (suffixTValue -> Just s)
+                                  -> return ([], s)
+        VFun _ -> fail "Cannot create uninterpreted higher-order function"
+        _ -> fail $ "Cannot create uninterpreted function with argument " ++ show v
 
 vWord :: SWord -> SValue
 vWord lv = VWord lv

saw-core-what4/src/Verifier/SAW/Simulator/What4.hs

@@ -826,7 +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)
-    _ -> fail $ "Could not create argument for " ++ show v
+    TValue (suffixTValue -> Just s)
+                              -> return (suffixUnintApp s app0)
+    VFun _ -> fail "Cannot create uninterpreted higher-order function"
+    _ -> fail $ "Cannot create uninterpreted function with argument " ++ show v
+
 
 ------------------------------------------------------------
 

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