From 7424731e3f4d70c6238f083cbd93c1151e4f6b1d Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Fri, 15 Jun 2018 17:45:57 -0700
Subject: [PATCH] Generalize `[a,b..c]` to work for types in class `Literal`.

---
 lib/Cryptol.cry           |  8 ++++----
 src/Cryptol/Prims/Eval.hs | 13 +++++--------
 2 files changed, 9 insertions(+), 12 deletions(-)

diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry
index c9d911c4..eaba2d3f 100644
--- a/lib/Cryptol.cry
+++ b/lib/Cryptol.cry
@@ -485,10 +485,10 @@ primitive fromTo : {first, last, a} (fin last, last >= first, Literal last a) =>
  *
  * '[a,b..c]' is syntactic sugar for 'fromThenTo`{first=a,next=b,last=c}'.
  */
-primitive fromThenTo : {first, next, last, bits, len} (fin first, fin next,
-                        fin last, fin bits, bits >= width first,
-                        bits >= width next, bits >= width last,
-                        lengthFromThenTo first next last == len) => [len][bits]
+primitive fromThenTo : {first, next, last, a, len}
+                       ( fin first, fin next, fin last
+                       , Literal first a, Literal next a, Literal last a
+                       , lengthFromThenTo first next last == len) => [len]a
 
 /**
  * An infinite sequence counting up from the given starting value.
diff --git a/src/Cryptol/Prims/Eval.hs b/src/Cryptol/Prims/Eval.hs
index 0127a195..adb8d46f 100644
--- a/src/Cryptol/Prims/Eval.hs
+++ b/src/Cryptol/Prims/Eval.hs
@@ -1414,16 +1414,13 @@ fromThenToV  =
   nlam $ \ first ->
   nlam $ \ next  ->
   nlam $ \ lst   ->
-  nlam $ \ bits  ->
+  tlam $ \ ty    ->
   nlam $ \ len   ->
-    case (first, next, lst, len, bits) of
-      (_         , _        , _       , _       , Nat bits')
-        | bits' >= Arch.maxBigIntWidth -> wordTooWide bits'
-      (Nat first', Nat next', Nat _lst', Nat len', Nat bits') ->
+    let !f = mkLit ty in
+    case (first, next, lst, len) of
+      (Nat first', Nat next', Nat _lst', Nat len') ->
         let diff = next' - first'
-         in VSeq len' $ IndexSeqMap $ \i ->
-               ready $ VWord bits' $ return $
-                 WordVal $ wordLit bits' (first' + i*diff)
+        in VSeq len' $ IndexSeqMap $ \i -> ready $ f (first' + i*diff)
       _ -> evalPanic "fromThenToV" ["invalid arguments"]