Implemented modular code generation.
authorberghofe
Fri Jul 01 14:18:27 2005 +0200 (2005-07-01 ago)
changeset 16649d88271eb5b26
parent 16648 fc2a425f0977
child 16650 bd4f7149ba1e
Implemented modular code generation.
src/Pure/codegen.ML
     1.1 --- a/src/Pure/codegen.ML	Fri Jul 01 14:17:32 2005 +0200
     1.2 +++ b/src/Pure/codegen.ML	Fri Jul 01 14:18:27 2005 +0200
     1.3 @@ -18,6 +18,8 @@
     1.4      | Pretty of Pretty.T
     1.5      | Quote of 'a;
     1.6  
     1.7 +  type deftab
     1.8 +  type codegr
     1.9    type 'a codegen
    1.10  
    1.11    val add_codegen: string -> term codegen -> theory -> theory
    1.12 @@ -26,35 +28,40 @@
    1.13    val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory
    1.14    val preprocess: theory -> thm list -> thm list
    1.15    val print_codegens: theory -> unit
    1.16 -  val generate_code: theory -> (string * string) list -> string
    1.17 -  val generate_code_i: theory -> (string * term) list -> string
    1.18 +  val generate_code: theory -> (string * string) list -> (string * string) list
    1.19 +  val generate_code_i: theory -> (string * term) list -> (string * string) list
    1.20    val assoc_consts: (xstring * string option * term mixfix list) list -> theory -> theory
    1.21    val assoc_consts_i: (xstring * typ option * term mixfix list) list -> theory -> theory
    1.22    val assoc_types: (xstring * typ mixfix list) list -> theory -> theory
    1.23    val get_assoc_code: theory -> string -> typ -> term mixfix list option
    1.24    val get_assoc_type: theory -> string -> typ mixfix list option
    1.25 -  val invoke_codegen: theory -> string -> bool ->
    1.26 -    (exn option * string) Graph.T * term -> (exn option * string) Graph.T * Pretty.T
    1.27 -  val invoke_tycodegen: theory -> string -> bool ->
    1.28 -    (exn option * string) Graph.T * typ -> (exn option * string) Graph.T * Pretty.T
    1.29 +  val invoke_codegen: theory -> deftab -> string -> string -> bool ->
    1.30 +    codegr * term -> codegr * Pretty.T
    1.31 +  val invoke_tycodegen: theory -> deftab -> string -> string -> bool ->
    1.32 +    codegr * typ -> codegr * Pretty.T
    1.33    val mk_id: string -> string
    1.34 -  val mk_const_id: theory -> string -> string
    1.35 -  val mk_type_id: theory -> string -> string
    1.36 +  val mk_const_id: theory -> string -> string -> string -> string
    1.37 +  val mk_type_id: theory -> string -> string -> string -> string
    1.38 +  val thyname_of_type: string -> theory -> string
    1.39 +  val thyname_of_const: string -> theory -> string
    1.40 +  val rename_terms: term list -> term list
    1.41    val rename_term: term -> term
    1.42    val new_names: term -> string list -> string list
    1.43    val new_name: term -> string -> string
    1.44 -  val get_defn: theory -> string -> typ -> ((term list * term) * int option) option
    1.45 +  val get_defn: theory -> deftab -> string -> typ ->
    1.46 +    ((typ * (string * (term list * term))) * int option) option
    1.47    val is_instance: theory -> typ -> typ -> bool
    1.48    val parens: Pretty.T -> Pretty.T
    1.49    val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T
    1.50    val eta_expand: term -> term list -> int -> term
    1.51    val strip_tname: string -> string
    1.52    val mk_type: bool -> typ -> Pretty.T
    1.53 -  val mk_term_of: theory -> bool -> typ -> Pretty.T
    1.54 -  val mk_gen: theory -> bool -> string list -> string -> typ -> Pretty.T
    1.55 +  val mk_term_of: theory -> string -> bool -> typ -> Pretty.T
    1.56 +  val mk_gen: theory -> string -> bool -> string list -> string -> typ -> Pretty.T
    1.57    val test_fn: (int -> (string * term) list option) ref
    1.58    val test_term: theory -> int -> int -> term -> (string * term) list option
    1.59    val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
    1.60 +  val mk_deftab: theory -> deftab
    1.61  end;
    1.62  
    1.63  structure Codegen : CODEGEN =
    1.64 @@ -93,10 +100,34 @@
    1.65  
    1.66  (**** theory data ****)
    1.67  
    1.68 +(* preprocessed definition table *)
    1.69 +
    1.70 +type deftab =
    1.71 +  (typ *              (* type of constant *)
    1.72 +    (string *         (* name of theory containing definition of constant *)
    1.73 +      (term list *    (* parameters *)
    1.74 +       term)))        (* right-hand side *)
    1.75 +  list Symtab.table;
    1.76 +
    1.77 +(* code dependency graph *)
    1.78 +
    1.79 +type codegr =
    1.80 +  (exn option *    (* slot for arbitrary data *)
    1.81 +   string *        (* name of structure containing piece of code *)
    1.82 +   string)         (* piece of code *)
    1.83 +  Graph.T;
    1.84 +
    1.85  (* type of code generators *)
    1.86  
    1.87 -type 'a codegen = theory -> (exn option * string) Graph.T ->
    1.88 -  string -> bool -> 'a -> ((exn option * string) Graph.T * Pretty.T) option;
    1.89 +type 'a codegen =
    1.90 +  theory ->    (* theory in which generate_code was called *)
    1.91 +  deftab ->    (* definition table (for efficiency) *)
    1.92 +  codegr ->    (* code dependency graph *)
    1.93 +  string ->    (* node name of caller (for recording dependencies) *)
    1.94 +  string ->    (* theory name of caller (for modular code generation) *)
    1.95 +  bool ->      (* whether to parenthesize generated expression *)
    1.96 +  'a ->        (* item to generate code from *)
    1.97 +  (codegr * Pretty.T) option;
    1.98  
    1.99  (* parameters for random testing *)
   1.100  
   1.101 @@ -298,7 +329,7 @@
   1.102    let
   1.103      val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
   1.104        CodegenData.get thy;
   1.105 -    val tc = Sign.intern_type (sign_of thy) s
   1.106 +    val tc = Sign.intern_type thy s
   1.107    in
   1.108      (case assoc (types, tc) of
   1.109         NONE => CodegenData.put {codegens = codegens,
   1.110 @@ -339,13 +370,58 @@
   1.111      if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s'
   1.112    end;
   1.113  
   1.114 -fun mk_const_id thy s =
   1.115 -  let val s' = mk_id (Sign.extern_const thy s)
   1.116 -  in if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' end;
   1.117 +fun extrn thy f thyname s =
   1.118 +  let
   1.119 +    val xs = NameSpace.unpack s;
   1.120 +    val s' = setmp NameSpace.long_names false (setmp NameSpace.short_names false
   1.121 +      (setmp NameSpace.unique_names true (f thy))) s;
   1.122 +    val xs' = NameSpace.unpack s'
   1.123 +  in
   1.124 +    if "modular" mem !mode andalso length xs = length xs' andalso hd xs' = thyname
   1.125 +    then NameSpace.pack (tl xs') else s'
   1.126 +  end;
   1.127 +
   1.128 +(* thyname:  theory name for caller                                        *)
   1.129 +(* thyname': theory name for callee                                        *)
   1.130 +(* if caller and callee reside in different theories, use qualified access *)
   1.131 +
   1.132 +fun mk_const_id thy thyname thyname' s =
   1.133 +  let
   1.134 +    val s' = mk_id (extrn thy Sign.extern_const thyname' s);
   1.135 +    val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s'
   1.136 +  in
   1.137 +    if "modular" mem !mode andalso thyname <> thyname' andalso thyname' <> ""
   1.138 +    then thyname' ^ "." ^ s'' else s''
   1.139 +  end;
   1.140  
   1.141 -fun mk_type_id thy s =
   1.142 -  let val s' = mk_id (Sign.extern_type thy s)
   1.143 -  in if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' end;
   1.144 +fun mk_type_id' f thy thyname thyname' s =
   1.145 +  let
   1.146 +    val s' = mk_id (extrn thy Sign.extern_type thyname' s);
   1.147 +    val s'' = f (if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s')
   1.148 +  in
   1.149 +    if "modular" mem !mode andalso thyname <> thyname' andalso thyname' <> ""
   1.150 +    then thyname' ^ "." ^ s'' else s''
   1.151 +  end;
   1.152 +
   1.153 +val mk_type_id = mk_type_id' I;
   1.154 +
   1.155 +fun theory_of_type s thy = 
   1.156 +  if Sign.declared_tyname thy s
   1.157 +  then SOME (if_none (get_first (theory_of_type s) (Theory.parents_of thy)) thy)
   1.158 +  else NONE;
   1.159 +
   1.160 +fun theory_of_const s thy = 
   1.161 +  if Sign.declared_const thy s
   1.162 +  then SOME (if_none (get_first (theory_of_const s) (Theory.parents_of thy)) thy)
   1.163 +  else NONE;
   1.164 +
   1.165 +fun thyname_of_type s thy = (case theory_of_type s thy of
   1.166 +    NONE => error ("thyname_of_type: no such type: " ^ quote s)
   1.167 +  | SOME thy' => Context.theory_name thy');
   1.168 +
   1.169 +fun thyname_of_const s thy = (case theory_of_const s thy of
   1.170 +    NONE => error ("thyname_of_const: no such constant: " ^ quote s)
   1.171 +  | SOME thy' => Context.theory_name thy');
   1.172  
   1.173  fun rename_terms ts =
   1.174    let
   1.175 @@ -374,53 +450,60 @@
   1.176  (**** retrieve definition of constant ****)
   1.177  
   1.178  fun is_instance thy T1 T2 =
   1.179 -  Sign.typ_instance (sign_of thy) (T1, Type.varifyT T2);
   1.180 +  Sign.typ_instance thy (T1, Type.varifyT T2);
   1.181  
   1.182  fun get_assoc_code thy s T = Option.map snd (find_first (fn ((s', T'), _) =>
   1.183    s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));
   1.184  
   1.185 -fun get_defn thy s T =
   1.186 +fun mk_deftab thy =
   1.187    let
   1.188 -    val axms = Theory.all_axioms_of thy;
   1.189 +    val axmss = map (fn thy' =>
   1.190 +      (Context.theory_name thy', snd (#axioms (Theory.rep_theory thy'))))
   1.191 +      (thy :: Theory.ancestors_of thy);
   1.192      fun prep_def def = (case preprocess thy [def] of
   1.193 -      [def'] => prop_of def' | _ => error "get_defn: bad preprocessor");
   1.194 +      [def'] => prop_of def' | _ => error "mk_deftab: bad preprocessor");
   1.195      fun dest t =
   1.196        let
   1.197          val (lhs, rhs) = Logic.dest_equals t;
   1.198          val (c, args) = strip_comb lhs;
   1.199 -        val (s', T') = dest_Const c
   1.200 -      in if s = s' then SOME (T', (args, rhs)) else NONE
   1.201 +        val (s, T) = dest_Const c
   1.202 +      in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE
   1.203        end handle TERM _ => NONE;
   1.204 -    val defs = List.mapPartial (fn (name, t) => Option.map (pair name) (dest t)) axms;
   1.205 -    val i = find_index (is_instance thy T o fst o snd) defs
   1.206 +    fun add_def thyname (defs, (name, t)) = (case dest t of
   1.207 +        NONE => defs
   1.208 +      | SOME _ => (case dest (prep_def (Thm.get_axiom thy name)) of
   1.209 +          NONE => defs
   1.210 +        | SOME (s, (T, (args, rhs))) => Symtab.update
   1.211 +            ((s, (T, (thyname, split_last (rename_terms (args @ [rhs])))) ::
   1.212 +            if_none (Symtab.lookup (defs, s)) []), defs)))
   1.213    in
   1.214 -    if i >= 0 then
   1.215 -      let val (name, (T', (args, _))) = List.nth (defs, i)
   1.216 -      in case dest (prep_def (Thm.get_axiom thy name)) of
   1.217 -          NONE => NONE
   1.218 -        | SOME (T'', p as (args', rhs)) =>
   1.219 -            if T' = T'' andalso args = args' then
   1.220 -              SOME (split_last (rename_terms (args @ [rhs])),
   1.221 -                if length defs = 1 then NONE else SOME i)
   1.222 -            else NONE
   1.223 -      end
   1.224 -    else NONE
   1.225 +    foldl (fn ((thyname, axms), defs) =>
   1.226 +      Symtab.foldl (add_def thyname) (defs, axms)) Symtab.empty axmss
   1.227    end;
   1.228  
   1.229 +fun get_defn thy defs s T = (case Symtab.lookup (defs, s) of
   1.230 +    NONE => NONE
   1.231 +  | SOME ds =>
   1.232 +      let val i = find_index (is_instance thy T o fst) ds
   1.233 +      in if i >= 0 then
   1.234 +          SOME (List.nth (ds, i), if length ds = 1 then NONE else SOME i)
   1.235 +        else NONE
   1.236 +      end);
   1.237 +
   1.238  
   1.239  (**** invoke suitable code generator for term / type ****)
   1.240  
   1.241 -fun invoke_codegen thy dep brack (gr, t) = (case get_first
   1.242 -   (fn (_, f) => f thy gr dep brack t) (#codegens (CodegenData.get thy)) of
   1.243 +fun invoke_codegen thy defs dep thyname brack (gr, t) = (case get_first
   1.244 +   (fn (_, f) => f thy defs gr dep thyname brack t) (#codegens (CodegenData.get thy)) of
   1.245        NONE => error ("Unable to generate code for term:\n" ^
   1.246 -        Sign.string_of_term (sign_of thy) t ^ "\nrequired by:\n" ^
   1.247 +        Sign.string_of_term thy t ^ "\nrequired by:\n" ^
   1.248          commas (Graph.all_succs gr [dep]))
   1.249      | SOME x => x);
   1.250  
   1.251 -fun invoke_tycodegen thy dep brack (gr, T) = (case get_first
   1.252 -   (fn (_, f) => f thy gr dep brack T) (#tycodegens (CodegenData.get thy)) of
   1.253 +fun invoke_tycodegen thy defs dep thyname brack (gr, T) = (case get_first
   1.254 +   (fn (_, f) => f thy defs gr dep thyname brack T) (#tycodegens (CodegenData.get thy)) of
   1.255        NONE => error ("Unable to generate code for type:\n" ^
   1.256 -        Sign.string_of_typ (sign_of thy) T ^ "\nrequired by:\n" ^
   1.257 +        Sign.string_of_typ thy T ^ "\nrequired by:\n" ^
   1.258          commas (Graph.all_succs gr [dep]))
   1.259      | SOME x => x);
   1.260  
   1.261 @@ -463,15 +546,15 @@
   1.262  
   1.263  fun new_name t x = hd (new_names t [x]);
   1.264  
   1.265 -fun default_codegen thy gr dep brack t =
   1.266 +fun default_codegen thy defs gr dep thyname brack t =
   1.267    let
   1.268      val (u, ts) = strip_comb t;
   1.269 -    fun codegens brack = foldl_map (invoke_codegen thy dep brack)
   1.270 +    fun codegens brack = foldl_map (invoke_codegen thy defs dep thyname brack)
   1.271    in (case u of
   1.272        Var ((s, i), T) =>
   1.273          let
   1.274            val (gr', ps) = codegens true (gr, ts);
   1.275 -          val (gr'', _) = invoke_tycodegen thy dep false (gr', T)
   1.276 +          val (gr'', _) = invoke_tycodegen thy defs dep thyname false (gr', T)
   1.277          in SOME (gr'', mk_app brack (Pretty.str (s ^
   1.278             (if i=0 then "" else string_of_int i))) ps)
   1.279          end
   1.280 @@ -479,7 +562,7 @@
   1.281      | Free (s, T) =>
   1.282          let
   1.283            val (gr', ps) = codegens true (gr, ts);
   1.284 -          val (gr'', _) = invoke_tycodegen thy dep false (gr', T)
   1.285 +          val (gr'', _) = invoke_tycodegen thy defs dep thyname false (gr', T)
   1.286          in SOME (gr'', mk_app brack (Pretty.str s) ps) end
   1.287  
   1.288      | Const (s, T) =>
   1.289 @@ -487,7 +570,7 @@
   1.290           SOME ms =>
   1.291             let val i = num_args ms
   1.292             in if length ts < i then
   1.293 -               default_codegen thy gr dep brack (eta_expand u ts i)
   1.294 +               default_codegen thy defs gr dep thyname brack (eta_expand u ts i)
   1.295               else
   1.296                 let
   1.297                   val (ts1, ts2) = args_of ms ts;
   1.298 @@ -498,15 +581,17 @@
   1.299                   SOME (gr3, mk_app brack (Pretty.block (pretty_mixfix ms ps1 ps3)) ps2)
   1.300                 end
   1.301             end
   1.302 -       | NONE => (case get_defn thy s T of
   1.303 +       | NONE => (case get_defn thy defs s T of
   1.304             NONE => NONE
   1.305 -         | SOME ((args, rhs), k) =>
   1.306 +         | SOME ((U, (thyname', (args, rhs))), k) =>
   1.307               let
   1.308 -               val id = mk_const_id (sign_of thy) s ^ (case k of
   1.309 -                 NONE => "" | SOME i => "_def" ^ string_of_int i);
   1.310 +               val suffix = (case k of NONE => "" | SOME i => "_def" ^ string_of_int i);
   1.311 +               val node_id = s ^ suffix;
   1.312 +               val def_id = mk_const_id thy thyname' thyname' s ^ suffix;
   1.313 +               val call_id = mk_const_id thy thyname thyname' s ^ suffix;
   1.314                 val (gr', ps) = codegens true (gr, ts);
   1.315               in
   1.316 -               SOME (Graph.add_edge (id, dep) gr' handle Graph.UNDEF _ =>
   1.317 +               SOME (Graph.add_edge (node_id, dep) gr' handle Graph.UNDEF _ =>
   1.318                   let
   1.319                     val _ = message ("expanding definition of " ^ s);
   1.320                     val (Ts, _) = strip_type T;
   1.321 @@ -514,17 +599,19 @@
   1.322                       if not (null args) orelse null Ts then (args, rhs) else
   1.323                         let val v = Free (new_name rhs "x", hd Ts)
   1.324                         in ([v], betapply (rhs, v)) end;
   1.325 -                   val (gr1, p) = invoke_codegen thy id false
   1.326 -                     (Graph.add_edge (id, dep)
   1.327 -                        (Graph.new_node (id, (NONE, "")) gr'), rhs');
   1.328 +                   val (gr1, p) = invoke_codegen thy defs node_id thyname' false
   1.329 +                     (Graph.add_edge (node_id, dep)
   1.330 +                        (Graph.new_node (node_id, (NONE, "", "")) gr'), rhs');
   1.331                     val (gr2, xs) = codegens false (gr1, args');
   1.332 -                   val (gr3, ty) = invoke_tycodegen thy id false (gr2, T);
   1.333 -                 in Graph.map_node id (K (NONE, Pretty.string_of (Pretty.block
   1.334 -                   (separate (Pretty.brk 1) (if null args' then
   1.335 -                       [Pretty.str ("val " ^ id ^ " :"), ty]
   1.336 -                     else Pretty.str ("fun " ^ id) :: xs) @
   1.337 -                    [Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n")) gr3
   1.338 -                 end, mk_app brack (Pretty.str id) ps)
   1.339 +                   val (gr3, _) = invoke_tycodegen thy defs dep thyname false (gr2, T);
   1.340 +                   val (gr4, ty) = invoke_tycodegen thy defs node_id thyname' false (gr3, U);
   1.341 +                 in Graph.map_node node_id (K (NONE, thyname', Pretty.string_of
   1.342 +                   (Pretty.block (separate (Pretty.brk 1)
   1.343 +                     (if null args' then
   1.344 +                        [Pretty.str ("val " ^ def_id ^ " :"), ty]
   1.345 +                      else Pretty.str ("fun " ^ def_id) :: xs) @
   1.346 +                    [Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n")) gr4
   1.347 +                 end, mk_app brack (Pretty.str call_id) ps)
   1.348               end))
   1.349  
   1.350      | Abs _ =>
   1.351 @@ -533,7 +620,7 @@
   1.352          val t = strip_abs_body u
   1.353          val bs' = new_names t bs;
   1.354          val (gr1, ps) = codegens true (gr, ts);
   1.355 -        val (gr2, p) = invoke_codegen thy dep false
   1.356 +        val (gr2, p) = invoke_codegen thy defs dep thyname false
   1.357            (gr1, subst_bounds (map Free (rev (bs' ~~ Ts)), t));
   1.358        in
   1.359          SOME (gr2, mk_app brack (Pretty.block (Pretty.str "(" :: pretty_fn bs' p @
   1.360 @@ -543,18 +630,21 @@
   1.361      | _ => NONE)
   1.362    end;
   1.363  
   1.364 -fun default_tycodegen thy gr dep brack (TVar ((s, i), _)) =
   1.365 +fun default_tycodegen thy defs gr dep thyname brack (TVar ((s, i), _)) =
   1.366        SOME (gr, Pretty.str (s ^ (if i = 0 then "" else string_of_int i)))
   1.367 -  | default_tycodegen thy gr dep brack (TFree (s, _)) = SOME (gr, Pretty.str s)
   1.368 -  | default_tycodegen thy gr dep brack (Type (s, Ts)) =
   1.369 +  | default_tycodegen thy defs gr dep thyname brack (TFree (s, _)) =
   1.370 +      SOME (gr, Pretty.str s)
   1.371 +  | default_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) =
   1.372        (case assoc (#types (CodegenData.get thy), s) of
   1.373           NONE => NONE
   1.374         | SOME ms =>
   1.375             let
   1.376               val (gr', ps) = foldl_map
   1.377 -               (invoke_tycodegen thy dep false) (gr, fst (args_of ms Ts));
   1.378 +               (invoke_tycodegen thy defs dep thyname false)
   1.379 +               (gr, fst (args_of ms Ts));
   1.380               val (gr'', qs) = foldl_map
   1.381 -               (invoke_tycodegen thy dep false) (gr', quotes_of ms)
   1.382 +               (invoke_tycodegen thy defs dep thyname false)
   1.383 +               (gr', quotes_of ms)
   1.384             in SOME (gr'', Pretty.block (pretty_mixfix ms ps qs)) end);
   1.385  
   1.386  val _ = Context.add_setup
   1.387 @@ -562,23 +652,62 @@
   1.388    add_tycodegen "default" default_tycodegen];
   1.389  
   1.390  
   1.391 -fun output_code gr xs = implode (map (snd o Graph.get_node gr)
   1.392 -  (rev (Graph.all_preds gr xs)));
   1.393 +fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
   1.394 +
   1.395 +fun add_to_module name s ms =
   1.396 +  overwrite (ms, (name, the (assoc (ms, name)) ^ s));
   1.397 +
   1.398 +fun output_code gr xs =
   1.399 +  let
   1.400 +    val code =
   1.401 +      map (fn s => (s, Graph.get_node gr s)) (rev (Graph.all_preds gr xs))
   1.402 +    fun string_of_cycle (a :: b :: cs) =
   1.403 +          let val SOME (x, y) = get_first (fn (x, (_, a', _)) =>
   1.404 +            if a = a' then Option.map (pair x)
   1.405 +              (find_first (equal b o #2 o Graph.get_node gr)
   1.406 +                (Graph.imm_succs gr x))
   1.407 +            else NONE) code
   1.408 +          in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end
   1.409 +      | string_of_cycle _ = ""
   1.410 +  in
   1.411 +    if "modular" mem !mode then
   1.412 +      let
   1.413 +        val modules = distinct (map (#2 o snd) code);
   1.414 +        val mod_gr = foldr (uncurry Graph.add_edge_acyclic)
   1.415 +          (foldr (uncurry (Graph.new_node o rpair ())) Graph.empty modules)
   1.416 +          (List.concat (map (fn (s, (_, thyname, _)) => map (pair thyname)
   1.417 +            (filter_out (equal thyname) (map (#2 o Graph.get_node gr)
   1.418 +              (Graph.imm_succs gr s)))) code));
   1.419 +        val modules' =
   1.420 +          rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs))
   1.421 +      in
   1.422 +        foldl (fn ((_, (_, thyname, s)), ms) => add_to_module thyname s ms)
   1.423 +          (map (rpair "") modules') code
   1.424 +      end handle Graph.CYCLES (cs :: _) =>
   1.425 +        error ("Cyclic dependency of modules:\n" ^ commas cs ^
   1.426 +          "\n" ^ string_of_cycle cs)
   1.427 +    else [("Generated", implode (map (#3 o snd) code))]
   1.428 +  end;
   1.429  
   1.430  fun gen_generate_code prep_term thy =
   1.431    setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs =>
   1.432    let
   1.433 -    val gr = Graph.new_node ("<Top>", (NONE, "")) Graph.empty;
   1.434 +    val defs = mk_deftab thy;
   1.435 +    val gr = Graph.new_node ("<Top>", (NONE, "Generated", "")) Graph.empty;
   1.436 +    fun expand (t as Abs _) = t
   1.437 +      | expand t = (case fastype_of t of
   1.438 +          Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t);
   1.439      val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s)
   1.440 -      (invoke_codegen thy "<Top>" false (gr, t)))
   1.441 -        (gr, map (apsnd (prep_term thy)) xs)
   1.442 +      (invoke_codegen thy defs "<Top>" "Generated" false (gr, t)))
   1.443 +        (gr, map (apsnd (expand o prep_term thy)) xs);
   1.444      val code =
   1.445 -      "structure Generated =\nstruct\n\n" ^
   1.446 -      output_code gr' ["<Top>"] ^
   1.447        space_implode "\n\n" (map (fn (s', p) => Pretty.string_of (Pretty.block
   1.448          [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"])) ps) ^
   1.449 -      "\n\nend;\n\nopen Generated;\n";
   1.450 -  in code end));
   1.451 +      "\n\n"
   1.452 +  in
   1.453 +    map (fn (name, s) => (name, mk_struct name s))
   1.454 +      (add_to_module "Generated" code (output_code gr' ["<Top>"]))
   1.455 +  end));
   1.456  
   1.457  val generate_code_i = gen_generate_code (K I);
   1.458  val generate_code = gen_generate_code
   1.459 @@ -600,23 +729,29 @@
   1.460        [Pretty.str "Type", Pretty.brk 1, Pretty.str ("(\"" ^ s ^ "\","),
   1.461         Pretty.brk 1, pretty_list (map (mk_type false) Ts), Pretty.str ")"]);
   1.462  
   1.463 -fun mk_term_of _ p (TVar ((s, i), _)) = Pretty.str
   1.464 +fun mk_term_of thy thyname p (TVar ((s, i), _)) = Pretty.str
   1.465        (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F")
   1.466 -  | mk_term_of _ p (TFree (s, _)) = Pretty.str (strip_tname s ^ "F")
   1.467 -  | mk_term_of thy p (Type (s, Ts)) = (if p then parens else I) (Pretty.block
   1.468 -      (separate (Pretty.brk 1) (Pretty.str ("term_of_" ^ mk_type_id thy s) ::
   1.469 -        List.concat (map (fn T => [mk_term_of thy true T, mk_type true T]) Ts))));
   1.470 +  | mk_term_of thy thyname p (TFree (s, _)) = Pretty.str (strip_tname s ^ "F")
   1.471 +  | mk_term_of thy thyname p (Type (s, Ts)) = (if p then parens else I)
   1.472 +      (Pretty.block (separate (Pretty.brk 1)
   1.473 +        (Pretty.str (mk_type_id' (fn s' => "term_of_" ^ s')
   1.474 +          thy thyname (thyname_of_type s thy) s) ::
   1.475 +        List.concat (map (fn T =>
   1.476 +          [mk_term_of thy thyname true T, mk_type true T]) Ts))));
   1.477  
   1.478  
   1.479  (**** Test data generators ****)
   1.480  
   1.481 -fun mk_gen _ p xs a (TVar ((s, i), _)) = Pretty.str
   1.482 +fun mk_gen thy thyname p xs a (TVar ((s, i), _)) = Pretty.str
   1.483        (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G")
   1.484 -  | mk_gen _ p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G")
   1.485 -  | mk_gen thy p xs a (Type (s, Ts)) = (if p then parens else I) (Pretty.block
   1.486 -      (separate (Pretty.brk 1) (Pretty.str ("gen_" ^ mk_type_id thy s ^
   1.487 -        (if s mem xs then "'" else "")) :: map (mk_gen thy true xs a) Ts @
   1.488 -        (if s mem xs then [Pretty.str a] else []))));
   1.489 +  | mk_gen thy thyname p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G")
   1.490 +  | mk_gen thy thyname p xs a (Type (s, Ts)) = (if p then parens else I)
   1.491 +      (Pretty.block (separate (Pretty.brk 1)
   1.492 +        (Pretty.str (mk_type_id' (fn s' => "gen_" ^ s')
   1.493 +          thy thyname (thyname_of_type s thy) s ^
   1.494 +          (if s mem xs then "'" else "")) ::
   1.495 +         map (mk_gen thy thyname true xs a) Ts @
   1.496 +         (if s mem xs then [Pretty.str a] else []))));
   1.497  
   1.498  val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE);
   1.499  
   1.500 @@ -628,16 +763,17 @@
   1.501        "Term to be tested contains schematic variables";
   1.502      val frees = map dest_Free (term_frees t);
   1.503      val szname = variant (map fst frees) "i";
   1.504 -    val s = "structure TestTerm =\nstruct\n\n" ^
   1.505 -      setmp mode ["term_of", "test"] (generate_code_i thy)
   1.506 -        [("testf", list_abs_free (frees, t))] ^
   1.507 -      "\n" ^ Pretty.string_of
   1.508 +    val code = space_implode "\n" (map snd
   1.509 +      (setmp mode ["term_of", "test"] (generate_code_i thy)
   1.510 +        [("testf", list_abs_free (frees, t))]));
   1.511 +    val s = "structure TestTerm =\nstruct\n\n" ^ code ^
   1.512 +      "\nopen Generated;\n\n" ^ Pretty.string_of
   1.513          (Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
   1.514            Pretty.brk 1, Pretty.str ("(fn " ^ szname ^ " =>"), Pretty.brk 1,
   1.515            Pretty.blk (0, [Pretty.str "let", Pretty.brk 1,
   1.516              Pretty.blk (0, separate Pretty.fbrk (map (fn (s, T) =>
   1.517                Pretty.block [Pretty.str ("val " ^ mk_id s ^ " ="), Pretty.brk 1,
   1.518 -              mk_gen thy false [] "" T, Pretty.brk 1,
   1.519 +              mk_gen thy "" false [] "" T, Pretty.brk 1,
   1.520                Pretty.str (szname ^ ";")]) frees)),
   1.521              Pretty.brk 1, Pretty.str "in", Pretty.brk 1,
   1.522              Pretty.block [Pretty.str "if ",
   1.523 @@ -648,7 +784,7 @@
   1.524                  List.concat (separate [Pretty.str ",", Pretty.brk 1]
   1.525                    (map (fn (s, T) => [Pretty.block
   1.526                      [Pretty.str ("(" ^ Library.quote (Symbol.escape s) ^ ","), Pretty.brk 1,
   1.527 -                     mk_app false (mk_term_of thy false T)
   1.528 +                     mk_app false (mk_term_of thy "" false T)
   1.529                         [Pretty.str (mk_id s)], Pretty.str ")"]]) frees)) @
   1.530                    [Pretty.str "]"])]],
   1.531              Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
   1.532 @@ -716,7 +852,7 @@
   1.533      (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")") >>
   1.534       (fn xs => Toplevel.theory (fn thy => assoc_types
   1.535         (map (fn (name, mfx) => (name, parse_mixfix
   1.536 -         (typ_of o read_ctyp (sign_of thy)) mfx)) xs) thy)));
   1.537 +         (typ_of o read_ctyp thy) mfx)) xs) thy)));
   1.538  
   1.539  val assoc_constP =
   1.540    OuterSyntax.command "consts_code"
   1.541 @@ -726,7 +862,7 @@
   1.542          P.$$$ "(" -- P.string --| P.$$$ ")") >>
   1.543       (fn xs => Toplevel.theory (fn thy => assoc_consts
   1.544         (map (fn ((name, optype), mfx) => (name, optype, parse_mixfix
   1.545 -         (term_of o read_cterm (sign_of thy) o rpair TypeInfer.logicT) mfx))
   1.546 +         (term_of o read_cterm thy o rpair TypeInfer.logicT) mfx))
   1.547             xs) thy)));
   1.548  
   1.549  val generate_codeP =
   1.550 @@ -735,10 +871,18 @@
   1.551       Scan.optional (P.$$$ "[" |-- P.enum "," P.xname --| P.$$$ "]") (!mode) --
   1.552       Scan.repeat1 (P.name --| P.$$$ "=" -- P.term) >>
   1.553       (fn ((opt_fname, mode'), xs) => Toplevel.theory (fn thy =>
   1.554 -        ((case opt_fname of
   1.555 -            NONE => use_text Context.ml_output false
   1.556 -          | SOME fname => File.write (Path.unpack fname))
   1.557 -              (setmp mode mode' (generate_code thy) xs); thy))));
   1.558 +       let val code = setmp mode mode' (generate_code thy) xs
   1.559 +       in ((case opt_fname of
   1.560 +           NONE => use_text Context.ml_output false
   1.561 +             (space_implode "\n" (map snd code) ^ "\nopen Generated;\n")
   1.562 +         | SOME fname =>
   1.563 +             if "modular" mem mode' then
   1.564 +               app (fn (name, s) => File.write
   1.565 +                   (Path.append (Path.unpack fname) (Path.basic (name ^ ".ML"))) s)
   1.566 +                 (("ROOT", implode (map (fn (name, _) =>
   1.567 +                     "use \"" ^ name ^ ".ML\";\n") code)) :: code)
   1.568 +             else File.write (Path.unpack fname) (snd (hd code))); thy)
   1.569 +       end)));
   1.570  
   1.571  val params =
   1.572    [("size", P.nat >> (K o set_size)),
   1.573 @@ -759,7 +903,7 @@
   1.574    OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
   1.575      (P.$$$ "[" |-- P.list1 parse_test_params --| P.$$$ "]" >>
   1.576        (fn fs => Toplevel.theory (fn thy =>
   1.577 -         map_test_params (app (map (fn f => f (sign_of thy)) fs)) thy)));
   1.578 +         map_test_params (app (map (fn f => f thy) fs)) thy)));
   1.579  
   1.580  val testP =
   1.581    OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag