suzanne.soy/kaplan-tarjan-dequeues-ocaml
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

WIP: buffer and deque colors

Browse Source
This commit is contained in:
Georges Dupéron 2018-08-06 00:45:39 +02:00
parent 9fdde72b51
commit 3aa74ea869
1 changed files with 160 additions and 74 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

234
deques.ml
View File

@ -3,7 +3,7 @@
(** jacm-final.pdf p.8 (584) §4.1 media 60 380 368 40 *)
module Buffers = struct
type 'a buffer0 = [`Buffer0]
type buffer0 = [`Buffer0]
type 'a buffer1 = [`Buffer1 of 'a]
type 'a buffer2 = [`Buffer2 of 'a * 'a]
type 'a buffer3 = [`Buffer3 of 'a * 'a * 'a]
@ -16,29 +16,19 @@ open Buffers
module Colors = struct
type 'a green = ['a buffer2 | 'a buffer3]
type 'a yellow = ['a buffer1 | 'a buffer4]
type 'a red = ['a buffer0 | 'a buffer5]
type 'a red = [ buffer0 | 'a buffer5]
(* In addition to the colors defined by Kaplan and Tarjan, we define the
shorhand "empty" for buffers of size zero (which are used later on). *)
type empty = [ | buffer0]
end
open Colors
(** jacm-final.pdf p.9 (585) §4.1 media 60 134 368 36 *)
type 'a buffer = [
`Green of 'a green
| `Yellow of 'a yellow
| `Red of 'a red
]
(** jacm-final.pdf p.8 / 584 §4.1 60 408 368 48 *)
type 'a deque = {
prefix: 'a buffer;
child: ('a * 'a) deque option;
suffix: 'a buffer;
}
(** jacm-final.pdf p.9 (585) §4.1 media 60 206 368 12 *)
module ColorOrder = struct
type nonrec 'a green = [`Green of 'a green]
type nonrec 'a yellow = [`Yellow of 'a yellow]
type nonrec 'a red = [`Red of 'a red]
type nonrec empty = [`Red of empty]
type 'a leGreen = [ | 'a green | 'a yellow | 'a red]
type 'a leYellow = [ | 'a yellow | 'a red]
@ -50,68 +40,164 @@ module ColorOrder = struct
end
open ColorOrder
type 'a nestedDeque = [`Some of ('a * 'a) deque]
type ('prefix, 'substack, 'stack, 'suffix) deque2 = {
prefix: 'prefix;
substack: 'substack;
stack: 'stack;
suffix: 'suffix;
}
(** jacm-final.pdf p.9 (585) §4.1 media 60 230 368 48 *)
module ColoredDeques = struct
type ('a, 'color, 'leColor) coloredDeque =
[ `Full of ('color, 'a nestedDeque, 'leColor) deque2 (* TODO: the nested deque should be a recursive type *)
(* TODO: `L and `R should be merged into a single case + constructor inside, and the empty parts the info deleted *)
| `L of ('a buffer0, [`None], 'leColor) deque2
| `R of ('color, [`None], 'a buffer0) deque2] constraint 'xyz = 'xyz (* TODO: use constraint to allow or forbid the empty child (L/R) case for yellow. *)
type 'a greenDeque = [`Green of ('a, 'a green, 'a leGreen) coloredDeque]
type 'a yellowDeque = [`Yellow of ('a, 'a yellow, 'a leYellow) coloredDeque]
type 'a redDeque = [`Red of ('a, 'a red, 'a leRed) coloredDeque]
(** jacm-final.pdf p.9 (585) §4.1 media 60 134 368 36 *)
module BufferColors = struct
type 'a buffer = ['a green | 'a yellow | 'a red]
end
open ColoredDeques
open BufferColors
(** jacm-final.pdf p.8 / 584 §4.1 60 408 368 48 *)
module Deques = struct
(* We use polymorphic variants instead of the usual 't option so that it is
possible later to indicate in which contexts a deque must or must not
have a non-empty child. *)
type 'a deque = {
prefix: 'a buffer;
child: [`Child of ('a * 'a) deque | `NoChild];
suffix: 'a buffer;
}
(* We can't easily factor this, as OCaml cannot inline polymorphic variants
before they are completely defined. *)
type 'a child = [`Child of ('a * 'a) deque]
type noChild = [`NoChild]
let prefix d = d.prefix
let child d = d.child
let suffix d = d.suffix
end
open Deques
module DequesColors = struct
type ('prefix, 'child, 'suffix) deque = {
prefix: 'prefix;
child: 'child;
suffix: 'suffix;
}
(** jacm-final.pdf p.9 (585) §4.1 media 60 230 368 48 *)
type ('color, 'geColor, 'child) min = [
`LeftMin of ('color, [`Child of 'child | `NoChild], 'geColor) deque
| `RightMin of ('geColor, [`Child of 'child | `NoChild], 'color) deque
(* When the 'color is red, the two cases below are partially redundant
with the ones above. For example, a buffer0,`NoChild,buffer5 dequeue
could be labeled as `RightOnly or `LeftMin or `RightMin. This does not
affect the safety properties, but it would be nicer if we had an
unambiguous labeling. *)
| `LeftOnly of ('color, [ `NoChild], empty) deque
| `RightOnly of ( empty, [ `NoChild], 'color) deque
]
(** jacm-final.pdf p.9 (585) §4.1 media 60 230 368 48 *)
module ColoredDeques2 = struct
type ('a, 'color, 'leColor, 'substack, 'stack) coloredDeque =
[ `Full of ('color, 'substack, 'stack, 'leColor) deque2]
(** The astute reader will notice that if the child of a deque is empty,
then it is the first (deepest) element on the stack. Therefore, the cases
considering that the colour of a deque is that of its only non-empty
buffer, if its child is also empty, apply only to the first element of the
stack. *)
type ('a, 'color, 'leColor, 'substack, 'stack) coloredLRDeque = [
('a, 'color, 'leColor, 'substack, 'stack) coloredDeque
| `L of ('a buffer0, [`None], [`None], 'leColor) deque2
| `R of ('color, [`None], [`None], 'a buffer0) deque2]
(** jacm-final.pdf p.9 (585) §4.1 media 60 290 368 60 *)
(* If we try to inline and merge together polymorphic variants (e.g. ['a
greenDeque|'yellowGDeque]) which are defined as mutually-recursive types,
OCamle gives the following error: *)
(* "Error: The type constructor yellowDeque is not yet completely defined"
if we don't use a fixup: all expanded cases in […|…] have to be
completely defined (or wrapped with a `X so that they need not be
substituted) *)
type 'a greenDeque = ('a, 'a green, 'a leGreen, [`None|`Yellow of 'a yellowDeque], [`None | `Green of 'a greenDeque | `Red of 'a redDeque]) coloredDeque
and 'a yellowDeque = ('a, 'a yellow, 'a leYellow, [`None|`Yellow of 'a yellowDeque], [`None]) coloredDeque
and 'a redDeque = ('a, 'a red, 'a leRed, [`None|`Yellow of 'a yellowDeque], [`None | `Green of 'a greenDeque]) coloredDeque
end
open ColoredDeques2
We therefore first define the types by moving the [`X of …] at the
use-site, and stripping it away from the definition site. Then, we wrap
the types defined that way in order to put back the [`X of …] around each
type. *)
(* Since OCaml does not allow types to be shadowed, we define the first
unwrapped version of the types in a submodule. Types which are made
available in the current scope by using "open" can be shadowed by later
uses of "open" and later definitions. *)
module ToFixup = struct
type 'a greenDeque = ('a green, 'a geGreen, [ `Green of 'a greenDeque
| `Yellow of 'a yellowGRDeque
| `Red of 'a redDeque ]) min
and 'a yellowGDeque = ('a yellow, 'a geYellow, [ `Green of 'a greenDeque
| `Yellow of 'a yellowGDeque ]) min
and 'a yellowGRDeque = ('a yellow, 'a geYellow, [ `Green of 'a greenDeque
| `Yellow of 'a yellowGRDeque
| `Red of 'a redDeque ]) min
and 'a redDeque = ('a red, 'a geRed, [ `Green of 'a greenDeque
| `Yellow of 'a yellowGDeque ]) min
end
open ToFixup
type nonrec 'a greenDeque = [`Green of 'a greenDeque]
type nonrec 'a yellowGDeque = [`Yellow of 'a yellowGDeque]
type nonrec 'a yellowGRDeque = [`Yellow of 'a yellowGRDeque]
type nonrec 'a redDeque = [`Red of 'a redDeque]
module ColoredDequesFixup = struct
type nonrec 'a greenDeque = [`Green of 'a greenDeque ]
and 'a yellowDeque = [`Yellow of 'a yellowDeque]
and 'a redDeque = [`Red of 'a redDeque ]
(** * jacm-final.pdf p.9 (585) §4.1 media 60 290 368 60 *)
type 'a semiregular = ['a greenDeque | 'a yellowGRDeque | 'a redDeque]
(** * jacm-final.pdf p.9 (585) §4.1 media 60 338 368 24 *)
type 'a regular = ['a greenDeque | 'a yellowGDeque | 'a redDeque]
end
open ColoredDequesFixup
open DequesColors
(* module DequeWithSubstack = struct
* type 'a nestedDeque = [`Some of ('a * 'a) deque]
* type ('prefix, 'substack, 'stack, 'suffix) deque = {
* prefix: 'prefix;
* substack: 'substack;
* stack: 'stack;
* suffix: 'suffix;
* }
* end
* open DequeWithSubstack *)
(* module ColoredDeques = struct
* type ('a, 'color, 'leColor) coloredDeque =
* [ `Full of ('color, 'a nestedDeque, 'leColor) deque (\* TODO: the nested deque should be a recursive type *\)
* (\* TODO: `L and `R should be merged into a single case + constructor inside, and the empty parts the info deleted *\)
* | `L of ('a buffer0, [`None], 'leColor) deque
* | `R of ('color, [`None], 'a buffer0) deque] constraint 'xyz = 'xyz (\* TODO: use constraint to allow or forbid the empty child (L/R) case for yellow. *\)
* type 'a greenDeque = [`Green of ('a, 'a green, 'a leGreen) coloredDeque]
* type 'a yellowDeque = [`Yellow of ('a, 'a yellow, 'a leYellow) coloredDeque]
* type 'a redDeque = [`Red of ('a, 'a red, 'a leRed) coloredDeque]
* end
* open ColoredDeques *)
(* (\** jacm-final.pdf p.9 (585) §4.1 media 60 230 368 48 *\)
* module ColoredDeques2 = struct
* type ('a, 'color, 'leColor, 'substack, 'stack) coloredDeque =
* [ `Full of ('color, 'substack, 'stack, 'leColor) deque]
* (\** The astute reader will notice that if the child of a deque is empty,
* then it is the first (deepest) element on the stack. Therefore, the cases
* considering that the colour of a deque is that of its only non-empty
* buffer, if its child is also empty, apply only to the first element of the
* stack. *\)
* type ('a, 'color, 'leColor, 'substack, 'stack) coloredLRDeque = [
* ('a, 'color, 'leColor, 'substack, 'stack) coloredDeque
* | `L of ('a buffer0, [`None], [`None], 'leColor) deque
* | `R of ('color, [`None], [`None], 'a buffer0) deque]
*
* (\* "Error: The type constructor yellowDeque is not yet completely defined"
* if we don't use a fixup: all expanded cases in […|…] have to be
* completely defined (or wrapped with a `X so that they need not be
* substituted) *\)
* type 'a greenDeque = ('a, 'a green, 'a leGreen, [`Yellow of 'a yellowDeque], [`Green of 'a greenDeque|`Red of 'a redDeque]) coloredDeque
* and 'a yellowDeque = ('a, 'a yellow, 'a leYellow, [`Yellow of 'a yellowDeque], [`None]) coloredDeque (\* The first deque, if it is yellow, may have a stack pointer which is not `None. *\)
* and 'a redDeque = ('a, 'a red, 'a leRed, [`Yellow of 'a yellowDeque], [`Green of 'a greenDeque]) coloredDeque
* end
* open ColoredDeques2
*
* module ColoredDequesFixup = struct
* type nonrec 'a greenDeque = [`Green of 'a greenDeque ]
* and 'a yellowDeque = [`Yellow of 'a yellowDeque]
* and 'a redDeque = [`Red of 'a redDeque ]
* end
* open ColoredDequesFixup *)
(* jacm-final.pdf p.8 / 584 §4.1 60 480 368 36 *)
@ -126,9 +212,9 @@ open ColoredDequesFixup
(* TODO: show the naïve (wrong) version here. *)
(* type ('a, 'color, 'leColor, 'nested) colored9 =
* [ `Full of ('color, 'nestedSubstack, 'nestedStack, 'leColor) deque2
* | `L of ('a buffer0, [`None], 'nestedStack, 'leColor) deque2
* | `R of ('color, [`None], 'nestedStack, 'a buffer0) deque2]
* [ `Full of ('color, 'nestedSubstack, 'nestedStack, 'leColor) deque
* | `L of ('a buffer0, [`None], 'nestedStack, 'leColor) deque
* | `R of ('color, [`None], 'nestedStack, 'a buffer0) deque]
* type 'a greenDeque = [`Green of ('a, 'a green, 'a leGreen) colored9]
* type 'a yellowDeque = [`Yellow of ('a, 'a yellow, 'a leYellow) colored9]
* type 'a redDeque = [`Red of ('a, 'a red, 'a leRed) colored9] *)