Traverse from the beginning of a singly-linked list to the end.



See also

 Array
 Associative array: Creation, Iteration
 Collections
 Compound data type
 Doubly-linked list: Definition, Element definition, Element insertion, List Traversal, Element Removal
 Linked list
 Queue: Definition, Usage
 Set
 Singly-linked list: Element definition, Element insertion, List Traversal, Element Removal
 Stack


(*------------------------------------------------------------------*)
 
(* 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 () = ()