Added some optimized versions of functions dealing with sets
(i.e. mem, ins, eq_set etc.) which do not use the polymorphic =
operator
--- a/src/Pure/library.ML Wed Mar 13 11:56:15 1996 +0100
+++ b/src/Pure/library.ML Thu Mar 14 10:40:21 1996 +0100
@@ -8,8 +8,9 @@
input / output, timing, filenames, misc functions.
*)
-infix |> ~~ \ \\ orelf ins orf andf prefix upto downto mem union inter subset
- subdir_of;
+infix |> ~~ \ \\ orelf ins ins_string ins_int orf andf prefix upto downto
+ mem mem_int mem_string union union_string union_int inter inter_int
+ inter_string subset subset_int subset_string subdir_of;
structure Library =
@@ -430,6 +431,14 @@
fun x mem [] = false
| x mem (y :: ys) = x = y orelse x mem ys;
+(*membership in a list, optimized version for int lists*)
+fun (x:int) mem_int [] = false
+ | x mem_int (y :: ys) = x = y orelse x mem_int ys;
+
+(*membership in a list, optimized version for string lists*)
+fun (x:string) mem_string [] = false
+ | x mem_string (y :: ys) = x = y orelse x mem_string ys;
+
(*generalized membership test*)
fun gen_mem eq (x, []) = false
| gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys);
@@ -438,6 +447,12 @@
(*insertion into list if not already there*)
fun x ins xs = if x mem xs then xs else x :: xs;
+(*insertion into list if not already there, optimized version for int lists*)
+fun (x:int) ins_int xs = if x mem_int xs then xs else x :: xs;
+
+(*insertion into list if not already there, optimized version for string lists*)
+fun (x:string) ins_string xs = if x mem_string xs then xs else x :: xs;
+
(*generalized insertion*)
fun gen_ins eq (x, xs) = if gen_mem eq (x, xs) then xs else x :: xs;
@@ -447,6 +462,16 @@
| [] union ys = ys
| (x :: xs) union ys = xs union (x ins ys);
+(*union of sets represented as lists: no repetitions, optimized version for int lists*)
+fun (xs:int list) union_int [] = xs
+ | [] union_int ys = ys
+ | (x :: xs) union_int ys = xs union_int (x ins_int ys);
+
+(*union of sets represented as lists: no repetitions, optimized version for string lists*)
+fun (xs:string list) union_string [] = xs
+ | [] union_string ys = ys
+ | (x :: xs) union_string ys = xs union_string (x ins_string ys);
+
(*generalized union*)
fun gen_union eq (xs, []) = xs
| gen_union eq ([], ys) = ys
@@ -458,11 +483,29 @@
| (x :: xs) inter ys =
if x mem ys then x :: (xs inter ys) else xs inter ys;
+(*intersection, optimized version for int lists*)
+fun ([]:int list) inter_int ys = []
+ | (x :: xs) inter_int ys =
+ if x mem_int ys then x :: (xs inter_int ys) else xs inter_int ys;
+
+(*intersection, optimized version for string lists *)
+fun ([]:string list) inter_string ys = []
+ | (x :: xs) inter_string ys =
+ if x mem_string ys then x :: (xs inter_string ys) else xs inter_string ys;
+
(*subset*)
fun [] subset ys = true
| (x :: xs) subset ys = x mem ys andalso xs subset ys;
+(*subset, optimized version for int lists*)
+fun ([]:int list) subset_int ys = true
+ | (x :: xs) subset_int ys = x mem_int ys andalso xs subset_int ys;
+
+(*subset, optimized version for string lists*)
+fun ([]:string list) subset_string ys = true
+ | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys;
+
fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs;
@@ -471,6 +514,16 @@
fun eq_set (xs, ys) =
xs = ys orelse (xs subset ys andalso ys subset xs);
+(*eq_set, optimized version for int lists*)
+
+fun eq_set_int ((xs:int list), ys) =
+ xs = ys orelse (xs subset_int ys andalso ys subset_int xs);
+
+(*eq_set, optimized version for string lists*)
+
+fun eq_set_string ((xs:string list), ys) =
+ xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
+
(*removing an element from a list WITHOUT duplicates*)
fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
@@ -532,6 +585,21 @@
| assoc ((keyi, xi) :: pairs, key) =
if key = keyi then Some xi else assoc (pairs, key);
+(*association list lookup, optimized version for int lists*)
+fun assoc_int ([], (key:int)) = None
+ | assoc_int ((keyi, xi) :: pairs, key) =
+ if key = keyi then Some xi else assoc_int (pairs, key);
+
+(*association list lookup, optimized version for string lists*)
+fun assoc_string ([], (key:string)) = None
+ | assoc_string ((keyi, xi) :: pairs, key) =
+ if key = keyi then Some xi else assoc_string (pairs, key);
+
+(*association list lookup, optimized version for string*int lists*)
+fun assoc_string_int ([], (key:string*int)) = None
+ | assoc_string_int ((keyi, xi) :: pairs, key) =
+ if key = keyi then Some xi else assoc_string_int (pairs, key);
+
fun assocs ps x =
(case assoc (ps, x) of
None => []
--- a/src/Pure/pattern.ML Wed Mar 13 11:56:15 1996 +0100
+++ b/src/Pure/pattern.ML Thu Mar 14 10:40:21 1996 +0100
@@ -72,7 +72,7 @@
fun ints_of [] = []
| ints_of (Bound i ::bs) =
let val is = ints_of bs
- in if i mem is then raise Pattern else i::is end
+ in if i mem_int is then raise Pattern else i::is end
| ints_of _ = raise Pattern;
@@ -167,10 +167,10 @@
fun flexflex2(env,binders,F,Fty,is,G,Gty,js) =
let fun ff(F,Fty,is,G as (a,_),Gty,js) =
- if js subset is
+ if js subset_int is
then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
in Envir.update((F,t),env) end
- else let val ks = is inter js
+ else let val ks = is inter_int js
val Hty = type_of_G(Fty,length is,map (idx is) ks)
val (env',H) = Envir.genvar a (env,Hty)
fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
@@ -227,7 +227,7 @@
fun eta_contract (Abs(a,T,body)) =
(case eta_contract body of
body' as (f $ Bound i) =>
- if i=0 andalso not (0 mem loose_bnos f) then incr_boundvars ~1 f
+ if i=0 andalso not (0 mem_int loose_bnos f) then incr_boundvars ~1 f
else Abs(a,T,body')
| body' => Abs(a,T,body'))
| eta_contract(f$t) = eta_contract f $ eta_contract t
@@ -249,7 +249,7 @@
fun mtch (tyinsts,insts) = fn
(Var(ixn,T), t) =>
if loose_bvar(t,0) then raise MATCH
- else (case assoc(insts,ixn) of
+ else (case assoc_string_int(insts,ixn) of
None => (typ_match (tyinsts, (T, fastype_of t)),
(ixn,t)::insts)
| Some u => if t aconv u then (tyinsts,insts) else raise MATCH)
@@ -270,7 +270,7 @@
let val js = loose_bnos t
in if null is
then if null js then (ixn,t)::itms else raise MATCH
- else if js subset is
+ else if js subset_int is
then let val t' = if downto0(is,length binders - 1) then t
else mapbnd (idx is) t
in (ixn, mkabs(binders,is,t')) :: itms end
@@ -320,7 +320,7 @@
in case ph of
Var(ixn,_) =>
let val is = ints_of pargs
- in case assoc(itms,ixn) of
+ in case assoc_string_int(itms,ixn) of
None => (iTs,match_bind(itms,binders,ixn,is,obj))
| Some u => if obj aeconv (red u is []) then env
else raise MATCH
--- a/src/Pure/sign.ML Wed Mar 13 11:56:15 1996 +0100
+++ b/src/Pure/sign.ML Thu Mar 14 10:40:21 1996 +0100
@@ -225,7 +225,7 @@
Type(_,Ts) => foldl nodup_TVars (tvars,Ts)
| TFree _ => tvars
| TVar(v as (a,S)) =>
- (case assoc(tvars,a) of
+ (case assoc_string_int(tvars,a) of
Some(S') => if S=S' then tvars
else raise_type
("Type variable "^Syntax.string_of_vname a^
@@ -238,7 +238,7 @@
Const(c,T) => (vars, nodup_TVars(tvars,T))
| Free(a,T) => (vars, nodup_TVars(tvars,T))
| Var(v as (ixn,T)) =>
- (case assoc(vars,ixn) of
+ (case assoc_string_int(vars,ixn) of
Some(T') => if T=T' then (vars,nodup_TVars(tvars,T))
else raise_type
("Variable "^Syntax.string_of_vname ixn^
--- a/src/Pure/thm.ML Wed Mar 13 11:56:15 1996 +0100
+++ b/src/Pure/thm.ML Thu Mar 14 10:40:21 1996 +0100
@@ -1127,7 +1127,7 @@
in
case findrep cs of
c::_ => error ("Bound variables not distinct: " ^ c)
- | [] => (case cs inter freenames of
+ | [] => (case cs inter_string freenames of
a::_ => error ("Bound/Free variable clash: " ^ a)
| [] => fix_shyps [state] []
(Thm{sign = sign,
@@ -1173,11 +1173,11 @@
val vids = map (#1 o #1 o dest_Var) vars;
fun rename(t as Var((x,i),T)) =
(case assoc(al,x) of
- Some(y) => if x mem vids orelse y mem vids then t
+ Some(y) => if x mem_string vids orelse y mem_string vids then t
else Var((y,i),T)
| None=> t)
| rename(Abs(x,T,t)) =
- Abs(case assoc(al,x) of Some(y) => y | None => x,
+ Abs(case assoc_string(al,x) of Some(y) => y | None => x,
T, rename t)
| rename(f$t) = rename f $ rename t
| rename(t) = t;
@@ -1528,7 +1528,7 @@
fun ren_inst(insts,prop,pat,obj) =
let val ren = match_bvs(pat,obj,[])
fun renAbs(Abs(x,T,b)) =
- Abs(case assoc(ren,x) of None => x | Some(y) => y, T, renAbs(b))
+ Abs(case assoc_string(ren,x) of None => x | Some(y) => y, T, renAbs(b))
| renAbs(f$t) = renAbs(f) $ renAbs(t)
| renAbs(t) = t
in subst_vars insts (if null(ren) then prop else renAbs(prop)) end;
@@ -1686,7 +1686,7 @@
val (h,ts) = strip_comb t
in case h of
Const(a,_) =>
- (case assoc(congs,a) of
+ (case assoc_string(congs,a) of
None => appc()
| Some(cong) => (congc (prover mss,sign) cong trec
handle Pattern.MATCH => appc() ) )