# HG changeset patch # User wenzelm # Date 1169240905 -3600 # Node ID 6917be2e647dd237e0d15c903d5fda4c04319437 # Parent cde511c2a625febb1fbdfa2559cb0bc51aa92579 added various ML setup functions (from sign.ML, pure_thy.ML); diff -r cde511c2a625 -r 6917be2e647d src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Fri Jan 19 22:08:24 2007 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Fri Jan 19 22:08:25 2007 +0100 @@ -7,6 +7,14 @@ signature ISAR_CMD = sig + val generic_setup: string option -> theory -> theory + val parse_ast_translation: bool * string -> theory -> theory + val parse_translation: bool * string -> theory -> theory + val print_translation: bool * string -> theory -> theory + val typed_print_translation: bool * string -> theory -> theory + val print_ast_translation: bool * string -> theory -> theory + val token_translation: string -> theory -> theory + val oracle: bstring * string * string -> theory -> theory val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory @@ -121,6 +129,85 @@ struct +(** theory declarations **) + +(* generic_setup *) + +fun generic_setup NONE = (fn thy => thy |> Context.setup ()) + | generic_setup (SOME txt) = + ML_Context.use_let "val setup: theory -> theory" "Context.map_theory setup" txt + |> Context.theory_map; + + +(* translation functions *) + +local + +fun advancedT false = "" + | advancedT true = "Proof.context -> "; + +fun advancedN false = "" + | advancedN true = "advanced_"; + +in + +fun parse_ast_translation (a, txt) = + txt |> ML_Context.use_let ("val parse_ast_translation: (string * (" ^ advancedT a ^ + "Syntax.ast list -> Syntax.ast)) list") + ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))") + |> Context.theory_map; + +fun parse_translation (a, txt) = + txt |> ML_Context.use_let ("val parse_translation: (string * (" ^ advancedT a ^ + "term list -> term)) list") + ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))") + |> Context.theory_map; + +fun print_translation (a, txt) = + txt |> ML_Context.use_let ("val print_translation: (string * (" ^ advancedT a ^ + "term list -> term)) list") + ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))") + |> Context.theory_map; + +fun print_ast_translation (a, txt) = + txt |> ML_Context.use_let ("val print_ast_translation: (string * (" ^ advancedT a ^ + "Syntax.ast list -> Syntax.ast)) list") + ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))") + |> Context.theory_map; + +fun typed_print_translation (a, txt) = + txt |> ML_Context.use_let ("val typed_print_translation: (string * (" ^ advancedT a ^ + "bool -> typ -> term list -> term)) list") + ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)") + |> Context.theory_map; + +val token_translation = + ML_Context.use_let "val token_translation: (string * string * (string -> string * real)) list" + "Context.map_theory (Sign.add_tokentrfuns token_translation)" + #> Context.theory_map; + +end; + + +(* oracles *) + +fun oracle (name, T, oracle) = + let val txt = + "local\n\ + \ type T = " ^ T ^ ";\n\ + \ val oracle: theory -> T -> term = " ^ oracle ^ ";\n\ + \ val name = " ^ quote name ^ ";\n\ + \ exception Arg of T;\n\ + \ val _ = ML_Context.>> (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x));\n\ + \ val thy = ML_Context.the_context ();\n\ + \ val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\ + \in\n\ + \ fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\ + \end;\n"; + in ML_Context.use_mltext_update txt false end + |> Context.theory_map; + + (* axioms *) fun add_axms f args thy = @@ -145,7 +232,8 @@ (* declarations *) val declaration = - Context.use_let "val declaration: morphism -> Context.generic -> Context.generic" + ML_Context.use_let + "val declaration: Morphism.morphism -> Context.generic -> Context.generic" "Context.map_proof (LocalTheory.declaration declaration)" #> Context.proof_map; @@ -216,7 +304,7 @@ val welcome = Toplevel.imperative (writeln o Session.welcome); val exit = Toplevel.keep (fn state => - (Context.set_context (try Toplevel.generic_theory_of state); raise Toplevel.TERMINATE)); + (ML_Context.set_context (try Toplevel.generic_theory_of state); raise Toplevel.TERMINATE)); val quit = Toplevel.imperative quit; @@ -283,14 +371,14 @@ (* use ML text *) fun use path = Toplevel.keep (fn state => - Context.setmp (try Toplevel.generic_theory_of state) (ThyInfo.load_file false) path); + ML_Context.setmp (try Toplevel.generic_theory_of state) (ThyInfo.load_file false) path); (*passes changes of theory context*) -val use_mltext_theory = Toplevel.theory' o (Context.theory_map oo Context.use_mltext_update); +val use_mltext_theory = Toplevel.theory' o (Context.theory_map oo ML_Context.use_mltext_update); (*ignore result theory context*) fun use_mltext v txt = Toplevel.keep' (fn verb => fn state => - (Context.use_mltext txt (v andalso verb) (try Toplevel.generic_theory_of state))); + (ML_Context.use_mltext txt (v andalso verb) (try Toplevel.generic_theory_of state))); val use_commit = Toplevel.imperative Secure.commit; @@ -303,11 +391,11 @@ (* load theory files *) -fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name); -fun use_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy_only name); -fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name); +fun use_thy name = Toplevel.imperative (fn () => ML_Context.save ThyInfo.use_thy name); +fun use_thy_only name = Toplevel.imperative (fn () => ML_Context.save ThyInfo.use_thy_only name); +fun update_thy name = Toplevel.imperative (fn () => ML_Context.save ThyInfo.update_thy name); fun update_thy_only name = - Toplevel.imperative (fn () => Context.save ThyInfo.update_thy_only name); + Toplevel.imperative (fn () => ML_Context.save ThyInfo.update_thy_only name); (* present draft files *) @@ -388,7 +476,7 @@ val print_methods = Toplevel.unknown_theory o Toplevel.keep (Method.print_methods o Toplevel.theory_of); -val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations; +val print_antiquotations = Toplevel.imperative ThyOutput.print_antiquotations; val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => let @@ -503,7 +591,7 @@ fun present _ txt true node = OuterSyntax.check_text txt (SOME node) | present f (s, _) false node = - Context.setmp (try (Toplevel.cases_node I (Context.Proof o Proof.context_of)) node) f s; + ML_Context.setmp (try (Toplevel.cases_node I (Context.Proof o Proof.context_of)) node) f s; fun present_local_theory f (loc, txt) = Toplevel.present_local_theory loc (present f txt); fun present_proof f txt = Toplevel.print o Toplevel.present_proof (present f txt);