src/Pure/library.ML
 author wenzelm Mon Nov 29 11:08:17 1993 +0100 (1993-11-29 ago) changeset 160 80ccb6c354ba parent 41 97aae241094b child 172 3224c46737ef permissions -rw-r--r--
added equal, not_equal: ''a -> ''a -> bool
 wenzelm@41 ` 1` ```(* Title: Pure/library.ML ``` clasohm@0 ` 2` ``` ID: \$Id\$ ``` clasohm@0 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@0 ` 4` ``` Copyright 1992 University of Cambridge ``` clasohm@0 ` 5` clasohm@0 ` 6` ```Basic library: booleans, lists, pairs, input/output, etc. ``` clasohm@0 ` 7` ```*) ``` clasohm@0 ` 8` clasohm@0 ` 9` clasohm@0 ` 10` ```(**** Booleans: operators for combining predicates ****) ``` clasohm@0 ` 11` clasohm@0 ` 12` ```infix orf; ``` clasohm@0 ` 13` ```fun p orf q = fn x => p x orelse q x ; ``` clasohm@0 ` 14` clasohm@0 ` 15` ```infix andf; ``` clasohm@0 ` 16` ```fun p andf q = fn x => p x andalso q x ; ``` clasohm@0 ` 17` clasohm@0 ` 18` ```fun notf p x = not (p x) ; ``` clasohm@0 ` 19` clasohm@0 ` 20` ```fun orl [] = false ``` clasohm@0 ` 21` ``` | orl (x::l) = x orelse orl l; ``` clasohm@0 ` 22` clasohm@0 ` 23` ```fun andl [] = true ``` clasohm@0 ` 24` ``` | andl (x::l) = x andalso andl l; ``` clasohm@0 ` 25` clasohm@0 ` 26` ```(*exists pred [x1,...,xn] ======> pred(x1) orelse ... orelse pred(xn)*) ``` clasohm@0 ` 27` ```fun exists (pred: 'a -> bool) : 'a list -> bool = ``` clasohm@0 ` 28` ``` let fun boolf [] = false ``` clasohm@0 ` 29` ``` | boolf (x::l) = (pred x) orelse boolf l ``` clasohm@0 ` 30` ``` in boolf end; ``` clasohm@0 ` 31` clasohm@0 ` 32` ```(*forall pred [x1,...,xn] ======> pred(x1) andalso ... andalso pred(xn)*) ``` clasohm@0 ` 33` ```fun forall (pred: 'a -> bool) : 'a list -> bool = ``` clasohm@0 ` 34` ``` let fun boolf [] = true ``` clasohm@0 ` 35` ``` | boolf (x::l) = (pred x) andalso (boolf l) ``` clasohm@0 ` 36` ``` in boolf end; ``` clasohm@0 ` 37` clasohm@0 ` 38` wenzelm@160 ` 39` ```(** curried equality **) ``` wenzelm@160 ` 40` wenzelm@160 ` 41` ```fun equal x y = (x = y); ``` wenzelm@160 ` 42` wenzelm@160 ` 43` ```fun not_equal x y = x <> y; ``` wenzelm@160 ` 44` wenzelm@160 ` 45` wenzelm@160 ` 46` clasohm@0 ` 47` ```(*** Lists ***) ``` clasohm@0 ` 48` clasohm@0 ` 49` ```exception LIST of string; ``` clasohm@0 ` 50` clasohm@0 ` 51` ```(*discriminator and selectors for lists. *) ``` clasohm@0 ` 52` ```fun null [] = true ``` clasohm@0 ` 53` ``` | null (_::_) = false; ``` clasohm@0 ` 54` clasohm@0 ` 55` ```fun hd [] = raise LIST "hd" ``` clasohm@0 ` 56` ``` | hd (a::_) = a; ``` clasohm@0 ` 57` clasohm@0 ` 58` ```fun tl [] = raise LIST "tl" ``` clasohm@0 ` 59` ``` | tl (_::l) = l; ``` clasohm@0 ` 60` clasohm@0 ` 61` wenzelm@41 ` 62` ```(*curried cons and reverse cons*) ``` wenzelm@41 ` 63` wenzelm@41 ` 64` ```fun cons x xs = x :: xs; ``` wenzelm@41 ` 65` wenzelm@41 ` 66` ```fun rcons xs x = x :: xs; ``` wenzelm@41 ` 67` wenzelm@41 ` 68` clasohm@0 ` 69` ```(*curried functions for pairing and reversed pairing*) ``` clasohm@0 ` 70` ```fun pair x y = (x,y); ``` clasohm@0 ` 71` ```fun rpair x y = (y,x); ``` clasohm@0 ` 72` clasohm@0 ` 73` ```fun fst(x,y) = x and snd(x,y) = y; ``` clasohm@0 ` 74` clasohm@0 ` 75` ```(*Handy combinators*) ``` clasohm@0 ` 76` ```fun curry f x y = f(x,y); ``` clasohm@0 ` 77` ```fun uncurry f(x,y) = f x y; ``` clasohm@0 ` 78` ```fun I x = x and K x y = x; ``` clasohm@0 ` 79` clasohm@0 ` 80` ```(*Combine two functions forming the union of their domains*) ``` clasohm@0 ` 81` ```infix orelf; ``` clasohm@0 ` 82` ```fun f orelf g = fn x => f x handle Match=> g x; ``` clasohm@0 ` 83` clasohm@0 ` 84` clasohm@0 ` 85` ```(*Application of (infix) operator to its left or right argument*) ``` clasohm@0 ` 86` ```fun apl (x,f) y = f(x,y); ``` clasohm@0 ` 87` ```fun apr (f,y) x = f(x,y); ``` clasohm@0 ` 88` clasohm@0 ` 89` clasohm@0 ` 90` ```(*functional for pairs*) ``` clasohm@0 ` 91` ```fun pairself f (x,y) = (f x, f y); ``` clasohm@0 ` 92` clasohm@0 ` 93` ```(*Apply the function to a component of a pair*) ``` clasohm@0 ` 94` ```fun apfst f (x, y) = (f x, y); ``` clasohm@0 ` 95` ```fun apsnd f (x, y) = (x, f y); ``` clasohm@0 ` 96` clasohm@0 ` 97` ```fun square (n: int) = n*n; ``` clasohm@0 ` 98` clasohm@0 ` 99` ```fun fact 0 = 1 ``` clasohm@0 ` 100` ``` | fact n = n * fact(n-1); ``` clasohm@0 ` 101` clasohm@0 ` 102` clasohm@0 ` 103` ```(*The following versions of fold are designed to fit nicely with infixes.*) ``` clasohm@0 ` 104` clasohm@0 ` 105` ```(* (op @) (e, [x1,...,xn]) ======> ((e @ x1) @ x2) ... @ xn ``` clasohm@0 ` 106` ``` for operators that associate to the left. TAIL RECURSIVE*) ``` clasohm@0 ` 107` ```fun foldl (f: 'a * 'b -> 'a) : 'a * 'b list -> 'a = ``` clasohm@0 ` 108` ``` let fun itl (e, []) = e ``` clasohm@0 ` 109` ``` | itl (e, a::l) = itl (f(e,a), l) ``` clasohm@0 ` 110` ``` in itl end; ``` clasohm@0 ` 111` clasohm@0 ` 112` ```(* (op @) ([x1,...,xn], e) ======> x1 @ (x2 ... @ (xn @ e)) ``` clasohm@0 ` 113` ``` for operators that associate to the right. Not tail recursive.*) ``` clasohm@0 ` 114` ```fun foldr f (l,e) = ``` clasohm@0 ` 115` ``` let fun itr [] = e ``` clasohm@0 ` 116` ``` | itr (a::l) = f(a, itr l) ``` clasohm@0 ` 117` ``` in itr l end; ``` clasohm@0 ` 118` clasohm@0 ` 119` ```(* (op @) [x1,...,xn] ======> x1 @ (x2 ..(x[n-1]. @ xn)) ``` clasohm@0 ` 120` ``` for n>0, operators that associate to the right. Not tail recursive.*) ``` clasohm@0 ` 121` ```fun foldr1 f l = ``` clasohm@0 ` 122` ``` let fun itr [x] = x ``` clasohm@0 ` 123` ``` | itr (x::l) = f(x, itr l) ``` clasohm@0 ` 124` ``` in itr l end; ``` clasohm@0 ` 125` clasohm@0 ` 126` clasohm@0 ` 127` ```(*Length of a list. Should unquestionably be a standard function*) ``` clasohm@0 ` 128` ```local fun length1 (n, [ ]) = n (*TAIL RECURSIVE*) ``` clasohm@0 ` 129` ``` | length1 (n, x::l) = length1 (n+1, l) ``` clasohm@0 ` 130` ```in fun length l = length1 (0,l) end; ``` clasohm@0 ` 131` clasohm@0 ` 132` clasohm@0 ` 133` ```(*Take the first n elements from l.*) ``` clasohm@0 ` 134` ```fun take (n, []) = [] ``` clasohm@0 ` 135` ``` | take (n, x::xs) = if n>0 then x::take(n-1,xs) ``` clasohm@0 ` 136` ``` else []; ``` clasohm@0 ` 137` clasohm@0 ` 138` ```(*Drop the first n elements from l.*) ``` clasohm@0 ` 139` ```fun drop (_, []) = [] ``` clasohm@0 ` 140` ``` | drop (n, x::xs) = if n>0 then drop (n-1, xs) ``` clasohm@0 ` 141` ``` else x::xs; ``` clasohm@0 ` 142` clasohm@0 ` 143` ```(*Return nth element of l, where 0 designates the first element; ``` clasohm@0 ` 144` ``` raise EXCEPTION if list too short.*) ``` clasohm@0 ` 145` ```fun nth_elem NL = case (drop NL) of ``` clasohm@0 ` 146` ``` [] => raise LIST "nth_elem" ``` clasohm@0 ` 147` ``` | x::l => x; ``` clasohm@0 ` 148` clasohm@0 ` 149` wenzelm@41 ` 150` ```(*Last element of a list*) ``` wenzelm@41 ` 151` ```fun last_elem [] = raise LIST "last_elem" ``` wenzelm@41 ` 152` ``` | last_elem [x] = x ``` wenzelm@41 ` 153` ``` | last_elem (_ :: xs) = last_elem xs; ``` wenzelm@41 ` 154` wenzelm@41 ` 155` clasohm@0 ` 156` ```(*make the list [from, from+1, ..., to]*) ``` clasohm@0 ` 157` ```infix upto; ``` clasohm@0 ` 158` ```fun from upto to = ``` clasohm@0 ` 159` ``` if from>to then [] else from :: ((from+1) upto to); ``` clasohm@0 ` 160` clasohm@0 ` 161` ```(*make the list [from, from-1, ..., to]*) ``` clasohm@0 ` 162` ```infix downto; ``` clasohm@0 ` 163` ```fun from downto to = ``` clasohm@0 ` 164` ``` if from is = [n,n-1,...,0] *) ``` clasohm@0 ` 167` ```fun downto0(i::is,n) = i=n andalso downto0(is,n-1) ``` clasohm@0 ` 168` ``` | downto0([],n) = n = ~1; ``` clasohm@0 ` 169` clasohm@0 ` 170` ```(*Like Lisp's MAPC -- seq proc [x1,...,xn] evaluates ``` clasohm@0 ` 171` ``` proc(x1); ... ; proc(xn) for side effects.*) ``` clasohm@0 ` 172` ```fun seq (proc: 'a -> unit) : 'a list -> unit = ``` clasohm@0 ` 173` ``` let fun seqf [] = () ``` clasohm@0 ` 174` ``` | seqf (x::l) = (proc x; seqf l) ``` clasohm@0 ` 175` ``` in seqf end; ``` clasohm@0 ` 176` clasohm@0 ` 177` clasohm@0 ` 178` ```(*** Balanced folding; access to balanced trees ***) ``` clasohm@0 ` 179` clasohm@0 ` 180` ```exception Balance; (*indicates non-positive argument to balancing fun*) ``` clasohm@0 ` 181` clasohm@0 ` 182` ```(*Balanced folding; avoids deep nesting*) ``` clasohm@0 ` 183` ```fun fold_bal f [x] = x ``` clasohm@0 ` 184` ``` | fold_bal f [] = raise Balance ``` clasohm@0 ` 185` ``` | fold_bal f xs = ``` clasohm@0 ` 186` ``` let val k = length xs div 2 ``` clasohm@0 ` 187` ``` in f (fold_bal f (take(k,xs)), ``` clasohm@0 ` 188` ``` fold_bal f (drop(k,xs))) ``` clasohm@0 ` 189` ``` end; ``` clasohm@0 ` 190` clasohm@0 ` 191` ```(*Construct something of the form f(...g(...(x)...)) for balanced access*) ``` clasohm@0 ` 192` ```fun access_bal (f,g,x) n i = ``` clasohm@0 ` 193` ``` let fun acc n i = (* 1<=i<=n*) ``` clasohm@0 ` 194` ``` if n=1 then x else ``` clasohm@0 ` 195` ``` let val n2 = n div 2 ``` clasohm@0 ` 196` ``` in if i<=n2 then f (acc n2 i) ``` clasohm@0 ` 197` ``` else g (acc (n-n2) (i-n2)) ``` clasohm@0 ` 198` ``` end ``` clasohm@0 ` 199` ``` in if 1<=i andalso i<=n then acc n i else raise Balance end; ``` clasohm@0 ` 200` clasohm@0 ` 201` ```(*Construct ALL such accesses; could try harder to share recursive calls!*) ``` clasohm@0 ` 202` ```fun accesses_bal (f,g,x) n = ``` clasohm@0 ` 203` ``` let fun acc n = ``` clasohm@0 ` 204` ``` if n=1 then [x] else ``` clasohm@0 ` 205` ``` let val n2 = n div 2 ``` clasohm@0 ` 206` ``` val acc2 = acc n2 ``` clasohm@0 ` 207` ``` in if n-n2=n2 then map f acc2 @ map g acc2 ``` clasohm@0 ` 208` ``` else map f acc2 @ map g (acc (n-n2)) end ``` clasohm@0 ` 209` ``` in if 1<=n then acc n else raise Balance end; ``` clasohm@0 ` 210` clasohm@0 ` 211` clasohm@0 ` 212` ```(*** Input/Output ***) ``` clasohm@0 ` 213` clasohm@0 ` 214` ```fun prs s = output(std_out,s); ``` clasohm@0 ` 215` ```fun writeln s = prs (s ^ "\n"); ``` clasohm@0 ` 216` clasohm@0 ` 217` ```(*Print error message and abort to top level*) ``` clasohm@0 ` 218` ```exception ERROR; ``` clasohm@0 ` 219` ```fun error (msg) = (writeln msg; raise ERROR); ``` clasohm@0 ` 220` clasohm@0 ` 221` ```fun assert p msg = if p then () else error msg; ``` clasohm@0 ` 222` ```fun deny p msg = if p then error msg else (); ``` clasohm@0 ` 223` clasohm@0 ` 224` ```(*For the "test" target in Makefiles -- signifies successful termination*) ``` clasohm@0 ` 225` ```fun maketest msg = ``` clasohm@0 ` 226` ``` (writeln msg; ``` clasohm@0 ` 227` ``` output(open_out "test", "Test examples ran successfully\n")); ``` clasohm@0 ` 228` clasohm@0 ` 229` ```(*print a list surrounded by the brackets lpar and rpar, with comma separator ``` clasohm@0 ` 230` ``` print nothing for empty list*) ``` clasohm@0 ` 231` ```fun print_list (lpar, rpar, pre: 'a -> unit) (l : 'a list) = ``` clasohm@0 ` 232` ``` let fun prec(x) = (prs","; pre(x)) ``` clasohm@0 ` 233` ``` in case l of ``` clasohm@0 ` 234` ``` [] => () ``` clasohm@0 ` 235` ``` | x::l => (prs lpar; pre x; seq prec l; prs rpar) ``` clasohm@0 ` 236` ``` end; ``` clasohm@0 ` 237` clasohm@0 ` 238` ```(*print a list of items separated by newlines*) ``` clasohm@0 ` 239` ```fun print_list_ln (pre: 'a -> unit) : 'a list -> unit = ``` clasohm@0 ` 240` ``` seq (fn x => (pre x; writeln"")); ``` clasohm@0 ` 241` clasohm@0 ` 242` ```fun is_letter ch = ``` clasohm@0 ` 243` ``` (ord"A" <= ord ch) andalso (ord ch <= ord"Z") orelse ``` clasohm@0 ` 244` ``` (ord"a" <= ord ch) andalso (ord ch <= ord"z"); ``` clasohm@0 ` 245` clasohm@0 ` 246` ```fun is_digit ch = ``` clasohm@0 ` 247` ``` (ord"0" <= ord ch) andalso (ord ch <= ord"9"); ``` clasohm@0 ` 248` clasohm@0 ` 249` ```(*letter or _ or prime (') *) ``` clasohm@0 ` 250` ```fun is_quasi_letter "_" = true ``` clasohm@0 ` 251` ``` | is_quasi_letter "'" = true ``` clasohm@0 ` 252` ``` | is_quasi_letter ch = is_letter ch; ``` clasohm@0 ` 253` clasohm@0 ` 254` ```(*white space: blanks, tabs, newlines*) ``` clasohm@0 ` 255` ```val is_blank : string -> bool = fn ``` clasohm@0 ` 256` ``` " " => true | "\t" => true | "\n" => true | _ => false; ``` clasohm@0 ` 257` clasohm@0 ` 258` ```val is_letdig = is_quasi_letter orf is_digit; ``` clasohm@0 ` 259` clasohm@0 ` 260` ```val to_lower = ``` clasohm@0 ` 261` ``` let ``` clasohm@0 ` 262` ``` fun lower ch = ``` clasohm@0 ` 263` ``` if ch >= "A" andalso ch <= "Z" then ``` clasohm@0 ` 264` ``` chr (ord ch - ord "A" + ord "a") ``` clasohm@0 ` 265` ``` else ch; ``` clasohm@0 ` 266` ``` in ``` clasohm@0 ` 267` ``` implode o (map lower) o explode ``` clasohm@0 ` 268` ``` end; ``` clasohm@0 ` 269` clasohm@0 ` 270` clasohm@0 ` 271` ```(*** Timing ***) ``` clasohm@0 ` 272` clasohm@0 ` 273` ```(*Unconditional timing function*) ``` clasohm@0 ` 274` ```val timeit = cond_timeit true; ``` clasohm@0 ` 275` clasohm@0 ` 276` ```(*Timed application function*) ``` clasohm@0 ` 277` ```fun timeap f x = timeit(fn()=> f x); ``` clasohm@0 ` 278` clasohm@0 ` 279` ```(*Timed "use" function, printing filenames*) ``` clasohm@0 ` 280` ```fun time_use fname = timeit(fn()=> ``` clasohm@0 ` 281` ``` (writeln("\n**** Starting " ^ fname ^ " ****"); use fname; ``` clasohm@0 ` 282` ``` writeln("\n**** Finished " ^ fname ^ " ****"))); ``` clasohm@0 ` 283` clasohm@0 ` 284` clasohm@0 ` 285` ```(*** Misc functions ***) ``` clasohm@0 ` 286` clasohm@0 ` 287` ```(*Function exponentiation: f(...(f x)...) with n applications of f *) ``` clasohm@0 ` 288` ```fun funpow n f x = ``` clasohm@0 ` 289` ``` let fun rep (0,x) = x ``` clasohm@0 ` 290` ``` | rep (n,x) = rep (n-1, f x) ``` clasohm@0 ` 291` ``` in rep (n,x) end; ``` clasohm@0 ` 292` clasohm@0 ` 293` ```(*Combine two lists forming a list of pairs: ``` clasohm@0 ` 294` ``` [x1,...,xn] ~~ [y1,...,yn] ======> [(x1,y1), ..., (xn,yn)] *) ``` clasohm@0 ` 295` ```infix ~~; ``` clasohm@0 ` 296` ```fun [] ~~ [] = [] ``` clasohm@0 ` 297` ``` | (x::xs) ~~ (y::ys) = (x,y) :: (xs ~~ ys) ``` clasohm@0 ` 298` ``` | _ ~~ _ = raise LIST "~~"; ``` clasohm@0 ` 299` clasohm@0 ` 300` ```(*Inverse of ~~; the old 'split'. ``` clasohm@0 ` 301` ``` [(x1,y1), ..., (xn,yn)] ======> ( [x1,...,xn] , [y1,...,yn] ) *) ``` clasohm@0 ` 302` ```fun split_list (l: ('a*'b)list) = (map #1 l, map #2 l); ``` clasohm@0 ` 303` clasohm@0 ` 304` ```(*make the list [x; x; ...; x] of length n*) ``` clasohm@0 ` 305` ```fun replicate n (x: 'a) : 'a list = ``` clasohm@0 ` 306` ``` let fun rep (0,xs) = xs ``` clasohm@0 ` 307` ``` | rep (n,xs) = rep(n-1, x::xs) ``` clasohm@0 ` 308` ``` in if n<0 then raise LIST "replicate" ``` clasohm@0 ` 309` ``` else rep (n,[]) ``` clasohm@0 ` 310` ``` end; ``` clasohm@0 ` 311` clasohm@0 ` 312` ```(*Flatten a list of lists to a list.*) ``` clasohm@0 ` 313` ```fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls,[]); ``` clasohm@0 ` 314` clasohm@0 ` 315` clasohm@0 ` 316` ```(*** polymorphic set operations ***) ``` clasohm@0 ` 317` clasohm@0 ` 318` ```(*membership in a list*) ``` clasohm@0 ` 319` ```infix mem; ``` clasohm@0 ` 320` ```fun x mem [] = false ``` clasohm@0 ` 321` ``` | x mem (y::l) = (x=y) orelse (x mem l); ``` clasohm@0 ` 322` clasohm@0 ` 323` ```(*insertion into list if not already there*) ``` clasohm@0 ` 324` ```infix ins; ``` clasohm@0 ` 325` ```fun x ins xs = if x mem xs then xs else x::xs; ``` clasohm@0 ` 326` clasohm@0 ` 327` ```(*union of sets represented as lists: no repetitions*) ``` clasohm@0 ` 328` ```infix union; ``` clasohm@0 ` 329` ```fun xs union [] = xs ``` clasohm@0 ` 330` ``` | [] union ys = ys ``` clasohm@0 ` 331` ``` | (x::xs) union ys = xs union (x ins ys); ``` clasohm@0 ` 332` clasohm@0 ` 333` ```infix inter; ``` clasohm@0 ` 334` ```fun [] inter ys = [] ``` clasohm@0 ` 335` ``` | (x::xs) inter ys = if x mem ys then x::(xs inter ys) ``` clasohm@0 ` 336` ``` else xs inter ys; ``` clasohm@0 ` 337` clasohm@0 ` 338` ```infix subset; ``` clasohm@0 ` 339` ```fun [] subset ys = true ``` clasohm@0 ` 340` ``` | (x::xs) subset ys = x mem ys andalso xs subset ys; ``` clasohm@0 ` 341` clasohm@0 ` 342` ```(*removing an element from a list WITHOUT duplicates*) ``` clasohm@0 ` 343` ```infix \; ``` clasohm@0 ` 344` ```fun (y::ys) \ x = if x=y then ys else y::(ys \ x) ``` clasohm@0 ` 345` ``` | [] \ x = []; ``` clasohm@0 ` 346` clasohm@0 ` 347` ```infix \\; ``` clasohm@0 ` 348` ```val op \\ = foldl (op \); ``` clasohm@0 ` 349` clasohm@0 ` 350` ```(*** option stuff ***) ``` clasohm@0 ` 351` clasohm@0 ` 352` ```datatype 'a option = None | Some of 'a; ``` clasohm@0 ` 353` clasohm@0 ` 354` ```exception OPTION of string; ``` clasohm@0 ` 355` clasohm@0 ` 356` ```fun the (Some x) = x ``` clasohm@0 ` 357` ``` | the None = raise OPTION "the"; ``` clasohm@0 ` 358` clasohm@0 ` 359` ```fun is_some (Some _) = true ``` clasohm@0 ` 360` ``` | is_some None = false; ``` clasohm@0 ` 361` clasohm@0 ` 362` ```fun is_none (Some _) = false ``` clasohm@0 ` 363` ``` | is_none None = true; ``` clasohm@0 ` 364` clasohm@0 ` 365` clasohm@0 ` 366` ```(*** Association lists ***) ``` clasohm@0 ` 367` clasohm@0 ` 368` ```(*Association list lookup*) ``` clasohm@0 ` 369` ```fun assoc ([], key) = None ``` clasohm@0 ` 370` ``` | assoc ((keyi,xi)::pairs, key) = ``` clasohm@0 ` 371` ``` if key=keyi then Some xi else assoc (pairs,key); ``` clasohm@0 ` 372` clasohm@0 ` 373` ```fun assocs ps x = case assoc(ps,x) of None => [] | Some(ys) => ys; ``` clasohm@0 ` 374` clasohm@0 ` 375` ```(*Association list update*) ``` clasohm@0 ` 376` ```fun overwrite(al,p as (key,_)) = ``` clasohm@0 ` 377` ``` let fun over((q as (keyi,_))::pairs) = ``` clasohm@0 ` 378` ``` if keyi=key then p::pairs else q::(over pairs) ``` clasohm@0 ` 379` ``` | over[] = [p] ``` clasohm@0 ` 380` ``` in over al end; ``` clasohm@0 ` 381` clasohm@0 ` 382` ```(*Copy the list preserving elements that satisfy the predicate*) ``` clasohm@0 ` 383` ```fun filter (pred: 'a->bool) : 'a list -> 'a list = ``` clasohm@0 ` 384` ``` let fun filt [] = [] ``` clasohm@0 ` 385` ``` | filt (x::xs) = if pred(x) then x :: filt xs else filt xs ``` clasohm@0 ` 386` ``` in filt end; ``` clasohm@0 ` 387` clasohm@0 ` 388` ```fun filter_out f = filter (not o f); ``` clasohm@0 ` 389` clasohm@0 ` 390` clasohm@0 ` 391` ```(*** List operations, generalized to an arbitrary equality function "eq" ``` clasohm@0 ` 392` ``` -- so what good are equality types?? ***) ``` clasohm@0 ` 393` clasohm@0 ` 394` ```(*removing an element from a list -- possibly WITH duplicates*) ``` clasohm@0 ` 395` ```fun gen_rem eq (xs,y) = filter_out (fn x => eq(x,y)) xs; ``` clasohm@0 ` 396` clasohm@0 ` 397` ```(*generalized membership test*) ``` clasohm@0 ` 398` ```fun gen_mem eq (x, []) = false ``` clasohm@0 ` 399` ``` | gen_mem eq (x, y::ys) = eq(x,y) orelse gen_mem eq (x,ys); ``` clasohm@0 ` 400` clasohm@0 ` 401` ```(*generalized insertion*) ``` clasohm@0 ` 402` ```fun gen_ins eq (x,xs) = if gen_mem eq (x,xs) then xs else x::xs; ``` clasohm@0 ` 403` clasohm@0 ` 404` ```(*generalized union*) ``` clasohm@0 ` 405` ```fun gen_union eq (xs,[]) = xs ``` clasohm@0 ` 406` ``` | gen_union eq ([],ys) = ys ``` clasohm@0 ` 407` ``` | gen_union eq (x::xs,ys) = gen_union eq (xs, gen_ins eq (x,ys)); ``` clasohm@0 ` 408` clasohm@0 ` 409` ```(*Generalized association list lookup*) ``` clasohm@0 ` 410` ```fun gen_assoc eq ([], key) = None ``` clasohm@0 ` 411` ``` | gen_assoc eq ((keyi,xi)::pairs, key) = ``` clasohm@0 ` 412` ``` if eq(key,keyi) then Some xi else gen_assoc eq (pairs,key); ``` clasohm@0 ` 413` clasohm@0 ` 414` ```(** Finding list elements and duplicates **) ``` clasohm@0 ` 415` clasohm@0 ` 416` ```(* find the position of an element in a list *) ``` clasohm@0 ` 417` ```fun find(x,ys) = ``` clasohm@0 ` 418` ``` let fun f(y::ys,i) = if x=y then i else f(ys,i+1) ``` clasohm@0 ` 419` ``` | f(_,_) = raise LIST "find" ``` clasohm@0 ` 420` ``` in f(ys,0) end; ``` clasohm@0 ` 421` clasohm@0 ` 422` ```(*Returns the tail beginning with the first repeated element, or []. *) ``` clasohm@0 ` 423` ```fun findrep [] = [] ``` clasohm@0 ` 424` ``` | findrep (x::xs) = if x mem xs then x::xs else findrep xs; ``` clasohm@0 ` 425` clasohm@0 ` 426` ```fun distinct1 (seen, []) = rev seen ``` clasohm@0 ` 427` ``` | distinct1 (seen, x::xs) = ``` clasohm@0 ` 428` ``` if x mem seen then distinct1 (seen, xs) ``` clasohm@0 ` 429` ``` else distinct1 (x::seen, xs); ``` clasohm@0 ` 430` clasohm@0 ` 431` ```(*Makes a list of the distinct members of the input*) ``` clasohm@0 ` 432` ```fun distinct xs = distinct1([],xs); ``` clasohm@0 ` 433` clasohm@0 ` 434` clasohm@0 ` 435` ```(*Use the keyfun to make a list of (x,key) pairs.*) ``` clasohm@0 ` 436` ```fun make_keylist (keyfun: 'a->'b) : 'a list -> ('a * 'b) list = ``` clasohm@0 ` 437` ``` let fun keypair x = (x, keyfun x) ``` clasohm@0 ` 438` ``` in map keypair end; ``` clasohm@0 ` 439` clasohm@0 ` 440` ```(*Given a list of (x,key) pairs and a searchkey ``` clasohm@0 ` 441` ``` return the list of xs from each pair whose key equals searchkey*) ``` clasohm@0 ` 442` ```fun keyfilter [] searchkey = [] ``` clasohm@0 ` 443` ``` | keyfilter ((x,key)::pairs) searchkey = ``` clasohm@0 ` 444` ``` if key=searchkey then x :: keyfilter pairs searchkey ``` clasohm@0 ` 445` ``` else keyfilter pairs searchkey; ``` clasohm@0 ` 446` clasohm@0 ` 447` ```fun mapfilter (f: 'a -> 'b option) ([]: 'a list) = [] : 'b list ``` clasohm@0 ` 448` ``` | mapfilter f (x::xs) = ``` clasohm@0 ` 449` ``` case (f x) of ``` clasohm@0 ` 450` ``` None => mapfilter f xs ``` clasohm@0 ` 451` ``` | Some y => y :: mapfilter f xs; ``` clasohm@0 ` 452` clasohm@0 ` 453` clasohm@0 ` 454` ```(*Partition list into elements that satisfy predicate and those that don't. ``` clasohm@0 ` 455` ``` Preserves order of elements in both lists. *) ``` clasohm@0 ` 456` ```fun partition (pred: 'a->bool) (ys: 'a list) : ('a list * 'a list) = ``` clasohm@0 ` 457` ``` let fun part ([], answer) = answer ``` clasohm@0 ` 458` ``` | part (x::xs, (ys, ns)) = if pred(x) ``` clasohm@0 ` 459` ``` then part (xs, (x::ys, ns)) ``` clasohm@0 ` 460` ``` else part (xs, (ys, x::ns)) ``` clasohm@0 ` 461` ``` in part (rev ys, ([],[])) end; ``` clasohm@0 ` 462` clasohm@0 ` 463` clasohm@0 ` 464` ```fun partition_eq (eq:'a * 'a -> bool) = ``` clasohm@0 ` 465` ``` let fun part [] = [] ``` clasohm@0 ` 466` ``` | part (x::ys) = let val (xs,xs') = partition (apl(x,eq)) ys ``` clasohm@0 ` 467` ``` in (x::xs)::(part xs') end ``` clasohm@0 ` 468` ``` in part end; ``` clasohm@0 ` 469` clasohm@0 ` 470` clasohm@0 ` 471` ```(*Partition a list into buckets [ bi, b(i+1),...,bj ] ``` clasohm@0 ` 472` ``` putting x in bk if p(k)(x) holds. Preserve order of elements if possible.*) ``` clasohm@0 ` 473` ```fun partition_list p i j = ``` clasohm@0 ` 474` ``` let fun part k xs = ``` clasohm@0 ` 475` ``` if k>j then ``` clasohm@0 ` 476` ``` (case xs of [] => [] ``` clasohm@0 ` 477` ``` | _ => raise LIST "partition_list") ``` clasohm@0 ` 478` ``` else ``` clasohm@0 ` 479` ``` let val (ns,rest) = partition (p k) xs; ``` clasohm@0 ` 480` ``` in ns :: part(k+1)rest end ``` clasohm@0 ` 481` ``` in part i end; ``` clasohm@0 ` 482` clasohm@0 ` 483` clasohm@0 ` 484` ```(*Insertion sort. Stable (does not reorder equal elements) ``` clasohm@0 ` 485` ``` 'less' is less-than test on type 'a. *) ``` clasohm@0 ` 486` ```fun sort (less: 'a*'a -> bool) = ``` clasohm@0 ` 487` ``` let fun insert (x, []) = [x] ``` clasohm@0 ` 488` ``` | insert (x, y::ys) = ``` clasohm@0 ` 489` ``` if less(y,x) then y :: insert (x,ys) else x::y::ys; ``` clasohm@0 ` 490` ``` fun sort1 [] = [] ``` clasohm@0 ` 491` ``` | sort1 (x::xs) = insert (x, sort1 xs) ``` clasohm@0 ` 492` ``` in sort1 end; ``` clasohm@0 ` 493` wenzelm@41 ` 494` ```(*sort strings*) ``` wenzelm@41 ` 495` ```val sort_strings = sort (op <= : string * string -> bool); ``` wenzelm@41 ` 496` wenzelm@41 ` 497` clasohm@0 ` 498` ```(*Transitive Closure. Not Warshall's algorithm*) ``` clasohm@0 ` 499` ```fun transitive_closure [] = [] ``` clasohm@0 ` 500` ``` | transitive_closure ((x,ys)::ps) = ``` clasohm@0 ` 501` ``` let val qs = transitive_closure ps ``` clasohm@0 ` 502` ``` val zs = foldl (fn (zs,y) => assocs qs y union zs) (ys,ys) ``` clasohm@0 ` 503` ``` fun step(u,us) = (u, if x mem us then zs union us else us) ``` clasohm@0 ` 504` ``` in (x,zs) :: map step qs end; ``` clasohm@0 ` 505` clasohm@0 ` 506` ```(*** Converting integers to strings, generating identifiers, etc. ***) ``` clasohm@0 ` 507` clasohm@0 ` 508` ```(*Expand the number in the given base ``` clasohm@0 ` 509` ``` example: radixpand(2, 8) gives [1, 0, 0, 0] *) ``` clasohm@0 ` 510` ```fun radixpand (base,num) : int list = ``` clasohm@0 ` 511` ``` let fun radix (n,tail) = ``` clasohm@0 ` 512` ``` if nn then max(m::ns) else max(n::ns) ``` clasohm@0 ` 569` ``` | max [] = raise LIST "max"; ``` clasohm@0 ` 570` clasohm@0 ` 571` ```fun min[m : int] = m ``` clasohm@0 ` 572` ``` | min(m::n::ns) = if m ([x1,...,x(i-1)], [xi,..., xn]) ``` clasohm@0 ` 579` ``` where xi is the first element that does not satisfy the predicate*) ``` clasohm@0 ` 580` ```fun take_prefix (pred : 'a -> bool) (xs: 'a list) : 'a list * 'a list = ``` clasohm@0 ` 581` ``` let fun take (rxs, []) = (rev rxs, []) ``` clasohm@0 ` 582` ``` | take (rxs, x::xs) = ``` clasohm@0 ` 583` ``` if pred x then take(x::rxs, xs) else (rev rxs, x::xs) ``` clasohm@0 ` 584` ``` in take([],xs) end; ``` clasohm@0 ` 585` wenzelm@41 ` 586` ```(* [x1,...,xi,...,xn] ---> ([x1,...,xi], [x(i+1),..., xn]) ``` wenzelm@41 ` 587` ``` where xi is the last element that does not satisfy the predicate*) ``` wenzelm@41 ` 588` ```fun take_suffix _ [] = ([], []) ``` wenzelm@41 ` 589` ``` | take_suffix pred (x :: xs) = ``` wenzelm@41 ` 590` ``` (case take_suffix pred xs of ``` wenzelm@41 ` 591` ``` ([], sffx) => if pred x then ([], x :: sffx) else ([x], sffx) ``` wenzelm@41 ` 592` ``` | (prfx, sffx) => (x :: prfx, sffx)); ``` wenzelm@41 ` 593` wenzelm@41 ` 594` clasohm@0 ` 595` ```infix prefix; ``` clasohm@0 ` 596` ```fun [] prefix _ = true ``` clasohm@0 ` 597` ``` | (x::xs) prefix (y::ys) = (x=y) andalso (xs prefix ys) ``` clasohm@0 ` 598` ``` | _ prefix _ = false; ``` clasohm@0 ` 599` clasohm@0 ` 600` ```(* [x1, x2, ..., xn] ---> [x1, s, x2, s, ..., s, xn] *) ``` clasohm@0 ` 601` ```fun separate s (x :: (xs as _ :: _)) = x :: s :: separate s xs ``` clasohm@0 ` 602` ``` | separate _ xs = xs; ``` clasohm@0 ` 603` clasohm@0 ` 604` ```(*space_implode "..." (explode "hello"); gives "h...e...l...l...o" *) ``` clasohm@0 ` 605` ```fun space_implode a bs = implode (separate a bs); ``` clasohm@0 ` 606` wenzelm@41 ` 607` ```(*simple quoting (does not escape special chars) *) ``` clasohm@0 ` 608` ```fun quote s = "\"" ^ s ^ "\""; ``` clasohm@0 ` 609` clasohm@0 ` 610` ```(*Concatenate messages, one per line, into a string*) ``` clasohm@0 ` 611` ```val cat_lines = implode o (map (apr(op^,"\n"))); ``` clasohm@0 ` 612` clasohm@0 ` 613` ```(*Scan a list of characters into "words" composed of "letters" (recognized ``` clasohm@0 ` 614` ``` by is_let) and separated by any number of non-"letters".*) ``` clasohm@0 ` 615` ```fun scanwords is_let cs = ``` clasohm@0 ` 616` ``` let fun scan1 [] = [] ``` clasohm@0 ` 617` ``` | scan1 cs = ``` clasohm@0 ` 618` ``` let val (lets, rest) = take_prefix is_let cs ``` clasohm@0 ` 619` ``` in implode lets :: scanwords is_let rest end; ``` clasohm@0 ` 620` ``` in scan1 (#2 (take_prefix (not o is_let) cs)) end; ``` clasohm@24 ` 621` clasohm@24 ` 622` clasohm@24 ` 623` ```(*** Operations on filenames ***) ``` clasohm@24 ` 624` clasohm@24 ` 625` ```(*Convert Unix filename of the form path/file to "path/" and "file" ; ``` clasohm@24 ` 626` ``` if filename contains no slash, then it returns "" and "file" *) ``` clasohm@24 ` 627` ```fun split_filename name = ``` clasohm@24 ` 628` ``` let val (file,path) = take_prefix (apr(op<>,"/")) (rev (explode name)) ``` clasohm@24 ` 629` ``` in (implode(rev path), implode(rev file)) end; ``` clasohm@24 ` 630` clasohm@24 ` 631` ```(*Merge splitted filename (path and file); ``` clasohm@24 ` 632` ``` if path does not end with one a slash is appended *) ``` clasohm@24 ` 633` ```fun tack_on "" name = name ``` clasohm@24 ` 634` ``` | tack_on path name = ``` wenzelm@41 ` 635` ``` if last_elem (explode path) = "/" then path ^ name ``` wenzelm@41 ` 636` ``` else path ^ "/" ^ name; ``` clasohm@24 ` 637` clasohm@24 ` 638` ```(*Remove the extension of a filename, i.e. the part after the last '.' *) ``` clasohm@24 ` 639` ```fun remove_ext name = ``` clasohm@24 ` 640` ``` let val (file,_) = take_prefix (apr(op<>,".")) (rev (explode name)) ``` clasohm@24 ` 641` ``` in implode (rev file) end; ``` clasohm@24 ` 642`