291 Pretty.block |
291 Pretty.block |
292 ([Pretty.str "(fn ", mk_tuple out_ps, Pretty.str " =>", Pretty.brk 1] @ |
292 ([Pretty.str "(fn ", mk_tuple out_ps, Pretty.str " =>", Pretty.brk 1] @ |
293 (Pretty.block ((if eqs=[] then [] else Pretty.str "if " :: |
293 (Pretty.block ((if eqs=[] then [] else Pretty.str "if " :: |
294 [Pretty.block eqs, Pretty.brk 1, Pretty.str "then "]) @ |
294 [Pretty.block eqs, Pretty.brk 1, Pretty.str "then "]) @ |
295 (success_p :: |
295 (success_p :: |
296 (if eqs=[] then [] else [Pretty.brk 1, Pretty.str "else Seq.empty"]))) :: |
296 (if eqs=[] then [] else [Pretty.brk 1, Pretty.str "else DSeq.empty"]))) :: |
297 (if can_fail then |
297 (if can_fail then |
298 [Pretty.brk 1, Pretty.str "| _ => Seq.empty)"] |
298 [Pretty.brk 1, Pretty.str "| _ => DSeq.empty)"] |
299 else [Pretty.str ")"]))) |
299 else [Pretty.str ")"]))) |
300 end; |
300 end; |
301 |
301 |
302 fun modename module s (iss, is) gr = |
302 fun modename module s (iss, is) gr = |
303 let val (gr', id) = if s = "op =" then (gr, ("", "equal")) |
303 let val (gr', id) = if s = "op =" then (gr, ("", "equal")) |
356 |
356 |
357 val (in_ts, out_ts) = get_args is 1 ts; |
357 val (in_ts, out_ts) = get_args is 1 ts; |
358 val ((all_vs', eqs), in_ts') = |
358 val ((all_vs', eqs), in_ts') = |
359 foldl_map check_constrt ((all_vs, []), in_ts); |
359 foldl_map check_constrt ((all_vs, []), in_ts); |
360 |
360 |
361 fun is_ind t = (case head_of t of |
|
362 Const (s, _) => s = "op =" orelse AList.defined (op =) modes s |
|
363 | Var ((s, _), _) => s mem arg_vs); |
|
364 |
|
365 fun compile_prems out_ts' vs names gr [] = |
361 fun compile_prems out_ts' vs names gr [] = |
366 let |
362 let |
367 val (gr2, out_ps) = foldl_map |
363 val (gr2, out_ps) = foldl_map |
368 (invoke_codegen thy defs dep module false) (gr, out_ts); |
364 (invoke_codegen thy defs dep module false) (gr, out_ts); |
369 val (gr3, eq_ps) = foldl_map compile_eq (gr2, eqs); |
365 val (gr3, eq_ps) = foldl_map compile_eq (gr2, eqs); |
374 val (gr4, out_ps') = foldl_map |
370 val (gr4, out_ps') = foldl_map |
375 (invoke_codegen thy defs dep module false) (gr3, out_ts'''); |
371 (invoke_codegen thy defs dep module false) (gr3, out_ts'''); |
376 val (gr5, eq_ps') = foldl_map compile_eq (gr4, eqs') |
372 val (gr5, eq_ps') = foldl_map compile_eq (gr4, eqs') |
377 in |
373 in |
378 (gr5, compile_match (snd nvs) (eq_ps @ eq_ps') out_ps' |
374 (gr5, compile_match (snd nvs) (eq_ps @ eq_ps') out_ps' |
379 (Pretty.block [Pretty.str "Seq.single", Pretty.brk 1, mk_tuple out_ps]) |
375 (Pretty.block [Pretty.str "DSeq.single", Pretty.brk 1, mk_tuple out_ps]) |
380 (exists (not o is_exhaustive) out_ts''')) |
376 (exists (not o is_exhaustive) out_ts''')) |
381 end |
377 end |
382 | compile_prems out_ts vs names gr ps = |
378 | compile_prems out_ts vs names gr ps = |
383 let |
379 let |
384 val vs' = distinct (op =) (List.concat (vs :: map term_vs out_ts)); |
380 val vs' = distinct (op =) (List.concat (vs :: map term_vs out_ts)); |
397 Prem (us, t) => |
393 Prem (us, t) => |
398 let |
394 let |
399 val (in_ts, out_ts''') = get_args js 1 us; |
395 val (in_ts, out_ts''') = get_args js 1 us; |
400 val (gr2, in_ps) = foldl_map |
396 val (gr2, in_ps) = foldl_map |
401 (invoke_codegen thy defs dep module true) (gr1, in_ts); |
397 (invoke_codegen thy defs dep module true) (gr1, in_ts); |
402 val (gr3, ps) = if is_ind t then |
398 val (gr3, ps) = (case body_type (fastype_of t) of |
|
399 Type ("bool", []) => |
403 apsnd (fn ps => ps @ |
400 apsnd (fn ps => ps @ |
404 (if null in_ps then [] else [Pretty.brk 1]) @ |
401 (if null in_ps then [] else [Pretty.brk 1]) @ |
405 separate (Pretty.brk 1) in_ps) |
402 separate (Pretty.brk 1) in_ps) |
406 (compile_expr thy defs dep module false modes |
403 (compile_expr thy defs dep module false modes |
407 (gr2, (mode, t))) |
404 (gr2, (mode, t))) |
408 else |
405 | _ => |
409 apsnd (fn p => [Pretty.str "Seq.of_list", Pretty.brk 1, p]) |
406 apsnd (fn p => [Pretty.str "DSeq.of_list", Pretty.brk 1, p]) |
410 (invoke_codegen thy defs dep module true (gr2, t)); |
407 (invoke_codegen thy defs dep module true (gr2, t))); |
411 val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps'; |
408 val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps'; |
412 in |
409 in |
413 (gr4, compile_match (snd nvs) eq_ps out_ps |
410 (gr4, compile_match (snd nvs) eq_ps out_ps |
414 (Pretty.block (ps @ |
411 (Pretty.block (ps @ |
415 [Pretty.str " :->", Pretty.brk 1, rest])) |
412 [Pretty.str " :->", Pretty.brk 1, rest])) |
427 end) |
424 end) |
428 end; |
425 end; |
429 |
426 |
430 val (gr', prem_p) = compile_prems in_ts' arg_vs all_vs' gr ps; |
427 val (gr', prem_p) = compile_prems in_ts' arg_vs all_vs' gr ps; |
431 in |
428 in |
432 (gr', Pretty.block [Pretty.str "Seq.single", Pretty.brk 1, inp, |
429 (gr', Pretty.block [Pretty.str "DSeq.single", Pretty.brk 1, inp, |
433 Pretty.str " :->", Pretty.brk 1, prem_p]) |
430 Pretty.str " :->", Pretty.brk 1, prem_p]) |
434 end; |
431 end; |
435 |
432 |
436 fun compile_pred thy defs gr dep module prfx all_vs arg_vs modes s cls mode = |
433 fun compile_pred thy defs gr dep module prfx all_vs arg_vs modes s cls mode = |
437 let |
434 let |
607 mk_const_id module' name |>>> |
604 mk_const_id module' name |>>> |
608 modename module' pname ([], mode); |
605 modename module' pname ([], mode); |
609 val vars = map (fn i => Pretty.str ("x" ^ string_of_int i)) mode; |
606 val vars = map (fn i => Pretty.str ("x" ^ string_of_int i)) mode; |
610 val s = Pretty.string_of (Pretty.block |
607 val s = Pretty.string_of (Pretty.block |
611 [mk_app false (Pretty.str ("fun " ^ snd fun_id)) vars, Pretty.str " =", |
608 [mk_app false (Pretty.str ("fun " ^ snd fun_id)) vars, Pretty.str " =", |
612 Pretty.brk 1, Pretty.str "Seq.hd", Pretty.brk 1, |
609 Pretty.brk 1, Pretty.str "DSeq.hd", Pretty.brk 1, |
613 parens (Pretty.block (separate (Pretty.brk 1) (Pretty.str mode_id :: |
610 parens (Pretty.block (separate (Pretty.brk 1) (Pretty.str mode_id :: |
614 vars)))]) ^ ";\n\n"; |
611 vars)))]) ^ ";\n\n"; |
615 val gr'' = mk_ind_def thy defs (add_edge (name, dep) |
612 val gr'' = mk_ind_def thy defs (add_edge (name, dep) |
616 (new_node (name, (NONE, module', s)) gr')) name [pname] module' |
613 (new_node (name, (NONE, module', s)) gr')) name [pname] module' |
617 [(pname, [([], mode)])] clauses 0; |
614 [(pname, [([], mode)])] clauses 0; |
637 in (mk_tuple [p, q], xs'') end |
634 in (mk_tuple [p, q], xs'') end |
638 else (hd xs, tl xs) |
635 else (hd xs, tl xs) |
639 in |
636 in |
640 if k > 0 then |
637 if k > 0 then |
641 Pretty.block |
638 Pretty.block |
642 [Pretty.str "Seq.map (fn", Pretty.brk 1, |
639 [Pretty.str "DSeq.map (fn", Pretty.brk 1, |
643 mk_tuple xs', Pretty.str " =>", Pretty.brk 1, fst (conv xs []), |
640 mk_tuple xs', Pretty.str " =>", Pretty.brk 1, fst (conv xs []), |
644 Pretty.str ")", Pretty.brk 1, parens p] |
641 Pretty.str ")", Pretty.brk 1, parens p] |
645 else p |
642 else p |
646 end; |
643 end; |
647 |
644 |
663 no_loose ts1 andalso no_loose its |
660 no_loose ts1 andalso no_loose its |
664 then |
661 then |
665 let val (gr', call_p) = mk_ind_call thy defs gr dep module true |
662 let val (gr', call_p) = mk_ind_call thy defs gr dep module true |
666 s T (ts1 @ ts2') names thyname k intrs |
663 s T (ts1 @ ts2') names thyname k intrs |
667 in SOME (gr', (if brack then parens else I) (Pretty.block |
664 in SOME (gr', (if brack then parens else I) (Pretty.block |
668 [Pretty.str "Seq.list_of", Pretty.brk 1, Pretty.str "(", |
665 [Pretty.str "DSeq.list_of", Pretty.brk 1, Pretty.str "(", |
669 conv_ntuple fs ots call_p, Pretty.str ")"])) |
666 conv_ntuple fs ots call_p, Pretty.str ")"])) |
670 end |
667 end |
671 else NONE |
668 else NONE |
672 end |
669 end |
673 | _ => NONE) |
670 | _ => NONE) |
701 Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add); |
698 Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add); |
702 |
699 |
703 end; |
700 end; |
704 |
701 |
705 |
702 |
|
703 (**** sequences with recursion depth limit ****) |
|
704 |
|
705 structure DSeq = |
|
706 struct |
|
707 |
|
708 fun maps f s 0 = Seq.empty |
|
709 | maps f s i = Seq.maps (fn a => f a i) (s (i - 1)); |
|
710 |
|
711 fun map f s i = Seq.map f (s i); |
|
712 |
|
713 fun append s1 s2 i = Seq.append (s1 i) (s2 i); |
|
714 |
|
715 fun interleave s1 s2 i = Seq.interleave (s1 i, s2 i); |
|
716 |
|
717 fun single x i = Seq.single x; |
|
718 |
|
719 fun empty i = Seq.empty; |
|
720 |
|
721 fun of_list xs i = Seq.of_list xs; |
|
722 |
|
723 fun list_of s = Seq.list_of (s ~1); |
|
724 |
|
725 fun pull s = Seq.pull (s ~1); |
|
726 |
|
727 fun hd s = Seq.hd (s ~1); |
|
728 |
|
729 end; |
|
730 |
|
731 |
706 (**** combinators for code generated from inductive predicates ****) |
732 (**** combinators for code generated from inductive predicates ****) |
707 |
733 |
708 infix 5 :->; |
734 infix 5 :->; |
709 infix 3 ++; |
735 infix 3 ++; |
710 |
736 |
711 fun s :-> f = Seq.maps f s; |
737 fun s :-> f = DSeq.maps f s; |
712 |
738 |
713 fun s1 ++ s2 = Seq.append s1 s2; |
739 fun s1 ++ s2 = DSeq.append s1 s2; |
714 |
740 |
715 fun ?? b = if b then Seq.single () else Seq.empty; |
741 fun ?? b = if b then DSeq.single () else DSeq.empty; |
716 |
742 |
717 fun ??? f g = f o g; |
743 fun ??? f g = f o g; |
718 |
744 |
719 fun ?! s = is_some (Seq.pull s); |
745 fun ?! s = is_some (DSeq.pull s); |
720 |
746 |
721 fun equal__1 x = Seq.single x; |
747 fun equal__1 x = DSeq.single x; |
722 |
748 |
723 val equal__2 = equal__1; |
749 val equal__2 = equal__1; |
724 |
750 |
725 fun equal__1_2 (x, y) = ?? (x = y); |
751 fun equal__1_2 (x, y) = ?? (x = y); |