From 41613ade025cfcbea932ee4f9be3fd2ca43ed78f Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Fri, 12 Nov 2021 18:29:19 -0800 Subject: [PATCH] Tweak the type signature for `scanl` and `scanr`. It is convenient for Coq extraction for the constant 1 factor to be on the left of the addition symbol. --- lib/Cryptol.cry | 4 ++-- src/Cryptol/Eval/Generic.hs | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index 17249c3d..ca99aad7 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -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)) /** diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs index 1d3fdacd..f98203cd 100644 --- a/src/Cryptol/Eval/Generic.hs +++ b/src/Cryptol/Eval/Generic.hs @@ -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 ->