Singly-linked list/Element insertion: Difference between revisions
Singly-linked list/Element insertion (view source)
Revision as of 00:22, 21 March 2022
, 2 years ago→{{header|AutoHotkey}}
(Added XPL0 example.) |
|||
Line 645:
iMagicNumber: .int 0xCCCCCCCD
</lang>
=={{header|ATS}}==
I repeated the ‘Rosetta Code linear list type’ here, so you can simply copy
the code, compile it, and run it.
Also I put the executable parts in initialization rather than the main program,
to avoid being forced to finalize the list. I felt that would be a distraction.
Notice that the insertion routine proves that the resulting list is either of
the same length as or one longer than the original list. Also there is proof
that the insertion routine will terminate.
<lang ATS>(*------------------------------------------------------------------*)
(* 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))
(* An axiom one will need: lists never have negative lengths. *)
extern praxi {vt : vt@ype}
rclist_vt_param {n : int}
(lst : !rclist_vt (vt, n)) :<prf>
[0 <= n] void
(*------------------------------------------------------------------*)
(* 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 _ = rclist_vt_param lst
val _ = find (lst, after, x)
}
(* Now let’s try it. *)
val A = 123
val B = 789
val C = 456
(* ‘var’ to make lst a mutable variable rather than a
value (‘val’). *)
var lst = rclist_vt_cons (A, rclist_vt_cons (B, rclist_vt_nil ()))
(* Do the insertion. *)
val () = rclist_int_insert (lst, A, C)
fun
loop {k : int | 0 <= k} .<k>.
(p : !rclist_vt (int, k)) : void =
case+ p of
| rclist_vt_nil () => ()
| rclist_vt_cons (head, tail) =>
begin
println! (head);
loop tail
end
prval () = rclist_vt_param lst
val () = loop lst
(*------------------------------------------------------------------*)
implement
main0 () = ()</lang>
{{out}}
<pre>$ patscc -DATS_MEMALLOC_LIBC singly_linked_list.dats && ./a.out
123
456
789</pre>
=={{header|AutoHotkey}}==
| |||