Compare commits
21 Commits
| Author | SHA1 | Date | |
|---|---|---|---|
|
7496fd2637 | ||
|
|
9c1c2a82d7 | ||
|
|
ca47c0b5a5 | ||
|
|
1bac86494b | ||
|
|
fa3ed3b3da | ||
|
|
cba1d3f867 | ||
|
|
8bb879dc16 | ||
|
|
5888eff68b | ||
|
|
0149738fd8 | ||
|
|
4071de59f7 | ||
|
|
2ddc601a3d | ||
|
|
a22715b749 | ||
|
|
1bd3cf00cd | ||
|
|
ce9e429eeb | ||
|
|
77c37cf5ac | ||
|
|
6658bdcaa6 | ||
|
|
3aa74ea869 | ||
|
|
9fdde72b51 | ||
|
|
0ba3a253ac | ||
|
|
2ff9f777cf | ||
|
|
bac59a6495 |
9
.gitignore
vendored
9
.gitignore
vendored
|
|
@ -2,3 +2,12 @@
|
|||
/deques.cmi
|
||||
/deques.cmo
|
||||
/deques.mli
|
||||
/jacm-final.pdf
|
||||
/jacm-final-page*.pdf
|
||||
/jacm-final-crop-*-*-*-*-page*.pdf
|
||||
/jacm-final-crop-*-*-*-*-page*.png
|
||||
/deques.html
|
||||
/doc
|
||||
/deques.d
|
||||
/deques.color.html
|
||||
/deques.html
|
||||
|
|
@ -1,9 +1,13 @@
|
|||
sudo: false
|
||||
language: c
|
||||
|
||||
addons:
|
||||
apt:
|
||||
packages:
|
||||
- ocaml-interp
|
||||
- ocaml
|
||||
- ocaml-findlib
|
||||
- caml2html
|
||||
- libpodofo-utils
|
||||
|
||||
script:
|
||||
- make print-tool-versions
|
||||
|
|
|
|||
66
Makefile
66
Makefile
|
|
@ -1,12 +1,70 @@
|
|||
.PHONY: all
|
||||
all: deques deques.mli Makefile
|
||||
.SECONDEXPANSION:
|
||||
|
||||
deques: deques.ml Makefile
|
||||
.PHONY: all
|
||||
all: deques deques.mli doc deques.html Makefile
|
||||
|
||||
deques: deques.ml deques.cmi Makefile
|
||||
ocamlc $< -o $@
|
||||
|
||||
deques.mli: deques.ml Makefile
|
||||
ocamlc -i $< > $@
|
||||
|
||||
deques.cmi: deques.mli Makefile
|
||||
ocamlc $< -o $@
|
||||
|
||||
re=\( *\)(\*\* jacm-final.pdf p.\([0-9]\+\) \(([0-9]\+)\) \(§[.0-9]\+\) media \([0-9]\+\) \([0-9]\+\) \([0-9]\+\) \([0-9]\+\) \*)
|
||||
deques.d: deques.ml Makefile
|
||||
(printf 'deques.html: '; sed -ne 's~^$(re)$$~jacm-final-crop-\5-\6-\7-\8-page\2.png~p' $< | tr '\n' ' ') > $@
|
||||
|
||||
-include deques.d
|
||||
|
||||
deques.color.html: deques.ml Makefile
|
||||
caml2html -charset utf-8 $< -t -o $@
|
||||
|
||||
# TODO: put this in a <style>…</style> tag
|
||||
style=style="width:63em; margin: 1.5em 0em; display: block; padding: 0.5em 0em 0.5em 1em; border-left: thick solid \#ccc;"
|
||||
|
||||
deques.html: deques.color.html Makefile
|
||||
# (echo '<!DOCTYPE html><meta http-equiv="Content-Type" content="text/html; charset=utf-8" /><title>$(<)</title><pre>'; \
|
||||
# sed -e 's~[&]~\&~' -e 's~<~\>~' -e 's~>~\<~' -e 's~"~\"~' -e "s~'~\'~" deques.ml \
|
||||
# | sed -e 's~^$(re)$$~<img style="width:63em;" src="jacm-final-crop-\5-\6-\7-\8-page\2.png" alt="jacm-final.pdf page \2 \3 \4" />~'; \
|
||||
# echo '</pre>') > $@
|
||||
sed -e 's~$(re)~<img $(style) src="jacm-final-crop-\5-\6-\7-\8-page\2.png" alt="jacm-final.pdf page \2 \3 \4" />~g' $< > $@
|
||||
|
||||
.PHONY: print-tool-versions
|
||||
print-tool-versions:
|
||||
print-tool-versions: Makefile
|
||||
ocamlc -version
|
||||
|
||||
jacm-final.pdf: Makefile
|
||||
wget http://www.math.tau.ac.il/~haimk/adv-ds-2000/jacm-final.pdf -O$@ && touch $@
|
||||
|
||||
#sudo apt-get install libpodofo-utils to get podofobox
|
||||
jacm-final-page%.pdf: jacm-final.pdf Makefile
|
||||
pdftk P=$< cat P$* output $@
|
||||
|
||||
# jacm-final-crop-LEFT-TOP-WIDTH-HEIGHT-pagePAGE.pdf
|
||||
# Original page width: 488, original page height: 721.
|
||||
# podofobox expects LEFT BOTTOM WIDTH HEIGHT, multiplied by 100.
|
||||
jacm-final-crop-%.pdf: $$(shell echo '%.pdf' | sed -e 's/^[-0-9]*-page/jacm-final-page/')
|
||||
f () { \
|
||||
podofobox $< $@ \
|
||||
media $$(( ($$1) * 100 )) \
|
||||
$$(( ( 720 - ($$2) - ($$4) ) * 100 )) \
|
||||
$$(( ($$3) * 100 )) \
|
||||
$$(( ($$4) * 100 )); \
|
||||
}; \
|
||||
f $$(echo '$*' | sed -e 's/page[0-9]*$$//' -e 's/-/ /g')
|
||||
|
||||
jacm-final-crop-%.png: jacm-final-crop-%.pdf Makefile
|
||||
convert -density 300 $< $@
|
||||
|
||||
doc: deques.ml Makefile
|
||||
git clean -dfx doc
|
||||
mkdir doc
|
||||
ocamlfind ocamldoc -html -all-params -colorize-code -charset utf-8 $< -d $@
|
||||
touch doc
|
||||
|
||||
.PHONY: clean
|
||||
clean: Makefile
|
||||
rm -- jacm-final-page*.pdf jacm-final-crop-*-page*.pdf jacm-final-crop-*-page*.png deques.html
|
||||
rm -r -- doc
|
||||
|
|
|
|||
133
deques-old.ml
Normal file
133
deques-old.ml
Normal file
|
|
@ -0,0 +1,133 @@
|
|||
(** An implementation of purely functional deques as described by Kaplan and
|
||||
Tarjan. *)
|
||||
|
||||
(** jacm-final.pdf p.8 (584) §4.1 media 60 380 368 40 *)
|
||||
module Buffers = struct
|
||||
type buffer0 = [`Buffer0]
|
||||
type 'a buffer1 = [`Buffer1 of 'a]
|
||||
type 'a buffer2 = [`Buffer2 of 'a * 'a]
|
||||
type 'a buffer3 = [`Buffer3 of 'a * 'a * 'a]
|
||||
type 'a buffer4 = [`Buffer4 of 'a * 'a * 'a * 'a]
|
||||
type 'a buffer5 = [`Buffer5 of 'a * 'a * 'a * 'a * 'a]
|
||||
end
|
||||
open Buffers
|
||||
|
||||
(** jacm-final.pdf p.9 (585) §4.1 media 60 158 368 24 *)
|
||||
module Colors = struct
|
||||
type 'a green = ['a buffer2 | 'a buffer3]
|
||||
type 'a yellow = ['a buffer1 | 'a buffer4]
|
||||
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 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]
|
||||
type 'a leRed = [ | 'a red]
|
||||
|
||||
type 'a geGreen = [ | 'a green ]
|
||||
type 'a geYellow = [ | 'a green | 'a yellow ]
|
||||
type 'a geRed = [ | 'a green | 'a yellow | 'a red]
|
||||
end
|
||||
open ColorOrder
|
||||
|
||||
(** 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 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 ('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, 'b_last) min = 'result
|
||||
constraint 'b_last = ([ `LeftMin of ('color, 'substack, 'geColor) deque
|
||||
| `RightMin of ('geColor, 'substack, 'color) deque]
|
||||
*[ `LeftMin of ('color, 'substack, 'geColor) deque
|
||||
| `RightMin of ('geColor, 'substack, 'color) deque
|
||||
| `LeftOnly of ('color, [`Nil], empty) deque
|
||||
| `RightOnly of ( empty, [`Nil], 'color) deque]
|
||||
*'result)
|
||||
(* type ('color, 'geColor, 'substack) lastMin = [
|
||||
* ('color, 'geColor, 'substack) min
|
||||
* | `LeftOnly of ('color, [`Nil], empty) deque
|
||||
* | `RightOnly of ( empty, [`Nil], 'color) deque] *)
|
||||
|
||||
type ('a, 'b_last) minTail = Deque of ('a yellow, 'a geYellow, ('a child, 'b_last1) minTail, 'b_last2) min
|
||||
constraint 'b_last = (('t1 * 'f1 * 't1) * ('t1 * 'f1 * 't1))
|
||||
*(('t1 * 'f1 * 'f1) * ('t1 * 'f1 * 'f1))
|
||||
*('b_last1 * 'b_last2)
|
||||
(* type 'a lastMinTail = Deque of ('a yellow, 'a geYellow, 'a child lastMinTail) lastMin *)
|
||||
type ('a, 'color, 'geColor, 'b_last1, 'b_last2) min' = ('color, 'geColor, ('a child, 'b_last1) minTail, 'b_last2) 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 *)
|
||||
type ('a, 'color, 'geColor, 'b_last1, 'b_last2) substack = ('a, 'color, 'geColor, 'b_last1, 'b_last2) min'
|
||||
|
||||
type ('a, 'b_last1, 'b_last2) greenSubstack = ('a, 'a green, 'a geGreen, 'b_last1, 'b_last2) substack
|
||||
(* A yellow substack can only appear as the topmost substack in a stack. *)
|
||||
type ('a, 'b_last1, 'b_last2) yellowSubstack = ('a, 'a yellow, 'a geYellow, 'b_last1, 'b_last2) substack
|
||||
type ('a, 'b_last1, 'b_last2) redSubstack = ('a, 'a red, 'a geRed, 'b_last1, 'b_last2) 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, 't1 * 'f1 * 't1, 't2 * 'f2 * 't2) greenSubstack * [`Null]]
|
||||
type 'a yStackLast = [ `YellowStackLast of ('a, 't1 * 'f1 * 't1, 't2 * 'f2 * 't2) yellowSubstack * [`Null]]
|
||||
type 'a rStackLast = [ `RedStackLast of ('a, 't1 * 'f1 * 't1, 't2 * 'f2 * 't2) redSubstack * [`Null]]
|
||||
type ('a, 'b) _gStack = [ 'a gStackLast
|
||||
| `GreenStack of ('a, 't1 * 'f1 * 'f1, 't2 * 'f2 * 'f2) greenSubstack * 'b]
|
||||
type ('a, 'b) _yStack = [ 'a yStackLast
|
||||
| `YellowStack of ('a, 't1 * 'f1 * 'f1, 't2 * 'f2 * 'f2) yellowSubstack * 'b]
|
||||
type ('a, 'b) _rStack = [ 'a rStackLast
|
||||
| `RedStack of ('a, 't1 * 'f1 * 'f1, 't2 * 'f2 * 'f2) 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
|
||||
colors: green is allways possible, but some stack elements may be
|
||||
followed by a red stack element. We therefore need to introduce
|
||||
polymorphic constructors in order to make a union of the two cases. In
|
||||
practice, these cases are already disjoint types, but performing their
|
||||
union is more readily done by defining a variant at this level. *)
|
||||
|
||||
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]
|
||||
end
|
||||
open DequesColorsStack
|
||||
|
||||
(** jacm-final.pdf p.8 (584) §4.1 media 60 480 368 36 *)
|
||||
(* let rec child i d =
|
||||
if i = 0 then d
|
||||
else child (i - 1) d.child *)
|
||||
21
deques.ml
21
deques.ml
|
|
@ -0,0 +1,21 @@
|
|||
module Buffers = struct
|
||||
type ('a, _) buffer =
|
||||
| Buffer0 : ('a, [`Red]) buffer
|
||||
| Buffer1 : 'a -> ('a, [`Yellow]) buffer
|
||||
| Buffer2 : 'a * 'a -> ('a, [`Green]) buffer
|
||||
| Buffer3 : 'a * 'a * 'a -> ('a, [`Green]) buffer
|
||||
| Buffer4 : 'a * 'a * 'a * 'a -> ('a, [`Yellow]) buffer
|
||||
| Buffer5 : 'a * 'a * 'a * 'a * 'a -> ('a, [`Red]) buffer
|
||||
end
|
||||
open Buffers
|
||||
|
||||
type 'a somebuffer =
|
||||
| Buffer : ('a, 'x) buffer -> 'a somebuffer
|
||||
type z = int somebuffer
|
||||
(* let f b = match b with
|
||||
* Buffer0 -> 42
|
||||
* | Buffer1 x -> 42
|
||||
* | Buffer2 (x, y) -> 42
|
||||
* | Buffer3 (x, y, z) -> 42
|
||||
* | Buffer4 (x, y, z, t) -> 42
|
||||
* | Buffer5 (x, y, z, t, u) -> 42 *)
|
||||
149
deques_typelevelprogramming.ml
Normal file
149
deques_typelevelprogramming.ml
Normal file
|
|
@ -0,0 +1,149 @@
|
|||
(* Unification in the HM type system, along with OCaml's constraint keyword,
|
||||
allows us to describe relations between types. The type-level functions
|
||||
below are using this in a way that is reminiscent of Prolog's
|
||||
predicates. We try to put the results on the left-hand side of the equals
|
||||
sign, even though a use of the constraint keyword establishes an unordered
|
||||
relation between two types. This explains why it is possible to write
|
||||
constraint 'x = ('hd, 'tl) push to indicate that 'x is the result, and the
|
||||
equivalent constraint ('hd, 'tl) push = 'x to indicate that 'hd and 'tl are
|
||||
expected to be extracted from a known 'x. *)
|
||||
module T = struct
|
||||
(* TODO: bundle together the stack and an on-demand infinite stack of free variables *)
|
||||
(* This should not be exported in the sig. *)
|
||||
module Private = struct
|
||||
(* stack of type-level operands *)
|
||||
type ('tl, 'hd, 'fv) _stack = Stack of 'tl * 'hd * 'fv
|
||||
type ('stack, 'freevars) _state = State of 'stack * 'freevars (* constraint 'tail = ('a,'b) state *)
|
||||
|
||||
type __start = ()
|
||||
type 'freevars _start = (__start, 'freevars) _state
|
||||
(* internal: quote a type and place it on the stack *)
|
||||
type 't _typ = Typ of 't
|
||||
type 't _polytyp = PolyTyp of 't
|
||||
|
||||
(* Push a new type-level value onto the stack *)
|
||||
(* 'fv denotes the free variables in 'v, which will be bound to a dummy
|
||||
type if the value 'v is dropped from the stack. *)
|
||||
type ('state, 'v, 'fv) _push = (('stack, 'v, 'fv) _stack, 'freevars) _state
|
||||
constraint ('stack, 'freevars) _state = 'state
|
||||
|
||||
(* fetch the value on top of the the stack and its free variables *)
|
||||
type 'state _peekv = 'v
|
||||
constraint (('stack, 'v, 'fv) _stack, 'freevars) _state = 'state
|
||||
type 'state _peekfv = 'fv
|
||||
constraint (('stack, 'v, 'fv) _stack, 'freevars) _state = 'state
|
||||
|
||||
(* drop the value on top of the the stack *)
|
||||
(* type closed_freevar = [`FreeVar of (closed_freevar * closed_freevar)] *)
|
||||
type closed_freevar1 = [`FreeVar of unit * unit]
|
||||
(* 'x serves as a handled. If is is not unified with anything, it does not
|
||||
cause any harm. If it is unified with ('u * 'u * 'v * 'v * 'w * 'w), it
|
||||
causes three pairs of types to unify, thereby closing a local type
|
||||
variable and propagating that close order down to the two children. *)
|
||||
type 'dummy close_freevars = ('u * 'u * 'v * 'v * 'w * 'w) constraint ('u * 'v * 'w) = 'dummy
|
||||
type ('a, 'x) _fv = [`FreeVar of 'a * 'x]
|
||||
constraint ( 'a * closed_freevar1
|
||||
* unit * unit (* ignored *)
|
||||
* unit * unit (* ignored *)) = 'x
|
||||
type ('a, 'b, 'x) _fvs = [`FreeVar of ('a * 'b) * 'x]
|
||||
constraint ( unit * unit (* ignored *)
|
||||
* 'a * [`FreeVar of 'one * 'dummy1 close_freevars]
|
||||
* 'b * [`FreeVar of 'two * 'dummy2 close_freevars]) = 'x
|
||||
(*TODO: possibly need to bind: 'one 'two 'dummy1 'dummy2 *)
|
||||
type no_freevar = closed_freevar1
|
||||
type 'state _pop = ('tail, 'freevars) _state
|
||||
constraint (('tail, 'v, 'fv) _stack, 'freevars) _state = 'state
|
||||
type 'state _discard = ('tail, 'freevars) _state
|
||||
constraint (('tail, 'v, 'fv) _stack, 'freevars) _state = 'state
|
||||
constraint 'fv = [`FreeVar of 'fv_ * 'dummy close_freevars]
|
||||
end
|
||||
open Private
|
||||
|
||||
(* Instantiate a new free variable. *)
|
||||
type ('state, 'freevar) _freevar = ('stack, 'new_freevars) _state
|
||||
constraint ('stack, 'freevars) _state = 'state
|
||||
constraint 'new_freevars * 'freevar = 'freevars
|
||||
|
||||
(* Unwrap the single element on the stack. *)
|
||||
type 'state return = 'returned
|
||||
constraint 'state = ((__start, 'returned _typ, 'fvs) _stack, closed_freevar1) _state
|
||||
constraint 'fvs = [`FreeVar of 'fvs_ * 'dummy close_freevars]
|
||||
|
||||
(* Quote a type and place it on the stack. *)
|
||||
type ('state, 't) typ = (('stack, 't _typ, no_freevar) _stack, 'freevars) _state
|
||||
constraint ('stack, 'freevars) _state = 'state
|
||||
|
||||
(* Quote a polymorphic type and place it on the stack. *)
|
||||
(* 'x should be a free variable on the caller's site,
|
||||
'xt should be 'x t where t is the polymorphic type to quote. *)
|
||||
type ('state, 'x, 'xt) polytyp = (('stack, ('xt * 'x) _polytyp, ('x, 'fv) _fv) _stack, 'freevars) _state
|
||||
constraint ('stack, 'freevars) _state = ('state, 'x * 'fv) _freevar
|
||||
|
||||
(* type-level booleans *)
|
||||
type 'state tru = ('state2, ('a * 'b * 'a * 'b), (('a, 'fva) _fv, ('b, 'fvb) _fv, 'fvab) _fvs) _push
|
||||
constraint 'state2 = ('state, 'a * 'b * 'fva * 'fvb * 'fvab) _freevar
|
||||
type 'state fals = ('state2, ('a * 'b * 'b * 'a), (('a, 'fva) _fv, ('b, 'fvb) _fv, 'fvab) _fvs) _push
|
||||
constraint 'state2 = ('state, 'a * 'b * 'fva * 'fvb * 'fvab) _freevar
|
||||
|
||||
type ('x, 'y) _cons = Cons of 'x * 'y
|
||||
type 'state cons = ('state2 _pop _pop,
|
||||
('state2 _pop _peekv, 'state2 _peekv) _cons,
|
||||
('state2 _pop _peekfv, 'state2 _peekfv, 'fv) _fvs) _push
|
||||
constraint 'state2 = ('state, 'fv) _freevar
|
||||
type 'state uncons = (('state _pop, 'x, 'fvx) _push, 'y, 'fvy) _push
|
||||
constraint ('x, 'y) _cons = 'state _peekv
|
||||
constraint ('fvx, 'fvy, 'fvxy) _fvs = 'state _peekfv
|
||||
constraint 'fvxy = ( unit * unit (* ignored *)
|
||||
* 'a * [`FreeVar of 'one * 'dummy1 close_freevars]
|
||||
* 'b * [`FreeVar of 'two * 'dummy2 close_freevars])
|
||||
|
||||
(* type-level conditional *)
|
||||
type 'state ifelse = (('tail, 'tresult, 'fvr) _stack, 'freevars) _state
|
||||
constraint 'state = (((('tail, 'tcondition, 'fvc) _stack, 'tthen, 'fvt) _stack, 'telse, 'fve) _stack, 'freevars) _state
|
||||
constraint 'tcondition = ([`v_fv of 'tthen * 'fvt])
|
||||
* ([`v_fv of 'telse * 'fve])
|
||||
* ([`v_fv of 'tresult * 'fvr])
|
||||
* ([`v_fv of 'tdiscard * 'fvd])
|
||||
(* Since the discarded value may contain some free variables, we need to
|
||||
bind them to some dummy value. *)
|
||||
constraint 'fvd = [`FreeVar of 'fvd_ * 'dummy close_freevars]
|
||||
constraint 'fvc = [`FreeVar of 'fvab * 'x]
|
||||
constraint 'x = unit (* release the 'x of 'fvc, since the condition was used *)
|
||||
|
||||
(* type-level duplication of a boolean
|
||||
|
||||
We prefer not to allow duplication of a quoted type, as there would be no
|
||||
way to avoid using the same polymorphic variables in both occurrences. *)
|
||||
type 'state dup = 'state tru tru cons fals fals cons ifelse uncons
|
||||
type 'state exch = (('state _pop _pop, 'state _peekv, 'state _peekfv) _push, 'state _pop _peekv, 'state _pop _peekfv) _push
|
||||
type 'state pop = 'state _discard
|
||||
|
||||
(* apply a single-argument polymorphic type to an argument *)
|
||||
type 'state polyapp = 'result
|
||||
(* left-hand-side of product type is output, right-hand-side is input *)
|
||||
constraint ('result * ('state _pop)) _polytyp = 'state _peekv
|
||||
|
||||
(* type 'x push = 'a * 'b constraint 'x = 'a * 'b *)
|
||||
(* type ('tcondition, 'tthen, 'telse) ifelse = 'tresult constraint 'tcondition = 'tthen * 'telse * 'tresult *)
|
||||
|
||||
type 'state typ_string = ('state, string) typ
|
||||
type 'state typ_int = ('state, int) typ
|
||||
type 'state typ_unit = ('state, unit) typ
|
||||
end
|
||||
|
||||
module TypeLevelFunctionsExamples = struct
|
||||
open T
|
||||
|
||||
type 'state s = 'state typ_string typ_int ifelse return
|
||||
type s1 = 't tru s (* push true on the stack, call s => string *)
|
||||
type s2 = 't fals s (* push false on the stack, call s => int *)
|
||||
|
||||
type 'state f = 'state tru typ_string
|
||||
type 'state t = 'state polyapp typ_int ifelse return
|
||||
type 'state push_f = ('state, 'x, 'x f) polytyp
|
||||
type t1 = 't push_f t (* => string *)
|
||||
|
||||
type 'state u = 'state dup typ_int typ_string ifelse typ_unit exch ifelse return
|
||||
type u1 = 't tru u
|
||||
type u2 = 't fals u
|
||||
end
|
||||
Loading…
Reference in New Issue
Block a user