diff --git a/src/Pure/General/position.ML b/src/Pure/General/position.ML --- a/src/Pure/General/position.ML +++ b/src/Pure/General/position.ML @@ -1,298 +1,302 @@ (* Title: Pure/General/position.ML Author: Markus Wenzel, TU Muenchen Source positions: counting Isabelle symbols, starting from 1. *) signature POSITION = sig eqtype T val ord: T ord val make: Thread_Position.T -> T val dest: T -> Thread_Position.T val line_of: T -> int option val offset_of: T -> int option val end_offset_of: T -> int option val file_of: T -> string option val advance: Symbol.symbol -> T -> T val advance_offsets: int -> T -> T val distance_of: T * T -> int option val none: T val start: T val file_name: string -> Properties.T val file_only: string -> T val file: string -> T val line_file_only: int -> string -> T val line_file: int -> string -> T val line: int -> T val get_props: T -> Properties.T val id: string -> T val id_only: string -> T val get_id: T -> string option val put_id: string -> T -> T val copy_id: T -> T -> T val id_properties_of: T -> Properties.T val parse_id: T -> int option val adjust_offsets: (int -> int option) -> T -> T val of_properties: Properties.T -> T val properties_of: T -> Properties.T val offset_properties_of: T -> Properties.T val def_properties_of: T -> Properties.T + val entity_markup: string -> string * T -> Markup.T val entity_properties_of: bool -> serial -> T -> Properties.T val default_properties: T -> Properties.T -> Properties.T val markup: T -> Markup.T -> Markup.T val is_reported: T -> bool val is_reported_range: T -> bool val reported_text: T -> Markup.T -> string -> string val report_text: T -> Markup.T -> string -> unit val report: T -> Markup.T -> unit type report = T * Markup.T type report_text = report * string val reports_text: report_text list -> unit val reports: report list -> unit val store_reports: report_text list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit val append_reports: report_text list Unsynchronized.ref -> report list -> unit val here_strs: T -> string * string val here: T -> string val here_list: T list -> string type range = T * T val no_range: range val no_range_position: T -> T val range_position: range -> T val range: T * T -> range val range_of_properties: Properties.T -> range val properties_of_range: range -> Properties.T val thread_data: unit -> T val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b val default: T -> bool * T end; structure Position: POSITION = struct (* datatype position *) datatype T = Pos of (int * int * int) * Properties.T; fun ord (pos1 as Pos ((i, j, k), props), pos2 as Pos ((i', j', k'), props')) = if pointer_eq (pos1, pos2) then EQUAL else (case int_ord (i, i') of EQUAL => (case int_ord (j, j') of EQUAL => (case int_ord (k, k') of EQUAL => Properties.ord (props, props') | ord => ord) | ord => ord) | ord => ord); fun norm_props (props: Properties.T) = maps (fn a => the_list (find_first (fn (b, _) => a = b) props)) Markup.position_properties'; fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props); fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props}; fun valid (i: int) = i > 0; fun if_valid i i' = if valid i then i' else i; (* fields *) fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE; fun offset_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE; fun end_offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE; fun file_of (Pos (_, props)) = Properties.get props Markup.fileN; (* advance *) fun advance_count "\n" (i: int, j: int, k: int) = (if_valid i (i + 1), if_valid j (j + 1), k) | advance_count s (i, j, k) = if Symbol.not_eof s then (i, if_valid j (j + 1), k) else (i, j, k); fun invalid_count (i, j, _: int) = not (valid i orelse valid j); fun advance sym (pos as (Pos (count, props))) = if invalid_count count then pos else Pos (advance_count sym count, props); fun advance_offsets offset (pos as (Pos (count as (i, j, k), props))) = if offset = 0 orelse invalid_count count then pos else if offset < 0 then raise Fail "Illegal offset" else if valid i then raise Fail "Illegal line position" else Pos ((i, if_valid j (j + offset), if_valid k (k + offset)), props); (* distance of adjacent positions *) fun distance_of (Pos ((_, j, _), _), Pos ((_, j', _), _)) = if valid j andalso valid j' then SOME (j' - j) else NONE; (* make position *) val none = Pos ((0, 0, 0), []); val start = Pos ((1, 1, 0), []); fun file_name "" = [] | file_name name = [(Markup.fileN, name)]; fun file_only name = Pos ((0, 0, 0), file_name name); fun file name = Pos ((1, 1, 0), file_name name); fun line_file_only i name = Pos ((i, 0, 0), file_name name); fun line_file i name = Pos ((i, 1, 0), file_name name); fun line i = line_file i ""; fun get_props (Pos (_, props)) = props; fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]); fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]); fun get_id (Pos (_, props)) = Properties.get props Markup.idN; fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props)); fun copy_id pos = (case get_id pos of NONE => I | SOME id => put_id id); fun parse_id pos = Option.map Value.parse_int (get_id pos); fun id_properties_of pos = (case get_id pos of SOME id => [(Markup.idN, id)] | NONE => []); fun adjust_offsets adjust (pos as Pos (_, props)) = if is_none (file_of pos) then (case parse_id pos of SOME id => (case adjust id of SOME offset => let val Pos (count, _) = advance_offsets offset pos in Pos (count, Properties.remove Markup.idN props) end | NONE => pos) | NONE => pos) else pos; (* markup properties *) fun get props name = (case Properties.get props name of NONE => 0 | SOME s => Value.parse_int s); fun of_properties props = make {line = get props Markup.lineN, offset = get props Markup.offsetN, end_offset = get props Markup.end_offsetN, props = props}; fun value k i = if valid i then [(k, Value.print_int i)] else []; fun properties_of (Pos ((i, j, k), props)) = value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props; fun offset_properties_of (Pos ((_, j, k), _)) = value Markup.offsetN j @ value Markup.end_offsetN k; val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y)); +fun entity_markup kind (name, pos) = + Markup.entity kind name |> Markup.properties (def_properties_of pos); + fun entity_properties_of def serial pos = if def then (Markup.defN, Value.print_int serial) :: properties_of pos else (Markup.refN, Value.print_int serial) :: def_properties_of pos; fun default_properties default props = if exists (member (op =) Markup.position_properties o #1) props then props else properties_of default @ props; val markup = Markup.properties o properties_of; (* reports *) fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos); fun is_reported_range pos = is_reported pos andalso is_some (end_offset_of pos); fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else ""; fun report_text pos markup txt = Output.report [reported_text pos markup txt]; fun report pos markup = report_text pos markup ""; type report = T * Markup.T; type report_text = report * string; val reports_text = map (fn ((pos, m), txt) => if is_reported pos then Markup.markup (markup pos m) txt else "") #> Output.report; val reports = map (rpair "") #> reports_text; fun store_reports _ [] _ _ = () | store_reports (r: report_text list Unsynchronized.ref) ps markup x = let val ms = markup x in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end; fun append_reports (r: report_text list Unsynchronized.ref) reports = Unsynchronized.change r (append (map (rpair "") reports)); (* here: user output *) fun here_strs pos = (case (line_of pos, file_of pos) of (SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")") | (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")") | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")") | _ => if is_reported pos then ("", "\092<^here>") else ("", "")); fun here pos = let val props = properties_of pos; val (s1, s2) = here_strs pos; in if s2 = "" then "" else s1 ^ Markup.markup (Markup.properties props Markup.position) s2 end; val here_list = map here #> distinct (op =) #> implode; (* range *) type range = T * T; val no_range = (none, none); fun no_range_position (Pos ((i, j, _), props)) = Pos ((i, j, 0), props); fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props); fun range (pos, pos') = (range_position (pos, pos'), no_range_position pos'); fun range_of_properties props = let val pos = of_properties props; val pos' = make {line = get props Markup.end_lineN, offset = get props Markup.end_offsetN, end_offset = 0, props = props}; in (pos, pos') end; fun properties_of_range (pos, pos') = properties_of pos @ value Markup.end_lineN (the_default 0 (line_of pos')); (* thread data *) val thread_data = make o Thread_Position.get; fun setmp_thread_data pos = Thread_Position.setmp (dest pos); fun default pos = if pos = none then (false, thread_data ()) else (true, pos); end; diff --git a/src/Pure/Isar/method.ML b/src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML +++ b/src/Pure/Isar/method.ML @@ -1,822 +1,821 @@ (* Title: Pure/Isar/method.ML Author: Markus Wenzel, TU Muenchen Isar proof methods. *) signature METHOD = sig type method = thm list -> context_tactic val CONTEXT_METHOD: (thm list -> context_tactic) -> method val METHOD: (thm list -> tactic) -> method val fail: method val succeed: method val insert_tac: Proof.context -> thm list -> int -> tactic val insert: thm list -> method val SIMPLE_METHOD: tactic -> method val SIMPLE_METHOD': (int -> tactic) -> method val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method val goal_cases_tac: string list -> context_tactic val cheating: bool -> method val intro: Proof.context -> thm list -> method val elim: Proof.context -> thm list -> method val unfold: thm list -> Proof.context -> method val fold: thm list -> Proof.context -> method val atomize: bool -> Proof.context -> method val this: Proof.context -> method val fact: thm list -> Proof.context -> method val assm_tac: Proof.context -> int -> tactic val all_assm_tac: Proof.context -> tactic val assumption: Proof.context -> method val rule_trace: bool Config.T val trace: Proof.context -> thm list -> unit val rule_tac: Proof.context -> thm list -> thm list -> int -> tactic val some_rule_tac: Proof.context -> thm list -> thm list -> int -> tactic val intros_tac: Proof.context -> thm list -> thm list -> tactic val try_intros_tac: Proof.context -> thm list -> thm list -> tactic val rule: Proof.context -> thm list -> method val erule: Proof.context -> int -> thm list -> method val drule: Proof.context -> int -> thm list -> method val frule: Proof.context -> int -> thm list -> method val set_tactic: (morphism -> thm list -> tactic) -> Context.generic -> Context.generic val clean_facts: thm list -> thm list val set_facts: thm list -> Proof.context -> Proof.context val get_facts: Proof.context -> thm list type combinator_info val no_combinator_info: combinator_info datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int datatype text = Source of Token.src | Basic of Proof.context -> method | Combinator of combinator_info * combinator * text list val map_source: (Token.src -> Token.src) -> text -> text val primitive_text: (Proof.context -> thm -> thm) -> text val succeed_text: text val standard_text: text val this_text: text val done_text: text val sorry_text: bool -> text val finish_text: text option * bool -> text val print_methods: bool -> Proof.context -> unit val check_name: Proof.context -> xstring * Position.T -> string val check_src: Proof.context -> Token.src -> Token.src val check_text: Proof.context -> text -> text val checked_text: text -> bool val method_syntax: (Proof.context -> method) context_parser -> Token.src -> Proof.context -> method val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory val local_setup: binding -> (Proof.context -> method) context_parser -> string -> local_theory -> local_theory val method_setup: bstring * Position.T -> Input.source -> string -> local_theory -> local_theory val method: Proof.context -> Token.src -> Proof.context -> method val method_closure: Proof.context -> Token.src -> Token.src val closure: bool Config.T val method_cmd: Proof.context -> Token.src -> Proof.context -> method val detect_closure_state: thm -> bool val STATIC: (unit -> unit) -> context_tactic val RUNTIME: context_tactic -> context_tactic val sleep: Time.time -> context_tactic val evaluate: text -> Proof.context -> method val evaluate_runtime: text -> Proof.context -> method type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T} val modifier: attribute -> Position.T -> modifier val old_section_parser: bool Config.T val sections: modifier parser list -> unit context_parser type text_range = text * Position.range val text: text_range option -> text option val position: text_range option -> Position.T val reports_of: text_range -> Position.report list val report: text_range -> unit val parser: int -> text_range parser val parse: text_range parser val read: Proof.context -> Token.src -> text val read_closure: Proof.context -> Token.src -> text * Token.src val read_closure_input: Proof.context -> Input.source -> text * Token.src val text_closure: text context_parser end; structure Method: METHOD = struct (** proof methods **) (* type method *) type method = thm list -> context_tactic; fun CONTEXT_METHOD tac : method = fn facts => CONTEXT_TACTIC (ALLGOALS Goal.conjunction_tac) #> Seq.maps_results (tac facts); fun METHOD tac : method = fn facts => CONTEXT_TACTIC (ALLGOALS Goal.conjunction_tac THEN tac facts); val fail = METHOD (K no_tac); val succeed = METHOD (K all_tac); (* insert facts *) fun insert_tac _ [] _ = all_tac | insert_tac ctxt facts i = EVERY (map (fn r => resolve_tac ctxt [Drule.forall_intr_vars r COMP_INCR revcut_rl] i) facts); fun insert thms = CONTEXT_METHOD (fn _ => fn (ctxt, st) => st |> ALLGOALS (insert_tac ctxt thms) |> TACTIC_CONTEXT ctxt); fun SIMPLE_METHOD tac = CONTEXT_METHOD (fn facts => fn (ctxt, st) => st |> (ALLGOALS (insert_tac ctxt facts) THEN tac) |> TACTIC_CONTEXT ctxt); fun SIMPLE_METHOD'' quant tac = CONTEXT_METHOD (fn facts => fn (ctxt, st) => st |> quant (insert_tac ctxt facts THEN' tac) |> TACTIC_CONTEXT ctxt); val SIMPLE_METHOD' = SIMPLE_METHOD'' HEADGOAL; (* goals as cases *) fun goal_cases_tac case_names : context_tactic = fn (ctxt, st) => let val cases = (if null case_names then map string_of_int (1 upto Thm.nprems_of st) else case_names) |> map (rpair [] o rpair []) |> Rule_Cases.make_common ctxt (Thm.prop_of (Rule_Cases.internalize_params st)); in CONTEXT_CASES cases all_tac (ctxt, st) end; (* cheating *) fun cheating int = CONTEXT_METHOD (fn _ => fn (ctxt, st) => if int orelse Config.get ctxt quick_and_dirty then TACTIC_CONTEXT ctxt (ALLGOALS (Skip_Proof.cheat_tac ctxt) st) else error "Cheating requires quick_and_dirty mode!"); (* unfold intro/elim rules *) fun intro ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ctxt ths)); fun elim ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt ths)); (* unfold/fold definitions *) fun unfold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.unfold_tac ctxt ths)); fun fold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.fold_tac ctxt ths)); (* atomize rule statements *) fun atomize false ctxt = SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac ctxt) | atomize true ctxt = Context_Tactic.CONTEXT_TACTIC o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt)); (* this -- resolve facts directly *) fun this ctxt = METHOD (EVERY o map (HEADGOAL o resolve_tac ctxt o single)); (* fact -- composition by facts from context *) fun fact [] ctxt = SIMPLE_METHOD' (Proof_Context.some_fact_tac ctxt) | fact rules ctxt = SIMPLE_METHOD' (Proof_Context.fact_tac ctxt rules); (* assumption *) local fun cond_rtac ctxt cond rule = SUBGOAL (fn (prop, i) => if cond (Logic.strip_assums_concl prop) then resolve_tac ctxt [rule] i else no_tac); in fun assm_tac ctxt = assume_tac ctxt APPEND' Goal.assume_rule_tac ctxt APPEND' cond_rtac ctxt (can Logic.dest_equals) Drule.reflexive_thm APPEND' cond_rtac ctxt (can Logic.dest_term) Drule.termI; fun all_assm_tac ctxt = let fun tac i st = if i > Thm.nprems_of st then all_tac st else ((assm_tac ctxt i THEN tac i) ORELSE tac (i + 1)) st; in tac 1 end; fun assumption ctxt = METHOD (HEADGOAL o (fn [] => assm_tac ctxt | [fact] => solve_tac ctxt [fact] | _ => K no_tac)); fun finish immed ctxt = METHOD (K ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac ctxt)); end; (* rule etc. -- single-step refinements *) val rule_trace = Attrib.setup_config_bool \<^binding>\rule_trace\ (fn _ => false); fun trace ctxt rules = if Config.get ctxt rule_trace andalso not (null rules) then Pretty.big_list "rules:" (map (Thm.pretty_thm_item ctxt) rules) |> Pretty.string_of |> tracing else (); local fun gen_rule_tac tac ctxt rules facts = (fn i => fn st => if null facts then tac ctxt rules i st else Seq.maps (fn rule => (tac ctxt o single) rule i st) (Drule.multi_resolves (SOME ctxt) facts rules)) THEN_ALL_NEW Goal.norm_hhf_tac ctxt; fun gen_arule_tac tac ctxt j rules facts = EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j (assume_tac ctxt)); fun gen_some_rule_tac tac ctxt arg_rules facts = SUBGOAL (fn (goal, i) => let val rules = if not (null arg_rules) then arg_rules else flat (Context_Rules.find_rules ctxt false facts goal); in trace ctxt rules; tac ctxt rules facts i end); fun meth tac x y = METHOD (HEADGOAL o tac x y); fun meth' tac x y z = METHOD (HEADGOAL o tac x y z); in val rule_tac = gen_rule_tac resolve_tac; val rule = meth rule_tac; val some_rule_tac = gen_some_rule_tac rule_tac; val some_rule = meth some_rule_tac; val erule = meth' (gen_arule_tac eresolve_tac); val drule = meth' (gen_arule_tac dresolve_tac); val frule = meth' (gen_arule_tac forward_tac); end; (* intros_tac -- pervasive search spanned by intro rules *) fun gen_intros_tac goals ctxt intros facts = goals (insert_tac ctxt facts THEN' REPEAT_ALL_NEW (resolve_tac ctxt intros)) THEN Tactic.distinct_subgoals_tac; val intros_tac = gen_intros_tac ALLGOALS; val try_intros_tac = gen_intros_tac TRYALL; (** method syntax **) (* context data *) structure Data = Generic_Data ( type T = {methods: ((Token.src -> Proof.context -> method) * string) Name_Space.table, ml_tactic: (morphism -> thm list -> tactic) option, facts: thm list option}; val empty : T = {methods = Name_Space.empty_table "method", ml_tactic = NONE, facts = NONE}; val extend = I; fun merge ({methods = methods1, ml_tactic = ml_tactic1, facts = facts1}, {methods = methods2, ml_tactic = ml_tactic2, facts = facts2}) : T = {methods = Name_Space.merge_tables (methods1, methods2), ml_tactic = merge_options (ml_tactic1, ml_tactic2), facts = merge_options (facts1, facts2)}; ); fun map_data f = Data.map (fn {methods, ml_tactic, facts} => let val (methods', ml_tactic', facts') = f (methods, ml_tactic, facts) in {methods = methods', ml_tactic = ml_tactic', facts = facts'} end); val get_methods = #methods o Data.get; val ops_methods = {get_data = get_methods, put_data = fn methods => map_data (fn (_, ml_tactic, facts) => (methods, ml_tactic, facts))}; (* ML tactic *) fun set_tactic ml_tactic = map_data (fn (methods, _, facts) => (methods, SOME ml_tactic, facts)); fun the_tactic context = (case #ml_tactic (Data.get context) of SOME tac => tac | NONE => raise Fail "Undefined ML tactic"); val parse_tactic = Scan.state :|-- (fn context => Scan.lift (Args.text_declaration (fn source => let val tac = context |> ML_Context.expression (Input.pos_of source) (ML_Lex.read "Context.>> (Method.set_tactic (fn morphism: Morphism.morphism => fn facts: thm list => (" @ ML_Lex.read_source source @ ML_Lex.read ")))") |> the_tactic; in fn phi => set_tactic (fn _ => Context.setmp_generic_context (SOME context) (tac phi)) end)) >> (fn decl => Morphism.form (the_tactic (Morphism.form decl context)))); (* method facts *) val clean_facts = filter_out Thm.is_dummy; fun set_facts facts = (Context.proof_map o map_data) (fn (methods, ml_tactic, _) => (methods, ml_tactic, SOME (clean_facts facts))); val get_facts_generic = these o #facts o Data.get; val get_facts = get_facts_generic o Context.Proof; val _ = Theory.setup (Global_Theory.add_thms_dynamic (Binding.make ("method_facts", \<^here>), get_facts_generic)); (* method text *) datatype combinator_info = Combinator_Info of {keywords: Position.T list}; fun combinator_info keywords = Combinator_Info {keywords = keywords}; val no_combinator_info = combinator_info []; datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int; datatype text = Source of Token.src | Basic of Proof.context -> method | Combinator of combinator_info * combinator * text list; fun map_source f (Source src) = Source (f src) | map_source _ (Basic meth) = Basic meth | map_source f (Combinator (info, comb, txts)) = Combinator (info, comb, map (map_source f) txts); fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r); val succeed_text = Basic (K succeed); val standard_text = Source (Token.make_src ("standard", Position.none) []); val this_text = Basic this; val done_text = Basic (K (SIMPLE_METHOD all_tac)); fun sorry_text int = Basic (fn _ => cheating int); fun finish_text (NONE, immed) = Basic (finish immed) | finish_text (SOME txt, immed) = Combinator (no_combinator_info, Then, [txt, Basic (finish immed)]); (* method definitions *) fun print_methods verbose ctxt = let val meths = get_methods (Context.Proof ctxt); fun prt_meth (name, (_, "")) = Pretty.mark_str name | prt_meth (name, (_, comment)) = Pretty.block (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment); in [Pretty.big_list "methods:" (map prt_meth (Name_Space.markup_table verbose ctxt meths))] |> Pretty.writeln_chunks end; (* define *) fun define_global binding meth comment = Entity.define_global ops_methods binding (meth, comment); fun define binding meth comment = Entity.define ops_methods binding (meth, comment); (* check *) fun check_name ctxt = let val context = Context.Proof ctxt in #1 o Name_Space.check context (get_methods context) end; fun check_src ctxt = #1 o Token.check_src ctxt (get_methods o Context.Proof); fun check_text ctxt (Source src) = Source (check_src ctxt src) | check_text _ (Basic m) = Basic m | check_text ctxt (Combinator (x, y, body)) = Combinator (x, y, map (check_text ctxt) body); fun checked_text (Source src) = Token.checked_src src | checked_text (Basic _) = true | checked_text (Combinator (_, _, body)) = forall checked_text body; (* method setup *) fun method_syntax scan src ctxt : method = let val (m, ctxt') = Token.syntax scan src ctxt in m ctxt' end; fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd; fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd; fun method_setup binding source comment = ML_Context.expression (Input.pos_of source) (ML_Lex.read ("Theory.local_setup (Method.local_setup (" ^ ML_Syntax.make_binding binding ^ ") (") @ ML_Lex.read_source source @ ML_Lex.read (")" ^ ML_Syntax.print_string comment ^ ")")) |> Context.proof_map; (* prepare methods *) fun method ctxt = let val table = get_methods (Context.Proof ctxt) in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end; fun method_closure ctxt src = let val src' = map Token.init_assignable src; val ctxt' = Context_Position.not_really ctxt; val _ = Seq.pull (method ctxt' src' ctxt' [] (ctxt', Goal.protect 0 Drule.dummy_thm)); in map Token.closure src' end; val closure = Config.declare_bool ("Method.closure", \<^here>) (K true); fun method_cmd ctxt = check_src ctxt #> Config.get ctxt closure ? method_closure ctxt #> method ctxt; (* static vs. runtime state *) fun detect_closure_state st = (case try Logic.dest_term (Thm.concl_of (perhaps (try Goal.conclude) st)) of NONE => false | SOME t => Term.is_dummy_pattern t); fun STATIC test : context_tactic = fn (ctxt, st) => if detect_closure_state st then (test (); Seq.single (Seq.Result (ctxt, st))) else Seq.empty; fun RUNTIME (tac: context_tactic) (ctxt, st) = if detect_closure_state st then Seq.empty else tac (ctxt, st); fun sleep t = RUNTIME (fn ctxt_st => (OS.Process.sleep t; Seq.single (Seq.Result ctxt_st))); (* evaluate method text *) local val op THEN = Seq.THEN; fun BYPASS_CONTEXT (tac: tactic) = fn result => (case result of Seq.Error _ => Seq.single result | Seq.Result (ctxt, st) => tac st |> TACTIC_CONTEXT ctxt); val preparation = BYPASS_CONTEXT (ALLGOALS Goal.conjunction_tac); fun RESTRICT_GOAL i n method = BYPASS_CONTEXT (PRIMITIVE (Goal.restrict i n)) THEN method THEN BYPASS_CONTEXT (PRIMITIVE (Goal.unrestrict i)); fun SELECT_GOAL method i = RESTRICT_GOAL i 1 method; fun (method1 THEN_ALL_NEW method2) i (result : context_state Seq.result) = (case result of Seq.Error _ => Seq.single result | Seq.Result (_, st) => result |> method1 i |> Seq.maps (fn result' => (case result' of Seq.Error _ => Seq.single result' | Seq.Result (_, st') => result' |> Seq.INTERVAL method2 i (i + Thm.nprems_of st' - Thm.nprems_of st)))) fun COMBINATOR1 comb [meth] = comb meth | COMBINATOR1 _ _ = raise Fail "Method combinator requires exactly one argument"; fun combinator Then = Seq.EVERY | combinator Then_All_New = (fn [] => Seq.single | methods => preparation THEN (foldl1 (op THEN_ALL_NEW) (map SELECT_GOAL methods) 1)) | combinator Orelse = Seq.FIRST | combinator Try = COMBINATOR1 Seq.TRY | combinator Repeat1 = COMBINATOR1 Seq.REPEAT1 | combinator (Select_Goals n) = COMBINATOR1 (fn method => preparation THEN RESTRICT_GOAL 1 n method); in fun evaluate text ctxt0 facts = let val ctxt = set_facts facts ctxt0; fun eval0 m = Seq.single #> Seq.maps_results (m facts); fun eval (Basic m) = eval0 (m ctxt) | eval (Source src) = eval0 (method_cmd ctxt src ctxt) | eval (Combinator (_, c, txts)) = combinator c (map eval txts); in eval text o Seq.Result end; end; fun evaluate_runtime text ctxt = let val text' = text |> (map_source o map o Token.map_facts) (fn SOME name => (case Proof_Context.lookup_fact ctxt name of SOME {dynamic = true, thms} => K thms | _ => I) | NONE => I); val ctxt' = Config.put closure false ctxt; in fn facts => RUNTIME (fn st => evaluate text' ctxt' facts st) end; (** concrete syntax **) (* type modifier *) type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}; fun modifier attribute pos : modifier = {init = I, attribute = attribute, pos = pos}; (* sections *) val old_section_parser = Config.declare_bool ("Method.old_section_parser", \<^here>) (K false); local fun thms ss = Scan.repeats (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm); fun app {init, attribute, pos = _} ths context = fold_map (Thm.apply_attribute attribute) ths (Context.map_proof init context); fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|-- (fn (m, ths) => Scan.succeed (swap (app m ths context)))); in fun old_sections ss = Scan.repeat (section ss) >> K (); end; local fun sect (modifier : modifier parser) = Scan.depend (fn context => Scan.ahead Parse.not_eof -- Scan.trace modifier -- Scan.repeat (Scan.unless modifier Parse.thm) >> (fn ((tok0, ({init, attribute, pos}, modifier_toks)), xthms) => let val decl = (case Token.get_value tok0 of SOME (Token.Declaration decl) => decl | _ => let val ctxt = Context.proof_of context; val prep_att = Attrib.check_src ctxt #> map (Token.assign NONE); val thms = map (fn (a, bs) => (Proof_Context.get_fact ctxt a, map prep_att bs)) xthms; val facts = Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)] |> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K attribute)]), bs)); fun decl phi = Context.mapping I init #> Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd; val modifier_report = (#1 (Token.range_of modifier_toks), - Markup.properties (Position.def_properties_of pos) - (Markup.entity Markup.method_modifierN "")); + Position.entity_markup Markup.method_modifierN ("", pos)); val _ = Context_Position.reports ctxt (modifier_report :: Token.reports_of_value tok0); val _ = Token.assign (SOME (Token.Declaration decl)) tok0; in decl end); in (Morphism.form decl context, decl) end)); in fun sections ss = Args.context :|-- (fn ctxt => if Config.get ctxt old_section_parser then old_sections ss else Scan.repeat (sect (Scan.first ss)) >> K ()); end; (* extra rule methods *) fun xrule_meth meth = Scan.lift (Scan.optional (Args.parens Parse.nat) 0) -- Attrib.thms >> (fn (n, ths) => fn ctxt => meth ctxt n ths); (* text range *) type text_range = text * Position.range; fun text NONE = NONE | text (SOME (txt, _)) = SOME txt; fun position NONE = Position.none | position (SOME (_, (pos, _))) = pos; (* reports *) local fun keyword_positions (Source _) = [] | keyword_positions (Basic _) = [] | keyword_positions (Combinator (Combinator_Info {keywords}, _, texts)) = keywords @ maps keyword_positions texts; in fun reports_of ((text, (pos, _)): text_range) = (pos, Markup.language_method) :: maps (fn p => map (pair p) (Markup.keyword3 :: Completion.suppress_abbrevs "")) (keyword_positions text); fun report text_range = if Context_Position.pide_reports () then Position.reports (reports_of text_range) else (); end; (* parser *) local fun is_symid_meth s = s <> "|" andalso s <> "?" andalso s <> "+" andalso Token.ident_or_symbolic s; in fun parser pri = let val meth_name = Parse.token Parse.name; fun meth5 x = (meth_name >> (Source o single) || Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok => Source (Token.make_src ("cartouche", Position.none) [tok])) || Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x and meth4 x = (meth5 -- Parse.position (Parse.$$$ "?") >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) || meth5 -- Parse.position (Parse.$$$ "+") >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) || meth5 -- (Parse.position (Parse.$$$ "[") -- Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]")) >> (fn (m, (((_, pos1), n), (_, pos2))) => Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) || meth5) x and meth3 x = (meth_name ::: Parse.args1 is_symid_meth >> Source || meth4) x and meth2 x = (Parse.enum1_positions "," meth3 >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then, ms))) x and meth1 x = (Parse.enum1_positions ";" meth2 >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then_All_New, ms))) x and meth0 x = (Parse.enum1_positions "|" meth1 >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Orelse, ms))) x; val meth = nth [meth0, meth1, meth2, meth3, meth4, meth5] pri handle General.Subscript => raise Fail ("Bad method parser priority " ^ string_of_int pri); in Scan.trace meth >> (fn (m, toks) => (m, Token.range_of toks)) end; val parse = parser 4; end; (* read method text *) fun read ctxt src = (case Scan.read Token.stopper (Parse.!!! (parser 0 --| Scan.ahead Parse.eof)) src of SOME (text, range) => if checked_text text then text else (report (text, range); check_text ctxt text) | NONE => error ("Failed to parse method" ^ Position.here (#1 (Token.range_of src)))); fun read_closure ctxt src0 = let val src1 = map Token.init_assignable src0; val text = read ctxt src1 |> map_source (method_closure ctxt); val src2 = map Token.closure src1; in (text, src2) end; fun read_closure_input ctxt input = let val syms = Input.source_explode input in (case Token.read_body (Thy_Header.get_keywords' ctxt) (Scan.many Token.not_eof) syms of SOME res => read_closure ctxt res | NONE => error ("Bad input" ^ Position.here (Input.pos_of input))) end; val text_closure = Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) => (case Token.get_value tok of SOME (Token.Source src) => read ctxt src | _ => let val (text, src) = read_closure_input ctxt (Token.input_of tok); val _ = Token.assign (SOME (Token.Source src)) tok; in text end)); (* theory setup *) val _ = Theory.setup (setup \<^binding>\fail\ (Scan.succeed (K fail)) "force failure" #> setup \<^binding>\succeed\ (Scan.succeed (K succeed)) "succeed" #> setup \<^binding>\sleep\ (Scan.lift Parse.real >> (fn s => fn _ => fn _ => sleep (seconds s))) "succeed after delay (in seconds)" #> setup \<^binding>\-\ (Scan.succeed (K (SIMPLE_METHOD all_tac))) "insert current facts, nothing else" #> setup \<^binding>\goal_cases\ (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn _ => CONTEXT_METHOD (fn _ => fn (ctxt, st) => (case drop (Thm.nprems_of st) names of [] => NONE | bad => if detect_closure_state st then NONE else SOME (fn () => ("Excessive case name(s): " ^ commas_quote (map Token.content_of bad) ^ Position.here (#1 (Token.range_of bad))))) |> (fn SOME msg => Seq.single (Seq.Error msg) | NONE => goal_cases_tac (map Token.content_of names) (ctxt, st))))) "bind cases for goals" #> setup \<^binding>\subproofs\ (text_closure >> (Context_Tactic.SUBPROOFS ooo evaluate_runtime)) "apply proof method to subproofs with closed derivation" #> setup \<^binding>\insert\ (Attrib.thms >> (K o insert)) "insert theorems, ignoring facts" #> setup \<^binding>\intro\ (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths)) "repeatedly apply introduction rules" #> setup \<^binding>\elim\ (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths)) "repeatedly apply elimination rules" #> setup \<^binding>\unfold\ (Attrib.thms >> unfold_meth) "unfold definitions" #> setup \<^binding>\fold\ (Attrib.thms >> fold_meth) "fold definitions" #> setup \<^binding>\atomize\ (Scan.lift (Args.mode "full") >> atomize) "present local premises as object-level statements" #> setup \<^binding>\rule\ (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths)) "apply some intro/elim rule" #> setup \<^binding>\erule\ (xrule_meth erule) "apply rule in elimination manner (improper)" #> setup \<^binding>\drule\ (xrule_meth drule) "apply rule in destruct manner (improper)" #> setup \<^binding>\frule\ (xrule_meth frule) "apply rule in forward manner (improper)" #> setup \<^binding>\this\ (Scan.succeed this) "apply current facts as rules" #> setup \<^binding>\fact\ (Attrib.thms >> fact) "composition by facts from context" #> setup \<^binding>\assumption\ (Scan.succeed assumption) "proof by assumption, preferring facts" #> setup \<^binding>\rename_tac\ (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >> (fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs)))) "rename parameters of goal" #> setup \<^binding>\rotate_tac\ (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >> (fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i)))) "rotate assumptions of goal" #> setup \<^binding>\tactic\ (parse_tactic >> (K o METHOD)) "ML tactic as proof method" #> setup \<^binding>\raw_tactic\ (parse_tactic >> (fn tac => fn _ => Context_Tactic.CONTEXT_TACTIC o tac)) "ML tactic as raw proof method" #> setup \<^binding>\use\ (Attrib.thms -- (Scan.lift (Parse.$$$ "in") |-- text_closure) >> (fn (thms, text) => fn ctxt => fn _ => evaluate_runtime text ctxt thms)) "indicate method facts and context for method expression"); (*final declarations of this structure!*) val unfold = unfold_meth; val fold = fold_meth; end; val CONTEXT_METHOD = Method.CONTEXT_METHOD; val METHOD = Method.METHOD; val SIMPLE_METHOD = Method.SIMPLE_METHOD; val SIMPLE_METHOD' = Method.SIMPLE_METHOD'; val SIMPLE_METHOD'' = Method.SIMPLE_METHOD''; diff --git a/src/Pure/Isar/proof_context.ML b/src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML +++ b/src/Pure/Isar/proof_context.ML @@ -1,1649 +1,1647 @@ (* Title: Pure/Isar/proof_context.ML Author: Markus Wenzel, TU Muenchen The key concept of Isar proof contexts: elevates primitive local reasoning Gamma |- phi to a structured concept, with generic context elements. See also structure Variable and Assumption. *) signature PROOF_CONTEXT = sig val theory_of: Proof.context -> theory val init_global: theory -> Proof.context val get_global: theory -> string -> Proof.context type mode val mode_default: mode val mode_pattern: mode val mode_schematic: mode val mode_abbrev: mode val set_mode: mode -> Proof.context -> Proof.context val get_mode: Proof.context -> mode val restore_mode: Proof.context -> Proof.context -> Proof.context val abbrev_mode: Proof.context -> bool val syn_of: Proof.context -> Syntax.syntax val tsig_of: Proof.context -> Type.tsig val set_defsort: sort -> Proof.context -> Proof.context val default_sort: Proof.context -> indexname -> sort val arity_sorts: Proof.context -> string -> sort -> sort list val consts_of: Proof.context -> Consts.T val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context val naming_of: Proof.context -> Name_Space.naming val restore_naming: Proof.context -> Proof.context -> Proof.context val full_name: Proof.context -> binding -> string val get_scope: Proof.context -> Binding.scope option val new_scope: Proof.context -> Binding.scope * Proof.context val private_scope: Binding.scope -> Proof.context -> Proof.context val private: Position.T -> Proof.context -> Proof.context val qualified_scope: Binding.scope -> Proof.context -> Proof.context val qualified: Position.T -> Proof.context -> Proof.context val concealed: Proof.context -> Proof.context val class_space: Proof.context -> Name_Space.T val type_space: Proof.context -> Name_Space.T val const_space: Proof.context -> Name_Space.T val defs_context: Proof.context -> Defs.context val intern_class: Proof.context -> xstring -> string val intern_type: Proof.context -> xstring -> string val intern_const: Proof.context -> xstring -> string val extern_class: Proof.context -> string -> xstring val markup_class: Proof.context -> string -> string val pretty_class: Proof.context -> string -> Pretty.T val extern_type: Proof.context -> string -> xstring val markup_type: Proof.context -> string -> string val pretty_type: Proof.context -> string -> Pretty.T val extern_const: Proof.context -> string -> xstring val markup_const: Proof.context -> string -> string val pretty_const: Proof.context -> string -> Pretty.T val transfer: theory -> Proof.context -> Proof.context val transfer_facts: theory -> Proof.context -> Proof.context val background_theory: (theory -> theory) -> Proof.context -> Proof.context val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context val facts_of: Proof.context -> Facts.T val facts_of_fact: Proof.context -> string -> Facts.T val markup_extern_fact: Proof.context -> string -> Markup.T list * xstring val augment: term -> Proof.context -> Proof.context val print_name: Proof.context -> string -> string val pretty_name: Proof.context -> string -> Pretty.T val pretty_term_abbrev: Proof.context -> term -> Pretty.T val pretty_fact: Proof.context -> string * thm list -> Pretty.T val check_class: Proof.context -> xstring * Position.T -> class * Position.report list val read_class: Proof.context -> string -> class val read_typ: Proof.context -> string -> typ val read_typ_syntax: Proof.context -> string -> typ val read_typ_abbrev: Proof.context -> string -> typ val cert_typ: Proof.context -> typ -> typ val cert_typ_syntax: Proof.context -> typ -> typ val cert_typ_abbrev: Proof.context -> typ -> typ val infer_type: Proof.context -> string * typ -> typ val inferred_param: string -> Proof.context -> (string * typ) * Proof.context val inferred_fixes: Proof.context -> (string * typ) list * Proof.context val check_type_name: {proper: bool, strict: bool} -> Proof.context -> xstring * Position.T -> typ * Position.report list val read_type_name: {proper: bool, strict: bool} -> Proof.context -> string -> typ val consts_completion_message: Proof.context -> xstring * Position.T list -> string val check_const: {proper: bool, strict: bool} -> Proof.context -> xstring * Position.T list -> term * Position.report list val read_const: {proper: bool, strict: bool} -> Proof.context -> string -> term val read_arity: Proof.context -> xstring * string list * string -> arity val cert_arity: Proof.context -> arity -> arity val allow_dummies: Proof.context -> Proof.context val prepare_sortsT: Proof.context -> typ list -> string list * typ list val prepare_sorts: Proof.context -> term list -> string list * term list val check_tfree: Proof.context -> string * sort -> string * sort val read_term_pattern: Proof.context -> string -> term val read_term_schematic: Proof.context -> string -> term val read_term_abbrev: Proof.context -> string -> term val show_abbrevs: bool Config.T val expand_abbrevs: Proof.context -> term -> term val cert_term: Proof.context -> term -> term val cert_prop: Proof.context -> term -> term val def_type: Proof.context -> indexname -> typ option val standard_typ_check: Proof.context -> typ list -> typ list val standard_term_check_finish: Proof.context -> term list -> term list val standard_term_uncheck: Proof.context -> term list -> term list val goal_export: Proof.context -> Proof.context -> thm list -> thm list val export: Proof.context -> Proof.context -> thm list -> thm list val export_morphism: Proof.context -> Proof.context -> morphism val norm_export_morphism: Proof.context -> Proof.context -> morphism val auto_bind_goal: term list -> Proof.context -> Proof.context val auto_bind_facts: term list -> Proof.context -> Proof.context val simult_matches: Proof.context -> term * term list -> (indexname * term) list val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context val bind_term: indexname * term -> Proof.context -> Proof.context val cert_propp: Proof.context -> (term * term list) list list -> (term list list * (indexname * term) list) val read_propp: Proof.context -> (string * string list) list list -> (term list list * (indexname * term) list) val fact_tac: Proof.context -> thm list -> int -> tactic val some_fact_tac: Proof.context -> int -> tactic val lookup_fact: Proof.context -> string -> {dynamic: bool, thms: thm list} option val dynamic_facts_dummy: bool Config.T val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list val get_fact: Proof.context -> Facts.ref -> thm list val get_fact_single: Proof.context -> Facts.ref -> thm val get_thms: Proof.context -> xstring -> thm list val get_thm: Proof.context -> xstring -> thm val is_stmt: Proof.context -> bool val set_stmt: bool -> Proof.context -> Proof.context val restore_stmt: Proof.context -> Proof.context -> Proof.context val add_thms_dynamic: binding * (Context.generic -> thm list) -> Proof.context -> string * Proof.context val add_thms_lazy: string -> (binding * thm list lazy) -> Proof.context -> Proof.context val note_thms: string -> Thm.binding * (thm list * attribute list) list -> Proof.context -> (string * thm list) * Proof.context val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list -> Proof.context -> (string * thm list) list * Proof.context val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context val alias_fact: binding -> string -> Proof.context -> Proof.context val read_var: binding * string option * mixfix -> Proof.context -> (binding * typ option * mixfix) * Proof.context val cert_var: binding * typ option * mixfix -> Proof.context -> (binding * typ option * mixfix) * Proof.context val add_fixes: (binding * typ option * mixfix) list -> Proof.context -> string list * Proof.context val add_fixes_cmd: (binding * string option * mixfix) list -> Proof.context -> string list * Proof.context val add_assms: Assumption.export -> (Thm.binding * (term * term list) list) list -> Proof.context -> (string * thm list) list * Proof.context val add_assms_cmd: Assumption.export -> (Thm.binding * (string * string list) list) list -> Proof.context -> (string * thm list) list * Proof.context val dest_cases: Proof.context option -> Proof.context -> (string * Rule_Cases.T) list val update_cases: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context val check_case: Proof.context -> bool -> string * Position.T -> binding option list -> Rule_Cases.T val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context val generic_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism -> Context.generic -> Context.generic val generic_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism -> Context.generic -> Context.generic val type_alias: binding -> string -> Proof.context -> Proof.context val const_alias: binding -> string -> Proof.context -> Proof.context val add_const_constraint: string * typ option -> Proof.context -> Proof.context val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context val revert_abbrev: string -> string -> Proof.context -> Proof.context val generic_add_abbrev: string -> binding * term -> Context.generic -> (term * term) * Context.generic val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic type stmt = {vars: ((binding * typ option * mixfix) * (string * term)) list, propss: term list list, binds: (indexname * term) list, result_binds: (indexname * term) list} val cert_stmt: (binding * typ option * mixfix) list -> (term * term list) list list -> Proof.context -> stmt * Proof.context val read_stmt: (binding * string option * mixfix) list -> (string * string list) list list -> Proof.context -> stmt * Proof.context type statement = {fixes: (string * term) list, assumes: term list list, shows: term list list, result_binds: (indexname * term option) list, text: term, result_text: term} val cert_statement: (binding * typ option * mixfix) list -> (term * term list) list list -> (term * term list) list list -> Proof.context -> statement * Proof.context val read_statement: (binding * string option * mixfix) list -> (string * string list) list list -> (string * string list) list list -> Proof.context -> statement * Proof.context val print_syntax: Proof.context -> unit val print_abbrevs: bool -> Proof.context -> unit val pretty_term_bindings: Proof.context -> Pretty.T list val pretty_local_facts: bool -> Proof.context -> Pretty.T list val print_local_facts: bool -> Proof.context -> unit val pretty_cases: Proof.context -> Pretty.T list val print_cases_proof: Proof.context -> Proof.context -> string val debug: bool Config.T val verbose: bool Config.T val pretty_ctxt: Proof.context -> Pretty.T list val pretty_context: Proof.context -> Pretty.T list end; structure Proof_Context: PROOF_CONTEXT = struct val theory_of = Proof_Context.theory_of; val init_global = Proof_Context.init_global; val get_global = Proof_Context.get_global; (** inner syntax mode **) datatype mode = Mode of {pattern: bool, (*pattern binding schematic variables*) schematic: bool, (*term referencing loose schematic variables*) abbrev: bool}; (*abbrev mode -- no normalization*) fun make_mode (pattern, schematic, abbrev) = Mode {pattern = pattern, schematic = schematic, abbrev = abbrev}; val mode_default = make_mode (false, false, false); val mode_pattern = make_mode (true, false, false); val mode_schematic = make_mode (false, true, false); val mode_abbrev = make_mode (false, false, true); (** Isar proof context information **) type cases = Rule_Cases.T Name_Space.table; val empty_cases: cases = Name_Space.empty_table Markup.caseN; datatype data = Data of {mode: mode, (*inner syntax mode*) syntax: Local_Syntax.T, (*local syntax*) tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*) consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*) facts: Facts.T, (*local facts, based on initial global facts*) cases: cases}; (*named case contexts*) fun make_data (mode, syntax, tsig, consts, facts, cases) = Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases}; structure Data = Proof_Data ( type T = data; fun init thy = make_data (mode_default, Local_Syntax.init thy, (Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy), (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy), Global_Theory.facts_of thy, empty_cases); ); fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); fun map_data_result f ctxt = let val Data {mode, syntax, tsig, consts, facts, cases} = Data.get ctxt; val (res, data') = f (mode, syntax, tsig, consts, facts, cases) ||> make_data; in (res, Data.put data' ctxt) end; fun map_data f = snd o map_data_result (pair () o f); fun set_mode mode = map_data (fn (_, syntax, tsig, consts, facts, cases) => (mode, syntax, tsig, consts, facts, cases)); fun map_syntax f = map_data (fn (mode, syntax, tsig, consts, facts, cases) => (mode, f syntax, tsig, consts, facts, cases)); fun map_syntax_idents f ctxt = let val (opt_idents', syntax') = f (#syntax (rep_data ctxt)) in ctxt |> map_syntax (K syntax') |> (case opt_idents' of NONE => I | SOME idents' => Syntax_Trans.put_idents idents') end; fun map_tsig f = map_data (fn (mode, syntax, tsig, consts, facts, cases) => (mode, syntax, f tsig, consts, facts, cases)); fun map_consts f = map_data (fn (mode, syntax, tsig, consts, facts, cases) => (mode, syntax, tsig, f consts, facts, cases)); fun map_facts_result f = map_data_result (fn (mode, syntax, tsig, consts, facts, cases) => let val (res, facts') = f facts in (res, (mode, syntax, tsig, consts, facts', cases)) end); fun map_facts f = snd o map_facts_result (pair () o f); fun map_cases f = map_data (fn (mode, syntax, tsig, consts, facts, cases) => (mode, syntax, tsig, consts, facts, f cases)); val get_mode = #mode o rep_data; val restore_mode = set_mode o get_mode; val abbrev_mode = get_mode #> (fn Mode {abbrev, ...} => abbrev); val syntax_of = #syntax o rep_data; val syn_of = Local_Syntax.syn_of o syntax_of; val set_syntax_mode = map_syntax o Local_Syntax.set_mode; val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of; val tsig_of = #1 o #tsig o rep_data; val set_defsort = map_tsig o apfst o Type.set_defsort; fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt; fun arity_sorts ctxt = Type.arity_sorts (Context.Proof ctxt) (tsig_of ctxt); val consts_of = #1 o #consts o rep_data; val cases_of = #cases o rep_data; (* naming *) val naming_of = Name_Space.naming_of o Context.Proof; val map_naming = Context.proof_map o Name_Space.map_naming; val restore_naming = map_naming o K o naming_of; val full_name = Name_Space.full_name o naming_of; val get_scope = Name_Space.get_scope o naming_of; fun new_scope ctxt = let val (scope, naming') = Name_Space.new_scope (naming_of ctxt); val ctxt' = map_naming (K naming') ctxt; in (scope, ctxt') end; val private_scope = map_naming o Name_Space.private_scope; val private = map_naming o Name_Space.private; val qualified_scope = map_naming o Name_Space.qualified_scope; val qualified = map_naming o Name_Space.qualified; val concealed = map_naming Name_Space.concealed; (* name spaces *) val class_space = Type.class_space o tsig_of; val type_space = Type.type_space o tsig_of; val const_space = Consts.space_of o consts_of; fun defs_context ctxt = (ctxt, (const_space ctxt, type_space ctxt)); val intern_class = Name_Space.intern o class_space; val intern_type = Name_Space.intern o type_space; val intern_const = Name_Space.intern o const_space; fun extern_class ctxt = Name_Space.extern ctxt (class_space ctxt); fun extern_type ctxt = Name_Space.extern ctxt (type_space ctxt); fun extern_const ctxt = Name_Space.extern ctxt (const_space ctxt); fun markup_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |-> Markup.markup; fun markup_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |-> Markup.markup; fun markup_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c |-> Markup.markup; fun pretty_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |> Pretty.mark_str; fun pretty_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |> Pretty.mark_str; fun pretty_const ctxt c = Name_Space.markup_extern ctxt (const_space ctxt) c |> Pretty.mark_str; (* theory transfer *) fun transfer_syntax thy ctxt = ctxt |> map_syntax (Local_Syntax.rebuild thy) |> map_tsig (fn tsig as (local_tsig, global_tsig) => let val thy_tsig = Sign.tsig_of thy in if Type.eq_tsig (thy_tsig, global_tsig) then tsig else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig) (*historic merge order*) end) |> map_consts (fn consts as (local_consts, global_consts) => let val thy_consts = Sign.consts_of thy in if Consts.eq_consts (thy_consts, global_consts) then consts else (Consts.merge (local_consts, thy_consts), thy_consts) (*historic merge order*) end); fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy; fun transfer_facts thy = map_facts (fn local_facts => Facts.merge (Global_Theory.facts_of thy, local_facts)); fun background_theory f ctxt = transfer (f (theory_of ctxt)) ctxt; fun background_theory_result f ctxt = let val (res, thy') = f (theory_of ctxt) in (res, ctxt |> transfer thy') end; (* hybrid facts *) val facts_of = #facts o rep_data; fun facts_of_fact ctxt name = let val local_facts = facts_of ctxt; val global_facts = Global_Theory.facts_of (theory_of ctxt); in if Facts.defined local_facts name then local_facts else global_facts end; fun markup_extern_fact ctxt name = let val facts = facts_of_fact ctxt name; val (markup, xname) = Facts.markup_extern ctxt facts name; val markups = if Facts.is_dynamic facts name then [markup, Markup.dynamic_fact name] else [markup]; in (markups, xname) end; (* augment context by implicit term declarations *) fun augment t ctxt = ctxt |> Variable.add_fixes_implicit t |> Variable.declare_term t |> Soft_Type_System.augment t; (** pretty printing **) val print_name = Token.print_name o Thy_Header.get_keywords'; val pretty_name = Pretty.str oo print_name; fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt); fun pretty_fact_name ctxt a = Pretty.block [Pretty.marks_str (markup_extern_fact ctxt a), Pretty.str ":"]; fun pretty_fact ctxt = let val pretty_thm = Thm.pretty_thm ctxt; val pretty_thms = map (Thm.pretty_thm_item ctxt); in fn ("", [th]) => pretty_thm th | ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths)) | (a, [th]) => Pretty.block [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm th] | (a, ths) => Pretty.block (Pretty.fbreaks (pretty_fact_name ctxt a :: pretty_thms ths)) end; (** prepare types **) (* classes *) fun check_class ctxt (xname, pos) = let val tsig = tsig_of ctxt; val class_space = Type.class_space tsig; val name = Type.cert_class tsig (Name_Space.intern class_space xname) handle TYPE (msg, _, _) => error (msg ^ Position.here pos ^ Completion.markup_report [Name_Space.completion (Context.Proof ctxt) class_space (K true) (xname, pos)]); val reports = if Context_Position.is_reported ctxt pos then [(pos, Name_Space.markup class_space name)] else []; in (name, reports) end; fun read_class ctxt text = let val source = Syntax.read_input text; val (c, reports) = check_class ctxt (Input.source_content source); val _ = Context_Position.reports ctxt reports; in c end; (* types *) fun read_typ_mode mode ctxt s = Syntax.read_typ (Type.set_mode mode ctxt) s; val read_typ = read_typ_mode Type.mode_default; val read_typ_syntax = read_typ_mode Type.mode_syntax; val read_typ_abbrev = read_typ_mode Type.mode_abbrev; fun cert_typ_mode mode ctxt T = Type.cert_typ_mode mode (tsig_of ctxt) T handle TYPE (msg, _, _) => error msg; val cert_typ = cert_typ_mode Type.mode_default; val cert_typ_syntax = cert_typ_mode Type.mode_syntax; val cert_typ_abbrev = cert_typ_mode Type.mode_abbrev; (** prepare terms and propositions **) (* inferred types of parameters *) fun infer_type ctxt x = Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x)); fun inferred_param x ctxt = let val p = (x, infer_type ctxt (x, dummyT)) in (p, ctxt |> Variable.declare_term (Free p)) end; fun inferred_fixes ctxt = fold_map inferred_param (map #2 (Variable.dest_fixes ctxt)) ctxt; (* type names *) fun check_type_name {proper, strict} ctxt (c, pos) = if Lexicon.is_tid c then if proper then error ("Not a type constructor: " ^ quote c ^ Position.here pos) else let val reports = if Context_Position.is_reported ctxt pos then [(pos, Markup.tfree)] else []; in (TFree (c, default_sort ctxt (c, ~1)), reports) end else let val ((d, reports), decl) = Type.check_decl (Context.Proof ctxt) (tsig_of ctxt) (c, pos); fun err () = error ("Bad type name: " ^ quote d ^ Position.here pos); val args = (case decl of Type.LogicalType n => n | Type.Abbreviation (vs, _, _) => if strict then err () else length vs | Type.Nonterminal => if strict then err () else 0); in (Type (d, replicate args dummyT), reports) end; fun read_type_name flags ctxt text = let val source = Syntax.read_input text; val (T, reports) = check_type_name flags ctxt (Input.source_content source); val _ = Context_Position.reports ctxt reports; in T end; (* constant names *) fun consts_completion_message ctxt (c, ps) = ps |> map (fn pos => Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (K true) (c, pos)) |> Completion.markup_report; fun check_const {proper, strict} ctxt (c, ps) = let val _ = Name.reject_internal (c, ps) handle ERROR msg => error (msg ^ consts_completion_message ctxt (c, ps)); fun err msg = error (msg ^ Position.here_list ps); val consts = consts_of ctxt; val fixed = if proper then NONE else Variable.lookup_fixed ctxt c; val (t, reports) = (case (fixed, Variable.lookup_const ctxt c) of (SOME x, NONE) => let val reports = ps |> filter (Context_Position.is_reported ctxt) |> map (fn pos => (pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free))); in (Free (x, infer_type ctxt (x, dummyT)), reports) end | (_, SOME d) => let val T = Consts.type_scheme consts d handle TYPE (msg, _, _) => err msg; val reports = ps |> filter (Context_Position.is_reported ctxt) |> map (fn pos => (pos, Name_Space.markup (Consts.space_of consts) d)); in (Const (d, T), reports) end | _ => Consts.check_const (Context.Proof ctxt) consts (c, ps)); val _ = (case (strict, t) of (true, Const (d, _)) => (ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg) | _ => ()); in (t, reports) end; fun read_const flags ctxt text = let val source = Syntax.read_input text; val (c, pos) = Input.source_content source; val (t, reports) = check_const flags ctxt (c, [pos]); val _ = Context_Position.reports ctxt reports; in t end; (* type arities *) local fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) = let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S) in Type.add_arity (Context.Proof ctxt) arity (tsig_of ctxt); arity end; in val read_arity = prep_arity ((#1 o dest_Type) oo read_type_name {proper = true, strict = true}) Syntax.read_sort; val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of); end; (* read_term *) fun read_term_mode mode ctxt = Syntax.read_term (set_mode mode ctxt); val read_term_pattern = read_term_mode mode_pattern; val read_term_schematic = read_term_mode mode_schematic; val read_term_abbrev = read_term_mode mode_abbrev; (* local abbreviations *) local fun certify_consts ctxt = Consts.certify (Context.Proof ctxt) (tsig_of ctxt) (not (abbrev_mode ctxt)) (consts_of ctxt); fun expand_binds ctxt = let val Mode {pattern, schematic, ...} = get_mode ctxt; fun reject_schematic (t as Var _) = error ("Unbound schematic variable: " ^ Syntax.string_of_term ctxt t) | reject_schematic (Abs (_, _, t)) = reject_schematic t | reject_schematic (t $ u) = (reject_schematic t; reject_schematic u) | reject_schematic _ = (); in if pattern then I else Variable.expand_binds ctxt #> (if schematic then I else tap reject_schematic) end; in fun expand_abbrevs ctxt = certify_consts ctxt #> expand_binds ctxt; end; val show_abbrevs = Config.declare_bool ("show_abbrevs", \<^here>) (K true); fun contract_abbrevs ctxt t = let val thy = theory_of ctxt; val consts = consts_of ctxt; val Mode {abbrev, ...} = get_mode ctxt; val retrieve = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]); fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u)); in if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of t) then t else Pattern.rewrite_term_top thy [] [match_abbrev] t end; (* patterns *) fun prepare_patternT ctxt T = let val Mode {pattern, schematic, ...} = get_mode ctxt; val _ = pattern orelse schematic orelse T |> Term.exists_subtype (fn T as TVar (xi, _) => not (Type_Infer.is_param xi) andalso error ("Illegal schematic type variable: " ^ Syntax.string_of_typ ctxt T) | _ => false) in T end; local val dummies = Config.declare_bool ("Proof_Context.dummies", \<^here>) (K false); fun check_dummies ctxt t = if Config.get ctxt dummies then t else Term.no_dummy_patterns t handle TERM _ => error "Illegal dummy pattern(s) in term"; fun prepare_dummies ts = #1 (fold_map Term.replace_dummy_patterns ts 1); in val allow_dummies = Config.put dummies true; fun prepare_patterns ctxt = let val Mode {pattern, ...} = get_mode ctxt in Type_Infer.fixate ctxt pattern #> pattern ? Variable.polymorphic ctxt #> (map o Term.map_types) (prepare_patternT ctxt) #> (if pattern then prepare_dummies else map (check_dummies ctxt)) end; end; (* sort constraints *) local fun prepare_sorts_env ctxt tys = let val tsig = tsig_of ctxt; val defaultS = Type.defaultS tsig; val dummy_var = ("'_dummy_", ~1); fun constraint (xi, raw_S) env = let val (ps, S) = Term_Position.decode_positionS raw_S in if xi = dummy_var orelse S = dummyS then env else Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env handle Vartab.DUP _ => error ("Inconsistent sort constraints for type variable " ^ quote (Term.string_of_vname' xi) ^ Position.here_list ps) end; val env = (fold o fold_atyps) (fn TFree (x, S) => constraint ((x, ~1), S) | TVar v => constraint v | _ => I) tys Vartab.empty; fun get_sort xi raw_S = if xi = dummy_var then Type.minimize_sort tsig (#2 (Term_Position.decode_positionS raw_S)) else (case (Vartab.lookup env xi, Variable.def_sort ctxt xi) of (NONE, NONE) => defaultS | (NONE, SOME S) => S | (SOME S, NONE) => S | (SOME S, SOME S') => if Type.eq_sort tsig (S, S') then S' else error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^ " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^ " for type variable " ^ quote (Term.string_of_vname' xi))); fun add_report S pos reports = if Position.is_reported pos andalso not (AList.defined (op =) reports pos) then (pos, Position.reported_text pos Markup.sorting (Syntax.string_of_sort ctxt S)) :: reports else reports; fun get_sort_reports xi raw_S = let val ps = #1 (Term_Position.decode_positionS raw_S); val S = get_sort xi raw_S handle ERROR msg => error (msg ^ Position.here_list ps); in fold (add_report S) ps end; val reports = (fold o fold_atyps) (fn T => if Term_Position.is_positionT T then I else (case T of TFree (x, raw_S) => get_sort_reports (x, ~1) raw_S | TVar (xi, raw_S) => get_sort_reports xi raw_S | _ => I)) tys []; in (map #2 reports, get_sort) end; fun replace_sortsT get_sort = map_atyps (fn T => if Term_Position.is_positionT T then T else (case T of TFree (x, raw_S) => TFree (x, get_sort (x, ~1) raw_S) | TVar (xi, raw_S) => TVar (xi, get_sort xi raw_S) | _ => T)); in fun prepare_sortsT ctxt tys = let val (sorting_report, get_sort) = prepare_sorts_env ctxt tys in (sorting_report, map (replace_sortsT get_sort) tys) end; fun prepare_sorts ctxt tms = let val tys = rev ((fold o fold_types) cons tms []); val (sorting_report, get_sort) = prepare_sorts_env ctxt tys; in (sorting_report, (map o map_types) (replace_sortsT get_sort) tms) end; fun check_tfree ctxt v = let val (sorting_report, [TFree a]) = prepare_sortsT ctxt [TFree v]; val _ = if Context_Position.reports_enabled ctxt then Output.report sorting_report else (); in a end; end; (* certify terms *) local fun gen_cert prop ctxt t = t |> expand_abbrevs ctxt |> (fn t' => #1 (Sign.certify' prop (Context.Proof ctxt) false (consts_of ctxt) (theory_of ctxt) t') handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg); in val cert_term = gen_cert false; val cert_prop = gen_cert true; end; (* check/uncheck *) fun def_type ctxt = let val Mode {pattern, ...} = get_mode ctxt in Variable.def_type ctxt pattern end; fun standard_typ_check ctxt = map (cert_typ_mode (Type.get_mode ctxt) ctxt #> prepare_patternT ctxt); val standard_term_check_finish = prepare_patterns; fun standard_term_uncheck ctxt = map (contract_abbrevs ctxt); (** export results **) fun common_export is_goal inner outer = map (Assumption.export is_goal inner outer) #> Variable.export inner outer; val goal_export = common_export true; val export = common_export false; fun export_morphism inner outer = Assumption.export_morphism inner outer $> Variable.export_morphism inner outer; fun norm_export_morphism inner outer = export_morphism inner outer $> Morphism.thm_morphism "Proof_Context.norm_export" (Goal.norm_result outer); (** term bindings **) (* auto bindings *) fun auto_bind f props ctxt = fold Variable.maybe_bind_term (f ctxt props) ctxt; val auto_bind_goal = auto_bind Auto_Bind.goal; val auto_bind_facts = auto_bind Auto_Bind.facts; (* match bindings *) fun simult_matches ctxt (t, pats) = (case Seq.pull (Unify.matchers (Context.Proof ctxt) (map (rpair t) pats)) of NONE => error "Pattern match failed!" | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []); fun maybe_bind_term (xi, t) ctxt = ctxt |> Variable.maybe_bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t); val bind_term = maybe_bind_term o apsnd SOME; (* propositions with patterns *) local fun prep_propp prep_props ctxt raw_args = let val props = prep_props ctxt (maps (map fst) raw_args); val props_ctxt = fold Variable.declare_term props ctxt; val patss = maps (map (prep_props (set_mode mode_pattern props_ctxt) o snd)) raw_args; val propps = unflat raw_args (props ~~ patss); val binds = (maps o maps) (simult_matches props_ctxt) propps; in (map (map fst) propps, binds) end; in val cert_propp = prep_propp (map o cert_prop); val read_propp = prep_propp Syntax.read_props; end; (** theorems **) (* fact_tac *) local fun comp_hhf_tac ctxt th i st = PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true} (false, Drule.lift_all ctxt (Thm.cprem_of st i) th, 0) i) st; fun comp_incr_tac _ [] _ = no_tac | comp_incr_tac ctxt (th :: ths) i = (fn st => comp_hhf_tac ctxt (Drule.incr_indexes st th) i st) APPEND comp_incr_tac ctxt ths i; val vacuous_facts = [Drule.termI]; in fun potential_facts ctxt prop = let val body = Term.strip_all_body prop; val vacuous = filter (fn th => Term.could_unify (body, Thm.concl_of th)) vacuous_facts |> map (rpair Position.none); in Facts.could_unify (facts_of ctxt) body @ vacuous end; fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac ctxt facts; fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac ctxt (map #1 (potential_facts ctxt goal)) i); end; (* lookup facts *) fun lookup_fact ctxt name = let val context = Context.Proof ctxt; val thy = Proof_Context.theory_of ctxt; in (case Facts.lookup context (facts_of ctxt) name of NONE => Facts.lookup context (Global_Theory.facts_of thy) name | some => some) end; (* retrieve facts *) val dynamic_facts_dummy = Config.declare_bool ("dynamic_facts_dummy_", \<^here>) (K false); local fun retrieve_global context = Facts.retrieve context (Global_Theory.facts_of (Context.theory_of context)); fun retrieve_generic (context as Context.Proof ctxt) arg = (Facts.retrieve context (facts_of ctxt) arg handle ERROR local_msg => (retrieve_global context arg handle ERROR _ => error local_msg)) | retrieve_generic context arg = retrieve_global context arg; fun retrieve pick context (Facts.Fact s) = let val ctxt = Context.the_proof context; val pos = Syntax.read_input_pos s; val prop = Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s |> singleton (Variable.polymorphic ctxt); fun err ps msg = error (msg ^ Position.here_list (pos :: ps) ^ ":\n" ^ Syntax.string_of_term ctxt prop); val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1); fun prove th = Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th]))); val results = map_filter (try (apfst prove)) (potential_facts ctxt prop'); val (thm, thm_pos) = (case distinct (eq_fst Thm.eq_thm_prop) results of [res] => res | [] => err [] "Failed to retrieve literal fact" | dups => err (distinct (op =) (map #2 dups)) "Ambiguous specification of literal fact"); - val markup = - Markup.entity Markup.literal_factN "" - |> Markup.properties (Position.def_properties_of thm_pos); + val markup = Position.entity_markup Markup.literal_factN ("", thm_pos); val _ = Context_Position.report_generic context pos markup; in pick true ("", thm_pos) [thm] end | retrieve pick context (Facts.Named ((xname, pos), sel)) = let val thy = Context.theory_of context; fun immediate thms = {name = xname, dynamic = false, thms = map (Thm.transfer thy) thms}; val {name, dynamic, thms} = (case xname of "" => immediate [Drule.dummy_thm] | "_" => immediate [Drule.asm_rl] | "nothing" => immediate [] | _ => retrieve_generic context (xname, pos)); val thms' = if dynamic andalso Config.get_generic context dynamic_facts_dummy then [Drule.free_dummy_thm] else Facts.select (Facts.Named ((name, pos), sel)) thms; in pick (dynamic andalso is_none sel) (name, pos) thms' end; in val get_fact_generic = retrieve (fn dynamic => fn (name, _) => fn thms => (if dynamic then SOME name else NONE, thms)); val get_fact = retrieve (K (K I)) o Context.Proof; val get_fact_single = retrieve (K Facts.the_single) o Context.Proof; fun get_thms ctxt = get_fact ctxt o Facts.named; fun get_thm ctxt = get_fact_single ctxt o Facts.named; end; (* inner statement mode *) val inner_stmt = Config.declare_bool ("inner_stmt", \<^here>) (K false); fun is_stmt ctxt = Config.get ctxt inner_stmt; val set_stmt = Config.put inner_stmt; val restore_stmt = set_stmt o is_stmt; (* facts *) fun add_thms_dynamic arg ctxt = ctxt |> map_facts_result (Facts.add_dynamic (Context.Proof ctxt) arg); local fun add_facts {index} arg ctxt = ctxt |> map_facts_result (Facts.add_static (Context.Proof ctxt) {strict = false, index = index} arg); fun update_facts flags (b, SOME ths) ctxt = ctxt |> add_facts flags (b, Lazy.value ths) |> #2 | update_facts _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b)); fun bind_name ctxt b = (full_name ctxt b, Binding.default_pos_of b); in fun add_thms_lazy kind (b, ths) ctxt = let val name_pos = bind_name ctxt b; val ths' = Global_Theory.check_thms_lazy ths |> Lazy.map_finished (Global_Theory.name_thms Global_Theory.unofficial1 name_pos #> map (Thm.kind_rule kind)); val (_, ctxt') = add_facts {index = is_stmt ctxt} (b, ths') ctxt; in ctxt' end; fun note_thms kind ((b, more_atts), facts) ctxt = let val (name, pos) = bind_name ctxt b; val facts' = facts |> Global_Theory.burrow_fact (Global_Theory.name_thms Global_Theory.unofficial1 (name, pos)); fun app (ths, atts) = fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths; val (res, ctxt') = fold_map app facts' ctxt; val thms = Global_Theory.name_thms Global_Theory.unofficial2 (name, pos) (flat res); val (_, ctxt'') = ctxt' |> add_facts {index = is_stmt ctxt} (b, Lazy.value thms); in ((name, thms), ctxt'') end; val note_thmss = fold_map o note_thms; fun put_thms index thms ctxt = ctxt |> map_naming (K Name_Space.local_naming) |> Context_Position.set_visible false |> update_facts {index = index} (apfst Binding.name thms) |> Context_Position.restore_visible ctxt |> restore_naming ctxt; end; fun alias_fact b c ctxt = map_facts (Facts.alias (naming_of ctxt) b c) ctxt; (** basic logical entities **) (* variables *) fun declare_var (x, opt_T, mx) ctxt = let val T = (case opt_T of SOME T => T | NONE => Mixfix.default_constraint mx) in (T, ctxt |> Variable.declare_constraints (Free (x, T))) end; fun add_syntax vars ctxt = map_syntax_idents (Local_Syntax.add_syntax ctxt (map (pair Local_Syntax.Fixed) vars)) ctxt; fun check_var internal b = let val x = Variable.check_name b; val check = if internal then Name.reject_skolem else Name.reject_internal; val _ = if can check (x, []) andalso Symbol_Pos.is_identifier x then () else error ("Bad name: " ^ Binding.print b); in x end; local fun check_mixfix ctxt (b, T, mx) = let val ([x], ctxt') = Variable.add_fixes_binding [Binding.reset_pos b] ctxt; val mx' = Mixfix.reset_pos mx; val _ = add_syntax [(x, T, if Context_Position.reports_enabled ctxt then mx else mx')] ctxt'; in mx' end; fun prep_var prep_typ internal (b, raw_T, mx) ctxt = let val x = check_var internal b; fun cond_tvars T = if internal then T else Type.no_tvars T handle TYPE (msg, _, _) => error msg; val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T; val (T, ctxt') = ctxt |> declare_var (x, opt_T, mx); val mx' = if Mixfix.is_empty mx then mx else check_mixfix ctxt' (b, T, mx); in ((b, SOME T, mx'), ctxt') end; in val read_var = prep_var Syntax.read_typ false; val cert_var = prep_var cert_typ true; end; (* notation *) local fun type_syntax (Type (c, args), mx) = SOME (Local_Syntax.Type, (Lexicon.mark_type c, Mixfix.make_type (length args), mx)) | type_syntax _ = NONE; fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx)) | const_syntax ctxt (Const (c, _), mx) = (case try (Consts.type_scheme (consts_of ctxt)) c of SOME T => SOME (Local_Syntax.Const, (Lexicon.mark_const c, T, mx)) | NONE => NONE) | const_syntax _ _ = NONE; fun gen_notation syntax add mode args ctxt = ctxt |> map_syntax_idents (Local_Syntax.update_modesyntax ctxt add mode (map_filter (syntax ctxt) args)); in val type_notation = gen_notation (K type_syntax); val notation = gen_notation const_syntax; fun generic_type_notation add mode args phi = let val args' = args |> map_filter (fn (T, mx) => let val T' = Morphism.typ phi T; val similar = (case (T, T') of (Type (c, _), Type (c', _)) => c = c' | _ => false); in if similar then SOME (T', mx) else NONE end); in Context.mapping (Sign.type_notation add mode args') (type_notation add mode args') end; fun generic_notation add mode args phi = let val args' = args |> map_filter (fn (t, mx) => let val t' = Morphism.term phi t in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end); in Context.mapping (Sign.notation add mode args') (notation add mode args') end; end; (* aliases *) fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt; fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt; (* local constants *) fun add_const_constraint (c, opt_T) ctxt = let fun prepT raw_T = let val T = cert_typ ctxt raw_T in cert_term ctxt (Const (c, T)); T end; in ctxt |> (map_consts o apfst) (Consts.constrain (c, Option.map prepT opt_T)) end; fun add_abbrev mode (b, raw_t) ctxt = let val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b); val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0]; val ((lhs, rhs), consts') = consts_of ctxt |> Consts.abbreviate (Context.Proof ctxt) (tsig_of ctxt) mode (b, t); in ctxt |> (map_consts o apfst) (K consts') |> Variable.declare_term rhs |> pair (lhs, rhs) end; fun revert_abbrev mode c = (map_consts o apfst) (Consts.revert_abbrev mode c); fun generic_add_abbrev mode arg = Context.mapping_result (Sign.add_abbrev mode arg) (add_abbrev mode arg); fun generic_revert_abbrev mode arg = Context.mapping (Sign.revert_abbrev mode arg) (revert_abbrev mode arg); (* fixes *) local fun gen_fixes prep_var raw_vars ctxt = let val (vars, _) = fold_map prep_var raw_vars ctxt; val (xs, ctxt') = Variable.add_fixes_binding (map #1 vars) ctxt; val _ = Context_Position.reports ctxt' (flat (map2 (fn x => fn pos => [(pos, Variable.markup ctxt' x), (pos, Variable.markup_entity_def ctxt' x)]) xs (map (Binding.pos_of o #1) vars))); val vars' = map2 (fn x => fn (_, opt_T, mx) => (x, opt_T, mx)) xs vars; val (Ts, ctxt'') = fold_map declare_var vars' ctxt'; val vars'' = map2 (fn T => fn (x, _, mx) => (x, T, mx)) Ts vars'; in (xs, add_syntax vars'' ctxt'') end; in val add_fixes = gen_fixes cert_var; val add_fixes_cmd = gen_fixes read_var; end; (** assumptions **) local fun gen_assms prep_propp exp args ctxt = let val (propss, binds) = prep_propp ctxt (map snd args); val props = flat propss; in ctxt |> fold Variable.declare_term props |> tap (Variable.warn_extra_tfrees ctxt) |> fold_burrow (Assumption.add_assms exp o map (Thm.cterm_of ctxt)) propss |-> (fn premss => auto_bind_facts props #> fold Variable.bind_term binds #> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss)) end; in val add_assms = gen_assms cert_propp; val add_assms_cmd = gen_assms read_propp; end; (** cases **) fun dest_cases prev_ctxt ctxt = let val serial_of = #serial oo (Name_Space.the_entry o Name_Space.space_of_table); val ignored = (case prev_ctxt of NONE => Inttab.empty | SOME ctxt0 => let val cases0 = cases_of ctxt0 in Name_Space.fold_table (fn (a, _) => Inttab.insert_set (serial_of cases0 a)) cases0 Inttab.empty end); val cases = cases_of ctxt; in Name_Space.fold_table (fn (a, c) => let val i = serial_of cases a in not (Inttab.defined ignored i) ? cons (i, (a, c)) end) cases [] |> sort (int_ord o apply2 #1) |> map #2 end; local fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b | drop_schematic b = b; fun update_case _ ("", _) cases = cases | update_case _ (name, NONE) cases = Name_Space.del_table name cases | update_case context (name, SOME c) cases = #2 (Name_Space.define context false (Binding.name name, c) cases); fun fix (b, T) ctxt = let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt in (Free (x, T), ctxt') end; in fun update_cases args ctxt = let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming); in map_cases (fold (update_case context) args) ctxt end; fun case_result c ctxt = let val Rule_Cases.Case {fixes, ...} = c; val (ts, ctxt') = ctxt |> fold_map fix fixes; val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c; in ctxt' |> fold (maybe_bind_term o drop_schematic) binds |> update_cases (map (apsnd SOME) cases) |> pair (assumes, (binds, cases)) end; val apply_case = apfst fst oo case_result; fun check_case ctxt internal (name, pos) param_specs = let val (_, Rule_Cases.Case {fixes, assumes, binds, cases}) = Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos); val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) param_specs; fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys | replace [] ys = ys | replace (_ :: _) [] = error ("Too many parameters for case " ^ quote name ^ Position.here pos); val fixes' = replace param_specs fixes; val binds' = map drop_schematic binds; in if null (fold (Term.add_tvarsT o snd) fixes []) andalso null (fold (fold Term.add_vars o snd) assumes []) then Rule_Cases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases} else error ("Illegal schematic variable(s) in case " ^ quote name ^ Position.here pos) end; end; (* structured statements *) type stmt = {vars: ((binding * typ option * mixfix) * (string * term)) list, propss: term list list, binds: (indexname * term) list, result_binds: (indexname * term) list}; type statement = {fixes: (string * term) list, assumes: term list list, shows: term list list, result_binds: (indexname * term option) list, text: term, result_text: term}; local fun export_binds ctxt' ctxt params binds = let val rhss = map (the_list o Option.map (Logic.close_term params) o snd) binds |> burrow (Variable.export_terms ctxt' ctxt) |> map (try the_single); in map fst binds ~~ rhss end; fun prep_stmt prep_var prep_propp raw_vars raw_propps ctxt = let val (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt; val xs = map (Variable.check_name o #1) vars; val (xs', fixes_ctxt) = add_fixes vars vars_ctxt; val (propss, binds) = prep_propp fixes_ctxt raw_propps; val (ps, params_ctxt) = fixes_ctxt |> (fold o fold) Variable.declare_term propss |> fold_map inferred_param xs'; val params = xs ~~ map Free ps; val vars' = map2 (fn (b, _, mx) => fn (_, T) => (b, SOME T, mx)) vars ps; val binds' = binds |> map (apsnd SOME) |> export_binds params_ctxt ctxt params |> map (apsnd the); val _ = Variable.warn_extra_tfrees fixes_ctxt params_ctxt; val result : stmt = {vars = vars' ~~ params, propss = propss, binds = binds, result_binds = binds'}; in (result, params_ctxt) end; fun prep_statement prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt = let val ((fixes, (assumes, shows), binds), ctxt') = ctxt |> prep_stmt prep_var prep_propp raw_fixes (raw_assumes @ raw_shows) |-> (fn {vars, propss, binds, ...} => fold Variable.bind_term binds #> pair (map #2 vars, chop (length raw_assumes) propss, binds)); val binds' = (Auto_Bind.facts ctxt' (flat shows) @ (case try List.last (flat shows) of NONE => [] | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds)) |> export_binds ctxt' ctxt fixes; val text = Logic.close_prop fixes (flat assumes) (Logic.mk_conjunction_list (flat shows)); val text' = singleton (Variable.export_terms ctxt' ctxt) text; val result : statement = {fixes = fixes, assumes = assumes, shows = shows, result_binds = binds', text = text, result_text = text'}; in (result, ctxt') end; in val cert_stmt = prep_stmt cert_var cert_propp; val read_stmt = prep_stmt read_var read_propp; val cert_statement = prep_statement cert_var cert_propp; val read_statement = prep_statement read_var read_propp; end; (** print context information **) (* local syntax *) val print_syntax = Syntax.print_syntax o syn_of; (* abbreviations *) fun pretty_abbrevs verbose show_globals ctxt = let val space = const_space ctxt; val (constants, global_constants) = apply2 (#constants o Consts.dest) (#consts (rep_data ctxt)); val globals = Symtab.make global_constants; fun add_abbr (_, (_, NONE)) = I | add_abbr (c, (T, SOME t)) = if not show_globals andalso Symtab.defined globals c then I else cons (c, Logic.mk_equals (Const (c, T), t)); val abbrevs = Name_Space.markup_entries verbose ctxt space (fold add_abbr constants []); in if null abbrevs then [] else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)] end; fun print_abbrevs verbose = Pretty.writeln_chunks o pretty_abbrevs verbose true; (* term bindings *) fun pretty_term_bindings ctxt = let val binds = Variable.binds_of ctxt; fun prt_bind (xi, (T, t)) = pretty_term_abbrev ctxt (Logic.mk_equals (Var (xi, T), t)); in if Vartab.is_empty binds then [] else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))] end; (* local facts *) fun pretty_local_facts verbose ctxt = let val facts = facts_of ctxt; val props = map #1 (Facts.props facts); val local_facts = (if null props then [] else [("", props)]) @ Facts.dest_static verbose [Global_Theory.facts_of (theory_of ctxt)] facts; in if null local_facts then [] else [Pretty.big_list "local facts:" (map #1 (sort_by (#1 o #2) (map (`(pretty_fact ctxt)) local_facts)))] end; fun print_local_facts verbose ctxt = Pretty.writeln_chunks (pretty_local_facts verbose ctxt); (* named local contexts *) local fun pretty_case (name, (fixes, ((asms, (lets, cs)), ctxt))) = let val prt_name = pretty_name ctxt; val prt_term = Syntax.pretty_term ctxt; fun prt_let (xi, t) = Pretty.block [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1, Pretty.quote (prt_term t)]; fun prt_asm (a, ts) = Pretty.block (Pretty.breaks ((if a = "" then [] else [prt_name a, Pretty.str ":"]) @ map (Pretty.quote o prt_term) ts)); fun prt_sect _ _ _ [] = [] | prt_sect head sep prt xs = [Pretty.block (Pretty.breaks (head :: flat (separate sep (map (single o prt) xs))))]; in Pretty.block (prt_name name :: Pretty.str ":" :: Pretty.fbrk :: Pretty.fbreaks (prt_sect (Pretty.keyword1 "fix") [] (prt_name o Binding.name_of o fst) fixes @ prt_sect (Pretty.keyword1 "let") [Pretty.keyword2 "and"] prt_let (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @ (if forall (null o #2) asms then [] else prt_sect (Pretty.keyword1 "assume") [Pretty.keyword2 "and"] prt_asm asms) @ prt_sect (Pretty.str "subcases:") [] (prt_name o fst) cs)) end; in fun pretty_cases ctxt = let val cases = dest_cases NONE ctxt |> map (fn (name, c as Rule_Cases.Case {fixes, ...}) => (name, (fixes, case_result c ctxt))); in if null cases then [] else [Pretty.big_list "cases:" (map pretty_case cases)] end; end; fun print_cases_proof ctxt0 ctxt = let val print_name = Token.print_name (Thy_Header.get_keywords' ctxt); fun trim_name x = if Name.is_internal x then Name.clean x else "_"; val trim_names = map trim_name #> drop_suffix (equal "_"); fun print_case name xs = (case trim_names xs of [] => print_name name | xs' => enclose "(" ")" (space_implode " " (map print_name (name :: xs')))); fun is_case x t = x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t); fun print_proof (name, Rule_Cases.Case {fixes, binds, ...}) = let val concl = if exists (fn ((x, _), SOME t) => is_case x t | _ => false) binds then Rule_Cases.case_conclN else Auto_Bind.thesisN; in cat_lines [" case " ^ print_case name (map (Binding.name_of o #1) fixes), " then show ?" ^ concl ^ " sorry"] end; in (case map print_proof (dest_cases (SOME ctxt0) ctxt) of [] => "" | proofs => "Proof outline with cases:\n" ^ Active.sendback_markup_command (space_implode "\nnext\n" proofs ^ "\nqed")) end; (* core context *) val debug = Config.declare_bool ("Proof_Context.debug", \<^here>) (K false); val verbose = Config.declare_bool ("Proof_Context.verbose", \<^here>) (K false); fun pretty_ctxt ctxt = if not (Config.get ctxt debug) then [] else let val prt_term = Syntax.pretty_term ctxt; (*structures*) val {structs, ...} = Syntax_Trans.get_idents ctxt; val prt_structs = if null structs then [] else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 :: Pretty.commas (map Pretty.str structs))]; (*fixes*) fun prt_fix (x, x') = if x = x' then Pretty.str x else Pretty.block [Pretty.str x, Pretty.str " =", Pretty.brk 1, prt_term (Syntax.free x')]; val fixes = filter_out ((Name.is_internal orf member (op =) structs) o #1) (Variable.dest_fixes ctxt); val prt_fixes = if null fixes then [] else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 :: Pretty.commas (map prt_fix fixes))]; (*assumptions*) val prt_assms = (case Assumption.all_prems_of ctxt of [] => [] | prems => [Pretty.big_list "assumptions:" [pretty_fact ctxt ("", prems)]]); in prt_structs @ prt_fixes @ prt_assms end; (* main context *) fun pretty_context ctxt = let val verbose = Config.get ctxt verbose; fun verb f x = if verbose then f (x ()) else []; val prt_term = Syntax.pretty_term ctxt; val prt_typ = Syntax.pretty_typ ctxt; val prt_sort = Syntax.pretty_sort ctxt; (*theory*) val pretty_thy = Pretty.block [Pretty.str "theory:", Pretty.brk 1, Context.pretty_thy (theory_of ctxt)]; (*defaults*) fun prt_atom prt prtT (x, X) = Pretty.block [prt x, Pretty.str " ::", Pretty.brk 1, prtT X]; fun prt_var (x, ~1) = prt_term (Syntax.free x) | prt_var xi = prt_term (Syntax.var xi); fun prt_varT (x, ~1) = prt_typ (TFree (x, [])) | prt_varT xi = prt_typ (TVar (xi, [])); val prt_defT = prt_atom prt_var prt_typ; val prt_defS = prt_atom prt_varT prt_sort; val (types, sorts) = Variable.constraints_of ctxt; in verb single (K pretty_thy) @ pretty_ctxt ctxt @ verb (pretty_abbrevs true false) (K ctxt) @ verb pretty_term_bindings (K ctxt) @ verb (pretty_local_facts true) (K ctxt) @ verb pretty_cases (K ctxt) @ verb single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @ verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts))) end; end; val show_abbrevs = Proof_Context.show_abbrevs; diff --git a/src/Pure/ML/ml_compiler.ML b/src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML +++ b/src/Pure/ML/ml_compiler.ML @@ -1,304 +1,301 @@ (* Title: Pure/ML/ml_compiler.ML Author: Makarius Runtime compilation and evaluation. *) signature ML_COMPILER = sig type flags = {environment: string, redirect: bool, verbose: bool, debug: bool option, writeln: string -> unit, warning: string -> unit} val debug_flags: bool option -> flags val flags: flags val verbose: bool -> flags -> flags val eval: flags -> Position.T -> ML_Lex.token list -> unit end; structure ML_Compiler: ML_COMPILER = struct (* flags *) type flags = {environment: string, redirect: bool, verbose: bool, debug: bool option, writeln: string -> unit, warning: string -> unit}; fun debug_flags opt_debug : flags = {environment = "", redirect = false, verbose = false, debug = opt_debug, writeln = writeln, warning = warning}; val flags = debug_flags NONE; fun verbose b (flags: flags) = {environment = #environment flags, redirect = #redirect flags, verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags}; (* parse trees *) fun breakpoint_position loc = let val pos = Position.no_range_position (Exn_Properties.position_of_polyml_location loc) in (case Position.offset_of pos of NONE => pos | SOME 1 => pos | SOME j => Position.properties_of pos |> Properties.put (Markup.offsetN, Value.print_int (j - 1)) |> Position.of_properties) end; fun report_parse_tree redirect depth name_space parse_tree = let val reports_enabled = (case Context.get_generic_context () of SOME context => Context_Position.reports_enabled_generic context | NONE => Context_Position.pide_reports ()); fun is_reported pos = reports_enabled andalso Position.is_reported pos; (* syntax reports *) fun reported_types loc types = let val pos = Exn_Properties.position_of_polyml_location loc in is_reported pos ? let val xml = PolyML.NameSpace.Values.printType (types, depth, SOME name_space) |> Pretty.from_polyml |> Pretty.string_of |> Output.output |> YXML.parse_body; in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end end; fun reported_entity kind loc decl = let val pos = Exn_Properties.position_of_polyml_location loc; val def_pos = Exn_Properties.position_of_polyml_location decl; in (is_reported pos andalso pos <> def_pos) ? - let - fun markup () = - (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos); - in cons (pos, markup, fn () => "") end + cons (pos, fn () => Position.entity_markup kind ("", def_pos), fn () => "") end; fun reported_entity_id def id loc = let val pos = Exn_Properties.position_of_polyml_location loc; in (is_reported pos andalso id <> 0) ? let fun markup () = (Markup.entityN, [(if def then Markup.defN else Markup.refN, Value.print_int id)]); in cons (pos, markup, fn () => "") end end; fun reported_completions loc names = let val pos = Exn_Properties.position_of_polyml_location loc in if is_reported pos andalso not (null names) then let val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names); val xml = Completion.encode completion; in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end else I end; fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ()) | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ()) | reported loc (PolyML.PTdefId id) = reported_entity_id true (FixedInt.toLarge id) loc | reported loc (PolyML.PTrefId id) = reported_entity_id false (FixedInt.toLarge id) loc | reported loc (PolyML.PTtype types) = reported_types loc types | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl | reported loc (PolyML.PTcompletions names) = reported_completions loc names | reported _ _ = I and reported_tree (loc, props) = fold (reported loc) props; val persistent_reports = reported_tree parse_tree []; fun output () = persistent_reports |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ())) |> Output.report; val _ = if not (null persistent_reports) andalso redirect andalso Future.enabled () then Execution.print {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri} output else output (); (* breakpoints *) fun breakpoints _ (PolyML.PTnextSibling tree) = breakpoints_tree (tree ()) | breakpoints _ (PolyML.PTfirstChild tree) = breakpoints_tree (tree ()) | breakpoints loc (PolyML.PTbreakPoint b) = let val pos = breakpoint_position loc in if is_reported pos then let val id = serial (); in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end else I end | breakpoints _ _ = I and breakpoints_tree (loc, props) = fold (breakpoints loc) props; val all_breakpoints = rev (breakpoints_tree parse_tree []); val _ = Position.reports (map #1 all_breakpoints); in map (fn (_, (id, (b, pos))) => (id, (b, Position.dest pos))) all_breakpoints end; (* eval ML source tokens *) fun eval (flags: flags) pos toks = let val opt_context = Context.get_generic_context (); val env as {debug, name_space, add_breakpoints} = (case (ML_Recursive.get (), #environment flags <> "") of (SOME env, false) => env | _ => {debug = (case #debug flags of SOME debug => debug | NONE => ML_Options.debugger_enabled opt_context), name_space = ML_Env.make_name_space (#environment flags), add_breakpoints = ML_Env.add_breakpoints}); (* input *) val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos))); val {explode_token, ...} = ML_Env.operations opt_context (#environment flags); fun token_content tok = if ML_Lex.is_comment tok then NONE else SOME (`explode_token tok); val input_buffer = Unsynchronized.ref (map_filter token_content toks); fun get () = (case ! input_buffer of (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c) | ([], _) :: rest => (input_buffer := rest; SOME #" ") | [] => NONE); fun get_pos () = (case ! input_buffer of (_ :: _, tok) :: _ => ML_Lex.pos_of tok | ([], tok) :: _ => ML_Lex.end_pos_of tok | [] => Position.none); (* output *) val writeln_buffer = Unsynchronized.ref Buffer.empty; fun write s = Unsynchronized.change writeln_buffer (Buffer.add s); fun output_writeln () = #writeln flags (trim_line (Buffer.content (! writeln_buffer))); val warnings = Unsynchronized.ref ([]: string list); fun warn msg = Unsynchronized.change warnings (cons msg); fun output_warnings () = List.app (#warning flags) (rev (! warnings)); val error_buffer = Unsynchronized.ref Buffer.empty; fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n"); fun flush_error () = #writeln flags (trim_line (Buffer.content (! error_buffer))); fun raise_error msg = error (trim_line (Buffer.content (Buffer.add msg (! error_buffer)))); fun message {message = msg, hard, location = loc, context = _} = let val pos = Exn_Properties.position_of_polyml_location loc; val txt = (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^ Pretty.string_of (Pretty.from_polyml msg); in if hard then err txt else warn txt end; (* results *) val depth = FixedInt.fromInt (ML_Print_Depth.get_print_depth ()); fun apply_result {fixes, types, signatures, structures, functors, values} = let fun display disp x = if depth > 0 then (write (disp x |> Pretty.from_polyml |> Pretty.string_of); write "\n") else (); fun apply_fix (a, b) = (#enterFix name_space (a, b); display PolyML.NameSpace.Infixes.print b); fun apply_type (a, b) = (#enterType name_space (a, b); display PolyML.NameSpace.TypeConstrs.print (b, depth, SOME name_space)); fun apply_sig (a, b) = (#enterSig name_space (a, b); display PolyML.NameSpace.Signatures.print (b, depth, SOME name_space)); fun apply_struct (a, b) = (#enterStruct name_space (a, b); display PolyML.NameSpace.Structures.print (b, depth, SOME name_space)); fun apply_funct (a, b) = (#enterFunct name_space (a, b); display PolyML.NameSpace.Functors.print (b, depth, SOME name_space)); fun apply_val (a, b) = (#enterVal name_space (a, b); display PolyML.NameSpace.Values.printWithType (b, depth, SOME name_space)); in List.app apply_fix fixes; List.app apply_type types; List.app apply_sig signatures; List.app apply_struct structures; List.app apply_funct functors; List.app apply_val values end; exception STATIC_ERRORS of unit; fun result_fun (phase1, phase2) () = ((case phase1 of NONE => () | SOME parse_tree => add_breakpoints (report_parse_tree (#redirect flags) depth name_space parse_tree)); (case phase2 of NONE => raise STATIC_ERRORS () | SOME code => apply_result ((code |> Runtime.debugging opt_context |> Runtime.toplevel_error (err o Runtime.exn_message)) ()))); (* compiler invocation *) val parameters = [PolyML.Compiler.CPOutStream write, PolyML.Compiler.CPNameSpace name_space, PolyML.Compiler.CPErrorMessageProc message, PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos), PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos), PolyML.Compiler.CPFileName location_props, PolyML.Compiler.CPPrintDepth ML_Print_Depth.get_print_depth, PolyML.Compiler.CPCompilerResultFun result_fun, PolyML.Compiler.CPPrintInAlphabeticalOrder false, PolyML.Compiler.CPDebug debug, PolyML.Compiler.CPBindingSeq serial]; val _ = (while not (List.null (! input_buffer)) do ML_Recursive.recursive env (fn () => PolyML.compiler (get, parameters) ())) handle exn => if Exn.is_interrupt exn then Exn.reraise exn else let val exn_msg = (case exn of STATIC_ERRORS () => "" | Runtime.TOPLEVEL_ERROR => "" | _ => "Exception- " ^ Pretty.string_of (Runtime.pretty_exn exn) ^ " raised"); val _ = output_warnings (); val _ = output_writeln (); in raise_error exn_msg end; in if #verbose flags then (output_warnings (); flush_error (); output_writeln ()) else () end; end;