src/HOL/Tools/inductive_codegen.ML
changeset 12557 bb2e4689347e
parent 12453 806502073957
child 12562 323ce5a89695
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Dec 20 14:57:54 2001 +0100
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Dec 20 14:58:18 2001 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4  
     1.5  signature INDUCTIVE_CODEGEN =
     1.6  sig
     1.7 +  val add : theory attribute
     1.8    val setup : (theory -> theory) list
     1.9  end;
    1.10  
    1.11 @@ -16,10 +17,48 @@
    1.12  
    1.13  open Codegen;
    1.14  
    1.15 -exception Modes of (string * int list list) list * (string * int list list) list;
    1.16 +(**** theory data ****)
    1.17 +
    1.18 +structure CodegenArgs =
    1.19 +struct
    1.20 +  val name = "HOL/inductive_codegen";
    1.21 +  type T = thm list Symtab.table;
    1.22 +  val empty = Symtab.empty;
    1.23 +  val copy = I;
    1.24 +  val prep_ext = I;
    1.25 +  val merge = Symtab.merge_multi eq_thm;
    1.26 +  fun print _ _ = ();
    1.27 +end;
    1.28 +
    1.29 +structure CodegenData = TheoryDataFun(CodegenArgs);
    1.30 +
    1.31 +fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
    1.32 +  string_of_thm thm);
    1.33  
    1.34 -datatype indprem = Prem of string * term list * term list
    1.35 -                 | Sidecond of term;
    1.36 +fun add (p as (thy, thm)) =
    1.37 +  let
    1.38 +    val tsig = Sign.tsig_of (sign_of thy);
    1.39 +    val tab = CodegenData.get thy;
    1.40 +    val matches = curry (Pattern.matches tsig o pairself concl_of);
    1.41 +
    1.42 +  in (case concl_of thm of
    1.43 +      _ $ (Const ("op :", _) $ _ $ t) => (case head_of t of
    1.44 +        Const (s, _) => (CodegenData.put (Symtab.update ((s,
    1.45 +          filter_out (matches thm) (if_none (Symtab.lookup (tab, s)) []) @
    1.46 +            [thm]), tab)) thy, thm)
    1.47 +      | _ => (warn thm; p))
    1.48 +    | _ => (warn thm; p))
    1.49 +  end handle Pattern.Pattern => (warn thm; p);
    1.50 +
    1.51 +fun get_clauses thy s =
    1.52 +  (case Symtab.lookup (CodegenData.get thy, s) of
    1.53 +     None => (case InductivePackage.get_inductive thy s of
    1.54 +       None => None
    1.55 +     | Some ({names, ...}, {intrs, ...}) => Some (names, intrs))
    1.56 +   | Some thms => Some ([s], thms));
    1.57 +
    1.58 +
    1.59 +(**** improper tuples ****)
    1.60  
    1.61  fun prod_factors p (Const ("Pair", _) $ t $ u) =
    1.62        p :: prod_factors (1::p) t @ prod_factors (2::p) u
    1.63 @@ -30,10 +69,44 @@
    1.64           split_prod (1::p) ps t @ split_prod (2::p) ps u
    1.65       | _ => error "Inconsistent use of products") else [t];
    1.66  
    1.67 +datatype factors = FVar of int list list | FFix of int list list;
    1.68 +
    1.69 +exception Factors;
    1.70 +
    1.71 +fun mg_factor (FVar f) (FVar f') = FVar (f inter f')
    1.72 +  | mg_factor (FVar f) (FFix f') =
    1.73 +      if f' subset f then FFix f' else raise Factors
    1.74 +  | mg_factor (FFix f) (FVar f') =
    1.75 +      if f subset f' then FFix f else raise Factors
    1.76 +  | mg_factor (FFix f) (FFix f') =
    1.77 +      if f subset f' andalso f' subset f then FFix f else raise Factors;
    1.78 +
    1.79 +fun dest_factors (FVar f) = f
    1.80 +  | dest_factors (FFix f) = f;
    1.81 +
    1.82 +fun infer_factors sg extra_fs (fs, (optf, t)) =
    1.83 +  let fun err s = error (s ^ "\n" ^ Sign.string_of_term sg t)
    1.84 +  in (case (optf, strip_comb t) of
    1.85 +      (Some f, (Const (name, _), args)) =>
    1.86 +        (case assoc (extra_fs, name) of
    1.87 +           None => overwrite (fs, (name, if_none
    1.88 +             (apsome (mg_factor f) (assoc (fs, name))) f))
    1.89 +         | Some (fs', f') => (mg_factor f (FFix f');
    1.90 +             foldl (infer_factors sg extra_fs)
    1.91 +               (fs, map (apsome FFix) fs' ~~ args)))
    1.92 +    | (Some f, (Var ((name, _), _), [])) =>
    1.93 +        overwrite (fs, (name, if_none
    1.94 +          (apsome (mg_factor f) (assoc (fs, name))) f))
    1.95 +    | (None, _) => fs
    1.96 +    | _ => err "Illegal term")
    1.97 +      handle Factors => err "Product factor mismatch in"
    1.98 +  end;
    1.99 +
   1.100  fun string_of_factors p ps = if p mem ps then
   1.101      "(" ^ string_of_factors (1::p) ps ^ ", " ^ string_of_factors (2::p) ps ^ ")"
   1.102    else "_";
   1.103  
   1.104 +
   1.105  (**** check if a term contains only constructor functions ****)
   1.106  
   1.107  fun is_constrt thy =
   1.108 @@ -81,9 +154,32 @@
   1.109         in merge (map (fn ks => i::ks) is) is end
   1.110       else [[]];
   1.111  
   1.112 +fun cprod ([], ys) = []
   1.113 +  | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
   1.114 +
   1.115 +fun cprods xss = foldr (map op :: o cprod) (xss, [[]]);
   1.116 +
   1.117 +datatype mode = Mode of (int list option list * int list) * mode option list;
   1.118 +
   1.119 +fun modes_of modes t =
   1.120 +  let
   1.121 +    fun mk_modes name args = flat
   1.122 +      (map (fn (m as (iss, is)) => map (Mode o pair m) (cprods (map
   1.123 +        (fn (None, _) => [None]
   1.124 +          | (Some js, arg) => map Some
   1.125 +              (filter (fn Mode ((_, js'), _) => js=js') (modes_of modes arg)))
   1.126 +                (iss ~~ args)))) (the (assoc (modes, name))))
   1.127 +
   1.128 +  in (case strip_comb t of
   1.129 +      (Const (name, _), args) => mk_modes name args
   1.130 +    | (Var ((name, _), _), args) => mk_modes name args)
   1.131 +  end;
   1.132 +
   1.133 +datatype indprem = Prem of term list * term | Sidecond of term;
   1.134 +
   1.135  fun select_mode_prem thy modes vs ps =
   1.136    find_first (is_some o snd) (ps ~~ map
   1.137 -    (fn Prem (s, us, args) => find_first (fn is =>
   1.138 +    (fn Prem (us, t) => find_first (fn Mode ((_, is), _) =>
   1.139            let
   1.140              val (_, out_ts) = get_args is 1 us;
   1.141              val vTs = flat (map term_vTs out_ts);
   1.142 @@ -92,21 +188,25 @@
   1.143            in
   1.144              is subset known_args vs 1 us andalso
   1.145              forall (is_constrt thy) (snd (get_args is 1 us)) andalso
   1.146 -            terms_vs args subset vs andalso
   1.147 +            term_vs t subset vs andalso
   1.148              forall is_eqT dupTs
   1.149            end)
   1.150 -            (the (assoc (modes, s)))
   1.151 -      | Sidecond t => if term_vs t subset vs then Some [] else None) ps);
   1.152 +            (modes_of modes t)
   1.153 +      | Sidecond t => if term_vs t subset vs then Some (Mode (([], []), []))
   1.154 +          else None) ps);
   1.155  
   1.156 -fun check_mode_clause thy arg_vs modes mode (ts, ps) =
   1.157 +fun check_mode_clause thy arg_vs modes (iss, is) (ts, ps) =
   1.158    let
   1.159 +    val modes' = modes @ mapfilter
   1.160 +      (fn (_, None) => None | (v, Some js) => Some (v, [([], js)]))
   1.161 +        (arg_vs ~~ iss);
   1.162      fun check_mode_prems vs [] = Some vs
   1.163 -      | check_mode_prems vs ps = (case select_mode_prem thy modes vs ps of
   1.164 +      | check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of
   1.165            None => None
   1.166          | Some (x, _) => check_mode_prems
   1.167 -            (case x of Prem (_, us, _) => vs union terms_vs us | _ => vs)
   1.168 +            (case x of Prem (us, _) => vs union terms_vs us | _ => vs)
   1.169              (filter_out (equal x) ps));
   1.170 -    val (in_ts', _) = get_args mode 1 ts;
   1.171 +    val (in_ts', _) = get_args is 1 ts;
   1.172      val in_ts = filter (is_constrt thy) in_ts';
   1.173      val in_vs = terms_vs in_ts;
   1.174      val concl_vs = terms_vs ts
   1.175 @@ -125,9 +225,12 @@
   1.176    let val y = f x
   1.177    in if x = y then x else fixp f y end;
   1.178  
   1.179 -fun infer_modes thy extra_modes arg_vs preds = fixp (fn modes =>
   1.180 +fun infer_modes thy extra_modes factors arg_vs preds = fixp (fn modes =>
   1.181    map (check_modes_pred thy arg_vs preds (modes @ extra_modes)) modes)
   1.182 -    (map (fn (s, (ts, _)::_) => (s, subsets 1 (length ts))) preds);
   1.183 +    (map (fn (s, (fs, f)) => (s, cprod (cprods (map
   1.184 +      (fn None => [None]
   1.185 +        | Some f' => map Some (subsets 1 (length f' + 1))) fs),
   1.186 +      subsets 1 (length f + 1)))) factors);
   1.187  
   1.188  (**** code generation ****)
   1.189  
   1.190 @@ -167,17 +270,37 @@
   1.191         [Pretty.brk 1, Pretty.str "| _ => ", fail_p, Pretty.str ")"]))
   1.192    end;
   1.193  
   1.194 -fun modename thy s mode = space_implode "_"
   1.195 -  (mk_const_id (sign_of thy) s :: map string_of_int mode);
   1.196 +fun modename thy s (iss, is) = space_implode "__"
   1.197 +  (mk_const_id (sign_of thy) s ::
   1.198 +    map (space_implode "_" o map string_of_int) (mapfilter I iss @ [is]));
   1.199  
   1.200 -fun compile_clause thy gr dep all_vs arg_vs modes mode (ts, ps) =
   1.201 +fun compile_expr thy dep brack (gr, (None, t)) =
   1.202 +      apsnd single (invoke_codegen thy dep brack (gr, t))
   1.203 +  | compile_expr _ _ _ (gr, (Some _, Var ((name, _), _))) =
   1.204 +      (gr, [Pretty.str name])
   1.205 +  | compile_expr thy dep brack (gr, (Some (Mode (mode, ms)), t)) =
   1.206 +      let
   1.207 +        val (Const (name, _), args) = strip_comb t;
   1.208 +        val (gr', ps) = foldl_map
   1.209 +          (compile_expr thy dep true) (gr, ms ~~ args);
   1.210 +      in (gr', (if brack andalso not (null ps) then
   1.211 +        single o parens o Pretty.block else I)
   1.212 +          (flat (separate [Pretty.brk 1]
   1.213 +            ([Pretty.str (modename thy name mode)] :: ps))))
   1.214 +      end;
   1.215 +
   1.216 +fun compile_clause thy gr dep all_vs arg_vs modes (iss, is) (ts, ps) =
   1.217    let
   1.218 +    val modes' = modes @ mapfilter
   1.219 +      (fn (_, None) => None | (v, Some js) => Some (v, [([], js)]))
   1.220 +        (arg_vs ~~ iss);
   1.221 +
   1.222      fun check_constrt ((names, eqs), t) =
   1.223        if is_constrt thy t then ((names, eqs), t) else
   1.224          let val s = variant names "x";
   1.225          in ((s::names, (s, t)::eqs), Var ((s, 0), fastype_of t)) end;
   1.226  
   1.227 -    val (in_ts, out_ts) = get_args mode 1 ts;
   1.228 +    val (in_ts, out_ts) = get_args is 1 ts;
   1.229      val ((all_vs', eqs), in_ts') =
   1.230        foldl_map check_constrt ((all_vs, []), in_ts);
   1.231  
   1.232 @@ -200,27 +323,25 @@
   1.233        | compile_prems out_ts vs names gr ps =
   1.234            let
   1.235              val vs' = distinct (flat (vs :: map term_vs out_ts));
   1.236 -            val Some (p, Some mode') =
   1.237 -              select_mode_prem thy modes (arg_vs union vs') ps;
   1.238 +            val Some (p, mode as Some (Mode ((_, js), _))) =
   1.239 +              select_mode_prem thy modes' (arg_vs union vs') ps;
   1.240              val ps' = filter_out (equal p) ps;
   1.241            in
   1.242              (case p of
   1.243 -               Prem (s, us, args) =>
   1.244 +               Prem (us, t) =>
   1.245                   let
   1.246 -                   val (in_ts, out_ts') = get_args mode' 1 us;
   1.247 +                   val (in_ts, out_ts') = get_args js 1 us;
   1.248                     val (gr1, in_ps) = foldl_map
   1.249                       (invoke_codegen thy dep false) (gr, in_ts);
   1.250 -                   val (gr2, arg_ps) = foldl_map
   1.251 -                     (invoke_codegen thy dep true) (gr1, args);
   1.252                     val (nvs, out_ts'') = foldl_map distinct_v
   1.253                       ((names, map (fn x => (x, [x])) vs), out_ts);
   1.254 -                   val (gr3, out_ps) = foldl_map
   1.255 -                     (invoke_codegen thy dep false) (gr2, out_ts'')
   1.256 +                   val (gr2, out_ps) = foldl_map
   1.257 +                     (invoke_codegen thy dep false) (gr1, out_ts'');
   1.258 +                   val (gr3, ps) = compile_expr thy dep false (gr2, (mode, t));
   1.259                     val (gr4, rest) = compile_prems out_ts' vs' (fst nvs) gr3 ps';
   1.260                   in
   1.261                     (gr4, compile_match (snd nvs) [] out_ps
   1.262 -                      (Pretty.block (separate (Pretty.brk 1)
   1.263 -                        (Pretty.str (modename thy s mode') :: arg_ps) @
   1.264 +                      (Pretty.block (ps @
   1.265                           [Pretty.brk 1, mk_tuple in_ps,
   1.266                            Pretty.str " :->", Pretty.brk 1, rest]))
   1.267                        (Pretty.str "Seq.empty"))
   1.268 @@ -269,69 +390,91 @@
   1.269  
   1.270  (**** processing of introduction rules ****)
   1.271  
   1.272 -val string_of_mode = enclose "[" "]" o commas o map string_of_int;
   1.273 +exception Modes of
   1.274 +  (string * (int list option list * int list) list) list *
   1.275 +  (string * (int list list option list * int list list)) list;
   1.276 +
   1.277 +fun lookup_modes gr dep = apfst flat (apsnd flat (ListPair.unzip
   1.278 +  (map ((fn (Some (Modes x), _) => x | _ => ([], [])) o Graph.get_node gr)
   1.279 +    (Graph.all_preds gr [dep]))));
   1.280 +
   1.281 +fun string_of_mode (iss, is) = space_implode " -> " (map
   1.282 +  (fn None => "X"
   1.283 +    | Some js => enclose "[" "]" (commas (map string_of_int js)))
   1.284 +       (iss @ [Some is]));
   1.285  
   1.286  fun print_modes modes = message ("Inferred modes:\n" ^
   1.287    space_implode "\n" (map (fn (s, ms) => s ^ ": " ^ commas (map
   1.288      string_of_mode ms)) modes));
   1.289  
   1.290  fun print_factors factors = message ("Factors:\n" ^
   1.291 -  space_implode "\n" (map (fn (s, fs) => s ^ ": " ^ string_of_factors [] fs) factors));
   1.292 -  
   1.293 -fun get_modes (Some (Modes x), _) = x
   1.294 -  | get_modes _ = ([], []);
   1.295 +  space_implode "\n" (map (fn (s, (fs, f)) => s ^ ": " ^
   1.296 +    space_implode " -> " (map
   1.297 +      (fn None => "X" | Some f' => string_of_factors [] f')
   1.298 +        (fs @ [Some f]))) factors));
   1.299  
   1.300 -fun mk_ind_def thy gr dep names intrs =
   1.301 +fun mk_extra_defs thy gr dep names ts =
   1.302 +  foldl (fn (gr, name) =>
   1.303 +    if name mem names then gr
   1.304 +    else (case get_clauses thy name of
   1.305 +        None => gr
   1.306 +      | Some (names, intrs) =>
   1.307 +          mk_ind_def thy gr dep names intrs))
   1.308 +            (gr, foldr add_term_consts (ts, []))
   1.309 +
   1.310 +and mk_ind_def thy gr dep names intrs =
   1.311    let val ids = map (mk_const_id (sign_of thy)) names
   1.312    in Graph.add_edge (hd ids, dep) gr handle Graph.UNDEF _ =>
   1.313      let
   1.314 -      fun process_prem factors (gr, t' as _ $ (Const ("op :", _) $ t $ u)) =
   1.315 -            (case strip_comb u of
   1.316 -               (Const (name, _), args) =>
   1.317 -                  (case InductivePackage.get_inductive thy name of
   1.318 -                     None => (gr, Sidecond t')
   1.319 -                   | Some ({names=names', ...}, {intrs=intrs', ...}) =>
   1.320 -                       (if names = names' then gr
   1.321 -                          else mk_ind_def thy gr (hd ids) names' intrs',
   1.322 -                        Prem (name, split_prod []
   1.323 -                          (the (assoc (factors, name))) t, args)))
   1.324 -             | _ => (gr, Sidecond t'))
   1.325 -        | process_prem factors (gr, _ $ (Const ("op =", _) $ t $ u)) =
   1.326 -            (gr, Prem ("eq", [t, u], []))
   1.327 -        | process_prem factors (gr, _ $ t) = (gr, Sidecond t);
   1.328 +      fun dest_prem factors (_ $ (Const ("op :", _) $ t $ u)) =
   1.329 +            (case head_of u of
   1.330 +               Const (name, _) => Prem (split_prod []
   1.331 +                 (the (assoc (factors, name))) t, u)
   1.332 +             | Var ((name, _), _) => Prem (split_prod []
   1.333 +                 (the (assoc (factors, name))) t, u))
   1.334 +        | dest_prem factors (_ $ ((eq as Const ("op =", _)) $ t $ u)) =
   1.335 +            Prem ([t, u], eq)
   1.336 +        | dest_prem factors (_ $ t) = Sidecond t;
   1.337  
   1.338 -      fun add_clause factors ((clauses, gr), intr) =
   1.339 +      fun add_clause factors (clauses, intr) =
   1.340          let
   1.341            val _ $ (_ $ t $ u) = Logic.strip_imp_concl intr;
   1.342 -          val (Const (name, _), args) = strip_comb u;
   1.343 -          val (gr', prems) = foldl_map (process_prem factors)
   1.344 -            (gr, Logic.strip_imp_prems intr);
   1.345 +          val Const (name, _) = head_of u;
   1.346 +          val prems = map (dest_prem factors) (Logic.strip_imp_prems intr);
   1.347          in
   1.348            (overwrite (clauses, (name, if_none (assoc (clauses, name)) [] @
   1.349 -             [(split_prod [] (the (assoc (factors, name))) t, prems)])), gr')
   1.350 +             [(split_prod [] (the (assoc (factors, name))) t, prems)])))
   1.351          end;
   1.352  
   1.353 -      fun add_prod_factors (fs, x as _ $ (Const ("op :", _) $ t $ u)) =
   1.354 -            (case strip_comb u of
   1.355 -               (Const (name, _), _) =>
   1.356 -                 let val f = prod_factors [] t
   1.357 -                 in overwrite (fs, (name, f inter if_none (assoc (fs, name)) f)) end
   1.358 -             | _ => fs)
   1.359 -        | add_prod_factors (fs, _) = fs;
   1.360 +      fun add_prod_factors extra_fs (fs, _ $ (Const ("op :", _) $ t $ u)) =
   1.361 +            infer_factors (sign_of thy) extra_fs
   1.362 +              (fs, (Some (FVar (prod_factors [] t)), u))
   1.363 +        | add_prod_factors _ (fs, _) = fs;
   1.364  
   1.365        val intrs' = map (rename_term o #prop o rep_thm o standard) intrs;
   1.366 -      val factors = foldl add_prod_factors ([], flat (map (fn t =>
   1.367 -        Logic.strip_imp_concl t :: Logic.strip_imp_prems t) intrs'));
   1.368 -      val (clauses, gr') = foldl (add_clause factors) (([], Graph.add_edge (hd ids, dep)
   1.369 -        (Graph.new_node (hd ids, (None, "")) gr)), intrs');
   1.370        val _ $ (_ $ _ $ u) = Logic.strip_imp_concl (hd intrs');
   1.371        val (_, args) = strip_comb u;
   1.372        val arg_vs = flat (map term_vs args);
   1.373 -      val extra_modes = ("eq", [[1], [2], [1,2]]) :: (flat (map
   1.374 -        (fst o get_modes o Graph.get_node gr') (Graph.all_preds gr' [hd ids])));
   1.375 -      val modes = infer_modes thy extra_modes arg_vs clauses;
   1.376 +      val gr' = mk_extra_defs thy
   1.377 +        (Graph.add_edge (hd ids, dep)
   1.378 +          (Graph.new_node (hd ids, (None, "")) gr)) (hd ids) names intrs';
   1.379 +      val (extra_modes', extra_factors) = lookup_modes gr' (hd ids);
   1.380 +      val extra_modes =
   1.381 +        ("op =", [([], [1]), ([], [2]), ([], [1, 2])]) :: extra_modes';
   1.382 +      val fs = map (apsnd dest_factors)
   1.383 +        (foldl (add_prod_factors extra_factors) ([], flat (map (fn t =>
   1.384 +          Logic.strip_imp_concl t :: Logic.strip_imp_prems t) intrs')));
   1.385 +      val _ = (case map fst fs \\ names \\ arg_vs of
   1.386 +          [] => ()
   1.387 +        | xs => error ("Non-inductive sets: " ^ commas_quote xs));
   1.388 +      val factors = mapfilter (fn (name, f) =>
   1.389 +        if name mem arg_vs then None
   1.390 +        else Some (name, (map (curry assoc fs) arg_vs, f))) fs;
   1.391 +      val clauses =
   1.392 +        foldl (add_clause (fs @ map (apsnd snd) extra_factors)) ([], intrs');
   1.393 +      val modes = infer_modes thy extra_modes factors arg_vs clauses;
   1.394 +      val _ = print_factors factors;
   1.395        val _ = print_modes modes;
   1.396 -      val _ = print_factors factors;
   1.397        val (gr'', s) = compile_preds thy gr' (hd ids) (terms_vs intrs') arg_vs
   1.398          (modes @ extra_modes) clauses;
   1.399      in
   1.400 @@ -339,31 +482,33 @@
   1.401      end      
   1.402    end;
   1.403  
   1.404 -fun mk_ind_call thy gr dep t u is_query = (case strip_comb u of
   1.405 -  (Const (s, _), args) => (case InductivePackage.get_inductive thy s of
   1.406 +fun mk_ind_call thy gr dep t u is_query = (case head_of u of
   1.407 +  Const (s, _) => (case get_clauses thy s of
   1.408         None => None
   1.409 -     | Some ({names, ...}, {intrs, ...}) =>
   1.410 +     | Some (names, intrs) =>
   1.411           let
   1.412            fun mk_mode (((ts, mode), i), Var _) = ((ts, mode), i+1)
   1.413              | mk_mode (((ts, mode), i), Free _) = ((ts, mode), i+1)
   1.414              | mk_mode (((ts, mode), i), t) = ((ts @ [t], mode @ [i]), i+1);
   1.415  
   1.416 -           val gr1 = mk_ind_def thy gr dep names intrs;
   1.417 -           val (modes, factors) = pairself flat (ListPair.unzip
   1.418 -             (map (get_modes o Graph.get_node gr1) (Graph.all_preds gr1 [dep])));
   1.419 -           val ts = split_prod [] (the (assoc (factors, s))) t;
   1.420 -           val (ts', mode) = if is_query then
   1.421 +           val gr1 = mk_extra_defs thy
   1.422 +             (mk_ind_def thy gr dep names intrs) dep names [u];
   1.423 +           val (modes, factors) = lookup_modes gr1 dep;
   1.424 +           val ts = split_prod [] (snd (the (assoc (factors, s)))) t;
   1.425 +           val (ts', is) = if is_query then
   1.426                 fst (foldl mk_mode ((([], []), 1), ts))
   1.427               else (ts, 1 upto length ts);
   1.428 -           val _ = if mode mem the (assoc (modes, s)) then () else
   1.429 -             error ("No such mode for " ^ s ^ ": " ^ string_of_mode mode);
   1.430 +           val mode = (case find_first (fn Mode ((_, js), _) => is=js)
   1.431 +                  (modes_of modes u) of
   1.432 +                None => error ("No such mode for " ^ s ^ ": " ^
   1.433 +                  string_of_mode ([], is))
   1.434 +              | mode => mode);
   1.435             val (gr2, in_ps) = foldl_map
   1.436               (invoke_codegen thy dep false) (gr1, ts');
   1.437 -           val (gr3, arg_ps) = foldl_map
   1.438 -             (invoke_codegen thy dep true) (gr2, args);
   1.439 +           val (gr3, ps) = compile_expr thy dep false (gr2, (mode, u))
   1.440           in
   1.441 -           Some (gr3, Pretty.block (separate (Pretty.brk 1)
   1.442 -             (Pretty.str (modename thy s mode) :: arg_ps @ [mk_tuple in_ps])))
   1.443 +           Some (gr3, Pretty.block
   1.444 +             (ps @ [Pretty.brk 1, mk_tuple in_ps]))
   1.445           end)
   1.446    | _ => None);
   1.447  
   1.448 @@ -376,7 +521,10 @@
   1.449        mk_ind_call thy gr dep t u true
   1.450    | inductive_codegen thy gr dep brack _ = None;
   1.451  
   1.452 -val setup = [add_codegen "inductive" inductive_codegen];
   1.453 +val setup =
   1.454 +  [add_codegen "inductive" inductive_codegen,
   1.455 +   CodegenData.init,
   1.456 +   add_attribute "ind" add];
   1.457  
   1.458  end;
   1.459  
   1.460 @@ -394,6 +542,8 @@
   1.461  
   1.462  fun ?! s = is_some (Seq.pull s);    
   1.463  
   1.464 -fun eq_1 x = Seq.single x;
   1.465 +fun op__61__1 x = Seq.single x;
   1.466  
   1.467 -val eq_2 = eq_1;
   1.468 +val op__61__2 = op__61__1;
   1.469 +
   1.470 +fun op__61__1_2 (x, y) = ?? (x = y);