#{
  Paulson's examples in new style
#}

# Sec 1.2

GCD Int Int of Int;
GCD m n == n if m = 0 | GCD (n `Mod` m) m;

# Sec 1.4

Length (List a) of a;
Length . == 0;
Length (x:xs) == 1 + Length xs;

# Sec 2.1

2 + 2;

3.2 - 2.3;

Sqrt 2.0;

seconds := 60;

minutes := 60;

hours := 24;

seconds * minutes * hours;

it `Div` 24;

secsinhour := it;

secs_in_hour := seconds * minutes;

Pi of Float;
Pi == 3.14159;

r := 2.0;

area := Pi * r * r;

# Sec 2.2

Area Float of Float;
Area r == Pi * r * r;

Area 2.0;

# Sec 2.3

!?!?! of Int;
!?!?! == 1415;

# Sec 2.4

0;
-23;

(((m*n)*k) - (m `Div` j)) + j;
m * n * k - (m `Div` j) + j; # means the same

# It is an error to try to redefine any name that is parseable as a number
Float `E` Float of Float;
Inf of Float;
NaN Int of Float;
0.01;
2.718281828;
-1.2`E`12; # Scientific notation
7`E`-5;
100_000;
100_000.05;
3.141_592_653;
.0;
0.;

# Sec 2.5

"How now! a rat? Dead, for a ducat, dead!";

String @ String of String;
"Fair " @ "Ophelia";

Length String of Int;
Length it;

Title String of String;
Title name == "The Duke of " @ name;

Title "York";

"This above all:\nto thine own self be true\n";
"Continue this string\
  \past a line break";

'a';
'\n';

Chr Int of Char;
Ord Char of Int;

Digit Int of String;
Digit i == Chr (i + Ord '0');

String `Sub` Int of Char;

Digit Int of String;
Digit i == "0123456789" `Sub` i;

Str Char of String;

Str (Digit 5);

# Sec 2.6

Sign Int of Int;
Sign n == 1 if n > 0
        | 0 if n = 0
        | -1; # if n < 0

IsLower Char of Char;
IsLower c == 'a' <= c && c <= 'z';

# Sec 2.7

2.5, -1.2;

zerovec := 0.0, 0.0;
a := 1.5, 6.8;
b := 3.6, 0.9;

LengthVec (Float, Float) of Float;
LengthVec (x, y) == Sqrt (x*x + y*y);

LengthVec a;
LengthVec (1.0, 1.0);

NegVec (Float, Float) of (Float, Float);
NegVec (x, y) == (-x, -y);

NegVec (1.0, 1.0);

bn := NegVec b;

type Vec == Float, Float;

# Sec 2.8

Average (Float, Float) of Float;
Average (x, y) == (x+y) / 2.0;

Average (3.1, 3.3);

AddVec Vec Vec of Vec;
AddVec (x1,y1) (x2,y2) == (x1+x2, y1+y2);

SubVec Vec Vec of Vec;
SubVec v1 v2 == AddVec v1 (NegVec v2);

Distance Vec of Float;
Distance v1 v2 == LengthVec (SubVec v1 v2);

ScaleVec Float Vec of Vec;
ScaleVec r (x,y) == (r*x, r*y);

xc,yc := ScaleVec (4.0,a);

(x1,y1), (x2,y2) := AddVec (a,b), SubVec (a,b);

# Sec 2.10

Bool `Xor` Bool of Bool;
p `Xor` q == (p || q) && Not (p && q);

True `Xor` False `Xor` True;

String `Plus` String of String;
a `Plus` b == "(" @ a @ "+" @ b @ ")";

"1" `Plus` "2" `Plus` "3";

#infix @ "Mont" "Joy";

# Sec 2.24

PairSelf a of a, a;
# PairSelf + of +
# PairSelf - of -
PairSelf x == x, x;

Fst (a, b) of a;
# Fst + + of +
# Fst - + of -
Fst (x, y) == x;

FstFst ((a, b), c) of a;
# FstFst (+, +) + of +
# FstFst (-, +) + of -
FstFst x == Fst (Fst x);

Silly a of a;
# Silly + of +
# Silly - of -
Silly x == FstFst (PairSelf (PairSelf x));

I a of a;
# I + of +
# I - of -
I x == x;

# Chapter 3

Sin 0.5 : Cos 0.5 : Exp 0.5 : .;

Upto m n == . if m > n
          | m : Upto (m+1) n; # if m <= n

ProdOf3 (i:j:k:.) == i*j*k;

Prod . == 1;
Prod (n:ns) == n * Prod ns;

MaxL (m:.) == m;
MaxL (m:n:ns) == MaxL (m:ns) if m > n
               | MaxL (n:ns); # if m <= n

FactL n == Prod (Upto 1 n);

Null . == True;
Null (_:_) == False;

Hd (x:_) == x;
Tl (_:xs) == xs;

NLength . == 0;
NLength (x:xs) == 1 + NLength xs;

Length l == AddLen 0 l where {
    AddLen n . == n;
    AddLen n (x:l) == AddLen (n+1) l;
};

Take . _ == .;
Take (x:xs) i == . if i <= 0
               | x : Take xs (i-1); # if i > 0

RTake . _ taken == taken;
RTake (x:xs) i taken == taken if i <= 0
                      | RTake xs (i-1) (x:taken); # if i > 0

Drop . _ == .
Drop (x:xs) i == Drop xs (i-1) if i > 0
               | x:xs;

. @ ys == ys;
(x:xs) @ ys == x : (xs@ys);

NRev . == .;
NRev (x:xs) == NRev xs @ (x:.);

RevAppend . ys == ys;
RevAppend (x:xs) ys == RevAppend xs (x:ys);

Rev xs == RevAppend xs .;

Concat . == .;
Concat (l:ls) == l @ Concat ls;

Zip (x:xs) (y:ys) == (x,y) : Zip xs ys;
Zip _ _ == .;

ConsPair (x,y) (xs,ys) == x:xs, y:ys;

Unzip . == ., .;
Unzip (pair:pairs) == ConsPair pair (Unzip pairs);

Unzip . == ., .;
Unzip ((x,y):pairs) == x:xs, y:ys where xs, ys := Unzip pairs;

RevUnzip . xs ys = xs, ys;
RevUnzip ((x,y):pairs) xs ys == RevUnzip pairs (x:xs) (y:ys);

Change coinvals 0 == .;
Change (c:coinvals) amount ==
    Change coinvals amount
      if amount < c
  | c : Change (c:coinvals) (amount-c);
    # if amount >= c

gb_coins := 50:20:10:5:2:1:.;
us_coins := 25:10:5:1:.;

Change gb_coins 43;

Change us_coins 43;

Change (5:2:.) 16;

AllChange coins coinvals 0 == coins:.;
AllChange coins . amount == .
AllChange coins (c:coinvals) amount ==
    . if amount < 0
  | AllChange (c:coins) (c:coinvals) (amount-c)
      @ AllChange coins coinvals amount;

BinCarry 0 ps == ps;
BinCarry 1 . == 1:.;
BinCarry 1 (p:ps) == 1-p : BinCarry p ps;

BinSum c . qs == BinCarry c qs;
BinSum c ps . == BinCarry c ps;
BinSum c (p:ps) (q:qs) == (c+p+q) `Mod` 2 : BinSum ((c+p+q) `Div` 2) ps qs;

BinProd . _ == .;
BinProd (0:ps) qs == 0 : BinProd ps qs;
BinProd (1:ps) qs == BinSum 0 qs (0 : BinProd ps qs);

HeadCol . == .;
HeadCol ((x:_):rows) == x : HeadCol rows;

TailCols . == .;
TailCols ((_:xs):rows) == xs : TailCols rows;

Transp (.:rows) == .;
Transp rows == HeadCol rows : Transp (TailCols rows);

DotProd . . == 0.0;
DotProd (x:xs) (y:ys) == x * y + DotProd xs ys;

RowProd row . == .;
RowProd row (col:cols) == DotProd row col : RowProd row cols;

RowListProd . cols == .;
RowListProd (row:rows) cols == RowProd row cols : RowListProd rows cols;

MatProd rowsA rowsB == RowListProd rowsA (Transp rowsB);

PivotRow (row:.) == row;
PivotRow (row1:row2:rows) ==
    PivotRow (row1:rows) if Abs (Hd row1) >= Abs (Hd row2)
  | PivotRow (row2:rows);

DelRow p . == .;
DelRow p (row:rows) == rows if p = Hd row
                     | row : DelRow p rows;

ScalarProd k . == .;
ScalarProd k (x:xs) == k*x : ScalarProd k xs;

VectorSum . . == .;
VectorSum (x:xs) (y:ys) == x+y : VectorSum xs ys;

GaussElim (row:.) == (row:.);
GaussElim rows = (p:prow) : GaussElim (ElimCol (DelRow p rows)) where {
    p:prow := PivotRow rows;
    ElimCol . == .;
    ElimCol ((x:xs):rows) == VectorSum xs (ScalarProd (-x/p) prow)
                               : ElimCol rows;
};

Solutions . == -1.0:.;
Solutions ((x:xs):rows) == -DotProd solns xs/x : solns
                           where solns := Solutions rows;

Squares r == Between firstx 0 where {
    firstx := Floor (Sqrt r);
    Between x y == Above y where {
        diff := r - x*x;
        Above y == .                         if y > x
                 | Above (y+1)               if y*y < diff
                 | (x,y):Between (x-1) (y+1) if y*y = diff
                 | Between (x-1) y;          # if y*y > diff
    };
};

Next xlist (y:ys) == Next (y:xlist) ys if Hd xlist <= y
                   | Swap xlist        # if Hd xlist > y
where {
    Swap (x:.) == y:x:ys;
    Swap (x:xk:xs) == x:Swap (xk:xs)     if xk > y
                    | (y:xk:xs) @ (x:ys) # if xk <= y
};

NextPerm (y:ys) = Next (y:.) ys;

x `Mem` . == False;
x `Mem` (y:l) == x = y || (x `Mem` l);

NewMem x xs == xs if x `Mem` xs | x:xs;

SetOf . == .;
SetOf (x:xs) == NewMem x (SetOf xs);

Union . ys == ys;
Union (x:xs) ys == NewMem x (Union xs ys);

Inter . ys == ys;
Inter (x:xs) ys == x:Inter xs ys if x `Mem` ys | Inter xs ys;

. `Subs` ys == True;
(x:xs) `Subs` ys == x `Mem` ys && (xs `Subs` ys);

xs `Seq` ys == xs `Subs` ys && (ys `Subs` xs);

PowSet . base == (base:.);
PowSet (x:xs) base = PowSet xs base @ PowSet xs (x:base);

CartProd . ys == .;
CartProd (x:xs) ys == Pairx ys where {
    xsprod := CartProd xs ys;
    Pairx . == xsprod;
    Pairx (y:ytail) == (x,y) : Pairx ytail;
};

ItUnion . ys == ys;
ItUnion (x:xs) ys == ItUnion xs (NewMem x ys);

CProd . ys == .;
CProd (x:xs) ys == Pairx ys where {
    Pairx . == CProd xs ys;
    Pairx (y:ytail) = (x,y) : Pairx ytail;
};

battles := ("Crecy",1346):("Poitiers",1356):("Agincourt",1415)
          :("Trafalgar",1805):("Waterloo",1815):.;

Assoc . a == .;
Assoc ((x,y):pairs) a == y:. if a = x | Assoc pairs a;

Assoc battles "Agincourt";
Assoc battles "Austerlitz";

Nexts a . == .;
Nexts a ((x,y):pairs) == y:Nexts a pairs if a = x;
                       | Nexts a pairs;

DepthF . graph visited == Rev visited;
DepthF (x:xs) graph visited ==
    DepthF xs graph visited                       if x `Mem` visited
  | DepthF (Nexts x graph @ xs) graph (x:visited);

Depth . graph visited == Rev visited;
Depth (x:xs) graph visited ==
    Depth xs graph (visited             if x `Mem` visited
                  | Depth (Nexts x graph) graph (x:visited));

TopSort graph == Sort starts . where {
    starts,_ := Unzip graph;
    Sort . visited == visited;
    Sort (x:xs) visited == Sort xs (visited             if x `Mem` visited
                                  | x:Sort (Nexts x graph) visited);
};

PathSort graph == Sort starts . . where {
    starts,_ := Unzip graph;
    Sort . path visited == visited;
    Sort (x:xs) path visited == Hd . #{ abort! #}     if x `Mem` path
                              | Sort xs path (visited     if x `Mem` visited
                                     | x:Sort (Nexts x graph) (x:path) visited);
};

NewVisit x (visited, cys) == (x:visited, cys);

CycleSort graph == Sort starts . (., .) where {
    starts,_ := Unzip graph;
    Sort . path (visited, cys) == (visited, cys);
    Sort (x:xs) path (visited, cys) ==
        Sort xs path (visited, x:cys                   if x `Mem` path
                    | visited, cys                     if x `Mem` visited
                    | NewVisit x (Sort (Nexts x graph) (x:path) (visited, cys)));
};

def {
    NextRand seed == t - m * Floor (t/m) where t := a * seed;
}
where {
    a := 16_807.0;
    m := 2_147_483_647.0;
};

RandList n seed tail == seed, tail                 if n = 0
                      | RandList (n-1) (NextRand seed) (seed:tail);

Ins x . == x:.;
Ins x (y:ys) == x:y:ys           if x <= y
              | y:Ins x ys;

InSort . == .;
InSort (x:xs) == Ins x (InSort xs);

Quick . == .;
Quick (x:.) == (x:.);
Quick (a:bs) == Partition . . bs where {
    Partition left right . == Quick left @ (a:Quick right);
    Partition left right (x:xs) ==
        Partition (x:left) right xs             if x <= a
      | Partition left (x:right) xs;
};

Merge . ys == ys;
Merge xs . == xs;
Merge (x:xs) (y:ys) ==
    x : Merge xs (y:ys)                 if x <= y
  | y : Merge (x:xs) ys;

MergeSort . == .;
MergeSort (x:.) == (x:.);
MergeSort xs == Merge (MergeSort (xs `Take` k))
                      (MergeSort (xs `Drop` k))
    where k := Length xs `Div` 2;

MergePairs (l:.) k == (l:.);
MergePairs (l1:l2:ls) k ==
    l1:l2:ls
        if k `Mod` 2 = 1
  | MergePairs (Merge l1 l2:ls) (k `Div` 2);

Sorting . ls k == Hd (MergePairs ls 0);
Sorting (x:xs) ls k == Sorting xs (MergePairs ((x:.):ls) (k+1)) (k+1);

NextRun run . == Rev run, .;
NextRun run (x:xs) ==
    Rev run, x:xs                       if x < Hd run
  | NextRun (x:run) xs;

SAMSorting . ls k == Hd (MergePairs ls 0);
SAMSorting (x:xs) ls k == SAMSorting tail (MergePairs (run:ls) (k+1)) (k+1)
    where run, tail := NextRun (x:.) xs;

SAMSort xs == SAMSorting xs (.:.) 0;

Alts . xs ys == xs, ys;
Alts (x:.) xs ys == x:xs, ys;
Alts (x:y:l) xs ys == Alts l (x:xs) (y:ys);

TakeDrop . n xs == xs, .;
TakeDrop (x:l) n xs == TakeDrop l (n-1) (x:xs)          if n > 0
                     | xs, x:l;

Sum . us == us:t;
Sum ts . == ts;
Sum ((m,a):ts) ((n,b):us) ==
    (m,a) : Sum ts ((n,b):us)                   if m > n
  | (n,b) : Sum us ((m,a):ts)                   if n > m
  | Sum ts us                                   if a + b = 0.0
  | (m,a+b) : Sum ts us;

TermProd (m,a) . == .:t;
TermProd (m,a) ((n,b):ts) == (m+n, a*b) : TermProd (m,a) ts;

NProd . us == .;
NProd ((m,a):ts) us == Sum (TermProd (m,a) us) (NProd ts us);

Prod . us == .;
Prod ((m,a):.) us == TermProd (m,a) us;
Prod ts us == Sum (Prod (ts `Take` k) us) (Prod (ts `Drop` k) us)
    where k := Length ts `Div` 2;

QuoRem ts ((n,b):us) == Dividing ts . where {
    Dividing . qs == Rev qs, .;
    Dividing ((m,a):ts) qs ==
        Rev qs, (m,a):ts                        if m < n
      | Dividing (Sum ts (TermProd (m-n,-a/b) us))
                 ((m-n,a/b):qs);
};

GCD . us == us;
GCD ts us == GCD (Snd (QuoRem us ts)) ts;



# Chapter 4

data Person == {
    King;
    Peer String String Int;
    Knight String;
    Peasant String;
};

persons := King:Peasant "Jack Cade":Knight "Gawain":.;

Title == {
    King -> "His Majesty the King";
    Peer deg terr _ -> "The " @ deg @ " of " @ terr;
    Knight name -> "Sir " @ name;
    Peasant name -> name;
};

Sirs == {
    . -> .;
    Knight s : ps -> s : Sirs ps;
    p : ps -> Sirs ps;
};

Superior == {
    King, Peer _ -> True;
    King, Knight _ -> True;
    King, Peasant _ -> True;
    Peer _, Knight _ -> True;
    Peer _, Peasant _ -> True;
    Knight _, Peasant _ -> True;
    _ -> False;
};

Superior == {
    (King, Peer _) || (King, Knight _) || (King, Peasant _) ||
    (Peer _, Knight _) || (Peer _, Peasant _) || (Knight _, Peasant _)
        -> True;
    _ -> False;
};

Superior == match? {
    King, Peer _; King, Knight _; King, Peasant _;
    Peer _, Knight _; Peer _, Peasant _; Knight _, Peasant _;
};

data Degree == { Duke; Marquis; Earl; Viscount; Baron };

Lady == {
    Duke -> "Duchess";
    Marquis -> "Marchioness";
    Earl -> "Countess";
    Viscount -> "Viscountess";
    Baron -> "Baroness";
};

data Bool == { True; False };

Not == { True -> False; False -> True };

data Order == { LT; EQ; GT };

data Option a == { NONE; SOME a };

data Sum a b == { In1 a; In2 b };

Concat1 == {
    . -> "";
    In1 s : l -> s @ Concat1 l;
    In2 _ : l -> Concat1 l;
};

NextRun run . == ...;
NextRun (run && r:_) (x:xs) ==
    Rev run, x:xs               if x < r
  | NextRun (x:run) xs;

Merge xlist ylist == xlist with {
    . -> ylist;
    x:xs -> ylist with {
        . -> xlist;
        y:ys -> x : Merge xs ylist              if x <= y
              | y : Merge xlist ys;
    };
};

data ListExn == { Empty; Subscript };

Hd == { x:_ -> x; _ -> raise Empty };
Tl == { _:xs -> xs; _ -> raise Empty };

Nth (x:_) 0 == x
Nth (x:xs) n == Nth xs (n-1)            if n > 0
              | raise Subscript;
Nth _ _ == raise Subscript;

data Change == Change;

BackChange == {
    fn coinvals 0 -> .;
    fn . amount -> raise Change;
    fn (c:coinvals) amount -> raise Change if amount < 0
        | (c : fn (c:coinvals) (amount-c)
           handle Change -> fn coinvals amount);
};

data Tree a == { Lf; Br a (Tree a) (Tree a) };

birnam := Br "The" (Br "wood" Lf (Br "of" (Br "Birnam" Lf Lf) Lf)) Lf;

Size == { Lf -> 0; Br v t1 t2 -> 1 + fn t1 + fn t2 };
Depth == { Lf -> 0; Br v t1 t2 -> 1 + Max (fn t1) (fn t2) };

CompTree k n == Lf if n = 0 | Br k (CompTree (2*k) (n-1))
                                   (CompTree (2*k+1) (n-1));

Reflect == { Lf -> Lf; Br v t1 t2 -> Br v (fn t2) (fn t1) };

Preorder == { Lf -> .; Br v t1 t2 -> (v:.) @ fn t1 @ fn t2 };
Inorder == { Lf -> .; Br v t1 t2 -> fn t1 @ (v:.) @ fn t2 };
Postorder == { Lf -> .; Br v t1 t2 -> fn t1 @ fn t2 @ (v:.) };

Preord == {
    fn Lf vs -> vs;
    fn (Br v t1 t2) vs -> v : fn t1 (fn t2 vs);
};

Inord == {
    fn Lf vs -> vs;
    fn (Br v t1 t2) vs -> fn t1 (v : fn t2 vs);
};

Postord == {
    fn Lf vs -> vs;
    fn (Br v t1 t2) vs -> fn t1 (fn t2 (v : vs));
};

BalPre == {
    . -> Lf;
    x:xs -> Br x (fn (xs `Take` k)) (fn (xs `Drop` k)) where
        k := Length xs `Div` 2;
};

BalIn == {
    . -> Lf;
    xs -> Br y (fn (xs `Take` k)) (fn ys) where {
        k := Length xs `Div` 2;
        y:ys := xs `Drop` k;
    };
};

type Key == String;
type T a == Tree (Key, a);

data DictExn == E Key;

Empty == Lf;
Lookup == {
    fn Lf b -> raise E b;
    fn (Br (a,x) t1 t2) b -> Compare a b with {
        GT -> fn t1 b;
        EQ -> x;
        LT -> fn t2 b;
    };
};
Insert == {
    fn Lf b y -> Br (b,y) Lf Lf;
    fn (Br (a,x) t1 t2) b y -> Compare a b with {
        GT -> Br (a,x) (fn t1 b y) t2;
        EQ -> raise E b;
        LT -> Br (a,x) t1 (fn t2 b y);
    };
};
Update == {
    fn Lf b y -> Br (b,y) Lf Lf;
    fn (Br (a,x) t1 t2) b y -> Compare a b with {
        GT -> Br (a,x) (fn t1 b y) t2;
        EQ -> Br (a,y) t1 t2;
        LT -> Br (a,x) t1 (fn t2 b y);
    };
};

Sub == {
    fn Lf _ -> raise Subscript;
    fn (Br v t1 t2) k -> v                      if k = 1
                       | fn t1 (k `Div` 2)      if k `Mod` 2 = 0
                       | fn t2 (k `Div` 2);
};

Update == {
    fn Lf k w -> Br w Lf Lf                     if k = 1
               | raise Subscript;
    fn (Br v t1 t2) k w -> Br w t1 t2           if k = 1
                         | Br v (fn t1 (k `Div` 2) w) t2
                                                if k `Mod` 2 = 0
                         | Br v t1 (fn t2 (k `Div` 2) w);
};

Delete == {
    fn Lf n -> raise Subscript;
    fn (Br v t1 t2) n -> Lf                     if n = 1
                       | Br v (fn t1 (n `Div` 2)) t2
                                                if n `Mod` 2 = 0
                       | Br v t1 (fn t2 (n `Div` 2));
};

LoExt == {
    fn Lf w -> Br w Lf Lf;
    fn (Br v t1 t2) w -> Br w (fn t2 v) t1;
};

LoRem == {
    Lf -> raise Size;
    Br _ Lf Lf -> Lf;
    Br _ (t1 && Br v _ _) t2 -> Br v t2 (fn t1);
};

data Array a == Array (Tree a) Int;

Empty == Array Lf 0;
Length (Array _ n) == n;
Sub (Array t n) k == Braun.Sub t (k+1)          if 0 <= k && k < n
                   | raise Subscript;
Update (Array t n) k w == Array (Braun.Update t (k+1) w) n
                                                if 0 <= k && k < n
                        | raise Subscript;
LoExt (Array t n) w == Array (Braun.LoExt t w) (n+1);
LoRem (Array t n) == Array (Braun.LoRem t) (n-1) if n > 0 | raise Size;
HiExt (Array t n) w == Array (Braun.Update t (n+1) w) (n+1);
HiRem (Array t n) == Array (Braun.Delete t n) (n-1) if n > 0 | raise Size;

Insert == {
    fn w Lf -> Br w Lf Lf;
    fn w (Br v t1 t2) -> Br w (fn v t2) t1      if w <= v
                       | Br v (fn w t2) t1;
};

LeftRem == {
    Br v Lf Lf -> v, Lf;
    Br v t1 t2 -> w, Br v t2 t where w, t := fn t1;
};

SiftDown == {
    fn w Lf Lf -> Br w Lf Lf;
    fn w (t && Br v Lf Lf) Lf ->
        Br w t Lf                               if w <= v
      | Br v (Br w Lf Lf) Lf;
    fn w (t1 && Br v1 p1 q1) (t2 && Br v2 p2 q2) ->
        Br w t1 t2                              if w <= v1 && w <= v2
      | Br v1 (fn w p1 q1) t2                   if v1 <= v2
      | Br v2 t1 (fn w p2 q2);
};

DelMin == {
    Lf -> raise Size;
    Br v Lf _ -> Lf;
    Br v t1 t2 -> SiftDown w t2 t where w, t := LeftRem t1;
};

Heapify == {
    fn 0 vs -> Lf, vs;
    fn n (v:vs) -> SiftDown v t1 t2, vs2 where {
        t1, vs1 := fn (n `Div` 2) vs;
        t2, vs2 := fn (n-1 `Div` 2) vs1;
    };
};

FromList vs == Fst (Heapify (Length vs) vs);
ToList == { Lf -> .; t && Br v _ _ -> v : fn (DelMin t) };
Sort vs == ToList (FromList vs);

data Prop = { Atom String; Neg Prop; Conj Prop Prop; Disj Prop Prop };

Implies p q == Disj (Neg p) q;

Show == {
    Atom a -> a;
    Neg p -> "(~#)" (fn p);
    Conj p q -> "(# & #)" (fn p) (fn q);
    Disj p q -> "(# | #)" (fn p) (fn q);
};

NNF == {
    Atom a -> Atom a;
    Neg (Atom a) -> Neg (Atom a);
    Neg (Neg p) -> fn p;
    Neg (Conj p q) -> fn (Disj (Neg p) (Neg q));
    Neg (Disj p q) -> fn (Conj (Neg p) (Neg q));
    Conj p q -> Conj (fn p) (fn q);
    Disj p q -> Disj (fn p) (fn q);
};

NNFPos == {
    Atom a -> Atom a;
    Neg p -> NNFNeg p;
    Conj p q -> Conj (NNFPos p) (NNFPos q);
    Disj p q -> Disj (NNFPos p) (NNFPos q);
};
NNFNeg == {
    Atom a -> Neg (Atom a);
    Neg p -> NNFPos p;
    Conj p q -> Disj (NNFNeg p) (NNFNeg q);
    Disj p q -> Conj (NNFNeg p) (NNFNeg q);
};

Distrib == {
    fn p (Conj q r) -> Conj (fn p q) (fn p r);
    fn (Conj q r) p -> Conj (fn q p) (fn r p);
    fn p q -> Disj p q;
};

CNF == {
    Conj p q -> Conj (fn p) (fn q);
    Disj p q -> Distrib (fn p) (fn q);
    p -> p;
};

data CNFExn == NonCNF;

Positives == {
    Atom a -> a:.;
    Neg (Atom _) -> .;
    Disj p q -> fn p @ fn q;
    _ -> raise NonCNF;
};
Negatives == {
    Atom _ -> .;
    Neg (Atom a) -> a:.;
    Disj p q -> fn p @ fn q;
    _ -> raise NonCNF;
};

Taut == {
    Conj p q -> fn p && fn q;
    p -> Not (Null (Positives p `Inter` Negatives p));
};



# Chapter 5

(n -> n*2) 9;

Double == n -> n*2;

Prefix pre == Cat where Cat post == pre@post;

knightify := Prefix "Sir ";

Prefix pre post == pre@post;

RepList == { fn n x -> . if n = 0 | x : fn (n-1) x };

InSort lessequal == Sort where {
    Ins x == {
        . -> x:.;
        y:ys -> x:y:ys                          if x `lessequal` y
              | y:fn ys;
    };
    Sort == { . -> .; x:xs -> Ins x (fn xs) };
};

InSort (#infix <=) (5:3:7:5:9:8:.);
InSort (#infix >=) (5:3:7:5:9:8:.);

LeqStringPair (a,b) (c,d) == a<c || a=c && b<=d;

Summation f m == Sum 0 0.0 where Sum == {
    fn i z -> z                                 if i = m
            | Sum (i+1) (z+f i);
};

SecL x f y == f x y;
SecR f y x == f x y;
SecL x f == {x`f`_};
SecR f y == {_`f`y};

I x == x;
K x y == x;

Summation (K 7.0) 5;

S x y z == x z (y z);

S K K 17;

Map f == { . -> .; x:xs -> f x:fn xs };

Filter pred == { . -> .; x:xs -> x:fn xs if pred x | fn xs };

Transp == { .:_ -> .; rows -> Map Hd rows : fn (Map Tl rows) };

x \ f == f x;
l \\ f == Map f l;

Transp == { .:_ -> .; rows -> rows \\ Hd : fn (rows \\ Tl) }:
Inter xs ys == Filter (SecR Mem ys) xs;
xs `Inter` ys == Filter {_ `Mem` ys} xs;

TakeWhile pred == { . -> .; x:xs -> x:fn xs if pred x | . };
DropWhile pred == { . -> .; x:xs -> fn xs if pred x | x:xs };
Exists pred == { . -> False; x:xs -> pred x || fn xs };
All pred == { . -> True; x:xs -> pred x && fn xs };
x `Mem` xs == Exists {_ = x} xs;
Disjoint xs ys == All (x -> All (y -> x /= y) ys) xs;

FoldL f == { fn e . -> e; fn e (x:xs) -> fn (f x e) xs }:
FoldR f == { fn e . -> e; fn e (x:xs) -> f x (fn e xs) };
FoldR f e == { . -> e; x:xs -> f x (fn xs) };

xs \@ f == e -> FoldR f e xs;

CartProd xs ys == FoldR (fn x pairs -> FoldR (fn y l -> (x,y):l) pairs ys) . xs;
xs `CartProd` ys == FoldR (x `fn` pairs -> FoldR (y `fn` l -> (x,y):l) pairs ys) . xs;

Pair x y == x, y;

("Lord":"Lady":.) \\ {a -> ("Hastings":"Stanley":.) \\ Pair a};
("Lord":"Lady":.) \\ {a -> ("Hastings":"Stanley":.) \\ {a,_}};

Repeat f == { fn n x -> fn (n-1) (f x) if n > 0 | x };

Lf \ ({t -> Br "No" t t} `Repeat` 3);

FactAux == k, p -> k+1, k*p;
Repeat FactAux 5 (1,1);
(1,1) \ ({k, p -> k+1, k*p} `Repeat` 5);

TreeFold f e == { Lf -> e; Br u t1 t2 -> f u (fn t1) (fn t2) };

TreeFold {fn _ c1 c2 -> 1 + c1 + c2} 0;
TreeFold {fn _ d1 d2 -> 1 + (d1 `Max` d2)} 0;
TreeFold {fn u t1 t2 -> Br u t2 t1} Lf;
TreeFold {fn u l1 l2 -> (u:.) @ l1 @ l2} .;

TreeFold {1+_2+_3} 0;
TreeFold {1+(_2 `Max` _3)} 0;
TreeFold {Br _1 _3 _2} Lf;
TreeFold {(_:.) @ _ @ _} .;

data Term == { Var String; Fun String (List Term) };

Subst f == { Var a -> f a; Fun a args -> Fun a (args \\ fn) };
Vars == { Var a -> a:.; Fun _ args -> Concat (args \\ fn) };
AccumVars == {
    Var a, bs -> a:bs;
    Fun _ args, bs -> FoldR fn bs args;
};
AccumVars == {
    Var a, bs -> a:bs;
    Fun _ args, bs -> (args \@ fn) bs;
};

Replace t a b == t if a = b | Var b;

data Seq a == { Nil; Cons a (() => Seq a) };

data SeqExn == Empty;

Hd == { Cons x xf -> x; Nil -> raise Empty };
Tl == { Cons x xf -> xf(); Nil -> raise Empty };
Cons_ x xq == Cons x {xq};

FromList l == FoldR Cons_ Nil l;
FromList l == (l \@ Cons_) Nil;

From k == Cons k {From (k+1)};

Take == {
    fn xq 0 -> .;
    fn Nil n -> raise Subscript;
    fn (Cons x xf) n -> x : fn (xf()) (n-1);
};

Squares == { Nil -> Nil; Cons x xf -> Cons (x*x) {Squares (xf())} };
Add == {
    fn (Cons x xf) (Cons y yf) -> Cons (x+y) {Add (xf()) (yf())};
    fn _ _ -> Nil;
};
xq @ yq == xq with { Nil -> yq; Cons x xf -> Cons x {xf() @ yq} };

Interleave xq yq == xq with {
    Nil -> yq;
    Cons x xf -> Cons x {Interleave yq (xf())};
};

Map f == { Nil -> Nil; Cons x xf -> Cons (f x) {Map f (xf())} };
Filter pred == {
    Nil -> Nil;
    Cons x xf -> Cons x {Filter pred (xf())} if pred x | fn (xf());
};

Iterates f x == Cons x {Iterates f (f x)};