1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory ML_Goal
8imports Main
9keywords "ML_goal" :: thy_goal_stmt
10begin
11
12\<comment>\<open>
13  Defines a new command `ML_goal`. `ML_goal` is similar to @{command lemma}
14  and @{command theorem} in that it specifies a goal and enters a proof state
15  for you prove that goal.
16
17  However, instead of parsing goal terms from user input, `ML_goal` uses
18  an ML block to produce a list of ML terms, and then sets up the proof state
19  to prove those terms as goals.
20
21  Each goal term must be an instance of either @{typ bool} or @{typ prop}.
22
23  There are some concrete examples in @{file ML_Goal_Test.thy}.
24\<close>
25
26ML \<open>
27
28structure ML_goal_data = Proof_Data(
29  type T = term list
30  val init = K []
31);
32
33local
34
35\<comment>\<open>
36  Why are we stashing something into a `Proof_Data` and then immediately
37  taking it out again?
38
39  In @{ML "fn (pos, source, ctxt: Context.generic) =>
40      ML_Context.expression pos source ctxt"},
41  `source` is a fragment of ML code which gets evaluated in the ML context
42  associated with `ctxt`, which in this case should be the proof context
43  associated with the call to `ML_goal`. The result is a new generic context
44  with a new ML context, updated with the effects of evaluating `source`.
45
46  This means the only way to extract information out of `source` is via
47  its side-effects on the ML context. We have two main options:
48
49  - Declare an @{ML "Unsynchronized.ref"} in this file (ML_Goal), and stash
50    the value described by `source` into that.
51    - This is unlikely to play well with deferred or concurrent proofs.
52
53  - Use an instance of `Proof_Data` to declare some new state that's
54    associated with all proof contexts (in this case "the result of
55    the ML block passed to `ML_goal`"), and evaluate `source` in such a way
56    as to store the result there.
57    - This has more overhead compared to the `ref` solution, but it's
58      still negligible.
59    - This is the 'preferred' way to store 'local state' in contexts.
60    - This is safe for deferred or concurrent proofs.
61\<close>
62fun evaluate_goals source =
63    ML_Context.expression
64      (Input.pos_of source)
65      (ML_Lex.read "Theory.local_setup (ML_goal_data.put (("
66        @ ML_Lex.read_source source
67        @ ML_Lex.read "): term list))")
68    |> Context.proof_map
69    #> ML_goal_data.get;
70
71fun err_msg_bad_type goal (typ: typ) ctxt =
72    "The goal " ^ (@{make_string} (Syntax.pretty_term ctxt goal)) ^ " " ^
73    "has unsupported type " ^ (@{make_string} typ) ^ ". " ^
74    "The ML_goal command expects either a " ^ (@{make_string} @{typ bool}) ^ " " ^
75    "or a " ^ (@{make_string} @{typ prop}) ^ ".";
76
77fun begin_proof ((name, attrs): Attrib.binding, ml_block: Input.source) ctxt =
78    let
79      \<comment>\<open>
80        In the very common case that a goal is a @{typ bool}, we wrap
81        it in @{term Trueprop} to keep the Proof.theorem command happy.
82      \<close>
83      fun prop_wrap goal =
84          case Term.type_of goal of
85            @{typ bool} => goal |> HOLogic.mk_Trueprop
86          | @{typ prop} => goal
87          | other => error (err_msg_bad_type goal other ctxt);
88
89      val goals =
90          evaluate_goals ml_block ctxt
91          |> List.map prop_wrap
92
93          \<comment>\<open> Ensures free variables are type-consistent. \<close>
94          |> Syntax.check_props ctxt
95          |> List.map (rpair []);
96
97      \<comment>\<open>
98        Figures out that the `folded` in `[folded foo]` means
99        @{attribute folded}. Required for attributes to work.
100      \<close>
101      val parsed_attrs = map (Attrib.check_src ctxt) attrs;
102      val binding = (name, parsed_attrs);
103
104      val start_pos = Position.thread_data ();
105
106      fun after_qed (results: thm list list) ctxt =
107          let
108            val thms = results |> hd;
109            val ((res_name, res), ctxt') =
110                Local_Theory.note (binding, thms) ctxt;
111            val _ =
112                Proof_Display.print_results true start_pos ctxt'
113                  (("theorem", res_name), [("", res)])
114          in ctxt' end
115    in
116      Proof.theorem NONE
117        after_qed
118        [goals] ctxt
119    end;
120
121val ML_goal_cmd =
122    Scan.optional (Parse_Spec.opt_thm_name ":") Binding.empty_atts
123    -- Parse.ML_source
124    >> begin_proof
125
126val _  =
127    Outer_Syntax.local_theory_to_proof
128      \<^command_keyword>\<open>ML_goal\<close>
129      "ML-provided goal"
130      ML_goal_cmd;
131
132in end
133\<close>
134
135end