Merge branch 'release/2.4.0'

docs/CryptolPrims.md

@@ -74,7 +74,6 @@ Sequences
 
 
     // Abbreviations
-    splitBy n = split`{parts = n}
     groupBy n = split`{each  = n}
     tail n    = splitAt`{front = 1}.1
     take n    = splitAt`{front = n}.0

docs/ProgrammingCryptol/classic/Classic.tex

@@ -701,7 +701,8 @@ The signature\indSignature on {\tt msg'} is revealing: We are taking a
 string that has {\tt diameter * row} characters in it, and chopping it
 up so that it has {\tt row} elements, each of which is a string that
 has {\tt diameter} characters in it.  Here is Cryptol in action,
-encrypting the message {\tt ATTACKATDAWN}:
+encrypting the message {\tt ATTACKATDAWN}, with {\tt diameter} set to
+{\tt 3}:
 \begin{Verbatim}
   Cryptol> :set ascii=on
   Cryptol> scytale `{diameter=3} "ATTACKATDAWN"

docs/ProgrammingCryptol/crashCourse/CrashCourse.tex

@@ -672,11 +672,11 @@ worthwhile to try the following exercises to gain basic familiarity
 with the basic operations.
 
 \begin{Exercise}\label{ex:seq:11}
-Try the following expressions:\indTake\indDrop\indSplitBy\indGroup\indJoin\indTranspose
+Try the following expressions:\indTake\indDrop\indSplit\indGroup\indJoin\indTranspose
 \begin{Verbatim}
   take`{3} [1 .. 12]
   drop`{3} [1 .. 12]
-  splitBy`{3} [1 .. 12]
+  split`{3} [1 .. 12]
   groupBy`{3} [1 .. 12]
   join [[1 .. 4], [5 .. 8], [9 .. 12]]
   join [[1, 2, 3], [4, 5, 6], [7, 8, 9], [10, 11, 12]]
@@ -696,7 +696,7 @@ Here are Cryptol's responses:
   [1, 2, 3]
   Cryptol> drop`{3} [1 .. 12]
   [4, 5, 6, 7, 8, 9, 10, 11, 12]
-  Cryptol> splitBy`{3}[1 .. 12]
+  Cryptol> split`{3}[1 .. 12]
   [[1, 2, 3, 4], [5, 6, 7, 8], [9, 10, 11, 12]]
   Cryptol> groupBy`{3} [1 .. 12]
   [[1, 2, 3], [4, 5, 6], [7, 8, 9], [10, 11, 12]]
@@ -716,10 +716,10 @@ Here are Cryptol's responses:
 \begin{Exercise}\label{ex:seq:12}
   Based on your intuitions from the previous exercise, derive laws
   between the following pairs of functions: {\tt take} and {\tt drop};
-  {\tt join} and {\tt splitBy}; {\tt join} and {\tt groupBy}; {\tt
-    splitBy} and {\tt groupBy} and {\tt transpose} and itself.  For
+  {\tt join} and {\tt split}; {\tt join} and {\tt groupBy}; {\tt
+    split} and {\tt groupBy} and {\tt transpose} and itself.  For
   instance, {\tt take} and {\tt drop} satisfy the following
-  equality:\indTake\indDrop\indJoin\indSplitBy\indGroup\indTranspose
+  equality:\indTake\indDrop\indJoin\indSplit\indGroup\indTranspose
 \begin{Verbatim}
    (take`{n} xs) # (drop`{n} xs) == xs
 \end{Verbatim}
@@ -729,11 +729,11 @@ satisfy.
 \end{Exercise}
 \begin{Answer}\ansref{ex:seq:12}
   The following equalities are the simplest
-  candidates:\indJoin\indSplitBy\indGroup\indTranspose
+  candidates:\indJoin\indSplit\indGroup\indTranspose
 \begin{Verbatim}
-  join (splitBy`{parts=n} xs) == xs
+  join (split`{parts=n} xs) == xs
   join (groupBy`{each=n} xs) == xs
-  splitBy`{parts=n} xs == groupBy`{each=m} xs
+  split`{parts=n} xs == groupBy`{each=m} xs
   transpose (transpose xs) == xs
 \end{Verbatim}
 In the first two equalities {\tt n} must be a divisor of the length of
@@ -757,13 +757,12 @@ holds for all equal length sequences {\tt xs0}, {\tt xs1}, $\ldots$,
 {\tt xsN}.
 \end{Answer}
 
-\paragraph*{Type-directed splits} We have studied the functions {\tt
-  groupBy}\indGroup and {\tt splitBy}\indSplitBy above.  Cryptol also
-provides a function {\tt split}\indSplit that can split a sequence
-into any number of equal-length segments.  A common way to use {\tt
-  split} is to be explicit about the type of its result, instead of
-passing arguments as we did above with {\tt splitBy} and {\tt
-  groupBy}.
+\paragraph*{Type-directed splits} The Cryptol primitive function {\tt
+  split}\indSplit splits a sequence into any number of equal-length
+parts. An explicit result type is often used with {\tt split}, since
+the number of parts and the number of elements in each part are not
+given as arguments, but are determined by the type of the argument
+sequence and the result context.
 \begin{Verbatim}
   Cryptol> split [1..12] : [1][12][8]
   [[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]]
@@ -776,10 +775,11 @@ Here is what happens if we do {\em not} give an explicit signature on
 the result:\indSignature
 \begin{Verbatim}
   Cryptol> split [1..12]
-  <polymorphic value>
+  Cannot evaluate polymorphic value.
+  Type: {a, b, c} (fin b, fin c, b * a == 12, c >= 4) => [a][b][c]
   Cryptol> :t split [1..12]
-  split [1 .. 12] : {a, b, c} (a >= 4, fin a, fin c,
-                              12 == b * c) => [b][c][a]
+  split [1 .. 12] : {a, b, c} (fin b, fin c, b * a == 12,
+                               c >= 4) => [a][b][c]
 \end{Verbatim}
 %% cryptol 1 said: : {a b c} (fin c,c >= 4,a*b == 12) => [a][b][c]
 
@@ -1057,7 +1057,7 @@ remaining expressions.
   [0, 0, 1, 4]
 \end{Verbatim}
 We will show the evaluation steps for {\tt groupBy} here, and urge the
-reader to do the same for {\tt splitBy}:
+reader to do the same for {\tt split}:
 \begin{Verbatim}
   groupBy`{3} (12:[12])
     = groupBy`{3} [False, False, False, False, False, False, 
@@ -1801,21 +1801,6 @@ Cryptol divides {\tt 10} (the size of the second argument) by {\tt 3}
 does not match what we told it to use for {\tt parts}, i.e., {\tt
   2}. It is not hard to see that there is no instantiation to make this
 work, since {\tt 10} is not divisible by {\tt 3}.
-
-The message we get for the last equation is truly interesting:\indFin
-\begin{Verbatim}
-  Cryptol> groupBy`{3} [1..10]
-  <polymorphic value>
-  Cryptol> :t groupBy`{3} [1..10]
-  {a, b} (a >= 4, fin a, 10 == 3 * b) => [b][3][a]
-\end{Verbatim}
-Cryptol is telling us that the result is a polymorphic value, for all
-values of {\tt a} such that {\tt 3*a} is {\tt 10}.  Type inference in
-the presence of arbitrary expressions is undecidable,\indUndecidable
-and hence Cryptol tells us that this value will be instantiated to a
-concrete type as soon as we tell it what that {\tt a} must be. Since
-there is no such {\tt a}, we will never be able to use this value in a
-monomorphic context.
 \end{Answer}
 
 %~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

docs/ProgrammingCryptol/prims/Primitives.tex

@@ -24,25 +24,25 @@ primsPlaceHolder=1;
 %    negate            : {a b} (a >= 1) => [a]b -> [a]b
 \paragraph*{Polynomial arithmetic}
 \begin{Verbatim}
-    pdiv : {a, b} (fin a, fin b) => [a] -> [b] -> [a]
-    pmod : {a, b} (fin a, fin b) => [a] -> [1 + b] -> [b]
+    pdiv  : {a, b} (fin a, fin b) => [a] -> [b] -> [a]
+    pmod  : {a, b} (fin a, fin b) => [a] -> [1 + b] -> [b]
     pmult : {a, b} (fin a, fin b) => [a] -> [b] -> [max 1 (a + b) - 1]
 \end{Verbatim}
 \paragraph*{Sequences}
 \begin{Verbatim}
-    take : {front, back, elem} (fin front) 
-        => [front + back]elem -> [front]elem
-    drop : {front, back, elem} (fin front) 
-        => [front + back]elem -> [front]elem
-    tail : {a, b} [a+1]b -> [a]b
-    #    : {a, b, c} (fin a) => ([a]b,[c]b) -> [a+c]b
-    join : {parts, each, a} (fin each) 
-        => [parts][each]a -> [parts * each]a
+    take  : {front, back, elem} (fin front) 
+         => [front + back]elem -> [front]elem
+    drop  : {front, back, elem} (fin front) 
+         => [front + back]elem -> [front]elem
+    tail  : {a, b} [a+1]b -> [a]b
+    #     : {a, b, c} (fin a) => ([a]b,[c]b) -> [a+c]b
+    join  : {parts, each, a} (fin each) 
+         => [parts][each]a -> [parts * each]a
+    split : {parts, each, a} (fin a)
+         => [parts * each]a -> [parts][each]a
 
     groupBy : {each, parts, elem} (fin each) 
            => [parts * each]elem -> [parts][each]elem
-    splitBy : {parts, each, elem} 
-           => [parts * each]elem -> [parts][each]elem
     reverse : {a, b} (fin a) => [a]b -> [a]b
     @       : {a, b, c} ([a]b,[c]) -> b
     !       : {a, b, c} (fin a) => ([a]b,[c]) -> b

docs/ProgrammingCryptol/utils/Indexes.tex

@@ -126,7 +126,6 @@
 \newcommand{\indDrop}{\index{drop@\texttt{drop}}\xspace}
 \newcommand{\indJoin}{\index{join@\texttt{join}}\xspace}
 \newcommand{\indSplit}{\index{split@\texttt{split}}\xspace}
-\newcommand{\indSplitBy}{\index{splitBy@\texttt{splitBy}}\xspace}
 \newcommand{\indGroup}{\index{group@\texttt{group}}\xspace}
 \newcommand{\indTranspose}{\index{transpose@\texttt{transpose}}\xspace}
 \newcommand{\indTupleProj}{\index{project@\texttt{project}}\xspace}

examples/TripleDES.cry

@@ -25,7 +25,7 @@ PlainText = "The qufck brown fox jump"
 // Yes, that's the correct phrase.. (see the 7th letter of the phrase).
 // It's supposed to be "the quick..." but they made a mistake in transcribing
 // the ASCII into hex.
-[P1, P2, P3] = splitBy`{3} (join PlainText)
+[P1, P2, P3] = split`{3} (join PlainText)
 
 // B.1
 

lib/Cryptol.cry

@@ -321,10 +321,6 @@ width _ = `len
 undefined : {a} a
 undefined = error "undefined"
 
-splitBy : {parts,each,elem} (fin each) =>
-  [parts * each] elem -> [parts][each]elem
-splitBy = split
-
 groupBy : {each,parts,elem} (fin each) =>
   [parts * each] elem -> [parts][each]elem
 groupBy = split`{parts=parts}

tests/issues/issue148.icry.stdout

@@ -5,12 +5,12 @@ Loading module Main
   Defaulting type parameter 'bits'
              of literal or demoted expression
              at ./issue148.cry:4:34--4:35
-  to max 2 (width a`196)
+  to max 2 (width a`190)
 [warning] at ./issue148.cry:2:1--9:10:
   Defaulting 2nd type parameter
              of expression take
              at ./issue148.cry:6:10--6:14
-  to 16 * a`196
+  to 16 * a`190
 [warning] at <interactive>:1:1--1:36:
   Defaulting type parameter 'bits'
              of finite enumeration

tests/issues/issue198.icry.stdout

@@ -5,15 +5,15 @@ Loading module Main
   Defaulting type parameter 'bits'
              of literal or demoted expression
              at ./simon.cry2:87:34--87:35
-  to max 3 (width a`572)
+  to max 3 (width a`566)
 [warning] at ./simon.cry2:83:1--92:15:
   Defaulting type parameter 'bits'
              of literal or demoted expression
              at ./simon.cry2:90:29--90:31
-  to width a`574
+  to width a`568
 [warning] at ./simon.cry2:83:1--92:15:
   Defaulting type parameter 'bits'
              of literal or demoted expression
              at ./simon.cry2:89:36--89:38
-  to max 6 (max (width a`572) (width (a`573 - 1)))
+  to max 6 (max (width a`566) (width (a`567 - 1)))
 True

tests/issues/issue214.icry.stdout

@@ -5,9 +5,9 @@ Loading module Main
   Defaulting type parameter 'bits'
              of finite enumeration
              at ./issue214.cry:2:14--2:26
-  to max 2 (width (2 * a`196 - 2))
+  to max 2 (width (2 * a`190 - 2))
 [warning] at ./issue214.cry:2:1--2:49:
   Defaulting type parameter 'bits'
              of finite enumeration
              at ./issue214.cry:2:36--2:48
-  to max 2 (width (2 * a`196 - 1))
+  to max 2 (width (2 * a`190 - 1))

tests/issues/issue226.icry.stdout

@@ -76,8 +76,6 @@ Symbols
                                             each]a -> [parts][each]a
     splitAt : {front, back, a} (fin front) => [front +
                                                back]a -> ([front]a, [back]a)
-    splitBy : {parts, each, elem} (fin each) => [parts *
-                                                 each]elem -> [parts][each]elem
     tail : {a, b} [1 + a]b -> [a]b
     take : {front, back, elem} (fin front) => [front +
                                                back]elem -> [front]elem

tests/issues/issue290v2.icry.stdout

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

tests/mono-binds/test04.icry.stdout

@@ -25,8 +25,8 @@ Loading module test04
 [error] at ./test04.cry:3:19--3:21:
   Type mismatch:
     Expected type: ()
-    Inferred type: [?c8]
+    Inferred type: [?w7]
   where
-  ?c8 is type parameter 'bits'
+  ?w7 is type parameter 'bits'
          of literal or demoted expression
          at ./test04.cry:3:19--3:21