From 24fb6c9511ff140b3096de4baf202ba2e2358fc3 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 27 Feb 2019 16:57:00 -0800 Subject: [PATCH] Remove unused primitive `fromThen`. --- bench/data/PreludeWithExtras.cry | 5 ---- docs/ProgrammingCryptol/prims/Primitives.tex | 5 ---- lib/Cryptol.cry | 13 ---------- src/Cryptol/Eval/Reference.lhs | 27 ++++---------------- src/Cryptol/Prims/Eval.hs | 20 --------------- src/Cryptol/Symbolic/Prims.hs | 3 +-- src/Cryptol/TypeCheck/InferTypes.hs | 1 - tests/issues/T146.icry.stdout | 16 ++++++------ tests/issues/issue226.icry.stdout | 5 ---- tests/issues/issue290v2.icry.stdout | 4 +-- 10 files changed, 16 insertions(+), 83 deletions(-) diff --git a/bench/data/PreludeWithExtras.cry b/bench/data/PreludeWithExtras.cry index 0f9bdf48..55888371 100644 --- a/bench/data/PreludeWithExtras.cry +++ b/bench/data/PreludeWithExtras.cry @@ -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] diff --git a/docs/ProgrammingCryptol/prims/Primitives.tex b/docs/ProgrammingCryptol/prims/Primitives.tex index b4a2c820..93776606 100644 --- a/docs/ProgrammingCryptol/prims/Primitives.tex +++ b/docs/ProgrammingCryptol/prims/Primitives.tex @@ -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, diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index 83455650..b4ab5ce6 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -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'. * diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs index 29fcd77b..9af3e2b2 100644 --- a/src/Cryptol/Eval/Reference.lhs +++ b/src/Cryptol/Eval/Reference.lhs @@ -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) diff --git a/src/Cryptol/Prims/Eval.hs b/src/Cryptol/Prims/Eval.hs index 214906f2..7d535942 100644 --- a/src/Cryptol/Prims/Eval.hs +++ b/src/Cryptol/Prims/Eval.hs @@ -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 diff --git a/src/Cryptol/Symbolic/Prims.hs b/src/Cryptol/Symbolic/Prims.hs index ebb5da0e..645867a2 100644 --- a/src/Cryptol/Symbolic/Prims.hs +++ b/src/Cryptol/Symbolic/Prims.hs @@ -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) diff --git a/src/Cryptol/TypeCheck/InferTypes.hs b/src/Cryptol/TypeCheck/InferTypes.hs index 8075ca6f..314f122d 100644 --- a/src/Cryptol/TypeCheck/InferTypes.hs +++ b/src/Cryptol/TypeCheck/InferTypes.hs @@ -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 diff --git a/tests/issues/T146.icry.stdout b/tests/issues/T146.icry.stdout index 428f5da5..67590be8 100644 --- a/tests/issues/T146.icry.stdout +++ b/tests/issues/T146.icry.stdout @@ -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 diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout index 6c8bb3b8..fd25d262 100644 --- a/tests/issues/issue226.icry.stdout +++ b/tests/issues/issue226.icry.stdout @@ -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, diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout index f6b1c3ae..8f2c5281 100644 --- a/tests/issues/issue290v2.icry.stdout +++ b/tests/issues/issue290v2.icry.stdout @@ -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