GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-26 09:25:56 +03:00
Code Issues Projects Releases Wiki Activity

Remove implicit Bit type signature on rhs of property declarations.

Browse Source 
Fixes #224.

It might be desirable to add some other check for `property` declarations
to make sure that their types are predicates of some arity.
This commit is contained in:
Brian Huffman 2017-10-04 15:26:17 -07:00
parent 3a154f948a
commit 2b568897da
3 changed files with 2 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Cryptol/Parser/ParserUtils.hs
View File

@ -331,7 +331,7 @@ mkPoly rng terms = mk 0 (map fromInteger bits)
mkProperty :: LPName -> [Pattern PName] -> Expr PName -> Decl PName mkProperty :: LPName -> [Pattern PName] -> Expr PName -> Decl PName
mkProperty f ps e = DBind Bind { bName = f mkProperty f ps e = DBind Bind { bName = f
, bParams = reverse ps , bParams = reverse ps
, bDef = at e (Located emptyRange (DExpr (ETyped e TBit))) , bDef = at e (Located emptyRange (DExpr e))
, bSignature = Nothing , bSignature = Nothing
, bPragmas = [PragmaProperty] , bPragmas = [PragmaProperty]
, bMono = False , bMono = False

1
tests/issues/issue312.icry.fails
View File

@ -1 +0,0 @@
https://github.com/GaloisInc/cryptol/issues/224

2
tests/parser/docs.cry
View File

@ -18,7 +18,7 @@ test3 x = x
/** /**
* Test that doc strings work on property declarations * Test that doc strings work on property declarations
*/ */
property test4 x = x property test4 x = (x : Bit)
/** /**
* Test that doc strings work on fixity declarations * Test that doc strings work on fixity declarations