From 1bac86494b82a25bad68c7c77e353b1451b178c0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Tue, 14 Aug 2018 11:00:55 +0200 Subject: [PATCH] Forgot to have 'a * 'a in child deques, but this requires having a different constructor in cases that were unified --- deques.ml | 114 +++++++++--------------------------------------------- 1 file changed, 18 insertions(+), 96 deletions(-) diff --git a/deques.ml b/deques.ml index 61fa0f9..5761903 100644 --- a/deques.ml +++ b/deques.ml @@ -19,7 +19,7 @@ module Colors = struct 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] + type empty = buffer0 end open Colors @@ -40,111 +40,31 @@ module ColorOrder = struct end open ColorOrder -(** jacm-final.pdf p.9 (585) §4.1 media 60 134 368 36 *) +(** jacm-final.pdf p.9 (585) §4.1 media 60 146 368 24 *) module BufferColors = struct type 'a buffer = ['a green | 'a yellow | 'a red] end open BufferColors -(** jacm-final.pdf p.8 / 584 §4.1 60 408 368 48 *) +(** jacm-final.pdf p.8 (584) §4.1 media 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 - -(* If we naively translate Kaplan and Tarjan's constraints into a set of - polymorphic variants, we might end up with some variation of the following, - which describes the type of a (semi-)regular stack of deques, where the - stack's pointers are one of the fields of its elements. This first attempt - only implements a single stack of deques, not a stack of substacks (where - the elements of the stack are linked by one of two pointers). *) -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 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" - 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] - - (** * 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 DequesColors - -(* As we can see, the above translation defines the semiregular and regular - types as a variant of variants, with 10 cases in total in the - definition. Substacks will introduce a number of corner cases, and the - above definition could become a long list of those. *) -(* Instead, we choose to separate the concerns related to pairs of buffers, - substacks and stacks. Each level of the construction has its own corner - cases, which will be to some extent kept separate. We first start by - updating the definition of deques so that the stack becomes a separate, - apparent structure. *) -module DequesColorsStack = struct type ('prefix, 'substack, 'suffix) deque = { prefix: 'prefix; substack: 'substack; suffix: 'suffix} + type 'a child = 'a * 'a +end +open Deques + +module DequesColorsStack = struct (** jacm-final.pdf p.9 (585) §4.1 media 60 230 368 48 *) + (* TODO: this is ambiguous: when the colors are the same, or for the empty + cases, several constructors could be used for the same pair of + buffers. *) type ('color, 'geColor, 'substack) min = [ `LeftMin of ('color, 'substack, 'geColor) deque | `RightMin of ('geColor, 'substack, 'color) deque] @@ -153,12 +73,12 @@ module DequesColorsStack = struct | `LeftOnly of ('color, [`Nil], empty) deque | `RightOnly of ( empty, [`Nil], 'color) deque] - type 'a minTail = ('a yellow, 'a geYellow, 'a minTail) min - type ('a, 'color, 'geColor) min' = ('color, 'geColor, 'a minTail) min - type ('a, 'color, 'geColor) lastMin' = ('color, 'geColor, 'a minTail) lastMin + type 'a minTail = Deque1 of ('a yellow, 'a geYellow, 'a child minTail) min + type 'a lastMinTail = Deque2 of ('a yellow, 'a geYellow, 'a child lastMinTail) lastMin + type ('a, 'color, 'geColor) min' = ('color, 'geColor, 'a child minTail) min + type ('a, 'color, 'geColor) lastMin' = ('color, 'geColor, 'a child lastMinTail) lastMin (** jacm-final.pdf p.9 (585) §4.1 media 60 290 368 60 *) - (* TODO: move the decision just around min and lastMin, and merge min' with lastMin' *) type ('a, 'color, 'geColor, 'b_last) substack = 'result constraint 'b_last = ( 'a, 'color, 'geColor) min' * ('a, 'color, 'geColor) lastMin' @@ -169,6 +89,9 @@ module DequesColorsStack = struct type ('a, 'b_last) yellowSubstack = ('a, 'a yellow, 'a geYellow, 'b_last) substack type ('a, 'b_last) redSubstack = ('a, 'a red, 'a geRed, 'b_last) substack + (** jacm-final.pdf p.9 (585) §4.1 media 60 290 368 60 *) + (* In order to simplify the description of the types, we have separated the + outer stack from the substacks. *) type 'a gStackLast = [ `GreenStackLast of ('a, 't * 'f * 't) greenSubstack * [`Null]] type 'a yStackLast = [ `YellowStackLast of ('a, 't * 'f * 't) yellowSubstack * [`Null]] type 'a rStackLast = [ `RedStackLast of ('a, 't * 'f * 't) redSubstack * [`Null]] @@ -193,7 +116,6 @@ module DequesColorsStack = struct practice, these cases are already disjoint types, but performing their union is more readily done by defining a variant at this level. *) - (** jacm-final.pdf p.9 (585) §4.1 media 60 290 368 60 *) type 'a semiregular = ['a greenStack | 'a yellowGRStack | 'a redStack] (** jacm-final.pdf p.9 (585) §4.1 media 60 338 368 24 *) type 'a regular = ['a greenStack | 'a yellowGStack | 'a redStack]