# HG changeset patch # User clasohm # Date 817125496 -3600 # Node ID 8ea1a962ad721e762c3d4dc862c63cc42fdddab3 # Parent 7bdc4699ef4d7fcab01f6c41c45565a3b6ef2bfc files now define a structure to allow SML/NJ to optimize the code diff -r 7bdc4699ef4d -r 8ea1a962ad72 src/Pure/library.ML --- 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; diff -r 7bdc4699ef4d -r 8ea1a962ad72 src/Pure/term.ML --- a/src/Pure/term.ML Wed Nov 22 18:48:56 1995 +0100 +++ b/src/Pure/term.ML Thu Nov 23 12:18:16 1995 +0100 @@ -2,11 +2,18 @@ ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright Cambridge University 1992 + +Simply typed lambda-calculus: types, terms, and basic operations *) +infix 9 $; +infixr 5 -->; +infixr --->; +infix aconv; + -(*Simply typed lambda-calculus: types, terms, and basic operations*) - +structure Term = +struct (*Indexnames can be quickly renamed by adding an offset to the integer part, for resolution.*) @@ -21,11 +28,9 @@ | TFree of string * sort | TVar of indexname * sort; -infixr 5 -->; fun S --> T = Type("fun",[S,T]); (*handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)*) -infixr --->; val op ---> = foldr (op -->); @@ -39,7 +44,6 @@ -infix 9 $; (*application binds tightly!*) datatype term = Const of string * typ | Free of string * typ @@ -304,7 +308,6 @@ (*Tests whether 2 terms are alpha-convertible and have same type. Note that constants and Vars may have more than one type.*) -infix aconv; fun (Const(a,T)) aconv (Const(b,U)) = a=b andalso T=U | (Free(a,T)) aconv (Free(b,U)) = a=b andalso T=U | (Var(v,T)) aconv (Var(w,U)) = v=w andalso T=U @@ -588,3 +591,7 @@ in foldl rename_aT ([],vars) end; fun rename_wrt_term t = rename_aTs (add_term_names(t,[])); + +end; + +open Term;