GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 04:44:39 +03:00
Code Issues Projects Releases Wiki Activity

Adapt internal uses of demote primitive to its new type

Browse Source
This commit is contained in:
Brian Huffman 2017-11-10 08:34:58 -08:00
parent 5eb67c0513
commit 231c5713c4
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Cryptol/Eval/Value.hs
View File

@ -784,7 +784,7 @@ toExpr prims t0 v0 = findOne (go t0 v0)
(TCon (TC TCSeq) [a,(TCon (TC TCBit) [])], VWord _ wval) -> do
BV w v <- lift (asWordVal =<< wval)
guard (a == tNum w)
return $ ETApp (ETApp (prim "demote") (tNum v)) (tNum w)
return $ ETApp (ETApp (prim "demote") (tNum v)) (tWord (tNum w))
(_, VStream _) -> fail "cannot construct infinite expressions"
(_, VFun _) -> fail "cannot convert function values to expressions"
(_, VPoly _) -> fail "cannot convert polymorphic values to expressions"

2
src/Cryptol/TypeCheck/AST.hs
View File

@ -181,7 +181,7 @@ eString :: PrimMap -> String -> Expr
eString prims str = EList (map (eChar prims) str) tChar
eChar :: PrimMap -> Char -> Expr
eChar prims c = ETApp (ETApp (ePrim prims (packIdent "demote")) (tNum v)) (tNum w)
eChar prims c = ETApp (ETApp (ePrim prims (packIdent "demote")) (tNum v)) (tWord (tNum w))
where v = fromEnum c
w = 8 :: Int