16 val setup: theory -> theory |
16 val setup: theory -> theory |
17 val code_pred: string -> Proof.context -> Proof.state |
17 val code_pred: string -> Proof.context -> Proof.state |
18 val code_pred_cmd: string -> Proof.context -> Proof.state |
18 val code_pred_cmd: string -> Proof.context -> Proof.state |
19 val print_alternative_rules: theory -> theory (*FIXME diagnostic command?*) |
19 val print_alternative_rules: theory -> theory (*FIXME diagnostic command?*) |
20 val do_proofs: bool ref |
20 val do_proofs: bool ref |
21 val pred_intros: theory -> string -> thm list |
21 val pred_intros : theory -> string -> thm list |
22 val get_nparams: theory -> string -> int |
22 val get_nparams : theory -> string -> int |
|
23 val pred_term_of : theory -> term -> term option |
23 end; |
24 end; |
24 |
25 |
25 structure Predicate_Compile : PREDICATE_COMPILE = |
26 structure Predicate_Compile : PREDICATE_COMPILE = |
26 struct |
27 struct |
27 |
28 |
268 fun cprods xss = foldr (map op :: o cprod) [[]] xss; |
269 fun cprods xss = foldr (map op :: o cprod) [[]] xss; |
269 |
270 |
270 datatype hmode = Mode of mode * int list * hmode option list; (*FIXME don't understand |
271 datatype hmode = Mode of mode * int list * hmode option list; (*FIXME don't understand |
271 why there is another mode type!?*) |
272 why there is another mode type!?*) |
272 |
273 |
273 fun modes_of modes t = |
274 fun modes_of_term modes t = |
274 let |
275 let |
275 val ks = 1 upto length (binder_types (fastype_of t)); |
276 val ks = 1 upto length (binder_types (fastype_of t)); |
276 val default = [Mode (([], ks), ks, [])]; |
277 val default = [Mode (([], ks), ks, [])]; |
277 fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) => |
278 fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) => |
278 let |
279 let |
286 if not (is_prefix op = prfx is) then [] else |
287 if not (is_prefix op = prfx is) then [] else |
287 let val is' = map (fn i => i - k) (List.drop (is, k)) |
288 let val is' = map (fn i => i - k) (List.drop (is, k)) |
288 in map (fn x => Mode (m, is', x)) (cprods (map |
289 in map (fn x => Mode (m, is', x)) (cprods (map |
289 (fn (NONE, _) => [NONE] |
290 (fn (NONE, _) => [NONE] |
290 | (SOME js, arg) => map SOME (filter |
291 | (SOME js, arg) => map SOME (filter |
291 (fn Mode (_, js', _) => js=js') (modes_of modes arg))) |
292 (fn Mode (_, js', _) => js=js') (modes_of_term modes arg))) |
292 (iss ~~ args1))) |
293 (iss ~~ args1))) |
293 end |
294 end |
294 end)) (AList.lookup op = modes name) |
295 end)) (AList.lookup op = modes name) |
295 |
296 |
296 in (case strip_comb t of |
297 in (case strip_comb t of |
315 terms_vs (in_ts @ in_ts') subset vs andalso |
316 terms_vs (in_ts @ in_ts') subset vs andalso |
316 forall (is_eqT o fastype_of) in_ts' andalso |
317 forall (is_eqT o fastype_of) in_ts' andalso |
317 term_vs t subset vs andalso |
318 term_vs t subset vs andalso |
318 forall is_eqT dupTs |
319 forall is_eqT dupTs |
319 end) |
320 end) |
320 (modes_of modes t handle Option => |
321 (modes_of_term modes t handle Option => |
321 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)) |
322 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)) |
322 | Negprem (us, t) => find_first (fn Mode (_, is, _) => |
323 | Negprem (us, t) => find_first (fn Mode (_, is, _) => |
323 length us = length is andalso |
324 length us = length is andalso |
324 terms_vs us subset vs andalso |
325 terms_vs us subset vs andalso |
325 term_vs t subset vs) |
326 term_vs t subset vs) |
326 (modes_of modes t handle Option => |
327 (modes_of_term modes t handle Option => |
327 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)) |
328 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)) |
328 | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], [])) |
329 | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], [])) |
329 else NONE |
330 else NONE |
330 ) ps); |
331 ) ps); |
331 |
332 |
1424 |
1425 |
1425 (*FIXME |
1426 (*FIXME |
1426 - Naming of auxiliary rules necessary? |
1427 - Naming of auxiliary rules necessary? |
1427 *) |
1428 *) |
1428 |
1429 |
|
1430 (* transformation for code generation *) |
|
1431 |
|
1432 fun pred_term_of thy t = let |
|
1433 val (vars, body) = strip_abs t |
|
1434 val (pred, all_args) = strip_comb body |
|
1435 val (name, T) = dest_Const pred |
|
1436 val (params, args) = chop (get_nparams thy name) all_args |
|
1437 val user_mode = flat (map_index |
|
1438 (fn (i, t) => case t of Bound j => if j < length vars then [] else [i+1] | _ => [i+1]) |
|
1439 args) |
|
1440 val (inargs, _) = get_args user_mode args |
|
1441 val all_modes = Symtab.dest (#modes (IndCodegenData.get thy)) |
|
1442 val modes = filter (fn Mode (_, is, _) => is = user_mode) (modes_of_term all_modes (list_comb (pred, params))) |
|
1443 fun compile m = list_comb (compile_expr thy all_modes (SOME m, list_comb (pred, params)), inargs) |
|
1444 in |
|
1445 case modes of |
|
1446 [] => (let val _ = error "No mode possible for this term" in NONE end) |
|
1447 | [m] => SOME (compile m) |
|
1448 | ms => (let val _ = warning "Multiple modes possible for this term" |
|
1449 in SOME (compile (hd ms)) end) |
|
1450 end; |
|
1451 |
1429 end; |
1452 end; |
|
1453 |