Merge pull request #1303 from GaloisInc/primitive-scanl

Primitive scanl

lib/Cryptol.cry

@@ -915,14 +915,9 @@ primitive updateEnd : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a -> [n]a
  * given update pairs.
  */
 updates : {n, k, ix, a} (Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a
-updates xs0 idxs vals = xss!0
- where
-   xss = [ xs0 ] #
-         [ update xs i b
-         | xs <- xss
-         | i  <- idxs
-         | b  <- vals
-         ]
+updates xs0 idxs vals = foldl upd xs0 (zip idxs vals)
+  where
+    upd xs (i,b) = update xs i b
 
 /**
  * Perform a series of updates to a sequence.  The first argument is
@@ -932,14 +927,9 @@ updates xs0 idxs vals = xss!0
  * given update pairs.
  */
 updatesEnd : {n, k, ix, a} (fin n, Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a
-updatesEnd xs0 idxs vals = xss!0
- where
-   xss = [ xs0 ] #
-         [ updateEnd xs i b
-         | xs  <- xss
-         | i   <- idxs
-         | b   <- vals
-         ]
+updatesEnd xs0 idxs vals = foldl upd xs0 (zip idxs vals)
+  where
+    upd xs (i,b) = updateEnd xs i b
 
 /**
  * Produce a sequence using a generating function.
@@ -1157,27 +1147,22 @@ foldr' f acc xs = foldl' g acc (reverse xs)
 sum : {n, a} (fin n, Eq a, Ring a) => [n]a -> a
 sum xs = foldl' (+) (fromInteger 0) xs
 
-
 /**
  * Compute the product of the values in the sequence.
  */
 product : {n, a} (fin n, Eq a, Ring a) => [n]a -> a
 product xs = foldl' (*) (fromInteger 1) xs
 
-
 /**
  * Scan left is like a foldl that also emits the intermediate values.
  */
-scanl : {n, b, a}  (b -> a -> b) -> b -> [n]a -> [n+1]b
-scanl f acc xs = ys
-  where ys = [acc] # [f a x | a <- ys | x <- xs]
+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 f acc xs = reverse ys
-  where ys = [acc] # [f x a | a <- ys | x <- reverse xs]
+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))
 
 /**
  * Repeat a value.
@@ -1220,5 +1205,4 @@ curry f = \a b -> f (a, b)
  * list of successive function applications.
  */
 iterate : {a} (a -> a) -> a -> [inf]a
-iterate f x = xs
-  where xs = [x] # [ f v | v <- xs ]
+iterate f z = scanl (\x _ -> f x) z (zero:[inf]())

lib/Cryptol/Reference.cry

@@ -44,3 +44,33 @@ pmod x y = if y == 0 then 0/0 else last zs
     powers = [reduce 1] # [ reduce (p << 1) | p <- powers ]
 
     zs = [0] # [ z ^ (if xi then tail p else 0) | xi <- reverse x | p <- powers | z <- zs ]
+
+/**
+ * Functional left fold.
+ *
+ * foldl (+) 0 [1,2,3] = ((0 + 1) + 2) + 3
+ *
+ * Reference implementation.
+ */
+foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
+foldl f z bs = last (scanl f z bs)
+
+/**
+ * Scan left is like a foldl that also emits the intermediate values.
+ *
+ * Reference implementation.
+ */
+scanl : {n, a, b}  (a -> b -> a) -> a -> [n]b -> [1+n]a
+scanl f z bs = as
+  where
+    as = [z] # [ f a b | a <- as | b <- bs ]
+
+/**
+ * Map a function iteratively over a seed value, producing an infinite
+ * list of successive function applications.
+ *
+ * Reference implementation.
+ */
+iterate : {a} (a -> a) -> a -> [inf]a
+iterate f z = xs
+  where xs = [z] # [ f x | x <- xs ]

src/Cryptol/Eval/Generic.hs

@@ -35,7 +35,7 @@ import Data.Map(Map)
 import Data.Ratio ((%))
 
 import Cryptol.TypeCheck.AST
-import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),nMul)
+import Cryptol.TypeCheck.Solver.InfNat (Nat'(..),nMul,nAdd)
 import Cryptol.Backend
 import Cryptol.Backend.Concrete (Concrete(..))
 import Cryptol.Backend.Monad( Eval, evalPanic, EvalError(..), Unsupported(..) )
@@ -1814,6 +1814,40 @@ foldl'V sym =
        go1 f a' bs
 
 
+-- 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 ->
+  PTyPoly  \a ->
+  PTyPoly  \_b ->
+  PFun     \f ->
+  PFun     \z ->
+  PStrict  \v ->
+  PPrim
+    do sm <- case v of
+            VSeq _ m   -> scan n f z m
+            VWord _ wv -> scan n f z (VBit <$> asBitsMap sym wv)
+            VStream m  -> scan n f z m
+            _ -> panic "Cryptol.Eval.Generic.scanlV" ["Expected sequence"]
+       mkSeq sym (nAdd (Nat 1) n) a sm
+
+ where
+  scan :: Nat' ->
+          SEval sym (GenValue sym) ->
+          SEval sym (GenValue sym) ->
+          (SeqMap sym (GenValue sym)) ->
+          SEval sym (SeqMap sym (GenValue sym))
+  scan n f z m =
+    do (result, fill) <- sDeclareHole sym "scanl"
+       fill $ memoMap sym (nAdd (Nat 1) n) $ indexSeqMap $ \i ->
+         if i == 0 then z
+         else
+           do r <- result
+              f'  <- fromVFun sym <$> f
+              f'' <- fromVFun sym <$> f' (lookupSeqMap r (i-1))
+              f'' (lookupSeqMap m (i-1))
+       result
+
 -- Random Values ---------------------------------------------------------------
 
 {-# SPECIALIZE randomV ::
@@ -2200,6 +2234,9 @@ genericPrimTable sym getEOpts =
   , ("foldl'"     , {-# SCC "Prelude::foldl'" #-}
                     foldl'V sym)
 
+  , ("scanl"      , {-# SCC "Prelude::scanl" #-}
+                    scanlV sym)
+
   , ("deepseq"    , {-# SCC "Prelude::deepseq" #-}
                     PTyPoly \_a ->
                     PTyPoly \_b ->

tests/issues/T146.icry.stdout

@@ -4,15 +4,15 @@ Loading module Main
 
 [error] at T146.cry:1:18--6:10:
   The type ?a is not sufficiently polymorphic.
-    It cannot depend on quantified variables: fv`912
+    It cannot depend on quantified variables: fv`902
     When checking type of field 'v0'
   where
   ?a is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24
-  fv`912 is signature variable 'fv' at T146.cry:11:10--11:12
+  fv`902 is signature variable 'fv' at T146.cry:11:10--11:12
 [error] at T146.cry:5:19--5:24:
   The type ?b is not sufficiently polymorphic.
-    It cannot depend on quantified variables: fv`912
+    It cannot depend on quantified variables: fv`902
     When checking signature variable 'fv'
   where
   ?b is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24
-  fv`912 is signature variable 'fv' at T146.cry:11:10--11:12
+  fv`902 is signature variable 'fv' at T146.cry:11:10--11:12

tests/issues/issue1024.icry.stdout

@@ -13,20 +13,20 @@ Loading module Main
     Unused name: g
 
 [error] at issue1024a.cry:1:6--1:11:
-  Illegal kind assigned to type variable: f`909
+  Illegal kind assigned to type variable: f`899
   Unexpected: # -> *
   where
-  f`909 is signature variable 'f' at issue1024a.cry:1:12--1:24
+  f`899 is signature variable 'f' at issue1024a.cry:1:12--1:24
 [error] at issue1024a.cry:2:6--2:13:
-  Illegal kind assigned to type variable: f`910
+  Illegal kind assigned to type variable: f`900
   Unexpected: Prop
   where
-  f`910 is signature variable 'f' at issue1024a.cry:2:14--2:24
+  f`900 is signature variable 'f' at issue1024a.cry:2:14--2:24
 [error] at issue1024a.cry:4:13--4:49:
-  Illegal kind assigned to type variable: f`912
+  Illegal kind assigned to type variable: f`902
   Unexpected: # -> *
   where
-  f`912 is signature variable 'f' at issue1024a.cry:4:22--4:32
+  f`902 is signature variable 'f' at issue1024a.cry:4:22--4:32
 Loading module Cryptol
 Loading module Main
 0xffff

tests/issues/issue103.icry.stdout

@@ -2,7 +2,7 @@ Loading module Cryptol
 
 Run-time error: undefined
 -- Backtrace --
-Cryptol::error called at Cryptol:1043:13--1043:18
+Cryptol::error called at Cryptol:1033:13--1033:18
 Cryptol::undefined called at issue103.icry:1:9--1:18
 Using exhaustive testing.
 Testing... ERROR for the following inputs:

tests/issues/issue226.icry.stdout

@@ -193,7 +193,7 @@ Symbols
     roundAway : {a} (Round a) => a -> Integer
     roundToEven : {a} (Round a) => a -> Integer
     sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
-    scanl : {n, b, a} (b -> a -> b) -> b -> [n]a -> [1 + n]b
+    scanl : {n, a, b} (a -> b -> a) -> a -> [n]b -> [1 + n]a
     scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b
     scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
     sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m]

tests/issues/issue290v2.icry.stdout

@@ -4,9 +4,9 @@ Loading module Main
 
 [error] at issue290v2.cry:2:1--2:19:
   Unsolved constraints:
-    • n`909 == 1
+    • n`899 == 1
         arising from
         checking a pattern: type of 1st argument of Main::minMax
         at issue290v2.cry:2:8--2:11
   where
-  n`909 is signature variable 'n' at issue290v2.cry:1:11--1:12
+  n`899 is signature variable 'n' at issue290v2.cry:1:11--1:12

tests/issues/issue723.icry.stdout

@@ -10,9 +10,9 @@ Loading module Main
       assuming
         • fin k
       the following constraints hold:
-        • k == n`909
+        • k == n`899
             arising from
             matching types
             at issue723.cry:7:17--7:19
   where
-  n`909 is signature variable 'n' at issue723.cry:1:6--1:7
+  n`899 is signature variable 'n' at issue723.cry:1:6--1:7

tests/regression/reference.cry

@@ -0,0 +1,12 @@
+import Cryptol::Reference as Ref
+
+// NB, using subtraction here because is is not commutative or associative
+
+property foldl_eq (z:Integer) (xs:[10]Integer) =
+  foldl (-) z xs == Ref::foldl (-) z xs
+
+property scanl_eq (z:Integer) (xs:[10]Integer) =
+  scanl (-) z xs == Ref::scanl (-) z xs
+
+property iterate_eq (z:Integer) (i:[8]) =
+  (iterate (\x -> x + 1) z)@i == (Ref::iterate (\x -> x + 1) z)@i

tests/regression/reference.icry

@@ -0,0 +1,10 @@
+:l reference.cry
+
+:set tests=1000
+:check
+
+:set prover=sbv-z3
+:prove
+
+:set prover=w4-z3
+:prove

tests/regression/reference.icry.stdout

@@ -0,0 +1,22 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Cryptol::Reference
+Loading module Main
+property foldl_eq Using random testing.
+Testing... Passed 1000 tests.
+property scanl_eq Using random testing.
+Testing... Passed 1000 tests.
+property iterate_eq Using random testing.
+Testing... Passed 1000 tests.
+:prove foldl_eq
+	Q.E.D.
+:prove scanl_eq
+	Q.E.D.
+:prove iterate_eq
+	Q.E.D.
+:prove foldl_eq
+	Q.E.D.
+:prove scanl_eq
+	Q.E.D.
+:prove iterate_eq
+	Q.E.D.

tests/regression/safety.icry.stdout

@@ -3,7 +3,7 @@ Counterexample
 (\x -> assert x "asdf" "asdf") False ~> ERROR
 Run-time error: asdf
 -- Backtrace --
-Cryptol::error called at Cryptol:1051:41--1051:46
+Cryptol::error called at Cryptol:1041:41--1041:46
 Cryptol::assert called at safety.icry:3:14--3:20
 <interactive>::it called at safety.icry:3:7--3:37
 Counterexample

tests/regression/tc-errors.icry.stdout

@@ -83,19 +83,19 @@ Loading module Main
 
 [error] at tc-errors-5.cry:2:5--2:7:
   Inferred type is not sufficiently polymorphic.
-    Quantified variable: a`909
+    Quantified variable: a`899
     cannot match type: [0]?a
     When checking the type of 'Main::f'
   where
   ?a is type of sequence member at tc-errors-5.cry:2:5--2:7
-  a`909 is signature variable 'a' at tc-errors-5.cry:1:6--1:7
+  a`899 is signature variable 'a' at tc-errors-5.cry:1:6--1:7
 Loading module Cryptol
 Loading module Main
 
 [error] at tc-errors-6.cry:4:7--4:8:
   The type ?a is not sufficiently polymorphic.
-    It cannot depend on quantified variables: b`913
+    It cannot depend on quantified variables: b`903
     When checking the type of 'g'
   where
   ?a is the type of 'x' at tc-errors-6.cry:1:3--1:4
-  b`913 is signature variable 'b' at tc-errors-6.cry:3:8--3:9
+  b`903 is signature variable 'b' at tc-errors-6.cry:3:8--3:9