Quelle method.ML Sprache: SML

(*  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 method_space: Context.generic -> Name_Space.T
  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 parse_by: ((text_range * text_range option) * Position.report list) 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 [Thm.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>\<open>rule_trace\<close> (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 Markup.methodN, ml_tactic = NONE, facts = NONE};
  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))};

val method_space = Name_Space.space_of_table o get_methods;

(* ML tactic *)

fun set_tactic ml_tactic = map_data (fn (methods, _, facts) => (methods, SOME ml_tactic, facts));

fun the_tactic context =
  #ml_tactic (Data.get context)
  |> \<^if_none>\<open>raise Fail "Undefined ML tactic"\<close>;

val parse_tactic =
  Scan.state :|-- (fn context =>
    Scan.lift (Args.embedded_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
        Morphism.entity (fn phi =>
          set_tactic (fn _ => Context.setmp_generic_context (SOME context) (tac phi)))
      end)) >> (fn decl => Morphism.form_entity (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.chunks |> Pretty.writeln
  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;

val _ = Theory.setup
(ML_Antiquotation.inline_embedded \<^binding>\<open>method\<close>
    (Args.context -- Scan.lift Parse.embedded_position >>
      (ML_Syntax.print_string o uncurry check_name)));

(* 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 pos (K attribute)]),
                      Attrib.trim_context_thms bs));

                val decl =
                  Morphism.entity (fn phi => fn context =>
                    let val psi = Morphism.set_context'' context phi in
                      context
                      |> Context.mapping I init
                      |> Attrib.generic_notes "" (Attrib.transform_facts psi facts)
                      |> snd
                    end);

                val modifier_report =
                  (#1 (Token.range_of modifier_toks),
                    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.reports_enabled0 ()
  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;

val parse_by =
  Parse.$$$ "by" |-- parse -- Scan.option parse
    >> (fn (m1, m2) => ((m1, m2), maps reports_of (m1 :: the_list m2)));

(* 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 =
  let val keywords = Keyword.no_major_keywords (Thy_Header.get_keywords' ctxt)
  in Parse.read_embedded ctxt keywords (Scan.many Token.not_eof) #> read_closure ctxt end;

val text_closure =
  Args.context -- Scan.lift (Parse.token Parse.embedded) >> (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>\<open>fail\<close> (Scan.succeed (K fail)) "force failure" #>
  setup \<^binding>\<open>succeed\<close> (Scan.succeed (K succeed)) "succeed" #>
  setup \<^binding>\<open>sleep\<close> (Scan.lift Parse.real >> (fn s => fn _ => fn _ => sleep (seconds s)))
    "succeed after delay (in seconds)" #>
  setup \<^binding>\<open>-\<close> (Scan.succeed (K (SIMPLE_METHOD all_tac)))
    "insert current facts, nothing else" #>
  setup \<^binding>\<open>goal_cases\<close> (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>\<open>subproofs\<close> (text_closure >> (Context_Tactic.SUBPROOFS ooo evaluate_runtime))
    "apply proof method to subproofs with closed derivation" #>
  setup \<^binding>\<open>insert\<close> (Attrib.thms >> (K o insert))
    "insert theorems, ignoring facts" #>
  setup \<^binding>\<open>intro\<close> (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths))
    "repeatedly apply introduction rules" #>
  setup \<^binding>\<open>elim\<close> (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths))
    "repeatedly apply elimination rules" #>
  setup \<^binding>\<open>unfold\<close> (Attrib.thms >> unfold_meth) "unfold definitions" #>
  setup \<^binding>\<open>fold\<close> (Attrib.thms >> fold_meth) "fold definitions" #>
  setup \<^binding>\<open>atomize\<close> (Scan.lift (Args.mode "full") >> atomize)
    "present local premises as object-level statements" #>
  setup \<^binding>\<open>rule\<close> (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths))
    "apply some intro/elim rule" #>
  setup \<^binding>\<open>erule\<close> (xrule_meth erule) "apply rule in elimination manner (improper)" #>
  setup \<^binding>\<open>drule\<close> (xrule_meth drule) "apply rule in destruct manner (improper)" #>
  setup \<^binding>\<open>frule\<close> (xrule_meth frule) "apply rule in forward manner (improper)" #>
  setup \<^binding>\<open>this\<close> (Scan.succeed this) "apply current facts as rules" #>
  setup \<^binding>\<open>fact\<close> (Attrib.thms >> fact) "composition by facts from context" #>
  setup \<^binding>\<open>assumption\<close> (Scan.succeed assumption)
    "proof by assumption, preferring facts" #>
  setup \<^binding>\<open>rename_tac\<close> (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>\<open>rotate_tac\<close> (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>\<open>tactic\<close> (parse_tactic >> (K o METHOD))
    "ML tactic as proof method" #>
  setup \<^binding>\<open>raw_tactic\<close> (parse_tactic >> (fn tac => fn _ => Context_Tactic.CONTEXT_TACTIC o tac))
    "ML tactic as raw proof method" #>
  setup \<^binding>\<open>use\<close>
    (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'';

quality97%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Normalansicht

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.