summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Pure/library.ML

changeset 1364 | 8ea1a962ad72 |

parent 1290 | ee8f41456d28 |

child 1407 | c22cc592785f |

--- a/src/Pure/library.ML Wed Nov 22 18:48:56 1995 +0100 +++ b/src/Pure/library.ML Thu Nov 23 12:18:16 1995 +0100 @@ -8,6 +8,11 @@ input / output, timing, filenames, misc functions. *) +infix |> ~~ \ \\ orelf ins orf andf prefix upto downto mem union inter subset; + + +structure Library = +struct (** functions **) @@ -18,11 +23,9 @@ fun K x y = x; (*reverse apply*) -infix |>; fun (x |> f) = f x; (*combine two functions forming the union of their domains*) -infix orelf; fun f orelf g = fn x => f x handle Match => g x; (*application of (infix) operator to its left or right argument*) @@ -92,10 +95,8 @@ (* operators for combining predicates *) -infix orf; fun p orf q = fn x => p x orelse q x; -infix andf; fun p andf q = fn x => p x andalso q x; fun notf p x = not (p x); @@ -272,7 +273,6 @@ (*combine two lists forming a list of pairs: [x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*) -infix ~~; fun [] ~~ [] = [] | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys) | _ ~~ _ = raise LIST "~~"; @@ -285,7 +285,6 @@ (* prefixes, suffixes *) -infix prefix; fun [] prefix _ = true | (x :: xs) prefix (y :: ys) = x = y andalso (xs prefix ys) | _ prefix _ = false; @@ -317,12 +316,10 @@ (* lists of integers *) (*make the list [from, from + 1, ..., to]*) -infix upto; fun from upto to = if from > to then [] else from :: ((from + 1) upto to); (*make the list [from, from - 1, ..., to]*) -infix downto; fun from downto to = if from < to then [] else from :: ((from - 1) downto to); @@ -429,7 +426,6 @@ (** lists as sets **) (*membership in a list*) -infix mem; fun x mem [] = false | x mem (y :: ys) = x = y orelse x mem ys; @@ -439,7 +435,6 @@ (*insertion into list if not already there*) -infix ins; fun x ins xs = if x mem xs then xs else x :: xs; (*generalized insertion*) @@ -447,7 +442,6 @@ (*union of sets represented as lists: no repetitions*) -infix union; fun xs union [] = xs | [] union ys = ys | (x :: xs) union ys = xs union (x ins ys); @@ -459,14 +453,12 @@ (*intersection*) -infix inter; fun [] inter ys = [] | (x :: xs) inter ys = if x mem ys then x :: (xs inter ys) else xs inter ys; (*subset*) -infix subset; fun [] subset ys = true | (x :: xs) subset ys = x mem ys andalso xs subset ys; @@ -480,11 +472,9 @@ (*removing an element from a list WITHOUT duplicates*) -infix \; fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x) | [] \ x = []; -infix \\; val op \\ = foldl (op \); (*removing an element from a list -- possibly WITH duplicates*) @@ -860,3 +850,6 @@ in implode lets :: scanwords is_let rest end; in scan1 (#2 (take_prefix (not o is_let) cs)) end; +end; + +open Library;