files now define a structure to allow SML/NJ to optimize the code
authorclasohm
Thu Nov 23 12:18:16 1995 +0100 (1995-11-23)
changeset 13648ea1a962ad72
parent 1363 7bdc4699ef4d
child 1365 0defae128e43
files now define a structure to allow SML/NJ to optimize the code
src/Pure/library.ML
src/Pure/term.ML
     1.1 --- a/src/Pure/library.ML	Wed Nov 22 18:48:56 1995 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Nov 23 12:18:16 1995 +0100
     1.3 @@ -8,6 +8,11 @@
     1.4  input / output, timing, filenames, misc functions.
     1.5  *)
     1.6  
     1.7 +infix |> ~~ \ \\ orelf ins orf andf prefix upto downto mem union inter subset;
     1.8 +
     1.9 +
    1.10 +structure Library =
    1.11 +struct
    1.12  
    1.13  (** functions **)
    1.14  
    1.15 @@ -18,11 +23,9 @@
    1.16  fun K x y = x;
    1.17  
    1.18  (*reverse apply*)
    1.19 -infix |>;
    1.20  fun (x |> f) = f x;
    1.21  
    1.22  (*combine two functions forming the union of their domains*)
    1.23 -infix orelf;
    1.24  fun f orelf g = fn x => f x handle Match => g x;
    1.25  
    1.26  (*application of (infix) operator to its left or right argument*)
    1.27 @@ -92,10 +95,8 @@
    1.28  
    1.29  (* operators for combining predicates *)
    1.30  
    1.31 -infix orf;
    1.32  fun p orf q = fn x => p x orelse q x;
    1.33  
    1.34 -infix andf;
    1.35  fun p andf q = fn x => p x andalso q x;
    1.36  
    1.37  fun notf p x = not (p x);
    1.38 @@ -272,7 +273,6 @@
    1.39  
    1.40  (*combine two lists forming a list of pairs:
    1.41    [x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
    1.42 -infix ~~;
    1.43  fun [] ~~ [] = []
    1.44    | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
    1.45    | _ ~~ _ = raise LIST "~~";
    1.46 @@ -285,7 +285,6 @@
    1.47  
    1.48  (* prefixes, suffixes *)
    1.49  
    1.50 -infix prefix;
    1.51  fun [] prefix _ = true
    1.52    | (x :: xs) prefix (y :: ys) = x = y andalso (xs prefix ys)
    1.53    | _ prefix _ = false;
    1.54 @@ -317,12 +316,10 @@
    1.55  (* lists of integers *)
    1.56  
    1.57  (*make the list [from, from + 1, ..., to]*)
    1.58 -infix upto;
    1.59  fun from upto to =
    1.60    if from > to then [] else from :: ((from + 1) upto to);
    1.61  
    1.62  (*make the list [from, from - 1, ..., to]*)
    1.63 -infix downto;
    1.64  fun from downto to =
    1.65    if from < to then [] else from :: ((from - 1) downto to);
    1.66  
    1.67 @@ -429,7 +426,6 @@
    1.68  (** lists as sets **)
    1.69  
    1.70  (*membership in a list*)
    1.71 -infix mem;
    1.72  fun x mem [] = false
    1.73    | x mem (y :: ys) = x = y orelse x mem ys;
    1.74  
    1.75 @@ -439,7 +435,6 @@
    1.76  
    1.77  
    1.78  (*insertion into list if not already there*)
    1.79 -infix ins;
    1.80  fun x ins xs = if x mem xs then xs else x :: xs;
    1.81  
    1.82  (*generalized insertion*)
    1.83 @@ -447,7 +442,6 @@
    1.84  
    1.85  
    1.86  (*union of sets represented as lists: no repetitions*)
    1.87 -infix union;
    1.88  fun xs union [] = xs
    1.89    | [] union ys = ys
    1.90    | (x :: xs) union ys = xs union (x ins ys);
    1.91 @@ -459,14 +453,12 @@
    1.92  
    1.93  
    1.94  (*intersection*)
    1.95 -infix inter;
    1.96  fun [] inter ys = []
    1.97    | (x :: xs) inter ys =
    1.98        if x mem ys then x :: (xs inter ys) else xs inter ys;
    1.99  
   1.100  
   1.101  (*subset*)
   1.102 -infix subset;
   1.103  fun [] subset ys = true
   1.104    | (x :: xs) subset ys = x mem ys andalso xs subset ys;
   1.105  
   1.106 @@ -480,11 +472,9 @@
   1.107  
   1.108  
   1.109  (*removing an element from a list WITHOUT duplicates*)
   1.110 -infix \;
   1.111  fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
   1.112    | [] \ x = [];
   1.113  
   1.114 -infix \\;
   1.115  val op \\ = foldl (op \);
   1.116  
   1.117  (*removing an element from a list -- possibly WITH duplicates*)
   1.118 @@ -860,3 +850,6 @@
   1.119              in implode lets :: scanwords is_let rest end;
   1.120    in scan1 (#2 (take_prefix (not o is_let) cs)) end;
   1.121  
   1.122 +end;
   1.123 +
   1.124 +open Library;
     2.1 --- a/src/Pure/term.ML	Wed Nov 22 18:48:56 1995 +0100
     2.2 +++ b/src/Pure/term.ML	Thu Nov 23 12:18:16 1995 +0100
     2.3 @@ -2,11 +2,18 @@
     2.4      ID:         $Id$
     2.5      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     2.6      Copyright   Cambridge University 1992
     2.7 +
     2.8 +Simply typed lambda-calculus: types, terms, and basic operations
     2.9  *)
    2.10  
    2.11 +infix 9  $;
    2.12 +infixr 5 -->;
    2.13 +infixr   --->;
    2.14 +infix    aconv;
    2.15 +
    2.16  
    2.17 -(*Simply typed lambda-calculus: types, terms, and basic operations*)
    2.18 -
    2.19 +structure Term =
    2.20 +struct
    2.21  
    2.22  (*Indexnames can be quickly renamed by adding an offset to the integer part,
    2.23    for resolution.*)
    2.24 @@ -21,11 +28,9 @@
    2.25               | TFree of string * sort
    2.26  	     | TVar  of indexname * sort;
    2.27  
    2.28 -infixr 5 -->;
    2.29  fun S --> T = Type("fun",[S,T]);
    2.30  
    2.31  (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
    2.32 -infixr --->;
    2.33  val op ---> = foldr (op -->);
    2.34  
    2.35  
    2.36 @@ -39,7 +44,6 @@
    2.37  
    2.38  
    2.39  
    2.40 -infix 9 $;  (*application binds tightly!*)
    2.41  datatype term = 
    2.42      Const of string * typ
    2.43    | Free  of string * typ 
    2.44 @@ -304,7 +308,6 @@
    2.45  
    2.46  (*Tests whether 2 terms are alpha-convertible and have same type.
    2.47    Note that constants and Vars may have more than one type.*)
    2.48 -infix aconv;
    2.49  fun (Const(a,T)) aconv (Const(b,U)) = a=b  andalso  T=U
    2.50    | (Free(a,T)) aconv (Free(b,U)) = a=b  andalso  T=U
    2.51    | (Var(v,T)) aconv (Var(w,U)) =   v=w  andalso  T=U
    2.52 @@ -588,3 +591,7 @@
    2.53    in foldl rename_aT ([],vars) end;
    2.54  
    2.55  fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
    2.56 +
    2.57 +end;
    2.58 +
    2.59 +open Term;