GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-01 08:32:23 +03:00
Code Issues Projects Releases Wiki Activity

Add module parameters as extra vars---prints nicer error messages.

Browse Source
This commit is contained in:
Iavor Diatchki 2017-09-26 15:29:23 -07:00
parent 83d0132e50
commit b8707033d7
2 changed files with 5 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
examples/AE.cry
View File

@ -51,8 +51,8 @@ property
type Integer = [64] type Integer = [64]
encrypt : {m} fin m => encrypt :
K -> Nonce -> A -> [m * (p * n)] -> [m * (p * n) + tagAmount] {m} fin m => K -> Nonce -> A -> [m * (p * n)] -> [m * (p * n) + tagAmount]
encrypt key nonce state inputMsg = join ((drop`{1} go).0.message) # tag encrypt key nonce state inputMsg = join ((drop`{1} go).0.message) # tag
where where

4
src/Cryptol/TypeCheck/Solve.hs
View File

@ -186,8 +186,10 @@ proveImplication :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication lnam as ps gs = proveImplication lnam as ps gs =
do evars <- varsWithAsmps do evars <- varsWithAsmps
solver <- getSolver solver <- getSolver
pas <- Map.elems <$> getParamTypes
extra <- getParamConstraints extra <- getParamConstraints
(mbErr,su) <- io (proveImplicationIO solver lnam evars as (extra ++ ps) gs) (mbErr,su) <- io (proveImplicationIO solver lnam evars
(pas ++ as) (extra ++ ps) gs)
case mbErr of case mbErr of
Right ws -> mapM_ recordWarning ws Right ws -> mapM_ recordWarning ws
Left err -> recordError err Left err -> recordError err