GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-24 06:52:44 +03:00
Code Issues Projects Releases Wiki Activity

Remove unused primitive fromThen.

Browse Source
This commit is contained in:
Brian Huffman 2019-02-27 16:57:00 -08:00
parent 61a17adb02
commit 24fb6c9511
10 changed files with 16 additions and 83 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
bench/data/PreludeWithExtras.cry
View File

@ -260,11 +260,6 @@ primitive (!) : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b
*/
primitive (!!) : {a, b, c, d} (fin a, fin d) => [a]b -> [c][d] -> [c]b
primitive fromThen : {first, next, bits, len}
( fin first, fin next, fin bits
, bits >= width first, bits >= width next
, lengthFromThen first next bits == len) => [len][bits]
primitive fromTo : {first, last, bits} (fin last, fin bits, last >= first,
bits >= width last) => [1 + (last - first)][bits]

5
docs/ProgrammingCryptol/prims/Primitives.tex
View File

@ -117,11 +117,6 @@ primsPlaceHolder=1;
% (/$) : {a} (Arith a) => a -> a -> a
% number : {val, rep} (Literal val rep) => rep
% elem : {n, a} (fin n, Cmp a) => a -> [n]a -> Bit
% fromThen :
% {first, next, bits, len} (fin first, fin next, fin bits,
% bits >= width first, bits >= width next, first != next,
% lengthFromThen first next bits == len) =>
% [len][bits]
% fromThenTo :
% {first, next, last, a, len} (fin first, fin next, fin last,
% Literal first a, Literal next a, Literal last a, first != next,

13
lib/Cryptol.cry
View File

@ -452,19 +452,6 @@ updatesEnd xs0 idxs vals = xss!0
| b <- vals
]
/**
* A finite arithmetic sequence starting with 'first' and 'next',
* stopping when the values would wrap around modulo '2^^bits'.
*
* '[a,b..]' is syntactic sugar for 'fromThen`{first=a,next=b}'.
* '[a..]' is syntactic sugar for 'fromThen`{first=a,next=a+1}'.
*/
primitive fromThen : {first, next, bits, len}
( fin first, fin next, fin bits
, bits >= width first, bits >= width next
, first != next
, lengthFromThen first next bits == len) => [len][bits]
/**
* A finite sequence counting up from 'first' to 'last'.
*

27
src/Cryptol/Eval/Reference.lhs
View File

@ -543,7 +543,7 @@ Cryptol primitives fall into several groups:
* Indexing: `@`, `@@`, `!`, `!!`, `update`, `updateEnd`
* Enumerations: `fromThen`, `fromTo`, `fromThenTo`, `infFrom`, `infFromThen`
* Enumerations: `fromTo`, `fromThenTo`, `infFrom`, `infFromThen`
* Polynomials: `pmult`, `pdiv`, `pmod`
@ -648,13 +648,6 @@ Cryptol primitives fall into several groups:
> , ("updateEnd" , updatePrim updateBack)
>
> -- Enumerations:
> , ("fromThen" , vFinPoly $ \first ->
> vFinPoly $ \next ->
> vFinPoly $ \bits ->
> vFinPoly $ \len ->
> VList (Nat len)
> (map (vWordValue bits) (genericTake len [first, next ..])))
>
> , ("fromTo" , vFinPoly $ \first ->
> vFinPoly $ \lst ->
> VPoly $ \ty ->
@ -732,21 +725,11 @@ error if any of the input bits contain an evaluation error.
> signedBitsToInteger (b0 : bs) = foldl f (if b0 then -1 else 0) bs
> where f x b = if b then 2 * x + 1 else 2 * x
Functions `vWord` and `vWordValue` convert from integers back to the
big-endian bitvector representation. If an integer-producing function
raises a run-time exception, then the output bitvector will contain
the exception in all bit positions.
Function `vWord` converts an integer back to the big-endian bitvector
representation. If an integer-producing function raises a run-time
exception, then the output bitvector will contain the exception in all
bit positions.
> -- | Convert an integer to big-endian binary value of the specified width.
> vWordValue :: Integer -> Integer -> Value
> vWordValue w x = VList (Nat w) (map (VBit . Right) (integerToBits w x))
>
> -- | Convert an integer to a big-endian format of the specified width.
> integerToBits :: Integer -> Integer -> [Bool]
> integerToBits w x = go [] w x
> where go bs 0 _ = bs
> go bs n a = go (odd a : bs) (n - 1) $! (a `div` 2)
>
> vWord :: Integer -> Either EvalError Integer -> Value
> vWord w e = VList (Nat w) [ VBit (fmap (test i) e) | i <- [w-1, w-2 .. 0] ]
> where test i x = testBit x (fromInteger i)

20
src/Cryptol/Prims/Eval.hs
View File

@ -172,8 +172,6 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
lam $ \ x ->
splitAtV front back a =<< x)
, ("fromThen" , {-# SCC "Prelude::fromThen" #-}
fromThenV)
, ("fromTo" , {-# SCC "Prelude::fromTo" #-}
fromToV)
, ("fromThenTo" , {-# SCC "Prelude::fromThenTo" #-}
@ -1406,24 +1404,6 @@ updatePrim updateWord updateSeq =
VStream vs -> VStream <$> updateSeq len eltTy vs idx' val
_ -> evalPanic "Expected sequence value" ["updatePrim"]
-- @[ 0, 1 .. ]@
fromThenV :: BitWord b w i
=> GenValue b w i
fromThenV =
nlam $ \ first ->
nlam $ \ next ->
nlam $ \ bits ->
nlam $ \ len ->
case (first, next, len, bits) of
(_ , _ , _ , Nat bits')
| bits' >= Arch.maxBigIntWidth -> wordTooWide bits'
(Nat first', Nat next', Nat len', Nat bits') ->
let diff = next' - first'
in VSeq len' $ IndexSeqMap $ \i ->
ready $ VWord bits' $ return $
WordVal $ wordLit bits' (first' + i*diff)
_ -> evalPanic "fromThenV" ["invalid arguments"]
-- @[ 0 .. 10 ]@
fromToV :: BitWord b w i
=> GenValue b w i

3
src/Cryptol/Symbolic/Prims.hs
View File

@ -35,7 +35,7 @@ import Cryptol.Prims.Eval (binary, unary, arithUnary,
logicBinary, logicUnary, zeroV,
ccatV, splitAtV, joinV, ecSplitV,
reverseV, infFromV, infFromThenV,
fromThenV, fromToV, fromThenToV,
fromToV, fromThenToV,
transposeV, indexPrim,
ecToIntegerV, ecFromIntegerV,
ecNumberV, updatePrim, randomV, liftWord,
@ -183,7 +183,6 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
tlam $ \c ->
lam $ \xs -> transposeV a b c =<< xs)
, ("fromThen" , fromThenV)
, ("fromTo" , fromToV)
, ("fromThenTo" , fromThenToV)
, ("infFrom" , infFromV)

1
src/Cryptol/TypeCheck/InferTypes.hs
View File

@ -296,7 +296,6 @@ ppUse expr =
| identText prim == "number" -> "literal or demoted expression"
| identText prim == "infFrom" -> "infinite enumeration"
| identText prim == "infFromThen" -> "infinite enumeration (with step)"
| identText prim == "fromThen" -> "finite enumeration"
| identText prim == "fromTo" -> "finite enumeration"
| identText prim == "fromThenTo" -> "finite enumeration"
_ -> "expression" <+> pp expr

16
tests/issues/T146.icry.stdout
View File

@ -3,14 +3,14 @@ Loading module Cryptol
Loading module Main
[error] at ./T146.cry:1:18--6:10:
The type ?fv`864 is not sufficiently polymorphic.
It cannot depend on quantified variables: fv`848
The type ?fv`860 is not sufficiently polymorphic.
It cannot depend on quantified variables: fv`844
where
?fv`864 is type argument 'fv' of 'Main::ec_v1' at ./T146.cry:4:19--4:24
fv`848 is signature variable 'fv' at ./T146.cry:11:10--11:12
?fv`860 is type argument 'fv' of 'Main::ec_v1' at ./T146.cry:4:19--4:24
fv`844 is signature variable 'fv' at ./T146.cry:11:10--11:12
[error] at ./T146.cry:5:19--5:24:
The type ?fv`866 is not sufficiently polymorphic.
It cannot depend on quantified variables: fv`848
The type ?fv`862 is not sufficiently polymorphic.
It cannot depend on quantified variables: fv`844
where
?fv`866 is type argument 'fv' of 'Main::ec_v2' at ./T146.cry:5:19--5:24
fv`848 is signature variable 'fv' at ./T146.cry:11:10--11:12
?fv`862 is type argument 'fv' of 'Main::ec_v2' at ./T146.cry:5:19--5:24
fv`844 is signature variable 'fv' at ./T146.cry:11:10--11:12

5
tests/issues/issue226.icry.stdout
View File

@ -65,11 +65,6 @@ Symbols
foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b
foo : {a} a -> a
fromInteger : {a} (Arith a) => Integer -> a
fromThen :
{first, next, bits, len} (fin first, fin next, fin bits,
bits >= width first, bits >= width next, first != next,
lengthFromThen first next bits == len) =>
[len][bits]
fromThenTo :
{first, next, last, a, len} (fin first, fin next, fin last,
Literal first a, Literal next a, Literal last a, first != next,

4
tests/issues/issue290v2.icry.stdout
View File

@ -4,9 +4,9 @@ Loading module Main
[error] at ./issue290v2.cry:2:1--2:19:
Unsolved constraints:
• n`845 == 1
• n`841 == 1
arising from
checking a pattern: type of 1st argument of Main::minMax
at ./issue290v2.cry:2:8--2:11
where
n`845 is signature variable 'n' at ./issue290v2.cry:1:11--1:12
n`841 is signature variable 'n' at ./issue290v2.cry:1:11--1:12