examples_in_progress/bst.coma

   1 use int.Int
   2 use bintree.Tree
   3 use bintree.Occ
   4
   5 let fail = { false } any
   6
   7 let if (b: bool) (then {b}) (else {not b}) = any
   8
   9 let unTree < 'elt > (t: tree 'elt)
  10   (onNode (v: 'elt) (l r: tree 'elt) {t = Node l v r})
  11   (onLeaf {t = Empty})
  12   = any
  13
  14 let rec remove_min (t: tree 'a) {t <> Empty}
  15       (return (m: 'a) (o: tree 'a)
  16         { forall x. mem x t <-> (x = m || mem x o) })
  17   = unTree < 'a> {t} node fail
  18      [ node (x: 'a) (l r: tree 'a) ->
  19        if {l=Empty} (-> return {x} {r})
  20                     (-> remove_min {l}
  21                       (fun (m: 'a) (l': tree 'a) -> return {m} {Node l' x r}))
  22      ]
  23
  24 let remove_root (t: tree 'a) (return (o: tree 'a)) =
  25   unTree < 'a > {t}
  26   (fun (_x: 'a) (l r: tree 'a) ->
  27     (! if {r=Empty} (-> return {l})
  28                     (-> remove_min {r}
  29                       (fun (m: 'a) (r': tree 'a) -> return {Node l m r'}))
  30     )
  31     [ return (o: tree 'a) ->
  32       { forall x. mem x o <-> (mem x l || mem x r) }
  33       (! return {o}) ]
  34   )
  35   fail
  36
  37 function cl (tree 'a) : int
  38
  39 let rec count_leaf (&c: int) (t: tree 'a) [old_c: int = c] {}
  40   (return { c = old_c + cl t })
  41 = unTree < 'a > {t} (fun (_x: 'a) (l r: tree 'a) ->
  42     count_leaf &c {l} (-> count_leaf &c {r} return)) (-> [&c <- c + 1] return)