eliminated Codegen.mode in favour of explicit argument;
authorwenzelm
Tue Apr 19 23:57:28 2011 +0200 (2011-04-19)
changeset 42411ff997038e8eb
parent 42410 16bc5564535f
child 42422 6a2837ddde4b
eliminated Codegen.mode in favour of explicit argument;
src/HOL/HOL.thy
src/HOL/Int.thy
src/HOL/List.thy
src/HOL/Product_Type.thy
src/HOL/String.thy
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/recfun_codegen.ML
src/Pure/codegen.ML
     1.1 --- a/src/HOL/HOL.thy	Tue Apr 19 22:32:49 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Apr 19 23:57:28 2011 +0200
     1.3 @@ -1746,20 +1746,21 @@
     1.4  setup {*
     1.5  let
     1.6  
     1.7 -fun eq_codegen thy defs dep thyname b t gr =
     1.8 +fun eq_codegen thy mode defs dep thyname b t gr =
     1.9      (case strip_comb t of
    1.10         (Const (@{const_name HOL.eq}, Type (_, [Type ("fun", _), _])), _) => NONE
    1.11       | (Const (@{const_name HOL.eq}, _), [t, u]) =>
    1.12            let
    1.13 -            val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
    1.14 -            val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
    1.15 -            val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr'';
    1.16 +            val (pt, gr') = Codegen.invoke_codegen thy mode defs dep thyname false t gr;
    1.17 +            val (pu, gr'') = Codegen.invoke_codegen thy mode defs dep thyname false u gr';
    1.18 +            val (_, gr''') =
    1.19 +              Codegen.invoke_tycodegen thy mode defs dep thyname false HOLogic.boolT gr'';
    1.20            in
    1.21              SOME (Codegen.parens
    1.22                (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
    1.23            end
    1.24       | (t as Const (@{const_name HOL.eq}, _), ts) => SOME (Codegen.invoke_codegen
    1.25 -         thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
    1.26 +         thy mode defs dep thyname b (Codegen.eta_expand t ts 2) gr)
    1.27       | _ => NONE);
    1.28  
    1.29  in
     2.1 --- a/src/HOL/Int.thy	Tue Apr 19 22:32:49 2011 +0200
     2.2 +++ b/src/HOL/Int.thy	Tue Apr 19 23:57:28 2011 +0200
     2.3 @@ -2351,11 +2351,11 @@
     2.4  fun strip_number_of (@{term "Int.number_of :: int => int"} $ t) = t
     2.5    | strip_number_of t = t;
     2.6  
     2.7 -fun numeral_codegen thy defs dep module b t gr =
     2.8 +fun numeral_codegen thy mode defs dep module b t gr =
     2.9    let val i = HOLogic.dest_numeral (strip_number_of t)
    2.10    in
    2.11      SOME (Codegen.str (string_of_int i),
    2.12 -      snd (Codegen.invoke_tycodegen thy defs dep module false HOLogic.intT gr))
    2.13 +      snd (Codegen.invoke_tycodegen thy mode defs dep module false HOLogic.intT gr))
    2.14    end handle TERM _ => NONE;
    2.15  
    2.16  in
     3.1 --- a/src/HOL/List.thy	Tue Apr 19 22:32:49 2011 +0200
     3.2 +++ b/src/HOL/List.thy	Tue Apr 19 23:57:28 2011 +0200
     3.3 @@ -5207,13 +5207,13 @@
     3.4  
     3.5  setup {*
     3.6  let
     3.7 -  fun list_codegen thy defs dep thyname b t gr =
     3.8 +  fun list_codegen thy mode defs dep thyname b t gr =
     3.9      let
    3.10        val ts = HOLogic.dest_list t;
    3.11 -      val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
    3.12 +      val (_, gr') = Codegen.invoke_tycodegen thy mode defs dep thyname false
    3.13          (fastype_of t) gr;
    3.14        val (ps, gr'') = fold_map
    3.15 -        (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
    3.16 +        (Codegen.invoke_codegen thy mode defs dep thyname false) ts gr'
    3.17      in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
    3.18  in
    3.19    fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"]
     4.1 --- a/src/HOL/Product_Type.thy	Tue Apr 19 22:32:49 2011 +0200
     4.2 +++ b/src/HOL/Product_Type.thy	Tue Apr 19 23:57:28 2011 +0200
     4.3 @@ -336,7 +336,7 @@
     4.4    | strip_abs_split i t =
     4.5        strip_abs_split i (Abs ("x", hd (binder_types (fastype_of t)), t $ Bound 0));
     4.6  
     4.7 -fun let_codegen thy defs dep thyname brack t gr =
     4.8 +fun let_codegen thy mode defs dep thyname brack t gr =
     4.9    (case strip_comb t of
    4.10      (t1 as Const (@{const_name Let}, _), t2 :: t3 :: ts) =>
    4.11      let
    4.12 @@ -347,17 +347,17 @@
    4.13          | dest_let t = ([], t);
    4.14        fun mk_code (l, r) gr =
    4.15          let
    4.16 -          val (pl, gr1) = Codegen.invoke_codegen thy defs dep thyname false l gr;
    4.17 -          val (pr, gr2) = Codegen.invoke_codegen thy defs dep thyname false r gr1;
    4.18 +          val (pl, gr1) = Codegen.invoke_codegen thy mode defs dep thyname false l gr;
    4.19 +          val (pr, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false r gr1;
    4.20          in ((pl, pr), gr2) end
    4.21      in case dest_let (t1 $ t2 $ t3) of
    4.22          ([], _) => NONE
    4.23        | (ps, u) =>
    4.24            let
    4.25              val (qs, gr1) = fold_map mk_code ps gr;
    4.26 -            val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1;
    4.27 +            val (pu, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false u gr1;
    4.28              val (pargs, gr3) = fold_map
    4.29 -              (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
    4.30 +              (Codegen.invoke_codegen thy mode defs dep thyname true) ts gr2
    4.31            in
    4.32              SOME (Codegen.mk_app brack
    4.33                (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, flat
    4.34 @@ -370,14 +370,14 @@
    4.35      end
    4.36    | _ => NONE);
    4.37  
    4.38 -fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of
    4.39 +fun split_codegen thy mode defs dep thyname brack t gr = (case strip_comb t of
    4.40      (t1 as Const (@{const_name prod_case}, _), t2 :: ts) =>
    4.41        let
    4.42          val ([p], u) = strip_abs_split 1 (t1 $ t2);
    4.43 -        val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr;
    4.44 -        val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1;
    4.45 +        val (q, gr1) = Codegen.invoke_codegen thy mode defs dep thyname false p gr;
    4.46 +        val (pu, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false u gr1;
    4.47          val (pargs, gr3) = fold_map
    4.48 -          (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
    4.49 +          (Codegen.invoke_codegen thy mode defs dep thyname true) ts gr2
    4.50        in
    4.51          SOME (Codegen.mk_app brack
    4.52            (Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>",
     5.1 --- a/src/HOL/String.thy	Tue Apr 19 22:32:49 2011 +0200
     5.2 +++ b/src/HOL/String.thy	Tue Apr 19 23:57:28 2011 +0200
     5.3 @@ -227,10 +227,10 @@
     5.4  setup {*
     5.5  let
     5.6  
     5.7 -fun char_codegen thy defs dep thyname b t gr =
     5.8 +fun char_codegen thy mode defs dep thyname b t gr =
     5.9    let
    5.10      val i = HOLogic.dest_char t;
    5.11 -    val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
    5.12 +    val (_, gr') = Codegen.invoke_tycodegen thy mode defs dep thyname false
    5.13        (fastype_of t) gr;
    5.14    in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
    5.15    end handle TERM _ => NONE;
     6.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Apr 19 22:32:49 2011 +0200
     6.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Apr 19 23:57:28 2011 +0200
     6.3 @@ -151,7 +151,7 @@
     6.4  
     6.5  (* datatype definition *)
     6.6  
     6.7 -fun add_dt_defs thy defs dep module descr sorts gr =
     6.8 +fun add_dt_defs thy mode defs dep module descr sorts gr =
     6.9    let
    6.10      val descr' = filter (can (map Datatype_Aux.dest_DtTFree o #2 o snd)) descr;
    6.11      val rtnames = map (#1 o snd) (filter (fn (_, (_, _, cs)) =>
    6.12 @@ -159,7 +159,7 @@
    6.13  
    6.14      val (_, (tname, _, _)) :: _ = descr';
    6.15      val node_id = tname ^ " (type)";
    6.16 -    val module' = Codegen.if_library (Codegen.thyname_of_type thy tname) module;
    6.17 +    val module' = Codegen.if_library mode (Codegen.thyname_of_type thy tname) module;
    6.18  
    6.19      fun mk_dtdef prfx [] gr = ([], gr)
    6.20        | mk_dtdef prfx ((_, (tname, dts, cs))::xs) gr =
    6.21 @@ -169,7 +169,7 @@
    6.22              val ((_, type_id), gr') = Codegen.mk_type_id module' tname gr;
    6.23              val (ps, gr'') = gr' |>
    6.24                fold_map (fn (cname, cargs) =>
    6.25 -                fold_map (Codegen.invoke_tycodegen thy defs node_id module' false)
    6.26 +                fold_map (Codegen.invoke_tycodegen thy mode defs node_id module' false)
    6.27                    cargs ##>>
    6.28                  Codegen.mk_const_id module' cname) cs';
    6.29              val (rest, gr''') = mk_dtdef "and " xs gr''
    6.30 @@ -309,11 +309,11 @@
    6.31             Codegen.map_node node_id (K (NONE, module',
    6.32               Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
    6.33                 [Codegen.str ";"])) ^ "\n\n" ^
    6.34 -             (if member (op =) (! Codegen.mode) "term_of" then
    6.35 +             (if member (op =) mode "term_of" then
    6.36                  Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk
    6.37                    (mk_term_of_def gr2 "fun " descr') @ [Codegen.str ";"])) ^ "\n\n"
    6.38                else "") ^
    6.39 -             (if member (op =) (! Codegen.mode) "test" then
    6.40 +             (if member (op =) mode "test" then
    6.41                  Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk
    6.42                    (mk_gen_of_def gr2 "fun " descr') @ [Codegen.str ";"])) ^ "\n\n"
    6.43                else ""))) gr2
    6.44 @@ -323,10 +323,10 @@
    6.45  
    6.46  (* case expressions *)
    6.47  
    6.48 -fun pretty_case thy defs dep module brack constrs (c as Const (_, T)) ts gr =
    6.49 +fun pretty_case thy mode defs dep module brack constrs (c as Const (_, T)) ts gr =
    6.50    let val i = length constrs
    6.51    in if length ts <= i then
    6.52 -       Codegen.invoke_codegen thy defs dep module brack (Codegen.eta_expand c ts (i+1)) gr
    6.53 +       Codegen.invoke_codegen thy mode defs dep module brack (Codegen.eta_expand c ts (i+1)) gr
    6.54      else
    6.55        let
    6.56          val ts1 = take i ts;
    6.57 @@ -342,10 +342,10 @@
    6.58                  val xs = Name.variant_list names (replicate j "x");
    6.59                  val Us' = take j (binder_types U);
    6.60                  val frees = map2 (curry Free) xs Us';
    6.61 -                val (cp, gr0) = Codegen.invoke_codegen thy defs dep module false
    6.62 +                val (cp, gr0) = Codegen.invoke_codegen thy mode defs dep module false
    6.63                    (list_comb (Const (cname, Us' ---> dT), frees)) gr;
    6.64                  val t' = Envir.beta_norm (list_comb (t, frees));
    6.65 -                val (p, gr1) = Codegen.invoke_codegen thy defs dep module false t' gr0;
    6.66 +                val (p, gr1) = Codegen.invoke_codegen thy mode defs dep module false t' gr0;
    6.67                  val (ps, gr2) = pcase cs ts Us gr1;
    6.68                in
    6.69                  ([Pretty.block [cp, Codegen.str " =>", Pretty.brk 1, p]] :: ps, gr2)
    6.70 @@ -353,8 +353,8 @@
    6.71  
    6.72          val (ps1, gr1) = pcase constrs ts1 Ts gr ;
    6.73          val ps = flat (separate [Pretty.brk 1, Codegen.str "| "] ps1);
    6.74 -        val (p, gr2) = Codegen.invoke_codegen thy defs dep module false t gr1;
    6.75 -        val (ps2, gr3) = fold_map (Codegen.invoke_codegen thy defs dep module true) ts2 gr2;
    6.76 +        val (p, gr2) = Codegen.invoke_codegen thy mode defs dep module false t gr1;
    6.77 +        val (ps2, gr3) = fold_map (Codegen.invoke_codegen thy mode defs dep module true) ts2 gr2;
    6.78        in ((if not (null ts2) andalso brack then Codegen.parens else I)
    6.79          (Pretty.block (separate (Pretty.brk 1)
    6.80            (Pretty.block ([Codegen.str "(case ", p, Codegen.str " of",
    6.81 @@ -365,15 +365,15 @@
    6.82  
    6.83  (* constructors *)
    6.84  
    6.85 -fun pretty_constr thy defs dep module brack args (c as Const (s, T)) ts gr =
    6.86 +fun pretty_constr thy mode defs dep module brack args (c as Const (s, T)) ts gr =
    6.87    let val i = length args
    6.88    in if i > 1 andalso length ts < i then
    6.89 -      Codegen.invoke_codegen thy defs dep module brack (Codegen.eta_expand c ts i) gr
    6.90 +      Codegen.invoke_codegen thy mode defs dep module brack (Codegen.eta_expand c ts i) gr
    6.91       else
    6.92         let
    6.93           val id = Codegen.mk_qual_id module (Codegen.get_const_id gr s);
    6.94           val (ps, gr') = fold_map
    6.95 -           (Codegen.invoke_codegen thy defs dep module (i = 1)) ts gr;
    6.96 +           (Codegen.invoke_codegen thy mode defs dep module (i = 1)) ts gr;
    6.97         in
    6.98          (case args of
    6.99            _ :: _ :: _ => (if brack then Codegen.parens else I)
   6.100 @@ -385,14 +385,14 @@
   6.101  
   6.102  (* code generators for terms and types *)
   6.103  
   6.104 -fun datatype_codegen thy defs dep module brack t gr =
   6.105 +fun datatype_codegen thy mode defs dep module brack t gr =
   6.106    (case strip_comb t of
   6.107      (c as Const (s, T), ts) =>
   6.108        (case Datatype_Data.info_of_case thy s of
   6.109          SOME {index, descr, ...} =>
   6.110            if is_some (Codegen.get_assoc_code thy (s, T)) then NONE
   6.111            else
   6.112 -            SOME (pretty_case thy defs dep module brack
   6.113 +            SOME (pretty_case thy mode defs dep module brack
   6.114                (#3 (the (AList.lookup op = descr index))) c ts gr)
   6.115        | NONE =>
   6.116            (case (Datatype_Data.info_of_constr thy (s, T), body_type T) of
   6.117 @@ -406,28 +406,28 @@
   6.118                    if tyname <> tyname' then NONE
   6.119                    else
   6.120                      SOME
   6.121 -                      (pretty_constr thy defs
   6.122 +                      (pretty_constr thy mode defs
   6.123                          dep module brack args c ts
   6.124 -                        (snd (Codegen.invoke_tycodegen thy defs dep module false U gr)))
   6.125 +                        (snd (Codegen.invoke_tycodegen thy mode defs dep module false U gr)))
   6.126                  end
   6.127            | _ => NONE))
   6.128    | _ => NONE);
   6.129  
   6.130 -fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
   6.131 +fun datatype_tycodegen thy mode defs dep module brack (Type (s, Ts)) gr =
   6.132        (case Datatype_Data.get_info thy s of
   6.133           NONE => NONE
   6.134         | SOME {descr, sorts, ...} =>
   6.135             if is_some (Codegen.get_assoc_type thy s) then NONE else
   6.136             let
   6.137               val (ps, gr') = fold_map
   6.138 -               (Codegen.invoke_tycodegen thy defs dep module false) Ts gr;
   6.139 -             val (module', gr'') = add_dt_defs thy defs dep module descr sorts gr' ;
   6.140 +               (Codegen.invoke_tycodegen thy mode defs dep module false) Ts gr;
   6.141 +             val (module', gr'') = add_dt_defs thy mode defs dep module descr sorts gr' ;
   6.142               val (tyid, gr''') = Codegen.mk_type_id module' s gr''
   6.143             in SOME (Pretty.block ((if null Ts then [] else
   6.144                 [Codegen.mk_tuple ps, Codegen.str " "]) @
   6.145                 [Codegen.str (Codegen.mk_qual_id module tyid)]), gr''')
   6.146             end)
   6.147 -  | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
   6.148 +  | datatype_tycodegen _ _ _ _ _ _ _ _ = NONE;
   6.149  
   6.150  
   6.151  (** theory setup **)
     7.1 --- a/src/HOL/Tools/inductive_codegen.ML	Tue Apr 19 22:32:49 2011 +0200
     7.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Tue Apr 19 23:57:28 2011 +0200
     7.3 @@ -239,9 +239,9 @@
     7.4              end)
     7.5                ps));
     7.6  
     7.7 -fun use_random () = member (op =) (!Codegen.mode) "random_ind";
     7.8 +fun use_random codegen_mode = member (op =) codegen_mode "random_ind";
     7.9  
    7.10 -fun check_mode_clause thy arg_vs modes ((iss, is), rnd) (ts, ps) =
    7.11 +fun check_mode_clause thy codegen_mode arg_vs modes ((iss, is), rnd) (ts, ps) =
    7.12    let
    7.13      val modes' = modes @ map_filter
    7.14        (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [(([], js), false)]))
    7.15 @@ -253,7 +253,7 @@
    7.16              (rnd orelse needs_random m)
    7.17              (filter_out (equal x) ps)
    7.18          | (_, (_, vs') :: _) :: _ =>
    7.19 -            if use_random () then
    7.20 +            if use_random codegen_mode then
    7.21                check_mode_prems (union (op =) vs (map (fst o fst) vs')) true ps
    7.22              else NONE
    7.23          | _ => NONE);
    7.24 @@ -268,17 +268,17 @@
    7.25           let val missing_vs = missing_vars vs ts
    7.26           in
    7.27             if null missing_vs orelse
    7.28 -             use_random () andalso monomorphic_vars missing_vs
    7.29 +             use_random codegen_mode andalso monomorphic_vars missing_vs
    7.30             then SOME (rnd' orelse not (null missing_vs))
    7.31             else NONE
    7.32           end)
    7.33      else NONE
    7.34    end;
    7.35  
    7.36 -fun check_modes_pred thy arg_vs preds modes (p, ms) =
    7.37 +fun check_modes_pred thy codegen_mode arg_vs preds modes (p, ms) =
    7.38    let val SOME rs = AList.lookup (op =) preds p
    7.39    in (p, List.mapPartial (fn m as (m', _) =>
    7.40 -    let val xs = map (check_mode_clause thy arg_vs modes m) rs
    7.41 +    let val xs = map (check_mode_clause thy codegen_mode arg_vs modes m) rs
    7.42      in case find_index is_none xs of
    7.43          ~1 => SOME (m', exists (fn SOME b => b) xs)
    7.44        | i => (Codegen.message ("Clause " ^ string_of_int (i+1) ^ " of " ^
    7.45 @@ -290,8 +290,8 @@
    7.46    let val y = f x
    7.47    in if x = y then x else fixp f y end;
    7.48  
    7.49 -fun infer_modes thy extra_modes arities arg_vs preds = fixp (fn modes =>
    7.50 -  map (check_modes_pred thy arg_vs preds (modes @ extra_modes)) modes)
    7.51 +fun infer_modes thy codegen_mode extra_modes arities arg_vs preds = fixp (fn modes =>
    7.52 +  map (check_modes_pred thy codegen_mode arg_vs preds (modes @ extra_modes)) modes)
    7.53      (map (fn (s, (ks, k)) => (s, map (rpair false) (cprod (cprods (map
    7.54        (fn NONE => [NONE]
    7.55          | SOME k' => map SOME (subsets 1 k')) ks),
    7.56 @@ -358,34 +358,34 @@
    7.57      separate (Pretty.brk 1) (Codegen.str s :: replicate k (Codegen.str "|> ???")) @
    7.58      (if k = 0 then [] else [Codegen.str ")"])), Pretty.brk 1, p]);
    7.59  
    7.60 -fun compile_expr thy defs dep module brack modes (NONE, t) gr =
    7.61 -      apfst single (Codegen.invoke_codegen thy defs dep module brack t gr)
    7.62 -  | compile_expr _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr =
    7.63 +fun compile_expr thy codegen_mode defs dep module brack modes (NONE, t) gr =
    7.64 +      apfst single (Codegen.invoke_codegen thy codegen_mode defs dep module brack t gr)
    7.65 +  | compile_expr _ _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr =
    7.66        ([Codegen.str name], gr)
    7.67 -  | compile_expr thy defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr =
    7.68 +  | compile_expr thy codegen_mode defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr =
    7.69        (case strip_comb t of
    7.70           (Const (name, _), args) =>
    7.71             if name = @{const_name HOL.eq} orelse AList.defined op = modes name then
    7.72               let
    7.73                 val (args1, args2) = chop (length ms) args;
    7.74                 val ((ps, mode_id), gr') = gr |> fold_map
    7.75 -                   (compile_expr thy defs dep module true modes) (ms ~~ args1)
    7.76 +                   (compile_expr thy codegen_mode defs dep module true modes) (ms ~~ args1)
    7.77                     ||>> modename module name mode;
    7.78                 val (ps', gr'') = (case mode of
    7.79                     ([], []) => ([Codegen.str "()"], gr')
    7.80                   | _ => fold_map
    7.81 -                     (Codegen.invoke_codegen thy defs dep module true) args2 gr')
    7.82 +                     (Codegen.invoke_codegen thy codegen_mode defs dep module true) args2 gr')
    7.83               in ((if brack andalso not (null ps andalso null ps') then
    7.84                 single o Codegen.parens o Pretty.block else I)
    7.85                   (flat (separate [Pretty.brk 1]
    7.86                     ([Codegen.str mode_id] :: ps @ map single ps'))), gr')
    7.87               end
    7.88             else apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
    7.89 -             (Codegen.invoke_codegen thy defs dep module true t gr)
    7.90 +             (Codegen.invoke_codegen thy codegen_mode defs dep module true t gr)
    7.91         | _ => apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
    7.92 -           (Codegen.invoke_codegen thy defs dep module true t gr));
    7.93 +           (Codegen.invoke_codegen thy codegen_mode defs dep module true t gr));
    7.94  
    7.95 -fun compile_clause thy defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr =
    7.96 +fun compile_clause thy codegen_mode defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr =
    7.97    let
    7.98      val modes' = modes @ map_filter
    7.99        (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [(([], js), false)]))
   7.100 @@ -399,7 +399,7 @@
   7.101  
   7.102      fun compile_eq (s, t) gr =
   7.103        apfst (Pretty.block o cons (Codegen.str (s ^ " = ")) o single)
   7.104 -        (Codegen.invoke_codegen thy defs dep module false t gr);
   7.105 +        (Codegen.invoke_codegen thy codegen_mode defs dep module false t gr);
   7.106  
   7.107      val (in_ts, out_ts) = get_args is 1 ts;
   7.108      val (in_ts', (all_vs', eqs)) = fold_map check_constrt in_ts (all_vs, []);
   7.109 @@ -407,13 +407,13 @@
   7.110      fun compile_prems out_ts' vs names [] gr =
   7.111            let
   7.112              val (out_ps, gr2) =
   7.113 -              fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts gr;
   7.114 +              fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module false) out_ts gr;
   7.115              val (eq_ps, gr3) = fold_map compile_eq eqs gr2;
   7.116              val (out_ts'', (names', eqs')) = fold_map check_constrt out_ts' (names, []);
   7.117              val (out_ts''', nvs) =
   7.118                fold_map distinct_v out_ts'' (names', map (fn x => (x, [x])) vs);
   7.119              val (out_ps', gr4) =
   7.120 -              fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts''' gr3;
   7.121 +              fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module false) out_ts''' gr3;
   7.122              val (eq_ps', gr5) = fold_map compile_eq eqs' gr4;
   7.123              val vs' = distinct (op =) (flat (vs :: map term_vs out_ts'));
   7.124              val missing_vs = missing_vars vs' out_ts;
   7.125 @@ -425,7 +425,7 @@
   7.126                   final_p (exists (not o is_exhaustive) out_ts'''), gr5)
   7.127              else
   7.128                let
   7.129 -                val (pat_p, gr6) = Codegen.invoke_codegen thy defs dep module true
   7.130 +                val (pat_p, gr6) = Codegen.invoke_codegen thy codegen_mode defs dep module true
   7.131                    (HOLogic.mk_tuple (map Var missing_vs)) gr5;
   7.132                  val gen_p =
   7.133                    Codegen.mk_gen gr6 module true [] ""
   7.134 @@ -445,7 +445,7 @@
   7.135              val (out_ts', (names', eqs)) = fold_map check_constrt out_ts (names, []);
   7.136              val (out_ts'', nvs) = fold_map distinct_v out_ts' (names', map (fn x => (x, [x])) vs);
   7.137              val (out_ps, gr0) =
   7.138 -              fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts'' gr;
   7.139 +              fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module false) out_ts'' gr;
   7.140              val (eq_ps, gr1) = fold_map compile_eq eqs gr0;
   7.141            in
   7.142              (case hd (select_mode_prem thy modes' vs' ps) of
   7.143 @@ -454,13 +454,13 @@
   7.144                     val ps' = filter_out (equal p) ps;
   7.145                     val (in_ts, out_ts''') = get_args js 1 us;
   7.146                     val (in_ps, gr2) =
   7.147 -                    fold_map (Codegen.invoke_codegen thy defs dep module true) in_ts gr1;
   7.148 +                    fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module true) in_ts gr1;
   7.149                     val (ps, gr3) =
   7.150                       if not is_set then
   7.151                         apfst (fn ps => ps @
   7.152                             (if null in_ps then [] else [Pretty.brk 1]) @
   7.153                             separate (Pretty.brk 1) in_ps)
   7.154 -                         (compile_expr thy defs dep module false modes
   7.155 +                         (compile_expr thy codegen_mode defs dep module false modes
   7.156                             (SOME mode, t) gr2)
   7.157                       else
   7.158                         apfst (fn p =>
   7.159 @@ -468,7 +468,7 @@
   7.160                           Codegen.str "of", Codegen.str "Set", Codegen.str "xs", Codegen.str "=>",
   7.161                           Codegen.str "xs)"])
   7.162                           (*this is a very strong assumption about the generated code!*)
   7.163 -                           (Codegen.invoke_codegen thy defs dep module true t gr2);
   7.164 +                           (Codegen.invoke_codegen thy codegen_mode defs dep module true t gr2);
   7.165                     val (rest, gr4) = compile_prems out_ts''' vs' (fst nvs) ps' gr3;
   7.166                   in
   7.167                     (compile_match (snd nvs) eq_ps out_ps
   7.168 @@ -479,7 +479,8 @@
   7.169               | (p as Sidecond t, [(_, [])]) =>
   7.170                   let
   7.171                     val ps' = filter_out (equal p) ps;
   7.172 -                   val (side_p, gr2) = Codegen.invoke_codegen thy defs dep module true t gr1;
   7.173 +                   val (side_p, gr2) =
   7.174 +                    Codegen.invoke_codegen thy codegen_mode defs dep module true t gr1;
   7.175                     val (rest, gr3) = compile_prems [] vs' (fst nvs) ps' gr2;
   7.176                   in
   7.177                     (compile_match (snd nvs) eq_ps out_ps
   7.178 @@ -490,7 +491,8 @@
   7.179               | (_, (_, missing_vs) :: _) =>
   7.180                   let
   7.181                     val T = HOLogic.mk_tupleT (map snd missing_vs);
   7.182 -                   val (_, gr2) = Codegen.invoke_tycodegen thy defs dep module false T gr1;
   7.183 +                   val (_, gr2) =
   7.184 +                    Codegen.invoke_tycodegen thy codegen_mode defs dep module false T gr1;
   7.185                     val gen_p = Codegen.mk_gen gr2 module true [] "" T;
   7.186                     val (rest, gr3) = compile_prems
   7.187                       [HOLogic.mk_tuple (map Var missing_vs)] vs' (fst nvs) ps gr2
   7.188 @@ -508,12 +510,12 @@
   7.189         Codegen.str " :->", Pretty.brk 1, prem_p], gr')
   7.190    end;
   7.191  
   7.192 -fun compile_pred thy defs dep module prfx all_vs arg_vs modes s cls mode gr =
   7.193 +fun compile_pred thy codegen_mode defs dep module prfx all_vs arg_vs modes s cls mode gr =
   7.194    let
   7.195      val xs = map Codegen.str (Name.variant_list arg_vs
   7.196        (map (fn i => "x" ^ string_of_int i) (snd mode)));
   7.197      val ((cl_ps, mode_id), gr') = gr |>
   7.198 -      fold_map (fn cl => compile_clause thy defs
   7.199 +      fold_map (fn cl => compile_clause thy codegen_mode defs
   7.200          dep module all_vs arg_vs modes mode cl (mk_tuple xs)) cls ||>>
   7.201        modename module s mode
   7.202    in
   7.203 @@ -527,9 +529,9 @@
   7.204         flat (separate [Codegen.str " ++", Pretty.brk 1] (map single cl_ps))), (gr', "and "))
   7.205    end;
   7.206  
   7.207 -fun compile_preds thy defs dep module all_vs arg_vs modes preds gr =
   7.208 +fun compile_preds thy codegen_mode defs dep module all_vs arg_vs modes preds gr =
   7.209    let val (prs, (gr', _)) = fold_map (fn (s, cls) =>
   7.210 -    fold_map (fn (mode, _) => fn (gr', prfx') => compile_pred thy defs
   7.211 +    fold_map (fn (mode, _) => fn (gr', prfx') => compile_pred thy codegen_mode defs
   7.212        dep module prfx' all_vs arg_vs modes s cls mode gr')
   7.213          (((the o AList.lookup (op =) modes) s))) preds (gr, "fun ")
   7.214    in
   7.215 @@ -562,18 +564,19 @@
   7.216            NONE => xs
   7.217          | SOME xs' => inter (op = o apfst fst) xs' xs) :: constrain cs ys;
   7.218  
   7.219 -fun mk_extra_defs thy defs gr dep names module ts =
   7.220 +fun mk_extra_defs thy codegen_mode defs gr dep names module ts =
   7.221    fold (fn name => fn gr =>
   7.222      if member (op =) names name then gr
   7.223      else
   7.224        (case get_clauses thy name of
   7.225          NONE => gr
   7.226        | SOME (names, thyname, nparms, intrs) =>
   7.227 -          mk_ind_def thy defs gr dep names (Codegen.if_library thyname module)
   7.228 +          mk_ind_def thy codegen_mode defs gr dep names
   7.229 +            (Codegen.if_library codegen_mode thyname module)
   7.230              [] (prep_intrs intrs) nparms))
   7.231      (fold Term.add_const_names ts []) gr
   7.232  
   7.233 -and mk_ind_def thy defs gr dep names module modecs intrs nparms =
   7.234 +and mk_ind_def thy codegen_mode defs gr dep names module modecs intrs nparms =
   7.235    Codegen.add_edge_acyclic (hd names, dep) gr handle
   7.236      Graph.CYCLES (xs :: _) =>
   7.237        error ("Inductive_Codegen: illegal cyclic dependencies:\n" ^ commas xs)
   7.238 @@ -617,16 +620,16 @@
   7.239               length Us)) arities)
   7.240          end;
   7.241  
   7.242 -      val gr' = mk_extra_defs thy defs
   7.243 +      val gr' = mk_extra_defs thy codegen_mode defs
   7.244          (Codegen.add_edge (hd names, dep)
   7.245            (Codegen.new_node (hd names, (NONE, "", "")) gr)) (hd names) names module intrs;
   7.246        val (extra_modes, extra_arities) = lookup_modes gr' (hd names);
   7.247        val (clauses, arities) = fold add_clause intrs ([], []);
   7.248        val modes = constrain modecs
   7.249 -        (infer_modes thy extra_modes arities arg_vs clauses);
   7.250 +        (infer_modes thy codegen_mode extra_modes arities arg_vs clauses);
   7.251        val _ = print_arities arities;
   7.252        val _ = print_modes modes;
   7.253 -      val (s, gr'') = compile_preds thy defs (hd names) module (terms_vs intrs)
   7.254 +      val (s, gr'') = compile_preds thy codegen_mode defs (hd names) module (terms_vs intrs)
   7.255          arg_vs (modes @ extra_modes) clauses gr';
   7.256      in
   7.257        (Codegen.map_node (hd names)
   7.258 @@ -639,7 +642,7 @@
   7.259         ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
   7.260     | mode => mode);
   7.261  
   7.262 -fun mk_ind_call thy defs dep module is_query s T ts names thyname k intrs gr =
   7.263 +fun mk_ind_call thy codegen_mode defs dep module is_query s T ts names thyname k intrs gr =
   7.264    let
   7.265      val (ts1, ts2) = chop k ts;
   7.266      val u = list_comb (Const (s, T), ts1);
   7.267 @@ -647,9 +650,9 @@
   7.268      fun mk_mode (Const (@{const_name dummy_pattern}, _)) ((ts, mode), i) = ((ts, mode), i + 1)
   7.269        | mk_mode t ((ts, mode), i) = ((ts @ [t], mode @ [i]), i + 1);
   7.270  
   7.271 -    val module' = Codegen.if_library thyname module;
   7.272 -    val gr1 = mk_extra_defs thy defs
   7.273 -      (mk_ind_def thy defs gr dep names module'
   7.274 +    val module' = Codegen.if_library codegen_mode thyname module;
   7.275 +    val gr1 = mk_extra_defs thy codegen_mode defs
   7.276 +      (mk_ind_def thy codegen_mode defs gr dep names module'
   7.277        [] (prep_intrs intrs) k) dep names module' [u];
   7.278      val (modes, _) = lookup_modes gr1 dep;
   7.279      val (ts', is) =
   7.280 @@ -658,8 +661,9 @@
   7.281      val mode = find_mode gr1 dep s u modes is;
   7.282      val _ = if is_query orelse not (needs_random (the mode)) then ()
   7.283        else warning ("Illegal use of random data generators in " ^ s);
   7.284 -    val (in_ps, gr2) = fold_map (Codegen.invoke_codegen thy defs dep module true) ts' gr1;
   7.285 -    val (ps, gr3) = compile_expr thy defs dep module false modes (mode, u) gr2;
   7.286 +    val (in_ps, gr2) =
   7.287 +      fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module true) ts' gr1;
   7.288 +    val (ps, gr3) = compile_expr thy codegen_mode defs dep module false modes (mode, u) gr2;
   7.289    in
   7.290      (Pretty.block (ps @ (if null in_ps then [] else [Pretty.brk 1]) @
   7.291         separate (Pretty.brk 1) in_ps), gr3)
   7.292 @@ -675,7 +679,7 @@
   7.293        (list_comb (Const (s ^ "_aux", Ts @ [U] ---> HOLogic.boolT), ts @ [u]))))
   7.294    end;
   7.295  
   7.296 -fun mk_fun thy defs name eqns dep module module' gr =
   7.297 +fun mk_fun thy codegen_mode defs name eqns dep module module' gr =
   7.298    case try (Codegen.get_node gr) name of
   7.299      NONE =>
   7.300      let
   7.301 @@ -693,7 +697,7 @@
   7.302           Pretty.brk 1, Codegen.str "DSeq.hd", Pretty.brk 1,
   7.303           Codegen.parens (Pretty.block (separate (Pretty.brk 1) (Codegen.str mode_id ::
   7.304             vars)))]) ^ ";\n\n";
   7.305 -      val gr'' = mk_ind_def thy defs (Codegen.add_edge (name, dep)
   7.306 +      val gr'' = mk_ind_def thy codegen_mode defs (Codegen.add_edge (name, dep)
   7.307          (Codegen.new_node (name, (NONE, module', s)) gr')) name [pname] module'
   7.308          [(pname, [([], mode)])] clauses 0;
   7.309        val (modes, _) = lookup_modes gr'' dep;
   7.310 @@ -726,7 +730,7 @@
   7.311      else p
   7.312    end;
   7.313  
   7.314 -fun inductive_codegen thy defs dep module brack t gr  = (case strip_comb t of
   7.315 +fun inductive_codegen thy codegen_mode defs dep module brack t gr  = (case strip_comb t of
   7.316      (Const (@{const_name Collect}, _), [u]) =>
   7.317        let val (r, Ts, fs) = HOLogic.strip_psplits u
   7.318        in case strip_comb r of
   7.319 @@ -743,7 +747,7 @@
   7.320                    if null (duplicates op = ots) andalso
   7.321                      closed ts1 andalso closed its
   7.322                    then
   7.323 -                    let val (call_p, gr') = mk_ind_call thy defs dep module true
   7.324 +                    let val (call_p, gr') = mk_ind_call thy codegen_mode defs dep module true
   7.325                        s T (ts1 @ ts2') names thyname k intrs gr 
   7.326                      in SOME ((if brack then Codegen.parens else I) (Pretty.block
   7.327                        [Codegen.str "Set", Pretty.brk 1, Codegen.str "(DSeq.list_of", Pretty.brk 1,
   7.328 @@ -762,20 +766,21 @@
   7.329        (case (get_clauses thy s, Codegen.get_assoc_code thy (s, T)) of
   7.330          (SOME (names, thyname, k, intrs), NONE) =>
   7.331            if length ts < k then NONE else SOME
   7.332 -            (let val (call_p, gr') = mk_ind_call thy defs dep module false
   7.333 +            (let val (call_p, gr') = mk_ind_call thy codegen_mode defs dep module false
   7.334                 s T (map Term.no_dummy_patterns ts) names thyname k intrs gr
   7.335               in (mk_funcomp brack "?!"
   7.336                 (length (binder_types T) - length ts) (Codegen.parens call_p), gr')
   7.337 -             end handle TERM _ => mk_ind_call thy defs dep module true
   7.338 +             end handle TERM _ => mk_ind_call thy codegen_mode defs dep module true
   7.339                 s T ts names thyname k intrs gr )
   7.340        | _ => NONE)
   7.341      | SOME eqns =>
   7.342          let
   7.343            val (_, thyname) :: _ = eqns;
   7.344 -          val (id, gr') = mk_fun thy defs s (Codegen.preprocess thy (map fst (rev eqns)))
   7.345 -            dep module (Codegen.if_library thyname module) gr;
   7.346 -          val (ps, gr'') = fold_map
   7.347 -            (Codegen.invoke_codegen thy defs dep module true) ts gr';
   7.348 +          val (id, gr') =
   7.349 +            mk_fun thy codegen_mode defs s (Codegen.preprocess thy (map fst (rev eqns)))
   7.350 +              dep module (Codegen.if_library codegen_mode thyname module) gr;
   7.351 +          val (ps, gr'') =
   7.352 +            fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module true) ts gr';
   7.353          in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'')
   7.354          end)
   7.355    | _ => NONE);
   7.356 @@ -830,8 +835,9 @@
   7.357      val pred = HOLogic.mk_Trueprop (list_comb
   7.358        (Const (Sign.intern_const thy' "quickcheckp", T),
   7.359         map Term.dummy_pattern Ts));
   7.360 -    val (code, gr) = setmp_CRITICAL Codegen.mode ["term_of", "test", "random_ind"]
   7.361 -      (Codegen.generate_code_i thy' [] "Generated") [("testf", pred)];
   7.362 +    val (code, gr) =
   7.363 +      Codegen.generate_code_i thy' ["term_of", "test", "random_ind"] [] "Generated"
   7.364 +        [("testf", pred)];
   7.365      val s = "structure TestTerm =\nstruct\n\n" ^
   7.366        cat_lines (map snd code) ^
   7.367        "\nopen Generated;\n\n" ^ Codegen.string_of
     8.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue Apr 19 22:32:49 2011 +0200
     8.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Apr 19 23:57:28 2011 +0200
     8.3 @@ -70,7 +70,7 @@
     8.4    if member (op =) xs x then xs
     8.5    else fold (cycle g) (flat (Graph.all_paths (fst g) (x, x))) (x :: xs);
     8.6  
     8.7 -fun add_rec_funs thy defs dep module eqs gr =
     8.8 +fun add_rec_funs thy mode defs dep module eqs gr =
     8.9    let
    8.10      fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
    8.11        Logic.dest_equals (Codegen.rename_term t));
    8.12 @@ -81,10 +81,10 @@
    8.13      fun mk_fundef module fname first [] gr = ([], gr)
    8.14        | mk_fundef module fname first ((fname' : string, (lhs, rhs)) :: xs) gr =
    8.15        let
    8.16 -        val (pl, gr1) = Codegen.invoke_codegen thy defs dname module false lhs gr;
    8.17 -        val (pr, gr2) = Codegen.invoke_codegen thy defs dname module false rhs gr1;
    8.18 +        val (pl, gr1) = Codegen.invoke_codegen thy mode defs dname module false lhs gr;
    8.19 +        val (pr, gr2) = Codegen.invoke_codegen thy mode defs dname module false rhs gr1;
    8.20          val (rest, gr3) = mk_fundef module fname' false xs gr2 ;
    8.21 -        val (ty, gr4) = Codegen.invoke_tycodegen thy defs dname module false T gr3;
    8.22 +        val (ty, gr4) = Codegen.invoke_tycodegen thy mode defs dname module false T gr3;
    8.23          val num_args = (length o snd o strip_comb) lhs;
    8.24          val prfx = if fname = fname' then "  |"
    8.25            else if not first then "and"
    8.26 @@ -121,7 +121,7 @@
    8.27               if not (member (op =) xs dep) then
    8.28                 let
    8.29                   val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
    8.30 -                 val module' = Codegen.if_library thyname module;
    8.31 +                 val module' = Codegen.if_library mode thyname module;
    8.32                   val eqs'' = map (dest_eq o prop_of) (maps fst thmss);
    8.33                   val (fundef', gr3) = mk_fundef module' "" true eqs''
    8.34                     (Codegen.add_edge (dname, dep)
    8.35 @@ -137,7 +137,7 @@
    8.36            else if s = dep then gr else Codegen.add_edge (s, dep) gr))
    8.37    end;
    8.38  
    8.39 -fun recfun_codegen thy defs dep module brack t gr =
    8.40 +fun recfun_codegen thy mode defs dep module brack t gr =
    8.41    (case strip_comb t of
    8.42      (Const (p as (s, T)), ts) =>
    8.43       (case (get_equations thy defs p, Codegen.get_assoc_code thy (s, T)) of
    8.44 @@ -145,12 +145,12 @@
    8.45       | (_, SOME _) => NONE
    8.46       | ((eqns, thyname), NONE) =>
    8.47          let
    8.48 -          val module' = Codegen.if_library thyname module;
    8.49 +          val module' = Codegen.if_library mode thyname module;
    8.50            val (ps, gr') = fold_map
    8.51 -            (Codegen.invoke_codegen thy defs dep module true) ts gr;
    8.52 +            (Codegen.invoke_codegen thy mode defs dep module true) ts gr;
    8.53            val suffix = mk_suffix thy defs p;
    8.54            val (module'', gr'') =
    8.55 -            add_rec_funs thy defs dep module' (map prop_of eqns) gr';
    8.56 +            add_rec_funs thy mode defs dep module' (map prop_of eqns) gr';
    8.57            val (fname, gr''') = Codegen.mk_const_id module'' (s ^ suffix) gr''
    8.58          in
    8.59            SOME (Codegen.mk_app brack (Codegen.str (Codegen.mk_qual_id module fname)) ps, gr''')
     9.1 --- a/src/Pure/codegen.ML	Tue Apr 19 22:32:49 2011 +0200
     9.2 +++ b/src/Pure/codegen.ML	Tue Apr 19 23:57:28 2011 +0200
     9.3 @@ -8,7 +8,6 @@
     9.4  sig
     9.5    val quiet_mode : bool Unsynchronized.ref
     9.6    val message : string -> unit
     9.7 -  val mode : string list Unsynchronized.ref
     9.8    val margin : int Unsynchronized.ref
     9.9    val string_of : Pretty.T -> string
    9.10    val str : string -> Pretty.T
    9.11 @@ -31,9 +30,9 @@
    9.12    val preprocess: theory -> thm list -> thm list
    9.13    val preprocess_term: theory -> term -> term
    9.14    val print_codegens: theory -> unit
    9.15 -  val generate_code: theory -> string list -> string -> (string * string) list ->
    9.16 +  val generate_code: theory -> string list -> string list -> string -> (string * string) list ->
    9.17      (string * string) list * codegr
    9.18 -  val generate_code_i: theory -> string list -> string -> (string * term) list ->
    9.19 +  val generate_code_i: theory -> string list -> string list -> string -> (string * term) list ->
    9.20      (string * string) list * codegr
    9.21    val assoc_const: string * (term mixfix list *
    9.22      (string * string) list) -> theory -> theory
    9.23 @@ -46,9 +45,9 @@
    9.24    val get_assoc_type: theory -> string ->
    9.25      (typ mixfix list * (string * string) list) option
    9.26    val codegen_error: codegr -> string -> string -> 'a
    9.27 -  val invoke_codegen: theory -> deftab -> string -> string -> bool ->
    9.28 +  val invoke_codegen: theory -> string list -> deftab -> string -> string -> bool ->
    9.29      term -> codegr -> Pretty.T * codegr
    9.30 -  val invoke_tycodegen: theory -> deftab -> string -> string -> bool ->
    9.31 +  val invoke_tycodegen: theory -> string list -> deftab -> string -> string -> bool ->
    9.32      typ -> codegr -> Pretty.T * codegr
    9.33    val mk_id: string -> string
    9.34    val mk_qual_id: string -> string * string -> string
    9.35 @@ -62,7 +61,7 @@
    9.36    val rename_term: term -> term
    9.37    val new_names: term -> string list -> string list
    9.38    val new_name: term -> string -> string
    9.39 -  val if_library: 'a -> 'a -> 'a
    9.40 +  val if_library: string list -> 'a -> 'a -> 'a
    9.41    val get_defn: theory -> deftab -> string -> typ ->
    9.42      ((typ * (string * thm)) * int option) option
    9.43    val is_instance: typ -> typ -> bool
    9.44 @@ -105,8 +104,6 @@
    9.45  val quiet_mode = Unsynchronized.ref true;
    9.46  fun message s = if !quiet_mode then () else writeln s;
    9.47  
    9.48 -val mode = Unsynchronized.ref ([] : string list);   (* FIXME proper functional argument *)
    9.49 -
    9.50  val margin = Unsynchronized.ref 80;
    9.51  
    9.52  fun string_of p = Print_Mode.setmp [] (Pretty.string_of_margin (!margin)) p;
    9.53 @@ -171,13 +168,14 @@
    9.54  (* type of code generators *)
    9.55  
    9.56  type 'a codegen =
    9.57 -  theory ->    (* theory in which generate_code was called *)
    9.58 -  deftab ->    (* definition table (for efficiency) *)
    9.59 -  string ->    (* node name of caller (for recording dependencies) *)
    9.60 -  string ->    (* module name of caller (for modular code generation) *)
    9.61 -  bool ->      (* whether to parenthesize generated expression *)
    9.62 -  'a ->        (* item to generate code from *)
    9.63 -  codegr ->    (* code dependency graph *)
    9.64 +  theory ->      (* theory in which generate_code was called *)
    9.65 +  string list -> (* mode *)
    9.66 +  deftab ->      (* definition table (for efficiency) *)
    9.67 +  string ->      (* node name of caller (for recording dependencies) *)
    9.68 +  string ->      (* module name of caller (for modular code generation) *)
    9.69 +  bool ->        (* whether to parenthesize generated expression *)
    9.70 +  'a ->          (* item to generate code from *)
    9.71 +  codegr ->      (* code dependency graph *)
    9.72    (Pretty.T * codegr) option;
    9.73  
    9.74  
    9.75 @@ -478,8 +476,8 @@
    9.76  fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
    9.77    s = s' andalso is_instance T T') (#consts (CodegenData.get thy)));
    9.78  
    9.79 -fun get_aux_code xs = map_filter (fn (m, code) =>
    9.80 -  if m = "" orelse member (op =) (!mode) m then SOME code else NONE) xs;
    9.81 +fun get_aux_code mode xs = map_filter (fn (m, code) =>
    9.82 +  if m = "" orelse member (op =) mode m then SOME code else NONE) xs;
    9.83  
    9.84  fun dest_prim_def t =
    9.85    let
    9.86 @@ -525,14 +523,14 @@
    9.87  fun codegen_error (gr, _) dep s =
    9.88    error (s ^ "\nrequired by:\n" ^ commas (Graph.all_succs gr [dep]));
    9.89  
    9.90 -fun invoke_codegen thy defs dep module brack t gr = (case get_first
    9.91 -   (fn (_, f) => f thy defs dep module brack t gr) (#codegens (CodegenData.get thy)) of
    9.92 +fun invoke_codegen thy mode defs dep module brack t gr = (case get_first
    9.93 +   (fn (_, f) => f thy mode defs dep module brack t gr) (#codegens (CodegenData.get thy)) of
    9.94        NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^
    9.95          Syntax.string_of_term_global thy t)
    9.96      | SOME x => x);
    9.97  
    9.98 -fun invoke_tycodegen thy defs dep module brack T gr = (case get_first
    9.99 -   (fn (_, f) => f thy defs dep module brack T gr ) (#tycodegens (CodegenData.get thy)) of
   9.100 +fun invoke_tycodegen thy mode defs dep module brack T gr = (case get_first
   9.101 +   (fn (_, f) => f thy mode defs dep module brack T gr ) (#tycodegens (CodegenData.get thy)) of
   9.102        NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^
   9.103          Syntax.string_of_typ_global thy T)
   9.104      | SOME x => x);
   9.105 @@ -597,17 +595,17 @@
   9.106  
   9.107  fun new_name t x = hd (new_names t [x]);
   9.108  
   9.109 -fun if_library x y = if member (op =) (!mode) "library" then x else y;
   9.110 +fun if_library mode x y = if member (op =) mode "library" then x else y;
   9.111  
   9.112 -fun default_codegen thy defs dep module brack t gr =
   9.113 +fun default_codegen thy mode defs dep module brack t gr =
   9.114    let
   9.115      val (u, ts) = strip_comb t;
   9.116 -    fun codegens brack = fold_map (invoke_codegen thy defs dep module brack)
   9.117 +    fun codegens brack = fold_map (invoke_codegen thy mode defs dep module brack)
   9.118    in (case u of
   9.119        Var ((s, i), T) =>
   9.120          let
   9.121            val (ps, gr') = codegens true ts gr;
   9.122 -          val (_, gr'') = invoke_tycodegen thy defs dep module false T gr'
   9.123 +          val (_, gr'') = invoke_tycodegen thy mode defs dep module false T gr'
   9.124          in SOME (mk_app brack (str (s ^
   9.125             (if i=0 then "" else string_of_int i))) ps, gr'')
   9.126          end
   9.127 @@ -615,7 +613,7 @@
   9.128      | Free (s, T) =>
   9.129          let
   9.130            val (ps, gr') = codegens true ts gr;
   9.131 -          val (_, gr'') = invoke_tycodegen thy defs dep module false T gr'
   9.132 +          val (_, gr'') = invoke_tycodegen thy mode defs dep module false T gr'
   9.133          in SOME (mk_app brack (str s) ps, gr'') end
   9.134  
   9.135      | Const (s, T) =>
   9.136 @@ -623,26 +621,26 @@
   9.137           SOME (ms, aux) =>
   9.138             let val i = num_args_of ms
   9.139             in if length ts < i then
   9.140 -               default_codegen thy defs dep module brack (eta_expand u ts i) gr 
   9.141 +               default_codegen thy mode defs dep module brack (eta_expand u ts i) gr 
   9.142               else
   9.143                 let
   9.144                   val (ts1, ts2) = args_of ms ts;
   9.145                   val (ps1, gr1) = codegens false ts1 gr;
   9.146                   val (ps2, gr2) = codegens true ts2 gr1;
   9.147                   val (ps3, gr3) = codegens false (quotes_of ms) gr2;
   9.148 -                 val (_, gr4) = invoke_tycodegen thy defs dep module false
   9.149 +                 val (_, gr4) = invoke_tycodegen thy mode defs dep module false
   9.150                     (funpow (length ts) (hd o tl o snd o dest_Type) T) gr3;
   9.151                   val (module', suffix) = (case get_defn thy defs s T of
   9.152 -                     NONE => (if_library (thyname_of_const thy s) module, "")
   9.153 +                     NONE => (if_library mode (thyname_of_const thy s) module, "")
   9.154                     | SOME ((U, (module', _)), NONE) =>
   9.155 -                       (if_library module' module, "")
   9.156 +                       (if_library mode module' module, "")
   9.157                     | SOME ((U, (module', _)), SOME i) =>
   9.158 -                       (if_library module' module, " def" ^ string_of_int i));
   9.159 +                       (if_library mode module' module, " def" ^ string_of_int i));
   9.160                   val node_id = s ^ suffix;
   9.161                   fun p module' = mk_app brack (Pretty.block
   9.162                     (pretty_mixfix module module' ms ps1 ps3)) ps2
   9.163                 in SOME (case try (get_node gr4) node_id of
   9.164 -                   NONE => (case get_aux_code aux of
   9.165 +                   NONE => (case get_aux_code mode aux of
   9.166                         [] => (p module, gr4)
   9.167                       | xs => (p module', add_edge (node_id, dep) (new_node
   9.168                           (node_id, (NONE, module', cat_lines xs ^ "\n")) gr4)))
   9.169 @@ -654,7 +652,7 @@
   9.170             NONE => NONE
   9.171           | SOME ((U, (thyname, thm)), k) => (case prep_prim_def thy thm
   9.172              of SOME (_, (_, (args, rhs))) => let
   9.173 -               val module' = if_library thyname module;
   9.174 +               val module' = if_library mode thyname module;
   9.175                 val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i);
   9.176                 val node_id = s ^ suffix;
   9.177                 val ((ps, def_id), gr') = gr |> codegens true ts
   9.178 @@ -669,12 +667,12 @@
   9.179                         if not (null args) orelse null Ts then (args, rhs) else
   9.180                           let val v = Free (new_name rhs "x", hd Ts)
   9.181                           in ([v], betapply (rhs, v)) end;
   9.182 -                     val (p', gr1) = invoke_codegen thy defs node_id module' false
   9.183 +                     val (p', gr1) = invoke_codegen thy mode defs node_id module' false
   9.184                         rhs' (add_edge (node_id, dep)
   9.185                            (new_node (node_id, (NONE, "", "")) gr'));
   9.186                       val (xs, gr2) = codegens false args' gr1;
   9.187 -                     val (_, gr3) = invoke_tycodegen thy defs dep module false T gr2;
   9.188 -                     val (ty, gr4) = invoke_tycodegen thy defs node_id module' false U gr3;
   9.189 +                     val (_, gr3) = invoke_tycodegen thy mode defs dep module false T gr2;
   9.190 +                     val (ty, gr4) = invoke_tycodegen thy mode defs node_id module' false U gr3;
   9.191                     in (p, map_node node_id (K (NONE, module', string_of
   9.192                         (Pretty.block (separate (Pretty.brk 1)
   9.193                           (if null args' then
   9.194 @@ -692,7 +690,7 @@
   9.195          val t = strip_abs_body u
   9.196          val bs' = new_names t bs;
   9.197          val (ps, gr1) = codegens true ts gr;
   9.198 -        val (p, gr2) = invoke_codegen thy defs dep module false
   9.199 +        val (p, gr2) = invoke_codegen thy mode defs dep module false
   9.200            (subst_bounds (map Free (rev (bs' ~~ Ts)), t)) gr1;
   9.201        in
   9.202          SOME (mk_app brack (Pretty.block (str "(" :: pretty_fn bs' p @
   9.203 @@ -702,26 +700,26 @@
   9.204      | _ => NONE)
   9.205    end;
   9.206  
   9.207 -fun default_tycodegen thy defs dep module brack (TVar ((s, i), _)) gr =
   9.208 +fun default_tycodegen thy mode defs dep module brack (TVar ((s, i), _)) gr =
   9.209        SOME (str (s ^ (if i = 0 then "" else string_of_int i)), gr)
   9.210 -  | default_tycodegen thy defs dep module brack (TFree (s, _)) gr =
   9.211 +  | default_tycodegen thy mode defs dep module brack (TFree (s, _)) gr =
   9.212        SOME (str s, gr)
   9.213 -  | default_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
   9.214 +  | default_tycodegen thy mode defs dep module brack (Type (s, Ts)) gr =
   9.215        (case AList.lookup (op =) ((#types o CodegenData.get) thy) s of
   9.216           NONE => NONE
   9.217         | SOME (ms, aux) =>
   9.218             let
   9.219               val (ps, gr') = fold_map
   9.220 -               (invoke_tycodegen thy defs dep module false)
   9.221 +               (invoke_tycodegen thy mode defs dep module false)
   9.222                 (fst (args_of ms Ts)) gr;
   9.223               val (qs, gr'') = fold_map
   9.224 -               (invoke_tycodegen thy defs dep module false)
   9.225 +               (invoke_tycodegen thy mode defs dep module false)
   9.226                 (quotes_of ms) gr';
   9.227 -             val module' = if_library (thyname_of_type thy s) module;
   9.228 +             val module' = if_library mode (thyname_of_type thy s) module;
   9.229               val node_id = s ^ " (type)";
   9.230               fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs)
   9.231             in SOME (case try (get_node gr'') node_id of
   9.232 -               NONE => (case get_aux_code aux of
   9.233 +               NONE => (case get_aux_code mode aux of
   9.234                     [] => (p module', gr'')
   9.235                   | xs => (p module', snd (mk_type_id module' s
   9.236                         (add_edge (node_id, dep) (new_node (node_id,
   9.237 @@ -780,10 +778,10 @@
   9.238      else [(module, implode (map (#3 o snd) code))]
   9.239    end;
   9.240  
   9.241 -fun gen_generate_code prep_term thy modules module xs =
   9.242 +fun gen_generate_code prep_term thy mode modules module xs =
   9.243    let
   9.244      val _ = (module <> "" orelse
   9.245 -        member (op =) (!mode) "library" andalso forall (fn (s, _) => s = "") xs)
   9.246 +        member (op =) mode "library" andalso forall (fn (s, _) => s = "") xs)
   9.247        orelse error "missing module name";
   9.248      val graphs = get_modules thy;
   9.249      val defs = mk_deftab thy;
   9.250 @@ -800,7 +798,7 @@
   9.251        | expand t = (case fastype_of t of
   9.252            Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t);
   9.253      val (ps, gr') = fold_map (fn (s, t) => fn gr => apfst (pair s)
   9.254 -      (invoke_codegen thy defs "<Top>" module false t gr))
   9.255 +      (invoke_codegen thy mode defs "<Top>" module false t gr))
   9.256          (map (apsnd (expand o preprocess_term thy o prep_term thy)) xs) gr;
   9.257      val code = map_filter
   9.258        (fn ("", _) => NONE
   9.259 @@ -809,12 +807,12 @@
   9.260      val code' = space_implode "\n\n" code ^ "\n\n";
   9.261      val code'' =
   9.262        map_filter (fn (name, s) =>
   9.263 -          if member (op =) (!mode) "library" andalso name = module andalso null code
   9.264 +          if member (op =) mode "library" andalso name = module andalso null code
   9.265            then NONE
   9.266            else SOME (name, mk_struct name s))
   9.267          ((if null code then I
   9.268            else add_to_module module code')
   9.269 -           (output_code (fst gr') (if_library "" module) ["<Top>"]))
   9.270 +           (output_code (fst gr') (if_library mode "" module) ["<Top>"]))
   9.271    in
   9.272      (code'', del_nodes ["<Top>"] gr')
   9.273    end;
   9.274 @@ -873,8 +871,7 @@
   9.275  fun test_term ctxt t =
   9.276    let
   9.277      val thy = Proof_Context.theory_of ctxt;
   9.278 -    val (code, gr) = setmp_CRITICAL mode ["term_of", "test"]
   9.279 -      (generate_code_i thy [] "Generated") [("testf", t)];
   9.280 +    val (code, gr) = generate_code_i thy ["term_of", "test"] [] "Generated" [("testf", t)];
   9.281      val Ts = map snd (fst (strip_abs t));
   9.282      val args = map_index (fn (i, T) => ("arg" ^ string_of_int i, T)) Ts;
   9.283      val s = "structure TestTerm =\nstruct\n\n" ^
   9.284 @@ -913,9 +910,9 @@
   9.285            error "Term to be evaluated contains type variables";
   9.286          val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse
   9.287            error "Term to be evaluated contains variables";
   9.288 -        val (code, gr) = setmp_CRITICAL mode ["term_of"]
   9.289 -          (generate_code_i thy [] "Generated")
   9.290 -          [("result", Abs ("x", TFree ("'a", []), t))];
   9.291 +        val (code, gr) =
   9.292 +          generate_code_i thy ["term_of"] [] "Generated"
   9.293 +            [("result", Abs ("x", TFree ("'a", []), t))];
   9.294          val s = "structure EvalTerm =\nstruct\n\n" ^
   9.295            cat_lines (map snd code) ^
   9.296            "\nopen Generated;\n\n" ^ string_of
   9.297 @@ -988,7 +985,7 @@
   9.298           (const, (parse_mixfix (Syntax.read_term_global thy) mfx, aux)))) xs thy)));
   9.299  
   9.300  fun parse_code lib =
   9.301 -  Scan.optional (Parse.$$$ "(" |-- Parse.enum "," Parse.xname --| Parse.$$$ ")") (!mode) --
   9.302 +  Scan.optional (Parse.$$$ "(" |-- Parse.enum "," Parse.xname --| Parse.$$$ ")") [] --
   9.303    (if lib then Scan.optional Parse.name "" else Parse.name) --
   9.304    Scan.option (Parse.$$$ "file" |-- Parse.name) --
   9.305    (if lib then Scan.succeed []
   9.306 @@ -996,10 +993,10 @@
   9.307    Parse.$$$ "contains" --
   9.308    (   Scan.repeat1 (Parse.name --| Parse.$$$ "=" -- Parse.term)
   9.309     || Scan.repeat1 (Parse.term >> pair "")) >>
   9.310 -  (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
   9.311 +  (fn ((((mode, module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
   9.312      let
   9.313 -      val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
   9.314 -      val (code, gr) = setmp_CRITICAL mode mode'' (generate_code thy modules module) xs;
   9.315 +      val mode' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode);
   9.316 +      val (code, gr) = generate_code thy mode' modules module xs;
   9.317        val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>
   9.318          (case opt_fname of
   9.319            NONE => ML_Context.eval_text false Position.none (cat_lines (map snd code))