author  berghofe 
Wed, 13 Nov 2002 15:28:41 +0100  
changeset 13708  a3a410782c95 
parent 13105  3d1e7a199bdc 
child 14162  f05f299512e9 
permissions  rwrr 
12453  1 
(* Title: HOL/inductive_codegen.ML 
11537  2 
ID: $Id$ 
11539  3 
Author: Stefan Berghofer, TU Muenchen 
4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 

11537  5 

11539  6 
Code generator for inductive predicates. 
11537  7 
*) 
8 

9 
signature INDUCTIVE_CODEGEN = 

10 
sig 

12557  11 
val add : theory attribute 
11537  12 
val setup : (theory > theory) list 
13 
end; 

14 

15 
structure InductiveCodegen : INDUCTIVE_CODEGEN = 

16 
struct 

17 

18 
open Codegen; 

19 

12557  20 
(**** theory data ****) 
21 

22 
structure CodegenArgs = 

23 
struct 

24 
val name = "HOL/inductive_codegen"; 

25 
type T = thm list Symtab.table; 

26 
val empty = Symtab.empty; 

27 
val copy = I; 

28 
val prep_ext = I; 

13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
13038
diff
changeset

29 
val merge = Symtab.merge_multi Drule.eq_thm_prop; 
12557  30 
fun print _ _ = (); 
31 
end; 

32 

33 
structure CodegenData = TheoryDataFun(CodegenArgs); 

34 

35 
fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^ 

36 
string_of_thm thm); 

11537  37 

12557  38 
fun add (p as (thy, thm)) = 
12562  39 
let val tab = CodegenData.get thy; 
12557  40 
in (case concl_of thm of 
41 
_ $ (Const ("op :", _) $ _ $ t) => (case head_of t of 

42 
Const (s, _) => (CodegenData.put (Symtab.update ((s, 

12562  43 
if_none (Symtab.lookup (tab, s)) [] @ [thm]), tab)) thy, thm) 
12557  44 
 _ => (warn thm; p)) 
45 
 _ => (warn thm; p)) 

12562  46 
end; 
12557  47 

48 
fun get_clauses thy s = 

49 
(case Symtab.lookup (CodegenData.get thy, s) of 

50 
None => (case InductivePackage.get_inductive thy s of 

51 
None => None 

52 
 Some ({names, ...}, {intrs, ...}) => Some (names, intrs)) 

53 
 Some thms => Some ([s], thms)); 

54 

55 

56 
(**** improper tuples ****) 

11537  57 

58 
fun prod_factors p (Const ("Pair", _) $ t $ u) = 

59 
p :: prod_factors (1::p) t @ prod_factors (2::p) u 

60 
 prod_factors p _ = []; 

61 

62 
fun split_prod p ps t = if p mem ps then (case t of 

63 
Const ("Pair", _) $ t $ u => 

64 
split_prod (1::p) ps t @ split_prod (2::p) ps u 

65 
 _ => error "Inconsistent use of products") else [t]; 

66 

12557  67 
datatype factors = FVar of int list list  FFix of int list list; 
68 

69 
exception Factors; 

70 

71 
fun mg_factor (FVar f) (FVar f') = FVar (f inter f') 

72 
 mg_factor (FVar f) (FFix f') = 

73 
if f' subset f then FFix f' else raise Factors 

74 
 mg_factor (FFix f) (FVar f') = 

75 
if f subset f' then FFix f else raise Factors 

76 
 mg_factor (FFix f) (FFix f') = 

77 
if f subset f' andalso f' subset f then FFix f else raise Factors; 

78 

79 
fun dest_factors (FVar f) = f 

80 
 dest_factors (FFix f) = f; 

81 

82 
fun infer_factors sg extra_fs (fs, (optf, t)) = 

83 
let fun err s = error (s ^ "\n" ^ Sign.string_of_term sg t) 

84 
in (case (optf, strip_comb t) of 

85 
(Some f, (Const (name, _), args)) => 

86 
(case assoc (extra_fs, name) of 

87 
None => overwrite (fs, (name, if_none 

88 
(apsome (mg_factor f) (assoc (fs, name))) f)) 

89 
 Some (fs', f') => (mg_factor f (FFix f'); 

90 
foldl (infer_factors sg extra_fs) 

91 
(fs, map (apsome FFix) fs' ~~ args))) 

92 
 (Some f, (Var ((name, _), _), [])) => 

93 
overwrite (fs, (name, if_none 

94 
(apsome (mg_factor f) (assoc (fs, name))) f)) 

95 
 (None, _) => fs 

96 
 _ => err "Illegal term") 

97 
handle Factors => err "Product factor mismatch in" 

98 
end; 

99 

11537  100 
fun string_of_factors p ps = if p mem ps then 
101 
"(" ^ string_of_factors (1::p) ps ^ ", " ^ string_of_factors (2::p) ps ^ ")" 

102 
else "_"; 

103 

12557  104 

11537  105 
(**** check if a term contains only constructor functions ****) 
106 

107 
fun is_constrt thy = 

108 
let 

109 
val cnstrs = flat (flat (map 

110 
(map (fn (_, (_, _, cs)) => map (apsnd length) cs) o #descr o snd) 

111 
(Symtab.dest (DatatypePackage.get_datatypes thy)))); 

112 
fun check t = (case strip_comb t of 

113 
(Var _, []) => true 

114 
 (Const (s, _), ts) => (case assoc (cnstrs, s) of 

115 
None => false 

116 
 Some i => length ts = i andalso forall check ts) 

117 
 _ => false) 

118 
in check end; 

119 

120 
(**** check if a type is an equality type (i.e. doesn't contain fun) ****) 

121 

122 
fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts 

123 
 is_eqT _ = true; 

124 

125 
(**** mode inference ****) 

126 

127 
val term_vs = map (fst o fst o dest_Var) o term_vars; 

128 
val terms_vs = distinct o flat o (map term_vs); 

129 

13038  130 
fun assoc' s tab key = (case assoc (tab, key) of 
131 
None => error ("Unable to determine " ^ s ^ " of " ^ quote key) 

132 
 Some x => x); 

133 

11537  134 
(** collect all Vars in a term (with duplicates!) **) 
135 
fun term_vTs t = map (apfst fst o dest_Var) 

136 
(filter is_Var (foldl_aterms (op :: o Library.swap) ([], t))); 

137 

138 
fun known_args _ _ [] = [] 

139 
 known_args vs i (t::ts) = if term_vs t subset vs then i::known_args vs (i+1) ts 

140 
else known_args vs (i+1) ts; 

141 

142 
fun get_args _ _ [] = ([], []) 

143 
 get_args is i (x::xs) = (if i mem is then apfst else apsnd) (cons x) 

144 
(get_args is (i+1) xs); 

145 

146 
fun merge xs [] = xs 

147 
 merge [] ys = ys 

148 
 merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys) 

149 
else y::merge (x::xs) ys; 

150 

151 
fun subsets i j = if i <= j then 

152 
let val is = subsets (i+1) j 

153 
in merge (map (fn ks => i::ks) is) is end 

154 
else [[]]; 

155 

12557  156 
fun cprod ([], ys) = [] 
157 
 cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys); 

158 

159 
fun cprods xss = foldr (map op :: o cprod) (xss, [[]]); 

160 

161 
datatype mode = Mode of (int list option list * int list) * mode option list; 

162 

163 
fun modes_of modes t = 

164 
let 

165 
fun mk_modes name args = flat 

166 
(map (fn (m as (iss, is)) => map (Mode o pair m) (cprods (map 

167 
(fn (None, _) => [None] 

168 
 (Some js, arg) => map Some 

169 
(filter (fn Mode ((_, js'), _) => js=js') (modes_of modes arg))) 

13038  170 
(iss ~~ args)))) (assoc' "modes" modes name)) 
12557  171 

172 
in (case strip_comb t of 

173 
(Const (name, _), args) => mk_modes name args 

13038  174 
 (Var ((name, _), _), args) => mk_modes name args 
175 
 (Free (name, _), args) => mk_modes name args) 

12557  176 
end; 
177 

178 
datatype indprem = Prem of term list * term  Sidecond of term; 

179 

11537  180 
fun select_mode_prem thy modes vs ps = 
181 
find_first (is_some o snd) (ps ~~ map 

12557  182 
(fn Prem (us, t) => find_first (fn Mode ((_, is), _) => 
11537  183 
let 
184 
val (_, out_ts) = get_args is 1 us; 

185 
val vTs = flat (map term_vTs out_ts); 

186 
val dupTs = map snd (duplicates vTs) @ 

187 
mapfilter (curry assoc vTs) vs; 

188 
in 

189 
is subset known_args vs 1 us andalso 

190 
forall (is_constrt thy) (snd (get_args is 1 us)) andalso 

12557  191 
term_vs t subset vs andalso 
11537  192 
forall is_eqT dupTs 
193 
end) 

12557  194 
(modes_of modes t) 
195 
 Sidecond t => if term_vs t subset vs then Some (Mode (([], []), [])) 

196 
else None) ps); 

11537  197 

12557  198 
fun check_mode_clause thy arg_vs modes (iss, is) (ts, ps) = 
11537  199 
let 
12557  200 
val modes' = modes @ mapfilter 
201 
(fn (_, None) => None  (v, Some js) => Some (v, [([], js)])) 

202 
(arg_vs ~~ iss); 

11537  203 
fun check_mode_prems vs [] = Some vs 
12557  204 
 check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of 
11537  205 
None => None 
206 
 Some (x, _) => check_mode_prems 

12557  207 
(case x of Prem (us, _) => vs union terms_vs us  _ => vs) 
11537  208 
(filter_out (equal x) ps)); 
12557  209 
val (in_ts', _) = get_args is 1 ts; 
11537  210 
val in_ts = filter (is_constrt thy) in_ts'; 
211 
val in_vs = terms_vs in_ts; 

212 
val concl_vs = terms_vs ts 

213 
in 

214 
forall is_eqT (map snd (duplicates (flat (map term_vTs in_ts')))) andalso 

215 
(case check_mode_prems (arg_vs union in_vs) ps of 

216 
None => false 

217 
 Some vs => concl_vs subset vs) 

218 
end; 

219 

220 
fun check_modes_pred thy arg_vs preds modes (p, ms) = 

221 
let val Some rs = assoc (preds, p) 

222 
in (p, filter (fn m => forall (check_mode_clause thy arg_vs modes m) rs) ms) end 

223 

224 
fun fixp f x = 

225 
let val y = f x 

226 
in if x = y then x else fixp f y end; 

227 

12557  228 
fun infer_modes thy extra_modes factors arg_vs preds = fixp (fn modes => 
11537  229 
map (check_modes_pred thy arg_vs preds (modes @ extra_modes)) modes) 
12557  230 
(map (fn (s, (fs, f)) => (s, cprod (cprods (map 
231 
(fn None => [None] 

232 
 Some f' => map Some (subsets 1 (length f' + 1))) fs), 

233 
subsets 1 (length f + 1)))) factors); 

11537  234 

235 
(**** code generation ****) 

236 

237 
fun mk_eq (x::xs) = 

238 
let fun mk_eqs _ [] = [] 

239 
 mk_eqs a (b::cs) = Pretty.str (a ^ " = " ^ b) :: mk_eqs b cs 

240 
in mk_eqs x xs end; 

241 

242 
fun mk_tuple xs = Pretty.block (Pretty.str "(" :: 

243 
flat (separate [Pretty.str ",", Pretty.brk 1] (map single xs)) @ 

244 
[Pretty.str ")"]); 

245 

246 
fun mk_v ((names, vs), s) = (case assoc (vs, s) of 

247 
None => ((names, (s, [s])::vs), s) 

248 
 Some xs => let val s' = variant names s in 

249 
((s'::names, overwrite (vs, (s, s'::xs))), s') end); 

250 

251 
fun distinct_v (nvs, Var ((s, 0), T)) = 

252 
apsnd (Var o rpair T o rpair 0) (mk_v (nvs, s)) 

253 
 distinct_v (nvs, t $ u) = 

254 
let 

255 
val (nvs', t') = distinct_v (nvs, t); 

256 
val (nvs'', u') = distinct_v (nvs', u); 

257 
in (nvs'', t' $ u') end 

258 
 distinct_v x = x; 

259 

260 
fun compile_match nvs eq_ps out_ps success_p fail_p = 

261 
let val eqs = flat (separate [Pretty.str " andalso", Pretty.brk 1] 

262 
(map single (flat (map (mk_eq o snd) nvs) @ eq_ps))); 

263 
in 

264 
Pretty.block 

265 
([Pretty.str "(fn ", mk_tuple out_ps, Pretty.str " =>", Pretty.brk 1] @ 

266 
(Pretty.block ((if eqs=[] then [] else Pretty.str "if " :: 

267 
[Pretty.block eqs, Pretty.brk 1, Pretty.str "then "]) @ 

268 
(success_p :: 

269 
(if eqs=[] then [] else [Pretty.brk 1, Pretty.str "else ", fail_p]))) :: 

270 
[Pretty.brk 1, Pretty.str " _ => ", fail_p, Pretty.str ")"])) 

271 
end; 

272 

12557  273 
fun modename thy s (iss, is) = space_implode "__" 
274 
(mk_const_id (sign_of thy) s :: 

275 
map (space_implode "_" o map string_of_int) (mapfilter I iss @ [is])); 

11537  276 

12557  277 
fun compile_expr thy dep brack (gr, (None, t)) = 
278 
apsnd single (invoke_codegen thy dep brack (gr, t)) 

279 
 compile_expr _ _ _ (gr, (Some _, Var ((name, _), _))) = 

280 
(gr, [Pretty.str name]) 

281 
 compile_expr thy dep brack (gr, (Some (Mode (mode, ms)), t)) = 

282 
let 

283 
val (Const (name, _), args) = strip_comb t; 

284 
val (gr', ps) = foldl_map 

285 
(compile_expr thy dep true) (gr, ms ~~ args); 

286 
in (gr', (if brack andalso not (null ps) then 

287 
single o parens o Pretty.block else I) 

288 
(flat (separate [Pretty.brk 1] 

289 
([Pretty.str (modename thy name mode)] :: ps)))) 

290 
end; 

291 

292 
fun compile_clause thy gr dep all_vs arg_vs modes (iss, is) (ts, ps) = 

11537  293 
let 
12557  294 
val modes' = modes @ mapfilter 
295 
(fn (_, None) => None  (v, Some js) => Some (v, [([], js)])) 

296 
(arg_vs ~~ iss); 

297 

11537  298 
fun check_constrt ((names, eqs), t) = 
299 
if is_constrt thy t then ((names, eqs), t) else 

300 
let val s = variant names "x"; 

301 
in ((s::names, (s, t)::eqs), Var ((s, 0), fastype_of t)) end; 

302 

12557  303 
val (in_ts, out_ts) = get_args is 1 ts; 
11537  304 
val ((all_vs', eqs), in_ts') = 
305 
foldl_map check_constrt ((all_vs, []), in_ts); 

306 

307 
fun compile_prems out_ts' vs names gr [] = 

308 
let 

12453  309 
val (gr2, out_ps) = foldl_map 
310 
(invoke_codegen thy dep false) (gr, out_ts); 

11537  311 
val (gr3, eq_ps) = foldl_map (fn (gr, (s, t)) => 
312 
apsnd (Pretty.block o cons (Pretty.str (s ^ " = ")) o single) 

12453  313 
(invoke_codegen thy dep false (gr, t))) (gr2, eqs); 
11537  314 
val (nvs, out_ts'') = foldl_map distinct_v 
315 
((names, map (fn x => (x, [x])) vs), out_ts'); 

12453  316 
val (gr4, out_ps') = foldl_map 
317 
(invoke_codegen thy dep false) (gr3, out_ts''); 

11537  318 
in 
319 
(gr4, compile_match (snd nvs) eq_ps out_ps' 

320 
(Pretty.block [Pretty.str "Seq.single", Pretty.brk 1, mk_tuple out_ps]) 

321 
(Pretty.str "Seq.empty")) 

322 
end 

323 
 compile_prems out_ts vs names gr ps = 

324 
let 

325 
val vs' = distinct (flat (vs :: map term_vs out_ts)); 

12557  326 
val Some (p, mode as Some (Mode ((_, js), _))) = 
327 
select_mode_prem thy modes' (arg_vs union vs') ps; 

11537  328 
val ps' = filter_out (equal p) ps; 
329 
in 

330 
(case p of 

12557  331 
Prem (us, t) => 
11537  332 
let 
12557  333 
val (in_ts, out_ts') = get_args js 1 us; 
12453  334 
val (gr1, in_ps) = foldl_map 
335 
(invoke_codegen thy dep false) (gr, in_ts); 

11537  336 
val (nvs, out_ts'') = foldl_map distinct_v 
337 
((names, map (fn x => (x, [x])) vs), out_ts); 

12557  338 
val (gr2, out_ps) = foldl_map 
339 
(invoke_codegen thy dep false) (gr1, out_ts''); 

340 
val (gr3, ps) = compile_expr thy dep false (gr2, (mode, t)); 

11537  341 
val (gr4, rest) = compile_prems out_ts' vs' (fst nvs) gr3 ps'; 
342 
in 

343 
(gr4, compile_match (snd nvs) [] out_ps 

12557  344 
(Pretty.block (ps @ 
11537  345 
[Pretty.brk 1, mk_tuple in_ps, 
346 
Pretty.str " :>", Pretty.brk 1, rest])) 

347 
(Pretty.str "Seq.empty")) 

348 
end 

349 
 Sidecond t => 

350 
let 

12453  351 
val (gr1, side_p) = invoke_codegen thy dep true (gr, t); 
11537  352 
val (nvs, out_ts') = foldl_map distinct_v 
353 
((names, map (fn x => (x, [x])) vs), out_ts); 

12453  354 
val (gr2, out_ps) = foldl_map 
355 
(invoke_codegen thy dep false) (gr1, out_ts') 

11537  356 
val (gr3, rest) = compile_prems [] vs' (fst nvs) gr2 ps'; 
357 
in 

358 
(gr3, compile_match (snd nvs) [] out_ps 

359 
(Pretty.block [Pretty.str "?? ", side_p, 

360 
Pretty.str " :>", Pretty.brk 1, rest]) 

361 
(Pretty.str "Seq.empty")) 

362 
end) 

363 
end; 

364 

365 
val (gr', prem_p) = compile_prems in_ts' [] all_vs' gr ps; 

366 
in 

367 
(gr', Pretty.block [Pretty.str "Seq.single inp :>", Pretty.brk 1, prem_p]) 

368 
end; 

369 

370 
fun compile_pred thy gr dep prfx all_vs arg_vs modes s cls mode = 

371 
let val (gr', cl_ps) = foldl_map (fn (gr, cl) => 

372 
compile_clause thy gr dep all_vs arg_vs modes mode cl) (gr, cls) 

373 
in 

374 
((gr', "and "), Pretty.block 

375 
([Pretty.block (separate (Pretty.brk 1) 

376 
(Pretty.str (prfx ^ modename thy s mode) :: map Pretty.str arg_vs) @ 

377 
[Pretty.str " inp ="]), 

378 
Pretty.brk 1] @ 

379 
flat (separate [Pretty.str " ++", Pretty.brk 1] (map single cl_ps)))) 

380 
end; 

381 

382 
fun compile_preds thy gr dep all_vs arg_vs modes preds = 

383 
let val ((gr', _), prs) = foldl_map (fn ((gr, prfx), (s, cls)) => 

384 
foldl_map (fn ((gr', prfx'), mode) => 

385 
compile_pred thy gr' dep prfx' all_vs arg_vs modes s cls mode) 

386 
((gr, prfx), the (assoc (modes, s)))) ((gr, "fun "), preds) 

387 
in 

388 
(gr', space_implode "\n\n" (map Pretty.string_of (flat prs)) ^ ";\n\n") 

389 
end; 

390 

391 
(**** processing of introduction rules ****) 

392 

12557  393 
exception Modes of 
394 
(string * (int list option list * int list) list) list * 

395 
(string * (int list list option list * int list list)) list; 

396 

397 
fun lookup_modes gr dep = apfst flat (apsnd flat (ListPair.unzip 

398 
(map ((fn (Some (Modes x), _) => x  _ => ([], [])) o Graph.get_node gr) 

399 
(Graph.all_preds gr [dep])))); 

400 

401 
fun string_of_mode (iss, is) = space_implode " > " (map 

402 
(fn None => "X" 

403 
 Some js => enclose "[" "]" (commas (map string_of_int js))) 

404 
(iss @ [Some is])); 

11537  405 

406 
fun print_modes modes = message ("Inferred modes:\n" ^ 

407 
space_implode "\n" (map (fn (s, ms) => s ^ ": " ^ commas (map 

408 
string_of_mode ms)) modes)); 

409 

410 
fun print_factors factors = message ("Factors:\n" ^ 

12557  411 
space_implode "\n" (map (fn (s, (fs, f)) => s ^ ": " ^ 
412 
space_implode " > " (map 

413 
(fn None => "X"  Some f' => string_of_factors [] f') 

414 
(fs @ [Some f]))) factors)); 

11537  415 

12557  416 
fun mk_extra_defs thy gr dep names ts = 
417 
foldl (fn (gr, name) => 

418 
if name mem names then gr 

419 
else (case get_clauses thy name of 

420 
None => gr 

421 
 Some (names, intrs) => 

422 
mk_ind_def thy gr dep names intrs)) 

423 
(gr, foldr add_term_consts (ts, [])) 

424 

425 
and mk_ind_def thy gr dep names intrs = 

11537  426 
let val ids = map (mk_const_id (sign_of thy)) names 
427 
in Graph.add_edge (hd ids, dep) gr handle Graph.UNDEF _ => 

428 
let 

12557  429 
fun dest_prem factors (_ $ (Const ("op :", _) $ t $ u)) = 
430 
(case head_of u of 

431 
Const (name, _) => Prem (split_prod [] 

432 
(the (assoc (factors, name))) t, u) 

433 
 Var ((name, _), _) => Prem (split_prod [] 

434 
(the (assoc (factors, name))) t, u)) 

435 
 dest_prem factors (_ $ ((eq as Const ("op =", _)) $ t $ u)) = 

436 
Prem ([t, u], eq) 

437 
 dest_prem factors (_ $ t) = Sidecond t; 

11537  438 

12557  439 
fun add_clause factors (clauses, intr) = 
11537  440 
let 
441 
val _ $ (_ $ t $ u) = Logic.strip_imp_concl intr; 

12557  442 
val Const (name, _) = head_of u; 
443 
val prems = map (dest_prem factors) (Logic.strip_imp_prems intr); 

11537  444 
in 
445 
(overwrite (clauses, (name, if_none (assoc (clauses, name)) [] @ 

12557  446 
[(split_prod [] (the (assoc (factors, name))) t, prems)]))) 
11537  447 
end; 
448 

12557  449 
fun add_prod_factors extra_fs (fs, _ $ (Const ("op :", _) $ t $ u)) = 
450 
infer_factors (sign_of thy) extra_fs 

451 
(fs, (Some (FVar (prod_factors [] t)), u)) 

452 
 add_prod_factors _ (fs, _) = fs; 

11537  453 

454 
val intrs' = map (rename_term o #prop o rep_thm o standard) intrs; 

455 
val _ $ (_ $ _ $ u) = Logic.strip_imp_concl (hd intrs'); 

456 
val (_, args) = strip_comb u; 

457 
val arg_vs = flat (map term_vs args); 

12557  458 
val gr' = mk_extra_defs thy 
459 
(Graph.add_edge (hd ids, dep) 

460 
(Graph.new_node (hd ids, (None, "")) gr)) (hd ids) names intrs'; 

461 
val (extra_modes', extra_factors) = lookup_modes gr' (hd ids); 

462 
val extra_modes = 

463 
("op =", [([], [1]), ([], [2]), ([], [1, 2])]) :: extra_modes'; 

464 
val fs = map (apsnd dest_factors) 

465 
(foldl (add_prod_factors extra_factors) ([], flat (map (fn t => 

466 
Logic.strip_imp_concl t :: Logic.strip_imp_prems t) intrs'))); 

467 
val _ = (case map fst fs \\ names \\ arg_vs of 

468 
[] => () 

469 
 xs => error ("Noninductive sets: " ^ commas_quote xs)); 

470 
val factors = mapfilter (fn (name, f) => 

471 
if name mem arg_vs then None 

472 
else Some (name, (map (curry assoc fs) arg_vs, f))) fs; 

473 
val clauses = 

474 
foldl (add_clause (fs @ map (apsnd snd) extra_factors)) ([], intrs'); 

475 
val modes = infer_modes thy extra_modes factors arg_vs clauses; 

476 
val _ = print_factors factors; 

11537  477 
val _ = print_modes modes; 
478 
val (gr'', s) = compile_preds thy gr' (hd ids) (terms_vs intrs') arg_vs 

479 
(modes @ extra_modes) clauses; 

480 
in 

481 
(Graph.map_node (hd ids) (K (Some (Modes (modes, factors)), s)) gr'') 

482 
end 

483 
end; 

484 

12557  485 
fun mk_ind_call thy gr dep t u is_query = (case head_of u of 
13038  486 
Const (s, T) => (case (get_clauses thy s, get_assoc_code thy s T) of 
487 
(None, _) => None 

488 
 (Some (names, intrs), None) => 

11537  489 
let 
12565  490 
fun mk_mode (((ts, mode), i), Const ("dummy_pattern", _)) = 
491 
((ts, mode), i+1) 

11537  492 
 mk_mode (((ts, mode), i), t) = ((ts @ [t], mode @ [i]), i+1); 
493 

12557  494 
val gr1 = mk_extra_defs thy 
495 
(mk_ind_def thy gr dep names intrs) dep names [u]; 

496 
val (modes, factors) = lookup_modes gr1 dep; 

497 
val ts = split_prod [] (snd (the (assoc (factors, s)))) t; 

498 
val (ts', is) = if is_query then 

11537  499 
fst (foldl mk_mode ((([], []), 1), ts)) 
500 
else (ts, 1 upto length ts); 

12557  501 
val mode = (case find_first (fn Mode ((_, js), _) => is=js) 
502 
(modes_of modes u) of 

503 
None => error ("No such mode for " ^ s ^ ": " ^ 

504 
string_of_mode ([], is)) 

505 
 mode => mode); 

12453  506 
val (gr2, in_ps) = foldl_map 
507 
(invoke_codegen thy dep false) (gr1, ts'); 

12557  508 
val (gr3, ps) = compile_expr thy dep false (gr2, (mode, u)) 
11537  509 
in 
12557  510 
Some (gr3, Pretty.block 
511 
(ps @ [Pretty.brk 1, mk_tuple in_ps])) 

13038  512 
end 
513 
 _ => None) 

11537  514 
 _ => None); 
515 

516 
fun inductive_codegen thy gr dep brack (Const ("op :", _) $ t $ u) = 

12565  517 
((case mk_ind_call thy gr dep (Term.no_dummy_patterns t) u false of 
11537  518 
None => None 
519 
 Some (gr', call_p) => Some (gr', (if brack then parens else I) 

12453  520 
(Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"]))) 
12565  521 
handle TERM _ => mk_ind_call thy gr dep t u true) 
11537  522 
 inductive_codegen thy gr dep brack _ = None; 
523 

12557  524 
val setup = 
525 
[add_codegen "inductive" inductive_codegen, 

526 
CodegenData.init, 

527 
add_attribute "ind" add]; 

11537  528 

529 
end; 

12453  530 

531 

532 
(**** combinators for code generated from inductive predicates ****) 

533 

534 
infix 5 :>; 

535 
infix 3 ++; 

536 

537 
fun s :> f = Seq.flat (Seq.map f s); 

538 

539 
fun s1 ++ s2 = Seq.append (s1, s2); 

540 

541 
fun ?? b = if b then Seq.single () else Seq.empty; 

542 

543 
fun ?! s = is_some (Seq.pull s); 

544 

12557  545 
fun op__61__1 x = Seq.single x; 
12453  546 

12557  547 
val op__61__2 = op__61__1; 
548 

549 
fun op__61__1_2 (x, y) = ?? (x = y); 