datatype tree with nat = {n:nat} Node(n) of int(n) * int * treelist(n) and treelist with nat = Tempty(0) | {m:nat}{n:nat | m >= n} Tcons(m+1) of tree(m) * treelist(n) ;; datatype heap with nat = Hempty(0) | {m:nat}{n:nat | n = 0 \/ m+1 < n} Hcons(m+1) of tree(m) * heap(n) ;; let rank = function Node(r, _, _) -> r withtype {n:nat} tree(n) -> int(n) ;; let root = function Node(_, x, _) -> x withtype {n:nat} tree(n) -> int ;; let link (Node(r, x1, c1) as t1)= function Node(_, x2, c2) as t2 -> if (x1 <= x2) then Node(r+1, x1, Tcons(t2, c1)) else Node(r+1, x2, Tcons(t1, c2)) withtype {r:nat} tree(r) -> tree(r) -> tree(r+1) ;; let rec insTree t = function Hempty -> Hcons(t, Hempty) | Hcons(t', ts') as ts -> if lt_int (rank t) (rank t') then Hcons(t, ts) else insTree (link t t') ts' withtype {r:nat}{n:nat | n = 0 \/ r < n} tree(r) -> heap(n) -> [l:nat | l > r] heap(l) ;; let insert x hp = insTree (Node(0, x, Tempty)) hp withtype int -> [n:nat] heap(n) -> [n:nat | n > 0] heap(n) ;; let rec merge = function (hp1, Hempty) -> hp1 | (Hempty, hp2) -> hp2 | (Hcons(t1, hp1') as hp1), (Hcons(t2, hp2') as hp2) -> if lt_int (rank t1) (rank t2) then Hcons(t1, merge(hp1', hp2)) else if gt_int (rank t1) (rank t2) then Hcons(t2, merge(hp1, hp2')) else let hp = merge(hp1', hp2') in insTree (link t1 t2) hp withtype {m:nat}{n:nat} heap(m) * heap(n) -> [l:nat | (n = 0 /\ l = m) \/ (m = 0 /\ l = n) \/ (l >= min(m, n) > 0)] heap(l) ;; exception Empty_heap;; let rec removeMinTree = function Hempty -> raise Empty_heap | Hcons(t, Hempty) -> (t, Hempty) | Hcons(t, hp) -> let (t', hp') = removeMinTree hp in if root t < root t' then (t, hp) else (t', Hcons(t, hp')) withtype {n:nat} heap(n) -> [r:nat][l:nat | l = 0 \/ l >= n > 0] (tree(r) * heap(l)) ;; let findMin hp = let (t, _) = removeMinTree hp in root t withtype {n:nat} heap(n) -> int ;; let rec to_heap hp = function Tempty -> hp | Tcons(t, ts) -> to_heap (Hcons(t, hp)) ts withtype {m:nat}{n:nat | m = 0 \/ m > n} heap(m) -> treelist(n) -> heap ;; let deleteMin hp = let (Node(_, x, ts), hp) = removeMinTree hp in merge (to_heap Hempty ts, hp) withtype heap -> heap ;;