use AList operations;
authorwenzelm
Mon Aug 29 16:18:04 2005 +0200 (2005-08-29)
changeset 171843d80209e9a53
parent 17183 a788a05fb81b
child 17185 5140808111d1
use AList operations;
src/HOL/Tools/primrec_package.ML
src/Provers/splitter.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/induct_attrib.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Syntax/printer.ML
src/Pure/sign.ML
src/Pure/sorts.ML
src/Pure/thm.ML
src/Pure/type.ML
     1.1 --- a/src/HOL/Tools/primrec_package.ML	Mon Aug 29 16:18:03 2005 +0200
     1.2 +++ b/src/HOL/Tools/primrec_package.ML	Mon Aug 29 16:18:04 2005 +0200
     1.3 @@ -72,11 +72,11 @@
     1.4       (check_vars "repeated variable names in pattern: " (duplicates lfrees);
     1.5        check_vars "extra variables on rhs: "
     1.6          (map dest_Free (term_frees rhs) \\ lfrees);
     1.7 -      case assoc (rec_fns, fnameT) of
     1.8 +      case AList.lookup (op =) rec_fns fnameT of
     1.9          NONE =>
    1.10            (fnameT, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
    1.11        | SOME (_, rpos', eqns) =>
    1.12 -          if isSome (assoc (eqns, cname)) then
    1.13 +          if AList.defined (op =) eqns cname then
    1.14              raise RecError "constructor already occurred as pattern"
    1.15            else if rpos <> rpos' then
    1.16              raise RecError "position of recursive argument inconsistent"
    1.17 @@ -104,7 +104,7 @@
    1.18              if is_Const f andalso dest_Const f mem map fst rec_eqns then
    1.19                let
    1.20                  val fnameT' as (fname', _) = dest_Const f;
    1.21 -                val (_, rpos, _) = valOf (assoc (rec_eqns, fnameT'));
    1.22 +                val (_, rpos, _) = the (AList.lookup (op =) rec_eqns fnameT');
    1.23                  val ls = Library.take (rpos, ts);
    1.24                  val rest = Library.drop (rpos, ts);
    1.25                  val (x', rs) = (hd rest, tl rest)
    1.26 @@ -112,7 +112,7 @@
    1.27                     \ in recursive application\nof function " ^ quote fname' ^ " on rhs");
    1.28                  val (x, xs) = strip_comb x'
    1.29                in 
    1.30 -                (case assoc (subs, x) of
    1.31 +                (case AList.lookup (op =) subs x of
    1.32                      NONE =>
    1.33                        let
    1.34                          val (fs', ts') = foldl_map (subst subs) (fs, ts)
    1.35 @@ -134,7 +134,7 @@
    1.36      (* translate rec equations into function arguments suitable for rec comb *)
    1.37  
    1.38      fun trans eqns ((cname, cargs), (fnameTs', fnss', fns)) =
    1.39 -      (case assoc (eqns, cname) of
    1.40 +      (case AList.lookup (op =) eqns cname of
    1.41            NONE => (warning ("No equation for constructor " ^ quote cname ^
    1.42              "\nin definition of function " ^ quote fname);
    1.43                (fnameTs', fnss', (Const ("arbitrary", dummyT))::fns))
    1.44 @@ -154,13 +154,13 @@
    1.45  		(list_abs_free (cargs' @ subs @ ls @ rs, rhs'))::fns)
    1.46              end)
    1.47  
    1.48 -  in (case assoc (fnameTs, i) of
    1.49 +  in (case AList.lookup (op =) fnameTs i of
    1.50        NONE =>
    1.51          if exists (equal fnameT o snd) fnameTs then
    1.52            raise RecError ("inconsistent functions for datatype " ^ quote tname)
    1.53          else
    1.54            let
    1.55 -            val (_, _, eqns) = valOf (assoc (rec_eqns, fnameT));
    1.56 +            val (_, _, eqns) = the (AList.lookup (op =) rec_eqns fnameT);
    1.57              val (fnameTs', fnss', fns) = foldr (trans eqns)
    1.58                ((i, fnameT)::fnameTs, fnss, []) constrs
    1.59            in
    1.60 @@ -175,7 +175,7 @@
    1.61  (* prepare functions needed for definitions *)
    1.62  
    1.63  fun get_fns fns (((i, (tname, _, constrs)), rec_name), (fs, defs)) =
    1.64 -  case assoc (fns, i) of
    1.65 +  case AList.lookup (op =) fns i of
    1.66       NONE =>
    1.67         let
    1.68           val dummy_fns = map (fn (_, cargs) => Const ("arbitrary",
    1.69 @@ -216,7 +216,7 @@
    1.70    let
    1.71      fun constrs_of (_, (_, _, cs)) =
    1.72        map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
    1.73 -    val params_of = Library.assocs (List.concat (map constrs_of rec_eqns));
    1.74 +    val params_of = these o AList.lookup (op =) (List.concat (map constrs_of rec_eqns));
    1.75    in
    1.76      induction
    1.77      |> RuleCases.rename_params (map params_of (List.concat (map (map #1 o #3 o #2) descr)))
     2.1 --- a/src/Provers/splitter.ML	Mon Aug 29 16:18:03 2005 +0200
     2.2 +++ b/src/Provers/splitter.ML	Mon Aug 29 16:18:04 2005 +0200
     2.3 @@ -240,7 +240,7 @@
     2.4                               then mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2)
     2.5                               else find tups
     2.6                            end
     2.7 -                in find (assocs cmap c) end
     2.8 +                in find (these (AList.lookup (op =) cmap c)) end
     2.9              | _ => []
    2.10            in snd(Library.foldl iter ((0, a), ts)) end
    2.11    in posns Ts [] [] t end;
    2.12 @@ -331,7 +331,7 @@
    2.13              (case concl_of thm of _$(t as _$lhs)$_ =>
    2.14                 (case strip_comb lhs of (Const(a,aT),args) =>
    2.15                    let val info = (aT,lhs,thm,fastype_of t,length args)
    2.16 -                  in case assoc(cmap,a) of
    2.17 +                  in case AList.lookup (op =) cmap a of
    2.18                         SOME infos => overwrite(cmap,(a,info::infos))
    2.19                       | NONE => (a,[info])::cmap
    2.20                    end
     3.1 --- a/src/Pure/Isar/attrib.ML	Mon Aug 29 16:18:03 2005 +0200
     3.2 +++ b/src/Pure/Isar/attrib.ML	Mon Aug 29 16:18:04 2005 +0200
     3.3 @@ -338,18 +338,18 @@
     3.4      val external_insts''' = xs ~~ ts;
     3.5      val term_insts''' = internal_insts''' @ external_insts''';
     3.6      val thm''' = instantiate thy inferred external_insts''' thm'';
     3.7 -  in
     3.8 +
     3.9  
    3.10      (* assign internalized values *)
    3.11  
    3.12 -    mixed_insts |> List.app (fn (arg, (xi, _)) =>
    3.13 -      if is_tvar xi then
    3.14 -        Args.assign (SOME (Args.Typ (the (assoc (type_insts''', xi))))) arg
    3.15 -      else
    3.16 -        Args.assign (SOME (Args.Term (the (assoc (term_insts''', xi))))) arg);
    3.17 +    val _ =
    3.18 +      mixed_insts |> List.app (fn (arg, (xi, _)) =>
    3.19 +        if is_tvar xi then
    3.20 +          Args.assign (SOME (Args.Typ (the (AList.lookup (op =) type_insts''' xi)))) arg
    3.21 +        else
    3.22 +          Args.assign (SOME (Args.Term (the (AList.lookup (op =) term_insts''' xi)))) arg);
    3.23  
    3.24 -    (context, thm''' |> RuleCases.save thm)
    3.25 -  end;
    3.26 +  in (context, thm''' |> RuleCases.save thm) end;
    3.27  
    3.28  end;
    3.29  
     4.1 --- a/src/Pure/Isar/induct_attrib.ML	Mon Aug 29 16:18:03 2005 +0200
     4.2 +++ b/src/Pure/Isar/induct_attrib.ML	Mon Aug 29 16:18:04 2005 +0200
     4.3 @@ -85,7 +85,7 @@
     4.4    NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
     4.5      Drule.eq_thm_prop (th1, th2));
     4.6  
     4.7 -fun lookup_rule (rs: rules) name = assoc_string (NetRules.rules rs, name);
     4.8 +fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
     4.9  
    4.10  fun print_rules prt kind x rs =
    4.11    let val thms = map snd (NetRules.rules rs)
     5.1 --- a/src/Pure/Isar/isar_thy.ML	Mon Aug 29 16:18:03 2005 +0200
     5.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Aug 29 16:18:04 2005 +0200
     5.3 @@ -143,7 +143,7 @@
     5.4    ("const", (Sign.intern_const, Sign.declared_const, Theory.hide_consts_i))];
     5.5  
     5.6  fun gen_hide int (kind, xnames) thy =
     5.7 -  (case assoc_string (kinds, kind) of
     5.8 +  (case AList.lookup (op =) kinds kind of
     5.9      SOME (intern, check, hide) =>
    5.10        let
    5.11          val names = if int then map (intern thy) xnames else xnames;
     6.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Aug 29 16:18:03 2005 +0200
     6.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Aug 29 16:18:04 2005 +0200
     6.3 @@ -132,7 +132,7 @@
     6.4      SOME (((_, k), _), _) => OuterKeyword.tags_of k
     6.5    | NONE => []);
     6.6  
     6.7 -fun is_markup kind name = (assoc_string (! global_markups, name) = SOME kind);
     6.8 +fun is_markup kind name = (AList.lookup (op =) (! global_markups) name = SOME kind);
     6.9  
    6.10  
    6.11  (* augment syntax *)
     7.1 --- a/src/Pure/Isar/proof_context.ML	Mon Aug 29 16:18:03 2005 +0200
     7.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Aug 29 16:18:04 2005 +0200
     7.3 @@ -406,7 +406,7 @@
     7.4  
     7.5  (* internalize Skolem constants *)
     7.6  
     7.7 -fun lookup_skolem ctxt x = assoc (fixes_of ctxt, x);
     7.8 +val lookup_skolem = AList.lookup (op =) o fixes_of;
     7.9  fun get_skolem ctxt x = if_none (lookup_skolem ctxt x) x;
    7.10  
    7.11  fun no_skolem internal ctxt x =
    7.12 @@ -437,7 +437,7 @@
    7.13      val rev_fixes = map Library.swap (fixes_of ctxt);
    7.14  
    7.15      fun extern (t as Free (x, T)) =
    7.16 -          (case assoc (rev_fixes, x) of
    7.17 +          (case AList.lookup (op =) rev_fixes x of
    7.18              SOME x' => Free (if lookup_skolem ctxt x' = SOME x then x' else NameSpace.hidden x', T)
    7.19            | NONE => t)
    7.20        | extern (t $ u) = extern t $ extern u
    7.21 @@ -1259,7 +1259,7 @@
    7.22  in
    7.23  
    7.24  fun get_case ctxt name xs =
    7.25 -  (case assoc_string (cases_of ctxt, name) of
    7.26 +  (case AList.lookup (op =) (cases_of ctxt) name of
    7.27      NONE => raise CONTEXT ("Unknown case: " ^ quote name, ctxt)
    7.28    | SOME c => prep_case ctxt name xs c);
    7.29  
     8.1 --- a/src/Pure/Isar/rule_cases.ML	Mon Aug 29 16:18:03 2005 +0200
     8.2 +++ b/src/Pure/Isar/rule_cases.ML	Mon Aug 29 16:18:04 2005 +0200
     8.3 @@ -38,7 +38,7 @@
     8.4  
     8.5  fun lookup_consumes thm =
     8.6    let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [thm]) in
     8.7 -    (case Library.assoc (Thm.tags_of_thm thm, consumes_tagN) of
     8.8 +    (case AList.lookup (op =) (Thm.tags_of_thm thm) (consumes_tagN) of
     8.9        NONE => NONE
    8.10      | SOME [s] => (case Syntax.read_nat s of SOME n => SOME n | _ => err ())
    8.11      | _ => err ())
    8.12 @@ -64,7 +64,7 @@
    8.13        |> Drule.untag_rule cases_tagN
    8.14        |> Drule.tag_rule (cases_tagN, names);
    8.15  
    8.16 -fun lookup_case_names thm = Library.assoc (Thm.tags_of_thm thm, cases_tagN);
    8.17 +fun lookup_case_names thm = AList.lookup (op =) (Thm.tags_of_thm thm) cases_tagN;
    8.18  
    8.19  val save_case_names = put_case_names o lookup_case_names;
    8.20  val name = put_case_names o SOME;
     9.1 --- a/src/Pure/Syntax/printer.ML	Mon Aug 29 16:18:03 2005 +0200
     9.2 +++ b/src/Pure/Syntax/printer.ML	Mon Aug 29 16:18:04 2005 +0200
     9.3 @@ -191,8 +191,8 @@
     9.4  
     9.5  type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
     9.6  
     9.7 -fun mode_tab prtabs mode = if_none (assoc (prtabs, mode)) Symtab.empty;
     9.8 -fun mode_tabs prtabs modes = List.mapPartial (curry assoc prtabs) (modes @ [""]);
     9.9 +fun mode_tab prtabs mode = if_none (AList.lookup (op =) prtabs mode) Symtab.empty;
    9.10 +fun mode_tabs prtabs modes = List.mapPartial (AList.lookup (op =) prtabs) (modes @ [""]);
    9.11  
    9.12  
    9.13  (* xprod_to_fmt *)
    10.1 --- a/src/Pure/sign.ML	Mon Aug 29 16:18:03 2005 +0200
    10.2 +++ b/src/Pure/sign.ML	Mon Aug 29 16:18:04 2005 +0200
    10.3 @@ -327,7 +327,7 @@
    10.4    let
    10.5      fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end;
    10.6      val tab = List.mapPartial f' (add_names (t, []));
    10.7 -    fun get x = if_none (assoc_string (tab, x)) x;
    10.8 +    fun get x = if_none (AList.lookup (op =) tab x) x;
    10.9    in get end;
   10.10  
   10.11  fun typ_mapping f g thy T =
    11.1 --- a/src/Pure/sorts.ML	Mon Aug 29 16:18:03 2005 +0200
    11.2 +++ b/src/Pure/sorts.ML	Mon Aug 29 16:18:04 2005 +0200
    11.3 @@ -180,7 +180,7 @@
    11.4  fun mg_domain (classes, arities) a S =
    11.5    let
    11.6      fun dom c =
    11.7 -      (case Library.assoc_string (Symtab.lookup_multi (arities, a), c) of
    11.8 +      (case AList.lookup (op =) (Symtab.lookup_multi (arities, a)) c of
    11.9          NONE => raise DOMAIN (a, c)
   11.10        | SOME Ss => Ss);
   11.11      fun dom_inter c Ss = ListPair.map (inter_sort classes) (dom c, Ss);
    12.1 --- a/src/Pure/thm.ML	Mon Aug 29 16:18:03 2005 +0200
    12.2 +++ b/src/Pure/thm.ML	Mon Aug 29 16:18:04 2005 +0200
    12.3 @@ -1312,12 +1312,12 @@
    12.4          (*unknowns appearing elsewhere be preserved!*)
    12.5          val vids = map (#1 o #1 o dest_Var) vars;
    12.6          fun rename(t as Var((x,i),T)) =
    12.7 -                (case assoc_string (al,x) of
    12.8 +                (case AList.lookup (op =) al x of
    12.9                     SOME(y) => if x mem_string vids orelse y mem_string vids then t
   12.10                                else Var((y,i),T)
   12.11                   | NONE=> t)
   12.12            | rename(Abs(x,T,t)) =
   12.13 -              Abs (if_none (assoc_string (al, x)) x, T, rename t)
   12.14 +              Abs (if_none (AList.lookup (op =) al x) x, T, rename t)
   12.15            | rename(f$t) = rename f $ rename t
   12.16            | rename(t) = t;
   12.17          fun strip_ren Ai = strip_apply rename (Ai,B)
    13.1 --- a/src/Pure/type.ML	Mon Aug 29 16:18:03 2005 +0200
    13.2 +++ b/src/Pure/type.ML	Mon Aug 29 16:18:04 2005 +0200
    13.3 @@ -150,7 +150,7 @@
    13.4  local
    13.5  
    13.6  fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts)
    13.7 -  | inst_typ env (T as TFree (x, _)) = if_none (Library.assoc_string (env, x)) T
    13.8 +  | inst_typ env (T as TFree (x, _)) = if_none (AList.lookup (op =) env x) T
    13.9    | inst_typ _ T = T;
   13.10  
   13.11  fun certify_typ normalize syntax tsig ty =
   13.12 @@ -223,7 +223,7 @@
   13.13      val ixns = add_term_tvar_ixns (t, []);
   13.14      val fmap = fs ~~ map (rpair 0) (variantlist (map fst fs, map #1 ixns))
   13.15      fun thaw (f as (a, S)) =
   13.16 -      (case gen_assoc (op =) (fmap, f) of
   13.17 +      (case AList.lookup (op =) fmap f of
   13.18          NONE => TFree f
   13.19        | SOME xi => TVar (xi, S));
   13.20    in (map_term_types (map_type_tfree thaw) t, fmap) end;
   13.21 @@ -238,11 +238,11 @@
   13.22    in ((ix, v) :: pairs, v :: used) end;
   13.23  
   13.24  fun freeze_one alist (ix, sort) =
   13.25 -  TFree (the (assoc_string_int (alist, ix)), sort)
   13.26 +  TFree (the (AList.lookup (op =) alist ix), sort)
   13.27      handle Option =>
   13.28        raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);
   13.29  
   13.30 -fun thaw_one alist (a, sort) = TVar (the (assoc_string (alist, a)), sort)
   13.31 +fun thaw_one alist (a, sort) = TVar (the (AList.lookup (op =) alist a), sort)
   13.32    handle Option => TFree (a, sort);
   13.33  
   13.34  in
   13.35 @@ -464,7 +464,7 @@
   13.36    end;
   13.37  
   13.38  fun insert pp C t (c, Ss) ars =
   13.39 -  (case assoc_string (ars, c) of
   13.40 +  (case AList.lookup (op =) ars c of
   13.41      NONE => coregular pp C t (c, Ss) ars
   13.42    | SOME Ss' =>
   13.43        if Sorts.sorts_le C (Ss, Ss') then ars