mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-28 09:23:04 +03:00
Generalize [a,b..c]
to work for types in class Literal
.
This commit is contained in:
parent
cbba44f692
commit
7424731e3f
@ -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.
|
||||
|
@ -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"]
|
||||
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user