Add the short-cutting boolean operators (/\), (\/), and (==>)

to the Cryptol prelude.  This is in service of eventually addressing
issue #241.

lib/Cryptol.cry

@@ -10,8 +10,11 @@ module Cryptol where
  */
 primitive demote : {val, bits} (fin val, fin bits, bits >= width val) => [bits]
 
-infixr 10 ||
-infixr 20 &&
+infixr  5 ==>
+infixr 10 \/
+infixr 15 /\
+infixr 20 ||
+infixr 25 &&
 infix  30 ==, ===, !=, !==
 infix  40 >, >=, <, <=
 infixl 50 ^
@@ -99,7 +102,7 @@ primitive negate : {a} (Arith a) => a -> a
 primitive complement : {a} a -> a
 
 /**
- * Operator form of binary complement.
+ * Operator form of 'complement'.
  */
 (~) : {a} a -> a
 (~) = complement
@@ -158,6 +161,30 @@ min x y = if x < y then x else y
 max : {a} (Cmp a) => a -> a -> a
 max x y = if x > y then x else y
 
+/**
+ * Short-cutting boolean conjuction function.
+ * If the first argument is False, the second argument
+ * is not evaluated.
+ */
+(/\) : Bit -> Bit -> Bit
+x /\ y = if x then y else False
+
+/**
+ * Short-cutting boolean disjuction function.
+ * If the first argument is True, the second argument
+ * is not evaluated.
+ */
+(\/) : Bit -> Bit -> Bit
+x \/ y = if x then True else y
+
+/**
+ * Short-cutting logical implication.
+ * If the first argument is False, the second argument is
+ * not evaluated.
+ */
+(==>) : Bit -> Bit -> Bit
+a ==> b = if a then b else True
+
 /**
  * Logical `and' over bits. Extends element-wise over sequences, tuples.
  */

lib/Cryptol/Extras.cry

@@ -9,14 +9,6 @@
 
 module Cryptol::Extras where
 
-infixr 5 ==>
-
-/**
- * Logical implication
- */
-(==>) : Bit -> Bit -> Bit
-a ==> b = if a then b else True
-
 /**
  * Logical negation
  */

tests/issues/issue214.icry

@@ -1 +1,2 @@
+:set warnDefaulting = off
 :l issue214.cry

tests/issues/issue214.icry.stdout

@@ -1,13 +1,3 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
-[warning] at ./issue214.cry:2:1--2:49:
-  Defaulting type parameter 'bits'
-             of finite enumeration
-             at ./issue214.cry:2:14--2:26
-  to max 2 (width (2 * a`297 - 2))
-[warning] at ./issue214.cry:2:1--2:49:
-  Defaulting type parameter 'bits'
-             of finite enumeration
-             at ./issue214.cry:2:36--2:48
-  to max 2 (width (2 * a`297 - 1))

tests/issues/issue226.icry.stdout

@@ -24,12 +24,14 @@ Symbols
     (+) : {a} (Arith a) => a -> a -> a
     (-) : {a} (Arith a) => a -> a -> a
     (/) : {a} (Arith a) => a -> a -> a
+    (/\) : Bit -> Bit -> Bit
     (<) : {a} (Cmp a) => a -> a -> Bit
     (<<) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
     (<<<) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
     (<=) : {a} (Cmp a) => a -> a -> Bit
     (==) : {a} (Cmp a) => a -> a -> Bit
     (===) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
+    (==>) : Bit -> Bit -> Bit
     (>) : {a} (Cmp a) => a -> a -> Bit
     (>=) : {a} (Cmp a) => a -> a -> Bit
     (>>) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
@@ -38,6 +40,7 @@ Symbols
     (@@) : {a, b, c, d} (fin d) => [a]b -> [c][d] -> [c]b
     False : Bit
     True : Bit
+    (\/) : Bit -> Bit -> Bit
     (^) : {a} a -> a -> a
     (^^) : {a} (Arith a) => a -> a -> a
     complement : {a} a -> a

tests/issues/issue290v2.icry.stdout

@@ -4,7 +4,7 @@ Loading module Main
 
 [error] at ./issue290v2.cry:2:1--2:19:
   Unsolved constraint:
-    a`297 == 1
+    a`303 == 1
       arising from
       checking a pattern: type of 1st argument of Main::minMax
       at ./issue290v2.cry:2:8--2:11