mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-22 11:27:44 +03:00
WIP. Improve performance of the new evaluator.
To get acceptable performance, we need to be pretty aggressive about using word representations instead of list-of-bits. Unfortunately, with the new evaluator, this means we force things to be more strict than is correct. We are also still slower than the current evaluator. It is not clear where the problems are.
This commit is contained in:
Robert Dockins
parent
7e968d2d18
commit
e31b4ba57d
@ -339,5 +339,5 @@ type lg2 n = width (max n 1 - 1)
|
||||
*/
|
||||
primitive trace : {n, a, b} [n][8] -> a -> b -> b
|
||||
|
||||
traceVal : {n, a, b} [n][8] -> a -> a
|
||||
traceVal : {n, a} [n][8] -> a -> a
|
||||
traceVal msg x = trace msg x x
|
||||
|
||||
@ -37,7 +37,7 @@ import Control.Monad
|
||||
import Control.Monad.Fix
|
||||
import Data.IORef
|
||||
import Data.List
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Map.Strict as Map
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
@ -54,11 +54,20 @@ evalExpr env expr = case expr of
|
||||
VSeq (genericLength es) (isTBit (evalType env ty))
|
||||
<$> finiteSeqMap (map (evalExpr env) es)
|
||||
|
||||
ETuple es -> return $ VTuple (map eval es)
|
||||
ETuple es -> do
|
||||
xs <- mapM (delay Nothing . eval) es
|
||||
return $ VTuple xs
|
||||
|
||||
ERec fields -> return $ VRecord [ (f,eval e) | (f,e) <- fields ]
|
||||
ERec fields -> do
|
||||
xs <- sequence [ do thk <- delay Nothing (eval e)
|
||||
return (f,thk)
|
||||
| (f,e) <- fields
|
||||
]
|
||||
return $ VRecord xs
|
||||
|
||||
ESel e sel -> eval e >>= \e' -> evalSel e' sel
|
||||
ESel e sel -> do
|
||||
x <- eval e
|
||||
evalSel x sel
|
||||
|
||||
EIf c t f -> do
|
||||
b <- fromVBit <$> eval c
|
||||
@ -68,13 +77,9 @@ evalExpr env expr = case expr of
|
||||
eval f
|
||||
|
||||
EComp n t h gs -> do
|
||||
--io $ putStrLn $ "Eval comp"
|
||||
let len = evalType env n
|
||||
let elty = evalType env t
|
||||
--io $ putStrLn $ "at type: " ++ show (pp (tSeq (tValTy len) (tValTy elty)))
|
||||
z <- evalComp env len elty h gs
|
||||
--io $ putStrLn $ "Done with comp eval"
|
||||
return z
|
||||
evalComp env len elty h gs
|
||||
|
||||
EVar n -> do
|
||||
case lookupVar n env of
|
||||
@ -86,11 +91,12 @@ evalExpr env expr = case expr of
|
||||
, show envdoc
|
||||
]
|
||||
|
||||
ETAbs tv b -> return $ VPoly $ \ty -> evalExpr (bindType (tpVar tv) ty env) b
|
||||
ETAbs tv b ->
|
||||
return $ VPoly $ \ty -> evalExpr (bindType (tpVar tv) ty env) b
|
||||
|
||||
ETApp e ty -> do
|
||||
eval e >>= \case
|
||||
VPoly f -> f $ (evalType env ty)
|
||||
VPoly f -> f $! (evalType env ty)
|
||||
val -> do vdoc <- ppV val
|
||||
panic "[Eval] evalExpr"
|
||||
["expected a polymorphic value"
|
||||
@ -103,7 +109,8 @@ evalExpr env expr = case expr of
|
||||
it -> do itdoc <- ppV it
|
||||
panic "[Eval] evalExpr" ["not a function", show itdoc ]
|
||||
|
||||
EAbs n _ty b -> return $ VFun (\val -> bindVar n val env >>= \env' -> evalExpr env' b )
|
||||
EAbs n _ty b ->
|
||||
return $ VFun (\val -> bindVar n val env >>= \env' -> evalExpr env' b )
|
||||
|
||||
-- XXX these will likely change once there is an evidence value
|
||||
EProofAbs _ e -> evalExpr env e
|
||||
@ -118,7 +125,6 @@ evalExpr env expr = case expr of
|
||||
where
|
||||
|
||||
eval = evalExpr env
|
||||
|
||||
ppV = ppValue defaultPPOpts
|
||||
|
||||
|
||||
@ -226,54 +232,34 @@ evalSel val sel = case sel of
|
||||
|
||||
-- List Comprehension Environments ---------------------------------------------
|
||||
|
||||
-- | A variation of the ZipList type from Control.Applicative, with a
|
||||
-- separate constructor for pure values. This datatype is used to
|
||||
-- represent the list of values that each variable takes on within a
|
||||
-- list comprehension. The @Zip@ constructor is for bindings that take
|
||||
-- different values at different positions in the list, while the
|
||||
-- @Pure@ constructor is for bindings originating outside the list
|
||||
-- comprehension, which have the same value for all list positions.
|
||||
data ZList a = Pure a | Zip (Integer -> a)
|
||||
|
||||
getZList :: ZList a -> Integer -> a
|
||||
getZList (Pure x) = \_ -> x
|
||||
getZList (Zip xs) = xs
|
||||
|
||||
instance Functor ZList where
|
||||
fmap f (Pure x) = Pure (f x)
|
||||
fmap f (Zip xs) = Zip (f . xs)
|
||||
|
||||
instance Applicative ZList where
|
||||
pure x = Pure x
|
||||
Pure f <*> Pure x = Pure (f x)
|
||||
Pure f <*> Zip xs = Zip (\i -> f (xs i))
|
||||
Zip fs <*> Pure x = Zip (\i -> fs i x)
|
||||
Zip fs <*> Zip xs = Zip (\i -> fs i (xs i))
|
||||
|
||||
-- | Evaluation environments for list comprehensions: Each variable
|
||||
-- name is bound to a list of values, one for each element in the list
|
||||
-- comprehension.
|
||||
data ListEnv = ListEnv
|
||||
{ leVars :: Map.Map Name (ZList (Eval Value))
|
||||
, leTypes :: Map.Map TVar TValue
|
||||
{ leVars :: !(Map.Map Name (Integer -> Eval Value))
|
||||
, leStatic :: !(Map.Map Name (Eval Value))
|
||||
, leTypes :: !(Map.Map TVar TValue)
|
||||
}
|
||||
|
||||
instance Monoid ListEnv where
|
||||
mempty = ListEnv
|
||||
{ leVars = Map.empty
|
||||
, leTypes = Map.empty
|
||||
{ leVars = Map.empty
|
||||
, leStatic = Map.empty
|
||||
, leTypes = Map.empty
|
||||
}
|
||||
|
||||
mappend l r = ListEnv
|
||||
{ leVars = Map.union (leVars l) (leVars r)
|
||||
, leTypes = Map.union (leTypes l) (leTypes r)
|
||||
{ leVars = Map.union (leVars l) (leVars r)
|
||||
, leStatic = Map.union (leStatic l) (leStatic r)
|
||||
, leTypes = Map.union (leTypes l) (leTypes r)
|
||||
}
|
||||
|
||||
toListEnv :: EvalEnv -> ListEnv
|
||||
toListEnv e =
|
||||
ListEnv
|
||||
{ leVars = fmap Pure (envVars e)
|
||||
, leTypes = envTypes e
|
||||
{ leVars = mempty
|
||||
, leStatic = envVars e
|
||||
, leTypes = envTypes e
|
||||
}
|
||||
|
||||
-- | Take parallel slices of the list environment. If some names are
|
||||
@ -281,40 +267,23 @@ toListEnv e =
|
||||
-- parallel branch of a comprehension) then the last elements will be
|
||||
-- dropped as the lists are zipped together.
|
||||
zipListEnv :: ListEnv -> Integer -> EvalEnv
|
||||
zipListEnv (ListEnv vm tm) i =
|
||||
let v = getZList (sequenceA vm) i
|
||||
in EvalEnv { envVars = v, envTypes = tm }
|
||||
zipListEnv (ListEnv vm st tm) i =
|
||||
let v = fmap ($i) vm
|
||||
in v `seq` EvalEnv{ envVars = Map.union v st, envTypes = tm }
|
||||
|
||||
bindVarList :: Name -> (Integer -> Eval Value) -> ListEnv -> ListEnv
|
||||
bindVarList n vs lenv = lenv { leVars = Map.insert n (Zip vs) (leVars lenv) }
|
||||
|
||||
bindVarList n vs lenv = lenv { leVars = Map.insert n vs (leVars lenv) }
|
||||
|
||||
-- List Comprehensions ---------------------------------------------------------
|
||||
|
||||
-- | Evaluate a comprehension.
|
||||
evalComp :: ReadEnv -> TValue -> TValue -> Expr -> [[Match]] -> Eval Value
|
||||
evalComp env len elty body ms =
|
||||
do envMap <- mkEnvMap
|
||||
do lenv <- mconcat <$> mapM (branchEnvs (toListEnv env)) ms
|
||||
seq <- memoMap $ SeqMap $ \i -> do
|
||||
env' <- envMap i
|
||||
evalExpr env' body
|
||||
evalExpr (zipListEnv lenv i) body
|
||||
return $ mkSeq len elty $ seq
|
||||
|
||||
where
|
||||
mkEnvMap :: Eval (Integer -> Eval EvalEnv)
|
||||
mkEnvMap = do
|
||||
r <- io $ newIORef Map.empty
|
||||
benvs <- mconcat <$> mapM (branchEnvs (toListEnv env)) ms
|
||||
return $ \i -> do
|
||||
m <- io $ readIORef r
|
||||
case Map.lookup i m of
|
||||
Just e -> return e
|
||||
Nothing -> do
|
||||
--io $ putStrLn $ unwords ["Forcing env map value", show i]
|
||||
let e = zipListEnv benvs i
|
||||
io $ writeIORef r (Map.insert i e m)
|
||||
return e
|
||||
|
||||
-- | Turn a list of matches into the final environments for each iteration of
|
||||
-- the branch.
|
||||
branchEnvs :: ListEnv -> [Match] -> Eval ListEnv
|
||||
@ -329,19 +298,20 @@ evalMatch lenv m = case m of
|
||||
case numTValue len of
|
||||
Nat nLen -> do
|
||||
vss <- memoMap $ SeqMap $ \i -> evalExpr (zipListEnv lenv i) expr
|
||||
let stutter (Pure x) = Pure x
|
||||
stutter (Zip xs) = Zip $ \i -> xs (i `div` nLen)
|
||||
let stutter xs = \i -> xs (i `div` nLen)
|
||||
let lenv' = lenv { leVars = fmap stutter (leVars lenv) }
|
||||
let vs i = do let (q,r) = i `divMod` nLen
|
||||
let vs i = do let (q, r) = i `divMod` nLen
|
||||
xs <- fromSeq =<< lookupSeqMap vss q
|
||||
lookupSeqMap xs r
|
||||
return $ bindVarList n vs lenv'
|
||||
|
||||
Inf -> do
|
||||
let stutter (Pure x) = Pure x
|
||||
stutter (Zip xs) = Pure (xs 0)
|
||||
let lenv' = lenv { leVars = fmap stutter (leVars lenv) }
|
||||
xs <- delay Nothing (fromSeq =<< evalExpr (zipListEnv lenv 0) expr)
|
||||
let allvars = Map.union (fmap ($0) (leVars lenv)) (leStatic lenv)
|
||||
let lenv' = lenv { leVars = Map.empty
|
||||
, leStatic = allvars
|
||||
}
|
||||
let env = EvalEnv allvars (leTypes lenv)
|
||||
xs <- delay Nothing (fromSeq =<< evalExpr env expr)
|
||||
let vs i = do xseq <- xs
|
||||
lookupSeqMap xseq i
|
||||
return $ bindVarList n vs lenv'
|
||||
@ -349,8 +319,6 @@ evalMatch lenv m = case m of
|
||||
where
|
||||
tyenv = emptyEnv{ envTypes = leTypes lenv }
|
||||
len = evalType tyenv l
|
||||
elty = evalType tyenv ty
|
||||
|
||||
|
||||
-- XXX we don't currently evaluate these as though they could be recursive, as
|
||||
-- they are typechecked that way; the read environment to evalExpr is the same
|
||||
|
||||
@ -18,7 +18,7 @@ import Cryptol.ModuleSystem.Name
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.Utils.PP
|
||||
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Map.Strict as Map
|
||||
|
||||
import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
@ -32,8 +32,8 @@ import Prelude.Compat
|
||||
type ReadEnv = EvalEnv
|
||||
|
||||
data EvalEnv = EvalEnv
|
||||
{ envVars :: Map.Map Name (Eval Value)
|
||||
, envTypes :: Map.Map TVar TValue
|
||||
{ envVars :: !(Map.Map Name (Eval Value))
|
||||
, envTypes :: !(Map.Map TVar TValue)
|
||||
} deriving (Generic)
|
||||
|
||||
instance NFData EvalEnv where rnf = genericRnf
|
||||
@ -66,17 +66,21 @@ emptyEnv = mempty
|
||||
-- | Bind a variable in the evaluation environment.
|
||||
bindVar :: Name -> Eval Value -> EvalEnv -> Eval EvalEnv
|
||||
bindVar n val env = do
|
||||
val' <- delay (Just (show (ppLocName n))) val
|
||||
let nm = show $ ppLocName n
|
||||
val' <- delay (Just nm) val
|
||||
return $ env { envVars = Map.insert n val' (envVars env) }
|
||||
|
||||
-- | Lookup a variable in the environment.
|
||||
{-# INLINE lookupVar #-}
|
||||
lookupVar :: Name -> EvalEnv -> Maybe (Eval Value)
|
||||
lookupVar n env = Map.lookup n (envVars env)
|
||||
|
||||
-- | Bind a type variable of kind *.
|
||||
{-# INLINE bindType #-}
|
||||
bindType :: TVar -> TValue -> EvalEnv -> EvalEnv
|
||||
bindType p ty env = env { envTypes = Map.insert p ty (envTypes env) }
|
||||
|
||||
-- | Lookup a type variable.
|
||||
{-# INLINE lookupType #-}
|
||||
lookupType :: TVar -> EvalEnv -> Maybe TValue
|
||||
lookupType p env = Map.lookup p (envTypes env)
|
||||
|
||||
@ -39,15 +39,15 @@ ready :: a -> Eval a
|
||||
ready a = Ready a
|
||||
|
||||
data Eval a
|
||||
= Ready a
|
||||
= Ready !a
|
||||
| Thunk !(IO a)
|
||||
deriving (Functor)
|
||||
|
||||
data ThunkState a
|
||||
= Unforced
|
||||
| BlackHole
|
||||
| Forced a
|
||||
| Forced !a
|
||||
|
||||
{-# INLINE delay #-}
|
||||
delay :: Maybe String -> Eval a -> Eval (Eval a)
|
||||
delay _ (Ready a) = Ready (Ready a)
|
||||
delay msg (Thunk x) = Thunk $ do
|
||||
@ -79,18 +79,28 @@ runEval :: Eval a -> IO a
|
||||
runEval (Ready a) = return a
|
||||
runEval (Thunk x) = x
|
||||
|
||||
{-# INLINE evalBind #-}
|
||||
evalBind :: Eval a -> (a -> Eval b) -> Eval b
|
||||
evalBind (Ready a) f = f a
|
||||
evalBind (Thunk x) f = Thunk (x >>= runEval . f)
|
||||
|
||||
instance Functor Eval where
|
||||
fmap f (Ready x) = Ready (f x)
|
||||
fmap f (Thunk m) = Thunk (f <$> m)
|
||||
{-# INLINE fmap #-}
|
||||
|
||||
instance Applicative Eval where
|
||||
pure = return
|
||||
(<*>) = ap
|
||||
{-# INLINE pure #-}
|
||||
{-# INLINE (<*>) #-}
|
||||
|
||||
instance Monad Eval where
|
||||
return = Ready
|
||||
fail = Thunk . fail
|
||||
(>>=) = evalBind
|
||||
{-# INLINE return #-}
|
||||
{-# INLINE (>>=) #-}
|
||||
|
||||
instance MonadIO Eval where
|
||||
liftIO = io
|
||||
@ -104,6 +114,7 @@ instance MonadFix Eval where
|
||||
|
||||
io :: IO a -> Eval a
|
||||
io = Thunk
|
||||
{-# INLINE io #-}
|
||||
|
||||
|
||||
-- Errors ----------------------------------------------------------------------
|
||||
|
||||
@ -20,7 +20,7 @@ module Cryptol.Eval.Value where
|
||||
|
||||
import Data.IORef
|
||||
--import Data.Map (Map)
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Map.Strict as Map
|
||||
|
||||
import MonadLib
|
||||
|
||||
@ -141,6 +141,7 @@ splitSeqMap n xs = (hd,tl)
|
||||
hd = xs
|
||||
tl = SeqMap $ \i -> lookupSeqMap xs (i+n)
|
||||
|
||||
{-# INLINE memoMap #-}
|
||||
memoMap :: SeqMap b w -> Eval (SeqMap b w)
|
||||
memoMap x = do
|
||||
r <- io $ newIORef Map.empty
|
||||
@ -172,14 +173,14 @@ mapSeqMap f x =
|
||||
|
||||
-- | Generic value type, parameterized by bit and word types.
|
||||
data GenValue b w
|
||||
= VRecord [(Ident, Eval (GenValue b w))] -- @ { .. } @
|
||||
| VTuple [Eval (GenValue b w)] -- @ ( .. ) @
|
||||
| VBit b -- @ Bit @
|
||||
| VSeq !Integer !Bool (SeqMap b w) -- @ [n]a @
|
||||
= VRecord ![(Ident, Eval (GenValue b w))] -- @ { .. } @
|
||||
| VTuple ![Eval (GenValue b w)] -- @ ( .. ) @
|
||||
| VBit !b -- @ Bit @
|
||||
| VSeq !Integer !Bool !(SeqMap b w) -- @ [n]a @
|
||||
-- The boolean parameter indicates whether or not
|
||||
-- this is a sequence of bits.
|
||||
| VWord w -- @ [n]Bit @
|
||||
| VStream (SeqMap b w) -- @ [inf]a @
|
||||
| VWord !w -- @ [n]Bit @
|
||||
| VStream !(SeqMap b w) -- @ [inf]a @
|
||||
| VFun (Eval (GenValue b w) -> Eval (GenValue b w)) -- functions
|
||||
| VPoly (TValue -> Eval (GenValue b w)) -- polymorphic values (kind *)
|
||||
deriving (Generic)
|
||||
|
||||
@ -6,6 +6,7 @@
|
||||
-- Stability : provisional
|
||||
-- Portability : portable
|
||||
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE Trustworthy #-}
|
||||
{-# LANGUAGE TupleSections #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
@ -163,11 +164,12 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
|
||||
msg <- fromStr =<< s
|
||||
-- FIXME? get PPOPts from elsewhere?
|
||||
doc <- ppValue defaultPPOpts =<< x
|
||||
yv <- y
|
||||
io $ putStrLn $ show $ if null msg then
|
||||
doc
|
||||
else
|
||||
text msg <+> doc
|
||||
y)
|
||||
return yv)
|
||||
]
|
||||
|
||||
|
||||
@ -480,14 +482,26 @@ joinWords nParts nEach xs fallback =
|
||||
loop (mkBv 0 0) (enumerateSeqMap nParts xs)
|
||||
|
||||
where
|
||||
loop :: BV -> [Eval Value] -> Eval Value
|
||||
loop !bv [] = return $ VWord bv
|
||||
loop !bv (Ready (VWord w) : ws) = loop (joinWord bv w) ws
|
||||
loop !bv (w : ws) = w >>= \case
|
||||
VWord w' -> loop (joinWord bv w') ws
|
||||
_ -> fallback
|
||||
|
||||
loop _ _ = fallback
|
||||
|
||||
|
||||
-- loop !bv (Ready (VWord w) : ws) = loop (joinWord bv w) ws
|
||||
|
||||
-- loop !bv (w:ws) = do
|
||||
-- w' <- fromVWord "joinWords" =<< w
|
||||
-- loop (joinWord bv w') ws
|
||||
|
||||
|
||||
joinSeq :: TValue -> TValue -> TValue -> SeqValMap -> Eval Value
|
||||
joinSeq parts each a xs
|
||||
| Nat nEach <- numTValue each
|
||||
= mkSeq <$> memoMap (SeqMap $ \i -> do
|
||||
= return $ mkSeq $ (SeqMap $ \i -> do
|
||||
let (q,r) = divMod i nEach
|
||||
ys <- fromSeq =<< lookupSeqMap xs q
|
||||
lookupSeqMap ys r)
|
||||
@ -547,18 +561,25 @@ ecSplitV =
|
||||
tlam $ \ parts ->
|
||||
tlam $ \ each ->
|
||||
tlam $ \ a ->
|
||||
lam $ \ val -> do
|
||||
val' <- delay Nothing (fromSeq =<< val)
|
||||
case (numTValue parts, numTValue each) of
|
||||
(Nat p, Nat e) -> return $ VSeq p False $ SeqMap $ \i ->
|
||||
return $ VSeq e (isTBit a) $ SeqMap $ \j -> do
|
||||
xs <- val'
|
||||
lookupSeqMap xs (e * i + j)
|
||||
(Inf , Nat e) -> return $ VStream $ SeqMap $ \i ->
|
||||
return $ VSeq e (isTBit a) $ SeqMap $ \j -> do
|
||||
xs <- val'
|
||||
lookupSeqMap xs (e * i + j)
|
||||
_ -> evalPanic "splitV" ["invalid type arguments to split"]
|
||||
lam $ \ val ->
|
||||
case (numTValue parts, numTValue each) of
|
||||
(Nat p, Nat e) | isTBit a -> do
|
||||
BV _ x <- fromVWord "split" =<< val
|
||||
return $ VSeq p False $ SeqMap $ \i ->
|
||||
return $ VWord $ mkBv e $ (x `shiftR` (fromInteger ((p-i-1)*e)))
|
||||
(Nat p, Nat e) -> do
|
||||
val' <- delay Nothing (fromSeq =<< val)
|
||||
return $ VSeq p False $ SeqMap $ \i ->
|
||||
return $ VSeq e (isTBit a) $ SeqMap $ \j -> do
|
||||
xs <- val'
|
||||
lookupSeqMap xs (e * i + j)
|
||||
(Inf , Nat e) -> do
|
||||
val' <- delay Nothing (fromSeq =<< val)
|
||||
return $ VStream $ SeqMap $ \i ->
|
||||
return $ VSeq e (isTBit a) $ SeqMap $ \j -> do
|
||||
xs <- val'
|
||||
lookupSeqMap xs (e * i + j)
|
||||
_ -> evalPanic "splitV" ["invalid type arguments to split"]
|
||||
|
||||
-- | Split into infinitely many chunks
|
||||
infChunksOf :: Integer -> [a] -> [[a]]
|
||||
@ -604,6 +625,11 @@ ccatV :: TValue -> TValue -> TValue -> Eval Value -> Eval Value -> Eval Value
|
||||
ccatV _front _back (isTBit -> True) (Ready (VWord x)) (Ready (VWord y)) =
|
||||
return $ VWord $ joinWord x y
|
||||
|
||||
-- ccatV _front (numTValue -> Nat _nBack) (isTBit -> True) x y = do
|
||||
-- xw <- fromVWord "ccatV" =<< x
|
||||
-- yw <- fromVWord "ccatV" =<< y
|
||||
-- return $ VWord $ joinWord xw yw
|
||||
|
||||
ccatV front back elty l r = do
|
||||
l' <- delay Nothing (fromSeq =<< l)
|
||||
r' <- delay Nothing (fromSeq =<< r)
|
||||
@ -631,9 +657,14 @@ logicBinary op = loop
|
||||
case numTValue len of
|
||||
|
||||
-- words or finite sequences
|
||||
Nat w | isTBit aty, VWord (BV _ lw) <- l, VWord (BV _ rw) <- r
|
||||
-> return $ VWord $ (BV w (op lw rw))
|
||||
-- Nat w | isTBit aty, VWord (BV _ lw) <- l, VWord (BV _ rw) <- r
|
||||
-- -> return $ VWord $ (BV w (op lw rw))
|
||||
-- We assume that bitwise ops do not need re-masking
|
||||
Nat w | isTBit aty -> do
|
||||
BV _ lw <- fromVWord "logicLeft" l
|
||||
BV _ rw <- fromVWord "logicRight" r
|
||||
return $ VWord $ mkBv w (op lw rw)
|
||||
|
||||
| otherwise -> VSeq w (isTBit aty) <$> (join (zipSeqMap (loop aty) <$> (fromSeq l) <*> (fromSeq r)))
|
||||
|
||||
-- streams
|
||||
@ -671,8 +702,12 @@ logicUnary op = loop
|
||||
case numTValue len of
|
||||
|
||||
-- words or finite sequences
|
||||
Nat w | isTBit ety, VWord (BV _ v) <- val
|
||||
-> return $ VWord (mkBv w $ op v)
|
||||
-- Nat w | isTBit ety, VWord (BV _ v) <- val
|
||||
-- -> return $ VWord (mkBv w $ op v)
|
||||
Nat w | isTBit ety
|
||||
-> do v <- fromWord "logicUnary" val
|
||||
return $ VWord (mkBv w $ op v)
|
||||
|
||||
| otherwise
|
||||
-> VSeq w (isTBit ety) <$> (mapSeqMap (loop ety) =<< fromSeq val)
|
||||
|
||||
@ -705,11 +740,12 @@ logicShift opW opS
|
||||
lam $ \ r -> do
|
||||
if isTBit c
|
||||
then do -- words
|
||||
l' <- l
|
||||
BV w i <- fromVWord ("logicShift " ++ show l') l'
|
||||
VWord <$> (BV w <$> (opW w i <$> (fromWord "logic shift amount" =<< r)))
|
||||
BV w x <- fromVWord "logicShift" =<< l
|
||||
BV _ i <- fromVWord "logicShift amount" =<< r
|
||||
return $ VWord $ BV w $ opW w x i
|
||||
else do
|
||||
mkSeq a c <$> (opS a c <$> (fromSeq =<< l) <*> (fromWord "logic shift amount" =<< r))
|
||||
BV _ i <- fromVWord "logicShift amount" =<< r
|
||||
mkSeq a c <$> (opS a c <$> (fromSeq =<< l) <*> return i)
|
||||
|
||||
-- Left shift for words.
|
||||
shiftLW :: Integer -> Integer -> Integer -> Integer
|
||||
|
||||
Loading…
Reference in New Issue
Block a user