Braun trees are special binary trees that can be defined inductively as follows:

If a binary tree is empty, then it is a Braun tree.

If both children of a binary tree are Braun trees and the size of the left child minus the size of the right child equals 0 or 1, then the binary tree is a Braun tree.

A polymorphic datatype is declared as follows for representing binary trees:

datatype tree (a:t@ype) = | tree_nil of ((*void*)) | tree_cons of (a, tree(a)(*left*), tree(a)(*right*)) // end of [tree] // end of [datatype]

fun{ a:t@ype } size (t: tree a): int = case+ t of | tree_nil () => 0 | tree_cons (_, tl, tr) => 1 + size(tl) + size(tr) // end of [size] fun{ a:t@ype } brauntest0 (t: tree a): bool = ( case+ t of | tree_nil () => true | tree_cons (_, tl, tr) => let val cond1 = brauntest0(tl) andalso brauntest0(tr) in if cond1 then let val df = size(tl) - size(tr) in (df = 0) orelse (df = 1) end else false end // end of [tree_cons] ) (* end of [brauntest0] *)

In the following program, the defined function brauntest1 also tests whether a given binary tree is a Braun tree:

fun{ a:t@ype } brauntest1 (t: tree a): bool = let exception Negative of () fun aux (t: tree a): int = ( case+ t of | tree_nil () => 0 | tree_cons (_, tl, tr) => let val szl = aux (tl) and szr = aux (tr) val df = szl - szr in if df = 0 orelse df = 1 then 1+szl+szr else $raise Negative() end // end of [tree_cons] ) (* end of [aux] *) in try let val _ = aux (t) in true // [t] is a Braun tree end with ~Negative() => false // [t] is not a Braun tree // end of [try] end // end of [brauntest1]

The use of the exception mechanism in the implementation of brauntest1 is a convincing one because the range between the point where an exception is raised and the point where the raised exception is captured can span many function calls. If this range is short (e.g., spanning only one function call) in a case, then the programmer should probably investigate whether it is a sensible use of the exception mechanism. For instance, the use of exception in the following example may seem interesting but it actually leads to very inefficient code:

fun{ a:t@ype } list0_length (xs: list0 (a)): int = try 1 + list0_length (xs.tail()) with ~ListSubscriptExn() => 0 // end of [list0_length]

Please find the entirety of the code in this section plus some additional code for testing on-line.