File: list_rec_functions1.sail

package info (click to toggle)
sail-ocaml 0.19.1%2Bdfsg5-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 18,008 kB
  • sloc: ml: 75,941; ansic: 8,848; python: 1,342; exp: 560; sh: 474; makefile: 218; cpp: 36
file content (82 lines) | stat: -rw-r--r-- 2,064 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
default Order dec

$include <prelude.sail>
$include <string.sail>

val list_hd : forall ('a : Type). list('a) -> option('a)

function list_hd(xs) = match xs {
    [||] => None(),
    x :: xs => Some(x),
}

val list_length : forall ('a : Type). list('a) -> int

function list_length(xs) = match xs {
    [||] => 0,
    _ :: tail => 1 + list_length(tail),
}

val list_append : forall ('a : Type). (list('a), list('a)) -> list('a)

function list_append(xs, ys) = match xs {
    [||] => ys,
    x :: xs => x :: list_append(xs, ys),
}

val list_rev : forall ('a : Type). list('a) -> list('a)

function list_rev(xs) = match xs {
    [||] => [||],
    x :: xs => list_append(list_rev(xs), [|x|]),
}

val int_list_str : list(int) -> string

function int_list_str(xs) = match xs {
   [||] => "",
   [|x|] => dec_str(x),
   x :: xs => concat_str(dec_str(x), concat_str(", ", int_list_str(xs))),
}

val print_int_list : list(int) -> unit

function print_int_list(xs) =
    print_endline(concat_str("[|", concat_str(int_list_str(xs), "|]")))

val main : unit -> unit

function main() = {
    let xs: list(int) = [|1, 2, 3, 4, 5, 6, 7|];
    print_int_list(xs);
    print_int_list(list_rev(xs));
    print_int("list_length(xs) == ", list_length(xs));
    let ys: list(int) = 8 :: 9 :: [||];
    print_int_list(ys);
    let zs = list_append(xs, ys);
    print_int_list(zs);
    match list_hd(zs) {
        Some(z) => print_int("", z),
        None() => (),
    };
    match list_hd(list_rev(zs)) {
        Some(z) => print_int("", z),
        None() => (),
    };
    print_int("list_length(zs) == ", list_length(zs));
    match zs {
        z1 :: z2 :: ws => {
            print_int_list(ws);
            print_int("", z1);
            print_int("", z2);
            print_int("list_length(ws) == ", list_length(list_rev(list_rev(ws))));
            match list_hd(ws) {
                Some(w) => print_int("", w),
                None() => (),
            }
        },
        _ => (),
    };
    let zs = list_rev(zs);
    print_int("list_length(zs) == ", list_length(zs))
}