1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
(*
//
// HX-2013-04:
// some code for use in Matt's HCSS talk in May
//
*)
(* ****** ****** *)
//
#include
"share/atspre_staload.hats"
//
(* ****** ****** *)
staload "libats/SATS/sllist.sats"
staload _ = "libats/DATS/gnode.dats"
staload _ = "libats/DATS/sllist.dats"
(* ****** ****** *)
extern
fun{
a:t0p}{b:t0p
} sllist_mapfree$fwork (x: a): b
extern
fun{
a:t0p}{b:t0p
} sllist_mapfree {n:nat} (xs: sllist (INV(a), n)): sllist (b, n)
(* ****** ****** *)
#define nil sllist_nil
#define cons sllist_cons
#define :: sllist_cons
(* ****** ****** *)
implement{a}{b}
sllist_mapfree (xs) =
(
if sllist_is_cons (xs) then let
var xs = xs
val x0 = sllist_uncons (xs)
val y0 = sllist_mapfree$fwork<a><b> (x0)
in
y0 :: sllist_mapfree<a><b> (xs)
end else let
prval () = sllist_free_nil (xs)
in
sllist_nil ()
end (* end of [if] *)
)
(* ****** ****** *)
fun test() = let
//
val out = stdout_ref
val xs = sllist_nil{int}()
val xs = 1 :: 2 :: 3 :: 4 :: 5 :: xs
val () = fprintln! (out, "xs = ", xs)
//
local
implement
sllist_mapfree$fwork<int><int> (a) = a * a
in
val xs2 = sllist_mapfree<int><int> (xs)
end
//
val () = fprintln! (out, "xs2 = ", xs2)
//
val () = sllist_free<int> (xs2)
//
in
// nothing
end // end of [test]
(* ****** ****** *)
implement main0 (argc, argv) = test()
(* ****** ****** *)
(* end of [sllist_mapfree.dats] *)
|
