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