ExpandCollapse

+ 1 Boolean Logic

share/lib/std/scalar/bool.flx

  typedef bool = 2;
  
  Standard operations on boolean type.
  open class Bool
  {
    Short cut and via closure
    noinline fun andthen (x: bool, y:1->bool) : bool => 
      if x then #y else false
    ;
   
    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);
  }
  
  instance FloatAddgrp[2] {
    fun zero () => 0 :>> 2;
    fun - (x:2) => (sub (2, caseno x)) :>> 2;
    fun + (x:2, y:2) : 2 => (add ((caseno x , caseno y)) % 2) :>> 2;
    fun - (x:2, y:2) : 2 => (add (2, sub(caseno x , caseno y)) % 2) :>> 2;
  }
  
  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];
  open Addgrp[bool];
  

+ 2 Syntax

share/lib/std/scalar/boolexpr.fsyn

syntax boolexpr
{
  //$ Boolean false.
  satom := "false" =># "'(ast_typed_case  0 2)";

  //$ Boolean true.
  satom := "true" =># "'(ast_typed_case  1 2)";

  //$ Logical implication.
  x[simplies_condition_pri] := x[>simplies_condition_pri] "implies" x[>simplies_condition_pri] =># "(Infix)";

  //$ Logical disjunction (or).
  x[sor_condition_pri] := x[>sor_condition_pri] ( "or" x[>sor_condition_pri])+ =># "(chain 'ast_orlist _1 _2)" note "lor";

  //$ Logical conjunction (and).
  x[sand_condition_pri] := x[>sand_condition_pri] ( "and" x[>sand_condition_pri])+ =># "(chain 'ast_andlist _1 _2)" note "land";

  //$ Logical negation (not).
  x[snot_condition_pri] := "not" x[snot_condition_pri]  =># "`(ast_not ,_sr ,_2)";

  x[scomparison_pri]:= x[>scomparison_pri] "\not" cmp x[>scomparison_pri] =># "`(ast_not ,_sr (ast_apply ,_sr (,_3 (,_1 ,_4))))";

  // tex logic operators
  x[stex_implies_condition_pri] := x[>stex_implies_condition_pri]  "\implies" x[>stex_implies_condition_pri] =># "(infix 'implies)";
  x[stex_or_condition_pri] := x[>stex_or_condition_pri] ( "\lor" x[>stex_or_condition_pri])+ =># "(chain 'ast_orlist _1 _2)" note "lor";
  x[stex_and_condition_pri] := x[>stex_and_condition_pri] ( "\land" x[>stex_and_condition_pri])+ =># "(chain 'ast_andlist _1 _2)" note "land";
  x[stex_not_condition_pri] := "\lnot" x[stex_not_condition_pri]  =># "`(ast_not ,_sr ,_2)";


  bin := "\iff" =># '(nos _1)'; // NOT IMPLEMENTED FIXME
  bin := "\impliedby" =># '(nos _1)'; // NOT IMPLEMENTED FIXME

  //$ Conditional expression.
  satom := sconditional "endif" =># "_1";

  //$ Conditional expression (prefix).
  sconditional := "if" sexpr "then" sexpr selse_part =>#
      "`(ast_cond ,_sr (,_2 ,_4 ,_5))";

      selif := "elif" sexpr "then" sexpr =># "`(,_2 ,_4)";

      selifs := selif =># "`(,_1)";
      selifs := selifs selif =># "(cons _2 _1)";

      selse_part:= "else" sexpr =># "_2";
      selse_part:= selifs "else" sexpr =>#
          """
            (let ((f (lambda (result condthn)
              (let ((cond (first condthn)) (thn (second condthn)))
                `(ast_cond ,_sr (,cond ,thn ,result))))))
            (fold_left f _3 _1))
          """;
}

+ 3 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)
     ;
  
  }