module MergesortDc;
data Nat = Zero | S(Nat);
def Nat lengthNat(List xs) =
case xs {
Nil => Zero;
Cons(x,xsP) => S(lengthNat(xsP));
};
def Bool leq(Nat x, Nat y) =
case x {
Zero => True;
S(xP) => case y {
Zero => False;
S(yP) => leq(xP, yP);
};
};
def A const(A f, B x) = f;
// let const f x = f;;
def Nat halve(Nat x) =
case x {
Zero => Zero;
S(xP) => case xP {
Zero => S(Zero);
S(xPP) => S(halve(xPP));
};
};
exception Error;
// Already defined:
// def List tail(List l) =
// case l {
// Nil => Nil; // should be BOTTOM: throw Error;
// Cons(l,ls) => ls;
// };
// def A head(List l) =
// case l {
// Cons(l,ls) => l;
// };
def List takeNat(Nat n, List l) =
case n {
Zero => Nil;
S(nP) => Cons(head(l), takeNat(nP, tail(l)));
};
def List drop(Nat n, List l) =
case n {
Zero => l;
S(nP) => drop(nP, tail(l));
};
// let divideAndConquer isDivisible solve divide combine initial =
// let rec dc pb =
// match isDivisible pb with
// | False -> solve pb
// | True -> combine pb (map dc (divide pb))
// in dc initial
// ;;
def List divideAndConquer(isDivisible, solve, divide, combine)(List initial) =
if isDivisible(initial) then solve(pb) else combine(pb)(map(divideAndConquer(intial), divide(pb)));
// let rec merge ys zs =
// match ys with
// | Nil -> zs
// | Cons(y,ys') ->
// match zs with
// | Nil -> ys
// | Cons(z,zs') ->
// match leq y z with
// | True -> Cons(y,merge ys' zs)
// | False -> Cons(z,merge ys zs')
// ;;
def List merge(List ys, List zs) =
case ys {
Nil => zs;
Cons(y, ysP) => case zs {
Nil => ys;
Cons(z,zsP) => case leq(y,z) {
True => Cons(y, merge(ysP, zs));
False => Cons(z, merge(ys,zsP));
};
};
};
// let mergesort zs =
// let divisible ys =
// match ys with
// | Nil -> False
// | Cons(y,ys') ->
// match ys' with
// | Nil -> False
// | Cons(y',ys'') -> True
// and divide ys =
// let n = halve (length ys)
// in Cons(take n ys, Cons(drop n ys,Nil))
// and combine p =
// match p with
// | Nil -> raise Error
// | Cons(l1,p') ->
// match p' with
// | Cons(l2,p'') -> merge l1 l2
// | Nil -> raise Error
// in divideAndConquer divisible (fun ys -> ys) divide (const combine) zs
// ;;
// ()
def Bool divisible(List ys) =
case ys {
Nil => False;
Cons(y,ysP) => case ysP {
Nil => False;
Cons(_,_) => True;
};
};
def List> divide(List ys) =
let (Nat n) = halve(lengthNat(ys))
in Cons(takeNat(n,ys), Cons(drop(n, ys), Nil));
def List combine(List> p) =
case p {
Nil => Nil; // Should be be BOTTOM: throw Error;
Cons(l1, pP) => case pP {
Nil => Nil; // Should be be BOTTOM: throw Error;
Cons(l2, pPP) => merge(l1, l2);
};
};
def A id(A x) = x;
def List mergesort(List zs) = divideAndConquer(divisible, id, divide, const(combine))(zs);
def List start(List zs) = mergesort(zs);
{
}