diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index 84a0aebb..21397516 100644 --- a/lib/Cryptol.cry +++ b/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. */ diff --git a/lib/Cryptol/Extras.cry b/lib/Cryptol/Extras.cry index 9541a5ae..2dfc3d63 100644 --- a/lib/Cryptol/Extras.cry +++ b/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 */ diff --git a/tests/issues/issue214.icry b/tests/issues/issue214.icry index 8af11a1f..5484c63d 100644 --- a/tests/issues/issue214.icry +++ b/tests/issues/issue214.icry @@ -1 +1,2 @@ +:set warnDefaulting = off :l issue214.cry diff --git a/tests/issues/issue214.icry.stdout b/tests/issues/issue214.icry.stdout index ee024cfb..57a1d7a1 100644 --- a/tests/issues/issue214.icry.stdout +++ b/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)) diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout index c0448b5e..66d34715 100644 --- a/tests/issues/issue226.icry.stdout +++ b/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 diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout index 6def7b33..5f01b85a 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 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