From bd85f8a17b59ccebdfa53a1799a02b8f8ebfd877 Mon Sep 17 00:00:00 2001
From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>
Date: Thu, 9 Feb 2017 13:59:41 +0100
Subject: [PATCH] leftist_heap moved to new system

---
 examples/leftist_heap.mlw | 21 +++++++--------------
 1 file changed, 7 insertions(+), 14 deletions(-)

diff --git a/examples/leftist_heap.mlw b/examples/leftist_heap.mlw
index d69eee7b7..71746c34e 100644
--- a/examples/leftist_heap.mlw
+++ b/examples/leftist_heap.mlw
@@ -18,7 +18,7 @@ module Heap
 
   type heap
 
-  function size heap : int
+  val function size heap : int
 
   function occ elt heap : int
 
@@ -39,9 +39,6 @@ module Heap
   val is_empty (h: heap) : bool
     ensures { result <-> size h = 0 }
 
-  val size (h: heap) : int
-    ensures { result = size h }
-
   val merge (h1 h2: heap) : heap
     ensures { forall x. occ x result = occ x h1 + occ x h2 }
     ensures { size result = size h1 + size h2 }
@@ -74,7 +71,7 @@ module Size
   use import TreeRank
   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
     | N _ l _ r -> 1 + size l + size r
     end
@@ -105,7 +102,7 @@ end
 module LeftistHeap
 
   type elt
-  predicate le elt elt
+  val predicate le elt elt
   clone relations.TotalPreOrder with type t = elt, predicate rel = le
 
   use import TreeRank
@@ -117,7 +114,7 @@ module LeftistHeap
   type t = tree elt
 
   (* [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
     | N _ _ x _ -> le e x
     end
@@ -144,8 +141,8 @@ module LeftistHeap
   = match h with
     | E -> absurd
     | N _ l _ r ->
-       if l <> E then root_is_miminum l;
-       if r <> E then root_is_miminum r
+       match l with E -> root_is_miminum l | _ -> () end;
+       match r with E -> root_is_miminum r | _ -> () end
     end
 
   function rank (h: t) : int = match h with
@@ -172,11 +169,7 @@ module LeftistHeap
 
   let is_empty (h: t) : bool
     ensures { result <-> size h = 0 }
-  = h = E
-
-  let size (h: t) : int
-    ensures { result = size h }
-  = size h
+  = match h with E -> true | N _ _ _ _ -> false end
 
   let rank (h: t) : int
     requires { leftist_heap h }
-- 
GitLab