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 11(* provide an inputLine function �� la old version of the Basis Library *) 12structure StrictCBasics = 13struct 14 fun inputLine istr = case TextIO.inputLine istr of 15 NONE => "" 16 | SOME s => s 17 18 (* 19 val inputLine = TextIO.inputLine 20 *) 21 22 (* fix for Isabelle library change *) 23 fun assoc x = uncurry (AList.lookup (op =)) x; 24 25 (* recreated from Isabelle library change *) 26 fun assert p msg = if p then () else error msg; 27 28 29fun list_compare cfn = 30 let fun comp ([],[]) = EQUAL 31 | comp ([], _) = LESS 32 | comp (_, []) = GREATER 33 | comp (h1::t1, h2::t2) = 34 case cfn (h1,h2) of EQUAL => comp (t1,t2) | x => x 35 in comp end; 36 37fun pair_compare (acmp, bcmp) ((a1, b1), (a2, b2)) = 38 case acmp(a1, a2) of 39 EQUAL => bcmp(b1, b2) 40 | x => x 41 42fun option_compare _ (NONE, SOME _) = LESS 43 | option_compare _ (NONE, NONE) = EQUAL 44 | option_compare _ (SOME _, NONE) = GREATER 45 | option_compare cmp (SOME x, SOME y) = cmp(x,y) 46 47fun measure_cmp f (x,y) = Int.compare(f x, f y) 48fun inv_img_cmp f c (x,y) = c (f x, f y) 49 50end; 51 52open StrictCBasics 53 54signature FLIP_TABLE = 55sig 56 type key 57 type 'a table 58 val flip : key list table -> key list table 59end 60functor FlipTable(structure Table : TABLE) : FLIP_TABLE = 61struct 62 type key = Table.key 63 type 'a table = 'a Table.table 64 fun flip table = let 65 fun foldthis (k:key,elems:key list) acc = 66 List.foldl (fn (e,acc) => Table.cons_list (e,k) acc) acc elems 67 in 68 Table.fold foldthis table Table.empty 69 end 70end 71local 72 structure FlipSymTab = FlipTable(structure Table = Symtab) 73in 74 val flip_symtab = FlipSymTab.flip 75end 76