# HG changeset patch # User haftmann # Date 1125988243 -7200 # Node ID 2756a73f63a5b193fd70b80d056bf9d0f5ef8b73 # Parent 534b6e5e373663f324ee99988ff57dce54ae89ee introduced some new-style AList operations diff -r 534b6e5e3736 -r 2756a73f63a5 src/Provers/blast.ML --- a/src/Provers/blast.ML Tue Sep 06 08:29:17 2005 +0200 +++ b/src/Provers/blast.ML Tue Sep 06 08:30:43 2005 +0200 @@ -171,7 +171,7 @@ fun fromType alist (Term.Type(a,Ts)) = list_comb (Const a, map (fromType alist) Ts) | fromType alist (Term.TFree(a,_)) = Free a | fromType alist (Term.TVar (ixn,_)) = - (case (assoc_string_int(!alist,ixn)) of + (case (AList.lookup (op =) (!alist) ixn) of NONE => let val t' = Var(ref NONE) in alist := (ixn, t') :: !alist; t' end @@ -381,7 +381,7 @@ | from (Term.Free (a,_)) = Free a | from (Term.Bound i) = Bound i | from (Term.Var (ixn,T)) = - (case (assoc_string_int(!alistVar,ixn)) of + (case (AList.lookup (op =) (!alistVar) ixn) of NONE => let val t' = Var(ref NONE) in alistVar := (ixn, t') :: !alistVar; t' end @@ -1214,7 +1214,7 @@ | Term.Free (a,_) => apply (Free a) | Term.Bound i => apply (Bound i) | Term.Var (ix,_) => - (case (assoc_string_int(!alistVar,ix)) of + (case (AList.lookup (op =) (!alistVar) ix) of NONE => (alistVar := (ix, (ref NONE, bounds ts)) :: !alistVar; Var (hdvar(!alistVar))) diff -r 534b6e5e3736 -r 2756a73f63a5 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Tue Sep 06 08:29:17 2005 +0200 +++ b/src/Pure/Isar/locale.ML Tue Sep 06 08:30:43 2005 +0200 @@ -625,7 +625,7 @@ (* ren maps names to (new) names and syntax; represented as association list *) fun rename_var ren (x, mx) = - case assoc_string (ren, x) of + case AList.lookup (op =) ren x of NONE => (x, mx) | SOME (x', NONE) => (x', if mx = NONE then mx else SOME Syntax.NoSyn) (*drop syntax*) @@ -635,7 +635,7 @@ else (x', SOME mx'); (*change syntax*) fun rename ren x = - case assoc_string (ren, x) of + case AList.lookup (op =) ren x of NONE => x | SOME (x', _) => x'; (*ignore syntax*) @@ -1391,9 +1391,9 @@ fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) => - (x, assoc_string (parms, x), mx)) fixes) + (x, AList.lookup (op =) parms x, mx)) fixes) | finish_ext_elem parms _ (Constrains csts, _) = - Constrains (map (fn (x, _) => (x, valOf (assoc_string (parms, x)))) csts) + Constrains (map (fn (x, _) => (x, (the o AList.lookup (op =) parms) x)) csts) | finish_ext_elem _ close (Assumes asms, propp) = close (Assumes (map #1 asms ~~ propp)) | finish_ext_elem _ close (Defines defs, propp) = diff -r 534b6e5e3736 -r 2756a73f63a5 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Sep 06 08:29:17 2005 +0200 +++ b/src/Pure/Proof/extraction.ML Tue Sep 06 08:30:43 2005 +0200 @@ -532,7 +532,7 @@ (Bound (length Us), eT :: Us); val u = list_comb (incr_boundvars (length Us') t, map Bound (length Us - 1 downto 0)); - val u' = (case assoc_string (types, tname_of T) of + val u' = (case AList.lookup (op =) types (tname_of T) of SOME ((_, SOME f)) => f r eT u T | _ => Const ("realizes", eT --> T --> T) $ r $ u) in app_rlz_rews Ts vs (list_abs (map (pair "x") Us', u')) end diff -r 534b6e5e3736 -r 2756a73f63a5 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Tue Sep 06 08:29:17 2005 +0200 +++ b/src/Pure/tactic.ML Tue Sep 06 08:30:43 2005 +0200 @@ -240,7 +240,7 @@ let val thy = Thm.theory_of_thm st and params = params_of_state st i and rts = types_sorts rule and (types,sorts) = types_sorts st - fun types'(a, ~1) = (case assoc_string (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 used = Drule.add_used rule (Drule.add_used st []); in read_insts thy rts (types',sorts) used sinsts end; @@ -666,7 +666,7 @@ val frees = map Term.dest_Free (Term.term_frees statement); val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees; val fixed_tfrees = foldr Term.add_typ_tfrees [] (map #2 fixed_frees); - val params = List.mapPartial (fn x => Option.map (pair x) (assoc_string (frees, x))) xs; + val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs; fun err msg = raise ERROR_MESSAGE (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^ diff -r 534b6e5e3736 -r 2756a73f63a5 src/Pure/term.ML --- a/src/Pure/term.ML Tue Sep 06 08:29:17 2005 +0200 +++ b/src/Pure/term.ML Tue Sep 06 08:30:43 2005 +0200 @@ -736,7 +736,7 @@ let val ren = match_bvs (pat, obj, []); fun ren_abs (Abs (x, T, b)) = - Abs (if_none (assoc_string (ren, x)) x, T, ren_abs b) + Abs (if_none (AList.lookup (op =) ren x) x, T, ren_abs b) | ren_abs (f $ t) = ren_abs f $ ren_abs t | ren_abs t = t in if null ren then NONE else SOME (ren_abs t) end; @@ -934,7 +934,7 @@ | typ_subst_TVars inst ty = let fun subst (Type (a, Ts)) = Type (a, map subst Ts) - | subst (T as TVar (xi, _)) = if_none (assoc_string_int (inst, xi)) T + | subst (T as TVar (xi, _)) = if_none (AList.lookup (op =) inst xi) T | subst T = T; in subst ty end; @@ -945,7 +945,7 @@ fun subst_Vars [] tm = tm | subst_Vars inst tm = let - fun subst (t as Var (xi, _)) = if_none (assoc_string_int (inst, xi)) t + fun subst (t as Var (xi, _)) = if_none (AList.lookup (op =) inst xi) t | subst (Abs (a, T, t)) = Abs (a, T, subst t) | subst (t $ u) = subst t $ subst u | subst t = t; @@ -959,7 +959,7 @@ fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T) | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T) | subst (t as Var (xi, T)) = - (case assoc_string_int (inst, xi) of + (case AList.lookup (op =) inst xi of NONE => Var (xi, typ_subst_TVars instT T) | SOME t => t) | subst (t as Bound _) = t diff -r 534b6e5e3736 -r 2756a73f63a5 src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Tue Sep 06 08:29:17 2005 +0200 +++ b/src/Pure/type_infer.ML Tue Sep 06 08:30:43 2005 +0200 @@ -111,7 +111,7 @@ fun pretyp_of is_param (params, typ) = let fun add_parms (TVar (xi as (x, _), S)) ps = - if is_param xi andalso is_none (assoc_string_int (ps, xi)) + if is_param xi andalso is_none (AList.lookup (op =) ps xi) then (xi, mk_param S) :: ps else ps | add_parms (TFree _) ps = ps | add_parms (Type (_, Ts)) ps = fold add_parms Ts ps; @@ -119,7 +119,7 @@ val params' = add_parms typ params; fun pre_of (TVar (v as (xi, _))) = - (case assoc_string_int (params', xi) of + (case AList.lookup (op =) params' xi of NONE => PTVar v | SOME p => p) | pre_of (TFree ("'_dummy_", S)) = mk_param S @@ -137,7 +137,7 @@ fun preterm_of const_type is_param ((vparams, params), tm) = let fun add_vparm (ps, xi) = - if is_none (assoc_string_int (ps, xi)) then + if is_none (AList.lookup (op =) ps xi) then (xi, mk_param []) :: ps else ps; @@ -149,7 +149,7 @@ | add_vparms (ps, _) = ps; val vparams' = add_vparms (vparams, tm); - fun var_param xi = the (assoc_string_int (vparams', xi)); + fun var_param xi = (the o AList.lookup (op =) vparams') xi; val preT_of = pretyp_of is_param; @@ -457,7 +457,7 @@ ^ commas_quote (map (Syntax.string_of_vname' o fst) dups))); fun get xi = - (case (assoc_string_int (env, xi), def_sort xi) of + (case (AList.lookup (op =) env xi, def_sort xi) of (NONE, NONE) => Type.defaultS tsig | (NONE, SOME S) => S | (SOME S, NONE) => S