90 lines
2 KiB
Text
90 lines
2 KiB
Text
#include "share/atspre_staload.hats"
|
|
|
|
(* I will use the list type of prelude/SATS/list.sats *)
|
|
|
|
#define NIL list_nil ()
|
|
#define :: list_cons
|
|
|
|
fn {a : t@ype}
|
|
unit_List (x : a) : list (a, 1) =
|
|
x :: NIL
|
|
|
|
fn {a, b : t@ype}
|
|
bind_List (m : List a,
|
|
f : a -<cloref1> List b) : List0 b =
|
|
let
|
|
fun
|
|
reversed_segments (m : List a,
|
|
accum : List0 (List b))
|
|
: List0 (List b) =
|
|
case+ m of
|
|
| NIL => accum
|
|
| hd :: tl => reversed_segments (tl, f hd :: accum)
|
|
|
|
fun
|
|
assemble_segments (segments : List (List b),
|
|
accum : List0 b)
|
|
: List0 b =
|
|
case+ segments of
|
|
| NIL => accum
|
|
| hd :: tl =>
|
|
let
|
|
prval () = lemma_list_param hd
|
|
val accum = list_append (hd, accum)
|
|
in
|
|
assemble_segments (tl, accum)
|
|
end
|
|
in
|
|
assemble_segments (reversed_segments (m, NIL), NIL)
|
|
end
|
|
|
|
infixl 0 >>=
|
|
overload >>= with bind_List
|
|
|
|
fn
|
|
intseq_List {n : nat}
|
|
(i0 : int,
|
|
n : int n) :<cloref1> list (int, n) =
|
|
let
|
|
implement
|
|
list_tabulate$fopr<int> j = i0 + j
|
|
in
|
|
list_vt2t (list_tabulate<int> n)
|
|
end
|
|
|
|
implement
|
|
main0 () =
|
|
let
|
|
val n = 25
|
|
val pythagorean_triples =
|
|
intseq_List (1, n) >>=
|
|
(lam i =>
|
|
(intseq_List (succ (i : int), n) >>=
|
|
(lam j =>
|
|
(intseq_List (succ (j : int), n) >>=
|
|
(lam k =>
|
|
let
|
|
val i = i : int
|
|
and j = j : int
|
|
and k = k : int
|
|
in
|
|
if (i * i) + (j * j) = (k * k) then
|
|
@(i, j, k) :: NIL
|
|
else
|
|
NIL
|
|
end)))))
|
|
|
|
fun
|
|
loop {n : nat}
|
|
.<n>.
|
|
(m : list (@(int, int, int), n)) : void =
|
|
case+ m of
|
|
| NIL => ()
|
|
| (@(a, b, c) :: tl) =>
|
|
begin
|
|
println! ("(", a, ",", b, ",", c, ")");
|
|
loop tl
|
|
end
|
|
in
|
|
loop pythagorean_triples
|
|
end
|