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