introduced AList module in favor of assoc etc.
--- a/src/FOL/eqrule_FOL_data.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/FOL/eqrule_FOL_data.ML Tue Sep 20 16:17:34 2005 +0200
@@ -36,8 +36,8 @@
Const("Trueprop",_) $ p =>
(case Term.head_of p of
Const(a,_) =>
- (case Library.assoc(pairs,a) of
- SOME(rls) => List.concat (map atoms ([th] RL rls))
+ (case AList.lookup (op =) pairs a of
+ SOME rls => List.concat (map atoms ([th] RL rls))
| NONE => [th])
| _ => [th])
| _ => [th])
--- a/src/HOL/Integ/cooper_dec.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Integ/cooper_dec.ML Tue Sep 20 16:17:34 2005 +0200
@@ -467,12 +467,12 @@
else HOLogic.false_const)
handle _ => at)
else
- case assoc (operations,p) of
+ case AList.lookup (op =) operations p of
SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)
handle _ => at)
| _ => at)
|Const("Not",_)$(Const (p,_) $ s $ t) =>(
- case assoc (operations,p) of
+ case AList.lookup (op =) operations p of
SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then
HOLogic.false_const else HOLogic.true_const)
handle _ => at)
--- a/src/HOL/Integ/reflected_cooper.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Integ/reflected_cooper.ML Tue Sep 20 16:17:34 2005 +0200
@@ -10,7 +10,7 @@
fun i_of_term vs t =
case t of
- Free(xn,xT) => (case assoc(vs,t) of
+ Free(xn,xT) => (case AList.lookup (op =) vs t of
NONE => error "Variable not found in the list!!"
| SOME n => Var n)
| Const("0",iT) => Cst 0
--- a/src/HOL/Matrix/cplex/Cplex_tools.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Matrix/cplex/Cplex_tools.ML Tue Sep 20 16:17:34 2005 +0200
@@ -969,10 +969,10 @@
val header = readHeader ()
val result =
- case assoc (header, "STATUS") of
+ case AList.lookup (op =) header "STATUS" of
SOME "INFEASIBLE" => Infeasible
| SOME "UNBOUNDED" => Unbounded
- | SOME "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")),
+ | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
(skip_until_sep ();
skip_until_sep ();
load_values ()))
@@ -1118,10 +1118,10 @@
val header = readHeader ()
val result =
- case assoc (header, "STATUS") of
+ case AList.lookup (op =) header "STATUS" of
SOME "INFEASIBLE" => Infeasible
| SOME "NONOPTIMAL" => Unbounded
- | SOME "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")),
+ | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
(skip_paragraph ();
skip_paragraph ();
skip_paragraph ();
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML Tue Sep 20 16:17:34 2005 +0200
@@ -467,12 +467,12 @@
else HOLogic.false_const)
handle _ => at)
else
- case assoc (operations,p) of
+ case AList.lookup (op =) operations p of
SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)
handle _ => at)
| _ => at)
|Const("Not",_)$(Const (p,_) $ s $ t) =>(
- case assoc (operations,p) of
+ case AList.lookup (op =) operations p of
SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then
HOLogic.false_const else HOLogic.true_const)
handle _ => at)
--- a/src/HOL/Tools/Presburger/reflected_cooper.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/Presburger/reflected_cooper.ML Tue Sep 20 16:17:34 2005 +0200
@@ -10,7 +10,7 @@
fun i_of_term vs t =
case t of
- Free(xn,xT) => (case assoc(vs,t) of
+ Free(xn,xT) => (case AList.lookup (op =) vs t of
NONE => error "Variable not found in the list!!"
| SOME n => Var n)
| Const("0",iT) => Cst 0
--- a/src/HOL/Tools/datatype_codegen.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Tue Sep 20 16:17:34 2005 +0200
@@ -26,7 +26,7 @@
fun find_nonempty (descr: DatatypeAux.descr) is i =
let
- val (_, _, constrs) = valOf (assoc (descr, i));
+ val (_, _, constrs) = valOf (AList.lookup (op =) descr i);
fun arg_nonempty (_, DatatypeAux.DtRec i) = if i mem is then NONE
else Option.map (curry op + 1 o snd) (find_nonempty descr (i::is) i)
| arg_nonempty _ = SOME 0;
@@ -160,7 +160,7 @@
[Pretty.block [Pretty.str "(case", Pretty.brk 1,
Pretty.str "i", Pretty.brk 1, Pretty.str "of",
Pretty.brk 1, Pretty.str "0 =>", Pretty.brk 1,
- mk_constr "0" true (cname, valOf (assoc (cs, cname))),
+ mk_constr "0" true (cname, valOf (AList.lookup (op =) cs cname)),
Pretty.brk 1, Pretty.str "| _ =>", Pretty.brk 1,
mk_choice cs1, Pretty.str ")"]]
else [mk_choice cs2])) ::
@@ -263,15 +263,15 @@
(c as Const (s, T), ts) =>
(case find_first (fn (_, {index, descr, case_name, ...}) =>
s = case_name orelse
- isSome (assoc (#3 (valOf (assoc (descr, index))), s)))
+ AList.defined (op =) ((#3 o the o AList.lookup (op =) descr) index) s)
(Symtab.dest (DatatypePackage.get_datatypes thy)) of
NONE => NONE
| SOME (tname, {index, descr, ...}) =>
if isSome (get_assoc_code thy s T) then NONE else
- let val SOME (_, _, constrs) = assoc (descr, index)
- in (case (assoc (constrs, s), strip_type T) of
+ let val SOME (_, _, constrs) = AList.lookup (op =) descr index
+ in (case (AList.lookup (op =) constrs s, strip_type T) of
(NONE, _) => SOME (pretty_case thy defs gr dep module brack
- (#3 (valOf (assoc (descr, index)))) c ts)
+ (#3 (valOf (AList.lookup (op =) descr index))) c ts)
| (SOME args, (_, Type _)) => SOME (pretty_constr thy defs
(fst (invoke_tycodegen thy defs dep module false
(gr, snd (strip_type T))))
--- a/src/HOL/Tools/datatype_package.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML Tue Sep 20 16:17:34 2005 +0200
@@ -112,7 +112,7 @@
fun constrs_of thy tname = (case datatype_info thy tname of
SOME {index, descr, ...} =>
- let val (_, _, constrs) = valOf (assoc (descr, index))
+ let val (_, _, constrs) = valOf (AList.lookup (op =) descr index)
in SOME (map (fn (cname, _) => Const (cname, Sign.the_const_type thy cname)) constrs)
end
| _ => NONE);
@@ -126,7 +126,7 @@
fun find_tname var Bi =
let val frees = map dest_Free (term_frees Bi)
val params = rename_wrt_term Bi (Logic.strip_params Bi);
- in case assoc (frees @ params, var) of
+ in case AList.lookup (op =) (frees @ params) var of
NONE => error ("No such variable in subgoal: " ^ quote var)
| SOME(Type (tn, _)) => tn
| _ => error ("Cannot determine type of " ^ quote var)
@@ -139,7 +139,7 @@
val params = Logic.strip_params Bi; (*params of subgoal i*)
val params = rev (rename_wrt_term Bi params); (*as they are printed*)
val (types, sorts) = types_sorts state;
- fun types' (a, ~1) = (case assoc (params, a) of NONE => types(a, ~1) | sm => sm)
+ fun types' (a, ~1) = (case AList.lookup (op =) params a of NONE => types(a, ~1) | sm => sm)
| types' ixn = types ixn;
val (ct, _) = read_def_cterm (sign, types', sorts) [] false (aterm, TypeInfer.logicT);
in case #T (rep_cterm ct) of
@@ -261,7 +261,7 @@
fun dt_cases (descr: descr) (_, args, constrs) =
let
- fun the_bname i = Sign.base_name (#1 (valOf (assoc (descr, i))));
+ fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i)));
val bnames = map the_bname (distinct (List.concat (map dt_recs args)));
in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
@@ -269,7 +269,7 @@
fun induct_cases descr =
DatatypeProp.indexify_names (List.concat (map (dt_cases descr) (map #2 descr)));
-fun exhaust_cases descr i = dt_cases descr (valOf (assoc (descr, i)));
+fun exhaust_cases descr i = dt_cases descr (valOf (AList.lookup (op =) descr i));
in
@@ -456,7 +456,7 @@
strip_abs (length dts) t, is_dependent (length dts) t))
(constrs ~~ fs);
fun count_cases (cs, (_, _, true)) = cs
- | count_cases (cs, (cname, (_, body), false)) = (case assoc (cs, body) of
+ | count_cases (cs, (cname, (_, body), false)) = (case AList.lookup (op =) cs body of
NONE => (body, [cname]) :: cs
| SOME cnames => AList.update (op =) (body, cnames @ [cname]) cs);
val cases' = sort (int_ord o Library.swap o pairself (length o snd))
@@ -489,7 +489,7 @@
fun read_typ sign ((Ts, sorts), str) =
let
- val T = Type.no_tvars (Sign.read_typ (sign, (curry assoc)
+ val T = Type.no_tvars (Sign.read_typ (sign, AList.lookup (op =)
(map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
--- a/src/HOL/Tools/datatype_prop.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/datatype_prop.ML Tue Sep 20 16:17:34 2005 +0200
@@ -44,7 +44,7 @@
fun indexify_names names =
let
fun index (x :: xs) tab =
- (case assoc (tab, x) of
+ (case AList.lookup (op =) tab x of
NONE => if x mem xs then (x ^ "1") :: index xs ((x, 2) :: tab) else x :: index xs tab
| SOME i => (x ^ Library.string_of_int i) :: index xs ((x, i + 1) :: tab))
| index [] _ = [];
--- a/src/HOL/Tools/datatype_realizer.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Tue Sep 20 16:17:34 2005 +0200
@@ -141,7 +141,7 @@
val rvs = Drule.vars_of_terms [prop_of thm'];
val ivs1 = map Var (filter_out (fn (_, T) =>
tname_of (body_type T) mem ["set", "bool"]) ivs);
- val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (assoc (rvs, ixn)))) ivs;
+ val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs;
val prf = foldr forall_intr_prf
(foldr (fn ((f, p), prf) =>
@@ -182,7 +182,7 @@
list_comb (r, free_ts)))))
end;
- val SOME (_, _, constrs) = assoc (descr, index);
+ val SOME (_, _, constrs) = AList.lookup (op =) descr index;
val T = List.nth (get_rec_types descr sorts, index);
val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
val r = Const (case_name, map fastype_of rs ---> T --> rT);
--- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Sep 20 16:17:34 2005 +0200
@@ -79,7 +79,7 @@
else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs;
val arities = get_arities descr' \ 0;
val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names [] (leafTs' @ branchTs);
- val leafTs = leafTs' @ (map (fn n => TFree (n, valOf (assoc (sorts, n)))) unneeded_vars);
+ val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
val recTs = get_rec_types descr' sorts;
val newTs = Library.take (length (hd descr), recTs);
val oldTs = Library.drop (length (hd descr), recTs);
--- a/src/HOL/Tools/inductive_codegen.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Tue Sep 20 16:17:34 2005 +0200
@@ -124,15 +124,15 @@
let fun err s = error (s ^ "\n" ^ Sign.string_of_term sg t)
in (case (optf, strip_comb t) of
(SOME f, (Const (name, _), args)) =>
- (case assoc (extra_fs, name) of
- NONE => overwrite (fs, (name, getOpt
- (Option.map (mg_factor f) (assoc (fs, name)), f)))
+ (case AList.lookup (op =) extra_fs name of
+ NONE => AList.update (op =) (name, getOpt
+ (Option.map (mg_factor f) (AList.lookup (op =) fs name), f)) fs
| SOME (fs', f') => (mg_factor f (FFix f');
Library.foldl (infer_factors sg extra_fs)
(fs, map (Option.map FFix) fs' ~~ args)))
| (SOME f, (Var ((name, _), _), [])) =>
- overwrite (fs, (name, getOpt
- (Option.map (mg_factor f) (assoc (fs, name)), f)))
+ AList.update (op =) (name, getOpt
+ (Option.map (mg_factor f) (AList.lookup (op =) fs name), f)) fs
| (NONE, _) => fs
| _ => err "Illegal term")
handle Factors => err "Product factor mismatch in"
@@ -152,7 +152,7 @@
(Symtab.dest (DatatypePackage.get_datatypes thy))));
fun check t = (case strip_comb t of
(Var _, []) => true
- | (Const (s, _), ts) => (case assoc (cnstrs, s) of
+ | (Const (s, _), ts) => (case AList.lookup (op =) cnstrs s of
NONE => false
| SOME i => length ts = i andalso forall check ts)
| _ => false)
@@ -209,7 +209,7 @@
(fn (NONE, _) => [NONE]
| (SOME js, arg) => map SOME
(List.filter (fn Mode ((_, js'), _) => js=js') (modes_of modes arg)))
- (iss ~~ args)))) (valOf (assoc (modes, name))))
+ (iss ~~ args)))) ((the o AList.lookup (op =) modes) name))
in (case strip_comb t of
(Const ("op =", Type (_, [T, _])), _) =>
@@ -230,7 +230,7 @@
val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
val vTs = List.concat (map term_vTs out_ts');
val dupTs = map snd (duplicates vTs) @
- List.mapPartial (curry assoc vTs) vs;
+ List.mapPartial (AList.lookup (op =) vTs) vs;
in
terms_vs (in_ts @ in_ts') subset vs andalso
forall (is_eqT o fastype_of) in_ts' andalso
@@ -264,7 +264,7 @@
end;
fun check_modes_pred thy arg_vs preds modes (p, ms) =
- let val SOME rs = assoc (preds, p)
+ let val SOME rs = AList.lookup (op =) preds p
in (p, List.filter (fn m => case find_index
(not o check_mode_clause thy arg_vs modes m) rs of
~1 => true
@@ -339,10 +339,10 @@
else ps
end;
-fun mk_v ((names, vs), s) = (case assoc (vs, s) of
+fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of
NONE => ((names, (s, [s])::vs), s)
| SOME xs => let val s' = variant names s in
- ((s'::names, overwrite (vs, (s, s'::xs))), s') end);
+ ((s'::names, AList.update (op =) (s, s'::xs) vs), s') end);
fun distinct_v (nvs, Var ((s, 0), T)) =
apsnd (Var o rpair T o rpair 0) (mk_v (nvs, s))
@@ -417,7 +417,7 @@
foldl_map check_constrt ((all_vs, []), in_ts);
fun is_ind t = (case head_of t of
- Const (s, _) => s = "op =" orelse isSome (assoc (modes, s))
+ Const (s, _) => s = "op =" orelse AList.defined (op =) modes s
| Var ((s, _), _) => s mem arg_vs);
fun compile_prems out_ts' vs names gr [] =
@@ -508,7 +508,7 @@
let val ((gr', _), prs) = foldl_map (fn ((gr, prfx), (s, cls)) =>
foldl_map (fn ((gr', prfx'), mode) => compile_pred thy defs gr'
dep module prfx' all_vs arg_vs modes s cls mode)
- ((gr, prfx), valOf (assoc (modes, s)))) ((gr, "fun "), preds)
+ ((gr, prfx), ((the o AList.lookup (op =) modes) s))) ((gr, "fun "), preds)
in
(gr', space_implode "\n\n" (map Pretty.string_of (List.concat prs)) ^ ";\n\n")
end;
@@ -532,7 +532,7 @@
fun prep_intrs intrs = map (rename_term o #prop o rep_thm o standard) intrs;
fun constrain cs [] = []
- | constrain cs ((s, xs) :: ys) = (s, case assoc (cs, s) of
+ | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs s of
NONE => xs
| SOME xs' => xs inter xs') :: constrain cs ys;
@@ -554,7 +554,7 @@
val arg_vs = List.concat (map term_vs args);
fun dest_prem factors (_ $ (p as (Const ("op :", _) $ t $ u))) =
- (case assoc (factors, case head_of u of
+ (case AList.lookup (op =) factors (case head_of u of
Const (name, _) => name | Var ((name, _), _) => name) of
NONE => Prem (full_split_prod t, u)
| SOME f => Prem (split_prod [] f t, u))
@@ -568,8 +568,8 @@
val Const (name, _) = head_of u;
val prems = map (dest_prem factors) (Logic.strip_imp_prems intr);
in
- (overwrite (clauses, (name, getOpt (assoc (clauses, name), []) @
- [(split_prod [] (valOf (assoc (factors, name))) t, prems)])))
+ AList.update (op =) (name, ((these o AList.lookup (op =) clauses) name) @
+ [(split_prod [] ((the o AList.lookup (op =) factors) name) t, prems)]) clauses
end;
fun check_set (Const (s, _)) = s mem names orelse isSome (get_clauses thy s)
@@ -592,7 +592,7 @@
Logic.strip_imp_concl t :: Logic.strip_imp_prems t) intrs))));
val factors = List.mapPartial (fn (name, f) =>
if name mem arg_vs then NONE
- else SOME (name, (map (curry assoc fs) arg_vs, f))) fs;
+ else SOME (name, (map (AList.lookup (op =) fs) arg_vs, f))) fs;
val clauses =
Library.foldl (add_clause (fs @ map (apsnd snd) extra_factors)) ([], intrs);
val modes = constrain modecs
@@ -626,7 +626,7 @@
(mk_ind_def thy defs gr dep names module'
[] [] (prep_intrs intrs)) dep names module' [u];
val (modes, factors) = lookup_modes gr1 dep;
- val ts = split_prod [] (snd (valOf (assoc (factors, s)))) t;
+ val ts = split_prod [] ((snd o the o AList.lookup (op =) factors) s) t;
val (ts', is) = if is_query then
fst (Library.foldl mk_mode ((([], []), 1), ts))
else (ts, 1 upto length ts);
@@ -659,7 +659,7 @@
SOME (gr2, (if brack then parens else I)
(Pretty.block ([Pretty.str "Seq.list_of", Pretty.brk 1,
Pretty.str "("] @
- conv_ntuple' (snd (valOf (assoc (factors, s))))
+ conv_ntuple' (snd (valOf (AList.lookup (op =) factors s)))
(HOLogic.dest_setT (fastype_of u))
(ps @ [Pretty.brk 1, Pretty.str "()"]) @
[Pretty.str ")"])))
--- a/src/HOL/eqrule_HOL_data.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/HOL/eqrule_HOL_data.ML Tue Sep 20 16:17:34 2005 +0200
@@ -45,8 +45,8 @@
Const("Trueprop",_) $ p =>
(case Term.head_of p of
Const(a,_) =>
- (case Library.assoc(pairs,a) of
- SOME(rls) => List.concat (map atoms ([th] RL rls))
+ (case AList.lookup (op =) pairs a of
+ SOME rls => List.concat (map atoms ([th] RL rls))
| NONE => [th])
| _ => [th])
| _ => [th])
--- a/src/Pure/General/output.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/Pure/General/output.ML Tue Sep 20 16:17:34 2005 +0200
@@ -160,10 +160,13 @@
in asl l end;
fun overwrite_warn (args as (alist, (a, _))) msg =
- (if is_none (assoc (alist, a)) then () else warning msg;
+ (if is_none (AList.lookup (op =) alist a) then () else warning msg;
overwrite args);
-
+fun update_warn eq msg (kv as (key, value)) xs = (
+ if (not o AList.defined eq xs) key then () else warning msg;
+ AList.update eq kv xs
+)
(** handle errors **)
--- a/src/Pure/codegen.ML Tue Sep 20 15:12:40 2005 +0200
+++ b/src/Pure/codegen.ML Tue Sep 20 16:17:34 2005 +0200
@@ -267,7 +267,7 @@
fun add_codegen name f thy =
let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
CodegenData.get thy
- in (case assoc (codegens, name) of
+ in (case AList.lookup (op =) codegens name of
NONE => CodegenData.put {codegens = (name, f) :: codegens,
tycodegens = tycodegens, consts = consts, types = types,
attrs = attrs, preprocs = preprocs, modules = modules,
@@ -278,7 +278,7 @@
fun add_tycodegen name f thy =
let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
CodegenData.get thy
- in (case assoc (tycodegens, name) of
+ in (case AList.lookup (op =) tycodegens name of
NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens,
codegens = codegens, consts = consts, types = types,
attrs = attrs, preprocs = preprocs, modules = modules,
@@ -292,7 +292,7 @@
fun add_attribute name att thy =
let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
CodegenData.get thy
- in (case assoc (attrs, name) of
+ in (case AList.lookup (op =) attrs name of
NONE => CodegenData.put {tycodegens = tycodegens,
codegens = codegens, consts = consts, types = types,
attrs = if name = "" then attrs @ [(name, att)] else (name, att) :: attrs,
@@ -358,7 +358,7 @@
in if Sign.typ_instance thy (U, T) then U
else error ("Illegal type constraint for constant " ^ cname)
end)
- in (case assoc (consts, (cname, T')) of
+ in (case AList.lookup (op =) consts (cname, T') of
NONE => CodegenData.put {codegens = codegens,
tycodegens = tycodegens,
consts = ((cname, T'), syn) :: consts,
@@ -381,7 +381,7 @@
CodegenData.get thy;
val tc = Sign.intern_type thy s
in
- (case assoc (types, tc) of
+ (case AList.lookup (op =) types tc of
NONE => CodegenData.put {codegens = codegens,
tycodegens = tycodegens, consts = consts,
types = (tc, syn) :: types, attrs = attrs,
@@ -389,7 +389,7 @@
| SOME _ => error ("Type " ^ tc ^ " already associated with code"))
end) (thy, xs);
-fun get_assoc_type thy s = assoc (#types (CodegenData.get thy), s);
+fun get_assoc_type thy s = AList.lookup (op =) ((#types o CodegenData.get) thy) s;
(**** make valid ML identifiers ****)
@@ -514,7 +514,7 @@
val ps = (reserved @ illegal) ~~
variantlist (map (suffix "'") reserved @ alt_names, names);
- fun rename_id s = getOpt (assoc (ps, s), s);
+ fun rename_id s = AList.lookup (op =) ps s |> the_default s;
fun rename (Var ((a, i), T)) = Var ((rename_id a, i), T)
| rename (Free (a, T)) = Free (rename_id a, T)
@@ -748,7 +748,7 @@
| default_tycodegen thy defs gr dep module brack (TFree (s, _)) =
SOME (gr, Pretty.str s)
| default_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
- (case assoc (#types (CodegenData.get thy), s) of
+ (case AList.lookup (op =) ((#types o CodegenData.get) thy) s of
NONE => NONE
| SOME (ms, aux) =>
let
@@ -779,8 +779,7 @@
fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
-fun add_to_module name s ms =
- overwrite (ms, (name, the (assoc (ms, name)) ^ s));
+fun add_to_module name s = AList.map_entry (op =) name (suffix s);
fun output_code gr module xs =
let
@@ -954,8 +953,8 @@
val (gi, frees) = Logic.goal_params
(prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i;
val gi' = ObjectLogic.atomize_term thy (map_term_types
- (map_type_tfree (fn p as (s, _) => getOpt (assoc (tvinsts, s),
- getOpt (default_type,TFree p)))) (subst_bounds (frees, strip gi)));
+ (map_type_tfree (fn p as (s, _) => getOpt (AList.lookup (op =) tvinsts s,
+ getOpt (default_type, TFree p)))) (subst_bounds (frees, strip gi)));
in case test_term (Toplevel.theory_of st) size iterations gi' of
NONE => writeln "No counterexamples found."
| SOME cex => writeln ("Counterexample found:\n" ^
@@ -1075,7 +1074,7 @@
("default_type", P.typ >> set_default_type)];
val parse_test_params = P.short_ident :-- (fn s =>
- P.$$$ "=" |-- getOpt (assoc (params, s), Scan.fail)) >> snd;
+ P.$$$ "=" |-- (AList.lookup (op =) params s |> the_default Scan.fail)) >> snd;
fun parse_tyinst xs =
(P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>