GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-24 16:31:34 +03:00
Code Issues Projects Releases Wiki Activity

Implement a missing case in the definition of 'transpose'.

Browse Source 
Fixes issue #407
This commit is contained in:
Robert Dockins 2017-05-10 16:42:45 -07:00
parent f5aa763988
commit 7add78ec3c
3 changed files with 32 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -739,7 +739,7 @@ transposeV :: BitWord b w
-> GenValue b w -> GenValue b w
-> Eval (GenValue b w) -> Eval (GenValue b w)
transposeV a b c xs transposeV a b c xs
| isTBit c, Nat na <- a = | isTBit c, Nat na <- a = -- Fin a => [a][b]Bit -> [b][a]Bit
return $ bseq $ IndexSeqMap $ \bi -> return $ bseq $ IndexSeqMap $ \bi ->
return $ VWord na $ return $ BitsVal $ return $ VWord na $ return $ BitsVal $
Seq.fromFunction (fromInteger na) $ \ai -> do Seq.fromFunction (fromInteger na) $ \ai -> do
@ -749,7 +749,16 @@ transposeV a b c xs
VWord _ wv -> flip bitsSeq bi =<< wv VWord _ wv -> flip bitsSeq bi =<< wv
_ -> evalPanic "transpose" ["expected sequence of bits"] _ -> evalPanic "transpose" ["expected sequence of bits"]
| otherwise = do | isTBit c, Inf <- a = -- [inf][b]Bit -> [b][inf]Bit
return $ bseq $ IndexSeqMap $ \bi ->
return $ VStream $ IndexSeqMap $ \ai ->
do ys <- flip lookupSeqMap ai =<< fromSeq "transposeV" xs
case ys of
VStream ys' -> VBit . fromVBit <$> lookupSeqMap ys' bi
VWord _ wv -> VBit <$> (flip bitsSeq bi =<< wv)
_ -> evalPanic "transpose" ["expected sequence of bits"]
| otherwise = -- [a][b]c -> [b][a]c
return $ bseq $ IndexSeqMap $ \bi -> return $ bseq $ IndexSeqMap $ \bi ->
return $ aseq $ IndexSeqMap $ \ai -> do return $ aseq $ IndexSeqMap $ \ai -> do
ys <- flip lookupSeqMap ai =<< fromSeq "transposeV 1" xs ys <- flip lookupSeqMap ai =<< fromSeq "transposeV 1" xs

10
tests/issues/issue407.icry Normal file
View File

@ -0,0 +1,10 @@
:set prover-stats = off
transpose [0x0, 1 ...]
:pro (\(x:[4]) -> (transpose [x ...])@0@0 == False)
:pro (\(x:[4]) -> (transpose [x ...])@0@0 == x@0)
:pro (\(x:[4]) -> (transpose [x ...])@1@0 == x@1)
:pro (\(x:[4]) -> (transpose [x ...])@2@0 == x@2)
:pro (\(x:[4]) -> (transpose [x ...])@3@0 == x@3)
:pro (\(x:[4]) -> (transpose [x ...])@3@1 == ~(x@3))

11
tests/issues/issue407.icry.stdout Normal file
View File

@ -0,0 +1,11 @@
Loading module Cryptol
[[False, False, False, False, False, ...],
[False, False, False, False, True, ...],
[False, False, True, True, False, ...],
[False, True, False, True, False, ...]]
(\(x : [4]) -> (transpose [x ...]) @ 0 @ 0 == False) 0x8 = False
Q.E.D.
Q.E.D.
Q.E.D.
Q.E.D.
Q.E.D.