Quelle ml_thms.ML Sprache: SML

(*  Title:      Pure/ML/ml_thms.ML
    Author:     Makarius

Attribute source and theorem values within ML.
*)

signature ML_THMS =
sig
  val the_attributes: Proof.context -> int -> Token.src list
  val the_thmss: Proof.context -> thm list list
  val thm_binding: string -> bool -> thm list -> Proof.context ->
    (Proof.context -> string * string) * Proof.context
  val embedded_lemma: (Proof.context -> thm list * (term list * Proof.context)) parser
  val get_stored_thms: unit -> thm list
  val get_stored_thm: unit -> thm
  val store_thms: string * thm list -> unit
  val store_thm: string * thm -> unit
  val bind_thm: string * thm -> unit
  val bind_thms: string * thm list -> unit
end;

structure ML_Thms: ML_THMS =
struct

(* auxiliary data *)

type thms = (string * bool) * thm list;  (*name, single, value*)

structure Data = Proof_Data
(
  type T = Token.src list Inttab.table * thms list;
  fun init _ = (Inttab.empty, []);
);

val put_attributes = Data.map o apfst o Inttab.update;
fun the_attributes ctxt name = the (Inttab.lookup (fst (Data.get ctxt)) name);

val get_thmss = snd o Data.get;
val the_thmss = map snd o get_thmss;
val cons_thms = Data.map o apsnd o cons;

(* attribute source *)

val _ = Theory.setup
  (ML_Antiquotation.declaration \<^binding>\<open>attributes\<close> Attrib.attribs
    (fn _ => fn srcs => fn ctxt =>
      let val i = serial () in
        ctxt
        |> put_attributes (i, srcs)
        |> ML_Antiquotation.value_decl "attributes"
            ("ML_Thms.the_attributes ML_context " ^ string_of_int i)
      end));

(* fact references *)

fun thm_binding kind is_single thms ctxt =
  let
    val initial = null (get_thmss ctxt);
    val (name, ctxt') = ML_Context.variant kind ctxt;
    val ctxt'' = cons_thms ((name, is_single), thms) ctxt';

    val ml_body = ML_Context.struct_name ctxt ^ "." ^ name;
    fun decl final_ctxt =
      if initial then
        let
          val binds = get_thmss final_ctxt |> map (fn ((a, b), _) => (b ? enclose "[" "]") a);
          val ml_env = "val [" ^ commas binds ^ "] = ML_Thms.the_thmss ML_context;\n";
        in (ml_env, ml_body) end
      else ("", ml_body);
  in (decl, ctxt'') end;

val _ = Theory.setup
  (ML_Antiquotation.declaration \<^binding>\<open>thm\<close> (Attrib.thm >> single) (K (thm_binding "thm" true)) #>
   ML_Antiquotation.declaration \<^binding>\<open>thms\<close> Attrib.thms (K (thm_binding "thms" false)));

(* embedded lemma *)

val embedded_lemma =
  Args.mode "open" -- Parse.and_list1 (Scan.repeat1 Parse.embedded_inner_syntax)
    -- Parse.for_fixes -- Method.parse_by
    >> (fn (((is_open, raw_stmt), fixes), (methods, reports)) => fn ctxt =>
        let
          val _ = Context_Position.reports ctxt reports;

          val fixes_ctxt = #2 (Proof_Context.add_fixes_cmd fixes ctxt);
          val stmt = burrow (map (rpair []) o Syntax.read_props fixes_ctxt) raw_stmt;
          val stmt_ctxt = (fold o fold) (Proof_Context.augment o #1) stmt fixes_ctxt;

          val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation \<^here>;
          fun after_qed res goal_ctxt =
            Proof_Context.put_thms false (Auto_Bind.thisN,
              SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;

          val thms_ctxt = stmt_ctxt
            |> Proof.theorem NONE after_qed stmt
            |> Proof.global_terminal_proof methods;
          val thms =
            Proof_Context.get_fact thms_ctxt
              (Facts.named (Proof_Context.full_name thms_ctxt (Binding.name Auto_Bind.thisN)))
        in (thms, (map #1 (flat stmt), stmt_ctxt)) end);

val _ = Theory.setup
  (ML_Antiquotation.declaration \<^binding>\<open>lemma\<close> (Scan.lift embedded_lemma)
    (fn _ => fn make_lemma => fn ctxt =>
      let val thms = #1 (make_lemma ctxt)
      in thm_binding "lemma" (length thms = 1) thms ctxt end));

(* old-style theorem bindings *)

structure Data = Theory_Data
(
  type T = thm list;
  val empty = [];
  val merge = #1;
);

fun get_stored_thms () = Data.get (Context.the_global_context ());
val get_stored_thm = hd o get_stored_thms;

fun ml_store get (name, ths) =
  let
    val (_, ths') =
      Theory.setup_result (Global_Theory.note_thms "" ((Binding.name name, []), [(ths, [])]));
    val _ = Theory.setup (Data.put ths');
    val _ =
      if name = "" then ()
      else if not (ML_Syntax.is_identifier name) then
        error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
      else
        ML_Compiler.eval (ML_Compiler.verbose true ML_Compiler.flags) Position.none
          (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
    val _ = Theory.setup (Data.put []);
  in () end;

val store_thms = ml_store "ML_Thms.get_stored_thms";
fun store_thm (name, th) = ml_store "ML_Thms.get_stored_thm" (name, [th]);

fun bind_thm (name, thm) = store_thm (name, Drule.export_without_context thm);
fun bind_thms (name, thms) = store_thms (name, map Drule.export_without_context thms);

end;

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

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.