# 1 Boolean Logic

We have two kinds of boolean, cbool is the binding to C/C++ bool type which is usually a single byte.

The other kind, bool, is a synonym for type 2, which is a compact linear type and will use a a 64 bit word.

We provide the same operations on both, since as values they're compatible. However the Felix bool is the standard type.

Pointers to these two types are not compatible. Although a sole bool is much bigger than a cbool, 64 bools can fit in a single machine word, as opposed to only 8 cbools.

`share/lib/std/scalar/bool.flx`

```  typedef bool = 2;
type cbool = "bool" requires index TYPE_cbool;

open class Bool
{
ctor bool:cbool="\$1";

Short cut and via closure
noinline fun andthen (x: bool, y:1->bool) : bool =>
if x then #y else false
;

Short cut and via closure
noinline fun orelse (x: bool, y:1->bool) : bool =>
if x then true else #y
;

Disjunction: logical and.
fun land: bool * bool -> bool = "\$1&&\$2";      // x and y

Negated and.
fun nand: bool * bool -> bool = "!(\$1&&\$2)";   // not (x and y)

Conjunction: logical or.
fun lor: bool * bool -> bool = "\$1||\$2";       // x or y

Negated or.
fun nor: bool * bool -> bool = "!(\$1||\$2)";    // not (x or y)

Logical exclusive or.
fun xor: bool * bool -> bool = "\$1!=\$2";       // (x or y) and not (x and y)

Logical negation.
fun lnot: bool -> bool = "!\$1";                // not x

Logical implication.
fun implies: bool * bool -> bool = "!\$1||\$2";  // not x or y

Mutating or.
proc |= : &bool * bool = "*\$1|=\$2;";

Mutating and.
proc &= : &bool * bool = "*\$1&=\$2;";

// Elide double negations.
//reduce dneg(x:bool): lnot (lnot x) => x;
// Elide double negations.
//reduce dneg(x:bool,y:bool): lnot (nand(x,y)) => land(x,y);
// Elide double negations.
//reduce dneg(x:bool,y:bool): lnot (nor(x,y)) => lor(x,y);
}

Standard operations on cboolean type.
open class CBool
{
ctor cbool:bool="\$1";
const cfalse: cbool="false";
const ctrue: cbool="true";

Short cut and via closure
noinline fun andthen (x: cbool, y:1->cbool) : cbool =>
if x then #y else cfalse
;

Short cut and via closure
noinline fun orelse (x: cbool, y:1->cbool) : cbool =>
if x then ctrue else #y
;

Disjunction: logical and.
fun land: cbool * cbool -> cbool = "\$1&&\$2";      // x and y

Negated and.
fun nand: cbool * cbool -> cbool = "!(\$1&&\$2)";   // not (x and y)

Conjunction: logical or.
fun lor: cbool * cbool -> cbool = "\$1||\$2";       // x or y

Negated or.
fun nor: cbool * cbool -> cbool = "!(\$1||\$2)";    // not (x or y)

Logical exclusive or.
fun xor: cbool * cbool -> cbool = "\$1!=\$2";       // (x or y) and not (x and y)

Logical negation.
fun lnot: cbool -> cbool = "!\$1";                // not x

Logical implication.
fun implies: cbool * cbool -> cbool = "!\$1||\$2";  // not x or y

Mutating or.
proc |= : &cbool * cbool = "*\$1|=\$2;";

Mutating and.
proc &= : &cbool * cbool = "*\$1&=\$2;";

// Elide double negations.
//reduce dneg(x:cbool): lnot (lnot x) => x;
// Elide double negations.
//reduce dneg(x:cbool,y:cbool): lnot (nand(x,y)) => land(x,y);
// Elide double negations.
//reduce dneg(x:cbool,y:cbool): lnot (nor(x,y)) => lor(x,y);
}

fun zero () => 0 :>> bool;
fun - (x:bool) => (sub (2, caseno x)) :>> bool;
fun + (x:bool, y:bool) : bool => (add ((caseno x , caseno y)) % 2) :>> bool;
fun - (x:bool, y:bool) : bool => (add (2, sub(caseno x , caseno y)) % 2) :>> bool;
}

instance Str[bool] {
Convert bool to string.
fun str (b:bool) : string => if b then "true" else "false" endif;
}

instance Tord[bool] {
Total ordering of bools, false < true.
Note that x < y is equivalent to x implies y.
fun < : bool * bool -> bool = "\$1<\$2";
}

open Tord[bool];
open Show[bool];

instance Str[cbool] {
Convert cbool to string.
fun str (b:cbool) : string => if b then "ctrue" else "cfalse" endif;
}

instance Tord[cbool] {
Total ordering of cbools, false < true.
Note that x < y is equivalent to x implies y.
fun < : cbool * cbool -> cbool = "\$1<\$2";
}

open Tord[cbool];
open Show[cbool];

```

# 2 Predicate combinators.

A predicate is any function returning a boolean argument. Predicates are also relations by simply providing a tuple argument.

This is a simple class allowing predicates to be combined directly using symbolic operators to form new predicates, using logical conjunction `and`, disjunction `or`, implication `implies` and negation `not`. The parser maps these operator onto the functions `land`, `lor`, `implies`, and `lnot` respectively.

`share/lib/std/algebra/predicate.flx`

```
// Some operations on predicates.
// These also automatically apply to relations, but just taking
// the argument as a tuple.

open class Predicate[T]
{
fun land (f:T->bool,g:T->bool) =>
fun (x:T) => f x and g x
;

fun lor (f:T->bool,g:T->bool) =>
fun (x:T) => f x or g x
;

fun implies (f:T->bool,g:T->bool) =>
fun (x:T) => f x implies g x
;

fun lnot (f:T->bool) =>
fun (x:T) => not (f x)
;

}

```