This commit is contained in:
Georges Dupéron 2018-08-11 23:26:46 +02:00
parent 8bb879dc16
commit cba1d3f867

View File

@ -139,33 +139,52 @@ open DequesColors
updating the definition of deques so that the stack becomes a separate, updating the definition of deques so that the stack becomes a separate,
apparent structure. *) apparent structure. *)
module DequesColorsStack = struct module DequesColorsStack = struct
type ('prefix, 'suffix) deque = { type ('prefix, 'substack, 'suffix) deque = {
prefix: 'prefix; prefix: 'prefix;
suffix: 'suffix; substack: 'substack;
} suffix: 'suffix}
(** jacm-final.pdf p.9 (585) §4.1 media 60 230 368 48 *) (** jacm-final.pdf p.9 (585) §4.1 media 60 230 368 48 *)
type ('color, 'geColor) min = [ type ('color, 'geColor, 'substack) min = [
`LeftMin of ('color, 'geColor) deque `LeftMin of ('color, 'substack, 'geColor) deque
| `RightMin of ('geColor, 'color) deque | `RightMin of ('geColor, 'substack, 'color) deque]
] type ('color, 'geColor, 'substack) lastMin = [
type ('color, 'geColor) lastMin = [ ('color, 'geColor, 'substack) min
('color, 'geColor) min | `LeftOnly of ('color, [`Nil], empty) deque
| `LeftOnly of ('color, empty) deque | `RightOnly of ( empty, [`Nil], 'color) deque]
| `RightOnly of ( empty, '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
(* TODO: use a functor to fill in the <min> part which should be min or lastMin *)
(** jacm-final.pdf p.9 (585) §4.1 media 60 290 368 60 *) (** jacm-final.pdf p.9 (585) §4.1 media 60 290 368 60 *)
type 'a greenDeque = ('a green, 'a geGreen) min (* TODO: move the decision just around min and lastMin, and merge min' with lastMin' *)
type 'a yellowDeque = ('a yellow, 'a geYellow) min type ('a, 'color, 'geColor, 'b_last) substack = 'result
type 'a redDeque = ('a red, 'a geRed) min constraint 'b_last = ( 'a, 'color, 'geColor) min'
* ('a, 'color, 'geColor) lastMin'
* 'result
type 'a tailSubStack = [`Cons of 'a yellowDeque * 'a tailSubStack] type ('a, 'b_last) greenSubstack = ('a, 'a green, 'a geGreen, 'b_last) substack
type ('hd, 'a) subStack = [`Cons of 'hd * 'a tailSubStack]
type 'a greenSubStack = ('a greenDeque, 'a) subStack
(* A yellow substack can only appear as the topmost substack in a stack. *) (* A yellow substack can only appear as the topmost substack in a stack. *)
type 'a yellowSubStack = ('a yellowDeque, 'a) subStack type ('a, 'b_last) yellowSubstack = ('a, 'a yellow, 'a geYellow, 'b_last) substack
type 'a redSubStack = ('a redDeque, 'a) subStack type ('a, 'b_last) redSubstack = ('a, 'a red, 'a geRed, 'b_last) substack
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]]
type ('a, 'b) _gStack = [ 'a gStackLast
| `GreenStack of ('a, 't * 'f * 'f) greenSubstack * 'b]
type ('a, 'b) _yStack = [ 'a yStackLast
| `YellowStack of ('a, 't * 'f * 'f) yellowSubstack * 'b]
type ('a, 'b) _rStack = [ 'a rStackLast
| `RedStack of ('a, 't * 'f * 'f) redSubstack * 'b]
type ('a, 'b, 'c) _grStack = [('a, 'b) _gStack | ('a, 'c) _rStack]
type 'a greenStack = ('a, 'a greenOrRedStack) _gStack
and 'a yellowGStack = ('a, 'a greenStack) _yStack
and 'a yellowGRStack = ('a, 'a greenOrRedStack) _yStack
and 'a redStack = ('a, 'a redStack) _rStack
and 'a greenOrRedStack = ('a, 'a greenOrRedStack, 'a redStack) _grStack
(* Contrarily to substacks, the tail of a stack may start with different (* Contrarily to substacks, the tail of a stack may start with different
colors: green is allways possible, but some stack elements may be colors: green is allways possible, but some stack elements may be
@ -173,19 +192,6 @@ module DequesColorsStack = struct
polymorphic constructors in order to make a union of the two cases. In polymorphic constructors in order to make a union of the two cases. In
practice, these cases are already disjoint types, but performing their practice, these cases are already disjoint types, but performing their
union is more readily done by defining a variant at this level. *) union is more readily done by defining a variant at this level. *)
module ToFixup = struct
type 'a gStackTail = [`GreenStack of 'a greenStack | `Null]
and 'a gRStackTail = [`GreenStack of 'a greenStack | `RedStack of 'a redStack | `Null]
and 'a greenStack = 'a greenSubStack * 'a gRStackTail
and 'a yellowGStack = 'a yellowSubStack * 'a gStackTail
and 'a yellowGRStack = 'a yellowSubStack * 'a gRStackTail
and 'a redStack = 'a redSubStack * 'a gStackTail
end
open ToFixup
type nonrec 'a greenStack = [`GreenStack of 'a greenStack]
type nonrec 'a yellowGStack = [`YellowStack of 'a yellowGStack]
type nonrec 'a yellowGRStack = [`YellowStack of 'a yellowGRStack]
type nonrec 'a redStack = [`RedStack of 'a redStack]
(** * jacm-final.pdf p.9 (585) §4.1 media 60 290 368 60 *) (** * jacm-final.pdf p.9 (585) §4.1 media 60 290 368 60 *)
type 'a semiregular = ['a greenStack | 'a yellowGRStack | 'a redStack] type 'a semiregular = ['a greenStack | 'a yellowGRStack | 'a redStack]