// (* from Sereni: Size-Change Termination of Higher-Order Functional Programs; PRG-RR-04-20 *)
module RpmLazy;
data Nat = Zero | S(Nat);
data Tree = Leaf(A) | Node(Tree, Tree);
// let fix f =
// let rec x = lazy (Lazy.force (f x))
// in x
// ;;
def A fix(f)() = f(fix());
def Nat minNat(Nat a, Nat b) =
case a {
Zero => Zero;
S(aP) => case b {
Zero => Zero;
S(bP) => S(min(aP, bP));
};
};
// let rec rpm t m =
// match t with
// | Leaf(x) -> lazy (lazy(Leaf(Lazy.force m)), (lazy x))
// | Node(t1,t2) ->
// let p1 = Lazy.force (rpm t1 m)
// and p2 = Lazy.force (rpm t2 m)
// in lazy ((lazy (Node(Lazy.force (fst p1), Lazy.force (fst p2)))),
// (lazy (min (Lazy.force (snd p1)) (Lazy.force (snd p2)))))
// ;;
def Pair, Nat> rpm(Tree t, B m) =
case t {
Leaf(x) => Pair(Leaf(m), x);
Node(t1, t2) =>
let (Pair,Nat> p1) = rpm(t1,m) in
let (Pair,Nat> p2) = rpm(t2,m) in
Pair(Node(fst(p1),fst(p2)), minNat(snd(p1), snd(p2)));
};
// let repmin t =
// let f p = rpm t (lazy (Lazy.force (snd (Lazy.force p)))) in
// Lazy.force (fst (Lazy.force (fix f)))
// ;;
def Pair, Nat> f(Tree t, Pair p) = rpm(t, snd(p));
// No higher-order constructors suppored by abs!
def Nat repmin(Tree t) = fst(fix((A x) => f(t,x))());
// def Nat repmin(Tree t) =
// case rpm(t, snd())
// fst((fix(rpm(t,snd(p)))()));
// let main t = repmin t;;
{
}