diff --git a/src/Pure/Isar/isar_cmd.ML b/src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML +++ b/src/Pure/Isar/isar_cmd.ML @@ -1,301 +1,301 @@ (* Title: Pure/Isar/isar_cmd.ML Author: Markus Wenzel, TU Muenchen Miscellaneous Isar commands. *) signature ISAR_CMD = sig val setup: Input.source -> theory -> theory val local_setup: Input.source -> Proof.context -> Proof.context val parse_ast_translation: Input.source -> theory -> theory val parse_translation: Input.source -> theory -> theory val print_translation: Input.source -> theory -> theory val typed_print_translation: Input.source -> theory -> theory val print_ast_translation: Input.source -> theory -> theory val translations: (xstring * string) Syntax.trrule list -> theory -> theory val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory val oracle: bstring * Position.range -> Input.source -> theory -> theory val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory val simproc_setup: string * Position.T -> string list -> Input.source -> local_theory -> local_theory val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition val terminal_proof: Method.text_range * Method.text_range option -> Toplevel.transition -> Toplevel.transition val default_proof: Toplevel.transition -> Toplevel.transition val immediate_proof: Toplevel.transition -> Toplevel.transition val done_proof: Toplevel.transition -> Toplevel.transition val skip_proof: Toplevel.transition -> Toplevel.transition val ml_diag: bool -> Input.source -> Toplevel.transition -> Toplevel.transition val diag_state: Proof.context -> Toplevel.state val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm} val pretty_theorems: bool -> Toplevel.state -> Pretty.T list val print_stmts: string list * (Facts.ref * Token.src list) list -> Toplevel.transition -> Toplevel.transition val print_thms: string list * (Facts.ref * Token.src list) list -> Toplevel.transition -> Toplevel.transition val print_prfs: bool -> string list * (Facts.ref * Token.src list) list option -> Toplevel.transition -> Toplevel.transition val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition val print_type: (string list * (string * string option)) -> Toplevel.transition -> Toplevel.transition end; structure Isar_Cmd: ISAR_CMD = struct (** theory declarations **) (* generic setup *) fun setup source = ML_Context.expression (Input.pos_of source) (ML_Lex.read "Theory.setup (" @ ML_Lex.read_source source @ ML_Lex.read ")") |> Context.theory_map; fun local_setup source = ML_Context.expression (Input.pos_of source) (ML_Lex.read "Theory.local_setup (" @ ML_Lex.read_source source @ ML_Lex.read ")") |> Context.proof_map; (* translation functions *) fun parse_ast_translation source = ML_Context.expression (Input.pos_of source) (ML_Lex.read "Theory.setup (Sign.parse_ast_translation (" @ ML_Lex.read_source source @ ML_Lex.read "))") |> Context.theory_map; fun parse_translation source = ML_Context.expression (Input.pos_of source) (ML_Lex.read "Theory.setup (Sign.parse_translation (" @ ML_Lex.read_source source @ ML_Lex.read "))") |> Context.theory_map; fun print_translation source = ML_Context.expression (Input.pos_of source) (ML_Lex.read "Theory.setup (Sign.print_translation (" @ ML_Lex.read_source source @ ML_Lex.read "))") |> Context.theory_map; fun typed_print_translation source = ML_Context.expression (Input.pos_of source) (ML_Lex.read "Theory.setup (Sign.typed_print_translation (" @ ML_Lex.read_source source @ ML_Lex.read "))") |> Context.theory_map; fun print_ast_translation source = ML_Context.expression (Input.pos_of source) (ML_Lex.read "Theory.setup (Sign.print_ast_translation (" @ ML_Lex.read_source source @ ML_Lex.read "))") |> Context.theory_map; (* translation rules *) fun read_trrules thy raw_rules = let val ctxt = Proof_Context.init_global thy; val read_root = #1 o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} ctxt; in raw_rules |> map (Syntax.map_trrule (fn (r, s) => Syntax_Phases.parse_ast_pattern ctxt (read_root r, s))) end; fun translations args thy = Sign.add_trrules (read_trrules thy args) thy; fun no_translations args thy = Sign.del_trrules (read_trrules thy args) thy; (* oracles *) fun oracle (name, range) source = ML_Context.expression (Input.pos_of source) (ML_Lex.read "val " @ - ML_Lex.read_set_range range name @ + ML_Lex.read_range range name @ ML_Lex.read (" = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (" ^ ML_Syntax.make_binding (name, #1 range) ^ ", ") @ ML_Lex.read_source source @ ML_Lex.read "))))") |> Context.theory_map; (* declarations *) fun declaration {syntax, pervasive} source = ML_Context.expression (Input.pos_of source) (ML_Lex.read ("Theory.local_setup (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", pervasive = " ^ Bool.toString pervasive ^ "} (") @ ML_Lex.read_source source @ ML_Lex.read "))") |> Context.proof_map; (* simprocs *) fun simproc_setup name lhss source = ML_Context.expression (Input.pos_of source) (ML_Lex.read ("Theory.local_setup (Simplifier.define_simproc_cmd (" ^ ML_Syntax.make_binding name ^ ") {lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = (") @ ML_Lex.read_source source @ ML_Lex.read ")})") |> Context.proof_map; (* local endings *) fun local_qed m = Toplevel.proof (Proof.local_qed (m, true)); val local_terminal_proof = Toplevel.proof o Proof.local_future_terminal_proof; val local_default_proof = Toplevel.proof Proof.local_default_proof; val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof; val local_done_proof = Toplevel.proof Proof.local_done_proof; val local_skip_proof = Toplevel.proof' Proof.local_skip_proof; (* global endings *) fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true))); val global_terminal_proof = Toplevel.end_proof o K o Proof.global_future_terminal_proof; val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof); val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof); val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof; val global_done_proof = Toplevel.end_proof (K Proof.global_done_proof); (* common endings *) fun qed m = local_qed m o global_qed m; fun terminal_proof m = local_terminal_proof m o global_terminal_proof m; val default_proof = local_default_proof o global_default_proof; val immediate_proof = local_immediate_proof o global_immediate_proof; val done_proof = local_done_proof o global_done_proof; val skip_proof = local_skip_proof o global_skip_proof; (* diagnostic ML evaluation *) structure Diag_State = Proof_Data ( type T = Toplevel.state option; fun init _ = NONE; ); fun ml_diag verbose source = Toplevel.keep (fn state => let val opt_ctxt = try Toplevel.generic_theory_of state |> Option.map (Context.proof_of #> Diag_State.put (SOME state)); val flags = ML_Compiler.verbose verbose ML_Compiler.flags; in ML_Context.eval_source_in opt_ctxt flags source end); fun diag_state ctxt = (case Diag_State.get ctxt of SOME st => st | NONE => Toplevel.init_toplevel ()); val diag_goal = Proof.goal o Toplevel.proof_of o diag_state; val _ = Theory.setup (ML_Antiquotation.value (Binding.qualify true "Isar" \<^binding>\state\) (Scan.succeed "Isar_Cmd.diag_state ML_context") #> ML_Antiquotation.value (Binding.qualify true "Isar" \<^binding>\goal\) (Scan.succeed "Isar_Cmd.diag_goal ML_context")); (* theorems of theory or proof context *) fun pretty_theorems verbose st = if Toplevel.is_proof st then Proof_Context.pretty_local_facts verbose (Toplevel.context_of st) else let val ctxt = Toplevel.context_of st; val prev_thys = (case Toplevel.previous_theory_of st of SOME thy => [thy] | NONE => Theory.parents_of (Proof_Context.theory_of ctxt)); in Proof_Display.pretty_theorems_diff verbose prev_thys ctxt end; (* print theorems, terms, types etc. *) local fun string_of_stmts ctxt args = Attrib.eval_thms ctxt args |> map (Element.pretty_statement ctxt Thm.theoremK) |> Pretty.chunks2 |> Pretty.string_of; fun string_of_thms ctxt args = Pretty.string_of (Proof_Context.pretty_fact ctxt ("", Attrib.eval_thms ctxt args)); fun string_of_prfs full state arg = Pretty.string_of (case arg of NONE => let val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state); val thy = Proof_Context.theory_of ctxt; val prf = Thm.proof_of thm; val prop = Thm.full_prop_of thm; val prf' = Proofterm.rewrite_proof_notypes ([], []) prf; in Proof_Syntax.pretty_proof ctxt (if full then Proofterm.reconstruct_proof thy prop prf' else prf') end | SOME srcs => let val ctxt = Toplevel.context_of state; val pretty_proof = Proof_Syntax.pretty_standard_proof_of ctxt full; in Pretty.chunks (map pretty_proof (Attrib.eval_thms ctxt srcs)) end); fun string_of_prop ctxt s = let val prop = Syntax.read_prop ctxt s; val ctxt' = Proof_Context.augment prop ctxt; in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end; fun string_of_term ctxt s = let val t = Syntax.read_term ctxt s; val T = Term.type_of t; val ctxt' = Proof_Context.augment t ctxt; in Pretty.string_of (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk, Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)]) end; fun string_of_type ctxt (s, NONE) = let val T = Syntax.read_typ ctxt s in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end | string_of_type ctxt (s1, SOME s2) = let val ctxt' = Config.put show_sorts true ctxt; val raw_T = Syntax.parse_typ ctxt' s1; val S = Syntax.read_sort ctxt' s2; val T = Syntax.check_term ctxt' (Logic.mk_type raw_T |> Type.constraint (Term.itselfT (Type_Infer.anyT S))) |> Logic.dest_type; in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt' T)) end; fun print_item string_of (modes, arg) = Toplevel.keep (fn state => Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ()); in val print_stmts = print_item (string_of_stmts o Toplevel.context_of); val print_thms = print_item (string_of_thms o Toplevel.context_of); val print_prfs = print_item o string_of_prfs; val print_prop = print_item (string_of_prop o Toplevel.context_of); val print_term = print_item (string_of_term o Toplevel.context_of); val print_type = print_item (string_of_type o Toplevel.context_of); end; end; diff --git a/src/Pure/ML/ml_antiquotation.ML b/src/Pure/ML/ml_antiquotation.ML --- a/src/Pure/ML/ml_antiquotation.ML +++ b/src/Pure/ML/ml_antiquotation.ML @@ -1,74 +1,86 @@ (* Title: Pure/ML/ml_antiquotation.ML Author: Makarius ML antiquotations. *) signature ML_ANTIQUOTATION = sig + val value_decl: string -> string -> Proof.context -> + (Proof.context -> string * string) * Proof.context val declaration: binding -> 'a context_parser -> - (Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) -> + (Token.src -> 'a -> Proof.context -> (Proof.context -> string * string) * Proof.context) -> theory -> theory val declaration_embedded: binding -> 'a context_parser -> - (Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) -> + (Token.src -> 'a -> Proof.context -> (Proof.context -> string * string) * Proof.context) -> theory -> theory val inline: binding -> string context_parser -> theory -> theory val inline_embedded: binding -> string context_parser -> theory -> theory val value: binding -> string context_parser -> theory -> theory val value_embedded: binding -> string context_parser -> theory -> theory end; structure ML_Antiquotation: ML_ANTIQUOTATION = struct (* define antiquotations *) +fun value_decl a s ctxt = + let + val (b, ctxt') = ML_Context.variant a ctxt; + val env = "val " ^ b ^ " = " ^ s ^ ";\n"; + val body = ML_Context.struct_name ctxt ^ "." ^ b; + fun decl (_: Proof.context) = (env, body); + in (decl, ctxt') end; + local fun gen_declaration name embedded scan body = ML_Context.add_antiquotation name embedded - (fn src => fn orig_ctxt => - let val (x, _) = Token.syntax scan src orig_ctxt - in body src x orig_ctxt end); + (fn range => fn src => fn orig_ctxt => + let + val (x, _) = Token.syntax scan src orig_ctxt; + val (decl, ctxt') = body src x orig_ctxt; + in (decl #> apply2 (ML_Lex.tokenize_range range), ctxt') end); fun gen_inline name embedded scan = gen_declaration name embedded scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt)); fun gen_value name embedded scan = - gen_declaration name embedded scan (fn _ => ML_Context.value_decl (Binding.name_of name)); + gen_declaration name embedded scan (fn _ => value_decl (Binding.name_of name)); in fun declaration name = gen_declaration name false; fun declaration_embedded name = gen_declaration name true; fun inline name = gen_inline name false; fun inline_embedded name = gen_inline name true; fun value name = gen_value name false; fun value_embedded name = gen_value name true; end; (* basic antiquotations *) val _ = Theory.setup (declaration (Binding.make ("here", \<^here>)) (Scan.succeed ()) (fn src => fn () => - ML_Context.value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #> + value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #> inline (Binding.make ("make_string", \<^here>)) (Args.context >> K ML_Pretty.make_string_fn) #> value_embedded (Binding.make ("binding", \<^here>)) (Scan.lift (Parse.input Args.embedded) >> (ML_Syntax.make_binding o Input.source_content)) #> value_embedded (Binding.make ("cartouche", \<^here>)) (Scan.lift Args.cartouche_input >> (fn source => "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^ ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))) #> inline_embedded (Binding.make ("verbatim", \<^here>)) (Scan.lift Args.embedded >> ML_Syntax.print_string)); end; diff --git a/src/Pure/ML/ml_context.ML b/src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML +++ b/src/Pure/ML/ml_context.ML @@ -1,227 +1,214 @@ (* Title: Pure/ML/ml_context.ML Author: Makarius ML context and antiquotations. *) signature ML_CONTEXT = sig val check_antiquotation: Proof.context -> xstring * Position.T -> string val struct_name: Proof.context -> string val variant: string -> Proof.context -> string * Proof.context - type decl = Proof.context -> string * string - val value_decl: string -> string -> Proof.context -> decl * Proof.context - val add_antiquotation: binding -> bool -> (Token.src -> Proof.context -> decl * Proof.context) -> - theory -> theory + type decl = Proof.context -> ML_Lex.token list * ML_Lex.token list + type antiquotation = Position.range -> Token.src -> Proof.context -> decl * Proof.context + val add_antiquotation: binding -> bool -> antiquotation -> theory -> theory val print_antiquotations: bool -> Proof.context -> unit val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit val eval_file: ML_Compiler.flags -> Path.T -> unit val eval_source: ML_Compiler.flags -> Input.source -> unit val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit val eval_source_in: Proof.context option -> ML_Compiler.flags -> Input.source -> unit val exec: (unit -> unit) -> Context.generic -> Context.generic val expression: Position.T -> ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic end structure ML_Context: ML_CONTEXT = struct (** ML antiquotations **) (* names for generated environment *) structure Names = Proof_Data ( type T = string * Name.context; val init_names = ML_Syntax.reserved |> Name.declare "ML_context"; fun init _ = ("Isabelle0", init_names); ); fun struct_name ctxt = #1 (Names.get ctxt); val struct_begin = (Names.map o apfst) (fn _ => "Isabelle" ^ serial_string ()); fun variant a ctxt = let val names = #2 (Names.get ctxt); val (b, names') = Name.variant (Name.desymbolize (SOME false) a) names; val ctxt' = (Names.map o apsnd) (K names') ctxt; in (b, ctxt') end; -(* decl *) - -type decl = Proof.context -> string * string; (*final context -> ML env, ML body*) +(* theory data *) -fun value_decl a s ctxt = - let - val (b, ctxt') = variant a ctxt; - val env = "val " ^ b ^ " = " ^ s ^ ";\n"; - val body = struct_name ctxt ^ "." ^ b; - fun decl (_: Proof.context) = (env, body); - in (decl, ctxt') end; +type decl = + Proof.context -> ML_Lex.token list * ML_Lex.token list; (*final context -> ML env, ML body*) - -(* theory data *) +type antiquotation = + Position.range -> Token.src -> Proof.context -> decl * Proof.context; structure Antiquotations = Theory_Data ( - type T = (bool * (Token.src -> Proof.context -> decl * Proof.context)) Name_Space.table; + type T = (bool * antiquotation) Name_Space.table; val empty : T = Name_Space.empty_table Markup.ML_antiquotationN; val extend = I; fun merge data : T = Name_Space.merge_tables data; ); val get_antiquotations = Antiquotations.get o Proof_Context.theory_of; fun check_antiquotation ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_antiquotations ctxt); -fun add_antiquotation name embedded scan thy = thy - |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, (embedded, scan)) #> snd); +fun add_antiquotation name embedded antiquotation thy = + thy |> Antiquotations.map + (Name_Space.define (Context.Theory thy) true (name, (embedded, antiquotation)) #> #2); fun print_antiquotations verbose ctxt = Pretty.big_list "ML antiquotations:" (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_antiquotations ctxt))) |> Pretty.writeln; -fun apply_antiquotation pos src ctxt = +fun apply_antiquotation range src ctxt = let - val (src', (embedded, scan)) = Token.check_src ctxt get_antiquotations src; + val (src', (embedded, antiquotation)) = Token.check_src ctxt get_antiquotations src; val _ = if Options.default_bool "update_control_cartouches" then Context_Position.reports_text ctxt - (Antiquote.update_reports embedded pos (map Token.content_of src')) + (Antiquote.update_reports embedded (#1 range) (map Token.content_of src')) else (); - in scan src' ctxt end; + in antiquotation range src' ctxt end; (* parsing and evaluation *) local val antiq = Parse.!!! ((Parse.token Parse.liberal_name ::: Parse.args) --| Scan.ahead Parse.eof); fun make_env name visible = (ML_Lex.tokenize ("structure " ^ name ^ " =\nstruct\n\ \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^ " (Context.the_local_context ());\n"), ML_Lex.tokenize "end;"); fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end"); fun eval_antiquotes (ants, pos) opt_context = let val visible = (case opt_context of SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt | _ => true); val opt_ctxt = Option.map Context.proof_of opt_context; val ((ml_env, ml_body), opt_ctxt') = if forall (fn Antiquote.Text _ => true | _ => false) ants then (([], map (fn Antiquote.Text tok => tok) ants), opt_ctxt) else let - fun tokenize range = apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range)); - - fun expand_src range src ctxt = - let val (decl, ctxt') = apply_antiquotation (#1 range) src ctxt; - in (decl #> tokenize range, ctxt') end; - fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt) | expand (Antiquote.Control {name, range, body}) ctxt = - expand_src range + apply_antiquotation range (Token.make_src name (if null body then [] else [Token.read_cartouche body])) ctxt | expand (Antiquote.Antiq {range, body, ...}) ctxt = - expand_src range + apply_antiquotation range (Token.read_antiq (Thy_Header.get_keywords' ctxt) antiq (body, #1 range)) ctxt; val ctxt = (case opt_ctxt of NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.here pos) | SOME ctxt => struct_begin ctxt); val (begin_env, end_env) = make_env (struct_name ctxt) visible; val (decls, ctxt') = fold_map expand ants ctxt; val (ml_env, ml_body) = decls |> map (fn decl => decl ctxt') |> split_list |> apply2 flat; in ((begin_env @ ml_env @ end_env, ml_body), SOME ctxt') end; in ((ml_env, ml_body), opt_ctxt') end; in fun eval flags pos ants = let val non_verbose = ML_Compiler.verbose false flags; (*prepare source text*) val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.get_generic_context ()); val _ = (case env_ctxt of SOME ctxt => if Config.get ctxt ML_Options.source_trace andalso Context_Position.is_visible ctxt then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body]) else () | NONE => ()); (*prepare environment*) val _ = Context.setmp_generic_context (Option.map (Context.Proof o Context_Position.set_visible false) env_ctxt) (fn () => (ML_Compiler.eval non_verbose Position.none env; Context.get_generic_context ())) () |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit [context'])); (*eval body*) val _ = ML_Compiler.eval flags pos body; (*clear environment*) val _ = (case (env_ctxt, is_some (Context.get_generic_context ())) of (SOME ctxt, true) => let val name = struct_name ctxt; val _ = ML_Compiler.eval non_verbose Position.none (reset_env name); val _ = Context.>> (ML_Env.forget_structure name); in () end | _ => ()); in () end; end; (* derived versions *) fun eval_file flags path = let val pos = Path.position path in eval flags pos (ML_Lex.read_text (File.read path, pos)) end; fun eval_source flags source = let val opt_context = Context.get_generic_context (); val {read_source, ...} = ML_Env.operations opt_context (#environment flags); in eval flags (Input.pos_of source) (read_source source) end; fun eval_in ctxt flags pos ants = Context.setmp_generic_context (Option.map Context.Proof ctxt) (fn () => eval flags pos ants) (); fun eval_source_in ctxt flags source = Context.setmp_generic_context (Option.map Context.Proof ctxt) (fn () => eval_source flags source) (); fun exec (e: unit -> unit) context = (case Context.setmp_generic_context (SOME context) (fn () => (e (); Context.get_generic_context ())) () of SOME context' => context' | NONE => error "Missing context after execution"); fun expression pos ants = exec (fn () => eval ML_Compiler.flags pos ants); end; val ML = ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags); diff --git a/src/Pure/ML/ml_lex.ML b/src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML +++ b/src/Pure/ML/ml_lex.ML @@ -1,392 +1,394 @@ (* Title: Pure/ML/ml_lex.ML Author: Makarius Lexical syntax for Isabelle/ML and Standard ML. *) signature ML_LEX = sig val keywords: string list datatype token_kind = Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | Space | Comment of Comment.kind option | Error of string | EOF eqtype token val stopper: token Scan.stopper val is_regular: token -> bool val is_improper: token -> bool val is_comment: token -> bool val set_range: Position.range -> token -> token val range_of: token -> Position.range val pos_of: token -> Position.T val end_pos_of: token -> Position.T val kind_of: token -> token_kind val content_of: token -> string val check_content_of: token -> string val flatten: token list -> string val source: (Symbol.symbol, 'a) Source.source -> (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source val tokenize: string -> token list + val tokenize_range: Position.range -> string -> token list val read_text: Symbol_Pos.text * Position.T -> token Antiquote.antiquote list val read: Symbol_Pos.text -> token Antiquote.antiquote list - val read_set_range: Position.range -> Symbol_Pos.text -> token Antiquote.antiquote list + val read_range: Position.range -> Symbol_Pos.text -> token Antiquote.antiquote list val read_source': {language: bool -> Markup.T, opaque_warning: bool, symbols: bool} -> token Antiquote.antiquote Symbol_Pos.scanner -> Input.source -> token Antiquote.antiquote list val read_source: Input.source -> token Antiquote.antiquote list val read_source_sml: Input.source -> token Antiquote.antiquote list val read_symbols_sml: Symbol_Pos.T list -> token Antiquote.antiquote list end; structure ML_Lex: ML_LEX = struct (** keywords **) val keywords = ["#", "(", ")", ",", "->", "...", ":", ":>", ";", "=", "=>", "[", "]", "_", "{", "|", "}", "abstype", "and", "andalso", "as", "case", "datatype", "do", "else", "end", "eqtype", "exception", "fn", "fun", "functor", "handle", "if", "in", "include", "infix", "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse", "raise", "rec", "sharing", "sig", "signature", "struct", "structure", "then", "type", "val", "where", "while", "with", "withtype"]; val keywords2 = ["and", "case", "do", "else", "end", "if", "in", "let", "local", "of", "sig", "struct", "then", "while", "with"]; val keywords3 = ["handle", "open", "raise"]; val lexicon = Scan.make_lexicon (map raw_explode keywords); (** tokens **) (* datatype token *) datatype token_kind = Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | Space | Comment of Comment.kind option | Error of string | EOF; datatype token = Token of Position.range * (token_kind * string); (* position *) fun set_range range (Token (_, x)) = Token (range, x); fun range_of (Token (range, _)) = range; val pos_of = #1 o range_of; val end_pos_of = #2 o range_of; (* stopper *) fun mk_eof pos = Token ((pos, Position.none), (EOF, "")); val eof = mk_eof Position.none; fun is_eof (Token (_, (EOF, _))) = true | is_eof _ = false; val stopper = Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof; (* token content *) fun kind_of (Token (_, (k, _))) = k; fun content_of (Token (_, (_, x))) = x; fun token_leq (tok, tok') = content_of tok <= content_of tok'; fun is_keyword (Token (_, (Keyword, _))) = true | is_keyword _ = false; fun is_delimiter (Token (_, (Keyword, x))) = not (Symbol.is_ascii_identifier x) | is_delimiter _ = false; fun is_regular (Token (_, (Error _, _))) = false | is_regular (Token (_, (EOF, _))) = false | is_regular _ = true; fun is_improper (Token (_, (Space, _))) = true | is_improper (Token (_, (Comment _, _))) = true | is_improper _ = false; fun is_comment (Token (_, (Comment _, _))) = true | is_comment _ = false; fun warning_opaque tok = (case tok of Token (_, (Keyword, ":>")) => warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\ \prefer non-opaque matching (:) possibly with abstype" ^ Position.here (pos_of tok)) | _ => ()); fun check_content_of tok = (case kind_of tok of Error msg => error msg | _ => content_of tok); (* flatten *) fun flatten_content (tok :: (toks as tok' :: _)) = Symbol.escape (check_content_of tok) :: (if is_improper tok orelse is_improper tok' then flatten_content toks else Symbol.space :: flatten_content toks) | flatten_content toks = map (Symbol.escape o check_content_of) toks; val flatten = implode o flatten_content; (* markup *) local val token_kind_markup = fn Type_Var => (Markup.ML_tvar, "") | Word => (Markup.ML_numeral, "") | Int => (Markup.ML_numeral, "") | Real => (Markup.ML_numeral, "") | Char => (Markup.ML_char, "") | String => (Markup.ML_string, "") | Comment _ => (Markup.ML_comment, "") | Error msg => (Markup.bad (), msg) | _ => (Markup.empty, ""); in fun token_report (tok as Token ((pos, _), (kind, x))) = let val (markup, txt) = if not (is_keyword tok) then token_kind_markup kind else if is_delimiter tok then (Markup.ML_delimiter, "") else if member (op =) keywords2 x then (Markup.ML_keyword2 |> Markup.keyword_properties, "") else if member (op =) keywords3 x then (Markup.ML_keyword3 |> Markup.keyword_properties, "") else (Markup.ML_keyword1 |> Markup.keyword_properties, ""); in ((pos, markup), txt) end; end; (** scanners **) open Basic_Symbol_Pos; val err_prefix = "SML lexical error: "; fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg); (* identifiers *) local val scan_letdigs = Scan.many (Symbol.is_ascii_letdig o Symbol_Pos.symbol); val scan_alphanumeric = Scan.one (Symbol.is_ascii_letter o Symbol_Pos.symbol) ::: scan_letdigs; val scan_symbolic = Scan.many1 (member (op =) (raw_explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol); in val scan_ident = scan_alphanumeric || scan_symbolic; val scan_long_ident = Scan.repeats1 (scan_alphanumeric @@@ $$$ ".") @@@ (scan_ident || $$$ "="); val scan_type_var = $$$ "'" @@@ scan_letdigs; end; (* numerals *) local val scan_dec = Scan.many1 (Symbol.is_ascii_digit o Symbol_Pos.symbol); val scan_hex = Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol); val scan_sign = Scan.optional ($$$ "~") []; val scan_decint = scan_sign @@@ scan_dec; val scan_exp = ($$$ "E" || $$$ "e") @@@ scan_decint; in val scan_word = $$$ "0" @@@ $$$ "w" @@@ $$$ "x" @@@ scan_hex || $$$ "0" @@@ $$$ "w" @@@ scan_dec; val scan_int = scan_sign @@@ ($$$ "0" @@@ $$$ "x" @@@ scan_hex || scan_dec); val scan_rat = scan_decint @@@ Scan.optional ($$$ "/" @@@ scan_dec) []; val scan_real = scan_decint @@@ $$$ "." @@@ scan_dec @@@ Scan.optional scan_exp [] || scan_decint @@@ scan_exp; end; (* chars and strings *) val scan_blanks1 = Scan.many1 (Symbol.is_ascii_blank o Symbol_Pos.symbol); local val scan_escape = Scan.one (member (op =) (raw_explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single || $$$ "^" @@@ (Scan.one (fn (s, _) => Char.ord #"@" <= ord s andalso ord s <= Char.ord #"_") >> single) || Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) -- Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) -- Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]); val scan_str = Scan.one (fn (s, _) => Symbol.not_eof s andalso s <> "\"" andalso s <> "\\" andalso (not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single || $$$ "\\" @@@ !!! "bad escape character in string" scan_escape; val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\"; val scan_gaps = Scan.repeats scan_gap; in val scan_char = $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ scan_str @@@ scan_gaps @@@ $$$ "\""; val recover_char = $$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ Scan.optional (Scan.permissive scan_str @@@ scan_gaps) []; val scan_string = Scan.ahead ($$ "\"") |-- !!! "unclosed string literal" ($$$ "\"" @@@ Scan.repeats (scan_gap || scan_str) @@@ $$$ "\""); val recover_string = $$$ "\"" @@@ Scan.repeats (scan_gap || Scan.permissive scan_str); end; (* rat antiquotation *) val rat_name = Symbol_Pos.explode ("Pure.rat ", Position.none); val scan_rat_antiq = Symbol_Pos.scan_pos -- ($$ "@" |-- Symbol_Pos.scan_pos -- scan_rat) -- Symbol_Pos.scan_pos >> (fn ((pos1, (pos2, body)), pos3) => {start = Position.range_position (pos1, pos2), stop = Position.none, range = Position.range (pos1, pos3), body = rat_name @ body}); (* scan tokens *) local fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss)); val scan_sml = scan_char >> token Char || scan_string >> token String || scan_blanks1 >> token Space || Symbol_Pos.scan_comment err_prefix >> token (Comment NONE) || Scan.max token_leq (Scan.literal lexicon >> token Keyword) (scan_word >> token Word || scan_real >> token Real || scan_int >> token Int || scan_long_ident >> token Long_Ident || scan_ident >> token Ident || scan_type_var >> token Type_Var); val scan_sml_antiq = scan_sml >> Antiquote.Text; val scan_ml_antiq = Comment.scan_inner >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) || Antiquote.scan_control >> Antiquote.Control || Antiquote.scan_antiq >> Antiquote.Antiq || scan_rat_antiq >> Antiquote.Antiq || scan_sml_antiq; fun recover msg = (recover_char || recover_string || Symbol_Pos.recover_cartouche || Symbol_Pos.recover_comment || Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single) >> (single o token (Error msg)); fun reader {opaque_warning} scan syms = let val termination = if null syms then [] else let val pos1 = List.last syms |-> Position.advance; val pos2 = Position.advance Symbol.space pos1; in [Antiquote.Text (Token (Position.range (pos1, pos2), (Space, Symbol.space)))] end; fun check (Antiquote.Text tok) = (check_content_of tok; if opaque_warning then warning_opaque tok else ()) | check _ = (); val input = Source.of_list syms |> Source.source Symbol_Pos.stopper (Scan.recover (Scan.bulk (!!! "bad input" scan)) (fn msg => recover msg >> map Antiquote.Text)) |> Source.exhaust; val _ = Position.reports (Antiquote.antiq_reports input); val _ = Position.reports_text (maps (fn Antiquote.Text t => [token_report t] | _ => []) input); val _ = List.app check input; in input @ termination end; in fun source src = Symbol_Pos.source (Position.line 1) src |> Source.source Symbol_Pos.stopper (Scan.recover (Scan.bulk (!!! "bad input" scan_sml)) recover); val tokenize = Symbol.explode #> Source.of_list #> source #> Source.exhaust; +fun tokenize_range range = tokenize #> map (set_range range); val read_text = reader {opaque_warning = true} scan_ml_antiq o Symbol_Pos.explode; fun read text = read_text (text, Position.none); -fun read_set_range range = +fun read_range range = read #> map (fn Antiquote.Text tok => Antiquote.Text (set_range range tok) | antiq => antiq); fun read_source' {language, symbols, opaque_warning} scan source = let val pos = Input.pos_of source; val _ = if Position.is_reported_range pos then Position.report pos (language (Input.is_delimited source)) else (); in Input.source_explode source |> not symbols ? maps (fn (s, p) => raw_explode s |> map (rpair p)) |> reader {opaque_warning = opaque_warning} scan end; val read_source = read_source' {language = Markup.language_ML, symbols = true, opaque_warning = true} scan_ml_antiq; val read_source_sml = read_source' {language = Markup.language_SML, symbols = false, opaque_warning = false} scan_sml_antiq; val read_symbols_sml = reader {opaque_warning = false} scan_sml_antiq; end; end; diff --git a/src/Pure/ML/ml_thms.ML b/src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML +++ b/src/Pure/ML/ml_thms.ML @@ -1,143 +1,143 @@ (* Title: Pure/ML/ml_thms.ML Author: Makarius Attribute source and theorem values within ML. *) signature ML_THMS = sig val the_attributes: Proof.context -> int -> Token.src list val the_thmss: Proof.context -> thm list list val get_stored_thms: unit -> thm list val get_stored_thm: unit -> thm val store_thms: string * thm list -> unit val store_thm: string * thm -> unit val bind_thm: string * thm -> unit val bind_thms: string * thm list -> unit end; structure ML_Thms: ML_THMS = struct (* auxiliary data *) type thms = (string * bool) * thm list; (*name, single, value*) structure Data = Proof_Data ( type T = Token.src list Inttab.table * thms list; fun init _ = (Inttab.empty, []); ); val put_attributes = Data.map o apfst o Inttab.update; fun the_attributes ctxt name = the (Inttab.lookup (fst (Data.get ctxt)) name); val get_thmss = snd o Data.get; val the_thmss = map snd o get_thmss; val cons_thms = Data.map o apsnd o cons; (* attribute source *) val _ = Theory.setup (ML_Antiquotation.declaration \<^binding>\attributes\ Attrib.attribs (fn _ => fn srcs => fn ctxt => let val i = serial () in ctxt |> put_attributes (i, srcs) - |> ML_Context.value_decl "attributes" + |> ML_Antiquotation.value_decl "attributes" ("ML_Thms.the_attributes ML_context " ^ string_of_int i) end)); (* fact references *) fun thm_binding kind is_single thms ctxt = let val initial = null (get_thmss ctxt); val (name, ctxt') = ML_Context.variant kind ctxt; val ctxt'' = cons_thms ((name, is_single), thms) ctxt'; val ml_body = ML_Context.struct_name ctxt ^ "." ^ name; fun decl final_ctxt = if initial then let val binds = get_thmss final_ctxt |> map (fn ((a, b), _) => (b ? enclose "[" "]") a); val ml_env = "val [" ^ commas binds ^ "] = ML_Thms.the_thmss ML_context;\n"; in (ml_env, ml_body) end else ("", ml_body); in (decl, ctxt'') end; val _ = Theory.setup (ML_Antiquotation.declaration \<^binding>\thm\ (Attrib.thm >> single) (K (thm_binding "thm" true)) #> ML_Antiquotation.declaration \<^binding>\thms\ Attrib.thms (K (thm_binding "thms" false))); (* ad-hoc goals *) val and_ = Args.$$$ "and"; val by = Parse.reserved "by"; val goal = Scan.unless (by || and_) Args.embedded_inner_syntax; val _ = Theory.setup (ML_Antiquotation.declaration \<^binding>\lemma\ (Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) -- (Parse.position by -- Method.parse -- Scan.option Method.parse))) (fn _ => fn ((is_open, raw_propss), (((_, by_pos), m1), m2)) => fn ctxt => let val reports = (by_pos, Markup.keyword1 |> Markup.keyword_properties) :: maps Method.reports_of (m1 :: the_list m2); val _ = Context_Position.reports ctxt reports; val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation \<^here>; fun after_qed res goal_ctxt = Proof_Context.put_thms false (Auto_Bind.thisN, SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt; val ctxt' = ctxt |> Proof.theorem NONE after_qed propss |> Proof.global_terminal_proof (m1, m2); val thms = Proof_Context.get_fact ctxt' (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN))); in thm_binding "lemma" (length (flat propss) = 1) thms ctxt end)); (* old-style theorem bindings *) structure Data = Theory_Data ( type T = thm list; val empty = []; val extend = I; val merge = #1; ); fun get_stored_thms () = Data.get (Context.the_global_context ()); val get_stored_thm = hd o get_stored_thms; fun ml_store get (name, ths) = let val (_, ths') = Context.>>> (Context.map_theory_result (Global_Theory.note_thms "" ((Binding.name name, []), [(ths, [])]))); val _ = Theory.setup (Data.put ths'); val _ = if name = "" then () else if not (ML_Syntax.is_identifier name) then error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value") else ML_Compiler.eval (ML_Compiler.verbose true ML_Compiler.flags) Position.none (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();")); val _ = Theory.setup (Data.put []); in () end; val store_thms = ml_store "ML_Thms.get_stored_thms"; fun store_thm (name, th) = ml_store "ML_Thms.get_stored_thm" (name, [th]); fun bind_thm (name, thm) = store_thm (name, Drule.export_without_context thm); fun bind_thms (name, thms) = store_thms (name, map Drule.export_without_context thms); end;