118 lines
3.6 KiB
Text
118 lines
3.6 KiB
Text
|
(*------------------------------------------------------------------*)
|
|||
|
|
|
|||
|
|
(* The Rosetta Code linear list type can contain any vt@ype.
|
|||
|
|
(The ‘@’ means it doesn’t have to be the size of a pointer.
|
|||
|
|
You can read {0 <= n} as ‘for all non-negative n’. *)
|
|||
|
|
dataviewtype rclist_vt (vt : vt@ype+, n : int) =
|
|||
|
|
| rclist_vt_nil (vt, 0)
|
|||
|
|
| {0 <= n} rclist_vt_cons (vt, n + 1) of (vt, rclist_vt (vt, n))
|
|||
|
|
|
|||
|
|
(* A lemma one will need: lists never have negative lengths. *)
|
|||
|
|
extern prfun {vt : vt@ype}
|
|||
|
|
lemma_rclist_vt_param
|
|||
|
|
{n : int}
|
|||
|
|
(lst : !rclist_vt (vt, n)) :<prf> [0 <= n] void
|
|||
|
|
|
|||
|
|
(* Proof of the lemma. *)
|
|||
|
|
primplement {vt}
|
|||
|
|
lemma_rclist_vt_param lst =
|
|||
|
|
case+ lst of
|
|||
|
|
| rclist_vt_nil () => ()
|
|||
|
|
| rclist_vt_cons _ => ()
|
|||
|
|
|
|||
|
|
(*------------------------------------------------------------------*)
|
|||
|
|
|
|||
|
|
(* For simplicity, the Rosetta Code linear list insertion routine will
|
|||
|
|
be specifically for lists of ‘int’. We shall not take advantage of
|
|||
|
|
the template system. *)
|
|||
|
|
|
|||
|
|
(* Some things that will be needed. *)
|
|||
|
|
#include "share/atspre_staload.hats"
|
|||
|
|
|
|||
|
|
(* The list is passed by reference and will be replaced by the new
|
|||
|
|
list. The old list is invalidated. *)
|
|||
|
|
extern fun
|
|||
|
|
rclist_int_insert
|
|||
|
|
{m : int} (* ‘for all list lengths m’ *)
|
|||
|
|
(lst : &rclist_vt (int, m) >> (* & = pass by reference *)
|
|||
|
|
(* The new type will be a list of the same
|
|||
|
|
length (if no match were found) or a list
|
|||
|
|
one longer. *)
|
|||
|
|
[n : int | n == m || n == m + 1]
|
|||
|
|
rclist_vt (int, n),
|
|||
|
|
after : int,
|
|||
|
|
x : int) :<!wrt> void
|
|||
|
|
|
|||
|
|
implement
|
|||
|
|
rclist_int_insert {m} (lst, after, x) =
|
|||
|
|
{
|
|||
|
|
(* A recursive nested function that finds the matching element
|
|||
|
|
and inserts the new node. *)
|
|||
|
|
fun
|
|||
|
|
find {k : int | 0 <= k}
|
|||
|
|
.<k>. (* Means: ‘k must uniformly decrease towards zero.’
|
|||
|
|
If so, that is proof that ‘find’ terminates. *)
|
|||
|
|
(lst : &rclist_vt (int, k) >>
|
|||
|
|
[j : int | j == k || j == k + 1]
|
|||
|
|
rclist_vt (int, j),
|
|||
|
|
after : int,
|
|||
|
|
x : int) :<!wrt> void =
|
|||
|
|
case+ lst of
|
|||
|
|
| rclist_vt_nil () => () (* Not found. Do nothing *)
|
|||
|
|
| @ rclist_vt_cons (head, tail) when head = after =>
|
|||
|
|
{
|
|||
|
|
val _ = tail := rclist_vt_cons (x, tail)
|
|||
|
|
prval _ = fold@ lst (* I need this unfolding and refolding
|
|||
|
|
stuff to make ‘tail’ a reference
|
|||
|
|
rather than a value, so I can
|
|||
|
|
assign to it. *)
|
|||
|
|
}
|
|||
|
|
| @ rclist_vt_cons (head, tail) =>
|
|||
|
|
{
|
|||
|
|
val _ = find (tail, after, x)
|
|||
|
|
prval _ = fold@ lst
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
(* The following is needed to prove that the initial k above
|
|||
|
|
satisfies 0 <= k. *)
|
|||
|
|
prval _ = lemma_rclist_vt_param lst
|
|||
|
|
|
|||
|
|
val _ = find (lst, after, x)
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
(* Now let’s try it. *)
|
|||
|
|
|
|||
|
|
(* Some convenient notation. *)
|
|||
|
|
#define NIL rclist_vt_nil ()
|
|||
|
|
#define :: rclist_vt_cons
|
|||
|
|
overload insert with rclist_int_insert
|
|||
|
|
|
|||
|
|
val A = 123
|
|||
|
|
val B = 789
|
|||
|
|
val C = 456
|
|||
|
|
|
|||
|
|
(* ‘var’ to make lst a mutable variable rather than a
|
|||
|
|
value (‘val’). *)
|
|||
|
|
var lst = A :: B :: NIL
|
|||
|
|
|
|||
|
|
(* Do the insertion. *)
|
|||
|
|
val () = insert (lst, A, C)
|
|||
|
|
|
|||
|
|
fun
|
|||
|
|
loop {k : int | 0 <= k} .<k>.
|
|||
|
|
(p : !rclist_vt (int, k)) : void =
|
|||
|
|
case+ p of
|
|||
|
|
| NIL => ()
|
|||
|
|
| head :: tail =>
|
|||
|
|
begin
|
|||
|
|
println! (head);
|
|||
|
|
loop tail
|
|||
|
|
end
|
|||
|
|
prval () = lemma_rclist_vt_param lst
|
|||
|
|
val () = loop lst
|
|||
|
|
|
|||
|
|
(*------------------------------------------------------------------*)
|
|||
|
|
|
|||
|
|
implement
|
|||
|
|
main0 () = ()
|