Singly-linked list/Traversal: Difference between revisions

=={{header|ATS}}==

<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))

(* 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 traverse-and-print

routine will be specifically for lists of ‘int’. *)

(* Some things that will be needed. *)

#include "share/atspre_staload.hats"

(* The list is passed by value and will be preserved with the same

type. *)

extern fun

rclist_int_traverse_and_print

{m : int} (* ‘for all list lengths m’ *)

(lst : !rclist_vt (int, m) >> (* ! = pass by value *)

(* The new type will be the same as the old

type. *)

rclist_vt (int, m)) : void

implement

rclist_int_traverse_and_print {m} (lst) =

{

(* A recursive nested function that traverses the list, printing

elements along the way. *)

fun

traverse {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) >> rclist_vt (int, k)) :

void =

case+ lst of

| rclist_vt_nil () => () (* End of list. *)

| rclist_vt_cons (head, tail) =>

begin

println! (head);

traverse tail

end

(* The following is needed to prove that the initial k above

satisfies 0 <= k. *)

prval _ = lemma_rclist_vt_param lst

val _ = traverse lst

}

(* Now let’s try it. *)

(* Some convenient notation. *)

#define NIL rclist_vt_nil ()

#define :: rclist_vt_cons

overload traverse_and_print with rclist_int_traverse_and_print

val A = 123

val B = 789

val C = 456

val lst = A :: C :: B :: NIL

val () = traverse_and_print lst

(*------------------------------------------------------------------*)

implement

main0 () = ()</lang>