Skip to content

Commit 66491d9

Browse files
ashalkhakovashalkhakov
committed
Adding doubly-linked circular lists (ngc-style).
1 parent b8542b3 commit 66491d9

File tree

5 files changed

+469
-2
lines changed

5 files changed

+469
-2
lines changed

‎DATS/dlist.dats

Lines changed: 172 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,172 @@
1+
(* ****** ****** *)
2+
3+
staload "../SATS/dlist.sats"
4+
5+
(* ****** ****** *)
6+
//
7+
implement{}
8+
fprint_dlfcircular$sep (out) = fprint (out, ", ")
9+
//
10+
implement{}
11+
fprint_dlfcircular {n} {l} (pf_dlfc | out, p) = let
12+
//
13+
fun
14+
loop {n:nat} {lf:agz;lfn,lp,lr,lrn:addr} (
15+
pf_at: !dlnode_v (lf, lp, lfn)
16+
, pf_fseg: !dlfseg_v (n, lfn, lf, lr, lrn)
17+
| p: ptr lf
18+
, prn: ptr lrn
19+
, out: FILEref
20+
) : void = let
21+
//
22+
val pn = dlnode_ptr_next (pf_at | p)
23+
//
24+
val () = fprint_dlnode_ptr (pf_at | out, p)
25+
//
26+
prval () = dlfseg_lemma3 (pf_fseg)
27+
//
28+
in
29+
//
30+
if pn = prn then let
31+
prval dlfseg_v_nil () = pf_fseg
32+
prval () = pf_fseg := dlfseg_v_nil ()
33+
in
34+
(*void*)
35+
end else let
36+
val () = fprint_dlfcircular$sep<> (out)
37+
prval dlfseg_v_cons (pf1_at, pf1_fseg) = pf_fseg
38+
prval () = dlnode_ptr_is_gtz (pf1_at)
39+
val () = loop (pf1_at, pf1_fseg | pn, prn, out)
40+
prval () = pf_fseg := dlfseg_v_cons (pf1_at, pf1_fseg)
41+
in
42+
(*void*)
43+
end
44+
//
45+
end // end of [loop]
46+
//
47+
in
48+
//
49+
if p = the_null_ptr then let
50+
//
51+
prval dlfcircular_v_none () = pf_dlfc
52+
prval () = pf_dlfc := dlfcircular_v_none ()
53+
//
54+
in (*void*) end
55+
else let
56+
//
57+
prval dlfcircular_v_some (pf_hd, pf_fseg) = pf_dlfc
58+
val () = loop (pf_hd, pf_fseg | p, p, out)
59+
prval () = pf_dlfc := dlfcircular_v_some (pf_hd, pf_fseg)
60+
//
61+
in (*void*) end // end of [if]
62+
//
63+
end // end of [fprint_dlfcircular]
64+
//
65+
implement{}
66+
fprint_dlfcircular_sep {n} {l} (
67+
pf_dlfc
68+
| out: FILEref
69+
, p
70+
, sep
71+
) = let
72+
//
73+
implement
74+
fprint_dlfcircular$sep<> (out) = fprint (out, sep)
75+
//
76+
in
77+
fprint_dlfcircular (pf_dlfc | out, p)
78+
end // end of [fprint_dlfcircular_sep]
79+
//
80+
(* ****** ****** *)
81+
82+
implement
83+
dlfcircular_ptr_length {n} {l} (pf_dlfc | p) = let
84+
//
85+
fun
86+
loop {n,acc:nat} {lf:agz;lfn,lp,lr,lrn:addr} (
87+
pf_at: !dlnode_v (lf, lp, lfn)
88+
, pf_fseg: !dlfseg_v (n, lfn, lf, lr, lrn)
89+
| p: ptr lf
90+
, prn: ptr lrn
91+
, acc: int acc
92+
) : int (acc+n) = let
93+
//
94+
val pn = dlnode_ptr_next (pf_at | p)
95+
prval () = dlfseg_lemma3 (pf_fseg)
96+
//
97+
in
98+
//
99+
if pn = prn then let
100+
prval dlfseg_v_nil () = pf_fseg
101+
prval () = pf_fseg := dlfseg_v_nil ()
102+
in
103+
acc
104+
end else let
105+
prval dlfseg_v_cons (pf1_at, pf1_fseg) = pf_fseg
106+
prval () = dlnode_ptr_is_gtz (pf1_at)
107+
val res = loop (pf1_at, pf1_fseg | pn, prn, acc+1)
108+
prval () = pf_fseg := dlfseg_v_cons (pf1_at, pf1_fseg)
109+
in
110+
res
111+
end
112+
//
113+
end // end of [loop]
114+
//
115+
in
116+
//
117+
if p = the_null_ptr then let
118+
//
119+
prval dlfcircular_v_none () = pf_dlfc
120+
prval () = pf_dlfc := dlfcircular_v_none ()
121+
//
122+
in 0 end
123+
else let
124+
//
125+
prval dlfcircular_v_some (pf_hd, pf_fseg) = pf_dlfc
126+
val res = loop (pf_hd, pf_fseg | p, p, 1)
127+
prval () = pf_dlfc := dlfcircular_v_some (pf_hd, pf_fseg)
128+
//
129+
in res end // end of [if]
130+
//
131+
end // end of [dlfcircular_ptr_length]
132+
133+
(* ****** ****** *)
134+
135+
implement
136+
dlfcircular_ptr_free {n} {l} (pf_dlfc | p) = let
137+
//
138+
fun
139+
loop {n:nat} {lf:agz;lfn,lp,lr,lrn:addr} (
140+
pf_at: dlnode_v (lf, lp, lfn)
141+
, pf_fseg: dlfseg_v (n, lfn, lf, lr, lrn)
142+
| p: ptr lf
143+
, prn: ptr lrn
144+
) : void = let
145+
//
146+
val pn = dlnode_ptr_next (pf_at | p)
147+
val () = dlnode_ptr_free (pf_at | p)
148+
prval () = dlfseg_lemma3 (pf_fseg)
149+
//
150+
in
151+
if pn = prn then let
152+
prval dlfseg_v_nil () = pf_fseg
153+
in
154+
(*void*)
155+
end else let
156+
prval dlfseg_v_cons (pf1_at, pf1_fseg) = pf_fseg
157+
prval () = dlnode_ptr_is_gtz (pf1_at)
158+
in
159+
loop (pf1_at, pf1_fseg | pn, prn)
160+
end
161+
end // end of [loop]
162+
//
163+
in
164+
if p = the_null_ptr then let
165+
prval dlfcircular_v_none () = pf_dlfc
166+
in (*void*) end else let
167+
prval dlfcircular_v_some (pf_hd, pf_fseg) = pf_dlfc
168+
in
169+
loop (pf_hd, pf_fseg | p, p)
170+
end // end of [if]
171+
end // end of [dlfcircular_ptr_free]
172+

‎SATS/dlist.sats

Lines changed: 171 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,171 @@
1+
(* ****** ****** *)
2+
3+
#include
4+
"share/atspre_staload.hats"
5+
6+
(* ****** ****** *)
7+
//
8+
sortdef t0p = t@ype
9+
sortdef vt0p = viewt@ype
10+
//
11+
(* ****** ****** *)
12+
//
13+
absview
14+
dlnode_v (
15+
l: addr, lp: addr, ln: addr // lp: previous; ln: next
16+
) // end of [dlnode_v]
17+
//
18+
prfun
19+
dlnode_ptr_is_gtz
20+
{l,lp,ln:addr}
21+
(pf: !dlnode_v (l, lp, ln)): [l > null] void
22+
// end of [dlnode_ptr_is_gtz]
23+
//
24+
(* ****** ****** *)
25+
//
26+
dataview
27+
dlfseg_v (
28+
int(*len*)
29+
, addr(*leftmost*)
30+
, addr(*prev of leftmost*)
31+
, addr(*rightmost*)
32+
, addr(*next of rightmost*)
33+
) =
34+
| {n:nat}
35+
{lf,lfp:addr}
36+
{lr,lrn:addr}
37+
{lfn:addr}
38+
dlfseg_v_cons (n+1, lf, lfp, lr, lrn) of (
39+
dlnode_v (lf, lfp, lfn), dlfseg_v (n, lfn, lf, lr, lrn)
40+
) // end of [dlfseg_v_cons]
41+
| {lf:addr}
42+
{lr:addr}
43+
// why is this cyclic??? lf, lr, lr, lf?
44+
// because it's a segment! a segment is a portion of a list
45+
dlfseg_v_nil (0, lf, lr, lr, lf) of ()
46+
// end of [dlfseg_v]
47+
48+
// NOTE: unproven, because to show this, we'd have to always assume and check
49+
// that at-proofs don't alias (and they don't!)
50+
prfun
51+
dlfseg_lemma3 {n:nat} {lf,lfp,lr,lrn:addr} (
52+
pf_dl: !dlfseg_v (n, lf, lfp, lr, lrn)
53+
):<> [n == 0 && lf == lrn || n > 0 && lf != lrn] void
54+
(*
55+
primplement dlfseg_lemma3 {n} {lf,lfp,lr,lrn} (pf_dl) =
56+
case pf_dl of
57+
| dlfseg_v_nil () => let val () = pf_dl := dlfseg_v_nil () in end
58+
| dlfseg_v_cons (pf_at, pf1_dl) => let val () = pf_dl := dlfseg_v_cons (pf_at, pf1_dl) in end
59+
*)
60+
(* ****** ****** *)
61+
62+
dataview
63+
dlrseg_v (
64+
int(*size*)
65+
, addr(*leftmost*)
66+
, addr(*prev of leftmost*)
67+
, addr(*rightmost*)
68+
, addr(*next of rightmost*)
69+
) =
70+
| {n:nat}
71+
{lf,lfp:addr}
72+
{lr,lrn:addr}
73+
{lrp:addr}
74+
dlrseg_v_cons (n+1, lf, lfp, lr, lrn) of (
75+
dlrseg_v (n, lf, lfp, lrp, lr), dlnode_v (lr, lrp, lrn)
76+
) // end of [dlrseg_v_cons]
77+
| {lf:addr}
78+
{lr:addr}
79+
dlrseg_v_nil (0, lf, lr, lr, lf) of ()
80+
// end of [dlrseg_v]
81+
82+
(* ****** ****** *)
83+
84+
// API?
85+
// - insert new node after head, or before head
86+
// - fmap (forward or backwards)
87+
// - iterator (begin/end ptrs)
88+
// - deep copy
89+
// - circular list to array and vice versa
90+
// - is_empty, pop front, pop back, takeout the head node for mutation
91+
// - length
92+
// - find first that satisfies a predicate
93+
// - concat two circular lists
94+
// http://www.dcs.bbk.ac.uk/~trevor/FoC/NOTES/notes1%20lists%20p9_13.pdf
95+
96+
// next: what about singly-linked lists? these could also get a similar treatment!
97+
// library of pointer-linked data structures for ATS! also giving users complete
98+
// control over memory layout (this should be QUITE useful for gaming/simulation)
99+
100+
// what about e.g. portals-cells?
101+
// - cells are nodes of a graph
102+
// - portals are arcs connecting two cells
103+
// how to represent that?
104+
// - there can be MANY references to a cell...
105+
106+
(* ****** ****** *)
107+
108+
// forward-navigating circular list: either NULL, or a head element
109+
// followed by up to N elements, ending at the head
110+
dataview dlfcircular_v (int, addr) =
111+
| {n:nat}
112+
{lf:agz;lfn,lr:addr}
113+
dlfcircular_v_some (n+1, lf) of (
114+
dlnode_v (lf, lr, lfn)
115+
, dlfseg_v (n, lfn, lf, lr, lf)
116+
) (* end of [dlcircular_v_some] *)
117+
| dlfcircular_v_none (0, null)
118+
119+
(* ****** ****** *)
120+
// functions that every client must implement
121+
122+
// NOTE: this should actually be moved somewhere else, we should not
123+
// dictate to clients the memory layout of the node
124+
vtypedef dlnode0_vt = @{x=int, p=ptr null, n=ptr null}?
125+
vtypedef dlnode_vt (lp:addr, ln:addr) = @{x=int, p=ptr lp, n=ptr ln}
126+
127+
fun dlnode_alloc ():<> [l:addr] (dlnode0_vt @ l, mfree_gc_v (l) | ptr l)
128+
fun dlnode_init {l,lp,ln:addr} (
129+
mfree_gc_v (l), dlnode0_vt @ l
130+
| ptr l, int, ptr lp, ptr ln
131+
): (dlnode_v (l, lp, ln) | void)
132+
fun dlnode_free {l:addr} (pfgc: mfree_gc_v (l), pfat: dlnode0_vt @ l | p: ptr l):<> void
133+
//
134+
fun
135+
dlnode_ptr_next {l,lp,ln:addr} (!dlnode_v (l, lp, ln) | ptr l): ptr ln
136+
fun
137+
dlnode_ptr_prev {l,lp,ln:addr} (!dlnode_v (l, lp, ln) | ptr l): ptr lp
138+
fun
139+
dlnode_ptr_value {l,lp,ln:addr} (!dlnode_v (l, lp, ln) | ptr l): int
140+
//
141+
fun
142+
dlnode_ptr_free {l,lp,ln:addr} (dlnode_v (l, lp, ln) | ptr l): void
143+
//
144+
fun
145+
fprint_dlnode_ptr {l,lp,ln:addr} (!dlnode_v (l, lp, ln) | FILEref, ptr l): void
146+
//
147+
(* ****** ****** *)
148+
// functions provided by the library
149+
150+
//
151+
fun{}
152+
fprint_dlfcircular$sep (out: FILEref): void
153+
//
154+
fun{}
155+
fprint_dlfcircular {n:int} {l:addr} (!dlfcircular_v (n, l) | out: FILEref, ptr l): void
156+
//
157+
fun{}
158+
fprint_dlfcircular_sep {n:int} {l:addr}
159+
(
160+
!dlfcircular_v (n, l)
161+
| out: FILEref
162+
, ptr l
163+
, sep: NSH(string)
164+
) : void // end of [fprint_dlfcircular_sep]
165+
//
166+
fun
167+
dlfcircular_ptr_length {n:int} {l:addr} (!dlfcircular_v (n, l) | ptr l): int n
168+
//
169+
fun
170+
dlfcircular_ptr_free {n:int} {l:addr} (dlfcircular_v (n, l) | ptr l): void
171+
//

‎TEST/Makefile_dlist

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
#
2+
# A simple Makefile
3+
#
4+
5+
######
6+
7+
include $(PATSHOME)/share/atsmake-pre.mk
8+
9+
######
10+
11+
MYTARGET=MYTARGET
12+
MYCCRULE=MYCCRULE
13+
14+
######
15+
16+
include $(PATSHOME)/share/atsmake-post.mk
17+
18+
######
19+
20+
all:: \
21+
test-dlist
22+
test-dlist: test-dlist.dats ; \
23+
$(PATSCC2) -cleanaft -DATS_MEMALLOC_LIBC -o $@ $<
24+
regress:: test-dlist ; ./$<
25+
cleanall:: ; $(RMF) test-dlist
26+
27+
######
28+
29+
testall:: all
30+
testall:: regress
31+
testall:: cleanall
32+
33+
######
34+
35+
###### end of [Makefile] ######

0 commit comments

Comments
 (0)