src/HOL/Tools/inductive_codegen.ML
changeset 15031 726dc9146bb1
parent 14981 e73f8140af78
child 15061 61a52739cd82
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Jul 09 16:29:10 2004 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Jul 09 16:33:20 2004 +0200
     1.3 @@ -21,13 +21,19 @@
     1.4  structure CodegenArgs =
     1.5  struct
     1.6    val name = "HOL/inductive_codegen";
     1.7 -  type T = thm list Symtab.table * unit Graph.T;
     1.8 -  val empty = (Symtab.empty, Graph.empty);
     1.9 +  type T =
    1.10 +    {intros : thm list Symtab.table,
    1.11 +     graph : unit Graph.T,
    1.12 +     eqns : thm list Symtab.table};
    1.13 +  val empty =
    1.14 +    {intros = Symtab.empty, graph = Graph.empty, eqns = Symtab.empty};
    1.15    val copy = I;
    1.16    val prep_ext = I;
    1.17 -  fun merge ((tab1, graph1), (tab2, graph2)) =
    1.18 -    (Symtab.merge_multi Drule.eq_thm_prop (tab1, tab2),
    1.19 -     Graph.merge (K true) (graph1, graph2));
    1.20 +  fun merge ({intros=intros1, graph=graph1, eqns=eqns1},
    1.21 +    {intros=intros2, graph=graph2, eqns=eqns2}) =
    1.22 +    {intros = Symtab.merge_multi Drule.eq_thm_prop (intros1, intros2),
    1.23 +     graph = Graph.merge (K true) (graph1, graph2),
    1.24 +     eqns = Symtab.merge_multi Drule.eq_thm_prop (eqns1, eqns2)};
    1.25    fun print _ _ = ();
    1.26  end;
    1.27  
    1.28 @@ -39,24 +45,31 @@
    1.29  fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
    1.30  
    1.31  fun add (p as (thy, thm)) =
    1.32 -  let val (tab, graph) = CodegenData.get thy;
    1.33 +  let val {intros, graph, eqns} = CodegenData.get thy;
    1.34    in (case concl_of thm of
    1.35        _ $ (Const ("op :", _) $ _ $ t) => (case head_of t of
    1.36          Const (s, _) =>
    1.37            let val cs = foldr add_term_consts (prems_of thm, [])
    1.38            in (CodegenData.put
    1.39 -            (Symtab.update ((s,
    1.40 -               if_none (Symtab.lookup (tab, s)) [] @ [thm]), tab),
    1.41 -             foldr (uncurry (Graph.add_edge o pair s))
    1.42 -               (cs, foldl add_node (graph, s :: cs))) thy, thm)
    1.43 +            {intros = Symtab.update ((s,
    1.44 +               if_none (Symtab.lookup (intros, s)) [] @ [thm]), intros),
    1.45 +             graph = foldr (uncurry (Graph.add_edge o pair s))
    1.46 +               (cs, foldl add_node (graph, s :: cs)),
    1.47 +             eqns = eqns} thy, thm)
    1.48            end
    1.49        | _ => (warn thm; p))
    1.50 +    | _ $ (Const ("op =", _) $ t $ _) => (case head_of t of
    1.51 +        Const (s, _) =>
    1.52 +          (CodegenData.put {intros = intros, graph = graph,
    1.53 +             eqns = Symtab.update ((s,
    1.54 +               if_none (Symtab.lookup (eqns, s)) [] @ [thm]), eqns)} thy, thm)
    1.55 +      | _ => (warn thm; p))
    1.56      | _ => (warn thm; p))
    1.57    end;
    1.58  
    1.59  fun get_clauses thy s =
    1.60 -  let val (tab, graph) = CodegenData.get thy
    1.61 -  in case Symtab.lookup (tab, s) of
    1.62 +  let val {intros, graph, ...} = CodegenData.get thy
    1.63 +  in case Symtab.lookup (intros, s) of
    1.64        None => (case InductivePackage.get_inductive thy s of
    1.65          None => None
    1.66        | Some ({names, ...}, {intrs, ...}) => Some (names, intrs))
    1.67 @@ -64,7 +77,7 @@
    1.68          let val Some names = find_first
    1.69            (fn xs => s mem xs) (Graph.strong_conn graph)
    1.70          in Some (names,
    1.71 -          flat (map (fn s => the (Symtab.lookup (tab, s))) names))
    1.72 +          flat (map (fn s => the (Symtab.lookup (intros, s))) names))
    1.73          end
    1.74    end;
    1.75  
    1.76 @@ -80,6 +93,10 @@
    1.77           split_prod (1::p) ps t @ split_prod (2::p) ps u
    1.78       | _ => error "Inconsistent use of products") else [t];
    1.79  
    1.80 +fun full_split_prod (Const ("Pair", _) $ t $ u) =
    1.81 +      full_split_prod t @ full_split_prod u
    1.82 +  | full_split_prod t = [t];
    1.83 +
    1.84  datatype factors = FVar of int list list | FFix of int list list;
    1.85  
    1.86  exception Factors;
    1.87 @@ -143,18 +160,10 @@
    1.88  val term_vs = map (fst o fst o dest_Var) o term_vars;
    1.89  val terms_vs = distinct o flat o (map term_vs);
    1.90  
    1.91 -fun assoc' s tab key = (case assoc (tab, key) of
    1.92 -      None => error ("Unable to determine " ^ s ^ " of " ^ quote key)
    1.93 -    | Some x => x);
    1.94 -
    1.95  (** collect all Vars in a term (with duplicates!) **)
    1.96  fun term_vTs t = map (apfst fst o dest_Var)
    1.97    (filter is_Var (foldl_aterms (op :: o Library.swap) ([], t)));
    1.98  
    1.99 -fun known_args _ _ [] = []
   1.100 -  | known_args vs i (t::ts) = if term_vs t subset vs then i::known_args vs (i+1) ts
   1.101 -      else known_args vs (i+1) ts;
   1.102 -
   1.103  fun get_args _ _ [] = ([], [])
   1.104    | get_args is i (x::xs) = (if i mem is then apfst else apsnd) (cons x)
   1.105        (get_args is (i+1) xs);
   1.106 @@ -183,7 +192,7 @@
   1.107          (fn (None, _) => [None]
   1.108            | (Some js, arg) => map Some
   1.109                (filter (fn Mode ((_, js'), _) => js=js') (modes_of modes arg)))
   1.110 -                (iss ~~ args)))) (assoc' "modes" modes name))
   1.111 +                (iss ~~ args)))) (the (assoc (modes, name))))
   1.112  
   1.113    in (case strip_comb t of
   1.114        (Const ("op =", Type (_, [T, _])), _) =>
   1.115 @@ -200,17 +209,18 @@
   1.116    find_first (is_some o snd) (ps ~~ map
   1.117      (fn Prem (us, t) => find_first (fn Mode ((_, is), _) =>
   1.118            let
   1.119 -            val (_, out_ts) = get_args is 1 us;
   1.120 -            val vTs = flat (map term_vTs out_ts);
   1.121 +            val (in_ts, out_ts) = get_args is 1 us;
   1.122 +            val (out_ts', in_ts') = partition (is_constrt thy) out_ts;
   1.123 +            val vTs = flat (map term_vTs out_ts');
   1.124              val dupTs = map snd (duplicates vTs) @
   1.125                mapfilter (curry assoc vTs) vs;
   1.126            in
   1.127 -            is subset known_args vs 1 us andalso
   1.128 -            forall (is_constrt thy) (snd (get_args is 1 us)) andalso
   1.129 +            terms_vs (in_ts @ in_ts') subset vs andalso
   1.130 +            forall (is_eqT o fastype_of) in_ts' andalso
   1.131              term_vs t subset vs andalso
   1.132              forall is_eqT dupTs
   1.133            end)
   1.134 -            (modes_of modes t)
   1.135 +            (modes_of modes t handle OPTION => [Mode (([], []), [])])
   1.136        | Sidecond t => if term_vs t subset vs then Some (Mode (([], []), []))
   1.137            else None) ps);
   1.138  
   1.139 @@ -262,6 +272,51 @@
   1.140    flat (separate [Pretty.str ",", Pretty.brk 1] (map single xs)) @
   1.141    [Pretty.str ")"]);
   1.142  
   1.143 +(* convert nested pairs to n-tuple *)
   1.144 +
   1.145 +fun conv_ntuple [_] t ps = ps
   1.146 +  | conv_ntuple [_, _] t ps = ps
   1.147 +  | conv_ntuple us t ps =
   1.148 +      let
   1.149 +        val xs = map (fn i => Pretty.str ("x" ^ string_of_int i))
   1.150 +          (1 upto length us);
   1.151 +        fun ntuple (ys as (x, T) :: xs) U =
   1.152 +          if T = U then (x, xs)
   1.153 +          else
   1.154 +            let
   1.155 +              val Type ("*", [U1, U2]) = U;
   1.156 +              val (p1, ys1) = ntuple ys U1;
   1.157 +              val (p2, ys2) = ntuple ys1 U2
   1.158 +            in (mk_tuple [p1, p2], ys2) end
   1.159 +      in
   1.160 +        [Pretty.str "Seq.map (fn", Pretty.brk 1,
   1.161 +         fst (ntuple (xs ~~ map fastype_of us) (HOLogic.dest_setT (fastype_of t))),
   1.162 +         Pretty.str " =>", Pretty.brk 1, mk_tuple xs, Pretty.str ")",
   1.163 +         Pretty.brk 1, parens (Pretty.block ps)]
   1.164 +      end;
   1.165 +
   1.166 +(* convert n-tuple to nested pairs *)
   1.167 +
   1.168 +fun conv_ntuple' fs T ps =
   1.169 +  let
   1.170 +    fun mk_x i = Pretty.str ("x" ^ string_of_int i);
   1.171 +    fun conv i js (Type ("*", [T, U])) =
   1.172 +          if js mem fs then
   1.173 +            let
   1.174 +              val (p, i') = conv i (1::js) T;
   1.175 +              val (q, i'') = conv i' (2::js) U
   1.176 +            in (mk_tuple [p, q], i'') end
   1.177 +          else (mk_x i, i+1)
   1.178 +      | conv i js _ = (mk_x i, i+1)
   1.179 +    val (p, i) = conv 1 [] T
   1.180 +  in
   1.181 +    if i > 3 then
   1.182 +      [Pretty.str "Seq.map (fn", Pretty.brk 1,
   1.183 +       mk_tuple (map mk_x (1 upto i-1)), Pretty.str " =>", Pretty.brk 1,
   1.184 +       p, Pretty.str ")", Pretty.brk 1, parens (Pretty.block ps)]
   1.185 +    else ps
   1.186 +  end;
   1.187 +
   1.188  fun mk_v ((names, vs), s) = (case assoc (vs, s) of
   1.189        None => ((names, (s, [s])::vs), s)
   1.190      | Some xs => let val s' = variant names s in
   1.191 @@ -319,23 +374,32 @@
   1.192          let val s = variant names "x";
   1.193          in ((s::names, (s, t)::eqs), Var ((s, 0), fastype_of t)) end;
   1.194  
   1.195 +    fun compile_eq (gr, (s, t)) =
   1.196 +      apsnd (Pretty.block o cons (Pretty.str (s ^ " = ")) o single)
   1.197 +        (invoke_codegen thy dep false (gr, t));
   1.198 +
   1.199      val (in_ts, out_ts) = get_args is 1 ts;
   1.200      val ((all_vs', eqs), in_ts') =
   1.201        foldl_map check_constrt ((all_vs, []), in_ts);
   1.202  
   1.203 +    fun is_ind t = (case head_of t of
   1.204 +          Const (s, _) => s = "op =" orelse is_some (assoc (modes, s))
   1.205 +        | Var ((s, _), _) => s mem arg_vs);
   1.206 +
   1.207      fun compile_prems out_ts' vs names gr [] =
   1.208            let
   1.209              val (gr2, out_ps) = foldl_map
   1.210                (invoke_codegen thy dep false) (gr, out_ts);
   1.211 -            val (gr3, eq_ps) = foldl_map (fn (gr, (s, t)) =>
   1.212 -              apsnd (Pretty.block o cons (Pretty.str (s ^ " = ")) o single)
   1.213 -                (invoke_codegen thy dep false (gr, t))) (gr2, eqs);
   1.214 -            val (nvs, out_ts'') = foldl_map distinct_v
   1.215 -              ((names, map (fn x => (x, [x])) vs), out_ts');
   1.216 +            val (gr3, eq_ps) = foldl_map compile_eq (gr2, eqs);
   1.217 +            val ((names', eqs'), out_ts'') =
   1.218 +              foldl_map check_constrt ((names, []), out_ts');
   1.219 +            val (nvs, out_ts''') = foldl_map distinct_v
   1.220 +              ((names', map (fn x => (x, [x])) vs), out_ts'');
   1.221              val (gr4, out_ps') = foldl_map
   1.222 -              (invoke_codegen thy dep false) (gr3, out_ts'');
   1.223 +              (invoke_codegen thy dep false) (gr3, out_ts''');
   1.224 +            val (gr5, eq_ps') = foldl_map compile_eq (gr4, eqs')
   1.225            in
   1.226 -            (gr4, compile_match (snd nvs) eq_ps out_ps'
   1.227 +            (gr5, compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
   1.228                (Pretty.block [Pretty.str "Seq.single", Pretty.brk 1, mk_tuple out_ps])
   1.229                (Pretty.str "Seq.empty"))
   1.230            end
   1.231 @@ -345,36 +409,40 @@
   1.232              val Some (p, mode as Some (Mode ((_, js), _))) =
   1.233                select_mode_prem thy modes' (arg_vs union vs') ps;
   1.234              val ps' = filter_out (equal p) ps;
   1.235 +            val ((names', eqs), out_ts') =
   1.236 +              foldl_map check_constrt ((names, []), out_ts);
   1.237 +            val (nvs, out_ts'') = foldl_map distinct_v
   1.238 +              ((names', map (fn x => (x, [x])) vs), out_ts');
   1.239 +            val (gr0, out_ps) = foldl_map
   1.240 +              (invoke_codegen thy dep false) (gr, out_ts'');
   1.241 +            val (gr1, eq_ps) = foldl_map compile_eq (gr0, eqs)
   1.242            in
   1.243              (case p of
   1.244                 Prem (us, t) =>
   1.245                   let
   1.246 -                   val (in_ts, out_ts') = get_args js 1 us;
   1.247 -                   val (gr1, in_ps) = foldl_map
   1.248 -                     (invoke_codegen thy dep false) (gr, in_ts);
   1.249 -                   val (nvs, out_ts'') = foldl_map distinct_v
   1.250 -                     ((names, map (fn x => (x, [x])) vs), out_ts);
   1.251 -                   val (gr2, out_ps) = foldl_map
   1.252 -                     (invoke_codegen thy dep false) (gr1, out_ts'');
   1.253 -                   val (gr3, ps) = compile_expr thy dep false (gr2, (mode, t));
   1.254 -                   val (gr4, rest) = compile_prems out_ts' vs' (fst nvs) gr3 ps';
   1.255 +                   val (in_ts, out_ts''') = get_args js 1 us;
   1.256 +                   val (gr2, in_ps) = foldl_map
   1.257 +                     (invoke_codegen thy dep false) (gr1, in_ts);
   1.258 +                   val (gr3, ps) = if is_ind t then
   1.259 +                       apsnd (fn ps => ps @ [Pretty.brk 1, mk_tuple in_ps])
   1.260 +                         (compile_expr thy dep false (gr2, (mode, t)))
   1.261 +                     else
   1.262 +                       apsnd (fn p => conv_ntuple us t
   1.263 +                         [Pretty.str "Seq.of_list", Pretty.brk 1, p])
   1.264 +                           (invoke_codegen thy dep true (gr2, t));
   1.265 +                   val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps';
   1.266                   in
   1.267 -                   (gr4, compile_match (snd nvs) [] out_ps
   1.268 +                   (gr4, compile_match (snd nvs) eq_ps out_ps
   1.269                        (Pretty.block (ps @
   1.270 -                         [Pretty.brk 1, mk_tuple in_ps,
   1.271 -                          Pretty.str " :->", Pretty.brk 1, rest]))
   1.272 +                         [Pretty.str " :->", Pretty.brk 1, rest]))
   1.273                        (Pretty.str "Seq.empty"))
   1.274                   end
   1.275               | Sidecond t =>
   1.276                   let
   1.277 -                   val (gr1, side_p) = invoke_codegen thy dep true (gr, t);
   1.278 -                   val (nvs, out_ts') = foldl_map distinct_v
   1.279 -                     ((names, map (fn x => (x, [x])) vs), out_ts);
   1.280 -                   val (gr2, out_ps) = foldl_map
   1.281 -                     (invoke_codegen thy dep false) (gr1, out_ts')
   1.282 +                   val (gr2, side_p) = invoke_codegen thy dep true (gr1, t);
   1.283                     val (gr3, rest) = compile_prems [] vs' (fst nvs) gr2 ps';
   1.284                   in
   1.285 -                   (gr3, compile_match (snd nvs) [] out_ps
   1.286 +                   (gr3, compile_match (snd nvs) eq_ps out_ps
   1.287                        (Pretty.block [Pretty.str "?? ", side_p,
   1.288                          Pretty.str " :->", Pretty.brk 1, rest])
   1.289                        (Pretty.str "Seq.empty"))
   1.290 @@ -432,26 +500,35 @@
   1.291        (fn None => "X" | Some f' => string_of_factors [] f')
   1.292          (fs @ [Some f]))) factors));
   1.293  
   1.294 +fun prep_intrs intrs = map (rename_term o #prop o rep_thm o standard) intrs;
   1.295 +
   1.296 +fun constrain cs [] = []
   1.297 +  | constrain cs ((s, xs) :: ys) = (s, case assoc (cs, s) of
   1.298 +      None => xs
   1.299 +    | Some xs' => xs inter xs') :: constrain cs ys;
   1.300 +
   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 +          mk_ind_def thy gr dep names [] [] (prep_intrs intrs)))
   1.309              (gr, foldr add_term_consts (ts, []))
   1.310  
   1.311 -and mk_ind_def thy gr dep names intrs =
   1.312 +and mk_ind_def thy gr dep names modecs factorcs intrs =
   1.313    let val ids = map (mk_const_id (sign_of thy)) names
   1.314    in Graph.add_edge (hd ids, dep) gr handle Graph.UNDEF _ =>
   1.315      let
   1.316 +      val _ $ (_ $ _ $ u) = Logic.strip_imp_concl (hd intrs);
   1.317 +      val (_, args) = strip_comb u;
   1.318 +      val arg_vs = flat (map term_vs args);
   1.319 +
   1.320        fun dest_prem factors (_ $ (p as (Const ("op :", _) $ t $ u))) =
   1.321 -            (case head_of u of
   1.322 -               Const (name, _) => (case assoc (factors, name) of
   1.323 -                   None => Sidecond p
   1.324 -                 | Some f => Prem (split_prod [] f t, u))
   1.325 -             | Var ((name, _), _) => Prem (split_prod []
   1.326 -                 (the (assoc (factors, name))) t, u))
   1.327 +            (case assoc (factors, case head_of u of
   1.328 +                 Const (name, _) => name | Var ((name, _), _) => name) of
   1.329 +               None => Prem (full_split_prod t, u)
   1.330 +             | Some f => Prem (split_prod [] f t, u))
   1.331          | dest_prem factors (_ $ ((eq as Const ("op =", _)) $ t $ u)) =
   1.332              Prem ([t, u], eq)
   1.333          | dest_prem factors (_ $ t) = Sidecond t;
   1.334 @@ -466,42 +543,45 @@
   1.335               [(split_prod [] (the (assoc (factors, name))) t, prems)])))
   1.336          end;
   1.337  
   1.338 +      fun check_set (Const (s, _)) = s mem names orelse is_some (get_clauses thy s)
   1.339 +        | check_set (Var ((s, _), _)) = s mem arg_vs
   1.340 +        | check_set _ = false;
   1.341 +
   1.342        fun add_prod_factors extra_fs (fs, _ $ (Const ("op :", _) $ t $ u)) =
   1.343 -          (case apsome (get_clauses thy o fst) (try dest_Const (head_of u)) of
   1.344 -             Some None => fs
   1.345 -           | _ => infer_factors (sign_of thy) extra_fs
   1.346 -              (fs, (Some (FVar (prod_factors [] t)), u)))
   1.347 +            if check_set (head_of u)
   1.348 +            then infer_factors (sign_of thy) extra_fs
   1.349 +              (fs, (Some (FVar (prod_factors [] t)), u))
   1.350 +            else fs
   1.351          | add_prod_factors _ (fs, _) = fs;
   1.352  
   1.353 -      val intrs' = map (rename_term o #prop o rep_thm o standard) intrs;
   1.354 -      val _ $ (_ $ _ $ u) = Logic.strip_imp_concl (hd intrs');
   1.355 -      val (_, args) = strip_comb u;
   1.356 -      val arg_vs = flat (map term_vs args);
   1.357        val gr' = mk_extra_defs thy
   1.358          (Graph.add_edge (hd ids, dep)
   1.359 -          (Graph.new_node (hd ids, (None, "")) gr)) (hd ids) names intrs';
   1.360 +          (Graph.new_node (hd ids, (None, "")) gr)) (hd ids) names intrs;
   1.361        val (extra_modes, extra_factors) = lookup_modes gr' (hd ids);
   1.362 -      val fs = map (apsnd dest_factors)
   1.363 +      val fs = constrain factorcs (map (apsnd dest_factors)
   1.364          (foldl (add_prod_factors extra_factors) ([], flat (map (fn t =>
   1.365 -          Logic.strip_imp_concl t :: Logic.strip_imp_prems t) intrs')));
   1.366 -      val _ = (case map fst fs \\ names \\ arg_vs of
   1.367 -          [] => ()
   1.368 -        | xs => error ("Non-inductive sets: " ^ commas_quote xs));
   1.369 +          Logic.strip_imp_concl t :: Logic.strip_imp_prems t) intrs))));
   1.370        val factors = mapfilter (fn (name, f) =>
   1.371          if name mem arg_vs then None
   1.372          else Some (name, (map (curry assoc fs) arg_vs, f))) fs;
   1.373        val clauses =
   1.374 -        foldl (add_clause (fs @ map (apsnd snd) extra_factors)) ([], intrs');
   1.375 -      val modes = infer_modes thy extra_modes factors arg_vs clauses;
   1.376 +        foldl (add_clause (fs @ map (apsnd snd) extra_factors)) ([], intrs);
   1.377 +      val modes = constrain modecs
   1.378 +        (infer_modes thy extra_modes factors arg_vs clauses);
   1.379        val _ = print_factors factors;
   1.380        val _ = print_modes modes;
   1.381 -      val (gr'', s) = compile_preds thy gr' (hd ids) (terms_vs intrs') arg_vs
   1.382 +      val (gr'', s) = compile_preds thy gr' (hd ids) (terms_vs intrs) arg_vs
   1.383          (modes @ extra_modes) clauses;
   1.384      in
   1.385        (Graph.map_node (hd ids) (K (Some (Modes (modes, factors)), s)) gr'')
   1.386      end      
   1.387    end;
   1.388  
   1.389 +fun find_mode s u modes is = (case find_first (fn Mode ((_, js), _) => is=js)
   1.390 +  (modes_of modes u handle OPTION => []) of
   1.391 +     None => error ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
   1.392 +   | mode => mode);
   1.393 +
   1.394  fun mk_ind_call thy gr dep t u is_query = (case head_of u of
   1.395    Const (s, T) => (case (get_clauses thy s, get_assoc_code thy s T) of
   1.396         (None, _) => None
   1.397 @@ -512,17 +592,13 @@
   1.398              | mk_mode (((ts, mode), i), t) = ((ts @ [t], mode @ [i]), i+1);
   1.399  
   1.400             val gr1 = mk_extra_defs thy
   1.401 -             (mk_ind_def thy gr dep names intrs) dep names [u];
   1.402 +             (mk_ind_def thy gr dep names [] [] (prep_intrs intrs)) dep names [u];
   1.403             val (modes, factors) = lookup_modes gr1 dep;
   1.404             val ts = split_prod [] (snd (the (assoc (factors, s)))) t;
   1.405             val (ts', is) = if is_query then
   1.406                 fst (foldl mk_mode ((([], []), 1), ts))
   1.407               else (ts, 1 upto length ts);
   1.408 -           val mode = (case find_first (fn Mode ((_, js), _) => is=js)
   1.409 -                  (modes_of modes u) of
   1.410 -                None => error ("No such mode for " ^ s ^ ": " ^
   1.411 -                  string_of_mode ([], is))
   1.412 -              | mode => mode);
   1.413 +           val mode = find_mode s u modes is;
   1.414             val (gr2, in_ps) = foldl_map
   1.415               (invoke_codegen thy dep false) (gr1, ts');
   1.416             val (gr3, ps) = compile_expr thy dep false (gr2, (mode, u))
   1.417 @@ -533,13 +609,83 @@
   1.418       | _ => None)
   1.419    | _ => None);
   1.420  
   1.421 +fun list_of_indset thy gr dep brack u = (case head_of u of
   1.422 +  Const (s, T) => (case (get_clauses thy s, get_assoc_code thy s T) of
   1.423 +       (None, _) => None
   1.424 +     | (Some (names, intrs), None) =>
   1.425 +         let
   1.426 +           val gr1 = mk_extra_defs thy
   1.427 +             (mk_ind_def thy gr dep names [] [] (prep_intrs intrs)) dep names [u];
   1.428 +           val (modes, factors) = lookup_modes gr1 dep;
   1.429 +           val mode = find_mode s u modes [];
   1.430 +           val (gr2, ps) = compile_expr thy dep false (gr1, (mode, u))
   1.431 +         in
   1.432 +           Some (gr2, (if brack then parens else I)
   1.433 +             (Pretty.block ([Pretty.str "Seq.list_of", Pretty.brk 1,
   1.434 +               Pretty.str "("] @
   1.435 +               conv_ntuple' (snd (the (assoc (factors, s))))
   1.436 +                 (HOLogic.dest_setT (fastype_of u))
   1.437 +                 (ps @ [Pretty.brk 1, Pretty.str "()"]) @
   1.438 +               [Pretty.str ")"])))
   1.439 +         end
   1.440 +     | _ => None)
   1.441 +  | _ => None);
   1.442 +
   1.443 +fun clause_of_eqn eqn =
   1.444 +  let
   1.445 +    val (t, u) = HOLogic.dest_eq (HOLogic.dest_Trueprop (concl_of eqn));
   1.446 +    val (Const (s, T), ts) = strip_comb t;
   1.447 +    val (Ts, U) = strip_type T
   1.448 +  in
   1.449 +    rename_term
   1.450 +      (Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop (HOLogic.mk_mem
   1.451 +        (foldr1 HOLogic.mk_prod (ts @ [u]), Const (Sign.base_name s ^ "_aux",
   1.452 +          HOLogic.mk_setT (foldr1 HOLogic.mk_prodT (Ts @ [U])))))))
   1.453 +  end;
   1.454 +
   1.455 +fun mk_fun thy name eqns dep gr = 
   1.456 +  let val id = mk_const_id (sign_of thy) name
   1.457 +  in Graph.add_edge (id, dep) gr handle Graph.UNDEF _ =>
   1.458 +    let
   1.459 +      val clauses = map clause_of_eqn eqns;
   1.460 +      val pname = mk_const_id (sign_of thy) (Sign.base_name name ^ "_aux");
   1.461 +      val arity = length (snd (strip_comb (fst (HOLogic.dest_eq
   1.462 +        (HOLogic.dest_Trueprop (concl_of (hd eqns)))))));
   1.463 +      val mode = 1 upto arity;
   1.464 +      val vars = map (fn i => Pretty.str ("x" ^ string_of_int i)) mode;
   1.465 +      val s = Pretty.string_of (Pretty.block
   1.466 +        [mk_app false (Pretty.str ("fun " ^ id)) vars, Pretty.str " =",
   1.467 +         Pretty.brk 1, Pretty.str "Seq.hd", Pretty.brk 1,
   1.468 +         parens (Pretty.block [Pretty.str (modename thy pname ([], mode)),
   1.469 +           Pretty.brk 1, mk_tuple vars])]) ^ ";\n\n";
   1.470 +      val gr' = mk_ind_def thy (Graph.add_edge (id, dep)
   1.471 +        (Graph.new_node (id, (None, s)) gr)) id [pname]
   1.472 +        [(pname, [([], mode)])]
   1.473 +        [(pname, map (fn i => replicate i 2) (0 upto arity-1))]
   1.474 +        clauses;
   1.475 +      val (modes, _) = lookup_modes gr' dep;
   1.476 +      val _ = find_mode pname (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
   1.477 +        (Logic.strip_imp_concl (hd clauses))))) modes mode
   1.478 +    in gr' end
   1.479 +  end;
   1.480 +
   1.481  fun inductive_codegen thy gr dep brack (Const ("op :", _) $ t $ u) =
   1.482        ((case mk_ind_call thy gr dep (Term.no_dummy_patterns t) u false of
   1.483           None => None
   1.484         | Some (gr', call_p) => Some (gr', (if brack then parens else I)
   1.485             (Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"])))
   1.486          handle TERM _ => mk_ind_call thy gr dep t u true)
   1.487 -  | inductive_codegen thy gr dep brack _ = None;
   1.488 +  | inductive_codegen thy gr dep brack t = (case strip_comb t of
   1.489 +      (Const (s, _), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy), s) of
   1.490 +        None => list_of_indset thy gr dep brack t
   1.491 +      | Some eqns =>
   1.492 +          let
   1.493 +            val gr' = mk_fun thy s eqns dep gr
   1.494 +            val (gr'', ps) = foldl_map (invoke_codegen thy dep true) (gr', ts);
   1.495 +          in Some (gr'', mk_app brack (Pretty.str (mk_const_id
   1.496 +            (sign_of thy) s)) ps)
   1.497 +          end)
   1.498 +    | _ => None);
   1.499  
   1.500  val setup =
   1.501    [add_codegen "inductive" inductive_codegen,