unisonweb/unison
1
0
Fork 0
mirror of https://github.com/unisonweb/unison.git synced 2024-09-21 15:28:15 +03:00
Code Issues Projects Releases Wiki Activity

fix algos add a transcript that fails like a lot of others

Browse Source
This commit is contained in:
Stew O'Connor 2021-08-02 22:29:10 -07:00
parent 988ab694a1
commit e40aeee5d3
2 changed files with 48 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
parser-typechecker/src/Unison/Util/Bytes.hs
View File

@ -214,29 +214,29 @@ fillBE n i p = poke p (fromIntegral (shiftR n (i * 8)))
>> fillBE n (i - 1) (p `plusPtr` 1)
encodeNat64be :: Word64 -> Bytes
encodeNat64be n = Bytes (T.singleton (view (B.unsafeCreate 8 (fillBE n 8))))
encodeNat64be n = Bytes (T.singleton (view (B.unsafeCreate 8 (fillBE n 7))))
encodeNat32be :: Word64 -> Bytes
encodeNat32be n = Bytes (T.singleton (view (B.unsafeCreate 4 (fillBE n 4))))
encodeNat32be n = Bytes (T.singleton (view (B.unsafeCreate 4 (fillBE n 3))))
encodeNat16be :: Word64 -> Bytes
encodeNat16be n = Bytes (T.singleton (view (B.unsafeCreate 2 (fillBE n 2))))
encodeNat16be n = Bytes (T.singleton (view (B.unsafeCreate 2 (fillBE n 1))))
fillLE :: Word64 -> Int -> Int -> Ptr Word8 -> IO ()
fillLE n i j p =
if i == j then
poke p (fromIntegral n) >> return ()
return ()
else
poke p (fromIntegral (shiftR n (i * 8))) >> fillLE n (i + 1) j (p `plusPtr` 1)
encodeNat64le :: Word64 -> Bytes
encodeNat64le n = Bytes (T.singleton (view (B.unsafeCreate 8 (fillLE n 0 7))))
encodeNat64le n = Bytes (T.singleton (view (B.unsafeCreate 8 (fillLE n 0 8))))
encodeNat32le :: Word64 -> Bytes
encodeNat32le n = Bytes (T.singleton (view (B.unsafeCreate 4 (fillLE n 0 3))))
encodeNat32le n = Bytes (T.singleton (view (B.unsafeCreate 4 (fillLE n 0 4))))
encodeNat16le :: Word64 -> Bytes
encodeNat16le n = Bytes (T.singleton (view (B.unsafeCreate 2 (fillLE n 0 1))))
encodeNat16le n = Bytes (T.singleton (view (B.unsafeCreate 2 (fillLE n 0 2))))
toBase16 :: Bytes -> Bytes
toBase16 bs = foldl' step empty (chunks bs) where

41
unison-src/transcripts-using-base/binary-encoding-nats.md Normal file
View File

@ -0,0 +1,41 @@
```ucm:hide
.> builtins.merge
```
```unison
unique ability Abort where
abort: b
roundTrip: Nat -> Boolean
roundTrip n =
checkDecode: Optional (Nat, Bytes) -> {Abort} Bytes
checkDecode = cases
Some (n', bs) -> if n == n' then
watch "pass" bs
else
!(watch "fail")
abort
checkDecodes bs = cases
[] -> bs
dec +: rest -> checkDecodes (checkDecode (dec bs)) rest
go: Nat -> {Abort} Boolean
go n =
bs = ((encodeNat64be n) ++ ((encodeNat32be n) ++ ((encodeNat16be n) ++ ((encodeNat64le n) ++ ((encodeNat32le n) ++ (encodeNat16le n))))))
bs' = checkDecodes bs [decodeNat64be, decodeNat32be, decodeNat16be, decodeNat64le, decodeNat32le, decodeNat16le ]
watch "end" ((Bytes.size bs') == 0)
handle go n with cases
{ Abort.abort -> _ } -> false
{ r } -> r
test> testRoundTrip = runs 100 '(expect roundTrip (natIn 0 1000))
```