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

Tweak the type signature for scanl and scanr.

Browse Source 
It is convenient for Coq extraction for the constant 1 factor
to be on the left of the addition symbol.
This commit is contained in:
Rob Dockins 2021-11-12 18:29:19 -08:00
parent 253a7f26ab
commit 41613ade02
2 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lib/Cryptol.cry
View File

@ -1156,12 +1156,12 @@ product xs = foldl' (*) (fromInteger 1) xs
/**
* Scan left is like a foldl that also emits the intermediate values.
*/
primitive scanl : {n, a, b} (a -> b -> a) -> a -> [n]b -> [n+1]a
primitive scanl : {n, a, b} (a -> b -> a) -> a -> [n]b -> [1+n]a
/**
* Scan right is like a foldr that also emits the intermediate values.
*/
scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [n+1]b
scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1+n]b
scanr f acc xs = reverse (scanl (\a b -> f b a) acc (reverse xs))
/**

2
src/Cryptol/Eval/Generic.hs
View File

@ -1814,7 +1814,7 @@ foldl'V sym =
go1 f a' bs
-- scanl : {n, a, b} (a -> b -> a) -> a -> [n]b -> [n+1]a
-- scanl : {n, a, b} (a -> b -> a) -> a -> [n]b -> [1+n]a
scanlV :: forall sym. Backend sym => sym -> Prim sym
scanlV sym =
PNumPoly \n ->