55 val mk_qual_id: string -> string * string -> string |
55 val mk_qual_id: string -> string * string -> string |
56 val mk_const_id: string -> string -> codegr -> codegr * (string * string) |
56 val mk_const_id: string -> string -> codegr -> codegr * (string * string) |
57 val get_const_id: string -> codegr -> string * string |
57 val get_const_id: string -> codegr -> string * string |
58 val mk_type_id: string -> string -> codegr -> codegr * (string * string) |
58 val mk_type_id: string -> string -> codegr -> codegr * (string * string) |
59 val get_type_id: string -> codegr -> string * string |
59 val get_type_id: string -> codegr -> string * string |
60 val thyname_of_type: string -> theory -> string |
60 val thyname_of_type: theory -> string -> string |
61 val thyname_of_const: string -> theory -> string |
61 val thyname_of_const: theory -> string -> string |
62 val rename_terms: term list -> term list |
62 val rename_terms: term list -> term list |
63 val rename_term: term -> term |
63 val rename_term: term -> term |
64 val new_names: term -> string list -> string list |
64 val new_names: term -> string list -> string list |
65 val new_name: term -> string -> string |
65 val new_name: term -> string -> string |
66 val if_library: 'a -> 'a -> 'a |
66 val if_library: 'a -> 'a -> 'a |
494 fun add_edge_acyclic e (gr, x) = (Graph.add_edge_acyclic e gr, x); |
494 fun add_edge_acyclic e (gr, x) = (Graph.add_edge_acyclic e gr, x); |
495 fun del_nodes ks (gr, x) = (Graph.del_nodes ks gr, x); |
495 fun del_nodes ks (gr, x) = (Graph.del_nodes ks gr, x); |
496 fun map_node k f (gr, x) = (Graph.map_node k f gr, x); |
496 fun map_node k f (gr, x) = (Graph.map_node k f gr, x); |
497 fun new_node p (gr, x) = (Graph.new_node p gr, x); |
497 fun new_node p (gr, x) = (Graph.new_node p gr, x); |
498 |
498 |
499 fun theory_of_type s thy = |
499 fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN); |
500 if Sign.declared_tyname thy s |
500 |
501 then SOME (the_default thy (get_first (theory_of_type s) (Theory.parents_of thy))) |
501 fun thyname_of_type thy = |
502 else NONE; |
502 thyname_of thy (Type.the_tags (Sign.tsig_of thy)); |
503 |
503 |
504 fun theory_of_const s thy = |
504 fun thyname_of_const thy = |
505 if Sign.declared_const thy s |
505 thyname_of thy (Consts.the_tags (Sign.consts_of thy)); |
506 then SOME (the_default thy (get_first (theory_of_const s) (Theory.parents_of thy))) |
|
507 else NONE; |
|
508 |
|
509 fun thyname_of_type s thy = (case theory_of_type s thy of |
|
510 NONE => error ("thyname_of_type: no such type: " ^ quote s) |
|
511 | SOME thy' => Context.theory_name thy'); |
|
512 |
|
513 fun thyname_of_const s thy = (case theory_of_const s thy of |
|
514 NONE => error ("thyname_of_const: no such constant: " ^ quote s) |
|
515 | SOME thy' => Context.theory_name thy'); |
|
516 |
506 |
517 fun rename_terms ts = |
507 fun rename_terms ts = |
518 let |
508 let |
519 val names = List.foldr add_term_names |
509 val names = List.foldr add_term_names |
520 (map (fst o fst) (rev (fold Term.add_vars ts []))) ts; |
510 (map (fst o fst) (rev (fold Term.add_vars ts []))) ts; |
693 val (gr2, ps2) = codegens true (gr1, ts2); |
683 val (gr2, ps2) = codegens true (gr1, ts2); |
694 val (gr3, ps3) = codegens false (gr2, quotes_of ms); |
684 val (gr3, ps3) = codegens false (gr2, quotes_of ms); |
695 val (gr4, _) = invoke_tycodegen thy defs dep module false |
685 val (gr4, _) = invoke_tycodegen thy defs dep module false |
696 (gr3, funpow (length ts) (hd o tl o snd o dest_Type) T); |
686 (gr3, funpow (length ts) (hd o tl o snd o dest_Type) T); |
697 val (module', suffix) = (case get_defn thy defs s T of |
687 val (module', suffix) = (case get_defn thy defs s T of |
698 NONE => (if_library (thyname_of_const s thy) module, "") |
688 NONE => (if_library (thyname_of_const thy s) module, "") |
699 | SOME ((U, (module', _)), NONE) => |
689 | SOME ((U, (module', _)), NONE) => |
700 (if_library module' module, "") |
690 (if_library module' module, "") |
701 | SOME ((U, (module', _)), SOME i) => |
691 | SOME ((U, (module', _)), SOME i) => |
702 (if_library module' module, " def" ^ string_of_int i)); |
692 (if_library module' module, " def" ^ string_of_int i)); |
703 val node_id = s ^ suffix; |
693 val node_id = s ^ suffix; |
778 (invoke_tycodegen thy defs dep module false) |
768 (invoke_tycodegen thy defs dep module false) |
779 (gr, fst (args_of ms Ts)); |
769 (gr, fst (args_of ms Ts)); |
780 val (gr'', qs) = foldl_map |
770 val (gr'', qs) = foldl_map |
781 (invoke_tycodegen thy defs dep module false) |
771 (invoke_tycodegen thy defs dep module false) |
782 (gr', quotes_of ms); |
772 (gr', quotes_of ms); |
783 val module' = if_library (thyname_of_type s thy) module; |
773 val module' = if_library (thyname_of_type thy s) module; |
784 val node_id = s ^ " (type)"; |
774 val node_id = s ^ " (type)"; |
785 fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs) |
775 fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs) |
786 in SOME (case try (get_node gr'') node_id of |
776 in SOME (case try (get_node gr'') node_id of |
787 NONE => (case get_aux_code aux of |
777 NONE => (case get_aux_code aux of |
788 [] => (gr'', p module') |
778 [] => (gr'', p module') |