~thon/thon

c157067fa740ee91e299a10f6c7e871f71f53ae1 — Evan Bergeron 21 days ago 96d1b14
bst depth example
1 files changed, 53 insertions(+), 0 deletions(-)

A examples/bst-depth.thon
A examples/bst-depth.thon => examples/bst-depth.thon +53 -0
@@ 0,0 1,53 @@
data tree = Nil unit | Node nat * (tree * tree) 

in let decr : nat -> nat =
  \ x : nat ->
    ifz x of
      Z -> Z
    | S p -> p

in let sub : nat -> nat -> nat =
  \ x : nat ->
  \ y : nat ->
    rec y of
      Z -> x
    | prevRec -> (decr prevRec)

in let lt : nat -> nat -> nat =
  \ x : nat ->
  \ y : nat ->
  ifz (sub y x) of
    Z -> Z
  | S p -> S Z

in fun insert : nat -> tree -> tree =
    \ n : nat ->
    \ bst : tree ->
    case exposetree bst of
        empty -> Node(n, ((Nil unit), (Nil unit)))
      | natAndNodeAndNode ->
        let thisNode : nat = fst natAndNodeAndNode in
        let leftNode : tree = fst (snd natAndNodeAndNode) in
        let rightNode : tree = snd (snd natAndNodeAndNode) in
        ifz (lt n thisNode) of
            Z -> Node(n, (leftNode, (insert n rightNode)))
          | S p -> (Node(n, ((insert n leftNode), rightNode)))

in fun depth : tree -> nat =
    \ t : tree ->
    case exposetree t of
        empty -> Z
      | natAndNodeAndNode ->
        let leftDepth : nat = depth (fst (snd natAndNodeAndNode)) in
        let rightDepth : nat = depth (snd (snd natAndNodeAndNode)) in
        ifz (lt leftDepth rightDepth) of
            Z -> S leftDepth
          | S p -> S rightDepth

(* This tree has depth 2.
 *
 *     1
 *    / \
 *   0   2
 *)
in (depth (insert (S S Z) (insert (Z) (insert (S Z) (Nil unit)))))