Singly-linked list/Element insertion: Difference between revisions
Singly-linked list/Element insertion (view source)
Revision as of 22:18, 21 March 2022
, 2 years ago→{{header|ATS}}
m (→{{header|ATS}}) |
|||
Line 649:
I repeated the ‘Rosetta Code linear list type’ here, so you can simply copy
Also I put the executable parts in initialization rather than the main program,
to avoid being forced to
Notice that the insertion routine proves that the resulting list is either of
Line 667:
| {0 <= n} rclist_vt_cons (vt, n + 1) of (vt, rclist_vt (vt, n))
(*
extern
lemma_rclist_vt_param
(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 _ => ()
(*------------------------------------------------------------------*)
Line 728 ⟶ 735:
(* The following is needed to prove that the initial k above
satisfies 0 <= k. *)
prval _ =
val _ = find (lst, after, x)
Line 734 ⟶ 741:
(* 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
Line 740 ⟶ 753:
(* ‘var’ to make lst a mutable variable rather than a
value (‘val’). *)
var lst =
(* Do the insertion. *)
val () =
fun
Line 749 ⟶ 762:
(p : !rclist_vt (int, k)) : void =
case+ p of
|
|
begin
println! (head);
loop tail
end
prval () =
val () = loop lst
Line 764 ⟶ 777:
{{out}}
<pre>$ patscc -DATS_MEMALLOC_LIBC
123
456
| |||