GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-22 11:27:44 +03:00
Code Issues Projects Releases Wiki Activity

exposing low level uninterpreted interface

Browse Source
This commit is contained in:
Sam Anklesaria 2014-08-07 10:54:40 -07:00
parent 5fca89f8b1
commit 8e54775642
2 changed files with 12 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
sbv/Data/SBV/BitVectors/Model.hs
View File

@ -23,7 +23,7 @@
module Data.SBV.BitVectors.Model (
Mergeable(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), SIntegral
, sbvTestBit, sbvPopCount, setBitTo, sbvShiftLeft, sbvShiftRight, sbvSignedShiftArithRight
, sbvRotateLeft, sbvRotateRight
, sbvRotateLeft, sbvRotateRight, mkUninterpreted
, allEqual, allDifferent, inRange, sElem, oneIf, blastBE, blastLE, fullAdder, fullMultiplier
, lsb, msb, genVar, genVar_, forall, forall_, exists, exists_
, constrain, pConstrain, sBool, sBools, sWord8, sWord8s, sWord16, sWord16s, sWord32
@ -1495,6 +1495,15 @@ class Uninterpreted a where
uninterpret = sbvUninterpret Nothing
cgUninterpret nm code v = sbvUninterpret (Just (code, v)) nm
mkUninterpreted :: [Kind] -> [SBV ()] -> String -> SBV a
mkUninterpreted ks args nm = SBV ka $ Right $ cache result where
ka = last ks
result st = do
newUninterpreted st nm (SBVType ks) Nothing
sws <- mapM (sbvToSW st) args
mapM_ forceSWArg sws
newExpr st ka $ SBVApp (Uninterpreted nm) sws
-- Plain constants
instance HasKind a => Uninterpreted (SBV a) where
sbvUninterpret mbCgData nm

4
sbv/Data/SBV/Internals.hs
View File

@ -18,10 +18,10 @@ module Data.SBV.Internals (
, SBV(..), slet, CW(..), Kind(..), CWVal(..), AlgReal(..), mkConstCW, genVar, genVar_
, liftQRem, liftDMod
-- * Compilation to C
, compileToC', compileToCLib', CgPgmBundle(..), CgPgmKind(..)
, mkUninterpreted, compileToC', compileToCLib', CgPgmBundle(..), CgPgmKind(..)
) where
import Data.SBV.BitVectors.Data (Result, SBVRunMode(..), runSymbolic, runSymbolic', SBV(..), CW(..), Kind(..), CWVal(..), AlgReal(..), mkConstCW)
import Data.SBV.BitVectors.Model (genVar, genVar_, slet, liftQRem, liftDMod)
import Data.SBV.BitVectors.Model (genVar, genVar_, slet, liftQRem, liftDMod, mkUninterpreted)
import Data.SBV.Compilers.C (compileToC', compileToCLib')
import Data.SBV.Compilers.CodeGen (CgPgmBundle(..), CgPgmKind(..))