introduced new-style AList operations
authorhaftmann
Mon Sep 12 18:20:32 2005 +0200 (2005-09-12)
changeset 17325d9d50222808e
parent 17324 0a5eebd5ff58
child 17326 9fe23a5bb021
introduced new-style AList operations
src/FOL/simpdata.ML
src/FOLP/simp.ML
src/FOLP/simpdata.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/arith_data.ML
src/HOL/simpdata.ML
src/HOLCF/domain/extender.ML
src/HOLCF/domain/library.ML
src/HOLCF/pcpodef_package.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/splitter.ML
src/Pure/drule.ML
src/Pure/goals.ML
src/Pure/proofterm.ML
src/ZF/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Mon Sep 12 17:29:07 2005 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Mon Sep 12 18:20:32 2005 +0200
     1.3 @@ -115,7 +115,7 @@
     1.4             Const("Trueprop",_) $ p =>
     1.5               (case head_of p of
     1.6                  Const(a,_) =>
     1.7 -                  (case assoc(pairs,a) of
     1.8 +                  (case AList.lookup (op =) pairs a of
     1.9                       SOME(rls) => List.concat (map atoms ([th] RL rls))
    1.10                     | NONE => [th])
    1.11                | _ => [th])
     2.1 --- a/src/FOLP/simp.ML	Mon Sep 12 17:29:07 2005 +0200
     2.2 +++ b/src/FOLP/simp.ML	Mon Sep 12 18:20:32 2005 +0200
     2.3 @@ -179,7 +179,7 @@
     2.4          fun add_vars (tm,vars) = case tm of
     2.5                    Abs (_,_,body) => add_vars(body,vars)
     2.6                  | r$s => (case head_of tm of
     2.7 -                          Const(c,T) => (case assoc(new_asms,c) of
     2.8 +                          Const(c,T) => (case AList.lookup (op =) new_asms c of
     2.9                                    NONE => add_vars(r,add_vars(s,vars))
    2.10                                  | SOME(al) => add_list(tm,al,vars))
    2.11                          | _ => add_vars(r,add_vars(s,vars)))
     3.1 --- a/src/FOLP/simpdata.ML	Mon Sep 12 17:29:07 2005 +0200
     3.2 +++ b/src/FOLP/simpdata.ML	Mon Sep 12 18:20:32 2005 +0200
     3.3 @@ -84,7 +84,7 @@
     3.4             Const("Trueprop",_) $ p =>
     3.5               (case head_of p of
     3.6                  Const(a,_) =>
     3.7 -                  (case assoc(pairs,a) of
     3.8 +                  (case AList.lookup (op =) pairs a of
     3.9                       SOME(rls) => List.concat (map atoms ([th] RL rls))
    3.10                     | NONE => [th])
    3.11                | _ => [th])
     4.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Sep 12 17:29:07 2005 +0200
     4.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Sep 12 18:20:32 2005 +0200
     4.3 @@ -458,7 +458,7 @@
     4.4      fun count_cases (cs, (_, _, true)) = cs
     4.5        | count_cases (cs, (cname, (_, body), false)) = (case assoc (cs, body) of
     4.6            NONE => (body, [cname]) :: cs
     4.7 -        | SOME cnames => overwrite (cs, (body, cnames @ [cname])));
     4.8 +        | SOME cnames => AList.update (op =) (body, cnames @ [cname]) cs);
     4.9      val cases' = sort (int_ord o Library.swap o pairself (length o snd))
    4.10        (Library.foldl count_cases ([], cases));
    4.11      fun mk_case1 (cname, (vs, body), _) = Syntax.const "_case1" $
     5.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Sep 12 17:29:07 2005 +0200
     5.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Sep 12 18:20:32 2005 +0200
     5.3 @@ -230,7 +230,7 @@
     5.4  
     5.5  fun mg_prod_factors ts (fs, t $ u) = if t mem ts then
     5.6          let val f = prod_factors [] u
     5.7 -        in overwrite (fs, (t, f inter (curry getOpt) (assoc (fs, t)) f)) end
     5.8 +        in AList.update (op =) (t, f inter (AList.lookup (op =) fs t) |> the_default f) fs end
     5.9        else mg_prod_factors ts (mg_prod_factors ts (fs, t), u)
    5.10    | mg_prod_factors ts (fs, Abs (_, _, t)) = mg_prod_factors ts (fs, t)
    5.11    | mg_prod_factors ts (fs, _) = fs;
     6.1 --- a/src/HOL/Tools/inductive_realizer.ML	Mon Sep 12 17:29:07 2005 +0200
     6.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Mon Sep 12 18:20:32 2005 +0200
     6.3 @@ -275,7 +275,7 @@
     6.4      val _ $ (_ $ _ $ S) = concl_of r;
     6.5      val (Const (s, _), _) = strip_comb S;
     6.6      val rs = getOpt (assoc (rss, s), []);
     6.7 -  in overwrite (rss, (s, rs @ [r])) end;
     6.8 +  in AList.update (op =) (s, rs @ [r]) rss end;
     6.9  
    6.10  fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
    6.11    let
     7.1 --- a/src/HOL/arith_data.ML	Mon Sep 12 17:29:07 2005 +0200
     7.2 +++ b/src/HOL/arith_data.ML	Mon Sep 12 18:20:32 2005 +0200
     7.3 @@ -241,8 +241,8 @@
     7.4  fun nT (Type("fun",[N,_])) = N = HOLogic.natT
     7.5    | nT _ = false;
     7.6  
     7.7 -fun add_atom(t,m,(p,i)) = (case assoc(p,t) of NONE => ((t,m)::p,i)
     7.8 -                           | SOME n => (overwrite(p,(t,ratadd(n,m))), i));
     7.9 +fun add_atom(t,m,(p,i)) = (case AList.lookup (op =) p t of NONE => ((t, m) :: p, i)
    7.10 +                           | SOME n => (AList.update (op =) (t, ratadd (n, m)) p, i));
    7.11  
    7.12  exception Zero;
    7.13  
     8.1 --- a/src/HOL/simpdata.ML	Mon Sep 12 17:29:07 2005 +0200
     8.2 +++ b/src/HOL/simpdata.ML	Mon Sep 12 18:20:32 2005 +0200
     8.3 @@ -285,7 +285,7 @@
     8.4             Const("Trueprop",_) $ p =>
     8.5               (case head_of p of
     8.6                  Const(a,_) =>
     8.7 -                  (case assoc(pairs,a) of
     8.8 +                  (case AList.lookup (op =) pairs a of
     8.9                       SOME(rls) => List.concat (map atoms ([th] RL rls))
    8.10                     | NONE => [th])
    8.11                | _ => [th])
     9.1 --- a/src/HOLCF/domain/extender.ML	Mon Sep 12 17:29:07 2005 +0200
     9.2 +++ b/src/HOLCF/domain/extender.ML	Mon Sep 12 18:20:32 2005 +0200
     9.3 @@ -65,14 +65,14 @@
     9.4  	|   rm_sorts (TVar(s,_))  = TVar(s,[])
     9.5  	and remove_sorts l = map rm_sorts l;
     9.6  	val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
     9.7 -	fun analyse indirect (TFree(v,s))  = (case assoc_string(tvars,v) of 
     9.8 +	fun analyse indirect (TFree(v,s))  = (case AList.lookup (op =) tvars v of 
     9.9  		    NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
    9.10  	          | SOME sort => if eq_set_string (s,defaultS) orelse
    9.11  				    eq_set_string (s,sort    )
    9.12  				 then TFree(distinct_name v,sort)
    9.13  				 else error ("Inconsistent sort constraint" ^
    9.14  				             " for type variable " ^ quote v))
    9.15 -        |   analyse indirect (t as Type(s,typl)) = (case assoc_string(dtnvs,s)of
    9.16 +        |   analyse indirect (t as Type(s,typl)) = (case AList.lookup (op =) dtnvs s of
    9.17  		NONE          => if exists (fn x => x = s) indirect_ok
    9.18  				 then Type(s,map (analyse false) typl)
    9.19  				 else Type(s,map (analyse true) typl)
    10.1 --- a/src/HOLCF/domain/library.ML	Mon Sep 12 17:29:07 2005 +0200
    10.2 +++ b/src/HOLCF/domain/library.ML	Mon Sep 12 18:20:32 2005 +0200
    10.3 @@ -63,7 +63,7 @@
    10.4  fun mk_var_names ids : string list = let
    10.5      fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s;
    10.6      fun index_vnames(vn::vns,occupied) =
    10.7 -          (case assoc(occupied,vn) of
    10.8 +          (case AList.lookup (op =) occupied vn of
    10.9               NONE => if vn mem vns
   10.10                       then (vn^"1") :: index_vnames(vns,(vn,1)  ::occupied)
   10.11                       else  vn      :: index_vnames(vns,          occupied)
    11.1 --- a/src/HOLCF/pcpodef_package.ML	Mon Sep 12 17:29:07 2005 +0200
    11.2 +++ b/src/HOLCF/pcpodef_package.ML	Mon Sep 12 18:20:32 2005 +0200
    11.3 @@ -79,7 +79,7 @@
    11.4        else HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_nonempty set, mk_admissible set));
    11.5    
    11.6      (*lhs*)
    11.7 -    val lhs_tfrees = map (fn v => (v, getOpt (assoc (rhs_tfrees, v), HOLogic.typeS))) vs;
    11.8 +    val lhs_tfrees = map (fn v => (v, AList.lookup (op =) rhs_tfrees v |> the_default HOLogic.typeS)) vs;
    11.9      val lhs_sorts = map snd lhs_tfrees;
   11.10      val tname = Syntax.type_name t mx;
   11.11      val full_tname = full tname;
    12.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Mon Sep 12 17:29:07 2005 +0200
    12.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Sep 12 18:20:32 2005 +0200
    12.3 @@ -492,7 +492,7 @@
    12.4  end;
    12.5  
    12.6  fun coeff poly atom : IntInf.int =
    12.7 -  case assoc(poly,atom) of NONE => 0 | SOME i => i;
    12.8 +  AList.lookup (op =) poly atom |> the_default 0;
    12.9  
   12.10  fun lcms is = Library.foldl lcm (1, is);
   12.11  
    13.1 --- a/src/Provers/splitter.ML	Mon Sep 12 17:29:07 2005 +0200
    13.2 +++ b/src/Provers/splitter.ML	Mon Sep 12 18:20:32 2005 +0200
    13.3 @@ -332,7 +332,7 @@
    13.4                 (case strip_comb lhs of (Const(a,aT),args) =>
    13.5                    let val info = (aT,lhs,thm,fastype_of t,length args)
    13.6                    in case AList.lookup (op =) cmap a of
    13.7 -                       SOME infos => overwrite(cmap,(a,info::infos))
    13.8 +                       SOME infos => AList.update (op =) (a, info::infos) cmap
    13.9                       | NONE => (a,[info])::cmap
   13.10                    end
   13.11                  | _ => split_format_err())
    14.1 --- a/src/Pure/drule.ML	Mon Sep 12 17:29:07 2005 +0200
    14.2 +++ b/src/Pure/drule.ML	Mon Sep 12 18:20:32 2005 +0200
    14.3 @@ -302,8 +302,8 @@
    14.4          val frees = map dest_Free (term_frees big);
    14.5          val tvars = term_tvars big;
    14.6          val tfrees = term_tfrees big;
    14.7 -        fun typ(a,i) = if i<0 then assoc(frees,a) else assoc(vars,(a,i));
    14.8 -        fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i));
    14.9 +        fun typ(a,i) = if i<0 then AList.lookup (op =) frees a else AList.lookup (op =) vars (a,i);
   14.10 +        fun sort(a,i) = if i<0 then AList.lookup (op =) tfrees a else AList.lookup (op =) tvars (a,i);
   14.11      in (typ,sort) end;
   14.12  
   14.13  fun add_used thm used =
   14.14 @@ -344,7 +344,7 @@
   14.15  val internalK = "internal";
   14.16  
   14.17  fun get_kind thm =
   14.18 -  (case Library.assoc (#2 (Thm.get_name_tags thm), "kind") of
   14.19 +  (case AList.lookup (op =) ((#2 o Thm.get_name_tags) thm) "kind" of
   14.20      SOME (k :: _) => k
   14.21    | _ => "unknown");
   14.22  
   14.23 @@ -479,7 +479,7 @@
   14.24               val alist = foldr newName [] vars
   14.25               fun mk_inst (Var(v,T)) =
   14.26                   (cterm_of thy (Var(v,T)),
   14.27 -                  cterm_of thy (Free(valOf (assoc(alist,v)), T)))
   14.28 +                  cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
   14.29               val insts = map mk_inst vars
   14.30               fun thaw i th' = (*i is non-negative increment for Var indexes*)
   14.31                   th' |> forall_intr_list (map #2 insts)
   14.32 @@ -503,7 +503,7 @@
   14.33                 (prop :: Thm.terms_of_tpairs tpairs, [])) vars
   14.34               fun mk_inst (Var(v,T)) =
   14.35                   (cterm_of thy (Var(v,T)),
   14.36 -                  cterm_of thy (Free(valOf (assoc(alist,v)), T)))
   14.37 +                  cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
   14.38               val insts = map mk_inst vars
   14.39               fun thaw th' =
   14.40                   th' |> forall_intr_list (map #2 insts)
   14.41 @@ -999,7 +999,7 @@
   14.42    | rename_bvars vs thm =
   14.43      let
   14.44        val {thy, prop, ...} = rep_thm thm;
   14.45 -      fun ren (Abs (x, T, t)) = Abs (getOpt (assoc (vs, x), x), T, ren t)
   14.46 +      fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x |> the_default x, T, ren t)
   14.47          | ren (t $ u) = ren t $ ren u
   14.48          | ren t = t;
   14.49      in equal_elim (reflexive (cterm_of thy (ren prop))) thm end;
    15.1 --- a/src/Pure/goals.ML	Mon Sep 12 17:29:07 2005 +0200
    15.2 +++ b/src/Pure/goals.ML	Mon Sep 12 18:20:32 2005 +0200
    15.3 @@ -310,7 +310,7 @@
    15.4  
    15.5  (* get theorems *)
    15.6  
    15.7 -fun get_thm_locale name ((_, {thms, ...}: locale)) = assoc (thms, name);
    15.8 +fun get_thm_locale name ((_, {thms, ...}: locale)) = AList.lookup (op =) thms name;
    15.9  
   15.10  fun get_thmx f get thy name =
   15.11    (case get_first (get_thm_locale name) (get_scope thy) of
   15.12 @@ -338,7 +338,7 @@
   15.13  
   15.14  fun read_typ thy (envT, s) =
   15.15    let
   15.16 -    fun def_sort (x, ~1) = assoc (envT, x)
   15.17 +    fun def_sort (x, ~1) = AList.lookup (op =) envT x
   15.18        | def_sort _ = NONE;
   15.19      val T = Type.no_tvars (Sign.read_typ (thy, def_sort) s) handle TYPE (msg, _, _) => error msg;
   15.20    in (Term.add_typ_tfrees (T, envT), T) end;
   15.21 @@ -357,9 +357,9 @@
   15.22  
   15.23  fun read_axm thy ((envS, envT, used), (name, s)) =
   15.24    let
   15.25 -    fun def_sort (x, ~1) = assoc (envS, x)
   15.26 +    fun def_sort (x, ~1) = AList.lookup (op =) envS x
   15.27        | def_sort _ = NONE;
   15.28 -    fun def_type (x, ~1) = assoc (envT, x)
   15.29 +    fun def_type (x, ~1) = AList.lookup (op =) envT x
   15.30        | def_type _ = NONE;
   15.31      val (_, t) = Theory.read_def_axm (thy, def_type, def_sort) used (name, s);
   15.32    in
   15.33 @@ -382,9 +382,9 @@
   15.34          val envS = List.concat (map #1 defaults);
   15.35          val envT = List.concat (map #2 defaults);
   15.36          val used = List.concat (map #3 defaults);
   15.37 -        fun def_sort (x, ~1) = assoc (envS, x)
   15.38 +        fun def_sort (x, ~1) = AList.lookup (op =) envS x
   15.39            | def_sort _ = NONE;
   15.40 -        fun def_type (x, ~1) = assoc (envT, x)
   15.41 +        fun def_type (x, ~1) = AList.lookup (op =) envT x
   15.42            | def_type _ = NONE;
   15.43      in (if (is_open_loc thy)
   15.44          then (#1 o read_def_cterm (thy, def_type, def_sort) used true)
    16.1 --- a/src/Pure/proofterm.ML	Mon Sep 12 17:29:07 2005 +0200
    16.2 +++ b/src/Pure/proofterm.ML	Mon Sep 12 18:20:32 2005 +0200
    16.3 @@ -470,10 +470,10 @@
    16.4  (**** Freezing and thawing of variables in proof terms ****)
    16.5  
    16.6  fun frzT names =
    16.7 -  map_type_tvar (fn (ixn, xs) => TFree (the (assoc (names, ixn)), xs));
    16.8 +  map_type_tvar (fn (ixn, xs) => TFree ((the o AList.lookup (op =) names) ixn, xs));
    16.9  
   16.10  fun thawT names =
   16.11 -  map_type_tfree (fn (s, xs) => case assoc (names, s) of
   16.12 +  map_type_tfree (fn (s, xs) => case AList.lookup (op =) names s of
   16.13        NONE => TFree (s, xs)
   16.14      | SOME ixn => TVar (ixn, xs));
   16.15  
   16.16 @@ -484,7 +484,7 @@
   16.17    | freeze names names' (Const (s, T)) = Const (s, frzT names' T)
   16.18    | freeze names names' (Free (s, T)) = Free (s, frzT names' T)
   16.19    | freeze names names' (Var (ixn, T)) =
   16.20 -      Free (the (assoc (names, ixn)), frzT names' T)
   16.21 +      Free ((the o AList.lookup (op =) names) ixn, frzT names' T)
   16.22    | freeze names names' t = t;
   16.23  
   16.24  fun thaw names names' (t $ u) =
   16.25 @@ -494,7 +494,7 @@
   16.26    | thaw names names' (Const (s, T)) = Const (s, thawT names' T)
   16.27    | thaw names names' (Free (s, T)) = 
   16.28        let val T' = thawT names' T
   16.29 -      in case assoc (names, s) of
   16.30 +      in case AList.lookup (op =) names s of
   16.31            NONE => Free (s, T')
   16.32          | SOME ixn => Var (ixn, T')
   16.33        end
   16.34 @@ -566,7 +566,7 @@
   16.35    let val v = variant used (string_of_indexname ix)
   16.36    in  ((ix, v) :: pairs, v :: used)  end;
   16.37  
   16.38 -fun freeze_one alist (ix, sort) = (case assoc (alist, ix) of
   16.39 +fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of
   16.40      NONE => TVar (ix, sort)
   16.41    | SOME name => TFree (name, sort));
   16.42  
   16.43 @@ -892,7 +892,7 @@
   16.44          val (ts', ts'') = splitAt (length vs, ts)
   16.45          val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
   16.46          val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
   16.47 -          ixn ins (case assoc (insts, ixn) of
   16.48 +          ixn ins (case AList.lookup (op =) insts ixn of
   16.49                SOME (SOME t) => if is_proj t then ixns union ixns' else ixns'
   16.50              | _ => ixns union ixns'))
   16.51                (needed prop ts'' prfs, add_npvars false true [] ([], prop));
   16.52 @@ -982,7 +982,7 @@
   16.53    let
   16.54      val substT = Envir.typ_subst_TVars tyinsts;
   16.55  
   16.56 -    fun subst' lev (t as Var (ixn, _)) = (case assoc (insts, ixn) of
   16.57 +    fun subst' lev (t as Var (ixn, _)) = (case AList.lookup (op =) insts ixn of
   16.58            NONE => t
   16.59          | SOME u => incr_boundvars lev u)
   16.60        | subst' lev (Const (s, T)) = Const (s, substT T)
   16.61 @@ -997,7 +997,7 @@
   16.62            Abst (a, Option.map substT T, subst plev (tlev+1) body)
   16.63        | subst plev tlev (prf %% prf') = subst plev tlev prf %% subst plev tlev prf'
   16.64        | subst plev tlev (prf % t) = subst plev tlev prf % Option.map (subst' tlev) t
   16.65 -      | subst plev tlev (prf as Hyp (Var (ixn, _))) = (case assoc (pinst, ixn) of
   16.66 +      | subst plev tlev (prf as Hyp (Var (ixn, _))) = (case AList.lookup (op =) pinst ixn of
   16.67            NONE => prf
   16.68          | SOME prf' => incr_pboundvars plev tlev prf')
   16.69        | subst _ _ (PThm (id, prf, prop, Ts)) =
    17.1 --- a/src/ZF/simpdata.ML	Mon Sep 12 17:29:07 2005 +0200
    17.2 +++ b/src/ZF/simpdata.ML	Mon Sep 12 18:20:32 2005 +0200
    17.3 @@ -15,7 +15,7 @@
    17.4    let fun tryrules pairs t =
    17.5            case head_of t of
    17.6                Const(a,_) =>
    17.7 -                (case assoc(pairs,a) of
    17.8 +                (case AList.lookup (op =) pairs a of
    17.9                       SOME rls => List.concat (map (atomize (conn_pairs, mem_pairs))
   17.10                                         ([th] RL rls))
   17.11                     | NONE     => [th])