Adapted to modular code generation.
authorberghofe
Fri Jul 01 14:13:40 2005 +0200 (2005-07-01)
changeset 16645a152d6b21c31
parent 16644 701218c1301c
child 16646 666774b0d1b0
Adapted to modular 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
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Jul 01 14:11:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Jul 01 14:13:40 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 dep gr (descr: DatatypeAux.descr) =
     1.8 +fun add_dt_defs thy defs dep 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,8 @@
    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 (_, (_, _, (cname, _) :: _)) :: _ = descr';
    1.17 -    val dname = mk_const_id sg cname;
    1.18 +    val (_, (tname, _, (dname, _) :: _)) :: _ = descr';
    1.19 +    val thyname = thyname_of_type tname thy;
    1.20  
    1.21      fun mk_dtdef gr prfx [] = (gr, [])
    1.22        | mk_dtdef gr prfx ((_, (tname, dts, cs))::xs) =
    1.23 @@ -59,17 +59,17 @@
    1.24              val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs;
    1.25              val (gr', ps) = foldl_map (fn (gr, (cname, cargs)) =>
    1.26                apsnd (pair cname) (foldl_map
    1.27 -                (invoke_tycodegen thy dname false) (gr, cargs))) (gr, cs');
    1.28 +                (invoke_tycodegen thy defs dname thyname false) (gr, cargs))) (gr, cs');
    1.29              val (gr'', rest) = mk_dtdef gr' "and " xs
    1.30            in
    1.31              (gr'',
    1.32               Pretty.block (Pretty.str prfx ::
    1.33                 (if null tvs then [] else
    1.34                    [mk_tuple (map Pretty.str tvs), Pretty.str " "]) @
    1.35 -               [Pretty.str (mk_type_id sg tname ^ " ="), Pretty.brk 1] @
    1.36 +               [Pretty.str (mk_type_id sg thyname thyname tname ^ " ="), Pretty.brk 1] @
    1.37                 List.concat (separate [Pretty.brk 1, Pretty.str "| "]
    1.38                   (map (fn (cname, ps') => [Pretty.block
    1.39 -                   (Pretty.str (mk_const_id sg cname) ::
    1.40 +                   (Pretty.str (mk_const_id sg thyname thyname cname) ::
    1.41                      (if null ps' then [] else
    1.42                       List.concat ([Pretty.str " of", Pretty.brk 1] ::
    1.43                         separate [Pretty.str " *", Pretty.brk 1]
    1.44 @@ -89,15 +89,16 @@
    1.45                let val args = map (fn i =>
    1.46                  Pretty.str ("x" ^ string_of_int i)) (1 upto length Ts)
    1.47                in ("  | ", Pretty.blk (4,
    1.48 -                [Pretty.str prfx, mk_term_of sg false T, Pretty.brk 1,
    1.49 -                 if null Ts then Pretty.str (mk_const_id sg cname)
    1.50 -                 else parens (Pretty.block [Pretty.str (mk_const_id sg cname),
    1.51 +                [Pretty.str prfx, mk_term_of thy thyname false T, Pretty.brk 1,
    1.52 +                 if null Ts then Pretty.str (mk_const_id sg thyname thyname cname)
    1.53 +                 else parens (Pretty.block
    1.54 +                   [Pretty.str (mk_const_id sg thyname thyname cname),
    1.55                      Pretty.brk 1, mk_tuple args]),
    1.56                   Pretty.str " =", Pretty.brk 1] @
    1.57                   List.concat (separate [Pretty.str " $", Pretty.brk 1]
    1.58                     ([Pretty.str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1,
    1.59                       mk_type false (Ts ---> T), Pretty.str ")"] ::
    1.60 -                    map (fn (x, U) => [Pretty.block [mk_term_of sg false U,
    1.61 +                    map (fn (x, U) => [Pretty.block [mk_term_of thy thyname false U,
    1.62                        Pretty.brk 1, x]]) (args ~~ Ts)))))
    1.63                end) (prfx, cs')
    1.64            in eqs @ rest end;
    1.65 @@ -116,11 +117,11 @@
    1.66  
    1.67              fun mk_constr s b (cname, dts) =
    1.68                let
    1.69 -                val gs = map (fn dt => mk_app false (mk_gen sg false rtnames s
    1.70 +                val gs = map (fn dt => mk_app false (mk_gen thy thyname false rtnames s
    1.71                      (DatatypeAux.typ_of_dtyp descr sorts dt))
    1.72                    [Pretty.str (if b andalso DatatypeAux.is_rec_type dt then "0"
    1.73                       else "j")]) dts;
    1.74 -                val id = mk_const_id sg cname
    1.75 +                val id = mk_const_id sg thyname thyname cname
    1.76                in case gs of
    1.77                    _ :: _ :: _ => Pretty.block
    1.78                      [Pretty.str id, Pretty.brk 1, mk_tuple gs]
    1.79 @@ -135,7 +136,7 @@
    1.80                    [Pretty.str "]"]), Pretty.brk 1, Pretty.str "()"];
    1.81  
    1.82              val gs = map (Pretty.str o suffix "G" o strip_tname) tvs;
    1.83 -            val gen_name = "gen_" ^ mk_type_id sg tname
    1.84 +            val gen_name = "gen_" ^ mk_type_id sg thyname thyname tname
    1.85  
    1.86            in
    1.87              Pretty.blk (4, separate (Pretty.brk 1) 
    1.88 @@ -173,10 +174,10 @@
    1.89          handle Graph.CYCLES _ => gr) handle Graph.UNDEF _ =>
    1.90           let
    1.91             val gr1 = Graph.add_edge (dname, dep)
    1.92 -             (Graph.new_node (dname, (NONE, "")) gr);
    1.93 +             (Graph.new_node (dname, (NONE, "", "")) gr);
    1.94             val (gr2, dtdef) = mk_dtdef gr1 "datatype " descr';
    1.95           in
    1.96 -           Graph.map_node dname (K (NONE,
    1.97 +           Graph.map_node dname (K (NONE, thyname,
    1.98               Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
    1.99                 [Pretty.str ";"])) ^ "\n\n" ^
   1.100               (if "term_of" mem !mode then
   1.101 @@ -187,16 +188,16 @@
   1.102                  Pretty.string_of (Pretty.blk (0, separate Pretty.fbrk
   1.103                    (mk_gen_of_def "fun " descr') @ [Pretty.str ";"])) ^ "\n\n"
   1.104                else ""))) gr2
   1.105 -         end)
   1.106 +         end, thyname)
   1.107    end;
   1.108  
   1.109  
   1.110  (**** case expressions ****)
   1.111  
   1.112 -fun pretty_case thy gr dep brack constrs (c as Const (_, T)) ts =
   1.113 +fun pretty_case thy defs gr dep thyname brack constrs (c as Const (_, T)) ts =
   1.114    let val i = length constrs
   1.115    in if length ts <= i then
   1.116 -       invoke_codegen thy dep brack (gr, eta_expand c ts (i+1))
   1.117 +       invoke_codegen thy defs dep thyname brack (gr, eta_expand c ts (i+1))
   1.118      else
   1.119        let
   1.120          val ts1 = Library.take (i, ts);
   1.121 @@ -212,10 +213,10 @@
   1.122                  val xs = variantlist (replicate j "x", names);
   1.123                  val Us' = Library.take (j, fst (strip_type U));
   1.124                  val frees = map Free (xs ~~ Us');
   1.125 -                val (gr0, cp) = invoke_codegen thy dep false
   1.126 +                val (gr0, cp) = invoke_codegen thy defs dep thyname false
   1.127                    (gr, list_comb (Const (cname, Us' ---> dT), frees));
   1.128                  val t' = Envir.beta_norm (list_comb (t, frees));
   1.129 -                val (gr1, p) = invoke_codegen thy dep false (gr0, t');
   1.130 +                val (gr1, p) = invoke_codegen thy defs dep thyname false (gr0, t');
   1.131                  val (ps, gr2) = pcase gr1 cs ts Us;
   1.132                in
   1.133                  ([Pretty.block [cp, Pretty.str " =>", Pretty.brk 1, p]] :: ps, gr2)
   1.134 @@ -223,8 +224,8 @@
   1.135  
   1.136          val (ps1, gr1) = pcase gr constrs ts1 Ts;
   1.137          val ps = List.concat (separate [Pretty.brk 1, Pretty.str "| "] ps1);
   1.138 -        val (gr2, p) = invoke_codegen thy dep false (gr1, t);
   1.139 -        val (gr3, ps2) = foldl_map (invoke_codegen thy dep true) (gr2, ts2)
   1.140 +        val (gr2, p) = invoke_codegen thy defs dep thyname false (gr1, t);
   1.141 +        val (gr3, ps2) = foldl_map (invoke_codegen thy defs dep thyname true) (gr2, ts2)
   1.142        in (gr3, (if not (null ts2) andalso brack then parens else I)
   1.143          (Pretty.block (separate (Pretty.brk 1)
   1.144            (Pretty.block ([Pretty.str "(case ", p, Pretty.str " of",
   1.145 @@ -235,14 +236,16 @@
   1.146  
   1.147  (**** constructors ****)
   1.148  
   1.149 -fun pretty_constr thy gr dep brack args (c as Const (s, _)) ts =
   1.150 +fun pretty_constr thy defs gr dep thyname brack args (c as Const (s, T)) ts =
   1.151    let val i = length args
   1.152    in if i > 1 andalso length ts < i then
   1.153 -      invoke_codegen thy dep brack (gr, eta_expand c ts i)
   1.154 +      invoke_codegen thy defs dep thyname brack (gr, eta_expand c ts i)
   1.155       else
   1.156         let
   1.157 -         val id = mk_const_id (sign_of thy) s;
   1.158 -         val (gr', ps) = foldl_map (invoke_codegen thy dep (i = 1)) (gr, ts);
   1.159 +         val thyname' = thyname_of_type (fst (dest_Type (body_type T))) thy;
   1.160 +         val id = mk_const_id (sign_of thy) thyname thyname' s;
   1.161 +         val (gr', ps) = foldl_map
   1.162 +           (invoke_codegen thy defs dep thyname (i = 1)) (gr, ts);
   1.163         in (case args of
   1.164            _ :: _ :: _ => (gr', (if brack then parens else I)
   1.165              (Pretty.block [Pretty.str id, Pretty.brk 1, mk_tuple ps]))
   1.166 @@ -253,7 +256,7 @@
   1.167  
   1.168  (**** code generators for terms and types ****)
   1.169  
   1.170 -fun datatype_codegen thy gr dep brack t = (case strip_comb t of
   1.171 +fun datatype_codegen thy defs gr dep thyname brack t = (case strip_comb t of
   1.172     (c as Const (s, T), ts) =>
   1.173         (case find_first (fn (_, {index, descr, case_name, ...}) =>
   1.174           s = case_name orelse
   1.175 @@ -264,28 +267,31 @@
   1.176             if isSome (get_assoc_code thy s T) then NONE else
   1.177             let val SOME (_, _, constrs) = assoc (descr, index)
   1.178             in (case (assoc (constrs, s), strip_type T) of
   1.179 -               (NONE, _) => SOME (pretty_case thy gr dep brack
   1.180 +               (NONE, _) => SOME (pretty_case thy defs gr dep thyname brack
   1.181                   (#3 (valOf (assoc (descr, index)))) c ts)
   1.182 -             | (SOME args, (_, Type _)) => SOME (pretty_constr thy
   1.183 -                 (fst (invoke_tycodegen thy dep false (gr, snd (strip_type T))))
   1.184 -                 dep brack args c ts)
   1.185 +             | (SOME args, (_, Type _)) => SOME (pretty_constr thy defs
   1.186 +                 (fst (invoke_tycodegen thy defs dep thyname false
   1.187 +                    (gr, snd (strip_type T))))
   1.188 +                 dep thyname brack args c ts)
   1.189               | _ => NONE)
   1.190             end)
   1.191   |  _ => NONE);
   1.192  
   1.193 -fun datatype_tycodegen thy gr dep brack (Type (s, Ts)) =
   1.194 +fun datatype_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) =
   1.195        (case Symtab.lookup (DatatypePackage.get_datatypes thy, s) of
   1.196           NONE => NONE
   1.197         | SOME {descr, ...} =>
   1.198             if isSome (get_assoc_type thy s) then NONE else
   1.199 -           let val (gr', ps) = foldl_map
   1.200 -             (invoke_tycodegen thy dep false) (gr, Ts)
   1.201 -           in SOME (add_dt_defs thy dep gr' descr,
   1.202 +           let
   1.203 +             val (gr', ps) = foldl_map
   1.204 +               (invoke_tycodegen thy defs dep thyname false) (gr, Ts);
   1.205 +             val (gr'', thyname') = add_dt_defs thy defs dep gr' descr
   1.206 +           in SOME (gr'',
   1.207               Pretty.block ((if null Ts then [] else
   1.208                 [mk_tuple ps, Pretty.str " "]) @
   1.209 -               [Pretty.str (mk_type_id (sign_of thy) s)]))
   1.210 +               [Pretty.str (mk_type_id (sign_of thy) thyname thyname' s)]))
   1.211             end)
   1.212 -  | datatype_tycodegen _ _ _ _ _ = NONE;
   1.213 +  | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
   1.214  
   1.215  
   1.216  val setup =
     2.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Jul 01 14:11:06 2005 +0200
     2.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Jul 01 14:13:40 2005 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  
     2.5  signature INDUCTIVE_CODEGEN =
     2.6  sig
     2.7 -  val add : theory attribute
     2.8 +  val add : string option -> theory attribute
     2.9    val setup : (theory -> theory) list
    2.10  end;
    2.11  
    2.12 @@ -22,18 +22,20 @@
    2.13  (struct
    2.14    val name = "HOL/inductive_codegen";
    2.15    type T =
    2.16 -    {intros : thm list Symtab.table,
    2.17 +    {intros : (thm * string) list Symtab.table,
    2.18       graph : unit Graph.T,
    2.19 -     eqns : thm list Symtab.table};
    2.20 +     eqns : (thm * string) list Symtab.table};
    2.21    val empty =
    2.22      {intros = Symtab.empty, graph = Graph.empty, eqns = Symtab.empty};
    2.23    val copy = I;
    2.24    val extend = I;
    2.25    fun merge _ ({intros=intros1, graph=graph1, eqns=eqns1},
    2.26      {intros=intros2, graph=graph2, eqns=eqns2}) =
    2.27 -    {intros = Symtab.merge_multi Drule.eq_thm_prop (intros1, intros2),
    2.28 +    {intros = Symtab.merge_multi (Drule.eq_thm_prop o pairself fst)
    2.29 +       (intros1, intros2),
    2.30       graph = Graph.merge (K true) (graph1, graph2),
    2.31 -     eqns = Symtab.merge_multi Drule.eq_thm_prop (eqns1, eqns2)};
    2.32 +     eqns = Symtab.merge_multi (Drule.eq_thm_prop o pairself fst)
    2.33 +       (eqns1, eqns2)};
    2.34    fun print _ _ = ();
    2.35  end);
    2.36  
    2.37 @@ -43,15 +45,19 @@
    2.38  
    2.39  fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
    2.40  
    2.41 -fun add (p as (thy, thm)) =
    2.42 -  let val {intros, graph, eqns} = CodegenData.get thy;
    2.43 +fun add optmod (p as (thy, thm)) =
    2.44 +  let
    2.45 +    val {intros, graph, eqns} = CodegenData.get thy;
    2.46 +    fun thyname_of s = (case optmod of
    2.47 +      NONE => thyname_of_const s thy | SOME s => s);
    2.48    in (case concl_of thm of
    2.49        _ $ (Const ("op :", _) $ _ $ t) => (case head_of t of
    2.50          Const (s, _) =>
    2.51            let val cs = foldr add_term_consts [] (prems_of thm)
    2.52            in (CodegenData.put
    2.53              {intros = Symtab.update ((s,
    2.54 -               getOpt (Symtab.lookup (intros, s), []) @ [thm]), intros),
    2.55 +               getOpt (Symtab.lookup (intros, s), []) @
    2.56 +                 [(thm, thyname_of s)]), intros),
    2.57               graph = foldr (uncurry (Graph.add_edge o pair s))
    2.58                 (Library.foldl add_node (graph, s :: cs)) cs,
    2.59               eqns = eqns} thy, thm)
    2.60 @@ -61,7 +67,8 @@
    2.61          Const (s, _) =>
    2.62            (CodegenData.put {intros = intros, graph = graph,
    2.63               eqns = Symtab.update ((s,
    2.64 -               getOpt (Symtab.lookup (eqns, s), []) @ [thm]), eqns)} thy, thm)
    2.65 +               getOpt (Symtab.lookup (eqns, s), []) @
    2.66 +                 [(thm, thyname_of s)]), eqns)} thy, thm)
    2.67        | _ => (warn thm; p))
    2.68      | _ => (warn thm; p))
    2.69    end;
    2.70 @@ -71,13 +78,17 @@
    2.71    in case Symtab.lookup (intros, s) of
    2.72        NONE => (case InductivePackage.get_inductive thy s of
    2.73          NONE => NONE
    2.74 -      | SOME ({names, ...}, {intrs, ...}) => SOME (names, preprocess thy intrs))
    2.75 +      | SOME ({names, ...}, {intrs, ...}) =>
    2.76 +          SOME (names, thyname_of_const s thy,
    2.77 +            preprocess thy intrs))
    2.78      | SOME _ =>
    2.79 -        let val SOME names = find_first
    2.80 -          (fn xs => s mem xs) (Graph.strong_conn graph)
    2.81 -        in SOME (names, preprocess thy
    2.82 -          (List.concat (map (fn s => valOf (Symtab.lookup (intros, s))) names)))
    2.83 -        end
    2.84 +        let
    2.85 +          val SOME names = find_first
    2.86 +            (fn xs => s mem xs) (Graph.strong_conn graph);
    2.87 +          val intrs = List.concat (map
    2.88 +            (fn s => valOf (Symtab.lookup (intros, s))) names);
    2.89 +          val (_, (_, thyname)) = split_last intrs
    2.90 +        in SOME (names, thyname, preprocess thy (map fst intrs)) end
    2.91    end;
    2.92  
    2.93  
    2.94 @@ -364,26 +375,30 @@
    2.95          else [Pretty.str ")"])))
    2.96    end;
    2.97  
    2.98 -fun modename thy s (iss, is) = space_implode "__"
    2.99 -  (mk_const_id (sign_of thy) s ::
   2.100 +fun strip_spaces s = implode (fst (take_suffix (equal " ") (explode s)));
   2.101 +
   2.102 +fun modename thy thyname thyname' s (iss, is) = space_implode "__"
   2.103 +  (mk_const_id (sign_of thy) thyname thyname' (strip_spaces s) ::
   2.104      map (space_implode "_" o map string_of_int) (List.mapPartial I iss @ [is]));
   2.105  
   2.106 -fun compile_expr thy dep brack (gr, (NONE, t)) =
   2.107 -      apsnd single (invoke_codegen thy dep brack (gr, t))
   2.108 -  | compile_expr _ _ _ (gr, (SOME _, Var ((name, _), _))) =
   2.109 +fun compile_expr thy defs dep thyname brack thynames (gr, (NONE, t)) =
   2.110 +      apsnd single (invoke_codegen thy defs dep thyname brack (gr, t))
   2.111 +  | compile_expr _ _ _ _ _ _ (gr, (SOME _, Var ((name, _), _))) =
   2.112        (gr, [Pretty.str name])
   2.113 -  | compile_expr thy dep brack (gr, (SOME (Mode (mode, ms)), t)) =
   2.114 +  | compile_expr thy defs dep thyname brack thynames (gr, (SOME (Mode (mode, ms)), t)) =
   2.115        let
   2.116          val (Const (name, _), args) = strip_comb t;
   2.117          val (gr', ps) = foldl_map
   2.118 -          (compile_expr thy dep true) (gr, ms ~~ args);
   2.119 +          (compile_expr thy defs dep thyname true thynames) (gr, ms ~~ args);
   2.120        in (gr', (if brack andalso not (null ps) then
   2.121          single o parens o Pretty.block else I)
   2.122            (List.concat (separate [Pretty.brk 1]
   2.123 -            ([Pretty.str (modename thy name mode)] :: ps))))
   2.124 +            ([Pretty.str (modename thy thyname
   2.125 +                (if name = "op =" then ""
   2.126 +                 else the (assoc (thynames, name))) name mode)] :: ps))))
   2.127        end;
   2.128  
   2.129 -fun compile_clause thy gr dep all_vs arg_vs modes (iss, is) (ts, ps) =
   2.130 +fun compile_clause thy defs gr dep thyname all_vs arg_vs modes thynames (iss, is) (ts, ps) =
   2.131    let
   2.132      val modes' = modes @ List.mapPartial
   2.133        (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
   2.134 @@ -396,7 +411,7 @@
   2.135  
   2.136      fun compile_eq (gr, (s, t)) =
   2.137        apsnd (Pretty.block o cons (Pretty.str (s ^ " = ")) o single)
   2.138 -        (invoke_codegen thy dep false (gr, t));
   2.139 +        (invoke_codegen thy defs dep thyname false (gr, t));
   2.140  
   2.141      val (in_ts, out_ts) = get_args is 1 ts;
   2.142      val ((all_vs', eqs), in_ts') =
   2.143 @@ -409,14 +424,14 @@
   2.144      fun compile_prems out_ts' vs names gr [] =
   2.145            let
   2.146              val (gr2, out_ps) = foldl_map
   2.147 -              (invoke_codegen thy dep false) (gr, out_ts);
   2.148 +              (invoke_codegen thy defs dep thyname false) (gr, out_ts);
   2.149              val (gr3, eq_ps) = foldl_map compile_eq (gr2, eqs);
   2.150              val ((names', eqs'), out_ts'') =
   2.151                foldl_map check_constrt ((names, []), out_ts');
   2.152              val (nvs, out_ts''') = foldl_map distinct_v
   2.153                ((names', map (fn x => (x, [x])) vs), out_ts'');
   2.154              val (gr4, out_ps') = foldl_map
   2.155 -              (invoke_codegen thy dep false) (gr3, out_ts''');
   2.156 +              (invoke_codegen thy defs dep thyname false) (gr3, out_ts''');
   2.157              val (gr5, eq_ps') = foldl_map compile_eq (gr4, eqs')
   2.158            in
   2.159              (gr5, compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
   2.160 @@ -434,7 +449,7 @@
   2.161              val (nvs, out_ts'') = foldl_map distinct_v
   2.162                ((names', map (fn x => (x, [x])) vs), out_ts');
   2.163              val (gr0, out_ps) = foldl_map
   2.164 -              (invoke_codegen thy dep false) (gr, out_ts'');
   2.165 +              (invoke_codegen thy defs dep thyname false) (gr, out_ts'');
   2.166              val (gr1, eq_ps) = foldl_map compile_eq (gr0, eqs)
   2.167            in
   2.168              (case p of
   2.169 @@ -442,14 +457,15 @@
   2.170                   let
   2.171                     val (in_ts, out_ts''') = get_args js 1 us;
   2.172                     val (gr2, in_ps) = foldl_map
   2.173 -                     (invoke_codegen thy dep false) (gr1, in_ts);
   2.174 +                     (invoke_codegen thy defs dep thyname false) (gr1, in_ts);
   2.175                     val (gr3, ps) = if is_ind t then
   2.176                         apsnd (fn ps => ps @ [Pretty.brk 1, mk_tuple in_ps])
   2.177 -                         (compile_expr thy dep false (gr2, (mode, t)))
   2.178 +                         (compile_expr thy defs dep thyname false thynames
   2.179 +                           (gr2, (mode, t)))
   2.180                       else
   2.181                         apsnd (fn p => conv_ntuple us t
   2.182                           [Pretty.str "Seq.of_list", Pretty.brk 1, p])
   2.183 -                           (invoke_codegen thy dep true (gr2, t));
   2.184 +                           (invoke_codegen thy defs dep thyname true (gr2, t));
   2.185                     val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps';
   2.186                   in
   2.187                     (gr4, compile_match (snd nvs) eq_ps out_ps
   2.188 @@ -459,7 +475,7 @@
   2.189                   end
   2.190               | Sidecond t =>
   2.191                   let
   2.192 -                   val (gr2, side_p) = invoke_codegen thy dep true (gr1, t);
   2.193 +                   val (gr2, side_p) = invoke_codegen thy defs dep thyname true (gr1, t);
   2.194                     val (gr3, rest) = compile_prems [] vs' (fst nvs) gr2 ps';
   2.195                   in
   2.196                     (gr3, compile_match (snd nvs) eq_ps out_ps
   2.197 @@ -474,22 +490,23 @@
   2.198      (gr', Pretty.block [Pretty.str "Seq.single inp :->", Pretty.brk 1, prem_p])
   2.199    end;
   2.200  
   2.201 -fun compile_pred thy gr dep prfx all_vs arg_vs modes s cls mode =
   2.202 -  let val (gr', cl_ps) = foldl_map (fn (gr, cl) =>
   2.203 -    compile_clause thy gr dep all_vs arg_vs modes mode cl) (gr, cls)
   2.204 +fun compile_pred thy defs gr dep thyname prfx all_vs arg_vs modes thynames s cls mode =
   2.205 +  let val (gr', cl_ps) = foldl_map (fn (gr, cl) => compile_clause thy defs
   2.206 +    gr dep thyname all_vs arg_vs modes thynames mode cl) (gr, cls)
   2.207    in
   2.208      ((gr', "and "), Pretty.block
   2.209        ([Pretty.block (separate (Pretty.brk 1)
   2.210 -         (Pretty.str (prfx ^ modename thy s mode) :: map Pretty.str arg_vs) @
   2.211 +         (Pretty.str (prfx ^ modename thy thyname thyname s mode) ::
   2.212 +           map Pretty.str arg_vs) @
   2.213           [Pretty.str " inp ="]),
   2.214          Pretty.brk 1] @
   2.215         List.concat (separate [Pretty.str " ++", Pretty.brk 1] (map single cl_ps))))
   2.216    end;
   2.217  
   2.218 -fun compile_preds thy gr dep all_vs arg_vs modes preds =
   2.219 +fun compile_preds thy defs gr dep thyname all_vs arg_vs modes thynames preds =
   2.220    let val ((gr', _), prs) = foldl_map (fn ((gr, prfx), (s, cls)) =>
   2.221 -    foldl_map (fn ((gr', prfx'), mode) =>
   2.222 -      compile_pred thy gr' dep prfx' all_vs arg_vs modes s cls mode)
   2.223 +    foldl_map (fn ((gr', prfx'), mode) => compile_pred thy defs gr'
   2.224 +      dep thyname prfx' all_vs arg_vs modes thynames s cls mode)
   2.225          ((gr, prfx), valOf (assoc (modes, s)))) ((gr, "fun "), preds)
   2.226    in
   2.227      (gr', space_implode "\n\n" (map Pretty.string_of (List.concat prs)) ^ ";\n\n")
   2.228 @@ -499,11 +516,13 @@
   2.229  
   2.230  exception Modes of
   2.231    (string * (int list option list * int list) list) list *
   2.232 -  (string * (int list list option list * int list list)) list;
   2.233 +  (string * (int list list option list * int list list)) list *
   2.234 +  string;
   2.235  
   2.236 -fun lookup_modes gr dep = apfst List.concat (apsnd List.concat (ListPair.unzip
   2.237 -  (map ((fn (SOME (Modes x), _) => x | _ => ([], [])) o Graph.get_node gr)
   2.238 -    (Graph.all_preds gr [dep]))));
   2.239 +fun lookup_modes gr dep = foldl (fn ((xs, ys, z), (xss, yss, zss)) =>
   2.240 +    (xss @ xs, yss @ ys, zss @ map (rpair z o fst) ys)) ([], [], [])
   2.241 +  (map ((fn (SOME (Modes x), _, _) => x | _ => ([], [], "")) o Graph.get_node gr)
   2.242 +    (Graph.all_preds gr [dep]));
   2.243  
   2.244  fun print_factors factors = message ("Factors:\n" ^
   2.245    space_implode "\n" (map (fn (s, (fs, f)) => s ^ ": " ^
   2.246 @@ -518,18 +537,17 @@
   2.247        NONE => xs
   2.248      | SOME xs' => xs inter xs') :: constrain cs ys;
   2.249  
   2.250 -fun mk_extra_defs thy gr dep names ts =
   2.251 +fun mk_extra_defs thy defs gr dep names ts =
   2.252    Library.foldl (fn (gr, name) =>
   2.253      if name mem names then gr
   2.254      else (case get_clauses thy name of
   2.255          NONE => gr
   2.256 -      | SOME (names, intrs) =>
   2.257 -          mk_ind_def thy gr dep names [] [] (prep_intrs intrs)))
   2.258 +      | SOME (names, thyname, intrs) =>
   2.259 +          mk_ind_def thy defs gr dep names thyname [] [] (prep_intrs intrs)))
   2.260              (gr, foldr add_term_consts [] ts)
   2.261  
   2.262 -and mk_ind_def thy gr dep names modecs factorcs intrs =
   2.263 -  let val ids = map (mk_const_id (sign_of thy)) names
   2.264 -  in Graph.add_edge (hd ids, dep) gr handle Graph.UNDEF _ =>
   2.265 +and mk_ind_def thy defs gr dep names thyname modecs factorcs intrs =
   2.266 +  Graph.add_edge (hd names, dep) gr handle Graph.UNDEF _ =>
   2.267      let
   2.268        val _ $ (_ $ _ $ u) = Logic.strip_imp_concl (hd intrs);
   2.269        val (_, args) = strip_comb u;
   2.270 @@ -565,10 +583,10 @@
   2.271              else fs
   2.272          | add_prod_factors _ (fs, _) = fs;
   2.273  
   2.274 -      val gr' = mk_extra_defs thy
   2.275 -        (Graph.add_edge (hd ids, dep)
   2.276 -          (Graph.new_node (hd ids, (NONE, "")) gr)) (hd ids) names intrs;
   2.277 -      val (extra_modes, extra_factors) = lookup_modes gr' (hd ids);
   2.278 +      val gr' = mk_extra_defs thy defs
   2.279 +        (Graph.add_edge (hd names, dep)
   2.280 +          (Graph.new_node (hd names, (NONE, "", "")) gr)) (hd names) names intrs;
   2.281 +      val (extra_modes, extra_factors, extra_thynames) = lookup_modes gr' (hd names);
   2.282        val fs = constrain factorcs (map (apsnd dest_factors)
   2.283          (Library.foldl (add_prod_factors extra_factors) ([], List.concat (map (fn t =>
   2.284            Logic.strip_imp_concl t :: Logic.strip_imp_prems t) intrs))));
   2.285 @@ -581,38 +599,40 @@
   2.286          (infer_modes thy extra_modes factors arg_vs clauses);
   2.287        val _ = print_factors factors;
   2.288        val _ = print_modes modes;
   2.289 -      val (gr'', s) = compile_preds thy gr' (hd ids) (terms_vs intrs) arg_vs
   2.290 -        (modes @ extra_modes) clauses;
   2.291 +      val (gr'', s) = compile_preds thy defs gr' (hd names) thyname (terms_vs intrs)
   2.292 +        arg_vs (modes @ extra_modes)
   2.293 +        (map (rpair thyname o fst) factors @ extra_thynames) clauses;
   2.294      in
   2.295 -      (Graph.map_node (hd ids) (K (SOME (Modes (modes, factors)), s)) gr'')
   2.296 -    end      
   2.297 -  end;
   2.298 +      (Graph.map_node (hd names)
   2.299 +        (K (SOME (Modes (modes, factors, thyname)), thyname, s)) gr'')
   2.300 +    end;
   2.301  
   2.302  fun find_mode s u modes is = (case find_first (fn Mode ((_, js), _) => is=js)
   2.303    (modes_of modes u handle Option => []) of
   2.304       NONE => error ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
   2.305     | mode => mode);
   2.306  
   2.307 -fun mk_ind_call thy gr dep t u is_query = (case head_of u of
   2.308 +fun mk_ind_call thy defs gr dep thyname t u is_query = (case head_of u of
   2.309    Const (s, T) => (case (get_clauses thy s, get_assoc_code thy s T) of
   2.310         (NONE, _) => NONE
   2.311 -     | (SOME (names, intrs), NONE) =>
   2.312 +     | (SOME (names, thyname', intrs), NONE) =>
   2.313           let
   2.314            fun mk_mode (((ts, mode), i), Const ("dummy_pattern", _)) =
   2.315                  ((ts, mode), i+1)
   2.316              | mk_mode (((ts, mode), i), t) = ((ts @ [t], mode @ [i]), i+1);
   2.317  
   2.318 -           val gr1 = mk_extra_defs thy
   2.319 -             (mk_ind_def thy gr dep names [] [] (prep_intrs intrs)) dep names [u];
   2.320 -           val (modes, factors) = lookup_modes gr1 dep;
   2.321 +           val gr1 = mk_extra_defs thy defs
   2.322 +             (mk_ind_def thy defs gr dep names thyname' [] [] (prep_intrs intrs)) dep names [u];
   2.323 +           val (modes, factors, thynames) = lookup_modes gr1 dep;
   2.324             val ts = split_prod [] (snd (valOf (assoc (factors, s)))) t;
   2.325             val (ts', is) = if is_query then
   2.326                 fst (Library.foldl mk_mode ((([], []), 1), ts))
   2.327               else (ts, 1 upto length ts);
   2.328             val mode = find_mode s u modes is;
   2.329             val (gr2, in_ps) = foldl_map
   2.330 -             (invoke_codegen thy dep false) (gr1, ts');
   2.331 -           val (gr3, ps) = compile_expr thy dep false (gr2, (mode, u))
   2.332 +             (invoke_codegen thy defs dep thyname false) (gr1, ts');
   2.333 +           val (gr3, ps) =
   2.334 +             compile_expr thy defs dep thyname false thynames (gr2, (mode, u))
   2.335           in
   2.336             SOME (gr3, Pretty.block
   2.337               (ps @ [Pretty.brk 1, mk_tuple in_ps]))
   2.338 @@ -620,16 +640,17 @@
   2.339       | _ => NONE)
   2.340    | _ => NONE);
   2.341  
   2.342 -fun list_of_indset thy gr dep brack u = (case head_of u of
   2.343 +fun list_of_indset thy defs gr dep thyname brack u = (case head_of u of
   2.344    Const (s, T) => (case (get_clauses thy s, get_assoc_code thy s T) of
   2.345         (NONE, _) => NONE
   2.346 -     | (SOME (names, intrs), NONE) =>
   2.347 +     | (SOME (names, thyname', intrs), NONE) =>
   2.348           let
   2.349 -           val gr1 = mk_extra_defs thy
   2.350 -             (mk_ind_def thy gr dep names [] [] (prep_intrs intrs)) dep names [u];
   2.351 -           val (modes, factors) = lookup_modes gr1 dep;
   2.352 +           val gr1 = mk_extra_defs thy defs
   2.353 +             (mk_ind_def thy defs gr dep names thyname' [] [] (prep_intrs intrs)) dep names [u];
   2.354 +           val (modes, factors, thynames) = lookup_modes gr1 dep;
   2.355             val mode = find_mode s u modes [];
   2.356 -           val (gr2, ps) = compile_expr thy dep false (gr1, (mode, u))
   2.357 +           val (gr2, ps) =
   2.358 +             compile_expr thy defs dep thyname false thynames (gr1, (mode, u))
   2.359           in
   2.360             SOME (gr2, (if brack then parens else I)
   2.361               (Pretty.block ([Pretty.str "Seq.list_of", Pretty.brk 1,
   2.362 @@ -650,58 +671,63 @@
   2.363    in
   2.364      rename_term
   2.365        (Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop (HOLogic.mk_mem
   2.366 -        (foldr1 HOLogic.mk_prod (ts @ [u]), Const (Sign.base_name s ^ "_aux",
   2.367 +        (foldr1 HOLogic.mk_prod (ts @ [u]), Const (s ^ " ",
   2.368            HOLogic.mk_setT (foldr1 HOLogic.mk_prodT (Ts @ [U])))))))
   2.369    end;
   2.370  
   2.371 -fun mk_fun thy name eqns dep gr = 
   2.372 -  let val id = mk_const_id (sign_of thy) name
   2.373 -  in Graph.add_edge (id, dep) gr handle Graph.UNDEF _ =>
   2.374 +fun mk_fun thy defs name eqns dep thyname thyname' gr =
   2.375 +  let
   2.376 +    val fun_id = mk_const_id (sign_of thy) thyname' thyname' name;
   2.377 +    val call_id = mk_const_id (sign_of thy) thyname thyname' name
   2.378 +  in (Graph.add_edge (name, dep) gr handle Graph.UNDEF _ =>
   2.379      let
   2.380        val clauses = map clause_of_eqn eqns;
   2.381 -      val pname = mk_const_id (sign_of thy) (Sign.base_name name ^ "_aux");
   2.382 +      val pname = name ^ " ";
   2.383        val arity = length (snd (strip_comb (fst (HOLogic.dest_eq
   2.384          (HOLogic.dest_Trueprop (concl_of (hd eqns)))))));
   2.385        val mode = 1 upto arity;
   2.386        val vars = map (fn i => Pretty.str ("x" ^ string_of_int i)) mode;
   2.387        val s = Pretty.string_of (Pretty.block
   2.388 -        [mk_app false (Pretty.str ("fun " ^ id)) vars, Pretty.str " =",
   2.389 +        [mk_app false (Pretty.str ("fun " ^ fun_id)) vars, Pretty.str " =",
   2.390           Pretty.brk 1, Pretty.str "Seq.hd", Pretty.brk 1,
   2.391 -         parens (Pretty.block [Pretty.str (modename thy pname ([], mode)),
   2.392 +         parens (Pretty.block [Pretty.str (modename thy thyname' thyname' pname ([], mode)),
   2.393             Pretty.brk 1, mk_tuple vars])]) ^ ";\n\n";
   2.394 -      val gr' = mk_ind_def thy (Graph.add_edge (id, dep)
   2.395 -        (Graph.new_node (id, (NONE, s)) gr)) id [pname]
   2.396 +      val gr' = mk_ind_def thy defs (Graph.add_edge (name, dep)
   2.397 +        (Graph.new_node (name, (NONE, thyname', s)) gr)) name [pname] thyname'
   2.398          [(pname, [([], mode)])]
   2.399          [(pname, map (fn i => replicate i 2) (0 upto arity-1))]
   2.400          clauses;
   2.401 -      val (modes, _) = lookup_modes gr' dep;
   2.402 +      val (modes, _, _) = lookup_modes gr' dep;
   2.403        val _ = find_mode pname (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
   2.404          (Logic.strip_imp_concl (hd clauses))))) modes mode
   2.405 -    in gr' end
   2.406 +    in gr' end, call_id)
   2.407    end;
   2.408  
   2.409 -fun inductive_codegen thy gr dep brack (Const ("op :", _) $ t $ u) =
   2.410 -      ((case mk_ind_call thy gr dep (Term.no_dummy_patterns t) u false of
   2.411 +fun inductive_codegen thy defs gr dep thyname brack (Const ("op :", _) $ t $ u) =
   2.412 +      ((case mk_ind_call thy defs gr dep thyname (Term.no_dummy_patterns t) u false of
   2.413           NONE => NONE
   2.414         | SOME (gr', call_p) => SOME (gr', (if brack then parens else I)
   2.415             (Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"])))
   2.416 -        handle TERM _ => mk_ind_call thy gr dep t u true)
   2.417 -  | inductive_codegen thy gr dep brack t = (case strip_comb t of
   2.418 +        handle TERM _ => mk_ind_call thy defs gr dep thyname t u true)
   2.419 +  | inductive_codegen thy defs gr dep thyname brack t = (case strip_comb t of
   2.420        (Const (s, _), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy), s) of
   2.421 -        NONE => list_of_indset thy gr dep brack t
   2.422 +        NONE => list_of_indset thy defs gr dep thyname brack t
   2.423        | SOME eqns =>
   2.424            let
   2.425 -            val gr' = mk_fun thy s (preprocess thy eqns) dep gr
   2.426 -            val (gr'', ps) = foldl_map (invoke_codegen thy dep true) (gr', ts);
   2.427 -          in SOME (gr'', mk_app brack (Pretty.str (mk_const_id
   2.428 -            (sign_of thy) s)) ps)
   2.429 +            val (_, (_, thyname')) = split_last eqns;
   2.430 +            val (gr', id) = mk_fun thy defs s (preprocess thy (map fst eqns))
   2.431 +              dep thyname thyname' gr;
   2.432 +            val (gr'', ps) = foldl_map
   2.433 +              (invoke_codegen thy defs dep thyname true) (gr', ts);
   2.434 +          in SOME (gr'', mk_app brack (Pretty.str id) ps)
   2.435            end)
   2.436      | _ => NONE);
   2.437  
   2.438  val setup =
   2.439    [add_codegen "inductive" inductive_codegen,
   2.440     CodegenData.init,
   2.441 -   add_attribute "ind" (Scan.succeed add)];
   2.442 +   add_attribute "ind"
   2.443 +     (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)];
   2.444  
   2.445  end;
   2.446  
     3.1 --- a/src/HOL/Tools/recfun_codegen.ML	Fri Jul 01 14:11:06 2005 +0200
     3.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Fri Jul 01 14:13:40 2005 +0200
     3.3 @@ -7,7 +7,8 @@
     3.4  
     3.5  signature RECFUN_CODEGEN =
     3.6  sig
     3.7 -  val add: theory attribute
     3.8 +  val add: string option -> theory attribute
     3.9 +  val del: theory attribute
    3.10    val setup: (theory -> theory) list
    3.11  end;
    3.12  
    3.13 @@ -19,11 +20,11 @@
    3.14  structure CodegenData = TheoryDataFun
    3.15  (struct
    3.16    val name = "HOL/recfun_codegen";
    3.17 -  type T = thm list Symtab.table;
    3.18 +  type T = (thm * string option) list Symtab.table;
    3.19    val empty = Symtab.empty;
    3.20    val copy = I;
    3.21    val extend = I;
    3.22 -  fun merge _ = Symtab.merge_multi' Drule.eq_thm_prop;
    3.23 +  fun merge _ = Symtab.merge_multi' (Drule.eq_thm_prop o pairself fst);
    3.24    fun print _ _ = ();
    3.25  end);
    3.26  
    3.27 @@ -35,14 +36,14 @@
    3.28  fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^
    3.29    string_of_thm thm);
    3.30  
    3.31 -fun add (p as (thy, thm)) =
    3.32 +fun add optmod (p as (thy, thm)) =
    3.33    let
    3.34      val tab = CodegenData.get thy;
    3.35      val (s, _) = const_of (prop_of thm);
    3.36    in
    3.37      if Pattern.pattern (lhs_of thm) then
    3.38        (CodegenData.put (Symtab.update ((s,
    3.39 -        thm :: getOpt (Symtab.lookup (tab, s), [])), tab)) thy, thm)
    3.40 +        (thm, optmod) :: getOpt (Symtab.lookup (tab, s), [])), tab)) thy, thm)
    3.41      else (warn thm; p)
    3.42    end handle TERM _ => (warn thm; p);
    3.43  
    3.44 @@ -53,7 +54,7 @@
    3.45    in case Symtab.lookup (tab, s) of
    3.46        NONE => p
    3.47      | SOME thms => (CodegenData.put (Symtab.update ((s,
    3.48 -        gen_rem eq_thm (thms, thm)), tab)) thy, thm)
    3.49 +        gen_rem (eq_thm o apfst fst) (thms, thm)), tab)) thy, thm)
    3.50    end handle TERM _ => (warn thm; p);
    3.51  
    3.52  fun del_redundant thy eqs [] = eqs
    3.53 @@ -61,20 +62,27 @@
    3.54      let
    3.55        val tsig = Sign.tsig_of (sign_of thy);
    3.56        val matches = curry
    3.57 -        (Pattern.matches tsig o pairself lhs_of)
    3.58 +        (Pattern.matches tsig o pairself (lhs_of o fst))
    3.59      in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end;
    3.60  
    3.61 -fun get_equations thy (s, T) =
    3.62 +fun get_equations thy defs (s, T) =
    3.63    (case Symtab.lookup (CodegenData.get thy, s) of
    3.64 -     NONE => []
    3.65 -   | SOME thms => preprocess thy (del_redundant thy []
    3.66 -       (List.filter (fn thm => is_instance thy T
    3.67 -         (snd (const_of (prop_of thm)))) thms)));
    3.68 +     NONE => ([], "")
    3.69 +   | SOME thms => 
    3.70 +       let val thms' = del_redundant thy []
    3.71 +         (List.filter (fn (thm, _) => is_instance thy T
    3.72 +           (snd (const_of (prop_of thm)))) thms)
    3.73 +       in if null thms' then ([], "")
    3.74 +         else (preprocess thy (map fst thms'),
    3.75 +           case snd (snd (split_last thms')) of
    3.76 +               NONE => (case get_defn thy defs s T of
    3.77 +                   NONE => thyname_of_const s thy
    3.78 +                 | SOME ((_, (thyname, _)), _) => thyname)
    3.79 +             | SOME thyname => thyname)
    3.80 +       end);
    3.81  
    3.82 -fun mk_poly_id thy (s, T) = mk_const_id (sign_of thy) s ^
    3.83 -  (case get_defn thy s T of
    3.84 -     SOME (_, SOME i) => "_def" ^ string_of_int i
    3.85 -   | _ => "");
    3.86 +fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
    3.87 +  SOME (_, SOME i) => "_def" ^ string_of_int i | _ => "");
    3.88  
    3.89  exception EQN of string * typ * string;
    3.90  
    3.91 @@ -82,27 +90,27 @@
    3.92    if x mem xs then xs
    3.93    else Library.foldl (cycle g) (x :: xs, List.concat (Graph.find_paths g (x, x)));
    3.94  
    3.95 -fun add_rec_funs thy gr dep eqs =
    3.96 +fun add_rec_funs thy defs gr dep eqs thyname =
    3.97    let
    3.98 -    fun dest_eq t =
    3.99 -      (mk_poly_id thy (const_of t), dest_eqn (rename_term t));
   3.100 +    fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
   3.101 +      dest_eqn (rename_term t));
   3.102      val eqs' = map dest_eq eqs;
   3.103      val (dname, _) :: _ = eqs';
   3.104      val (s, T) = const_of (hd eqs);
   3.105  
   3.106 -    fun mk_fundef fname prfx gr [] = (gr, [])
   3.107 -      | mk_fundef fname prfx gr ((fname', (lhs, rhs)) :: xs) =
   3.108 +    fun mk_fundef thyname fname prfx gr [] = (gr, [])
   3.109 +      | mk_fundef thyname fname prfx gr ((fname', (lhs, rhs)) :: xs) =
   3.110        let
   3.111 -        val (gr1, pl) = invoke_codegen thy dname false (gr, lhs);
   3.112 -        val (gr2, pr) = invoke_codegen thy dname false (gr1, rhs);
   3.113 -        val (gr3, rest) = mk_fundef fname' "and " gr2 xs
   3.114 +        val (gr1, pl) = invoke_codegen thy defs dname thyname false (gr, lhs);
   3.115 +        val (gr2, pr) = invoke_codegen thy defs dname thyname false (gr1, rhs);
   3.116 +        val (gr3, rest) = mk_fundef thyname fname' "and " gr2 xs
   3.117        in
   3.118          (gr3, Pretty.blk (4, [Pretty.str (if fname = fname' then "  | " else prfx),
   3.119             pl, Pretty.str " =", Pretty.brk 1, pr]) :: rest)
   3.120        end;
   3.121  
   3.122 -    fun put_code fundef = Graph.map_node dname
   3.123 -      (K (SOME (EQN ("", dummyT, dname)), Pretty.string_of (Pretty.blk (0,
   3.124 +    fun put_code thyname fundef = Graph.map_node dname
   3.125 +      (K (SOME (EQN ("", dummyT, dname)), thyname, Pretty.string_of (Pretty.blk (0,
   3.126        separate Pretty.fbrk fundef @ [Pretty.str ";"])) ^ "\n\n"));
   3.127  
   3.128    in
   3.129 @@ -110,43 +118,47 @@
   3.130         NONE =>
   3.131           let
   3.132             val gr1 = Graph.add_edge (dname, dep)
   3.133 -             (Graph.new_node (dname, (SOME (EQN (s, T, "")), "")) gr);
   3.134 -           val (gr2, fundef) = mk_fundef "" "fun " gr1 eqs';
   3.135 +             (Graph.new_node (dname, (SOME (EQN (s, T, "")), "", "")) gr);
   3.136 +           val (gr2, fundef) = mk_fundef thyname "" "fun " gr1 eqs';
   3.137             val xs = cycle gr2 ([], dname);
   3.138             val cs = map (fn x => case Graph.get_node gr2 x of
   3.139 -               (SOME (EQN (s, T, _)), _) => (s, T)
   3.140 +               (SOME (EQN (s, T, _)), _, _) => (s, T)
   3.141               | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^
   3.142                  implode (separate ", " xs))) xs
   3.143           in (case xs of
   3.144 -             [_] => put_code fundef gr2
   3.145 +             [_] => put_code thyname fundef gr2
   3.146             | _ =>
   3.147               if not (dep mem xs) then
   3.148                 let
   3.149 -                 val eqs'' = map (dest_eq o prop_of)
   3.150 -                   (List.concat (map (get_equations thy) cs));
   3.151 -                 val (gr3, fundef') = mk_fundef "" "fun "
   3.152 +                 val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
   3.153 +                 val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss));
   3.154 +                 val (gr3, fundef') = mk_fundef thyname "" "fun "
   3.155                     (Graph.add_edge (dname, dep)
   3.156                       (foldr (uncurry Graph.new_node) (Graph.del_nodes xs gr2)
   3.157                         (map (fn k =>
   3.158 -                         (k, (SOME (EQN ("", dummyT, dname)), ""))) xs))) eqs''
   3.159 -               in put_code fundef' gr3 end
   3.160 +                         (k, (SOME (EQN ("", dummyT, dname)), thyname, ""))) xs))) eqs''
   3.161 +               in put_code thyname fundef' gr3 end
   3.162               else gr2)
   3.163           end
   3.164 -     | SOME (SOME (EQN (_, _, s)), _) =>
   3.165 +     | SOME (SOME (EQN (_, _, s)), _, _) =>
   3.166           if s = "" then
   3.167             if dname = dep then gr else Graph.add_edge (dname, dep) gr
   3.168           else if s = dep then gr else Graph.add_edge (s, dep) gr)
   3.169    end;
   3.170  
   3.171 -fun recfun_codegen thy gr dep brack t = (case strip_comb t of
   3.172 -    (Const (p as (s, T)), ts) => (case (get_equations thy p, get_assoc_code thy s T) of
   3.173 -       ([], _) => NONE
   3.174 +fun recfun_codegen thy defs gr dep thyname brack t = (case strip_comb t of
   3.175 +    (Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy s T) of
   3.176 +       (([], _), _) => NONE
   3.177       | (_, SOME _) => NONE
   3.178 -     | (eqns, NONE) =>
   3.179 -        let val (gr', ps) = foldl_map (invoke_codegen thy dep true) (gr, ts)
   3.180 +     | ((eqns, thyname'), NONE) =>
   3.181 +        let
   3.182 +          val (gr', ps) = foldl_map
   3.183 +            (invoke_codegen thy defs dep thyname true) (gr, ts);
   3.184 +          val suffix = mk_suffix thy defs p
   3.185          in
   3.186 -          SOME (add_rec_funs thy gr' dep (map prop_of eqns),
   3.187 -            mk_app brack (Pretty.str (mk_poly_id thy p)) ps)
   3.188 +          SOME (add_rec_funs thy defs gr' dep (map prop_of eqns) thyname',
   3.189 +            mk_app brack (Pretty.str
   3.190 +              (mk_const_id (sign_of thy) thyname thyname' s ^ suffix)) ps)
   3.191          end)
   3.192    | _ => NONE);
   3.193  
   3.194 @@ -154,6 +166,8 @@
   3.195  val setup =
   3.196    [CodegenData.init,
   3.197     add_codegen "recfun" recfun_codegen,
   3.198 -   add_attribute "" (Args.del |-- Scan.succeed del || Scan.succeed add)];
   3.199 +   add_attribute ""
   3.200 +     (   Args.del |-- Scan.succeed del
   3.201 +      || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)];
   3.202  
   3.203  end;
     4.1 --- a/src/HOL/Tools/typedef_package.ML	Fri Jul 01 14:11:06 2005 +0200
     4.2 +++ b/src/HOL/Tools/typedef_package.ML	Fri Jul 01 14:13:40 2005 +0200
     4.3 @@ -272,17 +272,18 @@
     4.4  
     4.5  (** trivial code generator **)
     4.6  
     4.7 -fun typedef_codegen thy gr dep brack t =
     4.8 +fun typedef_codegen thy defs gr dep thyname 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 dep false (gr, T);
    4.15 +        val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr, T);
    4.16          val (gr'', ps) =
    4.17 -          foldl_map (Codegen.invoke_codegen thy dep true) (gr', ts);
    4.18 -        val id = Codegen.mk_const_id thy s
    4.19 +          foldl_map (Codegen.invoke_codegen thy defs dep thyname true) (gr', ts);
    4.20 +        val id = Codegen.mk_const_id thy
    4.21 +          thyname (Codegen.thyname_of_type (get_name T) thy) s
    4.22        in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
    4.23 -    fun get_name (Type (tname, _)) = tname
    4.24 -      | get_name _ = "";
    4.25      fun lookup f T = getOpt (Option.map f (Symtab.lookup
    4.26        (TypedefData.get thy, get_name T)), "")
    4.27    in
    4.28 @@ -302,23 +303,25 @@
    4.29    | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)]
    4.30    | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
    4.31  
    4.32 -fun typedef_tycodegen thy gr dep brack (Type (s, Ts)) =
    4.33 +fun typedef_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) =
    4.34        (case Symtab.lookup (TypedefData.get thy, s) of
    4.35           NONE => NONE
    4.36         | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) =>
    4.37             if isSome (Codegen.get_assoc_type thy tname) then NONE else
    4.38             let
    4.39 -             val Abs_id = Codegen.mk_const_id thy Abs_name;
    4.40 -             val Rep_id = Codegen.mk_const_id thy Rep_name;
    4.41 -             val ty_id = Codegen.mk_type_id thy s;
    4.42 +             val thyname' = Codegen.thyname_of_type tname thy;
    4.43 +             val Abs_id = Codegen.mk_const_id thy thyname' thyname' Abs_name;
    4.44 +             val Rep_id = Codegen.mk_const_id thy thyname' thyname' Rep_name;
    4.45 +             val ty_id = Codegen.mk_type_id thy thyname' thyname' s;
    4.46 +             val ty_call_id = Codegen.mk_type_id thy thyname thyname' s;
    4.47               val (gr', qs) = foldl_map
    4.48 -               (Codegen.invoke_tycodegen thy dep (length Ts = 1)) (gr, Ts);
    4.49 -             val gr'' = Graph.add_edge (Abs_id, dep) gr' handle Graph.UNDEF _ =>
    4.50 +               (Codegen.invoke_tycodegen thy defs dep thyname (length Ts = 1)) (gr, Ts);
    4.51 +             val gr'' = Graph.add_edge (Abs_name, dep) gr' handle Graph.UNDEF _ =>
    4.52                 let
    4.53                   val (gr'', p :: ps) = foldl_map
    4.54 -                   (Codegen.invoke_tycodegen thy Abs_id false)
    4.55 -                   (Graph.add_edge (Abs_id, dep)
    4.56 -                      (Graph.new_node (Abs_id, (NONE, "")) gr'), oldT :: Us);
    4.57 +                   (Codegen.invoke_tycodegen thy defs Abs_name thyname' false)
    4.58 +                   (Graph.add_edge (Abs_name, dep)
    4.59 +                      (Graph.new_node (Abs_name, (NONE, "", "")) gr'), oldT :: Us);
    4.60                   val s =
    4.61                     Pretty.string_of (Pretty.block [Pretty.str "datatype ",
    4.62                       mk_tyexpr ps ty_id,
    4.63 @@ -329,28 +332,28 @@
    4.64                       Pretty.str "x) = x;"]) ^ "\n\n" ^
    4.65                     (if "term_of" mem !Codegen.mode then
    4.66                        Pretty.string_of (Pretty.block [Pretty.str "fun ",
    4.67 -                        Codegen.mk_term_of thy false newT, Pretty.brk 1,
    4.68 +                        Codegen.mk_term_of thy thyname' false newT, Pretty.brk 1,
    4.69                          Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
    4.70                          Pretty.str "x) =", Pretty.brk 1,
    4.71                          Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","),
    4.72                            Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
    4.73                            Pretty.str ")"], Pretty.str " $", Pretty.brk 1,
    4.74 -                        Codegen.mk_term_of thy false oldT, Pretty.brk 1,
    4.75 +                        Codegen.mk_term_of thy thyname' false oldT, Pretty.brk 1,
    4.76                          Pretty.str "x;"]) ^ "\n\n"
    4.77                      else "") ^
    4.78                     (if "test" mem !Codegen.mode then
    4.79                        Pretty.string_of (Pretty.block [Pretty.str "fun ",
    4.80 -                        Codegen.mk_gen thy false [] "" newT, Pretty.brk 1,
    4.81 +                        Codegen.mk_gen thy thyname' false [] "" newT, Pretty.brk 1,
    4.82                          Pretty.str "i =", Pretty.brk 1,
    4.83                          Pretty.block [Pretty.str (Abs_id ^ " ("),
    4.84 -                          Codegen.mk_gen thy false [] "" oldT, Pretty.brk 1,
    4.85 +                          Codegen.mk_gen thy thyname' false [] "" oldT, Pretty.brk 1,
    4.86                            Pretty.str "i);"]]) ^ "\n\n"
    4.87                      else "")
    4.88 -               in Graph.map_node Abs_id (K (NONE, s)) gr'' end
    4.89 +               in Graph.map_node Abs_name (K (NONE, thyname', s)) gr'' end
    4.90             in
    4.91 -             SOME (gr'', mk_tyexpr qs ty_id)
    4.92 +             SOME (gr'', mk_tyexpr qs ty_call_id)
    4.93             end)
    4.94 -  | typedef_tycodegen thy gr dep brack _ = NONE;
    4.95 +  | typedef_tycodegen thy defs gr dep thyname brack _ = NONE;
    4.96  
    4.97  val setup =
    4.98    [TypedefData.init,