# HG changeset patch # User berghofe # Date 826796421 -3600 # Node ID af8f43f742a03280fc2e8e430450b2aa7e4e9fd9 # Parent 4118fb066ba95a0b9683440b5279cf762c609990 Added some optimized versions of functions dealing with sets (i.e. mem, ins, eq_set etc.) which do not use the polymorphic = operator diff -r 4118fb066ba9 -r af8f43f742a0 src/Pure/library.ML --- 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 => [] diff -r 4118fb066ba9 -r af8f43f742a0 src/Pure/pattern.ML --- 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 diff -r 4118fb066ba9 -r af8f43f742a0 src/Pure/sign.ML --- 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^ diff -r 4118fb066ba9 -r af8f43f742a0 src/Pure/thm.ML --- 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() ) )