src/Pure/codegen.ML
changeset 17521 0f1c48de39f5
parent 17412 e26cb20ef0cc
child 17549 ee4408eac12c
     1.1 --- a/src/Pure/codegen.ML	Tue Sep 20 15:12:40 2005 +0200
     1.2 +++ b/src/Pure/codegen.ML	Tue Sep 20 16:17:34 2005 +0200
     1.3 @@ -267,7 +267,7 @@
     1.4  fun add_codegen name f thy =
     1.5    let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
     1.6      CodegenData.get thy
     1.7 -  in (case assoc (codegens, name) of
     1.8 +  in (case AList.lookup (op =) codegens name of
     1.9        NONE => CodegenData.put {codegens = (name, f) :: codegens,
    1.10          tycodegens = tycodegens, consts = consts, types = types,
    1.11          attrs = attrs, preprocs = preprocs, modules = modules,
    1.12 @@ -278,7 +278,7 @@
    1.13  fun add_tycodegen name f thy =
    1.14    let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
    1.15      CodegenData.get thy
    1.16 -  in (case assoc (tycodegens, name) of
    1.17 +  in (case AList.lookup (op =) tycodegens name of
    1.18        NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens,
    1.19          codegens = codegens, consts = consts, types = types,
    1.20          attrs = attrs, preprocs = preprocs, modules = modules,
    1.21 @@ -292,7 +292,7 @@
    1.22  fun add_attribute name att thy =
    1.23    let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
    1.24      CodegenData.get thy
    1.25 -  in (case assoc (attrs, name) of
    1.26 +  in (case AList.lookup (op =) attrs name of
    1.27        NONE => CodegenData.put {tycodegens = tycodegens,
    1.28          codegens = codegens, consts = consts, types = types,
    1.29          attrs = if name = "" then attrs @ [(name, att)] else (name, att) :: attrs,
    1.30 @@ -358,7 +358,7 @@
    1.31                    in if Sign.typ_instance thy (U, T) then U
    1.32                      else error ("Illegal type constraint for constant " ^ cname)
    1.33                    end)
    1.34 -         in (case assoc (consts, (cname, T')) of
    1.35 +         in (case AList.lookup (op =) consts (cname, T') of
    1.36               NONE => CodegenData.put {codegens = codegens,
    1.37                 tycodegens = tycodegens,
    1.38                 consts = ((cname, T'), syn) :: consts,
    1.39 @@ -381,7 +381,7 @@
    1.40        CodegenData.get thy;
    1.41      val tc = Sign.intern_type thy s
    1.42    in
    1.43 -    (case assoc (types, tc) of
    1.44 +    (case AList.lookup (op =) types tc of
    1.45         NONE => CodegenData.put {codegens = codegens,
    1.46           tycodegens = tycodegens, consts = consts,
    1.47           types = (tc, syn) :: types, attrs = attrs,
    1.48 @@ -389,7 +389,7 @@
    1.49       | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
    1.50    end) (thy, xs);
    1.51  
    1.52 -fun get_assoc_type thy s = assoc (#types (CodegenData.get thy), s);
    1.53 +fun get_assoc_type thy s = AList.lookup (op =) ((#types o CodegenData.get) thy) s;
    1.54  
    1.55  
    1.56  (**** make valid ML identifiers ****)
    1.57 @@ -514,7 +514,7 @@
    1.58      val ps = (reserved @ illegal) ~~
    1.59        variantlist (map (suffix "'") reserved @ alt_names, names);
    1.60  
    1.61 -    fun rename_id s = getOpt (assoc (ps, s), s);
    1.62 +    fun rename_id s = AList.lookup (op =) ps s |> the_default s;
    1.63  
    1.64      fun rename (Var ((a, i), T)) = Var ((rename_id a, i), T)
    1.65        | rename (Free (a, T)) = Free (rename_id a, T)
    1.66 @@ -748,7 +748,7 @@
    1.67    | default_tycodegen thy defs gr dep module brack (TFree (s, _)) =
    1.68        SOME (gr, Pretty.str s)
    1.69    | default_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
    1.70 -      (case assoc (#types (CodegenData.get thy), s) of
    1.71 +      (case AList.lookup (op =) ((#types o CodegenData.get) thy) s of
    1.72           NONE => NONE
    1.73         | SOME (ms, aux) =>
    1.74             let
    1.75 @@ -779,8 +779,7 @@
    1.76  
    1.77  fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
    1.78  
    1.79 -fun add_to_module name s ms =
    1.80 -  overwrite (ms, (name, the (assoc (ms, name)) ^ s));
    1.81 +fun add_to_module name s = AList.map_entry (op =) name (suffix s);
    1.82  
    1.83  fun output_code gr module xs =
    1.84    let
    1.85 @@ -954,8 +953,8 @@
    1.86      val (gi, frees) = Logic.goal_params
    1.87        (prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i;
    1.88      val gi' = ObjectLogic.atomize_term thy (map_term_types
    1.89 -      (map_type_tfree (fn p as (s, _) => getOpt (assoc (tvinsts, s),
    1.90 -        getOpt (default_type,TFree p)))) (subst_bounds (frees, strip gi)));
    1.91 +      (map_type_tfree (fn p as (s, _) => getOpt (AList.lookup (op =) tvinsts s,
    1.92 +        getOpt (default_type, TFree p)))) (subst_bounds (frees, strip gi)));
    1.93    in case test_term (Toplevel.theory_of st) size iterations gi' of
    1.94        NONE => writeln "No counterexamples found."
    1.95      | SOME cex => writeln ("Counterexample found:\n" ^
    1.96 @@ -1075,7 +1074,7 @@
    1.97     ("default_type", P.typ >> set_default_type)];
    1.98  
    1.99  val parse_test_params = P.short_ident :-- (fn s =>
   1.100 -  P.$$$ "=" |-- getOpt (assoc (params, s), Scan.fail)) >> snd;
   1.101 +  P.$$$ "=" |-- (AList.lookup (op =) params s |> the_default Scan.fail)) >> snd;
   1.102  
   1.103  fun parse_tyinst xs =
   1.104    (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>