1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 *)
10
11structure StrictCBasics =
12struct
13
14fun inputLine istr = case TextIO.inputLine istr of
15                       NONE => ""
16                     | SOME s => s
17
18fun assoc (l, x) =
19    case l of
20      [] => NONE
21    | (k,v) :: rest => if k = x then SOME v else assoc(rest, x)
22
23fun list_compare cfn =
24 let fun comp ([],[]) = EQUAL
25       | comp ([], _) = LESS
26       | comp (_, []) = GREATER
27       | comp (h1::t1, h2::t2) =
28          case cfn (h1,h2) of EQUAL => comp (t1,t2) | x => x
29  in comp end;
30
31fun pair_compare (acmp, bcmp) ((a1, b1), (a2, b2)) =
32    case acmp(a1, a2) of
33      EQUAL => bcmp(b1, b2)
34    | x => x
35
36fun option_compare cfn vals =
37    case vals of
38      (NONE, NONE) => EQUAL
39    | (NONE, _) => LESS
40    | (_, NONE) => GREATER
41    | (SOME v1, SOME v2) => cfn(v1, v2)
42
43
44fun measure_cmp f (x,y) = Int.compare(f x, f y)
45fun inv_img_cmp f c (x,y) = c (f x, f y)
46
47end
48open StrictCBasics
49
50fun apsnd f (x,y) = (x,f y)
51
52
53structure Hoare =
54struct
55  fun varname s = s ^ "_'"
56end
57
58infix 1 |> ||>> |->
59
60structure Basics =
61struct
62  fun cons h t = h::t
63  fun x |> f = f x
64  fun (x,y) ||>> f = let val (z, y') = f y in ((x,z), y') end
65  fun (x,y) |-> f = f x y
66  fun pair x y = (x,y)
67  val the = valOf
68  fun snd (x,y) = y
69  fun these NONE = []
70    | these (SOME l) = l
71  fun fold _ [] y = y
72    | fold f (x :: xs) y = fold f xs (f x y)
73  fun fold_rev _ [] y = y
74    | fold_rev f (x :: xs) y = f x (fold_rev f xs y)
75
76  fun K x y = x
77  fun I x = x
78
79end
80
81open Basics
82
83infix mem
84structure Library =
85struct
86
87  val int_ord = Int.compare
88  val fast_string_ord = String.compare
89
90  fun maps f [] = []
91    | maps f (x :: xs) = f x @ maps f xs
92
93  fun filter_out f = List.filter (not o f)
94  fun fold_index f = let
95    fun fold_aux (_: int) [] y = y
96      | fold_aux i (x :: xs) y = fold_aux (i + 1) xs (f (i, x) y)
97  in
98    fold_aux 0
99  end
100
101
102  fun member eq list x = let
103    fun memb [] = false
104      | memb (y :: ys) = eq (x, y) orelse memb ys
105  in memb list end
106
107  fun x mem xs = member (op =) xs x
108
109  fun insert eq x xs = if member eq xs x then xs else x :: xs
110
111  fun remove eq x xs = if member eq xs x then
112                         filter_out (fn y => eq (x, y)) xs
113                       else xs
114  fun update eq x xs = cons x (remove eq x xs)
115
116  fun merge _ ([], ys) = ys
117    | merge eq (xs, ys) = fold_rev (insert eq) ys xs
118
119  fun swap (x,y) = (y,x)
120
121  fun subset eq (xs, ys) = List.all (member eq ys) xs
122
123  (*set equality*)
124  fun eq_list eq (list1, list2) = let
125    fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys)
126      | eq_lst _ = true
127  in
128    length list1 = length list2 andalso eq_lst (list1, list2)
129  end
130
131  fun eq_set eq (xs, ys) =
132      eq_list eq (xs, ys) orelse
133      (subset eq (xs,ys) andalso subset (eq o swap) (ys,xs))
134
135
136  fun apfst f (x, y) = (f x, y)
137
138  fun separate sep list = let
139  fun recurse acc list =
140      case list of
141        [] => List.rev acc
142      | [e] => List.rev (e::acc)
143      | e::rest => recurse (sep::e::acc) rest
144  in
145    recurse [] list
146  end
147
148  fun uncurry f (x,y) = f x y
149
150  (*union of sets represented as lists: no repetitions*)
151  fun union eq = List.foldl (uncurry (insert eq))
152
153  fun single x = [x]
154
155  fun get_first f l =
156      case l of
157        [] => NONE
158      | h :: t => (case f h of NONE => get_first f t | x => x)
159
160  val is_some = isSome
161  val pointer_eq = MLton.eq
162
163  fun prod_ord a_ord b_ord ((x, y), (x', y')) =
164      (case a_ord (x, x') of EQUAL => b_ord (y, y') | ord => ord);
165
166
167end
168
169infix union
170
171open Library
172