327 | is_exhaustive (Const (@{const_name Pair}, _) $ t $ u) = |
325 | is_exhaustive (Const (@{const_name Pair}, _) $ t $ u) = |
328 is_exhaustive t andalso is_exhaustive u |
326 is_exhaustive t andalso is_exhaustive u |
329 | is_exhaustive _ = false; |
327 | is_exhaustive _ = false; |
330 |
328 |
331 fun compile_match nvs eq_ps out_ps success_p can_fail = |
329 fun compile_match nvs eq_ps out_ps success_p can_fail = |
332 let val eqs = flat (separate [str " andalso", Pretty.brk 1] |
330 let val eqs = flat (separate [Codegen.str " andalso", Pretty.brk 1] |
333 (map single (maps (mk_eq o snd) nvs @ eq_ps))); |
331 (map single (maps (mk_eq o snd) nvs @ eq_ps))); |
334 in |
332 in |
335 Pretty.block |
333 Pretty.block |
336 ([str "(fn ", mk_tuple out_ps, str " =>", Pretty.brk 1] @ |
334 ([Codegen.str "(fn ", mk_tuple out_ps, Codegen.str " =>", Pretty.brk 1] @ |
337 (Pretty.block ((if null eqs then [] else str "if " :: |
335 (Pretty.block ((if null eqs then [] else Codegen.str "if " :: |
338 [Pretty.block eqs, Pretty.brk 1, str "then "]) @ |
336 [Pretty.block eqs, Pretty.brk 1, Codegen.str "then "]) @ |
339 (success_p :: |
337 (success_p :: |
340 (if null eqs then [] else [Pretty.brk 1, str "else DSeq.empty"]))) :: |
338 (if null eqs then [] else [Pretty.brk 1, Codegen.str "else DSeq.empty"]))) :: |
341 (if can_fail then |
339 (if can_fail then |
342 [Pretty.brk 1, str "| _ => DSeq.empty)"] |
340 [Pretty.brk 1, Codegen.str "| _ => DSeq.empty)"] |
343 else [str ")"]))) |
341 else [Codegen.str ")"]))) |
344 end; |
342 end; |
345 |
343 |
346 fun modename module s (iss, is) gr = |
344 fun modename module s (iss, is) gr = |
347 let val (id, gr') = if s = @{const_name HOL.eq} then (("", "equal"), gr) |
345 let val (id, gr') = if s = @{const_name HOL.eq} then (("", "equal"), gr) |
348 else mk_const_id module s gr |
346 else Codegen.mk_const_id module s gr |
349 in (space_implode "__" |
347 in (space_implode "__" |
350 (mk_qual_id module id :: |
348 (Codegen.mk_qual_id module id :: |
351 map (space_implode "_" o map string_of_int) (map_filter I iss @ [is])), gr') |
349 map (space_implode "_" o map string_of_int) (map_filter I iss @ [is])), gr') |
352 end; |
350 end; |
353 |
351 |
354 fun mk_funcomp brack s k p = (if brack then parens else I) |
352 fun mk_funcomp brack s k p = (if brack then Codegen.parens else I) |
355 (Pretty.block [Pretty.block ((if k = 0 then [] else [str "("]) @ |
353 (Pretty.block [Pretty.block ((if k = 0 then [] else [Codegen.str "("]) @ |
356 separate (Pretty.brk 1) (str s :: replicate k (str "|> ???")) @ |
354 separate (Pretty.brk 1) (Codegen.str s :: replicate k (Codegen.str "|> ???")) @ |
357 (if k = 0 then [] else [str ")"])), Pretty.brk 1, p]); |
355 (if k = 0 then [] else [Codegen.str ")"])), Pretty.brk 1, p]); |
358 |
356 |
359 fun compile_expr thy defs dep module brack modes (NONE, t) gr = |
357 fun compile_expr thy defs dep module brack modes (NONE, t) gr = |
360 apfst single (invoke_codegen thy defs dep module brack t gr) |
358 apfst single (Codegen.invoke_codegen thy defs dep module brack t gr) |
361 | compile_expr _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr = |
359 | compile_expr _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr = |
362 ([str name], gr) |
360 ([Codegen.str name], gr) |
363 | compile_expr thy defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr = |
361 | compile_expr thy defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr = |
364 (case strip_comb t of |
362 (case strip_comb t of |
365 (Const (name, _), args) => |
363 (Const (name, _), args) => |
366 if name = @{const_name HOL.eq} orelse AList.defined op = modes name then |
364 if name = @{const_name HOL.eq} orelse AList.defined op = modes name then |
367 let |
365 let |
368 val (args1, args2) = chop (length ms) args; |
366 val (args1, args2) = chop (length ms) args; |
369 val ((ps, mode_id), gr') = gr |> fold_map |
367 val ((ps, mode_id), gr') = gr |> fold_map |
370 (compile_expr thy defs dep module true modes) (ms ~~ args1) |
368 (compile_expr thy defs dep module true modes) (ms ~~ args1) |
371 ||>> modename module name mode; |
369 ||>> modename module name mode; |
372 val (ps', gr'') = (case mode of |
370 val (ps', gr'') = (case mode of |
373 ([], []) => ([str "()"], gr') |
371 ([], []) => ([Codegen.str "()"], gr') |
374 | _ => fold_map |
372 | _ => fold_map |
375 (invoke_codegen thy defs dep module true) args2 gr') |
373 (Codegen.invoke_codegen thy defs dep module true) args2 gr') |
376 in ((if brack andalso not (null ps andalso null ps') then |
374 in ((if brack andalso not (null ps andalso null ps') then |
377 single o parens o Pretty.block else I) |
375 single o Codegen.parens o Pretty.block else I) |
378 (flat (separate [Pretty.brk 1] |
376 (flat (separate [Pretty.brk 1] |
379 ([str mode_id] :: ps @ map single ps'))), gr') |
377 ([Codegen.str mode_id] :: ps @ map single ps'))), gr') |
380 end |
378 end |
381 else apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t)))) |
379 else apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t)))) |
382 (invoke_codegen thy defs dep module true t gr) |
380 (Codegen.invoke_codegen thy defs dep module true t gr) |
383 | _ => apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t)))) |
381 | _ => apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t)))) |
384 (invoke_codegen thy defs dep module true t gr)); |
382 (Codegen.invoke_codegen thy defs dep module true t gr)); |
385 |
383 |
386 fun compile_clause thy defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr = |
384 fun compile_clause thy defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr = |
387 let |
385 let |
388 val modes' = modes @ map_filter |
386 val modes' = modes @ map_filter |
389 (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [(([], js), false)])) |
387 (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [(([], js), false)])) |
394 else |
392 else |
395 let val s = Name.variant names "x"; |
393 let val s = Name.variant names "x"; |
396 in (Var ((s, 0), fastype_of t), (s::names, (s, t)::eqs)) end; |
394 in (Var ((s, 0), fastype_of t), (s::names, (s, t)::eqs)) end; |
397 |
395 |
398 fun compile_eq (s, t) gr = |
396 fun compile_eq (s, t) gr = |
399 apfst (Pretty.block o cons (str (s ^ " = ")) o single) |
397 apfst (Pretty.block o cons (Codegen.str (s ^ " = ")) o single) |
400 (invoke_codegen thy defs dep module false t gr); |
398 (Codegen.invoke_codegen thy defs dep module false t gr); |
401 |
399 |
402 val (in_ts, out_ts) = get_args is 1 ts; |
400 val (in_ts, out_ts) = get_args is 1 ts; |
403 val (in_ts', (all_vs', eqs)) = fold_map check_constrt in_ts (all_vs, []); |
401 val (in_ts', (all_vs', eqs)) = fold_map check_constrt in_ts (all_vs, []); |
404 |
402 |
405 fun compile_prems out_ts' vs names [] gr = |
403 fun compile_prems out_ts' vs names [] gr = |
406 let |
404 let |
407 val (out_ps, gr2) = |
405 val (out_ps, gr2) = |
408 fold_map (invoke_codegen thy defs dep module false) out_ts gr; |
406 fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts gr; |
409 val (eq_ps, gr3) = fold_map compile_eq eqs gr2; |
407 val (eq_ps, gr3) = fold_map compile_eq eqs gr2; |
410 val (out_ts'', (names', eqs')) = fold_map check_constrt out_ts' (names, []); |
408 val (out_ts'', (names', eqs')) = fold_map check_constrt out_ts' (names, []); |
411 val (out_ts''', nvs) = |
409 val (out_ts''', nvs) = |
412 fold_map distinct_v out_ts'' (names', map (fn x => (x, [x])) vs); |
410 fold_map distinct_v out_ts'' (names', map (fn x => (x, [x])) vs); |
413 val (out_ps', gr4) = |
411 val (out_ps', gr4) = |
414 fold_map (invoke_codegen thy defs dep module false) out_ts''' gr3; |
412 fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts''' gr3; |
415 val (eq_ps', gr5) = fold_map compile_eq eqs' gr4; |
413 val (eq_ps', gr5) = fold_map compile_eq eqs' gr4; |
416 val vs' = distinct (op =) (flat (vs :: map term_vs out_ts')); |
414 val vs' = distinct (op =) (flat (vs :: map term_vs out_ts')); |
417 val missing_vs = missing_vars vs' out_ts; |
415 val missing_vs = missing_vars vs' out_ts; |
418 val final_p = Pretty.block |
416 val final_p = Pretty.block |
419 [str "DSeq.single", Pretty.brk 1, mk_tuple out_ps] |
417 [Codegen.str "DSeq.single", Pretty.brk 1, mk_tuple out_ps] |
420 in |
418 in |
421 if null missing_vs then |
419 if null missing_vs then |
422 (compile_match (snd nvs) (eq_ps @ eq_ps') out_ps' |
420 (compile_match (snd nvs) (eq_ps @ eq_ps') out_ps' |
423 final_p (exists (not o is_exhaustive) out_ts'''), gr5) |
421 final_p (exists (not o is_exhaustive) out_ts'''), gr5) |
424 else |
422 else |
425 let |
423 let |
426 val (pat_p, gr6) = invoke_codegen thy defs dep module true |
424 val (pat_p, gr6) = Codegen.invoke_codegen thy defs dep module true |
427 (HOLogic.mk_tuple (map Var missing_vs)) gr5; |
425 (HOLogic.mk_tuple (map Var missing_vs)) gr5; |
428 val gen_p = mk_gen gr6 module true [] "" |
426 val gen_p = |
429 (HOLogic.mk_tupleT (map snd missing_vs)) |
427 Codegen.mk_gen gr6 module true [] "" |
|
428 (HOLogic.mk_tupleT (map snd missing_vs)) |
430 in |
429 in |
431 (compile_match (snd nvs) eq_ps' out_ps' |
430 (compile_match (snd nvs) eq_ps' out_ps' |
432 (Pretty.block [str "DSeq.generator ", gen_p, |
431 (Pretty.block [Codegen.str "DSeq.generator ", gen_p, |
433 str " :->", Pretty.brk 1, |
432 Codegen.str " :->", Pretty.brk 1, |
434 compile_match [] eq_ps [pat_p] final_p false]) |
433 compile_match [] eq_ps [pat_p] final_p false]) |
435 (exists (not o is_exhaustive) out_ts'''), |
434 (exists (not o is_exhaustive) out_ts'''), |
436 gr6) |
435 gr6) |
437 end |
436 end |
438 end |
437 end |
439 | compile_prems out_ts vs names ps gr = |
438 | compile_prems out_ts vs names ps gr = |
440 let |
439 let |
441 val vs' = distinct (op =) (flat (vs :: map term_vs out_ts)); |
440 val vs' = distinct (op =) (flat (vs :: map term_vs out_ts)); |
442 val (out_ts', (names', eqs)) = fold_map check_constrt out_ts (names, []); |
441 val (out_ts', (names', eqs)) = fold_map check_constrt out_ts (names, []); |
443 val (out_ts'', nvs) = fold_map distinct_v out_ts' (names', map (fn x => (x, [x])) vs); |
442 val (out_ts'', nvs) = fold_map distinct_v out_ts' (names', map (fn x => (x, [x])) vs); |
444 val (out_ps, gr0) = fold_map (invoke_codegen thy defs dep module false) out_ts'' gr; |
443 val (out_ps, gr0) = |
|
444 fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts'' gr; |
445 val (eq_ps, gr1) = fold_map compile_eq eqs gr0; |
445 val (eq_ps, gr1) = fold_map compile_eq eqs gr0; |
446 in |
446 in |
447 (case hd (select_mode_prem thy modes' vs' ps) of |
447 (case hd (select_mode_prem thy modes' vs' ps) of |
448 (p as Prem (us, t, is_set), (mode as Mode (_, js, _), []) :: _) => |
448 (p as Prem (us, t, is_set), (mode as Mode (_, js, _), []) :: _) => |
449 let |
449 let |
450 val ps' = filter_out (equal p) ps; |
450 val ps' = filter_out (equal p) ps; |
451 val (in_ts, out_ts''') = get_args js 1 us; |
451 val (in_ts, out_ts''') = get_args js 1 us; |
452 val (in_ps, gr2) = fold_map |
452 val (in_ps, gr2) = |
453 (invoke_codegen thy defs dep module true) in_ts gr1; |
453 fold_map (Codegen.invoke_codegen thy defs dep module true) in_ts gr1; |
454 val (ps, gr3) = |
454 val (ps, gr3) = |
455 if not is_set then |
455 if not is_set then |
456 apfst (fn ps => ps @ |
456 apfst (fn ps => ps @ |
457 (if null in_ps then [] else [Pretty.brk 1]) @ |
457 (if null in_ps then [] else [Pretty.brk 1]) @ |
458 separate (Pretty.brk 1) in_ps) |
458 separate (Pretty.brk 1) in_ps) |
459 (compile_expr thy defs dep module false modes |
459 (compile_expr thy defs dep module false modes |
460 (SOME mode, t) gr2) |
460 (SOME mode, t) gr2) |
461 else |
461 else |
462 apfst (fn p => Pretty.breaks [str "DSeq.of_list", str "(case", p, |
462 apfst (fn p => |
463 str "of", str "Set", str "xs", str "=>", str "xs)"]) |
463 Pretty.breaks [Codegen.str "DSeq.of_list", Codegen.str "(case", p, |
|
464 Codegen.str "of", Codegen.str "Set", Codegen.str "xs", Codegen.str "=>", |
|
465 Codegen.str "xs)"]) |
464 (*this is a very strong assumption about the generated code!*) |
466 (*this is a very strong assumption about the generated code!*) |
465 (invoke_codegen thy defs dep module true t gr2); |
467 (Codegen.invoke_codegen thy defs dep module true t gr2); |
466 val (rest, gr4) = compile_prems out_ts''' vs' (fst nvs) ps' gr3; |
468 val (rest, gr4) = compile_prems out_ts''' vs' (fst nvs) ps' gr3; |
467 in |
469 in |
468 (compile_match (snd nvs) eq_ps out_ps |
470 (compile_match (snd nvs) eq_ps out_ps |
469 (Pretty.block (ps @ |
471 (Pretty.block (ps @ |
470 [str " :->", Pretty.brk 1, rest])) |
472 [Codegen.str " :->", Pretty.brk 1, rest])) |
471 (exists (not o is_exhaustive) out_ts''), gr4) |
473 (exists (not o is_exhaustive) out_ts''), gr4) |
472 end |
474 end |
473 | (p as Sidecond t, [(_, [])]) => |
475 | (p as Sidecond t, [(_, [])]) => |
474 let |
476 let |
475 val ps' = filter_out (equal p) ps; |
477 val ps' = filter_out (equal p) ps; |
476 val (side_p, gr2) = invoke_codegen thy defs dep module true t gr1; |
478 val (side_p, gr2) = Codegen.invoke_codegen thy defs dep module true t gr1; |
477 val (rest, gr3) = compile_prems [] vs' (fst nvs) ps' gr2; |
479 val (rest, gr3) = compile_prems [] vs' (fst nvs) ps' gr2; |
478 in |
480 in |
479 (compile_match (snd nvs) eq_ps out_ps |
481 (compile_match (snd nvs) eq_ps out_ps |
480 (Pretty.block [str "?? ", side_p, |
482 (Pretty.block [Codegen.str "?? ", side_p, |
481 str " :->", Pretty.brk 1, rest]) |
483 Codegen.str " :->", Pretty.brk 1, rest]) |
482 (exists (not o is_exhaustive) out_ts''), gr3) |
484 (exists (not o is_exhaustive) out_ts''), gr3) |
483 end |
485 end |
484 | (_, (_, missing_vs) :: _) => |
486 | (_, (_, missing_vs) :: _) => |
485 let |
487 let |
486 val T = HOLogic.mk_tupleT (map snd missing_vs); |
488 val T = HOLogic.mk_tupleT (map snd missing_vs); |
487 val (_, gr2) = invoke_tycodegen thy defs dep module false T gr1; |
489 val (_, gr2) = Codegen.invoke_tycodegen thy defs dep module false T gr1; |
488 val gen_p = mk_gen gr2 module true [] "" T; |
490 val gen_p = Codegen.mk_gen gr2 module true [] "" T; |
489 val (rest, gr3) = compile_prems |
491 val (rest, gr3) = compile_prems |
490 [HOLogic.mk_tuple (map Var missing_vs)] vs' (fst nvs) ps gr2 |
492 [HOLogic.mk_tuple (map Var missing_vs)] vs' (fst nvs) ps gr2 |
491 in |
493 in |
492 (compile_match (snd nvs) eq_ps out_ps |
494 (compile_match (snd nvs) eq_ps out_ps |
493 (Pretty.block [str "DSeq.generator", Pretty.brk 1, |
495 (Pretty.block [Codegen.str "DSeq.generator", Pretty.brk 1, |
494 gen_p, str " :->", Pretty.brk 1, rest]) |
496 gen_p, Codegen.str " :->", Pretty.brk 1, rest]) |
495 (exists (not o is_exhaustive) out_ts''), gr3) |
497 (exists (not o is_exhaustive) out_ts''), gr3) |
496 end) |
498 end) |
497 end; |
499 end; |
498 |
500 |
499 val (prem_p, gr') = compile_prems in_ts' arg_vs all_vs' ps gr ; |
501 val (prem_p, gr') = compile_prems in_ts' arg_vs all_vs' ps gr ; |
500 in |
502 in |
501 (Pretty.block [str "DSeq.single", Pretty.brk 1, inp, |
503 (Pretty.block [Codegen.str "DSeq.single", Pretty.brk 1, inp, |
502 str " :->", Pretty.brk 1, prem_p], gr') |
504 Codegen.str " :->", Pretty.brk 1, prem_p], gr') |
503 end; |
505 end; |
504 |
506 |
505 fun compile_pred thy defs dep module prfx all_vs arg_vs modes s cls mode gr = |
507 fun compile_pred thy defs dep module prfx all_vs arg_vs modes s cls mode gr = |
506 let |
508 let |
507 val xs = map str (Name.variant_list arg_vs |
509 val xs = map Codegen.str (Name.variant_list arg_vs |
508 (map (fn i => "x" ^ string_of_int i) (snd mode))); |
510 (map (fn i => "x" ^ string_of_int i) (snd mode))); |
509 val ((cl_ps, mode_id), gr') = gr |> |
511 val ((cl_ps, mode_id), gr') = gr |> |
510 fold_map (fn cl => compile_clause thy defs |
512 fold_map (fn cl => compile_clause thy defs |
511 dep module all_vs arg_vs modes mode cl (mk_tuple xs)) cls ||>> |
513 dep module all_vs arg_vs modes mode cl (mk_tuple xs)) cls ||>> |
512 modename module s mode |
514 modename module s mode |
513 in |
515 in |
514 (Pretty.block |
516 (Pretty.block |
515 ([Pretty.block (separate (Pretty.brk 1) |
517 ([Pretty.block (separate (Pretty.brk 1) |
516 (str (prfx ^ mode_id) :: |
518 (Codegen.str (prfx ^ mode_id) :: |
517 map str arg_vs @ |
519 map Codegen.str arg_vs @ |
518 (case mode of ([], []) => [str "()"] | _ => xs)) @ |
520 (case mode of ([], []) => [Codegen.str "()"] | _ => xs)) @ |
519 [str " ="]), |
521 [Codegen.str " ="]), |
520 Pretty.brk 1] @ |
522 Pretty.brk 1] @ |
521 flat (separate [str " ++", Pretty.brk 1] (map single cl_ps))), (gr', "and ")) |
523 flat (separate [Codegen.str " ++", Pretty.brk 1] (map single cl_ps))), (gr', "and ")) |
522 end; |
524 end; |
523 |
525 |
524 fun compile_preds thy defs dep module all_vs arg_vs modes preds gr = |
526 fun compile_preds thy defs dep module all_vs arg_vs modes preds gr = |
525 let val (prs, (gr', _)) = fold_map (fn (s, cls) => |
527 let val (prs, (gr', _)) = fold_map (fn (s, cls) => |
526 fold_map (fn (mode, _) => fn (gr', prfx') => compile_pred thy defs |
528 fold_map (fn (mode, _) => fn (gr', prfx') => compile_pred thy defs |
527 dep module prfx' all_vs arg_vs modes s cls mode gr') |
529 dep module prfx' all_vs arg_vs modes s cls mode gr') |
528 (((the o AList.lookup (op =) modes) s))) preds (gr, "fun ") |
530 (((the o AList.lookup (op =) modes) s))) preds (gr, "fun ") |
529 in |
531 in |
530 (space_implode "\n\n" (map string_of (flat prs)) ^ ";\n\n", gr') |
532 (space_implode "\n\n" (map Codegen.string_of (flat prs)) ^ ";\n\n", gr') |
531 end; |
533 end; |
532 |
534 |
533 (**** processing of introduction rules ****) |
535 (**** processing of introduction rules ****) |
534 |
536 |
535 exception Modes of |
537 exception Modes of |
536 (string * ((int list option list * int list) * bool) list) list * |
538 (string * ((int list option list * int list) * bool) list) list * |
537 (string * (int option list * int)) list; |
539 (string * (int option list * int)) list; |
538 |
540 |
539 fun lookup_modes gr dep = apfst flat (apsnd flat (ListPair.unzip |
541 fun lookup_modes gr dep = apfst flat (apsnd flat (ListPair.unzip |
540 (map ((fn (SOME (Modes x), _, _) => x | _ => ([], [])) o get_node gr) |
542 (map ((fn (SOME (Modes x), _, _) => x | _ => ([], [])) o Codegen.get_node gr) |
541 (Graph.all_preds (fst gr) [dep])))); |
543 (Graph.all_preds (fst gr) [dep])))); |
542 |
544 |
543 fun print_arities arities = message ("Arities:\n" ^ |
545 fun print_arities arities = Codegen.message ("Arities:\n" ^ |
544 cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^ |
546 cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^ |
545 space_implode " -> " (map |
547 space_implode " -> " (map |
546 (fn NONE => "X" | SOME k' => string_of_int k') |
548 (fn NONE => "X" | SOME k' => string_of_int k') |
547 (ks @ [SOME k]))) arities)); |
549 (ks @ [SOME k]))) arities)); |
548 |
550 |
549 fun prep_intrs intrs = map (rename_term o #prop o rep_thm o Drule.export_without_context) intrs; |
551 fun prep_intrs intrs = |
|
552 map (Codegen.rename_term o #prop o rep_thm o Drule.export_without_context) intrs; |
550 |
553 |
551 fun constrain cs [] = [] |
554 fun constrain cs [] = [] |
552 | constrain cs ((s, xs) :: ys) = |
555 | constrain cs ((s, xs) :: ys) = |
553 (s, |
556 (s, |
554 case AList.lookup (op =) cs (s : string) of |
557 case AList.lookup (op =) cs (s : string) of |
662 let |
665 let |
663 val (t, u) = HOLogic.dest_eq (HOLogic.dest_Trueprop (concl_of eqn)); |
666 val (t, u) = HOLogic.dest_eq (HOLogic.dest_Trueprop (concl_of eqn)); |
664 val (Const (s, T), ts) = strip_comb t; |
667 val (Const (s, T), ts) = strip_comb t; |
665 val (Ts, U) = strip_type T |
668 val (Ts, U) = strip_type T |
666 in |
669 in |
667 rename_term (Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop |
670 Codegen.rename_term (Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop |
668 (list_comb (Const (s ^ "_aux", Ts @ [U] ---> HOLogic.boolT), ts @ [u])))) |
671 (list_comb (Const (s ^ "_aux", Ts @ [U] ---> HOLogic.boolT), ts @ [u])))) |
669 end; |
672 end; |
670 |
673 |
671 fun mk_fun thy defs name eqns dep module module' gr = |
674 fun mk_fun thy defs name eqns dep module module' gr = |
672 case try (get_node gr) name of |
675 case try (Codegen.get_node gr) name of |
673 NONE => |
676 NONE => |
674 let |
677 let |
675 val clauses = map clause_of_eqn eqns; |
678 val clauses = map clause_of_eqn eqns; |
676 val pname = name ^ "_aux"; |
679 val pname = name ^ "_aux"; |
677 val arity = length (snd (strip_comb (fst (HOLogic.dest_eq |
680 val arity = length (snd (strip_comb (fst (HOLogic.dest_eq |
678 (HOLogic.dest_Trueprop (concl_of (hd eqns))))))); |
681 (HOLogic.dest_Trueprop (concl_of (hd eqns))))))); |
679 val mode = 1 upto arity; |
682 val mode = 1 upto arity; |
680 val ((fun_id, mode_id), gr') = gr |> |
683 val ((fun_id, mode_id), gr') = gr |> |
681 mk_const_id module' name ||>> |
684 Codegen.mk_const_id module' name ||>> |
682 modename module' pname ([], mode); |
685 modename module' pname ([], mode); |
683 val vars = map (fn i => str ("x" ^ string_of_int i)) mode; |
686 val vars = map (fn i => Codegen.str ("x" ^ string_of_int i)) mode; |
684 val s = string_of (Pretty.block |
687 val s = Codegen.string_of (Pretty.block |
685 [mk_app false (str ("fun " ^ snd fun_id)) vars, str " =", |
688 [Codegen.mk_app false (Codegen.str ("fun " ^ snd fun_id)) vars, Codegen.str " =", |
686 Pretty.brk 1, str "DSeq.hd", Pretty.brk 1, |
689 Pretty.brk 1, Codegen.str "DSeq.hd", Pretty.brk 1, |
687 parens (Pretty.block (separate (Pretty.brk 1) (str mode_id :: |
690 Codegen.parens (Pretty.block (separate (Pretty.brk 1) (Codegen.str mode_id :: |
688 vars)))]) ^ ";\n\n"; |
691 vars)))]) ^ ";\n\n"; |
689 val gr'' = mk_ind_def thy defs (add_edge (name, dep) |
692 val gr'' = mk_ind_def thy defs (Codegen.add_edge (name, dep) |
690 (new_node (name, (NONE, module', s)) gr')) name [pname] module' |
693 (Codegen.new_node (name, (NONE, module', s)) gr')) name [pname] module' |
691 [(pname, [([], mode)])] clauses 0; |
694 [(pname, [([], mode)])] clauses 0; |
692 val (modes, _) = lookup_modes gr'' dep; |
695 val (modes, _) = lookup_modes gr'' dep; |
693 val _ = find_mode gr'' dep pname (head_of (HOLogic.dest_Trueprop |
696 val _ = find_mode gr'' dep pname (head_of (HOLogic.dest_Trueprop |
694 (Logic.strip_imp_concl (hd clauses)))) modes mode |
697 (Logic.strip_imp_concl (hd clauses)))) modes mode |
695 in (mk_qual_id module fun_id, gr'') end |
698 in (Codegen.mk_qual_id module fun_id, gr'') end |
696 | SOME _ => |
699 | SOME _ => |
697 (mk_qual_id module (get_const_id gr name), add_edge (name, dep) gr); |
700 (Codegen.mk_qual_id module (Codegen.get_const_id gr name), Codegen.add_edge (name, dep) gr); |
698 |
701 |
699 (* convert n-tuple to nested pairs *) |
702 (* convert n-tuple to nested pairs *) |
700 |
703 |
701 fun conv_ntuple fs ts p = |
704 fun conv_ntuple fs ts p = |
702 let |
705 let |
703 val k = length fs; |
706 val k = length fs; |
704 val xs = map_range (fn i => str ("x" ^ string_of_int i)) (k + 1); |
707 val xs = map_range (fn i => Codegen.str ("x" ^ string_of_int i)) (k + 1); |
705 val xs' = map (fn Bound i => nth xs (k - i)) ts; |
708 val xs' = map (fn Bound i => nth xs (k - i)) ts; |
706 fun conv xs js = |
709 fun conv xs js = |
707 if member (op =) fs js then |
710 if member (op =) fs js then |
708 let |
711 let |
709 val (p, xs') = conv xs (1::js); |
712 val (p, xs') = conv xs (1::js); |
736 if null (duplicates op = ots) andalso |
739 if null (duplicates op = ots) andalso |
737 no_loose ts1 andalso no_loose its |
740 no_loose ts1 andalso no_loose its |
738 then |
741 then |
739 let val (call_p, gr') = mk_ind_call thy defs dep module true |
742 let val (call_p, gr') = mk_ind_call thy defs dep module true |
740 s T (ts1 @ ts2') names thyname k intrs gr |
743 s T (ts1 @ ts2') names thyname k intrs gr |
741 in SOME ((if brack then parens else I) (Pretty.block |
744 in SOME ((if brack then Codegen.parens else I) (Pretty.block |
742 [str "Set", Pretty.brk 1, str "(DSeq.list_of", Pretty.brk 1, str "(", |
745 [Codegen.str "Set", Pretty.brk 1, Codegen.str "(DSeq.list_of", Pretty.brk 1, |
743 conv_ntuple fs ots call_p, str "))"]), |
746 Codegen.str "(", conv_ntuple fs ots call_p, Codegen.str "))"]), |
744 (*this is a very strong assumption about the generated code!*) |
747 (*this is a very strong assumption about the generated code!*) |
745 gr') |
748 gr') |
746 end |
749 end |
747 else NONE |
750 else NONE |
748 end |
751 end |
749 | _ => NONE) |
752 | _ => NONE) |
750 | _ => NONE |
753 | _ => NONE |
751 end |
754 end |
752 | (Const (s, T), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy)) s of |
755 | (Const (s, T), ts) => |
753 NONE => (case (get_clauses thy s, get_assoc_code thy (s, T)) of |
756 (case Symtab.lookup (#eqns (CodegenData.get thy)) s of |
|
757 NONE => |
|
758 (case (get_clauses thy s, Codegen.get_assoc_code thy (s, T)) of |
754 (SOME (names, thyname, k, intrs), NONE) => |
759 (SOME (names, thyname, k, intrs), NONE) => |
755 if length ts < k then NONE else SOME |
760 if length ts < k then NONE else SOME |
756 (let val (call_p, gr') = mk_ind_call thy defs dep module false |
761 (let val (call_p, gr') = mk_ind_call thy defs dep module false |
757 s T (map Term.no_dummy_patterns ts) names thyname k intrs gr |
762 s T (map Term.no_dummy_patterns ts) names thyname k intrs gr |
758 in (mk_funcomp brack "?!" |
763 in (mk_funcomp brack "?!" |
759 (length (binder_types T) - length ts) (parens call_p), gr') |
764 (length (binder_types T) - length ts) (Codegen.parens call_p), gr') |
760 end handle TERM _ => mk_ind_call thy defs dep module true |
765 end handle TERM _ => mk_ind_call thy defs dep module true |
761 s T ts names thyname k intrs gr ) |
766 s T ts names thyname k intrs gr ) |
762 | _ => NONE) |
767 | _ => NONE) |
763 | SOME eqns => |
768 | SOME eqns => |
764 let |
769 let |
765 val (_, thyname) :: _ = eqns; |
770 val (_, thyname) :: _ = eqns; |
766 val (id, gr') = mk_fun thy defs s (preprocess thy (map fst (rev eqns))) |
771 val (id, gr') = mk_fun thy defs s (Codegen.preprocess thy (map fst (rev eqns))) |
767 dep module (if_library thyname module) gr; |
772 dep module (Codegen.if_library thyname module) gr; |
768 val (ps, gr'') = fold_map |
773 val (ps, gr'') = fold_map |
769 (invoke_codegen thy defs dep module true) ts gr'; |
774 (Codegen.invoke_codegen thy defs dep module true) ts gr'; |
770 in SOME (mk_app brack (str id) ps, gr'') |
775 in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'') |
771 end) |
776 end) |
772 | _ => NONE); |
777 | _ => NONE); |
773 |
778 |
774 val setup = |
779 val setup = |
775 add_codegen "inductive" inductive_codegen #> |
780 Codegen.add_codegen "inductive" inductive_codegen #> |
776 Attrib.setup @{binding code_ind} |
781 Attrib.setup @{binding code_ind} |
777 (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) -- |
782 (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) -- |
778 Scan.option (Args.$$$ "params" |-- Args.colon |-- Parse.nat) >> uncurry add)) |
783 Scan.option (Args.$$$ "params" |-- Args.colon |-- Parse.nat) >> uncurry add)) |
779 "introduction rules for executable predicates"; |
784 "introduction rules for executable predicates"; |
780 |
785 |
818 [((Binding.name "quickcheckp", T), NoSyn)] [] |
823 [((Binding.name "quickcheckp", T), NoSyn)] [] |
819 [(Attrib.empty_binding, rl)] [] (Theory.copy thy); |
824 [(Attrib.empty_binding, rl)] [] (Theory.copy thy); |
820 val pred = HOLogic.mk_Trueprop (list_comb |
825 val pred = HOLogic.mk_Trueprop (list_comb |
821 (Const (Sign.intern_const thy' "quickcheckp", T), |
826 (Const (Sign.intern_const thy' "quickcheckp", T), |
822 map Term.dummy_pattern Ts)); |
827 map Term.dummy_pattern Ts)); |
823 val (code, gr) = setmp_CRITICAL mode ["term_of", "test", "random_ind"] |
828 val (code, gr) = setmp_CRITICAL Codegen.mode ["term_of", "test", "random_ind"] |
824 (generate_code_i thy' [] "Generated") [("testf", pred)]; |
829 (Codegen.generate_code_i thy' [] "Generated") [("testf", pred)]; |
825 val s = "structure TestTerm =\nstruct\n\n" ^ |
830 val s = "structure TestTerm =\nstruct\n\n" ^ |
826 cat_lines (map snd code) ^ |
831 cat_lines (map snd code) ^ |
827 "\nopen Generated;\n\n" ^ string_of |
832 "\nopen Generated;\n\n" ^ Codegen.string_of |
828 (Pretty.block [str "val () = Inductive_Codegen.test_fn :=", |
833 (Pretty.block [Codegen.str "val () = Inductive_Codegen.test_fn :=", |
829 Pretty.brk 1, str "(fn p =>", Pretty.brk 1, |
834 Pretty.brk 1, Codegen.str "(fn p =>", Pretty.brk 1, |
830 str "case Seq.pull (testf p) of", Pretty.brk 1, |
835 Codegen.str "case Seq.pull (testf p) of", Pretty.brk 1, |
831 str "SOME ", mk_tuple [mk_tuple (map (str o fst) args'), str "_"], |
836 Codegen.str "SOME ", mk_tuple [mk_tuple (map (Codegen.str o fst) args'), Codegen.str "_"], |
832 str " =>", Pretty.brk 1, str "SOME ", |
837 Codegen.str " =>", Pretty.brk 1, Codegen.str "SOME ", |
833 Pretty.enum "," "[" "]" |
838 Pretty.enum "," "[" "]" |
834 (map (fn (s, T) => Pretty.block |
839 (map (fn (s, T) => Pretty.block |
835 [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args'), |
840 [Codegen.mk_term_of gr "Generated" false T, Pretty.brk 1, Codegen.str s]) args'), |
836 Pretty.brk 1, |
841 Pretty.brk 1, |
837 str "| NONE => NONE);"]) ^ |
842 Codegen.str "| NONE => NONE);"]) ^ |
838 "\n\nend;\n"; |
843 "\n\nend;\n"; |
839 val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s; |
844 val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s; |
840 val values = Config.get ctxt random_values; |
845 val values = Config.get ctxt random_values; |
841 val bound = Config.get ctxt depth_bound; |
846 val bound = Config.get ctxt depth_bound; |
842 val start = Config.get ctxt depth_start; |
847 val start = Config.get ctxt depth_start; |