src/HOL/Tools/inductive_codegen.ML
changeset 17521 0f1c48de39f5
parent 17412 e26cb20ef0cc
child 18388 ab1a710a68ce
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Tue Sep 20 15:12:40 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Tue Sep 20 16:17:34 2005 +0200
     1.3 @@ -124,15 +124,15 @@
     1.4    let fun err s = error (s ^ "\n" ^ Sign.string_of_term sg t)
     1.5    in (case (optf, strip_comb t) of
     1.6        (SOME f, (Const (name, _), args)) =>
     1.7 -        (case assoc (extra_fs, name) of
     1.8 -           NONE => overwrite (fs, (name, getOpt
     1.9 -             (Option.map (mg_factor f) (assoc (fs, name)), f)))
    1.10 +        (case AList.lookup (op =) extra_fs name of
    1.11 +           NONE => AList.update (op =) (name, getOpt
    1.12 +             (Option.map (mg_factor f) (AList.lookup (op =) fs name), f)) fs
    1.13           | SOME (fs', f') => (mg_factor f (FFix f');
    1.14               Library.foldl (infer_factors sg extra_fs)
    1.15                 (fs, map (Option.map FFix) fs' ~~ args)))
    1.16      | (SOME f, (Var ((name, _), _), [])) =>
    1.17 -        overwrite (fs, (name, getOpt
    1.18 -          (Option.map (mg_factor f) (assoc (fs, name)), f)))
    1.19 +        AList.update (op =) (name, getOpt
    1.20 +          (Option.map (mg_factor f) (AList.lookup (op =) fs name), f)) fs
    1.21      | (NONE, _) => fs
    1.22      | _ => err "Illegal term")
    1.23        handle Factors => err "Product factor mismatch in"
    1.24 @@ -152,7 +152,7 @@
    1.25        (Symtab.dest (DatatypePackage.get_datatypes thy))));
    1.26      fun check t = (case strip_comb t of
    1.27          (Var _, []) => true
    1.28 -      | (Const (s, _), ts) => (case assoc (cnstrs, s) of
    1.29 +      | (Const (s, _), ts) => (case AList.lookup (op =) cnstrs s of
    1.30              NONE => false
    1.31            | SOME i => length ts = i andalso forall check ts)
    1.32        | _ => false)
    1.33 @@ -209,7 +209,7 @@
    1.34          (fn (NONE, _) => [NONE]
    1.35            | (SOME js, arg) => map SOME
    1.36                (List.filter (fn Mode ((_, js'), _) => js=js') (modes_of modes arg)))
    1.37 -                (iss ~~ args)))) (valOf (assoc (modes, name))))
    1.38 +                (iss ~~ args)))) ((the o AList.lookup (op =) modes) name))
    1.39  
    1.40    in (case strip_comb t of
    1.41        (Const ("op =", Type (_, [T, _])), _) =>
    1.42 @@ -230,7 +230,7 @@
    1.43              val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
    1.44              val vTs = List.concat (map term_vTs out_ts');
    1.45              val dupTs = map snd (duplicates vTs) @
    1.46 -              List.mapPartial (curry assoc vTs) vs;
    1.47 +              List.mapPartial (AList.lookup (op =) vTs) vs;
    1.48            in
    1.49              terms_vs (in_ts @ in_ts') subset vs andalso
    1.50              forall (is_eqT o fastype_of) in_ts' andalso
    1.51 @@ -264,7 +264,7 @@
    1.52    end;
    1.53  
    1.54  fun check_modes_pred thy arg_vs preds modes (p, ms) =
    1.55 -  let val SOME rs = assoc (preds, p)
    1.56 +  let val SOME rs = AList.lookup (op =) preds p
    1.57    in (p, List.filter (fn m => case find_index
    1.58      (not o check_mode_clause thy arg_vs modes m) rs of
    1.59        ~1 => true
    1.60 @@ -339,10 +339,10 @@
    1.61      else ps
    1.62    end;
    1.63  
    1.64 -fun mk_v ((names, vs), s) = (case assoc (vs, s) of
    1.65 +fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of
    1.66        NONE => ((names, (s, [s])::vs), s)
    1.67      | SOME xs => let val s' = variant names s in
    1.68 -        ((s'::names, overwrite (vs, (s, s'::xs))), s') end);
    1.69 +        ((s'::names, AList.update (op =) (s, s'::xs) vs), s') end);
    1.70  
    1.71  fun distinct_v (nvs, Var ((s, 0), T)) =
    1.72        apsnd (Var o rpair T o rpair 0) (mk_v (nvs, s))
    1.73 @@ -417,7 +417,7 @@
    1.74        foldl_map check_constrt ((all_vs, []), in_ts);
    1.75  
    1.76      fun is_ind t = (case head_of t of
    1.77 -          Const (s, _) => s = "op =" orelse isSome (assoc (modes, s))
    1.78 +          Const (s, _) => s = "op =" orelse AList.defined (op =) modes s
    1.79          | Var ((s, _), _) => s mem arg_vs);
    1.80  
    1.81      fun compile_prems out_ts' vs names gr [] =
    1.82 @@ -508,7 +508,7 @@
    1.83    let val ((gr', _), prs) = foldl_map (fn ((gr, prfx), (s, cls)) =>
    1.84      foldl_map (fn ((gr', prfx'), mode) => compile_pred thy defs gr'
    1.85        dep module prfx' all_vs arg_vs modes s cls mode)
    1.86 -        ((gr, prfx), valOf (assoc (modes, s)))) ((gr, "fun "), preds)
    1.87 +        ((gr, prfx), ((the o AList.lookup (op =) modes) s))) ((gr, "fun "), preds)
    1.88    in
    1.89      (gr', space_implode "\n\n" (map Pretty.string_of (List.concat prs)) ^ ";\n\n")
    1.90    end;
    1.91 @@ -532,7 +532,7 @@
    1.92  fun prep_intrs intrs = map (rename_term o #prop o rep_thm o standard) intrs;
    1.93  
    1.94  fun constrain cs [] = []
    1.95 -  | constrain cs ((s, xs) :: ys) = (s, case assoc (cs, s) of
    1.96 +  | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs s of
    1.97        NONE => xs
    1.98      | SOME xs' => xs inter xs') :: constrain cs ys;
    1.99  
   1.100 @@ -554,7 +554,7 @@
   1.101        val arg_vs = List.concat (map term_vs args);
   1.102  
   1.103        fun dest_prem factors (_ $ (p as (Const ("op :", _) $ t $ u))) =
   1.104 -            (case assoc (factors, case head_of u of
   1.105 +            (case AList.lookup (op =) factors (case head_of u of
   1.106                   Const (name, _) => name | Var ((name, _), _) => name) of
   1.107                 NONE => Prem (full_split_prod t, u)
   1.108               | SOME f => Prem (split_prod [] f t, u))
   1.109 @@ -568,8 +568,8 @@
   1.110            val Const (name, _) = head_of u;
   1.111            val prems = map (dest_prem factors) (Logic.strip_imp_prems intr);
   1.112          in
   1.113 -          (overwrite (clauses, (name, getOpt (assoc (clauses, name), []) @
   1.114 -             [(split_prod [] (valOf (assoc (factors, name))) t, prems)])))
   1.115 +          AList.update (op =) (name, ((these o AList.lookup (op =) clauses) name) @
   1.116 +             [(split_prod [] ((the o AList.lookup (op =) factors) name) t, prems)]) clauses
   1.117          end;
   1.118  
   1.119        fun check_set (Const (s, _)) = s mem names orelse isSome (get_clauses thy s)
   1.120 @@ -592,7 +592,7 @@
   1.121            Logic.strip_imp_concl t :: Logic.strip_imp_prems t) intrs))));
   1.122        val factors = List.mapPartial (fn (name, f) =>
   1.123          if name mem arg_vs then NONE
   1.124 -        else SOME (name, (map (curry assoc fs) arg_vs, f))) fs;
   1.125 +        else SOME (name, (map (AList.lookup (op =) fs) arg_vs, f))) fs;
   1.126        val clauses =
   1.127          Library.foldl (add_clause (fs @ map (apsnd snd) extra_factors)) ([], intrs);
   1.128        val modes = constrain modecs
   1.129 @@ -626,7 +626,7 @@
   1.130               (mk_ind_def thy defs gr dep names module'
   1.131               [] [] (prep_intrs intrs)) dep names module' [u];
   1.132             val (modes, factors) = lookup_modes gr1 dep;
   1.133 -           val ts = split_prod [] (snd (valOf (assoc (factors, s)))) t;
   1.134 +           val ts = split_prod [] ((snd o the o AList.lookup (op =) factors) s) t;
   1.135             val (ts', is) = if is_query then
   1.136                 fst (Library.foldl mk_mode ((([], []), 1), ts))
   1.137               else (ts, 1 upto length ts);
   1.138 @@ -659,7 +659,7 @@
   1.139             SOME (gr2, (if brack then parens else I)
   1.140               (Pretty.block ([Pretty.str "Seq.list_of", Pretty.brk 1,
   1.141                 Pretty.str "("] @
   1.142 -               conv_ntuple' (snd (valOf (assoc (factors, s))))
   1.143 +                conv_ntuple' (snd (valOf (AList.lookup (op =) factors s)))
   1.144                   (HOLogic.dest_setT (fastype_of u))
   1.145                   (ps @ [Pretty.brk 1, Pretty.str "()"]) @
   1.146                 [Pretty.str ")"])))