Skip to content

Commit

Permalink
Tweak the type signature for scanl and scanr.
Browse files Browse the repository at this point in the history
It is convenient for Coq extraction for the constant 1 factor
to be on the left of the addition symbol.
  • Loading branch information
robdockins committed Nov 13, 2021
1 parent 6cdce29 commit 5484a95
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
4 changes: 2 additions & 2 deletions lib/Cryptol.cry
Original file line number Diff line number Diff line change
Expand Up @@ -1158,12 +1158,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))

/**
Expand Down
2 changes: 1 addition & 1 deletion src/Cryptol/Eval/Generic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down

0 comments on commit 5484a95

Please sign in to comment.