496 #>> (fn class => Classparam (c, class)); |
496 #>> (fn class => Classparam (c, class)); |
497 fun stmt_fun ((vs, ty), raw_thms) = |
497 fun stmt_fun ((vs, ty), raw_thms) = |
498 let |
498 let |
499 val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty |
499 val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty |
500 then raw_thms |
500 then raw_thms |
501 else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms; |
501 else (map o apfst) (Code.expand_eta thy 1) raw_thms; |
502 in |
502 in |
503 fold_map (translate_tyvar_sort thy algbr funcgr) vs |
503 fold_map (translate_tyvar_sort thy algbr funcgr) vs |
504 ##>> translate_typ thy algbr funcgr ty |
504 ##>> translate_typ thy algbr funcgr ty |
505 ##>> fold_map (translate_eq thy algbr funcgr) thms |
505 ##>> fold_map (translate_eq thy algbr funcgr) thms |
506 #>> (fn info => Fun (c, info)) |
506 #>> (fn info => Fun (c, info)) |
632 in (not_undefined, (pat, body)) end; |
632 in (not_undefined, (pat, body)) end; |
633 val clauses = if null case_pats then let val ([v_ty], body) = |
633 val clauses = if null case_pats then let val ([v_ty], body) = |
634 Term.strip_abs_eta 1 (the_single ts_clause) |
634 Term.strip_abs_eta 1 (the_single ts_clause) |
635 in [(true, (Free v_ty, body))] end |
635 in [(true, (Free v_ty, body))] end |
636 else map (uncurry mk_clause) |
636 else map (uncurry mk_clause) |
637 (AList.make (Code_Unit.no_args thy) case_pats ~~ ts_clause); |
637 (AList.make (Code.no_args thy) case_pats ~~ ts_clause); |
638 fun retermify ty (_, (IVar x, body)) = |
638 fun retermify ty (_, (IVar x, body)) = |
639 (x, ty) `|-> body |
639 (x, ty) `|-> body |
640 | retermify _ (_, (pat, body)) = |
640 | retermify _ (_, (pat, body)) = |
641 let |
641 let |
642 val (IConst (_, (_, tys)), ts) = unfold_app pat; |
642 val (IConst (_, (_, tys)), ts) = unfold_app pat; |
810 | SOME thyname => filter belongs_here cs |
810 | SOME thyname => filter belongs_here cs |
811 end; |
811 end; |
812 fun read_const_expr "*" = ([], consts_of NONE) |
812 fun read_const_expr "*" = ([], consts_of NONE) |
813 | read_const_expr s = if String.isSuffix ".*" s |
813 | read_const_expr s = if String.isSuffix ".*" s |
814 then ([], consts_of (SOME (unsuffix ".*" s))) |
814 then ([], consts_of (SOME (unsuffix ".*" s))) |
815 else ([Code_Unit.read_const thy s], []); |
815 else ([Code.read_const thy s], []); |
816 in pairself flat o split_list o map read_const_expr end; |
816 in pairself flat o split_list o map read_const_expr end; |
817 |
817 |
818 fun code_depgr thy consts = |
818 fun code_depgr thy consts = |
819 let |
819 let |
820 val (_, eqngr) = Code_Preproc.obtain thy consts []; |
820 val (_, eqngr) = Code_Preproc.obtain thy consts []; |
837 |> maps (Graph.imm_succs eqngr) |
837 |> maps (Graph.imm_succs eqngr) |
838 |> subtract (op =) consts |
838 |> subtract (op =) consts |
839 |> map (the o Symtab.lookup mapping) |
839 |> map (the o Symtab.lookup mapping) |
840 |> distinct (op =); |
840 |> distinct (op =); |
841 val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss; |
841 val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss; |
842 fun namify consts = map (Code_Unit.string_of_const thy) consts |
842 fun namify consts = map (Code.string_of_const thy) consts |
843 |> commas; |
843 |> commas; |
844 val prgr = map (fn (consts, constss) => |
844 val prgr = map (fn (consts, constss) => |
845 { name = namify consts, ID = namify consts, dir = "", unfold = true, |
845 { name = namify consts, ID = namify consts, dir = "", unfold = true, |
846 path = "", parents = map namify constss }) conn; |
846 path = "", parents = map namify constss }) conn; |
847 in Present.display_graph prgr end; |
847 in Present.display_graph prgr end; |