GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-19 18:08:37 +03:00
Code Issues Projects Releases Wiki Activity

fix warnings and update stackage snapshot

Browse Source
This commit is contained in:
Adam C. Foltzer 2016-01-19 13:29:11 -08:00
parent 4d3fc9a413
commit fdfb94c120
5 changed files with 275 additions and 270 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

512
cabal.GHC7102.config
View File

File diff suppressed because it is too large Load Diff

4
src/Cryptol/Prims/Eval.hs
View File

@ -727,8 +727,8 @@ randomV ty seed =
Nothing -> zeroV ty
Just gen ->
-- unpack the seed into four Word64s
let mask = 0xFFFFFFFFFFFFFFFF
unpack s = fromIntegral (s .&. mask) : unpack (s `shiftR` 64)
let mask64 = 0xFFFFFFFFFFFFFFFF
unpack s = fromIntegral (s .&. mask64) : unpack (s `shiftR` 64)
[a, b, c, d] = take 4 (unpack seed)
in fst $ gen 100 $ seedTFGen (a, b, c, d)

1
src/Cryptol/Symbolic/Value.hs
View File

@ -29,7 +29,6 @@ module Cryptol.Symbolic.Value
import Data.List (foldl')
import Data.SBV (HasKind(..))
import Data.SBV.Dynamic
import Cryptol.Eval.Value (TValue, numTValue, toNumTValue, finTValue, isTBit,

16
src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs
View File

@ -372,20 +372,20 @@ cryNot prop =
-- | Simplificaiton for @:==@
cryIsEq :: Expr -> Expr -> Prop
cryIsEq x y =
case (x,y) of
cryIsEq l r =
case (l,r) of
(K m, K n) -> if m == n then PTrue else PFalse
(K Inf, _) -> Not (Fin y)
(_, K Inf) -> Not (Fin x)
(K Inf, _) -> Not (Fin r)
(_, K Inf) -> Not (Fin l)
(Div x y, z) -> x :>= z :* y :&& (one :+ z) :* y :> x
(K (Nat n),_) | Just p <- cryIsNat False n y -> p
(_,K (Nat n)) | Just p <- cryIsNat False n x -> p
(K (Nat n),_) | Just p <- cryIsNat False n r -> p
(_,K (Nat n)) | Just p <- cryIsNat False n l -> p
_ -> Not (Fin x) :&& Not (Fin y)
:|| Fin x :&& Fin y :&& cryNatOp (:==:) x y
_ -> Not (Fin l) :&& Not (Fin r)
:|| Fin l :&& Fin r :&& cryNatOp (:==:) l r

12
src/Cryptol/TypeCheck/Solver/Numeric/Simplify1.hs
View File

@ -28,6 +28,7 @@ import Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr
import Cryptol.TypeCheck.Solver.Numeric.AST
import Cryptol.TypeCheck.Solver.InfNat(genLog,rootExact)
import Cryptol.Utils.Misc ( anyJust )
import Cryptol.Utils.Panic
import Cryptol.Utils.PP
import Control.Monad ( liftM2 )
@ -309,6 +310,9 @@ pIsNat n expr =
| otherwise -> pAnd (pGt x (K (Nat (2^(n-1) - 1))))
(pGt (K (Nat (2 ^ n))) x)
x ->
panic "Cryptol.TypeCheck.Solver.Numeric.Simplify1.pIsNat"
[ "unexpected expression ", show x ]
{-
LenFromThen x y w
| n == 0 -> Just PFalse
@ -335,11 +339,11 @@ pIsNat n expr =
nothing = pAnd (pFin expr) (pAtom (AEq expr (K (Nat n))))
pIsGtThanNat :: Integer -> Expr -> I Bool
pIsGtThanNat = undefined
_pIsGtThanNat :: Integer -> Expr -> I Bool
_pIsGtThanNat = undefined
pNatIsGtThan :: Integer -> Expr -> I Bool
pNatIsGtThan = undefined
_pNatIsGtThan :: Integer -> Expr -> I Bool
_pNatIsGtThan = undefined
--------------------------------------------------------------------------------