src/Pure/ML/ml_thms.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 66067 cdbcb417db67
child 67147 dea94b1aabc3
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      Pure/ML/ml_thms.ML
     2     Author:     Makarius
     3 
     4 Attribute source and theorem values within ML.
     5 *)
     6 
     7 signature ML_THMS =
     8 sig
     9   val the_attributes: Proof.context -> int -> Token.src list
    10   val the_thmss: Proof.context -> thm list list
    11   val get_stored_thms: unit -> thm list
    12   val get_stored_thm: unit -> thm
    13   val store_thms: string * thm list -> unit
    14   val store_thm: string * thm -> unit
    15   val bind_thm: string * thm -> unit
    16   val bind_thms: string * thm list -> unit
    17 end;
    18 
    19 structure ML_Thms: ML_THMS =
    20 struct
    21 
    22 (* auxiliary data *)
    23 
    24 type thms = (string * bool) * thm list;  (*name, single, value*)
    25 
    26 structure Data = Proof_Data
    27 (
    28   type T = Token.src list Inttab.table * thms list;
    29   fun init _ = (Inttab.empty, []);
    30 );
    31 
    32 val put_attributes = Data.map o apfst o Inttab.update;
    33 fun the_attributes ctxt name = the (Inttab.lookup (fst (Data.get ctxt)) name);
    34 
    35 val get_thmss = snd o Data.get;
    36 val the_thmss = map snd o get_thmss;
    37 val cons_thms = Data.map o apsnd o cons;
    38 
    39 
    40 (* attribute source *)
    41 
    42 val _ = Theory.setup
    43   (ML_Antiquotation.declaration @{binding attributes} Attrib.attribs
    44     (fn _ => fn srcs => fn ctxt =>
    45       let val i = serial () in
    46         ctxt
    47         |> put_attributes (i, srcs)
    48         |> ML_Context.value_decl "attributes"
    49             ("ML_Thms.the_attributes ML_context " ^ string_of_int i)
    50       end));
    51 
    52 
    53 (* fact references *)
    54 
    55 fun thm_binding kind is_single thms ctxt =
    56   let
    57     val initial = null (get_thmss ctxt);
    58     val (name, ctxt') = ML_Context.variant kind ctxt;
    59     val ctxt'' = cons_thms ((name, is_single), thms) ctxt';
    60 
    61     val ml_body = ML_Context.struct_name ctxt ^ "." ^ name;
    62     fun decl final_ctxt =
    63       if initial then
    64         let
    65           val binds = get_thmss final_ctxt |> map (fn ((a, b), _) => (b ? enclose "[" "]") a);
    66           val ml_env = "val [" ^ commas binds ^ "] = ML_Thms.the_thmss ML_context;\n";
    67         in (ml_env, ml_body) end
    68       else ("", ml_body);
    69   in (decl, ctxt'') end;
    70 
    71 val _ = Theory.setup
    72   (ML_Antiquotation.declaration @{binding thm} (Attrib.thm >> single) (K (thm_binding "thm" true)) #>
    73    ML_Antiquotation.declaration @{binding thms} Attrib.thms (K (thm_binding "thms" false)));
    74 
    75 
    76 (* ad-hoc goals *)
    77 
    78 val and_ = Args.$$$ "and";
    79 val by = Parse.reserved "by";
    80 val goal = Scan.unless (by || and_) Args.embedded_inner_syntax;
    81 
    82 val _ = Theory.setup
    83   (ML_Antiquotation.declaration @{binding lemma}
    84     (Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) --
    85       (Parse.position by -- Method.parse -- Scan.option Method.parse)))
    86     (fn _ => fn ((is_open, raw_propss), (((_, by_pos), m1), m2)) => fn ctxt =>
    87       let
    88         val reports =
    89           (by_pos, Markup.keyword1 |> Markup.keyword_properties) ::
    90             maps Method.reports_of (m1 :: the_list m2);
    91         val _ = Context_Position.reports ctxt reports;
    92 
    93         val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
    94         val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation;
    95         fun after_qed res goal_ctxt =
    96           Proof_Context.put_thms false (Auto_Bind.thisN,
    97             SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
    98 
    99         val ctxt' = ctxt
   100           |> Proof.theorem NONE after_qed propss
   101           |> Proof.global_terminal_proof (m1, m2);
   102         val thms =
   103           Proof_Context.get_fact ctxt'
   104             (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
   105       in thm_binding "lemma" (length (flat propss) = 1) thms ctxt end));
   106 
   107 
   108 (* old-style theorem bindings *)
   109 
   110 structure Stored_Thms = Theory_Data
   111 (
   112   type T = thm list;
   113   val empty = [];
   114   fun extend _ = [];
   115   fun merge _ = [];
   116 );
   117 
   118 fun get_stored_thms () = Stored_Thms.get (Context.the_global_context ());
   119 val get_stored_thm = hd o get_stored_thms;
   120 
   121 fun ml_store get (name, ths) =
   122   let
   123     val ths' = Context.>>> (Context.map_theory_result
   124       (Global_Theory.store_thms (Binding.name name, ths)));
   125     val _ = Theory.setup (Stored_Thms.put ths');
   126     val _ =
   127       if name = "" then ()
   128       else if not (ML_Syntax.is_identifier name) then
   129         error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
   130       else
   131         ML_Compiler.eval (ML_Compiler.verbose true ML_Compiler.flags) Position.none
   132           (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
   133     val _ = Theory.setup (Stored_Thms.put []);
   134   in () end;
   135 
   136 val store_thms = ml_store "ML_Thms.get_stored_thms";
   137 fun store_thm (name, th) = ml_store "ML_Thms.get_stored_thm" (name, [th]);
   138 
   139 fun bind_thm (name, thm) = store_thm (name, Drule.export_without_context thm);
   140 fun bind_thms (name, thms) = store_thms (name, map Drule.export_without_context thms);
   141 
   142 end;