Update reference implementation and documentation

docs/CryptolPrims.md

@@ -20,6 +20,7 @@ a member of `Ring` and `Zero`.
 Literals
 -----------------------
     type Literal : # -> * -> Prop
+    type LiteralLessThan : # -> * -> Prop
 
     number : {val, rep} Literal val rep => rep
     length : {n, a, b} (fin n, Literal n b) => [n]a -> b
@@ -38,6 +39,11 @@ Literals
                    , lengthFromThenTo first next last == len) =>
                   [len]a
 
+    // '[a .. < b]` is syntactic sugar for 'fromToLessThan`{first=a,bound=b}'
+    fromToLessThan : {first, bound, a}
+         (fin first, bound >= first, LiteralLessThan bound a) =>
+         [bound - first]a
+
 Fractional Literals
 -------------------
 
@@ -48,7 +54,7 @@ or report an error if the number can't be represented exactly.
     type FLiteral : # -> # -> # -> * -> Prop
 
 
-Fractional literals are desugared into calles to the primitive `fraction`:
+Fractional literals are desugared into calls to the primitive `fraction`:
 
     fraction : { m, n, r, a } FLiteral m n r a => a
 
@@ -274,7 +280,7 @@ Sequences
     updates    : {n,k,ix,a} (Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a
     updatesEnd : {n,k,ix,d} (fin n, Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a
 
-    take       : {front,back,elem} (fin front) => [front + back]elem -> [front]elem
+    take       : {front,back,elem} [front + back]elem -> [front]elem
     drop       : {front,back,elem} (fin front) => [front + back]elem -> [back]elem
     head       : {a, b} [1 + a]b -> b
     tail       : {a, b} [1 + a]b -> [a]b
@@ -282,7 +288,7 @@ Sequences
 
     // Declarations of the form 'x @ i = e' are syntactic
     // sugar for 'x = generate (\i -> e)'.
-    generate   : {n, a} (fin n, n >= 1) => (Integer -> a) -> [n]a
+    generate : {n, a, ix} (Integral ix, LiteralLessThan n ix) => (ix -> a) -> [n]a
 
     groupBy    : {each,parts,elem} (fin each) => [parts * each]elem -> [parts][each]elem
 

docs/ProgrammingCryptol/crashCourse/CrashCourse.tex

@@ -790,7 +790,7 @@ Here are Cryptol's responses:
   []
   invalid sequence index: 12
    -- Backtrace --
-  (Cryptol::@) called at Cryptol:822:14--822:20
+  (Cryptol::@) called at Cryptol:820:14--820:20
   (Cryptol::@@) called at <interactive>:9:1--9:28
   [9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
   9
@@ -2109,12 +2109,13 @@ the Cryptol primitive {\tt take}\indTake:
 \restartrepl
 \begin{replPrompt}
   Cryptol> :t take
-  take : {front, back, a} (fin front) => [front + back]a -> [front]a
+  take : {front, back, a} [front + back]a -> [front]a
 \end{replPrompt}
 
 The type of {\tt take} says that it is parameterized over {\tt front}
-and {\tt back}, {\tt front} must be a finite value,\indFin it takes a
+and {\tt back} and a type {\tt a}, it takes a sequence
-sequence {\tt front + back} long, and returns a sequence {\tt front} long.
+{\tt front + back} long of elements of type {\tt a}, and returns a
+sequence {\tt front} long.
 
 The impact of this predicate shows up when we try to take more than
 what is available:

src/Cryptol/Eval/Reference.lhs

@@ -566,7 +566,7 @@ by corresponding type classes:
 
 * Indexing: `@`, `@@`, `!`, `!!`, `update`, `updateEnd`
 
-* Enumerations: `fromTo`, `fromThenTo`, `infFrom`, `infFromThen`
+* Enumerations: `fromTo`, `fromThenTo`, `fromToLessThan`, `infFrom`, `infFromThen`
 
 * Polynomials: `pmult`, `pdiv`, `pmod`
 
@@ -795,6 +795,17 @@ by corresponding type classes:
 >                     in pure (VList (Nat len)
 >                               (map f (genericTake len [first, next ..])))
 >
+>   , "fromToLessThan" ~>
+>                     vFinPoly $ \first -> pure $
+>                     VNumPoly $ \bound -> pure $
+>                     VPoly    $ \ty    ->
+>                     let f i = literal i ty in
+>                     case bound of
+>                       Inf -> pure (VList Inf (map f [first ..]))
+>                       Nat bound' ->
+>                         let len = bound' - first in
+>                         pure (VList (Nat len) (map f (genericTake len [first ..])))
+>
 >   , "infFrom"    ~> VPoly $ \ty -> pure $
 >                     VFun $ \first ->
 >                     do x <- cryToInteger ty first