Skip to content

Commit

Permalink
Update saw-core and adapt to changed FieldName type.
Browse files Browse the repository at this point in the history
GaloisInc/saw-core#111 changed type FieldName from String to
Data.Text.
  • Loading branch information
Brian Huffman committed Jan 19, 2021
1 parent cdec305 commit b08fbed
Show file tree
Hide file tree
Showing 4 changed files with 8 additions and 7 deletions.
2 changes: 1 addition & 1 deletion deps/saw-core-coq
4 changes: 2 additions & 2 deletions src/SAWScript/Builtins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -115,7 +115,7 @@ import qualified Cryptol.Backend.Monad as C (runEval)
import qualified Cryptol.Eval.Type as C (evalType)
import qualified Cryptol.Eval.Value as C (fromVBit, fromVWord)
import qualified Cryptol.Eval.Concrete as C (Concrete(..), bvVal)
import qualified Cryptol.Utils.Ident as C (packIdent, packModName)
import qualified Cryptol.Utils.Ident as C (mkIdent, packModName)
import qualified Cryptol.Utils.RecordMap as C (recordFromFields)
import Cryptol.Utils.PP (pretty)

Expand Down Expand Up @@ -192,7 +192,7 @@ readSBV path unintlst =
SBV.TFun t1 t2 -> C.tFun (toCType t1) (toCType t2)
SBV.TVec n t -> C.tSeq (C.tNum n) (toCType t)
SBV.TTuple ts -> C.tTuple (map toCType ts)
SBV.TRecord bs -> C.tRec (C.recordFromFields [ (C.packIdent n, toCType t) | (n, t) <- bs ])
SBV.TRecord bs -> C.tRec (C.recordFromFields [ (C.mkIdent n, toCType t) | (n, t) <- bs ])



Expand Down
7 changes: 4 additions & 3 deletions src/SAWScript/SBVParser.hs
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ import Control.Monad.State hiding (mapM)
import Data.List (intercalate)
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Text as Text
import Data.Traversable (mapM)
import Numeric.Natural (Natural)

Expand Down Expand Up @@ -210,15 +211,15 @@ data Typ
| TFun Typ Typ
| TVec SBV.Size Typ
| TTuple [Typ]
| TRecord [(String, Typ)]
| TRecord [(FieldName, Typ)]

instance Show Typ where
show TBool = "."
show (TFun t1 t2) = "(" ++ show t1 ++ " -> " ++ show t2 ++ ")"
show (TVec size t) = "[" ++ show size ++ "]" ++ show t
show (TTuple ts) = "(" ++ intercalate "," (map show ts) ++ ")"
show (TRecord fields) = "{" ++ intercalate "," (map showField fields) ++ "}"
where showField (s, t) = s ++ ":" ++ show t
where showField (s, t) = Text.unpack s ++ ":" ++ show t

parseIRType :: SBV.IRType -> Typ
parseIRType (SBV.TApp "." []) = TBool
Expand All @@ -227,7 +228,7 @@ parseIRType (SBV.TApp ":" [SBV.TInt n, a]) = TVec n (parseIRType a)
parseIRType (SBV.TApp c ts)
| c == "(" ++ replicate (length ts - 1) ',' ++ ")" = TTuple (map parseIRType ts)
parseIRType (SBV.TRecord fields) =
TRecord [ (name, parseIRType t) | (name, SBV.Scheme [] [] [] t) <- fields ]
TRecord [ (Text.pack name, parseIRType t) | (name, SBV.Scheme [] [] [] t) <- fields ]
parseIRType t = error ("parseIRType: " ++ show t)

typSizes :: Typ -> [SBV.Size]
Expand Down

0 comments on commit b08fbed

Please sign in to comment.