leftist_heap moved to new system

parent 7fd45176
...@@ -18,7 +18,7 @@ module Heap ...@@ -18,7 +18,7 @@ module Heap
type heap type heap
function size heap : int val function size heap : int
function occ elt heap : int function occ elt heap : int
...@@ -39,9 +39,6 @@ module Heap ...@@ -39,9 +39,6 @@ module Heap
val is_empty (h: heap) : bool val is_empty (h: heap) : bool
ensures { result <-> size h = 0 } ensures { result <-> size h = 0 }
val size (h: heap) : int
ensures { result = size h }
val merge (h1 h2: heap) : heap val merge (h1 h2: heap) : heap
ensures { forall x. occ x result = occ x h1 + occ x h2 } ensures { forall x. occ x result = occ x h1 + occ x h2 }
ensures { size result = size h1 + size h2 } ensures { size result = size h1 + size h2 }
...@@ -74,7 +71,7 @@ module Size ...@@ -74,7 +71,7 @@ module Size
use import TreeRank use import TreeRank
use import int.Int use import int.Int
function size (t: tree 'a) : int = match t with let rec function size (t: tree 'a) : int = match t with
| E -> 0 | E -> 0
| N _ l _ r -> 1 + size l + size r | N _ l _ r -> 1 + size l + size r
end end
...@@ -105,7 +102,7 @@ end ...@@ -105,7 +102,7 @@ end
module LeftistHeap module LeftistHeap
type elt type elt
predicate le elt elt val predicate le elt elt
clone relations.TotalPreOrder with type t = elt, predicate rel = le clone relations.TotalPreOrder with type t = elt, predicate rel = le
use import TreeRank use import TreeRank
...@@ -117,7 +114,7 @@ module LeftistHeap ...@@ -117,7 +114,7 @@ module LeftistHeap
type t = tree elt type t = tree elt
(* [e] is no greater than the root of [h], if any *) (* [e] is no greater than the root of [h], if any *)
predicate le_root (e: elt) (h: t) = match h with let predicate le_root (e: elt) (h: t) = match h with
| E -> true | E -> true
| N _ _ x _ -> le e x | N _ _ x _ -> le e x
end end
...@@ -144,8 +141,8 @@ module LeftistHeap ...@@ -144,8 +141,8 @@ module LeftistHeap
= match h with = match h with
| E -> absurd | E -> absurd
| N _ l _ r -> | N _ l _ r ->
if l <> E then root_is_miminum l; match l with E -> root_is_miminum l | _ -> () end;
if r <> E then root_is_miminum r match r with E -> root_is_miminum r | _ -> () end
end end
function rank (h: t) : int = match h with function rank (h: t) : int = match h with
...@@ -172,11 +169,7 @@ module LeftistHeap ...@@ -172,11 +169,7 @@ module LeftistHeap
let is_empty (h: t) : bool let is_empty (h: t) : bool
ensures { result <-> size h = 0 } ensures { result <-> size h = 0 }
= h = E = match h with E -> true | N _ _ _ _ -> false end
let size (h: t) : int
ensures { result = size h }
= size h
let rank (h: t) : int let rank (h: t) : int
requires { leftist_heap h } requires { leftist_heap h }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment