File: tree.coma

package info (click to toggle)
why3 1.8.2-3
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 45,028 kB
  • sloc: xml: 185,443; ml: 111,224; ansic: 3,998; sh: 2,578; makefile: 2,568; java: 865; python: 720; javascript: 290; lisp: 205; pascal: 173
file content (17 lines) | stat: -rw-r--r-- 421 bytes parent folder | download | duplicates (2) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
 
use int.Int
use int.MinMax
use bintree.Tree
use bintree.Height

let unTree (t: tree 'a)
    (onNode (x: 'a) (l r: tree 'a) { t = Node l x r })
    (onLeaf { t = Empty })
  = any

let rec height_cps (t: tree 'a) {} (ret (r:int) { r = height t })
= unTree {t}
    (fun (x: 'a) (l r: tree 'a) ->
        height_cps {l} (fun (hl:int) ->
        height_cps {r} (fun (hr:int) ->
        ret {1 + max hl hr})))
    (-> ret {0})