44 (string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory |
44 (string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory |
45 val add_tokentrfuns: |
45 val add_tokentrfuns: |
46 (string * string * (string -> string * real)) list -> theory -> theory |
46 (string * string * (string -> string * real)) list -> theory -> theory |
47 val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list |
47 val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list |
48 -> theory -> theory |
48 -> theory -> theory |
49 val parse_ast_translation: bool * string -> theory -> theory |
|
50 val parse_translation: bool * string -> theory -> theory |
|
51 val print_translation: bool * string -> theory -> theory |
|
52 val typed_print_translation: bool * string -> theory -> theory |
|
53 val print_ast_translation: bool * string -> theory -> theory |
|
54 val token_translation: string -> theory -> theory |
|
55 val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory |
49 val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory |
56 val del_trrules: (xstring * string) Syntax.trrule list -> theory -> theory |
50 val del_trrules: (xstring * string) Syntax.trrule list -> theory -> theory |
57 val add_trrules_i: ast Syntax.trrule list -> theory -> theory |
51 val add_trrules_i: ast Syntax.trrule list -> theory -> theory |
58 val del_trrules_i: ast Syntax.trrule list -> theory -> theory |
52 val del_trrules_i: ast Syntax.trrule list -> theory -> theory |
59 val add_path: string -> theory -> theory |
53 val add_path: string -> theory -> theory |
823 |
817 |
824 val add_tokentrfuns = map_syn o Syntax.extend_tokentrfuns; |
818 val add_tokentrfuns = map_syn o Syntax.extend_tokentrfuns; |
825 fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f)); |
819 fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f)); |
826 |
820 |
827 |
821 |
828 (* compile translation functions *) |
|
829 |
|
830 local |
|
831 |
|
832 fun advancedT false = "" |
|
833 | advancedT true = "Proof.context -> "; |
|
834 |
|
835 fun advancedN false = "" |
|
836 | advancedN true = "advanced_"; |
|
837 |
|
838 in |
|
839 |
|
840 fun parse_ast_translation (a, txt) = |
|
841 txt |> Context.use_let ("val parse_ast_translation: (string * (" ^ advancedT a ^ |
|
842 "Syntax.ast list -> Syntax.ast)) list") |
|
843 ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))") |
|
844 |> Context.theory_map; |
|
845 |
|
846 fun parse_translation (a, txt) = |
|
847 txt |> Context.use_let ("val parse_translation: (string * (" ^ advancedT a ^ |
|
848 "term list -> term)) list") |
|
849 ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))") |
|
850 |> Context.theory_map; |
|
851 |
|
852 fun print_translation (a, txt) = |
|
853 txt |> Context.use_let ("val print_translation: (string * (" ^ advancedT a ^ |
|
854 "term list -> term)) list") |
|
855 ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))") |
|
856 |> Context.theory_map; |
|
857 |
|
858 fun print_ast_translation (a, txt) = |
|
859 txt |> Context.use_let ("val print_ast_translation: (string * (" ^ advancedT a ^ |
|
860 "Syntax.ast list -> Syntax.ast)) list") |
|
861 ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))") |
|
862 |> Context.theory_map; |
|
863 |
|
864 fun typed_print_translation (a, txt) = |
|
865 txt |> Context.use_let ("val typed_print_translation: (string * (" ^ advancedT a ^ |
|
866 "bool -> typ -> term list -> term)) list") |
|
867 ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)") |
|
868 |> Context.theory_map; |
|
869 |
|
870 val token_translation = |
|
871 Context.use_let "val token_translation: (string * string * (string -> string * real)) list" |
|
872 "Context.map_theory (Sign.add_tokentrfuns token_translation)" |
|
873 #> Context.theory_map; |
|
874 |
|
875 end; |
|
876 |
|
877 |
|
878 (* translation rules *) |
822 (* translation rules *) |
879 |
823 |
880 fun gen_trrules f args thy = thy |> map_syn (fn syn => |
824 fun gen_trrules f args thy = thy |> map_syn (fn syn => |
881 let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args |
825 let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args |
882 in f (ProofContext.init thy) (is_logtype thy) syn rules syn end); |
826 in f (ProofContext.init thy) (is_logtype thy) syn rules syn end); |