Added some optimized versions of functions dealing with sets
authorberghofe
Thu Mar 14 10:40:21 1996 +0100 (1996-03-14)
changeset 1576af8f43f742a0
parent 1575 4118fb066ba9
child 1577 a84cc626ea69
Added some optimized versions of functions dealing with sets
(i.e. mem, ins, eq_set etc.) which do not use the polymorphic =
operator
src/Pure/library.ML
src/Pure/pattern.ML
src/Pure/sign.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/library.ML	Wed Mar 13 11:56:15 1996 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Mar 14 10:40:21 1996 +0100
     1.3 @@ -8,8 +8,9 @@
     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 -      subdir_of;
     1.9 +infix |> ~~ \ \\ orelf ins ins_string ins_int orf andf prefix upto downto
    1.10 +      mem mem_int mem_string union union_string union_int inter inter_int
    1.11 +      inter_string subset subset_int subset_string subdir_of;
    1.12  
    1.13  
    1.14  structure Library =
    1.15 @@ -430,6 +431,14 @@
    1.16  fun x mem [] = false
    1.17    | x mem (y :: ys) = x = y orelse x mem ys;
    1.18  
    1.19 +(*membership in a list, optimized version for int lists*)
    1.20 +fun (x:int) mem_int [] = false
    1.21 +  | x mem_int (y :: ys) = x = y orelse x mem_int ys;
    1.22 +
    1.23 +(*membership in a list, optimized version for string lists*)
    1.24 +fun (x:string) mem_string [] = false
    1.25 +  | x mem_string (y :: ys) = x = y orelse x mem_string ys;
    1.26 +
    1.27  (*generalized membership test*)
    1.28  fun gen_mem eq (x, []) = false
    1.29    | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys);
    1.30 @@ -438,6 +447,12 @@
    1.31  (*insertion into list if not already there*)
    1.32  fun x ins xs = if x mem xs then xs else x :: xs;
    1.33  
    1.34 +(*insertion into list if not already there, optimized version for int lists*)
    1.35 +fun (x:int) ins_int xs = if x mem_int xs then xs else x :: xs;
    1.36 +
    1.37 +(*insertion into list if not already there, optimized version for string lists*)
    1.38 +fun (x:string) ins_string xs = if x mem_string xs then xs else x :: xs;
    1.39 +
    1.40  (*generalized insertion*)
    1.41  fun gen_ins eq (x, xs) = if gen_mem eq (x, xs) then xs else x :: xs;
    1.42  
    1.43 @@ -447,6 +462,16 @@
    1.44    | [] union ys = ys
    1.45    | (x :: xs) union ys = xs union (x ins ys);
    1.46  
    1.47 +(*union of sets represented as lists: no repetitions, optimized version for int lists*)
    1.48 +fun (xs:int list) union_int [] = xs
    1.49 +  | [] union_int ys = ys
    1.50 +  | (x :: xs) union_int ys = xs union_int (x ins_int ys);
    1.51 +
    1.52 +(*union of sets represented as lists: no repetitions, optimized version for string lists*)
    1.53 +fun (xs:string list) union_string [] = xs
    1.54 +  | [] union_string ys = ys
    1.55 +  | (x :: xs) union_string ys = xs union_string (x ins_string ys);
    1.56 +
    1.57  (*generalized union*)
    1.58  fun gen_union eq (xs, []) = xs
    1.59    | gen_union eq ([], ys) = ys
    1.60 @@ -458,11 +483,29 @@
    1.61    | (x :: xs) inter ys =
    1.62        if x mem ys then x :: (xs inter ys) else xs inter ys;
    1.63  
    1.64 +(*intersection, optimized version for int lists*)
    1.65 +fun ([]:int list) inter_int ys = []
    1.66 +  | (x :: xs) inter_int ys =
    1.67 +      if x mem_int ys then x :: (xs inter_int ys) else xs inter_int ys;
    1.68 +
    1.69 +(*intersection, optimized version for string lists *)
    1.70 +fun ([]:string list) inter_string ys = []
    1.71 +  | (x :: xs) inter_string ys =
    1.72 +      if x mem_string ys then x :: (xs inter_string ys) else xs inter_string ys;
    1.73 +
    1.74  
    1.75  (*subset*)
    1.76  fun [] subset ys = true
    1.77    | (x :: xs) subset ys = x mem ys andalso xs subset ys;
    1.78  
    1.79 +(*subset, optimized version for int lists*)
    1.80 +fun ([]:int list) subset_int ys = true
    1.81 +  | (x :: xs) subset_int ys = x mem_int ys andalso xs subset_int ys;
    1.82 +
    1.83 +(*subset, optimized version for string lists*)
    1.84 +fun ([]:string list) subset_string ys = true
    1.85 +  | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys;
    1.86 +
    1.87  fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs;
    1.88  
    1.89  
    1.90 @@ -471,6 +514,16 @@
    1.91  fun eq_set (xs, ys) =
    1.92    xs = ys orelse (xs subset ys andalso ys subset xs);
    1.93  
    1.94 +(*eq_set, optimized version for int lists*)
    1.95 +
    1.96 +fun eq_set_int ((xs:int list), ys) =
    1.97 +  xs = ys orelse (xs subset_int ys andalso ys subset_int xs);
    1.98 +
    1.99 +(*eq_set, optimized version for string lists*)
   1.100 +
   1.101 +fun eq_set_string ((xs:string list), ys) =
   1.102 +  xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
   1.103 +
   1.104  
   1.105  (*removing an element from a list WITHOUT duplicates*)
   1.106  fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
   1.107 @@ -532,6 +585,21 @@
   1.108    | assoc ((keyi, xi) :: pairs, key) =
   1.109        if key = keyi then Some xi else assoc (pairs, key);
   1.110  
   1.111 +(*association list lookup, optimized version for int lists*)
   1.112 +fun assoc_int ([], (key:int)) = None
   1.113 +  | assoc_int ((keyi, xi) :: pairs, key) =
   1.114 +      if key = keyi then Some xi else assoc_int (pairs, key);
   1.115 +
   1.116 +(*association list lookup, optimized version for string lists*)
   1.117 +fun assoc_string ([], (key:string)) = None
   1.118 +  | assoc_string ((keyi, xi) :: pairs, key) =
   1.119 +      if key = keyi then Some xi else assoc_string (pairs, key);
   1.120 +
   1.121 +(*association list lookup, optimized version for string*int lists*)
   1.122 +fun assoc_string_int ([], (key:string*int)) = None
   1.123 +  | assoc_string_int ((keyi, xi) :: pairs, key) =
   1.124 +      if key = keyi then Some xi else assoc_string_int (pairs, key);
   1.125 +
   1.126  fun assocs ps x =
   1.127    (case assoc (ps, x) of
   1.128      None => []
     2.1 --- a/src/Pure/pattern.ML	Wed Mar 13 11:56:15 1996 +0100
     2.2 +++ b/src/Pure/pattern.ML	Thu Mar 14 10:40:21 1996 +0100
     2.3 @@ -72,7 +72,7 @@
     2.4  fun ints_of []             = []
     2.5    | ints_of (Bound i ::bs) = 
     2.6        let val is = ints_of bs
     2.7 -      in if i mem is then raise Pattern else i::is end
     2.8 +      in if i mem_int is then raise Pattern else i::is end
     2.9    | ints_of _              = raise Pattern;
    2.10  
    2.11  
    2.12 @@ -167,10 +167,10 @@
    2.13  
    2.14  fun flexflex2(env,binders,F,Fty,is,G,Gty,js) =
    2.15    let fun ff(F,Fty,is,G as (a,_),Gty,js) =
    2.16 -            if js subset is
    2.17 +            if js subset_int is
    2.18              then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
    2.19                   in Envir.update((F,t),env) end
    2.20 -            else let val ks = is inter js
    2.21 +            else let val ks = is inter_int js
    2.22                       val Hty = type_of_G(Fty,length is,map (idx is) ks)
    2.23                       val (env',H) = Envir.genvar a (env,Hty)
    2.24                       fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
    2.25 @@ -227,7 +227,7 @@
    2.26  fun eta_contract (Abs(a,T,body)) = 
    2.27        (case eta_contract body  of
    2.28          body' as (f $ Bound i) => 
    2.29 -	  if i=0 andalso not (0 mem loose_bnos f) then incr_boundvars ~1 f 
    2.30 +	  if i=0 andalso not (0 mem_int loose_bnos f) then incr_boundvars ~1 f 
    2.31  	  else Abs(a,T,body')
    2.32        | body' => Abs(a,T,body'))
    2.33    | eta_contract(f$t) = eta_contract f $ eta_contract t
    2.34 @@ -249,7 +249,7 @@
    2.35        fun mtch (tyinsts,insts) = fn
    2.36  	(Var(ixn,T), t)  =>
    2.37  	  if loose_bvar(t,0) then raise MATCH
    2.38 -	  else (case assoc(insts,ixn) of
    2.39 +	  else (case assoc_string_int(insts,ixn) of
    2.40  		  None => (typ_match (tyinsts, (T, fastype_of t)), 
    2.41  			   (ixn,t)::insts)
    2.42  		| Some u => if t aconv u then (tyinsts,insts) else raise MATCH)
    2.43 @@ -270,7 +270,7 @@
    2.44    let val js = loose_bnos t
    2.45    in if null is
    2.46       then if null js then (ixn,t)::itms else raise MATCH
    2.47 -     else if js subset is
    2.48 +     else if js subset_int is
    2.49            then let val t' = if downto0(is,length binders - 1) then t
    2.50                              else mapbnd (idx is) t
    2.51                 in (ixn, mkabs(binders,is,t')) :: itms end
    2.52 @@ -320,7 +320,7 @@
    2.53        in case ph of
    2.54             Var(ixn,_) =>
    2.55               let val is = ints_of pargs
    2.56 -             in case assoc(itms,ixn) of
    2.57 +             in case assoc_string_int(itms,ixn) of
    2.58                    None => (iTs,match_bind(itms,binders,ixn,is,obj))
    2.59                  | Some u => if obj aeconv (red u is []) then env
    2.60                              else raise MATCH
     3.1 --- a/src/Pure/sign.ML	Wed Mar 13 11:56:15 1996 +0100
     3.2 +++ b/src/Pure/sign.ML	Thu Mar 14 10:40:21 1996 +0100
     3.3 @@ -225,7 +225,7 @@
     3.4        Type(_,Ts) => foldl nodup_TVars (tvars,Ts)
     3.5      | TFree _ => tvars
     3.6      | TVar(v as (a,S)) =>
     3.7 -        (case assoc(tvars,a) of
     3.8 +        (case assoc_string_int(tvars,a) of
     3.9             Some(S') => if S=S' then tvars
    3.10                         else raise_type
    3.11                              ("Type variable "^Syntax.string_of_vname a^
    3.12 @@ -238,7 +238,7 @@
    3.13            Const(c,T) => (vars, nodup_TVars(tvars,T))
    3.14          | Free(a,T) => (vars, nodup_TVars(tvars,T))
    3.15          | Var(v as (ixn,T)) =>
    3.16 -            (case assoc(vars,ixn) of
    3.17 +            (case assoc_string_int(vars,ixn) of
    3.18                 Some(T') => if T=T' then (vars,nodup_TVars(tvars,T))
    3.19                             else raise_type
    3.20                               ("Variable "^Syntax.string_of_vname ixn^
     4.1 --- a/src/Pure/thm.ML	Wed Mar 13 11:56:15 1996 +0100
     4.2 +++ b/src/Pure/thm.ML	Thu Mar 14 10:40:21 1996 +0100
     4.3 @@ -1127,7 +1127,7 @@
     4.4    in
     4.5    case findrep cs of
     4.6       c::_ => error ("Bound variables not distinct: " ^ c)
     4.7 -   | [] => (case cs inter freenames of
     4.8 +   | [] => (case cs inter_string freenames of
     4.9         a::_ => error ("Bound/Free variable clash: " ^ a)
    4.10       | [] => fix_shyps [state] []
    4.11  		(Thm{sign = sign,
    4.12 @@ -1173,11 +1173,11 @@
    4.13          val vids = map (#1 o #1 o dest_Var) vars;
    4.14          fun rename(t as Var((x,i),T)) =
    4.15                  (case assoc(al,x) of
    4.16 -                   Some(y) => if x mem vids orelse y mem vids then t
    4.17 +                   Some(y) => if x mem_string vids orelse y mem_string vids then t
    4.18                                else Var((y,i),T)
    4.19                   | None=> t)
    4.20            | rename(Abs(x,T,t)) =
    4.21 -              Abs(case assoc(al,x) of Some(y) => y | None => x,
    4.22 +              Abs(case assoc_string(al,x) of Some(y) => y | None => x,
    4.23                    T, rename t)
    4.24            | rename(f$t) = rename f $ rename t
    4.25            | rename(t) = t;
    4.26 @@ -1528,7 +1528,7 @@
    4.27  fun ren_inst(insts,prop,pat,obj) =
    4.28    let val ren = match_bvs(pat,obj,[])
    4.29        fun renAbs(Abs(x,T,b)) =
    4.30 -            Abs(case assoc(ren,x) of None => x | Some(y) => y, T, renAbs(b))
    4.31 +            Abs(case assoc_string(ren,x) of None => x | Some(y) => y, T, renAbs(b))
    4.32          | renAbs(f$t) = renAbs(f) $ renAbs(t)
    4.33          | renAbs(t) = t
    4.34    in subst_vars insts (if null(ren) then prop else renAbs(prop)) end;
    4.35 @@ -1686,7 +1686,7 @@
    4.36  		   val (h,ts) = strip_comb t
    4.37  	       in case h of
    4.38  		    Const(a,_) =>
    4.39 -		      (case assoc(congs,a) of
    4.40 +		      (case assoc_string(congs,a) of
    4.41  			 None => appc()
    4.42  		       | Some(cong) => (congc (prover mss,sign) cong trec
    4.43                                          handle Pattern.MATCH => appc() ) )