85 lines
2.5 KiB
Text
85 lines
2.5 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 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 () = ()
|