# HG changeset patch # User haftmann # Date 1126542032 -7200 # Node ID d9d50222808e44ffd06122955a16ef8b1039931a # Parent 0a5eebd5ff581687f7bc3317fb95b92d5649a1ef introduced new-style AList operations diff -r 0a5eebd5ff58 -r d9d50222808e src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Mon Sep 12 17:29:07 2005 +0200 +++ b/src/FOL/simpdata.ML Mon Sep 12 18:20:32 2005 +0200 @@ -115,7 +115,7 @@ Const("Trueprop",_) $ p => (case head_of p of Const(a,_) => - (case assoc(pairs,a) of + (case AList.lookup (op =) pairs a of SOME(rls) => List.concat (map atoms ([th] RL rls)) | NONE => [th]) | _ => [th]) diff -r 0a5eebd5ff58 -r d9d50222808e src/FOLP/simp.ML --- a/src/FOLP/simp.ML Mon Sep 12 17:29:07 2005 +0200 +++ b/src/FOLP/simp.ML Mon Sep 12 18:20:32 2005 +0200 @@ -179,7 +179,7 @@ fun add_vars (tm,vars) = case tm of Abs (_,_,body) => add_vars(body,vars) | r$s => (case head_of tm of - Const(c,T) => (case assoc(new_asms,c) of + Const(c,T) => (case AList.lookup (op =) new_asms c of NONE => add_vars(r,add_vars(s,vars)) | SOME(al) => add_list(tm,al,vars)) | _ => add_vars(r,add_vars(s,vars))) diff -r 0a5eebd5ff58 -r d9d50222808e src/FOLP/simpdata.ML --- a/src/FOLP/simpdata.ML Mon Sep 12 17:29:07 2005 +0200 +++ b/src/FOLP/simpdata.ML Mon Sep 12 18:20:32 2005 +0200 @@ -84,7 +84,7 @@ Const("Trueprop",_) $ p => (case head_of p of Const(a,_) => - (case assoc(pairs,a) of + (case AList.lookup (op =) pairs a of SOME(rls) => List.concat (map atoms ([th] RL rls)) | NONE => [th]) | _ => [th]) diff -r 0a5eebd5ff58 -r d9d50222808e src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Mon Sep 12 17:29:07 2005 +0200 +++ b/src/HOL/Tools/datatype_package.ML Mon Sep 12 18:20:32 2005 +0200 @@ -458,7 +458,7 @@ fun count_cases (cs, (_, _, true)) = cs | count_cases (cs, (cname, (_, body), false)) = (case assoc (cs, body) of NONE => (body, [cname]) :: cs - | SOME cnames => overwrite (cs, (body, cnames @ [cname]))); + | SOME cnames => AList.update (op =) (body, cnames @ [cname]) cs); val cases' = sort (int_ord o Library.swap o pairself (length o snd)) (Library.foldl count_cases ([], cases)); fun mk_case1 (cname, (vs, body), _) = Syntax.const "_case1" $ diff -r 0a5eebd5ff58 -r d9d50222808e src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Mon Sep 12 17:29:07 2005 +0200 +++ b/src/HOL/Tools/inductive_package.ML Mon Sep 12 18:20:32 2005 +0200 @@ -230,7 +230,7 @@ fun mg_prod_factors ts (fs, t $ u) = if t mem ts then let val f = prod_factors [] u - in overwrite (fs, (t, f inter (curry getOpt) (assoc (fs, t)) f)) end + in AList.update (op =) (t, f inter (AList.lookup (op =) fs t) |> the_default f) fs end else mg_prod_factors ts (mg_prod_factors ts (fs, t), u) | mg_prod_factors ts (fs, Abs (_, _, t)) = mg_prod_factors ts (fs, t) | mg_prod_factors ts (fs, _) = fs; diff -r 0a5eebd5ff58 -r d9d50222808e src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Mon Sep 12 17:29:07 2005 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Mon Sep 12 18:20:32 2005 +0200 @@ -275,7 +275,7 @@ val _ $ (_ $ _ $ S) = concl_of r; val (Const (s, _), _) = strip_comb S; val rs = getOpt (assoc (rss, s), []); - in overwrite (rss, (s, rs @ [r])) end; + in AList.update (op =) (s, rs @ [r]) rss end; fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) = let diff -r 0a5eebd5ff58 -r d9d50222808e src/HOL/arith_data.ML --- a/src/HOL/arith_data.ML Mon Sep 12 17:29:07 2005 +0200 +++ b/src/HOL/arith_data.ML Mon Sep 12 18:20:32 2005 +0200 @@ -241,8 +241,8 @@ fun nT (Type("fun",[N,_])) = N = HOLogic.natT | nT _ = false; -fun add_atom(t,m,(p,i)) = (case assoc(p,t) of NONE => ((t,m)::p,i) - | SOME n => (overwrite(p,(t,ratadd(n,m))), i)); +fun add_atom(t,m,(p,i)) = (case AList.lookup (op =) p t of NONE => ((t, m) :: p, i) + | SOME n => (AList.update (op =) (t, ratadd (n, m)) p, i)); exception Zero; diff -r 0a5eebd5ff58 -r d9d50222808e src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Mon Sep 12 17:29:07 2005 +0200 +++ b/src/HOL/simpdata.ML Mon Sep 12 18:20:32 2005 +0200 @@ -285,7 +285,7 @@ Const("Trueprop",_) $ p => (case head_of p of Const(a,_) => - (case assoc(pairs,a) of + (case AList.lookup (op =) pairs a of SOME(rls) => List.concat (map atoms ([th] RL rls)) | NONE => [th]) | _ => [th]) diff -r 0a5eebd5ff58 -r d9d50222808e src/HOLCF/domain/extender.ML --- a/src/HOLCF/domain/extender.ML Mon Sep 12 17:29:07 2005 +0200 +++ b/src/HOLCF/domain/extender.ML Mon Sep 12 18:20:32 2005 +0200 @@ -65,14 +65,14 @@ | rm_sorts (TVar(s,_)) = TVar(s,[]) and remove_sorts l = map rm_sorts l; val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"] - fun analyse indirect (TFree(v,s)) = (case assoc_string(tvars,v) of + fun analyse indirect (TFree(v,s)) = (case AList.lookup (op =) tvars v of NONE => error ("Free type variable " ^ quote v ^ " on rhs.") | SOME sort => if eq_set_string (s,defaultS) orelse eq_set_string (s,sort ) then TFree(distinct_name v,sort) else error ("Inconsistent sort constraint" ^ " for type variable " ^ quote v)) - | analyse indirect (t as Type(s,typl)) = (case assoc_string(dtnvs,s)of + | analyse indirect (t as Type(s,typl)) = (case AList.lookup (op =) dtnvs s of NONE => if exists (fn x => x = s) indirect_ok then Type(s,map (analyse false) typl) else Type(s,map (analyse true) typl) diff -r 0a5eebd5ff58 -r d9d50222808e src/HOLCF/domain/library.ML --- a/src/HOLCF/domain/library.ML Mon Sep 12 17:29:07 2005 +0200 +++ b/src/HOLCF/domain/library.ML Mon Sep 12 18:20:32 2005 +0200 @@ -63,7 +63,7 @@ fun mk_var_names ids : string list = let fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s; fun index_vnames(vn::vns,occupied) = - (case assoc(occupied,vn) of + (case AList.lookup (op =) occupied vn of NONE => if vn mem vns then (vn^"1") :: index_vnames(vns,(vn,1) ::occupied) else vn :: index_vnames(vns, occupied) diff -r 0a5eebd5ff58 -r d9d50222808e src/HOLCF/pcpodef_package.ML --- a/src/HOLCF/pcpodef_package.ML Mon Sep 12 17:29:07 2005 +0200 +++ b/src/HOLCF/pcpodef_package.ML Mon Sep 12 18:20:32 2005 +0200 @@ -79,7 +79,7 @@ else HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_nonempty set, mk_admissible set)); (*lhs*) - val lhs_tfrees = map (fn v => (v, getOpt (assoc (rhs_tfrees, v), HOLogic.typeS))) vs; + val lhs_tfrees = map (fn v => (v, AList.lookup (op =) rhs_tfrees v |> the_default HOLogic.typeS)) vs; val lhs_sorts = map snd lhs_tfrees; val tname = Syntax.type_name t mx; val full_tname = full tname; diff -r 0a5eebd5ff58 -r d9d50222808e src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Mon Sep 12 17:29:07 2005 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Mon Sep 12 18:20:32 2005 +0200 @@ -492,7 +492,7 @@ end; fun coeff poly atom : IntInf.int = - case assoc(poly,atom) of NONE => 0 | SOME i => i; + AList.lookup (op =) poly atom |> the_default 0; fun lcms is = Library.foldl lcm (1, is); diff -r 0a5eebd5ff58 -r d9d50222808e src/Provers/splitter.ML --- a/src/Provers/splitter.ML Mon Sep 12 17:29:07 2005 +0200 +++ b/src/Provers/splitter.ML Mon Sep 12 18:20:32 2005 +0200 @@ -332,7 +332,7 @@ (case strip_comb lhs of (Const(a,aT),args) => let val info = (aT,lhs,thm,fastype_of t,length args) in case AList.lookup (op =) cmap a of - SOME infos => overwrite(cmap,(a,info::infos)) + SOME infos => AList.update (op =) (a, info::infos) cmap | NONE => (a,[info])::cmap end | _ => split_format_err()) diff -r 0a5eebd5ff58 -r d9d50222808e src/Pure/drule.ML --- a/src/Pure/drule.ML Mon Sep 12 17:29:07 2005 +0200 +++ b/src/Pure/drule.ML Mon Sep 12 18:20:32 2005 +0200 @@ -302,8 +302,8 @@ val frees = map dest_Free (term_frees big); val tvars = term_tvars big; val tfrees = term_tfrees big; - fun typ(a,i) = if i<0 then assoc(frees,a) else assoc(vars,(a,i)); - fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i)); + fun typ(a,i) = if i<0 then AList.lookup (op =) frees a else AList.lookup (op =) vars (a,i); + fun sort(a,i) = if i<0 then AList.lookup (op =) tfrees a else AList.lookup (op =) tvars (a,i); in (typ,sort) end; fun add_used thm used = @@ -344,7 +344,7 @@ val internalK = "internal"; fun get_kind thm = - (case Library.assoc (#2 (Thm.get_name_tags thm), "kind") of + (case AList.lookup (op =) ((#2 o Thm.get_name_tags) thm) "kind" of SOME (k :: _) => k | _ => "unknown"); @@ -479,7 +479,7 @@ val alist = foldr newName [] vars fun mk_inst (Var(v,T)) = (cterm_of thy (Var(v,T)), - cterm_of thy (Free(valOf (assoc(alist,v)), T))) + cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T))) val insts = map mk_inst vars fun thaw i th' = (*i is non-negative increment for Var indexes*) th' |> forall_intr_list (map #2 insts) @@ -503,7 +503,7 @@ (prop :: Thm.terms_of_tpairs tpairs, [])) vars fun mk_inst (Var(v,T)) = (cterm_of thy (Var(v,T)), - cterm_of thy (Free(valOf (assoc(alist,v)), T))) + cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T))) val insts = map mk_inst vars fun thaw th' = th' |> forall_intr_list (map #2 insts) @@ -999,7 +999,7 @@ | rename_bvars vs thm = let val {thy, prop, ...} = rep_thm thm; - fun ren (Abs (x, T, t)) = Abs (getOpt (assoc (vs, x), x), T, ren t) + fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x |> the_default x, T, ren t) | ren (t $ u) = ren t $ ren u | ren t = t; in equal_elim (reflexive (cterm_of thy (ren prop))) thm end; diff -r 0a5eebd5ff58 -r d9d50222808e src/Pure/goals.ML --- a/src/Pure/goals.ML Mon Sep 12 17:29:07 2005 +0200 +++ b/src/Pure/goals.ML Mon Sep 12 18:20:32 2005 +0200 @@ -310,7 +310,7 @@ (* get theorems *) -fun get_thm_locale name ((_, {thms, ...}: locale)) = assoc (thms, name); +fun get_thm_locale name ((_, {thms, ...}: locale)) = AList.lookup (op =) thms name; fun get_thmx f get thy name = (case get_first (get_thm_locale name) (get_scope thy) of @@ -338,7 +338,7 @@ fun read_typ thy (envT, s) = let - fun def_sort (x, ~1) = assoc (envT, x) + fun def_sort (x, ~1) = AList.lookup (op =) envT x | def_sort _ = NONE; val T = Type.no_tvars (Sign.read_typ (thy, def_sort) s) handle TYPE (msg, _, _) => error msg; in (Term.add_typ_tfrees (T, envT), T) end; @@ -357,9 +357,9 @@ fun read_axm thy ((envS, envT, used), (name, s)) = let - fun def_sort (x, ~1) = assoc (envS, x) + fun def_sort (x, ~1) = AList.lookup (op =) envS x | def_sort _ = NONE; - fun def_type (x, ~1) = assoc (envT, x) + fun def_type (x, ~1) = AList.lookup (op =) envT x | def_type _ = NONE; val (_, t) = Theory.read_def_axm (thy, def_type, def_sort) used (name, s); in @@ -382,9 +382,9 @@ val envS = List.concat (map #1 defaults); val envT = List.concat (map #2 defaults); val used = List.concat (map #3 defaults); - fun def_sort (x, ~1) = assoc (envS, x) + fun def_sort (x, ~1) = AList.lookup (op =) envS x | def_sort _ = NONE; - fun def_type (x, ~1) = assoc (envT, x) + fun def_type (x, ~1) = AList.lookup (op =) envT x | def_type _ = NONE; in (if (is_open_loc thy) then (#1 o read_def_cterm (thy, def_type, def_sort) used true) diff -r 0a5eebd5ff58 -r d9d50222808e src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Mon Sep 12 17:29:07 2005 +0200 +++ b/src/Pure/proofterm.ML Mon Sep 12 18:20:32 2005 +0200 @@ -470,10 +470,10 @@ (**** Freezing and thawing of variables in proof terms ****) fun frzT names = - map_type_tvar (fn (ixn, xs) => TFree (the (assoc (names, ixn)), xs)); + map_type_tvar (fn (ixn, xs) => TFree ((the o AList.lookup (op =) names) ixn, xs)); fun thawT names = - map_type_tfree (fn (s, xs) => case assoc (names, s) of + map_type_tfree (fn (s, xs) => case AList.lookup (op =) names s of NONE => TFree (s, xs) | SOME ixn => TVar (ixn, xs)); @@ -484,7 +484,7 @@ | freeze names names' (Const (s, T)) = Const (s, frzT names' T) | freeze names names' (Free (s, T)) = Free (s, frzT names' T) | freeze names names' (Var (ixn, T)) = - Free (the (assoc (names, ixn)), frzT names' T) + Free ((the o AList.lookup (op =) names) ixn, frzT names' T) | freeze names names' t = t; fun thaw names names' (t $ u) = @@ -494,7 +494,7 @@ | thaw names names' (Const (s, T)) = Const (s, thawT names' T) | thaw names names' (Free (s, T)) = let val T' = thawT names' T - in case assoc (names, s) of + in case AList.lookup (op =) names s of NONE => Free (s, T') | SOME ixn => Var (ixn, T') end @@ -566,7 +566,7 @@ let val v = variant used (string_of_indexname ix) in ((ix, v) :: pairs, v :: used) end; -fun freeze_one alist (ix, sort) = (case assoc (alist, ix) of +fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of NONE => TVar (ix, sort) | SOME name => TFree (name, sort)); @@ -892,7 +892,7 @@ val (ts', ts'') = splitAt (length vs, ts) val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts'; val nvs = Library.foldl (fn (ixns', (ixn, ixns)) => - ixn ins (case assoc (insts, ixn) of + ixn ins (case AList.lookup (op =) insts ixn of SOME (SOME t) => if is_proj t then ixns union ixns' else ixns' | _ => ixns union ixns')) (needed prop ts'' prfs, add_npvars false true [] ([], prop)); @@ -982,7 +982,7 @@ let val substT = Envir.typ_subst_TVars tyinsts; - fun subst' lev (t as Var (ixn, _)) = (case assoc (insts, ixn) of + fun subst' lev (t as Var (ixn, _)) = (case AList.lookup (op =) insts ixn of NONE => t | SOME u => incr_boundvars lev u) | subst' lev (Const (s, T)) = Const (s, substT T) @@ -997,7 +997,7 @@ Abst (a, Option.map substT T, subst plev (tlev+1) body) | subst plev tlev (prf %% prf') = subst plev tlev prf %% subst plev tlev prf' | subst plev tlev (prf % t) = subst plev tlev prf % Option.map (subst' tlev) t - | subst plev tlev (prf as Hyp (Var (ixn, _))) = (case assoc (pinst, ixn) of + | subst plev tlev (prf as Hyp (Var (ixn, _))) = (case AList.lookup (op =) pinst ixn of NONE => prf | SOME prf' => incr_pboundvars plev tlev prf') | subst _ _ (PThm (id, prf, prop, Ts)) = diff -r 0a5eebd5ff58 -r d9d50222808e src/ZF/simpdata.ML --- a/src/ZF/simpdata.ML Mon Sep 12 17:29:07 2005 +0200 +++ b/src/ZF/simpdata.ML Mon Sep 12 18:20:32 2005 +0200 @@ -15,7 +15,7 @@ let fun tryrules pairs t = case head_of t of Const(a,_) => - (case assoc(pairs,a) of + (case AList.lookup (op =) pairs a of SOME rls => List.concat (map (atomize (conn_pairs, mem_pairs)) ([th] RL rls)) | NONE => [th])