Skip to content

Commit

Permalink
Remove redundant prelude functions not, extend, and extendSigned.
Browse files Browse the repository at this point in the history
These were recently moved here from Cryptol::Extras. They are duplicates
of existing functions `complement`, `zext`, and `sext`.

See #427.
  • Loading branch information
Brian Huffman committed May 24, 2018
1 parent 9601436 commit ab00098
Show file tree
Hide file tree
Showing 4 changed files with 3 additions and 27 deletions.
18 changes: 0 additions & 18 deletions lib/Cryptol.cry
Original file line number Diff line number Diff line change
Expand Up @@ -607,12 +607,6 @@ traceVal msg x = trace msg x x

/* Functions previously in Cryptol::Extras */

/**
* Logical negation
*/
not : {a} (Logic a) => a -> a
not a = ~ a

/**
* Conjunction of all bits in a sequence.
*/
Expand Down Expand Up @@ -681,18 +675,6 @@ scanr : {a,b,n} (fin n) => (a -> b -> b) -> b -> [n]a -> [n+1]b
scanr f acc xs = reverse ys
where ys = [acc] # [f x a | a <- ys | x <- reverse xs]

/**
* Zero extension
*/
extend : {total,n} (fin total, fin n, total >= n) => [n]Bit -> [total]Bit
extend n = zero # n

/**
* Signed extension. `extendSigned 0bwxyz : [8] == 0bwwwwwxyz`.
*/
extendSigned : {total,n} (fin total, fin n, n >= 1, total >= n+1) => [n]Bit -> [total]Bit
extendSigned xs = repeat (xs @ 0) # xs

/**
* Repeat a value.
*/
Expand Down
6 changes: 0 additions & 6 deletions tests/issues/issue226.icry.stdout
Original file line number Diff line number Diff line change
Expand Up @@ -62,11 +62,6 @@ Symbols
{front, back, elem} (fin front) => [front + back]elem -> [back]elem
elem : {n, a} (fin n, Cmp a) => a -> [n]a -> Bit
error : {at, len} (fin len) => [len][8] -> at
extend :
{total, n} (fin total, fin n, total >= n) => [n] -> [total]
extendSigned :
{total, n} (fin total, fin n, n >= 1, total >= 1 + n) =>
[n] -> [total]
False : Bit
foldl : {a, b, n} (fin n) => (a -> b -> a) -> a -> [n]b -> a
foldr : {a, b, n} (fin n) => (a -> b -> b) -> b -> [n]a -> b
Expand Down Expand Up @@ -103,7 +98,6 @@ Symbols
max : {a} (Cmp a) => a -> a -> a
min : {a} (Cmp a) => a -> a -> a
negate : {a} (Arith a) => a -> a
not : {a} (Logic a) => a -> a
or : {n} (fin n) => [n] -> Bit
pdiv : {a, b} (fin a, fin b) => [a] -> [b] -> [a]
pmod : {a, b} (fin a, fin b) => [a] -> [1 + b] -> [b]
Expand Down
2 changes: 1 addition & 1 deletion tests/issues/issue290v2.icry.stdout
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ Loading module Main

[error] at ./issue290v2.cry:2:1--2:19:
Unsolved constraints:
a`884 == 1
a`855 == 1
arising from
checking a pattern: type of 1st argument of Main::minMax
at ./issue290v2.cry:2:8--2:11
4 changes: 2 additions & 2 deletions tests/mono-binds/test04.icry.stdout
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,8 @@ Loading module test04
[error] at ./test04.cry:3:19--3:21:
Type mismatch:
Expected type: ()
Inferred type: [?o34]
Inferred type: [?l33]
where
?o34 is type parameter 'bits'
?l33 is type parameter 'bits'
of literal or demoted expression
at ./test04.cry:3:19--3:21

0 comments on commit ab00098

Please sign in to comment.