← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to lib/heap.ml

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
lib/heap.ml
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* $Id: heap.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
10
 
 
11
(*s Heaps *)
 
12
 
 
13
module type Ordered = sig
 
14
  type t
 
15
  val compare : t -> t -> int
 
16
end
 
17
 
 
18
module type S =sig
 
19
  
 
20
  (* Type of functional heaps *)
 
21
  type t
 
22
 
 
23
  (* Type of elements *)
 
24
  type elt
 
25
    
 
26
  (* The empty heap *)
 
27
  val empty : t
 
28
    
 
29
  (* [add x h] returns a new heap containing the elements of [h], plus [x];
 
30
     complexity $O(log(n))$ *)
 
31
  val add : elt -> t -> t
 
32
    
 
33
  (* [maximum h] returns the maximum element of [h]; raises [EmptyHeap]
 
34
     when [h] is empty; complexity $O(1)$ *)
 
35
  val maximum : t -> elt
 
36
    
 
37
  (* [remove h] returns a new heap containing the elements of [h], except
 
38
     the maximum of [h]; raises [EmptyHeap] when [h] is empty; 
 
39
     complexity $O(log(n))$ *) 
 
40
  val remove : t -> t
 
41
    
 
42
  (* usual iterators and combinators; elements are presented in
 
43
     arbitrary order *)
 
44
  val iter : (elt -> unit) -> t -> unit
 
45
    
 
46
  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
 
47
    
 
48
end
 
49
 
 
50
exception EmptyHeap
 
51
 
 
52
(*s Functional implementation *)
 
53
 
 
54
module Functional(X : Ordered) = struct
 
55
 
 
56
  (* Heaps are encoded as complete binary trees, i.e., binary trees
 
57
     which are full expect, may be, on the bottom level where it is filled 
 
58
     from the left. 
 
59
     These trees also enjoy the heap property, namely the value of any node 
 
60
     is greater or equal than those of its left and right subtrees.
 
61
 
 
62
     There are 4 kinds of complete binary trees, denoted by 4 constructors:
 
63
     [FFF] for a full binary tree (and thus 2 full subtrees);
 
64
     [PPF] for a partial tree with a partial left subtree and a full
 
65
     right subtree;
 
66
     [PFF] for a partial tree with a full left subtree and a full right subtree
 
67
     (but of different heights);
 
68
     and [PFP] for a partial tree with a full left subtree and a partial
 
69
     right subtree. *)
 
70
 
 
71
  type t = 
 
72
    | Empty
 
73
    | FFF of t * X.t * t (* full    (full,    full) *)
 
74
    | PPF of t * X.t * t (* partial (partial, full) *)
 
75
    | PFF of t * X.t * t (* partial (full,    full) *)
 
76
    | PFP of t * X.t * t (* partial (full,    partial) *)
 
77
 
 
78
  type elt = X.t
 
79
 
 
80
  let empty = Empty
 
81
 
 
82
  (* smart constructors for insertion *)
 
83
  let p_f l x r = match l with
 
84
    | Empty | FFF _ -> PFF (l, x, r)
 
85
    | _ -> PPF (l, x, r)
 
86
 
 
87
  let pf_ l x = function
 
88
    | Empty | FFF _ as r -> FFF (l, x, r)
 
89
    | r -> PFP (l, x, r)
 
90
 
 
91
  let rec add x = function
 
92
    | Empty -> 
 
93
        FFF (Empty, x, Empty)
 
94
    (* insertion to the left *)
 
95
    | FFF (l, y, r) | PPF (l, y, r) ->
 
96
        if X.compare x y > 0 then p_f (add y l) x r else p_f (add x l) y r
 
97
    (* insertion to the right *)
 
98
    | PFF (l, y, r) | PFP (l, y, r) ->
 
99
        if X.compare x y > 0 then pf_ l x (add y r) else pf_ l y (add x r)
 
100
 
 
101
  let maximum = function
 
102
    | Empty -> raise EmptyHeap
 
103
    | FFF (_, x, _) | PPF (_, x, _) | PFF (_, x, _) | PFP (_, x, _) -> x
 
104
 
 
105
  (* smart constructors for removal; note that they are different
 
106
     from the ones for insertion! *)
 
107
  let p_f l x r = match l with
 
108
    | Empty | FFF _ -> FFF (l, x, r)
 
109
    | _ -> PPF (l, x, r)
 
110
 
 
111
  let pf_ l x = function
 
112
    | Empty | FFF _ as r -> PFF (l, x, r)
 
113
    | r -> PFP (l, x, r)
 
114
 
 
115
  let rec remove = function
 
116
    | Empty -> 
 
117
        raise EmptyHeap
 
118
    | FFF (Empty, _, Empty) -> 
 
119
        Empty
 
120
    | PFF (l, _, Empty) ->
 
121
        l
 
122
    (* remove on the left *)
 
123
    | PPF (l, x, r) | PFF (l, x, r) ->
 
124
        let xl = maximum l in
 
125
        let xr = maximum r in
 
126
        let l' = remove l in
 
127
        if X.compare xl xr >= 0 then 
 
128
          p_f l' xl r 
 
129
        else 
 
130
          p_f l' xr (add xl (remove r))
 
131
    (* remove on the right *)
 
132
    | FFF (l, x, r) | PFP (l, x, r) ->
 
133
        let xl = maximum l in
 
134
        let xr = maximum r in
 
135
        let r' = remove r in
 
136
        if X.compare xl xr > 0 then 
 
137
          pf_ (add xr (remove l)) xl r'
 
138
        else 
 
139
          pf_ l xr r'
 
140
 
 
141
  let rec iter f = function
 
142
    | Empty -> 
 
143
        ()
 
144
    | FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) -> 
 
145
        iter f l; f x; iter f r
 
146
 
 
147
  let rec fold f h x0 = match h with
 
148
    | Empty -> 
 
149
        x0
 
150
    | FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) -> 
 
151
        fold f l (fold f r (f x x0))
 
152
 
 
153
end