Merge pull request #1682 from GaloisInc/rwd/uninterp-prim

Allow SAWCore primitives to be treated as uninterpreted

Author: robdockins

saw-core/src/Verifier/SAW/Name.hs

@@ -41,6 +41,7 @@ module Verifier.SAW.Name
   , ExtCns(..)
   , scFreshNameURI
   , PrimName(..)
+  , primNameToExtCns
     -- * Naming Environments
   , SAWNamingEnv(..)
   , emptySAWNamingEnv
@@ -256,7 +257,8 @@ instance Ord (PrimName e) where
 instance Hashable (PrimName e) where
   hashWithSalt x pn = hashWithSalt x (primVarIndex pn)
 
-
+primNameToExtCns :: PrimName e -> ExtCns e
+primNameToExtCns (PrimName varIdx nm tp) = EC varIdx (ModuleIdentifier nm) tp
 
 scFreshNameURI :: Text -> VarIndex -> URI
 scFreshNameURI nm i = fromMaybe (panic "scFreshNameURI" ["Failed to constructed name URI", show nm, show i]) $

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

@@ -156,7 +156,9 @@ evalTermF cfg lam recEval tf env =
       case ftf of
         Primitive pn ->
           do pn' <- traverse evalType pn
-             simPrimitive cfg pn'
+             case simConstant cfg tf (primNameToExtCns pn') of
+               Just m  -> m
+               Nothing -> simPrimitive cfg pn'
 
         UnitValue           -> return VUnit