Modify 'updates' and 'updatesEnd' to take the indices and values

as separate vector arguments, rather than as a single vector
argument of pairs.

docs/CryptolPrims.md

@@ -73,8 +73,8 @@ Sequences
     (!!)       : {n,a,m,i} (fin n) => [n]a -> [m][i] -> [m]a
     update     : {n,a,m} (fin m) => [n]a -> [m] -> a -> [n]a
     updateEnd  : {n,a,m} (fin n, fin m) => [n]a -> [m] -> a -> [n]a
-    updates    : {n,a,m,d} (fin m, fin d) => [n]a -> [d]([m], a) -> [n]a
-    updatesEnd : {n,a,m,d} (fin n, fin m, fin d) => [n]a -> [d]([m], a) -> [n]a
+    updates    : {n,a,m,d} (fin m, fin d) => [n]a -> [d][m] -> [d]a -> [n]a
+    updatesEnd : {n,a,m,d} (fin n, fin m, fin d) => [n]a -> [d][m] -> [d]a -> [n]a
 
     // Abbreviations
     groupBy n = split`{each  = n}

lib/Cryptol.cry

@@ -308,34 +308,36 @@ primitive updateEnd : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b -> [a]b
 /**
  * Perform a series of updates to a sequence.  The first argument is
  * the initial sequence to update.  The second argument is a sequence
- * of index/element pairs with which to update the sequence.
+ * of indices, and the third argument is a sequence of values.
  * This function applies the 'update' function in sequence with the
  * given update pairs.
  */
-updates : {a,b,c,d} (fin c, fin d) => [a]b -> [d]([c], b) -> [a]b
-updates xs0 upds = xss!0
+updates : {a,b,c,d} (fin c, fin d) => [a]b -> [d][c] -> [d]b -> [a]b
+updates xs0 idxs vals = xss!0
  where
    xss = [ xs0 ] #
          [ update xs i b
-	 | xs    <- xss
-	 | (i,b) <- upds
-	 ]
+         | xs <- xss
+         | i  <- idxs
+         | b  <- vals
+         ]
 
 /**
  * Perform a series of updates to a sequence.  The first argument is
  * the initial sequence to update.  The second argument is a sequence
- * of index/element pairs with which to update the sequence.
+ * of indices, and the third argument is a sequence of values.
  * This function applies the 'updateEnd' function in sequence with the
  * given update pairs.
  */
-updatesEnd : {a,b,c,d} (fin a, fin c, fin d) => [a]b -> [d]([c], b) -> [a]b
-updatesEnd xs0 upds = xss!0
+updatesEnd : {a,b,c,d} (fin a, fin c, fin d) => [a]b -> [d][c] -> [d]b -> [a]b
+updatesEnd xs0 idxs vals = xss!0
  where
    xss = [ xs0 ] #
          [ updateEnd xs i b
-	 | xs    <- xss
-	 | (i,b) <- upds
-	 ]
+         | xs  <- xss
+         | i   <- idxs
+         | b   <- vals
+         ]
 
 
 primitive fromThen : {first, next, bits, len}

tests/issues/issue226.icry.stdout

@@ -88,10 +88,10 @@ Symbols
     undefined : {a} a
     update : {a, b, c} (fin c) => [a]b -> [c] -> b -> [a]b
     updateEnd : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b -> [a]b
-    updates : {a, b, c, d} (fin c, fin d) => [a]b -> [d]([c],
-                                                         b) -> [a]b
-    updatesEnd : {a, b, c, d} (fin a, fin c, fin d) => [a]b -> [d]([c],
-                                                                   b) -> [a]b
+    updates : {a, b, c, d} (fin c,
+                            fin d) => [a]b -> [d][c] -> [d]b -> [a]b
+    updatesEnd : {a, b, c, d} (fin a, fin c,
+                               fin d) => [a]b -> [d][c] -> [d]b -> [a]b
     width : {bits, len, elem} (fin len, fin bits,
                                bits >= width len) => [len]elem -> [bits]
     zero : {a} a

tests/issues/issue290v2.icry.stdout

@@ -4,7 +4,7 @@ Loading module Main
 
 [error] at ./issue290v2.cry:2:1--2:19:
   Unsolved constraint:
-    a`303 == 1
+    a`285 == 1
       arising from
       checking a pattern: type of 1st argument of Main::minMax
       at ./issue290v2.cry:2:8--2:11