From ab000984d2701c629c358a3a46761c014fff1b2e Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Thu, 24 May 2018 14:41:09 -0700
Subject: [PATCH] Remove redundant prelude functions `not`, `extend`, and
 `extendSigned`.

These were recently moved here from Cryptol::Extras. They are duplicates
of existing functions `complement`, `zext`, and `sext`.

See #427.
---
 lib/Cryptol.cry                     | 18 ------------------
 tests/issues/issue226.icry.stdout   |  6 ------
 tests/issues/issue290v2.icry.stdout |  2 +-
 tests/mono-binds/test04.icry.stdout |  4 ++--
 4 files changed, 3 insertions(+), 27 deletions(-)

diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry
index 1a025119..bb709e5b 100644
--- a/lib/Cryptol.cry
+++ b/lib/Cryptol.cry
@@ -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.
  */
@@ -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.
  */
diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout
index 5cd0f5e9..fb9e9475 100644
--- a/tests/issues/issue226.icry.stdout
+++ b/tests/issues/issue226.icry.stdout
@@ -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
@@ -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]
diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout
index 94f818f5..8c8ac4ce 100644
--- a/tests/issues/issue290v2.icry.stdout
+++ b/tests/issues/issue290v2.icry.stdout
@@ -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
diff --git a/tests/mono-binds/test04.icry.stdout b/tests/mono-binds/test04.icry.stdout
index b9893538..6689ffbf 100644
--- a/tests/mono-binds/test04.icry.stdout
+++ b/tests/mono-binds/test04.icry.stdout
@@ -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