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