Implemented incremental code generation.
authorberghofe
Thu Aug 25 16:10:16 2005 +0200 (2005-08-25)
changeset 171446642e0f96f44
parent 17143 2a8111863b16
child 17145 e623e57b0f44
Implemented incremental code generation.
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/typedef_package.ML
src/Pure/codegen.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu Aug 25 09:29:05 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Aug 25 16:10:16 2005 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4          (max (map (arg_nonempty o DatatypeAux.strip_dtyp) dts))) constrs)
     1.5    in case xs of [] => NONE | x :: _ => SOME x end;
     1.6  
     1.7 -fun add_dt_defs thy defs dep gr (descr: DatatypeAux.descr) =
     1.8 +fun add_dt_defs thy defs dep module gr (descr: DatatypeAux.descr) =
     1.9    let
    1.10      val sg = sign_of thy;
    1.11      val tab = DatatypePackage.get_datatypes thy;
    1.12 @@ -48,8 +48,9 @@
    1.13      val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) =>
    1.14        exists (exists DatatypeAux.is_rec_type o snd) cs) descr');
    1.15  
    1.16 -    val (_, (tname, _, (dname, _) :: _)) :: _ = descr';
    1.17 -    val thyname = thyname_of_type tname thy;
    1.18 +    val (_, (tname, _, _)) :: _ = descr';
    1.19 +    val node_id = tname ^ " (type)";
    1.20 +    val module' = if_library (thyname_of_type tname thy) module;
    1.21  
    1.22      fun mk_dtdef gr prfx [] = (gr, [])
    1.23        | mk_dtdef gr prfx ((_, (tname, dts, cs))::xs) =
    1.24 @@ -57,54 +58,57 @@
    1.25              val tvs = map DatatypeAux.dest_DtTFree dts;
    1.26              val sorts = map (rpair []) tvs;
    1.27              val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs;
    1.28 -            val (gr', ps) = foldl_map (fn (gr, (cname, cargs)) =>
    1.29 -              apsnd (pair cname) (foldl_map
    1.30 -                (invoke_tycodegen thy defs dname thyname false) (gr, cargs))) (gr, cs');
    1.31 -            val (gr'', rest) = mk_dtdef gr' "and " xs
    1.32 +            val (gr', (_, type_id)) = mk_type_id module' tname gr;
    1.33 +            val (gr'', ps) =
    1.34 +              foldl_map (fn (gr, (cname, cargs)) =>
    1.35 +                foldl_map (invoke_tycodegen thy defs node_id module' false)
    1.36 +                  (gr, cargs) |>>>
    1.37 +                mk_const_id module' cname) (gr', cs');
    1.38 +            val (gr''', rest) = mk_dtdef gr'' "and " xs
    1.39            in
    1.40 -            (gr'',
    1.41 +            (gr''',
    1.42               Pretty.block (Pretty.str prfx ::
    1.43                 (if null tvs then [] else
    1.44                    [mk_tuple (map Pretty.str tvs), Pretty.str " "]) @
    1.45 -               [Pretty.str (mk_type_id sg thyname thyname tname ^ " ="), Pretty.brk 1] @
    1.46 +               [Pretty.str (type_id ^ " ="), Pretty.brk 1] @
    1.47                 List.concat (separate [Pretty.brk 1, Pretty.str "| "]
    1.48 -                 (map (fn (cname, ps') => [Pretty.block
    1.49 -                   (Pretty.str (mk_const_id sg thyname thyname cname) ::
    1.50 +                 (map (fn (ps', (_, cname)) => [Pretty.block
    1.51 +                   (Pretty.str cname ::
    1.52                      (if null ps' then [] else
    1.53                       List.concat ([Pretty.str " of", Pretty.brk 1] ::
    1.54                         separate [Pretty.str " *", Pretty.brk 1]
    1.55                           (map single ps'))))]) ps))) :: rest)
    1.56            end;
    1.57  
    1.58 -    fun mk_term_of_def prfx [] = []
    1.59 -      | mk_term_of_def prfx ((_, (tname, dts, cs)) :: xs) =
    1.60 +    fun mk_term_of_def gr prfx [] = []
    1.61 +      | mk_term_of_def gr prfx ((_, (tname, dts, cs)) :: xs) =
    1.62            let
    1.63              val tvs = map DatatypeAux.dest_DtTFree dts;
    1.64              val sorts = map (rpair []) tvs;
    1.65              val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs;
    1.66              val dts' = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
    1.67              val T = Type (tname, dts');
    1.68 -            val rest = mk_term_of_def "and " xs;
    1.69 +            val rest = mk_term_of_def gr "and " xs;
    1.70              val (_, eqs) = foldl_map (fn (prfx, (cname, Ts)) =>
    1.71                let val args = map (fn i =>
    1.72                  Pretty.str ("x" ^ string_of_int i)) (1 upto length Ts)
    1.73                in ("  | ", Pretty.blk (4,
    1.74 -                [Pretty.str prfx, mk_term_of thy thyname false T, Pretty.brk 1,
    1.75 -                 if null Ts then Pretty.str (mk_const_id sg thyname thyname cname)
    1.76 +                [Pretty.str prfx, mk_term_of gr module' false T, Pretty.brk 1,
    1.77 +                 if null Ts then Pretty.str (snd (get_const_id cname gr))
    1.78                   else parens (Pretty.block
    1.79 -                   [Pretty.str (mk_const_id sg thyname thyname cname),
    1.80 +                   [Pretty.str (snd (get_const_id cname gr)),
    1.81                      Pretty.brk 1, mk_tuple args]),
    1.82                   Pretty.str " =", Pretty.brk 1] @
    1.83                   List.concat (separate [Pretty.str " $", Pretty.brk 1]
    1.84                     ([Pretty.str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1,
    1.85                       mk_type false (Ts ---> T), Pretty.str ")"] ::
    1.86 -                    map (fn (x, U) => [Pretty.block [mk_term_of thy thyname false U,
    1.87 +                    map (fn (x, U) => [Pretty.block [mk_term_of gr module' false U,
    1.88                        Pretty.brk 1, x]]) (args ~~ Ts)))))
    1.89                end) (prfx, cs')
    1.90            in eqs @ rest end;
    1.91  
    1.92 -    fun mk_gen_of_def prfx [] = []
    1.93 -      | mk_gen_of_def prfx ((i, (tname, dts, cs)) :: xs) =
    1.94 +    fun mk_gen_of_def gr prfx [] = []
    1.95 +      | mk_gen_of_def gr prfx ((i, (tname, dts, cs)) :: xs) =
    1.96            let
    1.97              val tvs = map DatatypeAux.dest_DtTFree dts;
    1.98              val sorts = map (rpair []) tvs;
    1.99 @@ -117,11 +121,11 @@
   1.100  
   1.101              fun mk_constr s b (cname, dts) =
   1.102                let
   1.103 -                val gs = map (fn dt => mk_app false (mk_gen thy thyname false rtnames s
   1.104 +                val gs = map (fn dt => mk_app false (mk_gen gr module' false rtnames s
   1.105                      (DatatypeAux.typ_of_dtyp descr sorts dt))
   1.106                    [Pretty.str (if b andalso DatatypeAux.is_rec_type dt then "0"
   1.107                       else "j")]) dts;
   1.108 -                val id = mk_const_id sg thyname thyname cname
   1.109 +                val (_, id) = get_const_id cname gr
   1.110                in case gs of
   1.111                    _ :: _ :: _ => Pretty.block
   1.112                      [Pretty.str id, Pretty.brk 1, mk_tuple gs]
   1.113 @@ -136,7 +140,7 @@
   1.114                    [Pretty.str "]"]), Pretty.brk 1, Pretty.str "()"];
   1.115  
   1.116              val gs = map (Pretty.str o suffix "G" o strip_tname) tvs;
   1.117 -            val gen_name = "gen_" ^ mk_type_id sg thyname thyname tname
   1.118 +            val gen_name = "gen_" ^ snd (get_type_id tname gr)
   1.119  
   1.120            in
   1.121              Pretty.blk (4, separate (Pretty.brk 1) 
   1.122 @@ -166,38 +170,38 @@
   1.123                 [Pretty.str " =", Pretty.brk 1] @
   1.124                 separate (Pretty.brk 1) (Pretty.str (gen_name ^ "'") :: gs @
   1.125                   [Pretty.str "i", Pretty.str "i"]))]) @
   1.126 -            mk_gen_of_def "and " xs
   1.127 +            mk_gen_of_def gr "and " xs
   1.128            end
   1.129  
   1.130    in
   1.131 -    ((Graph.add_edge_acyclic (dname, dep) gr
   1.132 +    (add_edge_acyclic (node_id, dep) gr
   1.133          handle Graph.CYCLES _ => gr) handle Graph.UNDEF _ =>
   1.134           let
   1.135 -           val gr1 = Graph.add_edge (dname, dep)
   1.136 -             (Graph.new_node (dname, (NONE, "", "")) gr);
   1.137 +           val gr1 = add_edge (node_id, dep)
   1.138 +             (new_node (node_id, (NONE, "", "")) gr);
   1.139             val (gr2, dtdef) = mk_dtdef gr1 "datatype " descr';
   1.140           in
   1.141 -           Graph.map_node dname (K (NONE, thyname,
   1.142 +           map_node node_id (K (NONE, module',
   1.143               Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
   1.144                 [Pretty.str ";"])) ^ "\n\n" ^
   1.145               (if "term_of" mem !mode then
   1.146                  Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk
   1.147 -                  (mk_term_of_def "fun " descr') @ [Pretty.str ";"])) ^ "\n\n"
   1.148 +                  (mk_term_of_def gr2 "fun " descr') @ [Pretty.str ";"])) ^ "\n\n"
   1.149                else "") ^
   1.150               (if "test" mem !mode then
   1.151                  Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk
   1.152 -                  (mk_gen_of_def "fun " descr') @ [Pretty.str ";"])) ^ "\n\n"
   1.153 +                  (mk_gen_of_def gr2 "fun " descr') @ [Pretty.str ";"])) ^ "\n\n"
   1.154                else ""))) gr2
   1.155 -         end, thyname)
   1.156 +         end
   1.157    end;
   1.158  
   1.159  
   1.160  (**** case expressions ****)
   1.161  
   1.162 -fun pretty_case thy defs gr dep thyname brack constrs (c as Const (_, T)) ts =
   1.163 +fun pretty_case thy defs gr dep module brack constrs (c as Const (_, T)) ts =
   1.164    let val i = length constrs
   1.165    in if length ts <= i then
   1.166 -       invoke_codegen thy defs dep thyname brack (gr, eta_expand c ts (i+1))
   1.167 +       invoke_codegen thy defs dep module brack (gr, eta_expand c ts (i+1))
   1.168      else
   1.169        let
   1.170          val ts1 = Library.take (i, ts);
   1.171 @@ -213,10 +217,10 @@
   1.172                  val xs = variantlist (replicate j "x", names);
   1.173                  val Us' = Library.take (j, fst (strip_type U));
   1.174                  val frees = map Free (xs ~~ Us');
   1.175 -                val (gr0, cp) = invoke_codegen thy defs dep thyname false
   1.176 +                val (gr0, cp) = invoke_codegen thy defs dep module false
   1.177                    (gr, list_comb (Const (cname, Us' ---> dT), frees));
   1.178                  val t' = Envir.beta_norm (list_comb (t, frees));
   1.179 -                val (gr1, p) = invoke_codegen thy defs dep thyname false (gr0, t');
   1.180 +                val (gr1, p) = invoke_codegen thy defs dep module false (gr0, t');
   1.181                  val (ps, gr2) = pcase gr1 cs ts Us;
   1.182                in
   1.183                  ([Pretty.block [cp, Pretty.str " =>", Pretty.brk 1, p]] :: ps, gr2)
   1.184 @@ -224,8 +228,8 @@
   1.185  
   1.186          val (ps1, gr1) = pcase gr constrs ts1 Ts;
   1.187          val ps = List.concat (separate [Pretty.brk 1, Pretty.str "| "] ps1);
   1.188 -        val (gr2, p) = invoke_codegen thy defs dep thyname false (gr1, t);
   1.189 -        val (gr3, ps2) = foldl_map (invoke_codegen thy defs dep thyname true) (gr2, ts2)
   1.190 +        val (gr2, p) = invoke_codegen thy defs dep module false (gr1, t);
   1.191 +        val (gr3, ps2) = foldl_map (invoke_codegen thy defs dep module true) (gr2, ts2)
   1.192        in (gr3, (if not (null ts2) andalso brack then parens else I)
   1.193          (Pretty.block (separate (Pretty.brk 1)
   1.194            (Pretty.block ([Pretty.str "(case ", p, Pretty.str " of",
   1.195 @@ -236,16 +240,15 @@
   1.196  
   1.197  (**** constructors ****)
   1.198  
   1.199 -fun pretty_constr thy defs gr dep thyname brack args (c as Const (s, T)) ts =
   1.200 +fun pretty_constr thy defs gr dep module brack args (c as Const (s, T)) ts =
   1.201    let val i = length args
   1.202    in if i > 1 andalso length ts < i then
   1.203 -      invoke_codegen thy defs dep thyname brack (gr, eta_expand c ts i)
   1.204 +      invoke_codegen thy defs dep module brack (gr, eta_expand c ts i)
   1.205       else
   1.206         let
   1.207 -         val thyname' = thyname_of_type (fst (dest_Type (body_type T))) thy;
   1.208 -         val id = mk_const_id (sign_of thy) thyname thyname' s;
   1.209 +         val id = mk_qual_id module (get_const_id s gr);
   1.210           val (gr', ps) = foldl_map
   1.211 -           (invoke_codegen thy defs dep thyname (i = 1)) (gr, ts);
   1.212 +           (invoke_codegen thy defs dep module (i = 1)) (gr, ts);
   1.213         in (case args of
   1.214            _ :: _ :: _ => (gr', (if brack then parens else I)
   1.215              (Pretty.block [Pretty.str id, Pretty.brk 1, mk_tuple ps]))
   1.216 @@ -256,7 +259,7 @@
   1.217  
   1.218  (**** code generators for terms and types ****)
   1.219  
   1.220 -fun datatype_codegen thy defs gr dep thyname brack t = (case strip_comb t of
   1.221 +fun datatype_codegen thy defs gr dep module brack t = (case strip_comb t of
   1.222     (c as Const (s, T), ts) =>
   1.223         (case find_first (fn (_, {index, descr, case_name, ...}) =>
   1.224           s = case_name orelse
   1.225 @@ -267,29 +270,29 @@
   1.226             if isSome (get_assoc_code thy s T) then NONE else
   1.227             let val SOME (_, _, constrs) = assoc (descr, index)
   1.228             in (case (assoc (constrs, s), strip_type T) of
   1.229 -               (NONE, _) => SOME (pretty_case thy defs gr dep thyname brack
   1.230 +               (NONE, _) => SOME (pretty_case thy defs gr dep module brack
   1.231                   (#3 (valOf (assoc (descr, index)))) c ts)
   1.232               | (SOME args, (_, Type _)) => SOME (pretty_constr thy defs
   1.233 -                 (fst (invoke_tycodegen thy defs dep thyname false
   1.234 +                 (fst (invoke_tycodegen thy defs dep module false
   1.235                      (gr, snd (strip_type T))))
   1.236 -                 dep thyname brack args c ts)
   1.237 +                 dep module brack args c ts)
   1.238               | _ => NONE)
   1.239             end)
   1.240   |  _ => NONE);
   1.241  
   1.242 -fun datatype_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) =
   1.243 +fun datatype_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
   1.244        (case Symtab.lookup (DatatypePackage.get_datatypes thy, s) of
   1.245           NONE => NONE
   1.246         | SOME {descr, ...} =>
   1.247             if isSome (get_assoc_type thy s) then NONE else
   1.248             let
   1.249               val (gr', ps) = foldl_map
   1.250 -               (invoke_tycodegen thy defs dep thyname false) (gr, Ts);
   1.251 -             val (gr'', thyname') = add_dt_defs thy defs dep gr' descr
   1.252 +               (invoke_tycodegen thy defs dep module false) (gr, Ts);
   1.253 +             val gr'' = add_dt_defs thy defs dep module gr' descr
   1.254             in SOME (gr'',
   1.255               Pretty.block ((if null Ts then [] else
   1.256                 [mk_tuple ps, Pretty.str " "]) @
   1.257 -               [Pretty.str (mk_type_id (sign_of thy) thyname thyname' s)]))
   1.258 +               [Pretty.str (mk_qual_id module (get_type_id s gr''))]))
   1.259             end)
   1.260    | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
   1.261  
     2.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Aug 25 09:29:05 2005 +0200
     2.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Aug 25 16:10:16 2005 +0200
     2.3 @@ -375,30 +375,31 @@
     2.4          else [Pretty.str ")"])))
     2.5    end;
     2.6  
     2.7 -fun strip_spaces s = implode (fst (take_suffix (equal " ") (explode s)));
     2.8 -
     2.9 -fun modename thy thyname thyname' s (iss, is) = space_implode "__"
    2.10 -  (mk_const_id (sign_of thy) thyname thyname' (strip_spaces s) ::
    2.11 -    map (space_implode "_" o map string_of_int) (List.mapPartial I iss @ [is]));
    2.12 +fun modename module s (iss, is) gr =
    2.13 +  let val (gr', id) = if s = "op =" then (gr, ("", "equal"))
    2.14 +    else mk_const_id module s gr
    2.15 +  in (gr', space_implode "__"
    2.16 +    (mk_qual_id module id ::
    2.17 +      map (space_implode "_" o map string_of_int) (List.mapPartial I iss @ [is])))
    2.18 +  end;
    2.19  
    2.20 -fun compile_expr thy defs dep thyname brack thynames (gr, (NONE, t)) =
    2.21 -      apsnd single (invoke_codegen thy defs dep thyname brack (gr, t))
    2.22 -  | compile_expr _ _ _ _ _ _ (gr, (SOME _, Var ((name, _), _))) =
    2.23 +fun compile_expr thy defs dep module brack (gr, (NONE, t)) =
    2.24 +      apsnd single (invoke_codegen thy defs dep module brack (gr, t))
    2.25 +  | compile_expr _ _ _ _ _ (gr, (SOME _, Var ((name, _), _))) =
    2.26        (gr, [Pretty.str name])
    2.27 -  | compile_expr thy defs dep thyname brack thynames (gr, (SOME (Mode (mode, ms)), t)) =
    2.28 +  | compile_expr thy defs dep module brack (gr, (SOME (Mode (mode, ms)), t)) =
    2.29        let
    2.30          val (Const (name, _), args) = strip_comb t;
    2.31 -        val (gr', ps) = foldl_map
    2.32 -          (compile_expr thy defs dep thyname true thynames) (gr, ms ~~ args);
    2.33 +        val (gr', (ps, mode_id)) = foldl_map
    2.34 +            (compile_expr thy defs dep module true) (gr, ms ~~ args) |>>>
    2.35 +          modename module name mode;
    2.36        in (gr', (if brack andalso not (null ps) then
    2.37          single o parens o Pretty.block else I)
    2.38            (List.concat (separate [Pretty.brk 1]
    2.39 -            ([Pretty.str (modename thy thyname
    2.40 -                (if name = "op =" then ""
    2.41 -                 else the (assoc (thynames, name))) name mode)] :: ps))))
    2.42 +            ([Pretty.str mode_id] :: ps))))
    2.43        end;
    2.44  
    2.45 -fun compile_clause thy defs gr dep thyname all_vs arg_vs modes thynames (iss, is) (ts, ps) =
    2.46 +fun compile_clause thy defs gr dep module all_vs arg_vs modes (iss, is) (ts, ps) =
    2.47    let
    2.48      val modes' = modes @ List.mapPartial
    2.49        (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
    2.50 @@ -411,7 +412,7 @@
    2.51  
    2.52      fun compile_eq (gr, (s, t)) =
    2.53        apsnd (Pretty.block o cons (Pretty.str (s ^ " = ")) o single)
    2.54 -        (invoke_codegen thy defs dep thyname false (gr, t));
    2.55 +        (invoke_codegen thy defs dep module false (gr, t));
    2.56  
    2.57      val (in_ts, out_ts) = get_args is 1 ts;
    2.58      val ((all_vs', eqs), in_ts') =
    2.59 @@ -424,14 +425,14 @@
    2.60      fun compile_prems out_ts' vs names gr [] =
    2.61            let
    2.62              val (gr2, out_ps) = foldl_map
    2.63 -              (invoke_codegen thy defs dep thyname false) (gr, out_ts);
    2.64 +              (invoke_codegen thy defs dep module false) (gr, out_ts);
    2.65              val (gr3, eq_ps) = foldl_map compile_eq (gr2, eqs);
    2.66              val ((names', eqs'), out_ts'') =
    2.67                foldl_map check_constrt ((names, []), out_ts');
    2.68              val (nvs, out_ts''') = foldl_map distinct_v
    2.69                ((names', map (fn x => (x, [x])) vs), out_ts'');
    2.70              val (gr4, out_ps') = foldl_map
    2.71 -              (invoke_codegen thy defs dep thyname false) (gr3, out_ts''');
    2.72 +              (invoke_codegen thy defs dep module false) (gr3, out_ts''');
    2.73              val (gr5, eq_ps') = foldl_map compile_eq (gr4, eqs')
    2.74            in
    2.75              (gr5, compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
    2.76 @@ -449,7 +450,7 @@
    2.77              val (nvs, out_ts'') = foldl_map distinct_v
    2.78                ((names', map (fn x => (x, [x])) vs), out_ts');
    2.79              val (gr0, out_ps) = foldl_map
    2.80 -              (invoke_codegen thy defs dep thyname false) (gr, out_ts'');
    2.81 +              (invoke_codegen thy defs dep module false) (gr, out_ts'');
    2.82              val (gr1, eq_ps) = foldl_map compile_eq (gr0, eqs)
    2.83            in
    2.84              (case p of
    2.85 @@ -457,15 +458,15 @@
    2.86                   let
    2.87                     val (in_ts, out_ts''') = get_args js 1 us;
    2.88                     val (gr2, in_ps) = foldl_map
    2.89 -                     (invoke_codegen thy defs dep thyname false) (gr1, in_ts);
    2.90 +                     (invoke_codegen thy defs dep module false) (gr1, in_ts);
    2.91                     val (gr3, ps) = if is_ind t then
    2.92                         apsnd (fn ps => ps @ [Pretty.brk 1, mk_tuple in_ps])
    2.93 -                         (compile_expr thy defs dep thyname false thynames
    2.94 +                         (compile_expr thy defs dep module false
    2.95                             (gr2, (mode, t)))
    2.96                       else
    2.97                         apsnd (fn p => conv_ntuple us t
    2.98                           [Pretty.str "Seq.of_list", Pretty.brk 1, p])
    2.99 -                           (invoke_codegen thy defs dep thyname true (gr2, t));
   2.100 +                           (invoke_codegen thy defs dep module true (gr2, t));
   2.101                     val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps';
   2.102                   in
   2.103                     (gr4, compile_match (snd nvs) eq_ps out_ps
   2.104 @@ -475,7 +476,7 @@
   2.105                   end
   2.106               | Sidecond t =>
   2.107                   let
   2.108 -                   val (gr2, side_p) = invoke_codegen thy defs dep thyname true (gr1, t);
   2.109 +                   val (gr2, side_p) = invoke_codegen thy defs dep module true (gr1, t);
   2.110                     val (gr3, rest) = compile_prems [] vs' (fst nvs) gr2 ps';
   2.111                   in
   2.112                     (gr3, compile_match (snd nvs) eq_ps out_ps
   2.113 @@ -490,23 +491,25 @@
   2.114      (gr', Pretty.block [Pretty.str "Seq.single inp :->", Pretty.brk 1, prem_p])
   2.115    end;
   2.116  
   2.117 -fun compile_pred thy defs gr dep thyname prfx all_vs arg_vs modes thynames s cls mode =
   2.118 -  let val (gr', cl_ps) = foldl_map (fn (gr, cl) => compile_clause thy defs
   2.119 -    gr dep thyname all_vs arg_vs modes thynames mode cl) (gr, cls)
   2.120 +fun compile_pred thy defs gr dep module prfx all_vs arg_vs modes s cls mode =
   2.121 +  let val (gr', (cl_ps, mode_id)) =
   2.122 +    foldl_map (fn (gr, cl) => compile_clause thy defs
   2.123 +      gr dep module all_vs arg_vs modes mode cl) (gr, cls) |>>>
   2.124 +    modename module s mode
   2.125    in
   2.126      ((gr', "and "), Pretty.block
   2.127        ([Pretty.block (separate (Pretty.brk 1)
   2.128 -         (Pretty.str (prfx ^ modename thy thyname thyname s mode) ::
   2.129 +         (Pretty.str (prfx ^ mode_id) ::
   2.130             map Pretty.str arg_vs) @
   2.131           [Pretty.str " inp ="]),
   2.132          Pretty.brk 1] @
   2.133         List.concat (separate [Pretty.str " ++", Pretty.brk 1] (map single cl_ps))))
   2.134    end;
   2.135  
   2.136 -fun compile_preds thy defs gr dep thyname all_vs arg_vs modes thynames preds =
   2.137 +fun compile_preds thy defs gr dep module all_vs arg_vs modes preds =
   2.138    let val ((gr', _), prs) = foldl_map (fn ((gr, prfx), (s, cls)) =>
   2.139      foldl_map (fn ((gr', prfx'), mode) => compile_pred thy defs gr'
   2.140 -      dep thyname prfx' all_vs arg_vs modes thynames s cls mode)
   2.141 +      dep module prfx' all_vs arg_vs modes s cls mode)
   2.142          ((gr, prfx), valOf (assoc (modes, s)))) ((gr, "fun "), preds)
   2.143    in
   2.144      (gr', space_implode "\n\n" (map Pretty.string_of (List.concat prs)) ^ ";\n\n")
   2.145 @@ -516,13 +519,11 @@
   2.146  
   2.147  exception Modes of
   2.148    (string * (int list option list * int list) list) list *
   2.149 -  (string * (int list list option list * int list list)) list *
   2.150 -  string;
   2.151 +  (string * (int list list option list * int list list)) list;
   2.152  
   2.153 -fun lookup_modes gr dep = foldl (fn ((xs, ys, z), (xss, yss, zss)) =>
   2.154 -    (xss @ xs, yss @ ys, zss @ map (rpair z o fst) ys)) ([], [], [])
   2.155 -  (map ((fn (SOME (Modes x), _, _) => x | _ => ([], [], "")) o Graph.get_node gr)
   2.156 -    (Graph.all_preds gr [dep]));
   2.157 +fun lookup_modes gr dep = apfst List.concat (apsnd List.concat (ListPair.unzip
   2.158 +  (map ((fn (SOME (Modes x), _, _) => x | _ => ([], [])) o get_node gr)
   2.159 +    (Graph.all_preds (fst gr) [dep]))));
   2.160  
   2.161  fun print_factors factors = message ("Factors:\n" ^
   2.162    space_implode "\n" (map (fn (s, (fs, f)) => s ^ ": " ^
   2.163 @@ -537,17 +538,18 @@
   2.164        NONE => xs
   2.165      | SOME xs' => xs inter xs') :: constrain cs ys;
   2.166  
   2.167 -fun mk_extra_defs thy defs gr dep names ts =
   2.168 +fun mk_extra_defs thy defs gr dep names module ts =
   2.169    Library.foldl (fn (gr, name) =>
   2.170      if name mem names then gr
   2.171      else (case get_clauses thy name of
   2.172          NONE => gr
   2.173        | SOME (names, thyname, intrs) =>
   2.174 -          mk_ind_def thy defs gr dep names thyname [] [] (prep_intrs intrs)))
   2.175 +          mk_ind_def thy defs gr dep names (if_library thyname module)
   2.176 +            [] [] (prep_intrs intrs)))
   2.177              (gr, foldr add_term_consts [] ts)
   2.178  
   2.179 -and mk_ind_def thy defs gr dep names thyname modecs factorcs intrs =
   2.180 -  Graph.add_edge (hd names, dep) gr handle Graph.UNDEF _ =>
   2.181 +and mk_ind_def thy defs gr dep names module modecs factorcs intrs =
   2.182 +  add_edge (hd names, dep) gr handle Graph.UNDEF _ =>
   2.183      let
   2.184        val _ $ (_ $ _ $ u) = Logic.strip_imp_concl (hd intrs);
   2.185        val (_, args) = strip_comb u;
   2.186 @@ -584,9 +586,9 @@
   2.187          | add_prod_factors _ (fs, _) = fs;
   2.188  
   2.189        val gr' = mk_extra_defs thy defs
   2.190 -        (Graph.add_edge (hd names, dep)
   2.191 -          (Graph.new_node (hd names, (NONE, "", "")) gr)) (hd names) names intrs;
   2.192 -      val (extra_modes, extra_factors, extra_thynames) = lookup_modes gr' (hd names);
   2.193 +        (add_edge (hd names, dep)
   2.194 +          (new_node (hd names, (NONE, "", "")) gr)) (hd names) names module intrs;
   2.195 +      val (extra_modes, extra_factors) = lookup_modes gr' (hd names);
   2.196        val fs = constrain factorcs (map (apsnd dest_factors)
   2.197          (Library.foldl (add_prod_factors extra_factors) ([], List.concat (map (fn t =>
   2.198            Logic.strip_imp_concl t :: Logic.strip_imp_prems t) intrs))));
   2.199 @@ -599,40 +601,42 @@
   2.200          (infer_modes thy extra_modes factors arg_vs clauses);
   2.201        val _ = print_factors factors;
   2.202        val _ = print_modes modes;
   2.203 -      val (gr'', s) = compile_preds thy defs gr' (hd names) thyname (terms_vs intrs)
   2.204 -        arg_vs (modes @ extra_modes)
   2.205 -        (map (rpair thyname o fst) factors @ extra_thynames) clauses;
   2.206 +      val (gr'', s) = compile_preds thy defs gr' (hd names) module (terms_vs intrs)
   2.207 +        arg_vs (modes @ extra_modes) clauses;
   2.208      in
   2.209 -      (Graph.map_node (hd names)
   2.210 -        (K (SOME (Modes (modes, factors, thyname)), thyname, s)) gr'')
   2.211 +      (map_node (hd names)
   2.212 +        (K (SOME (Modes (modes, factors)), module, s)) gr'')
   2.213      end;
   2.214  
   2.215 -fun find_mode s u modes is = (case find_first (fn Mode ((_, js), _) => is=js)
   2.216 +fun find_mode gr dep s u modes is = (case find_first (fn Mode ((_, js), _) => is=js)
   2.217    (modes_of modes u handle Option => []) of
   2.218 -     NONE => error ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
   2.219 +     NONE => codegen_error gr dep
   2.220 +       ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
   2.221     | mode => mode);
   2.222  
   2.223 -fun mk_ind_call thy defs gr dep thyname t u is_query = (case head_of u of
   2.224 +fun mk_ind_call thy defs gr dep module t u is_query = (case head_of u of
   2.225    Const (s, T) => (case (get_clauses thy s, get_assoc_code thy s T) of
   2.226         (NONE, _) => NONE
   2.227 -     | (SOME (names, thyname', intrs), NONE) =>
   2.228 +     | (SOME (names, thyname, intrs), NONE) =>
   2.229           let
   2.230            fun mk_mode (((ts, mode), i), Const ("dummy_pattern", _)) =
   2.231                  ((ts, mode), i+1)
   2.232              | mk_mode (((ts, mode), i), t) = ((ts @ [t], mode @ [i]), i+1);
   2.233  
   2.234 +           val module' = if_library thyname module;
   2.235             val gr1 = mk_extra_defs thy defs
   2.236 -             (mk_ind_def thy defs gr dep names thyname' [] [] (prep_intrs intrs)) dep names [u];
   2.237 -           val (modes, factors, thynames) = lookup_modes gr1 dep;
   2.238 +             (mk_ind_def thy defs gr dep names module'
   2.239 +             [] [] (prep_intrs intrs)) dep names module' [u];
   2.240 +           val (modes, factors) = lookup_modes gr1 dep;
   2.241             val ts = split_prod [] (snd (valOf (assoc (factors, s)))) t;
   2.242             val (ts', is) = if is_query then
   2.243                 fst (Library.foldl mk_mode ((([], []), 1), ts))
   2.244               else (ts, 1 upto length ts);
   2.245 -           val mode = find_mode s u modes is;
   2.246 +           val mode = find_mode gr1 dep s u modes is;
   2.247             val (gr2, in_ps) = foldl_map
   2.248 -             (invoke_codegen thy defs dep thyname false) (gr1, ts');
   2.249 +             (invoke_codegen thy defs dep module false) (gr1, ts');
   2.250             val (gr3, ps) =
   2.251 -             compile_expr thy defs dep thyname false thynames (gr2, (mode, u))
   2.252 +             compile_expr thy defs dep module false (gr2, (mode, u))
   2.253           in
   2.254             SOME (gr3, Pretty.block
   2.255               (ps @ [Pretty.brk 1, mk_tuple in_ps]))
   2.256 @@ -640,17 +644,19 @@
   2.257       | _ => NONE)
   2.258    | _ => NONE);
   2.259  
   2.260 -fun list_of_indset thy defs gr dep thyname brack u = (case head_of u of
   2.261 +fun list_of_indset thy defs gr dep module brack u = (case head_of u of
   2.262    Const (s, T) => (case (get_clauses thy s, get_assoc_code thy s T) of
   2.263         (NONE, _) => NONE
   2.264 -     | (SOME (names, thyname', intrs), NONE) =>
   2.265 +     | (SOME (names, thyname, intrs), NONE) =>
   2.266           let
   2.267 +           val module' = if_library thyname module;
   2.268             val gr1 = mk_extra_defs thy defs
   2.269 -             (mk_ind_def thy defs gr dep names thyname' [] [] (prep_intrs intrs)) dep names [u];
   2.270 -           val (modes, factors, thynames) = lookup_modes gr1 dep;
   2.271 -           val mode = find_mode s u modes [];
   2.272 +             (mk_ind_def thy defs gr dep names module'
   2.273 +             [] [] (prep_intrs intrs)) dep names module' [u];
   2.274 +           val (modes, factors) = lookup_modes gr1 dep;
   2.275 +           val mode = find_mode gr1 dep s u modes [];
   2.276             val (gr2, ps) =
   2.277 -             compile_expr thy defs dep thyname false thynames (gr1, (mode, u))
   2.278 +             compile_expr thy defs dep module false (gr1, (mode, u))
   2.279           in
   2.280             SOME (gr2, (if brack then parens else I)
   2.281               (Pretty.block ([Pretty.str "Seq.list_of", Pretty.brk 1,
   2.282 @@ -671,54 +677,56 @@
   2.283    in
   2.284      rename_term
   2.285        (Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop (HOLogic.mk_mem
   2.286 -        (foldr1 HOLogic.mk_prod (ts @ [u]), Const (s ^ " ",
   2.287 +        (foldr1 HOLogic.mk_prod (ts @ [u]), Const (s ^ "_aux",
   2.288            HOLogic.mk_setT (foldr1 HOLogic.mk_prodT (Ts @ [U])))))))
   2.289    end;
   2.290  
   2.291 -fun mk_fun thy defs name eqns dep thyname thyname' gr =
   2.292 -  let
   2.293 -    val fun_id = mk_const_id (sign_of thy) thyname' thyname' name;
   2.294 -    val call_id = mk_const_id (sign_of thy) thyname thyname' name
   2.295 -  in (Graph.add_edge (name, dep) gr handle Graph.UNDEF _ =>
   2.296 +fun mk_fun thy defs name eqns dep module module' gr =
   2.297 +  case try (get_node gr) name of
   2.298 +    NONE =>
   2.299      let
   2.300        val clauses = map clause_of_eqn eqns;
   2.301 -      val pname = name ^ " ";
   2.302 +      val pname = name ^ "_aux";
   2.303        val arity = length (snd (strip_comb (fst (HOLogic.dest_eq
   2.304          (HOLogic.dest_Trueprop (concl_of (hd eqns)))))));
   2.305        val mode = 1 upto arity;
   2.306 +      val (gr', (fun_id, mode_id)) = gr |>
   2.307 +        mk_const_id module' name |>>>
   2.308 +        modename module' pname ([], mode);
   2.309        val vars = map (fn i => Pretty.str ("x" ^ string_of_int i)) mode;
   2.310        val s = Pretty.string_of (Pretty.block
   2.311 -        [mk_app false (Pretty.str ("fun " ^ fun_id)) vars, Pretty.str " =",
   2.312 +        [mk_app false (Pretty.str ("fun " ^ snd fun_id)) vars, Pretty.str " =",
   2.313           Pretty.brk 1, Pretty.str "Seq.hd", Pretty.brk 1,
   2.314 -         parens (Pretty.block [Pretty.str (modename thy thyname' thyname' pname ([], mode)),
   2.315 +         parens (Pretty.block [Pretty.str mode_id,
   2.316             Pretty.brk 1, mk_tuple vars])]) ^ ";\n\n";
   2.317 -      val gr' = mk_ind_def thy defs (Graph.add_edge (name, dep)
   2.318 -        (Graph.new_node (name, (NONE, thyname', s)) gr)) name [pname] thyname'
   2.319 +      val gr'' = mk_ind_def thy defs (add_edge (name, dep)
   2.320 +        (new_node (name, (NONE, module', s)) gr')) name [pname] module'
   2.321          [(pname, [([], mode)])]
   2.322          [(pname, map (fn i => replicate i 2) (0 upto arity-1))]
   2.323          clauses;
   2.324 -      val (modes, _, _) = lookup_modes gr' dep;
   2.325 -      val _ = find_mode pname (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
   2.326 +      val (modes, _) = lookup_modes gr'' dep;
   2.327 +      val _ = find_mode gr'' dep pname (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
   2.328          (Logic.strip_imp_concl (hd clauses))))) modes mode
   2.329 -    in gr' end, call_id)
   2.330 -  end;
   2.331 +    in (gr'', mk_qual_id module fun_id) end
   2.332 +  | SOME _ =>
   2.333 +      (add_edge (name, dep) gr, mk_qual_id module (get_const_id name gr));
   2.334  
   2.335 -fun inductive_codegen thy defs gr dep thyname brack (Const ("op :", _) $ t $ u) =
   2.336 -      ((case mk_ind_call thy defs gr dep thyname (Term.no_dummy_patterns t) u false of
   2.337 +fun inductive_codegen thy defs gr dep module brack (Const ("op :", _) $ t $ u) =
   2.338 +      ((case mk_ind_call thy defs gr dep module (Term.no_dummy_patterns t) u false of
   2.339           NONE => NONE
   2.340         | SOME (gr', call_p) => SOME (gr', (if brack then parens else I)
   2.341             (Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"])))
   2.342 -        handle TERM _ => mk_ind_call thy defs gr dep thyname t u true)
   2.343 -  | inductive_codegen thy defs gr dep thyname brack t = (case strip_comb t of
   2.344 +        handle TERM _ => mk_ind_call thy defs gr dep module t u true)
   2.345 +  | inductive_codegen thy defs gr dep module brack t = (case strip_comb t of
   2.346        (Const (s, _), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy), s) of
   2.347 -        NONE => list_of_indset thy defs gr dep thyname brack t
   2.348 +        NONE => list_of_indset thy defs gr dep module brack t
   2.349        | SOME eqns =>
   2.350            let
   2.351 -            val (_, (_, thyname')) = split_last eqns;
   2.352 +            val (_, (_, thyname)) = split_last eqns;
   2.353              val (gr', id) = mk_fun thy defs s (preprocess thy (map fst eqns))
   2.354 -              dep thyname thyname' gr;
   2.355 +              dep module (if_library thyname module) gr;
   2.356              val (gr'', ps) = foldl_map
   2.357 -              (invoke_codegen thy defs dep thyname true) (gr', ts);
   2.358 +              (invoke_codegen thy defs dep module true) (gr', ts);
   2.359            in SOME (gr'', mk_app brack (Pretty.str id) ps)
   2.360            end)
   2.361      | _ => NONE);
   2.362 @@ -745,8 +753,8 @@
   2.363  
   2.364  fun ?! s = isSome (Seq.pull s);    
   2.365  
   2.366 -fun op_61__1 x = Seq.single x;
   2.367 +fun equal__1 x = Seq.single x;
   2.368  
   2.369 -val op_61__2 = op_61__1;
   2.370 +val equal__2 = equal__1;
   2.371  
   2.372 -fun op_61__1_2 (x, y) = ?? (x = y);
   2.373 +fun equal__1_2 (x, y) = ?? (x = y);
     3.1 --- a/src/HOL/Tools/recfun_codegen.ML	Thu Aug 25 09:29:05 2005 +0200
     3.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Thu Aug 25 16:10:16 2005 +0200
     3.3 @@ -82,15 +82,15 @@
     3.4         end);
     3.5  
     3.6  fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
     3.7 -  SOME (_, SOME i) => "_def" ^ string_of_int i | _ => "");
     3.8 +  SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
     3.9  
    3.10  exception EQN of string * typ * string;
    3.11  
    3.12  fun cycle g (xs, x) =
    3.13    if x mem xs then xs
    3.14 -  else Library.foldl (cycle g) (x :: xs, List.concat (Graph.find_paths g (x, x)));
    3.15 +  else Library.foldl (cycle g) (x :: xs, List.concat (Graph.find_paths (fst g) (x, x)));
    3.16  
    3.17 -fun add_rec_funs thy defs gr dep eqs thyname =
    3.18 +fun add_rec_funs thy defs gr dep eqs module =
    3.19    let
    3.20      fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
    3.21        dest_eqn (rename_term t));
    3.22 @@ -98,67 +98,71 @@
    3.23      val (dname, _) :: _ = eqs';
    3.24      val (s, T) = const_of (hd eqs);
    3.25  
    3.26 -    fun mk_fundef thyname fname prfx gr [] = (gr, [])
    3.27 -      | mk_fundef thyname fname prfx gr ((fname', (lhs, rhs)) :: xs) =
    3.28 +    fun mk_fundef module fname prfx gr [] = (gr, [])
    3.29 +      | mk_fundef module fname prfx gr ((fname', (lhs, rhs)) :: xs) =
    3.30        let
    3.31 -        val (gr1, pl) = invoke_codegen thy defs dname thyname false (gr, lhs);
    3.32 -        val (gr2, pr) = invoke_codegen thy defs dname thyname false (gr1, rhs);
    3.33 -        val (gr3, rest) = mk_fundef thyname fname' "and " gr2 xs
    3.34 +        val (gr1, pl) = invoke_codegen thy defs dname module false (gr, lhs);
    3.35 +        val (gr2, pr) = invoke_codegen thy defs dname module false (gr1, rhs);
    3.36 +        val (gr3, rest) = mk_fundef module fname' "and " gr2 xs
    3.37        in
    3.38          (gr3, Pretty.blk (4, [Pretty.str (if fname = fname' then "  | " else prfx),
    3.39             pl, Pretty.str " =", Pretty.brk 1, pr]) :: rest)
    3.40        end;
    3.41  
    3.42 -    fun put_code thyname fundef = Graph.map_node dname
    3.43 -      (K (SOME (EQN ("", dummyT, dname)), thyname, Pretty.string_of (Pretty.blk (0,
    3.44 +    fun put_code module fundef = map_node dname
    3.45 +      (K (SOME (EQN ("", dummyT, dname)), module, Pretty.string_of (Pretty.blk (0,
    3.46        separate Pretty.fbrk fundef @ [Pretty.str ";"])) ^ "\n\n"));
    3.47  
    3.48    in
    3.49 -    (case try (Graph.get_node gr) dname of
    3.50 +    (case try (get_node gr) dname of
    3.51         NONE =>
    3.52           let
    3.53 -           val gr1 = Graph.add_edge (dname, dep)
    3.54 -             (Graph.new_node (dname, (SOME (EQN (s, T, "")), "", "")) gr);
    3.55 -           val (gr2, fundef) = mk_fundef thyname "" "fun " gr1 eqs';
    3.56 +           val gr1 = add_edge (dname, dep)
    3.57 +             (new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr);
    3.58 +           val (gr2, fundef) = mk_fundef module "" "fun " gr1 eqs';
    3.59             val xs = cycle gr2 ([], dname);
    3.60 -           val cs = map (fn x => case Graph.get_node gr2 x of
    3.61 +           val cs = map (fn x => case get_node gr2 x of
    3.62                 (SOME (EQN (s, T, _)), _, _) => (s, T)
    3.63               | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^
    3.64                  implode (separate ", " xs))) xs
    3.65           in (case xs of
    3.66 -             [_] => put_code thyname fundef gr2
    3.67 +             [_] => (put_code module fundef gr2, module)
    3.68             | _ =>
    3.69               if not (dep mem xs) then
    3.70                 let
    3.71                   val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
    3.72 +                 val module' = if_library thyname module;
    3.73                   val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss));
    3.74 -                 val (gr3, fundef') = mk_fundef thyname "" "fun "
    3.75 -                   (Graph.add_edge (dname, dep)
    3.76 -                     (foldr (uncurry Graph.new_node) (Graph.del_nodes xs gr2)
    3.77 +                 val (gr3, fundef') = mk_fundef module' "" "fun "
    3.78 +                   (add_edge (dname, dep)
    3.79 +                     (foldr (uncurry new_node) (del_nodes xs gr2)
    3.80                         (map (fn k =>
    3.81 -                         (k, (SOME (EQN ("", dummyT, dname)), thyname, ""))) xs))) eqs''
    3.82 -               in put_code thyname fundef' gr3 end
    3.83 -             else gr2)
    3.84 +                         (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs))) eqs''
    3.85 +               in (put_code module' fundef' gr3, module') end
    3.86 +             else (gr2, module))
    3.87           end
    3.88 -     | SOME (SOME (EQN (_, _, s)), _, _) =>
    3.89 -         if s = "" then
    3.90 -           if dname = dep then gr else Graph.add_edge (dname, dep) gr
    3.91 -         else if s = dep then gr else Graph.add_edge (s, dep) gr)
    3.92 +     | SOME (SOME (EQN (_, _, s)), module', _) =>
    3.93 +         (if s = "" then
    3.94 +            if dname = dep then gr else add_edge (dname, dep) gr
    3.95 +          else if s = dep then gr else add_edge (s, dep) gr,
    3.96 +          module'))
    3.97    end;
    3.98  
    3.99 -fun recfun_codegen thy defs gr dep thyname brack t = (case strip_comb t of
   3.100 +fun recfun_codegen thy defs gr dep module brack t = (case strip_comb t of
   3.101      (Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy s T) of
   3.102         (([], _), _) => NONE
   3.103       | (_, SOME _) => NONE
   3.104 -     | ((eqns, thyname'), NONE) =>
   3.105 +     | ((eqns, thyname), NONE) =>
   3.106          let
   3.107 +          val module' = if_library thyname module;
   3.108            val (gr', ps) = foldl_map
   3.109 -            (invoke_codegen thy defs dep thyname true) (gr, ts);
   3.110 -          val suffix = mk_suffix thy defs p
   3.111 +            (invoke_codegen thy defs dep module true) (gr, ts);
   3.112 +          val suffix = mk_suffix thy defs p;
   3.113 +          val (gr'', module'') =
   3.114 +            add_rec_funs thy defs gr' dep (map prop_of eqns) module';
   3.115 +          val (gr''', fname) = mk_const_id module'' (s ^ suffix) gr''
   3.116          in
   3.117 -          SOME (add_rec_funs thy defs gr' dep (map prop_of eqns) thyname',
   3.118 -            mk_app brack (Pretty.str
   3.119 -              (mk_const_id (sign_of thy) thyname thyname' s ^ suffix)) ps)
   3.120 +          SOME (gr''', mk_app brack (Pretty.str (mk_qual_id module fname)) ps)
   3.121          end)
   3.122    | _ => NONE);
   3.123  
     4.1 --- a/src/HOL/Tools/typedef_package.ML	Thu Aug 25 09:29:05 2005 +0200
     4.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Aug 25 16:10:16 2005 +0200
     4.3 @@ -272,17 +272,16 @@
     4.4  
     4.5  (** trivial code generator **)
     4.6  
     4.7 -fun typedef_codegen thy defs gr dep thyname brack t =
     4.8 +fun typedef_codegen thy defs gr dep module brack t =
     4.9    let
    4.10      fun get_name (Type (tname, _)) = tname
    4.11        | get_name _ = "";
    4.12      fun mk_fun s T ts =
    4.13        let
    4.14 -        val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr, T);
    4.15 +        val (gr', _) = Codegen.invoke_tycodegen thy defs dep module false (gr, T);
    4.16          val (gr'', ps) =
    4.17 -          foldl_map (Codegen.invoke_codegen thy defs dep thyname true) (gr', ts);
    4.18 -        val id = Codegen.mk_const_id thy
    4.19 -          thyname (Codegen.thyname_of_type (get_name T) thy) s
    4.20 +          foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts);
    4.21 +        val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'')
    4.22        in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
    4.23      fun lookup f T = getOpt (Option.map f (Symtab.lookup
    4.24        (TypedefData.get thy, get_name T)), "")
    4.25 @@ -303,28 +302,32 @@
    4.26    | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)]
    4.27    | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
    4.28  
    4.29 -fun typedef_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) =
    4.30 +fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
    4.31        (case Symtab.lookup (TypedefData.get thy, s) of
    4.32           NONE => NONE
    4.33         | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) =>
    4.34             if isSome (Codegen.get_assoc_type thy tname) then NONE else
    4.35             let
    4.36 -             val thyname' = Codegen.thyname_of_type tname thy;
    4.37 -             val Abs_id = Codegen.mk_const_id thy thyname' thyname' Abs_name;
    4.38 -             val Rep_id = Codegen.mk_const_id thy thyname' thyname' Rep_name;
    4.39 -             val ty_id = Codegen.mk_type_id thy thyname' thyname' s;
    4.40 -             val ty_call_id = Codegen.mk_type_id thy thyname thyname' s;
    4.41 -             val (gr', qs) = foldl_map
    4.42 -               (Codegen.invoke_tycodegen thy defs dep thyname (length Ts = 1)) (gr, Ts);
    4.43 -             val gr'' = Graph.add_edge (Abs_name, dep) gr' handle Graph.UNDEF _ =>
    4.44 +             val module' = Codegen.if_library
    4.45 +               (Codegen.thyname_of_type tname thy) module;
    4.46 +             val node_id = tname ^ " (type)";
    4.47 +             val (gr', (((qs, (_, Abs_id)), (_, Rep_id)), ty_id)) = foldl_map
    4.48 +                 (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
    4.49 +                   (gr, Ts) |>>>
    4.50 +               Codegen.mk_const_id module' Abs_name |>>>
    4.51 +               Codegen.mk_const_id module' Rep_name |>>>
    4.52 +               Codegen.mk_type_id module' s;
    4.53 +             val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
    4.54 +           in SOME (case try (Codegen.get_node gr') node_id of
    4.55 +               NONE =>
    4.56                 let
    4.57                   val (gr'', p :: ps) = foldl_map
    4.58 -                   (Codegen.invoke_tycodegen thy defs Abs_name thyname' false)
    4.59 -                   (Graph.add_edge (Abs_name, dep)
    4.60 -                      (Graph.new_node (Abs_name, (NONE, "", "")) gr'), oldT :: Us);
    4.61 +                   (Codegen.invoke_tycodegen thy defs node_id module' false)
    4.62 +                   (Codegen.add_edge (node_id, dep)
    4.63 +                      (Codegen.new_node (node_id, (NONE, "", "")) gr'), oldT :: Us);
    4.64                   val s =
    4.65                     Pretty.string_of (Pretty.block [Pretty.str "datatype ",
    4.66 -                     mk_tyexpr ps ty_id,
    4.67 +                     mk_tyexpr ps (snd ty_id),
    4.68                       Pretty.str " =", Pretty.brk 1, Pretty.str (Abs_id ^ " of"),
    4.69                       Pretty.brk 1, p, Pretty.str ";"]) ^ "\n\n" ^
    4.70                     Pretty.string_of (Pretty.block [Pretty.str ("fun " ^ Rep_id),
    4.71 @@ -332,28 +335,27 @@
    4.72                       Pretty.str "x) = x;"]) ^ "\n\n" ^
    4.73                     (if "term_of" mem !Codegen.mode then
    4.74                        Pretty.string_of (Pretty.block [Pretty.str "fun ",
    4.75 -                        Codegen.mk_term_of thy thyname' false newT, Pretty.brk 1,
    4.76 +                        Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
    4.77                          Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
    4.78                          Pretty.str "x) =", Pretty.brk 1,
    4.79                          Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","),
    4.80                            Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
    4.81                            Pretty.str ")"], Pretty.str " $", Pretty.brk 1,
    4.82 -                        Codegen.mk_term_of thy thyname' false oldT, Pretty.brk 1,
    4.83 +                        Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
    4.84                          Pretty.str "x;"]) ^ "\n\n"
    4.85                      else "") ^
    4.86                     (if "test" mem !Codegen.mode then
    4.87                        Pretty.string_of (Pretty.block [Pretty.str "fun ",
    4.88 -                        Codegen.mk_gen thy thyname' false [] "" newT, Pretty.brk 1,
    4.89 +                        Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
    4.90                          Pretty.str "i =", Pretty.brk 1,
    4.91                          Pretty.block [Pretty.str (Abs_id ^ " ("),
    4.92 -                          Codegen.mk_gen thy thyname' false [] "" oldT, Pretty.brk 1,
    4.93 +                          Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
    4.94                            Pretty.str "i);"]]) ^ "\n\n"
    4.95                      else "")
    4.96 -               in Graph.map_node Abs_name (K (NONE, thyname', s)) gr'' end
    4.97 -           in
    4.98 -             SOME (gr'', mk_tyexpr qs ty_call_id)
    4.99 +               in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
   4.100 +             | SOME _ => Codegen.add_edge (node_id, dep) gr', tyexpr)
   4.101             end)
   4.102 -  | typedef_tycodegen thy defs gr dep thyname brack _ = NONE;
   4.103 +  | typedef_tycodegen thy defs gr dep module brack _ = NONE;
   4.104  
   4.105  val setup =
   4.106    [TypedefData.init,
     5.1 --- a/src/Pure/codegen.ML	Thu Aug 25 09:29:05 2005 +0200
     5.2 +++ b/src/Pure/codegen.ML	Thu Aug 25 16:10:16 2005 +0200
     5.3 @@ -20,6 +20,7 @@
     5.4      | Quote of 'a;
     5.5  
     5.6    type deftab
     5.7 +  type node
     5.8    type codegr
     5.9    type 'a codegen
    5.10  
    5.11 @@ -29,8 +30,10 @@
    5.12    val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory
    5.13    val preprocess: theory -> thm list -> thm list
    5.14    val print_codegens: theory -> unit
    5.15 -  val generate_code: theory -> (string * string) list -> (string * string) list
    5.16 -  val generate_code_i: theory -> (string * term) list -> (string * string) list
    5.17 +  val generate_code: theory -> string list -> string -> (string * string) list ->
    5.18 +    (string * string) list * codegr
    5.19 +  val generate_code_i: theory -> string list -> string -> (string * term) list ->
    5.20 +    (string * string) list * codegr
    5.21    val assoc_consts: (xstring * string option * (term mixfix list *
    5.22      (string * string) list)) list -> theory -> theory
    5.23    val assoc_consts_i: (xstring * typ option * (term mixfix list *
    5.24 @@ -41,19 +44,24 @@
    5.25      (term mixfix list * (string * string) list) option
    5.26    val get_assoc_type: theory -> string ->
    5.27      (typ mixfix list * (string * string) list) option
    5.28 +  val codegen_error: codegr -> string -> string -> 'a
    5.29    val invoke_codegen: theory -> deftab -> string -> string -> bool ->
    5.30      codegr * term -> codegr * Pretty.T
    5.31    val invoke_tycodegen: theory -> deftab -> string -> string -> bool ->
    5.32      codegr * typ -> codegr * Pretty.T
    5.33    val mk_id: string -> string
    5.34 -  val mk_const_id: theory -> string -> string -> string -> string
    5.35 -  val mk_type_id: theory -> string -> string -> string -> string
    5.36 +  val mk_qual_id: string -> string * string -> string
    5.37 +  val mk_const_id: string -> string -> codegr -> codegr * (string * string)
    5.38 +  val get_const_id: string -> codegr -> string * string
    5.39 +  val mk_type_id: string -> string -> codegr -> codegr * (string * string)
    5.40 +  val get_type_id: string -> codegr -> string * string
    5.41    val thyname_of_type: string -> theory -> string
    5.42    val thyname_of_const: string -> theory -> string
    5.43    val rename_terms: term list -> term list
    5.44    val rename_term: term -> term
    5.45    val new_names: term -> string list -> string list
    5.46    val new_name: term -> string -> string
    5.47 +  val if_library: 'a -> 'a -> 'a
    5.48    val get_defn: theory -> deftab -> string -> typ ->
    5.49      ((typ * (string * (term list * term))) * int option) option
    5.50    val is_instance: theory -> typ -> typ -> bool
    5.51 @@ -62,12 +70,18 @@
    5.52    val eta_expand: term -> term list -> int -> term
    5.53    val strip_tname: string -> string
    5.54    val mk_type: bool -> typ -> Pretty.T
    5.55 -  val mk_term_of: theory -> string -> bool -> typ -> Pretty.T
    5.56 -  val mk_gen: theory -> string -> bool -> string list -> string -> typ -> Pretty.T
    5.57 +  val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
    5.58 +  val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
    5.59    val test_fn: (int -> (string * term) list option) ref
    5.60    val test_term: theory -> int -> int -> term -> (string * term) list option
    5.61    val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
    5.62    val mk_deftab: theory -> deftab
    5.63 +  val get_node: codegr -> string -> node
    5.64 +  val add_edge: string * string -> codegr -> codegr
    5.65 +  val add_edge_acyclic: string * string -> codegr -> codegr
    5.66 +  val del_nodes: string list -> codegr -> codegr
    5.67 +  val map_node: string -> (node -> node) -> codegr -> codegr
    5.68 +  val new_node: string * node -> codegr -> codegr
    5.69  end;
    5.70  
    5.71  structure Codegen : CODEGEN =
    5.72 @@ -118,11 +132,23 @@
    5.73  
    5.74  (* code dependency graph *)
    5.75  
    5.76 -type codegr =
    5.77 +type nametab = (string * string) Symtab.table * unit Symtab.table;
    5.78 +
    5.79 +fun merge_nametabs ((tab, used), (tab', used')) =
    5.80 +  (Symtab.merge op = (tab, tab'), Symtab.merge op = (used, used'));
    5.81 +
    5.82 +type node =
    5.83    (exn option *    (* slot for arbitrary data *)
    5.84     string *        (* name of structure containing piece of code *)
    5.85 -   string)         (* piece of code *)
    5.86 -  Graph.T;
    5.87 +   string);        (* piece of code *)
    5.88 +
    5.89 +type codegr =
    5.90 +  node Graph.T *
    5.91 +  (nametab *       (* table for assigned constant names *)
    5.92 +   nametab);       (* table for assigned type names *)
    5.93 +
    5.94 +val emptygr : codegr = (Graph.empty,
    5.95 +  ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)));
    5.96  
    5.97  (* type of code generators *)
    5.98  
    5.99 @@ -131,7 +157,7 @@
   5.100    deftab ->    (* definition table (for efficiency) *)
   5.101    codegr ->    (* code dependency graph *)
   5.102    string ->    (* node name of caller (for recording dependencies) *)
   5.103 -  string ->    (* theory name of caller (for modular code generation) *)
   5.104 +  string ->    (* module name of caller (for modular code generation) *)
   5.105    bool ->      (* whether to parenthesize generated expression *)
   5.106    'a ->        (* item to generate code from *)
   5.107    (codegr * Pretty.T) option;
   5.108 @@ -175,27 +201,29 @@
   5.109       types : (string * (typ mixfix list * (string * string) list)) list,
   5.110       attrs: (string * (Args.T list -> theory attribute * Args.T list)) list,
   5.111       preprocs: (stamp * (theory -> thm list -> thm list)) list,
   5.112 +     modules: codegr Symtab.table,
   5.113       test_params: test_params};
   5.114  
   5.115    val empty =
   5.116      {codegens = [], tycodegens = [], consts = [], types = [], attrs = [],
   5.117 -     preprocs = [], test_params = default_test_params};
   5.118 +     preprocs = [], modules = Symtab.empty, test_params = default_test_params};
   5.119    val copy = I;
   5.120    val extend = I;
   5.121  
   5.122    fun merge _
   5.123      ({codegens = codegens1, tycodegens = tycodegens1,
   5.124        consts = consts1, types = types1, attrs = attrs1,
   5.125 -      preprocs = preprocs1, test_params = test_params1},
   5.126 +      preprocs = preprocs1, modules = modules1, test_params = test_params1},
   5.127       {codegens = codegens2, tycodegens = tycodegens2,
   5.128        consts = consts2, types = types2, attrs = attrs2,
   5.129 -      preprocs = preprocs2, test_params = test_params2}) =
   5.130 +      preprocs = preprocs2, modules = modules2, test_params = test_params2}) =
   5.131      {codegens = merge_alists' codegens1 codegens2,
   5.132       tycodegens = merge_alists' tycodegens1 tycodegens2,
   5.133       consts = merge_alists consts1 consts2,
   5.134       types = merge_alists types1 types2,
   5.135       attrs = merge_alists attrs1 attrs2,
   5.136       preprocs = merge_alists' preprocs1 preprocs2,
   5.137 +     modules = Symtab.merge (K true) (modules1, modules2),
   5.138       test_params = merge_test_params test_params1 test_params2};
   5.139  
   5.140    fun print _ ({codegens, tycodegens, ...} : T) =
   5.141 @@ -213,33 +241,48 @@
   5.142  fun get_test_params thy = #test_params (CodegenData.get thy);
   5.143  
   5.144  fun map_test_params f thy =
   5.145 -  let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
   5.146 +  let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   5.147      CodegenData.get thy;
   5.148    in CodegenData.put {codegens = codegens, tycodegens = tycodegens,
   5.149      consts = consts, types = types, attrs = attrs, preprocs = preprocs,
   5.150 -    test_params = f test_params} thy
   5.151 +    modules = modules, test_params = f test_params} thy
   5.152 +  end;
   5.153 +
   5.154 +
   5.155 +(**** access modules ****)
   5.156 +
   5.157 +fun get_modules thy = #modules (CodegenData.get thy);
   5.158 +
   5.159 +fun map_modules f thy =
   5.160 +  let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   5.161 +    CodegenData.get thy;
   5.162 +  in CodegenData.put {codegens = codegens, tycodegens = tycodegens,
   5.163 +    consts = consts, types = types, attrs = attrs, preprocs = preprocs,
   5.164 +    modules = f modules, test_params = test_params} thy
   5.165    end;
   5.166  
   5.167  
   5.168  (**** add new code generators to theory ****)
   5.169  
   5.170  fun add_codegen name f thy =
   5.171 -  let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
   5.172 +  let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   5.173      CodegenData.get thy
   5.174    in (case assoc (codegens, name) of
   5.175        NONE => CodegenData.put {codegens = (name, f) :: codegens,
   5.176          tycodegens = tycodegens, consts = consts, types = types,
   5.177 -        attrs = attrs, preprocs = preprocs, test_params = test_params} thy
   5.178 +        attrs = attrs, preprocs = preprocs, modules = modules,
   5.179 +        test_params = test_params} thy
   5.180      | SOME _ => error ("Code generator " ^ name ^ " already declared"))
   5.181    end;
   5.182  
   5.183  fun add_tycodegen name f thy =
   5.184 -  let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
   5.185 +  let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   5.186      CodegenData.get thy
   5.187    in (case assoc (tycodegens, name) of
   5.188        NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens,
   5.189          codegens = codegens, consts = consts, types = types,
   5.190 -        attrs = attrs, preprocs = preprocs, test_params = test_params} thy
   5.191 +        attrs = attrs, preprocs = preprocs, modules = modules,
   5.192 +        test_params = test_params} thy
   5.193      | SOME _ => error ("Code generator " ^ name ^ " already declared"))
   5.194    end;
   5.195  
   5.196 @@ -247,13 +290,13 @@
   5.197  (**** code attribute ****)
   5.198  
   5.199  fun add_attribute name att thy =
   5.200 -  let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
   5.201 +  let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   5.202      CodegenData.get thy
   5.203    in (case assoc (attrs, name) of
   5.204        NONE => CodegenData.put {tycodegens = tycodegens,
   5.205          codegens = codegens, consts = consts, types = types,
   5.206          attrs = if name = "" then attrs @ [(name, att)] else (name, att) :: attrs,
   5.207 -        preprocs = preprocs,
   5.208 +        preprocs = preprocs, modules = modules,
   5.209          test_params = test_params} thy
   5.210      | SOME _ => error ("Code attribute " ^ name ^ " already declared"))
   5.211    end;
   5.212 @@ -273,12 +316,12 @@
   5.213  (**** preprocessors ****)
   5.214  
   5.215  fun add_preprocessor p thy =
   5.216 -  let val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
   5.217 +  let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   5.218      CodegenData.get thy
   5.219    in CodegenData.put {tycodegens = tycodegens,
   5.220      codegens = codegens, consts = consts, types = types,
   5.221      attrs = attrs, preprocs = (stamp (), p) :: preprocs,
   5.222 -    test_params = test_params} thy
   5.223 +    modules = modules, test_params = test_params} thy
   5.224    end;
   5.225  
   5.226  fun preprocess thy ths =
   5.227 @@ -302,7 +345,7 @@
   5.228  
   5.229  fun gen_assoc_consts prep_type xs thy = Library.foldl (fn (thy, (s, tyopt, syn)) =>
   5.230    let
   5.231 -    val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
   5.232 +    val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   5.233        CodegenData.get thy;
   5.234      val cname = Sign.intern_const thy s;
   5.235    in
   5.236 @@ -320,7 +363,7 @@
   5.237                 tycodegens = tycodegens,
   5.238                 consts = ((cname, T'), syn) :: consts,
   5.239                 types = types, attrs = attrs, preprocs = preprocs,
   5.240 -               test_params = test_params} thy
   5.241 +               modules = modules, test_params = test_params} thy
   5.242             | SOME _ => error ("Constant " ^ cname ^ " already associated with code"))
   5.243           end
   5.244       | _ => error ("Not a constant: " ^ s))
   5.245 @@ -334,7 +377,7 @@
   5.246  
   5.247  fun assoc_types xs thy = Library.foldl (fn (thy, (s, syn)) =>
   5.248    let
   5.249 -    val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
   5.250 +    val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} =
   5.251        CodegenData.get thy;
   5.252      val tc = Sign.intern_type thy s
   5.253    in
   5.254 @@ -342,7 +385,7 @@
   5.255         NONE => CodegenData.put {codegens = codegens,
   5.256           tycodegens = tycodegens, consts = consts,
   5.257           types = (tc, syn) :: types, attrs = attrs,
   5.258 -         preprocs = preprocs, test_params = test_params} thy
   5.259 +         preprocs = preprocs, modules = modules, test_params = test_params} thy
   5.260       | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
   5.261    end) (thy, xs);
   5.262  
   5.263 @@ -377,40 +420,70 @@
   5.264      if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s'
   5.265    end;
   5.266  
   5.267 -fun extrn thy f thyname s =
   5.268 +fun mk_long_id (p as (tab, used)) module s =
   5.269    let
   5.270 -    val xs = NameSpace.unpack s;
   5.271 -    val s' = setmp NameSpace.long_names false (setmp NameSpace.short_names false
   5.272 -      (setmp NameSpace.unique_names true (f thy))) s;
   5.273 -    val xs' = NameSpace.unpack s'
   5.274 -  in
   5.275 -    if "modular" mem !mode andalso length xs = length xs' andalso hd xs' = thyname
   5.276 -    then NameSpace.pack (tl xs') else s'
   5.277 +    fun find_name [] = sys_error "mk_long_id"
   5.278 +      | find_name (ys :: yss) =
   5.279 +          let
   5.280 +            val s' = NameSpace.pack ys
   5.281 +            val s'' = NameSpace.append module s'
   5.282 +          in case Symtab.lookup (used, s'') of
   5.283 +              NONE => ((module, s'), (Symtab.update_new ((s, (module, s')), tab),
   5.284 +                Symtab.update_new ((s'', ()), used)))
   5.285 +            | SOME _ => find_name yss
   5.286 +          end
   5.287 +  in case Symtab.lookup (tab, s) of
   5.288 +      NONE => find_name (Library.suffixes1 (NameSpace.unpack s))
   5.289 +    | SOME name => (name, p)
   5.290    end;
   5.291  
   5.292 -(* thyname:  theory name for caller                                        *)
   5.293 -(* thyname': theory name for callee                                        *)
   5.294 -(* if caller and callee reside in different theories, use qualified access *)
   5.295 +(* module:  module name for caller                                        *)
   5.296 +(* module': module name for callee                                        *)
   5.297 +(* if caller and callee reside in different modules, use qualified access *)
   5.298  
   5.299 -fun mk_const_id thy thyname thyname' s =
   5.300 +fun mk_qual_id module (module', s) =
   5.301 +  if module = module' orelse module' = "" then s else module' ^ "." ^ s;
   5.302 +
   5.303 +fun mk_const_id module cname (gr, (tab1, tab2)) =
   5.304    let
   5.305 -    val s' = mk_id (extrn thy Sign.extern_const thyname' s);
   5.306 +    val ((module, s), tab1') = mk_long_id tab1 module cname
   5.307 +    val s' = mk_id s;
   5.308      val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s'
   5.309 -  in
   5.310 -    if "modular" mem !mode andalso thyname <> thyname' andalso thyname' <> ""
   5.311 -    then thyname' ^ "." ^ s'' else s''
   5.312 -  end;
   5.313 +  in ((gr, (tab1', tab2)), (module, s'')) end;
   5.314  
   5.315 -fun mk_type_id' f thy thyname thyname' s =
   5.316 +fun get_const_id cname (gr, (tab1, tab2)) =
   5.317 +  case Symtab.lookup (fst tab1, cname) of
   5.318 +    NONE => error ("get_const_id: no such constant: " ^ quote cname)
   5.319 +  | SOME (module, s) =>
   5.320 +      let
   5.321 +        val s' = mk_id s;
   5.322 +        val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s'
   5.323 +      in (module, s'') end;
   5.324 +
   5.325 +fun mk_type_id module tyname (gr, (tab1, tab2)) =
   5.326    let
   5.327 -    val s' = mk_id (extrn thy Sign.extern_type thyname' s);
   5.328 -    val s'' = f (if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s')
   5.329 -  in
   5.330 -    if "modular" mem !mode andalso thyname <> thyname' andalso thyname' <> ""
   5.331 -    then thyname' ^ "." ^ s'' else s''
   5.332 -  end;
   5.333 +    val ((module, s), tab2') = mk_long_id tab2 module tyname
   5.334 +    val s' = mk_id s;
   5.335 +    val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s'
   5.336 +  in ((gr, (tab1, tab2')), (module, s'')) end;
   5.337  
   5.338 -val mk_type_id = mk_type_id' I;
   5.339 +fun get_type_id tyname (gr, (tab1, tab2)) =
   5.340 +  case Symtab.lookup (fst tab2, tyname) of
   5.341 +    NONE => error ("get_type_id: no such type: " ^ quote tyname)
   5.342 +  | SOME (module, s) =>
   5.343 +      let
   5.344 +        val s' = mk_id s;
   5.345 +        val s'' = if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s'
   5.346 +      in (module, s'') end;
   5.347 +
   5.348 +fun get_type_id' f tyname tab = apsnd f (get_type_id tyname tab);
   5.349 +
   5.350 +fun get_node (gr, x) k = Graph.get_node gr k;
   5.351 +fun add_edge e (gr, x) = (Graph.add_edge e gr, x);
   5.352 +fun add_edge_acyclic e (gr, x) = (Graph.add_edge_acyclic e gr, x);
   5.353 +fun del_nodes ks (gr, x) = (Graph.del_nodes ks gr, x);
   5.354 +fun map_node k f (gr, x) = (Graph.map_node k f gr, x);
   5.355 +fun new_node p (gr, x) = (Graph.new_node p gr, x);
   5.356  
   5.357  fun theory_of_type s thy = 
   5.358    if Sign.declared_tyname thy s
   5.359 @@ -503,18 +576,19 @@
   5.360  
   5.361  (**** invoke suitable code generator for term / type ****)
   5.362  
   5.363 -fun invoke_codegen thy defs dep thyname brack (gr, t) = (case get_first
   5.364 -   (fn (_, f) => f thy defs gr dep thyname brack t) (#codegens (CodegenData.get thy)) of
   5.365 -      NONE => error ("Unable to generate code for term:\n" ^
   5.366 -        Sign.string_of_term thy t ^ "\nrequired by:\n" ^
   5.367 -        commas (Graph.all_succs gr [dep]))
   5.368 +fun codegen_error (gr, _) dep s =
   5.369 +  error (s ^ "\nrequired by:\n" ^ commas (Graph.all_succs gr [dep]));
   5.370 +
   5.371 +fun invoke_codegen thy defs dep module brack (gr, t) = (case get_first
   5.372 +   (fn (_, f) => f thy defs gr dep module brack t) (#codegens (CodegenData.get thy)) of
   5.373 +      NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^
   5.374 +        Sign.string_of_term thy t)
   5.375      | SOME x => x);
   5.376  
   5.377 -fun invoke_tycodegen thy defs dep thyname brack (gr, T) = (case get_first
   5.378 -   (fn (_, f) => f thy defs gr dep thyname brack T) (#tycodegens (CodegenData.get thy)) of
   5.379 -      NONE => error ("Unable to generate code for type:\n" ^
   5.380 -        Sign.string_of_typ thy T ^ "\nrequired by:\n" ^
   5.381 -        commas (Graph.all_succs gr [dep]))
   5.382 +fun invoke_tycodegen thy defs dep module brack (gr, T) = (case get_first
   5.383 +   (fn (_, f) => f thy defs gr dep module brack T) (#tycodegens (CodegenData.get thy)) of
   5.384 +      NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^
   5.385 +        Sign.string_of_typ thy T)
   5.386      | SOME x => x);
   5.387  
   5.388  
   5.389 @@ -532,7 +606,7 @@
   5.390    | pretty_mixfix module module' (Ignore :: ms) ps qs =
   5.391        pretty_mixfix module module' ms ps qs
   5.392    | pretty_mixfix module module' (Module :: ms) ps qs =
   5.393 -      (if "modular" mem !mode andalso module <> module'
   5.394 +      (if module <> module'
   5.395         then cons (Pretty.str (module' ^ ".")) else I)
   5.396        (pretty_mixfix module module' ms ps qs)
   5.397    | pretty_mixfix module module' (Pretty p :: ms) ps qs =
   5.398 @@ -564,15 +638,17 @@
   5.399  
   5.400  fun new_name t x = hd (new_names t [x]);
   5.401  
   5.402 -fun default_codegen thy defs gr dep thyname brack t =
   5.403 +fun if_library x y = if "library" mem !mode then x else y;
   5.404 +
   5.405 +fun default_codegen thy defs gr dep module brack t =
   5.406    let
   5.407      val (u, ts) = strip_comb t;
   5.408 -    fun codegens brack = foldl_map (invoke_codegen thy defs dep thyname brack)
   5.409 +    fun codegens brack = foldl_map (invoke_codegen thy defs dep module brack)
   5.410    in (case u of
   5.411        Var ((s, i), T) =>
   5.412          let
   5.413            val (gr', ps) = codegens true (gr, ts);
   5.414 -          val (gr'', _) = invoke_tycodegen thy defs dep thyname false (gr', T)
   5.415 +          val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T)
   5.416          in SOME (gr'', mk_app brack (Pretty.str (s ^
   5.417             (if i=0 then "" else string_of_int i))) ps)
   5.418          end
   5.419 @@ -580,7 +656,7 @@
   5.420      | Free (s, T) =>
   5.421          let
   5.422            val (gr', ps) = codegens true (gr, ts);
   5.423 -          val (gr'', _) = invoke_tycodegen thy defs dep thyname false (gr', T)
   5.424 +          val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T)
   5.425          in SOME (gr'', mk_app brack (Pretty.str s) ps) end
   5.426  
   5.427      | Const (s, T) =>
   5.428 @@ -588,60 +664,66 @@
   5.429           SOME (ms, aux) =>
   5.430             let val i = num_args ms
   5.431             in if length ts < i then
   5.432 -               default_codegen thy defs gr dep thyname brack (eta_expand u ts i)
   5.433 +               default_codegen thy defs gr dep module brack (eta_expand u ts i)
   5.434               else
   5.435                 let
   5.436                   val (ts1, ts2) = args_of ms ts;
   5.437                   val (gr1, ps1) = codegens false (gr, ts1);
   5.438                   val (gr2, ps2) = codegens true (gr1, ts2);
   5.439                   val (gr3, ps3) = codegens false (gr2, quotes_of ms);
   5.440 -                 val (thyname', suffix) = (case get_defn thy defs s T of
   5.441 -                     NONE => (thyname_of_const s thy, "")
   5.442 -                   | SOME ((U, (thyname', _)), NONE) => (thyname', "")
   5.443 -                   | SOME ((U, (thyname', _)), SOME i) =>
   5.444 -                       (thyname', "_def" ^ string_of_int i));
   5.445 +                 val (module', suffix) = (case get_defn thy defs s T of
   5.446 +                     NONE => (if_library (thyname_of_const s thy) module, "")
   5.447 +                   | SOME ((U, (module', _)), NONE) =>
   5.448 +                       (if_library module' module, "")
   5.449 +                   | SOME ((U, (module', _)), SOME i) =>
   5.450 +                       (if_library module' module, " def" ^ string_of_int i));
   5.451                   val node_id = s ^ suffix;
   5.452 -                 val p = mk_app brack (Pretty.block
   5.453 -                   (pretty_mixfix thyname thyname' ms ps1 ps3)) ps2
   5.454 -               in SOME (case try (Graph.get_node gr3) node_id of
   5.455 +                 fun p module' = mk_app brack (Pretty.block
   5.456 +                   (pretty_mixfix module module' ms ps1 ps3)) ps2
   5.457 +               in SOME (case try (get_node gr3) node_id of
   5.458                     NONE => (case get_aux_code aux of
   5.459 -                       [] => (gr3, p)
   5.460 -                     | xs => (Graph.add_edge (node_id, dep) (Graph.new_node
   5.461 -                         (node_id, (NONE, thyname', space_implode "\n" xs ^ "\n")) gr3), p))
   5.462 -                 | SOME _ => (Graph.add_edge (node_id, dep) gr3, p))
   5.463 +                       [] => (gr3, p module)
   5.464 +                     | xs => (add_edge (node_id, dep) (new_node
   5.465 +                         (node_id, (NONE, module', space_implode "\n" xs ^ "\n")) gr3),
   5.466 +                           p module'))
   5.467 +                 | SOME (_, module'', _) =>
   5.468 +                     (add_edge (node_id, dep) gr3, p module''))
   5.469                 end
   5.470             end
   5.471         | NONE => (case get_defn thy defs s T of
   5.472             NONE => NONE
   5.473 -         | SOME ((U, (thyname', (args, rhs))), k) =>
   5.474 +         | SOME ((U, (thyname, (args, rhs))), k) =>
   5.475               let
   5.476 -               val suffix = (case k of NONE => "" | SOME i => "_def" ^ string_of_int i);
   5.477 +               val module' = if_library thyname module;
   5.478 +               val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i);
   5.479                 val node_id = s ^ suffix;
   5.480 -               val def_id = mk_const_id thy thyname' thyname' s ^ suffix;
   5.481 -               val call_id = mk_const_id thy thyname thyname' s ^ suffix;
   5.482 -               val (gr', ps) = codegens true (gr, ts);
   5.483 -             in
   5.484 -               SOME (Graph.add_edge (node_id, dep) gr' handle Graph.UNDEF _ =>
   5.485 -                 let
   5.486 -                   val _ = message ("expanding definition of " ^ s);
   5.487 -                   val (Ts, _) = strip_type T;
   5.488 -                   val (args', rhs') =
   5.489 -                     if not (null args) orelse null Ts then (args, rhs) else
   5.490 -                       let val v = Free (new_name rhs "x", hd Ts)
   5.491 -                       in ([v], betapply (rhs, v)) end;
   5.492 -                   val (gr1, p) = invoke_codegen thy defs node_id thyname' false
   5.493 -                     (Graph.add_edge (node_id, dep)
   5.494 -                        (Graph.new_node (node_id, (NONE, "", "")) gr'), rhs');
   5.495 -                   val (gr2, xs) = codegens false (gr1, args');
   5.496 -                   val (gr3, _) = invoke_tycodegen thy defs dep thyname false (gr2, T);
   5.497 -                   val (gr4, ty) = invoke_tycodegen thy defs node_id thyname' false (gr3, U);
   5.498 -                 in Graph.map_node node_id (K (NONE, thyname', Pretty.string_of
   5.499 -                   (Pretty.block (separate (Pretty.brk 1)
   5.500 -                     (if null args' then
   5.501 -                        [Pretty.str ("val " ^ def_id ^ " :"), ty]
   5.502 -                      else Pretty.str ("fun " ^ def_id) :: xs) @
   5.503 -                    [Pretty.str " =", Pretty.brk 1, p, Pretty.str ";"])) ^ "\n\n")) gr4
   5.504 -                 end, mk_app brack (Pretty.str call_id) ps)
   5.505 +               val (gr', (ps, def_id)) = codegens true (gr, ts) |>>>
   5.506 +                 mk_const_id module' (s ^ suffix);
   5.507 +               val p = mk_app brack (Pretty.str (mk_qual_id module def_id)) ps
   5.508 +             in SOME (case try (get_node gr') node_id of
   5.509 +                 NONE =>
   5.510 +                   let
   5.511 +                     val _ = message ("expanding definition of " ^ s);
   5.512 +                     val (Ts, _) = strip_type T;
   5.513 +                     val (args', rhs') =
   5.514 +                       if not (null args) orelse null Ts then (args, rhs) else
   5.515 +                         let val v = Free (new_name rhs "x", hd Ts)
   5.516 +                         in ([v], betapply (rhs, v)) end;
   5.517 +                     val (gr1, p') = invoke_codegen thy defs node_id module' false
   5.518 +                       (add_edge (node_id, dep)
   5.519 +                          (new_node (node_id, (NONE, "", "")) gr'), rhs');
   5.520 +                     val (gr2, xs) = codegens false (gr1, args');
   5.521 +                     val (gr3, _) = invoke_tycodegen thy defs dep module false (gr2, T);
   5.522 +                     val (gr4, ty) = invoke_tycodegen thy defs node_id module' false (gr3, U);
   5.523 +                   in (map_node node_id (K (NONE, module', Pretty.string_of
   5.524 +                       (Pretty.block (separate (Pretty.brk 1)
   5.525 +                         (if null args' then
   5.526 +                            [Pretty.str ("val " ^ snd def_id ^ " :"), ty]
   5.527 +                          else Pretty.str ("fun " ^ snd def_id) :: xs) @
   5.528 +                        [Pretty.str " =", Pretty.brk 1, p', Pretty.str ";"])) ^ "\n\n")) gr4,
   5.529 +                     p)
   5.530 +                   end
   5.531 +               | SOME _ => (add_edge (node_id, dep) gr', p))
   5.532               end))
   5.533  
   5.534      | Abs _ =>
   5.535 @@ -650,7 +732,7 @@
   5.536          val t = strip_abs_body u
   5.537          val bs' = new_names t bs;
   5.538          val (gr1, ps) = codegens true (gr, ts);
   5.539 -        val (gr2, p) = invoke_codegen thy defs dep thyname false
   5.540 +        val (gr2, p) = invoke_codegen thy defs dep module false
   5.541            (gr1, subst_bounds (map Free (rev (bs' ~~ Ts)), t));
   5.542        in
   5.543          SOME (gr2, mk_app brack (Pretty.block (Pretty.str "(" :: pretty_fn bs' p @
   5.544 @@ -660,30 +742,33 @@
   5.545      | _ => NONE)
   5.546    end;
   5.547  
   5.548 -fun default_tycodegen thy defs gr dep thyname brack (TVar ((s, i), _)) =
   5.549 +fun default_tycodegen thy defs gr dep module brack (TVar ((s, i), _)) =
   5.550        SOME (gr, Pretty.str (s ^ (if i = 0 then "" else string_of_int i)))
   5.551 -  | default_tycodegen thy defs gr dep thyname brack (TFree (s, _)) =
   5.552 +  | default_tycodegen thy defs gr dep module brack (TFree (s, _)) =
   5.553        SOME (gr, Pretty.str s)
   5.554 -  | default_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) =
   5.555 +  | default_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
   5.556        (case assoc (#types (CodegenData.get thy), s) of
   5.557           NONE => NONE
   5.558         | SOME (ms, aux) =>
   5.559             let
   5.560               val (gr', ps) = foldl_map
   5.561 -               (invoke_tycodegen thy defs dep thyname false)
   5.562 +               (invoke_tycodegen thy defs dep module false)
   5.563                 (gr, fst (args_of ms Ts));
   5.564               val (gr'', qs) = foldl_map
   5.565 -               (invoke_tycodegen thy defs dep thyname false)
   5.566 +               (invoke_tycodegen thy defs dep module false)
   5.567                 (gr', quotes_of ms);
   5.568 -             val thyname' = thyname_of_type s thy;
   5.569 +             val module' = if_library (thyname_of_type s thy) module;
   5.570               val node_id = s ^ " (type)";
   5.571 -             val p = Pretty.block (pretty_mixfix thyname thyname' ms ps qs)
   5.572 -           in SOME (case try (Graph.get_node gr'') node_id of
   5.573 +             fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs)
   5.574 +           in SOME (case try (get_node gr'') node_id of
   5.575                 NONE => (case get_aux_code aux of
   5.576 -                   [] => (gr'', p)
   5.577 -                 | xs => (Graph.add_edge (node_id, dep) (Graph.new_node
   5.578 -                     (node_id, (NONE, thyname', space_implode "\n" xs ^ "\n")) gr''), p))
   5.579 -             | SOME _ => (Graph.add_edge (node_id, dep) gr'', p))
   5.580 +                   [] => (gr'', p module')
   5.581 +                 | xs => (fst (mk_type_id module' s
   5.582 +                       (add_edge (node_id, dep) (new_node (node_id,
   5.583 +                         (NONE, module', space_implode "\n" xs ^ "\n")) gr''))),
   5.584 +                     p module'))
   5.585 +             | SOME (_, module'', _) =>
   5.586 +                 (add_edge (node_id, dep) gr'', p module''))
   5.587             end);
   5.588  
   5.589  val _ = Context.add_setup
   5.590 @@ -696,10 +781,12 @@
   5.591  fun add_to_module name s ms =
   5.592    overwrite (ms, (name, the (assoc (ms, name)) ^ s));
   5.593  
   5.594 -fun output_code gr xs =
   5.595 +fun output_code gr module xs =
   5.596    let
   5.597 -    val code =
   5.598 -      map (fn s => (s, Graph.get_node gr s)) (rev (Graph.all_preds gr xs))
   5.599 +    val code = List.mapPartial (fn s =>
   5.600 +      let val c as (_, module', _) = Graph.get_node gr s
   5.601 +      in if module = "" orelse module = module' then SOME (s, c) else NONE end)
   5.602 +        (rev (Graph.all_preds gr xs));
   5.603      fun string_of_cycle (a :: b :: cs) =
   5.604            let val SOME (x, y) = get_first (fn (x, (_, a', _)) =>
   5.605              if a = a' then Option.map (pair x)
   5.606 @@ -709,43 +796,63 @@
   5.607            in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end
   5.608        | string_of_cycle _ = ""
   5.609    in
   5.610 -    if "modular" mem !mode then
   5.611 +    if module = "" then
   5.612        let
   5.613          val modules = distinct (map (#2 o snd) code);
   5.614          val mod_gr = foldr (uncurry Graph.add_edge_acyclic)
   5.615            (foldr (uncurry (Graph.new_node o rpair ())) Graph.empty modules)
   5.616 -          (List.concat (map (fn (s, (_, thyname, _)) => map (pair thyname)
   5.617 -            (filter_out (equal thyname) (map (#2 o Graph.get_node gr)
   5.618 +          (List.concat (map (fn (s, (_, module, _)) => map (pair module)
   5.619 +            (filter_out (equal module) (map (#2 o Graph.get_node gr)
   5.620                (Graph.imm_succs gr s)))) code));
   5.621          val modules' =
   5.622            rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs))
   5.623        in
   5.624 -        foldl (fn ((_, (_, thyname, s)), ms) => add_to_module thyname s ms)
   5.625 +        foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms)
   5.626            (map (rpair "") modules') code
   5.627        end handle Graph.CYCLES (cs :: _) =>
   5.628          error ("Cyclic dependency of modules:\n" ^ commas cs ^
   5.629            "\n" ^ string_of_cycle cs)
   5.630 -    else [("Generated", implode (map (#3 o snd) code))]
   5.631 +    else [(module, implode (map (#3 o snd) code))]
   5.632    end;
   5.633  
   5.634 -fun gen_generate_code prep_term thy =
   5.635 +fun gen_generate_code prep_term thy modules module =
   5.636    setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs =>
   5.637    let
   5.638 +    val _ = assert (module <> "" orelse
   5.639 +        "library" mem !mode andalso forall (equal "" o fst) xs)
   5.640 +      "missing module name";
   5.641 +    val graphs = get_modules thy;
   5.642      val defs = mk_deftab thy;
   5.643 -    val gr = Graph.new_node ("<Top>", (NONE, "Generated", "")) Graph.empty;
   5.644 +    val gr = new_node ("<Top>", (NONE, module, ""))
   5.645 +      (foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) =>
   5.646 +        (Graph.merge (fn ((_, module, _), (_, module', _)) =>
   5.647 +           module = module') (gr, gr'),
   5.648 +         (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr
   5.649 +           (map (fn s => case Symtab.lookup (graphs, s) of
   5.650 +                NONE => error ("Undefined code module: " ^ s)
   5.651 +              | SOME gr => gr) modules))
   5.652 +      handle Graph.DUPS ks => error ("Duplicate code for " ^ commas ks);
   5.653      fun expand (t as Abs _) = t
   5.654        | expand t = (case fastype_of t of
   5.655            Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t);
   5.656      val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s)
   5.657 -      (invoke_codegen thy defs "<Top>" "Generated" false (gr, t)))
   5.658 +      (invoke_codegen thy defs "<Top>" module false (gr, t)))
   5.659          (gr, map (apsnd (expand o prep_term thy)) xs);
   5.660 -    val code =
   5.661 -      space_implode "\n\n" (map (fn (s', p) => Pretty.string_of (Pretty.block
   5.662 -        [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"])) ps) ^
   5.663 -      "\n\n"
   5.664 +    val code = List.mapPartial
   5.665 +      (fn ("", _) => NONE
   5.666 +        | (s', p) => SOME (Pretty.string_of (Pretty.block
   5.667 +          [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"]))) ps;
   5.668 +    val code' = space_implode "\n\n" code ^ "\n\n";
   5.669 +    val code'' =
   5.670 +      List.mapPartial (fn (name, s) =>
   5.671 +          if "library" mem !mode andalso name = module andalso null code
   5.672 +          then NONE
   5.673 +          else SOME (name, mk_struct name s))
   5.674 +        ((if null code then I
   5.675 +          else add_to_module module code')
   5.676 +           (output_code (fst gr') (if_library "" module) ["<Top>"]))
   5.677    in
   5.678 -    map (fn (name, s) => (name, mk_struct name s))
   5.679 -      (add_to_module "Generated" code (output_code gr' ["<Top>"]))
   5.680 +    (code'', del_nodes ["<Top>"] gr')
   5.681    end));
   5.682  
   5.683  val generate_code_i = gen_generate_code (K I);
   5.684 @@ -768,28 +875,27 @@
   5.685        [Pretty.str "Type", Pretty.brk 1, Pretty.str ("(\"" ^ s ^ "\","),
   5.686         Pretty.brk 1, pretty_list (map (mk_type false) Ts), Pretty.str ")"]);
   5.687  
   5.688 -fun mk_term_of thy thyname p (TVar ((s, i), _)) = Pretty.str
   5.689 +fun mk_term_of gr module p (TVar ((s, i), _)) = Pretty.str
   5.690        (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F")
   5.691 -  | mk_term_of thy thyname p (TFree (s, _)) = Pretty.str (strip_tname s ^ "F")
   5.692 -  | mk_term_of thy thyname p (Type (s, Ts)) = (if p then parens else I)
   5.693 +  | mk_term_of gr module p (TFree (s, _)) = Pretty.str (strip_tname s ^ "F")
   5.694 +  | mk_term_of gr module p (Type (s, Ts)) = (if p then parens else I)
   5.695        (Pretty.block (separate (Pretty.brk 1)
   5.696 -        (Pretty.str (mk_type_id' (fn s' => "term_of_" ^ s')
   5.697 -          thy thyname (thyname_of_type s thy) s) ::
   5.698 +        (Pretty.str (mk_qual_id module
   5.699 +          (get_type_id' (fn s' => "term_of_" ^ s') s gr)) ::
   5.700          List.concat (map (fn T =>
   5.701 -          [mk_term_of thy thyname true T, mk_type true T]) Ts))));
   5.702 +          [mk_term_of gr module true T, mk_type true T]) Ts))));
   5.703  
   5.704  
   5.705  (**** Test data generators ****)
   5.706  
   5.707 -fun mk_gen thy thyname p xs a (TVar ((s, i), _)) = Pretty.str
   5.708 +fun mk_gen gr module p xs a (TVar ((s, i), _)) = Pretty.str
   5.709        (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G")
   5.710 -  | mk_gen thy thyname p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G")
   5.711 -  | mk_gen thy thyname p xs a (Type (s, Ts)) = (if p then parens else I)
   5.712 +  | mk_gen gr module p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G")
   5.713 +  | mk_gen gr module p xs a (Type (s, Ts)) = (if p then parens else I)
   5.714        (Pretty.block (separate (Pretty.brk 1)
   5.715 -        (Pretty.str (mk_type_id' (fn s' => "gen_" ^ s')
   5.716 -          thy thyname (thyname_of_type s thy) s ^
   5.717 +        (Pretty.str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') s gr) ^
   5.718            (if s mem xs then "'" else "")) ::
   5.719 -         map (mk_gen thy thyname true xs a) Ts @
   5.720 +         map (mk_gen gr module true xs a) Ts @
   5.721           (if s mem xs then [Pretty.str a] else []))));
   5.722  
   5.723  val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE);
   5.724 @@ -802,17 +908,17 @@
   5.725        "Term to be tested contains schematic variables";
   5.726      val frees = map dest_Free (term_frees t);
   5.727      val szname = variant (map fst frees) "i";
   5.728 -    val code = space_implode "\n" (map snd
   5.729 -      (setmp mode ["term_of", "test"] (generate_code_i thy)
   5.730 -        [("testf", list_abs_free (frees, t))]));
   5.731 -    val s = "structure TestTerm =\nstruct\n\n" ^ code ^
   5.732 +    val (code, gr) = setmp mode ["term_of", "test"]
   5.733 +      (generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))];
   5.734 +    val s = "structure TestTerm =\nstruct\n\n" ^
   5.735 +      space_implode "\n" (map snd code) ^
   5.736        "\nopen Generated;\n\n" ^ Pretty.string_of
   5.737          (Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
   5.738            Pretty.brk 1, Pretty.str ("(fn " ^ szname ^ " =>"), Pretty.brk 1,
   5.739            Pretty.blk (0, [Pretty.str "let", Pretty.brk 1,
   5.740              Pretty.blk (0, separate Pretty.fbrk (map (fn (s, T) =>
   5.741                Pretty.block [Pretty.str ("val " ^ mk_id s ^ " ="), Pretty.brk 1,
   5.742 -              mk_gen thy "" false [] "" T, Pretty.brk 1,
   5.743 +              mk_gen gr "Generated" false [] "" T, Pretty.brk 1,
   5.744                Pretty.str (szname ^ ";")]) frees)),
   5.745              Pretty.brk 1, Pretty.str "in", Pretty.brk 1,
   5.746              Pretty.block [Pretty.str "if ",
   5.747 @@ -823,7 +929,7 @@
   5.748                  List.concat (separate [Pretty.str ",", Pretty.brk 1]
   5.749                    (map (fn (s, T) => [Pretty.block
   5.750                      [Pretty.str ("(" ^ Library.quote (Symbol.escape s) ^ ","), Pretty.brk 1,
   5.751 -                     mk_app false (mk_term_of thy "" false T)
   5.752 +                     mk_app false (mk_term_of gr "Generated" false T)
   5.753                         [Pretty.str (mk_id s)], Pretty.str ")"]]) frees)) @
   5.754                    [Pretty.str "]"])]],
   5.755              Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
   5.756 @@ -898,12 +1004,12 @@
   5.757  
   5.758  structure P = OuterParse and K = OuterKeyword;
   5.759  
   5.760 -fun strip_newlines s = implode (fst (take_suffix (equal "\n")
   5.761 -  (snd (take_prefix (equal "\n") (explode s))))) ^ "\n";
   5.762 +fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ")
   5.763 +  (snd (take_prefix (equal "\n" orf equal " ") (explode s))))) ^ "\n";
   5.764  
   5.765  val parse_attach = Scan.repeat (P.$$$ "attach" |--
   5.766    Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" --
   5.767 -    (P.verbatim >> strip_newlines));
   5.768 +    (P.verbatim >> strip_whitespace));
   5.769  
   5.770  val assoc_typeP =
   5.771    OuterSyntax.command "types_code"
   5.772 @@ -924,24 +1030,44 @@
   5.773           (term_of o read_cterm thy o rpair TypeInfer.logicT) mfx, aux)))
   5.774             xs) thy)));
   5.775  
   5.776 -val generate_codeP =
   5.777 -  OuterSyntax.command "generate_code" "generates code for terms" K.thy_decl
   5.778 -    (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
   5.779 -     Scan.optional (P.$$$ "[" |-- P.enum "," P.xname --| P.$$$ "]") (!mode) --
   5.780 -     Scan.repeat1 (P.name --| P.$$$ "=" -- P.term) >>
   5.781 -     (fn ((opt_fname, mode'), xs) => Toplevel.theory (fn thy =>
   5.782 -       let val code = setmp mode mode' (generate_code thy) xs
   5.783 -       in ((case opt_fname of
   5.784 -           NONE => use_text Context.ml_output false
   5.785 -             (space_implode "\n" (map snd code) ^ "\nopen Generated;\n")
   5.786 -         | SOME fname =>
   5.787 -             if "modular" mem mode' then
   5.788 -               app (fn (name, s) => File.write
   5.789 -                   (Path.append (Path.unpack fname) (Path.basic (name ^ ".ML"))) s)
   5.790 -                 (("ROOT", implode (map (fn (name, _) =>
   5.791 -                     "use \"" ^ name ^ ".ML\";\n") code)) :: code)
   5.792 -             else File.write (Path.unpack fname) (snd (hd code))); thy)
   5.793 -       end)));
   5.794 +fun parse_code lib =
   5.795 +  Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) --
   5.796 +  (if lib then Scan.optional P.name "" else P.name) --
   5.797 +  Scan.option (P.$$$ "file" |-- P.name) --
   5.798 +  (if lib then Scan.succeed []
   5.799 +   else Scan.optional (P.$$$ "imports" |-- Scan.repeat1 P.name) []) --|
   5.800 +  P.$$$ "contains" --
   5.801 +  (   Scan.repeat1 (P.name --| P.$$$ "=" -- P.term)
   5.802 +   || Scan.repeat1 (P.term >> pair "")) >>
   5.803 +  (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
   5.804 +     let
   5.805 +       val mode'' = if lib then "library" ins (mode' \ "library")
   5.806 +         else mode' \ "library";
   5.807 +       val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs
   5.808 +     in ((case opt_fname of
   5.809 +         NONE => use_text Context.ml_output false
   5.810 +           (space_implode "\n" (map snd code))
   5.811 +       | SOME fname =>
   5.812 +           if lib then
   5.813 +             app (fn (name, s) => File.write
   5.814 +                 (Path.append (Path.unpack fname) (Path.basic (name ^ ".ML"))) s)
   5.815 +               (("ROOT", implode (map (fn (name, _) =>
   5.816 +                   "use \"" ^ name ^ ".ML\";\n") code)) :: code)
   5.817 +           else File.write (Path.unpack fname) (snd (hd code)));
   5.818 +           if lib then thy
   5.819 +           else map_modules (fn graphs =>
   5.820 +             Symtab.update ((module, gr), graphs)) thy)
   5.821 +     end));
   5.822 +
   5.823 +val code_libraryP =
   5.824 +  OuterSyntax.command "code_library"
   5.825 +    "generates code for terms (one structure for each theory)" K.thy_decl
   5.826 +    (parse_code true);
   5.827 +
   5.828 +val code_moduleP =
   5.829 +  OuterSyntax.command "code_module"
   5.830 +    "generates code for terms (single structure, incremental)" K.thy_decl
   5.831 +    (parse_code false);
   5.832  
   5.833  val params =
   5.834    [("size", P.nat >> (K o set_size)),
   5.835 @@ -974,9 +1100,9 @@
   5.836            (map (fn f => f (Toplevel.sign_of st))) ps, []))
   5.837          (get_test_params (Toplevel.theory_of st), [])) g st)));
   5.838  
   5.839 -val _ = OuterSyntax.add_keywords ["attach"];
   5.840 +val _ = OuterSyntax.add_keywords ["attach", "file", "contains"];
   5.841  
   5.842  val _ = OuterSyntax.add_parsers
   5.843 -  [assoc_typeP, assoc_constP, generate_codeP, test_paramsP, testP];
   5.844 +  [assoc_typeP, assoc_constP, code_libraryP, code_moduleP, test_paramsP, testP];
   5.845  
   5.846  end;