-
Notifications
You must be signed in to change notification settings - Fork 0
/
list.timl
88 lines (69 loc) · 3.03 KB
/
list.timl
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
83
84
85
86
87
88
(* List and its operations *)
structure List = struct
(* open Basic *)
(* length-indexed list *)
datatype list 'a : {Nat} =
Nil of list 'a {0}
| Cons {n : Nat} of 'a * list 'a {n} --> list 'a {n + 1}
fun length_int [a] {n : Nat} (l : list a {n}) return using $(2 * n) =
case l of
[] => 0
| _ :: xs => 1 + length_int xs
fun length [a] {n : Nat} (l : list a {n}) return nat {n} using $(2 * n) =
case l of
[] => #0
| _ :: xs => #1 #+ length xs
absidx T_map : BigO (fn m n => $m * $n) with
fun map ['a 'b] {m n : Nat} (f : 'a -- $m --> 'b) (ls : list (* 'a *)_ {n}) return list (* 'b *)_ {n} using T_map m n =
case ls of
Nil => Nil
| Cons (x, xs) => Cons (f x, map f xs)
end
fun app ['a] {m : Time} {n : Nat} (f : 'a -- m --> unit) (ls : list _ {n}) return using (m + 3.0) * $n =
case ls of
Nil => ()
| Cons (x, xs) => f x; app f xs
(* fold-left *)
fun foldl ['a 'b] {m n : Nat} (f : 'a * 'b -- $m --> 'b) acc (l : list 'a {n}) return (* 'b *) using $(m + 4) * $n =
case l of
[] => acc
| x :: xs => foldl f (f (x, acc)) xs
(* another version of [foldl] that uses big-O spec *)
absidx T_foldl : BigO (fn m n => $m * $n) with
fun foldl ['a 'b] {m n : Nat} (f : 'a * 'b -- $m --> 'b) y (xs : list 'a {n}) return (* 'b *) using T_foldl m n =
case xs of
[] => y
| x :: xs => foldl f (f (x, y)) xs
end
(* [hd] is a total function that requires its input list to be non-empty *)
fun hd {n: Nat | n > 0} (ls: list _ {n}) =
case ls of
x :: _ => x
| _ => never
(* reverse and append *)
fun rev_append {n m : Nat} (l : list _ {n}, acc : list _ {m}) return list _ {n + m} using $n =
case l of
[] => acc
| hd :: tl => rev_append (tl, hd :: acc)
fun rev {n : Nat} (xs : list _ {n}) return list _ {n} using 1.0 + $n = rev_append (xs, [])
(* val a = rev [1, 2] *)
(* val () = __&halt a *)
(* another version with Big-O complexity *)
absidx T_rev_append : BigO (fn n => $n) (* = fn n => 2.0 * $n *) with
fun rev_append_2 {n1 n2 : Nat} (xs : list _ {n1}) (ys : list _ {n2}) return list _ {n1 + n2} using T_rev_append n1 =
case xs of
[] => ys
| x :: xs => rev_append_2 xs (x :: ys)
end
(* reverse *)
absidx T_rev2 : BigO (fn n => $n) with
fun rev2 {n : Nat} (xs : list _ {n}) return list _ {n} using T_rev2 n = rev_append_2 xs []
end
open Nat
fun tabulate' ['a] {start len : Nat} {m : Time} (start : nat {start}, len : nat {len}, f : nat_less_than {start + len} -- m --> 'a) return list 'a {len} (* using (m + $4) * $len *) =
ifdec len #<= #0 then [] : list 'a {len}
else
f (NatLT start) :: tabulate' (start #+ #1, len #- #1, f) : list 'a {len} using (m + $4) * $len
fun tabulate ['a] {len : Nat} {m : Time} (n : nat {len}, f : nat_less_than {len} -- m --> 'a) =
tabulate' (#0, n, f)
end