1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Trace_Schematic_Insts
8imports
9  Main
10  MLUtils
11  TermPatternAntiquote
12begin
13
14text \<open>
15  See Trace_Schematic_Insts_Test for tests and examples.
16\<close>
17
18locale data_stash
19begin
20
21text \<open>
22  We use this to stash a list of the schematics in the conclusion of the proof
23  state. After running a method, we can read off the schematic instantiations
24  (if any) from this list, then restore the original conclusion. Schematic
25  types are added as "undefined :: ?'a" (for now, we don't worry about types
26  that don't have sort "type").
27
28  TODO: there ought to be some standard way of stashing things into the proof
29  state. Find out what that is and refactor
30\<close>
31definition container :: "'a \<Rightarrow> bool \<Rightarrow> bool"
32  where
33  "container a b \<equiv> True"
34
35lemma proof_state_add:
36  "Pure.prop PROP P \<equiv> PROP Pure.prop (container True xs \<Longrightarrow> PROP P)"
37  by (simp add: container_def)
38
39lemma proof_state_remove:
40  "PROP Pure.prop (container True xs \<Longrightarrow> PROP P) \<equiv> Pure.prop (PROP P)"
41  by (simp add: container_def)
42
43lemma rule_add:
44  "PROP P \<equiv> (container True xs \<Longrightarrow> PROP P)"
45  by (simp add: container_def)
46
47lemma rule_remove:
48  "(container True xs \<Longrightarrow> PROP P) \<equiv> PROP P"
49  by (simp add: container_def)
50
51lemma elim:
52  "container a b"
53  by (simp add: container_def)
54
55ML \<open>
56signature TRACE_SCHEMATIC_INSTS = sig
57  type instantiations = {
58    bounds: (string * typ) list,
59    terms: (term * term) list,
60    typs: (typ * typ) list
61  }
62  val empty_instantiations: instantiations
63
64  val trace_schematic_insts:
65        Method.method -> (instantiations -> unit) -> Method.method
66  val default_report:
67        Proof.context -> string -> instantiations -> unit
68
69  val trace_schematic_insts_tac:
70        Proof.context ->
71        (instantiations -> instantiations -> unit) ->
72        (thm -> int -> tactic) ->
73        thm -> int -> tactic
74  val default_rule_report:
75        Proof.context -> string -> instantiations -> instantiations -> unit
76
77  val skip_dummy_state: Method.method -> Method.method
78  val make_term_container: term list -> term
79  val dest_term_container: term -> term list
80
81  val attach_proof_annotations: Proof.context -> term list -> thm -> thm
82  val detach_proof_annotations: thm -> term list * thm
83
84  val attach_rule_annotations: Proof.context -> term list -> thm -> thm
85  val detach_rule_result_annotations:
86        Proof.context -> thm -> ((string * typ) list * term list) * thm
87
88  val instantiate_thm: Proof.context -> thm -> instantiations -> term
89end
90
91structure Trace_Schematic_Insts: TRACE_SCHEMATIC_INSTS = struct
92
93\<comment>\<open>
94  Each pair in the terms and typs fields are a (schematic, instantiation) pair.
95
96  The bounds field records the binders which are due to subgoal bounds.
97
98  An explanation: if we instantiate some schematic `?P` within a subgoal like
99  @{term "\<And>x y. Q"}, it might be instantiated to @{term "\<lambda>a. R a
100  x"}.  We need to capture `x` when reporting the instantiation, so we report
101  that `?P` has been instantiated to @{term "\<lambda>x y a. R a x"}. In order
102  to distinguish between the bound `x`, `y`, and `a`, we record the bound
103  variables from the subgoal so that we can handle them as necessary.
104
105  As an example, let us consider the case where the subgoal is
106  @{term "\<And>x::int. foo (\<lambda>a. a::'e) (\<lambda>a. a + x) (0::nat)"}
107  and the rule being applied is
108  @{term "foo ((f::'d \<Rightarrow> 'a \<Rightarrow> 'a) y) (g::'b \<Rightarrow> 'b) (0::'c::zero)"}.
109  This results in the instantiations
110  {bounds: [("x", int)],
111   terms: [(?f, \<lambda>x a b. b), (?g, \<lambda>x a. x + a), (?y, \<lambda>x. ?y x)],
112   typs: [(?'a, 'e), (?'b, int), (?'c, nat)]}.
113\<close>
114type instantiations = {
115  bounds: (string * typ) list,
116  terms: (term * term) list,
117  typs: (typ * typ) list
118}
119
120val empty_instantiations = {bounds = [], terms = [], typs = []}
121
122\<comment>\<open>
123  Work around Isabelle running every apply method on a dummy proof state
124\<close>
125fun skip_dummy_state method =
126  fn facts => fn (ctxt, st) =>
127    case Thm.prop_of st of
128        Const (@{const_name Pure.prop}, _) $
129          (Const (@{const_name Pure.term}, _) $ Const (@{const_name Pure.dummy_pattern}, _)) =>
130          Seq.succeed (Seq.Result (ctxt, st))
131      | _ => method facts (ctxt, st);
132
133\<comment>\<open>
134  Utils
135\<close>
136fun rewrite_state_concl eqn st =
137  Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of st) (K eqn)) st
138
139\<comment>\<open>
140  Strip the @{term Pure.prop} that wraps proof state conclusions
141\<close>
142fun strip_prop ct =
143      case Thm.term_of ct of
144        Const (@{const_name "Pure.prop"}, @{typ "prop \<Rightarrow> prop"}) $ _ => Thm.dest_arg ct
145      | _ => raise CTERM ("strip_prop: head is not Pure.prop", [ct])
146
147fun cconcl_of st =
148  funpow (Thm.nprems_of st) Thm.dest_arg (Thm.cprop_of st)
149  |> strip_prop
150
151fun vars_of_term t =
152  Term.add_vars t []
153  |> sort_distinct Term_Ord.var_ord
154
155fun type_vars_of_term t =
156  Term.add_tvars t []
157  |> sort_distinct Term_Ord.tvar_ord
158
159\<comment>\<open>
160  Create annotation list
161\<close>
162fun make_term_container ts =
163      fold (fn t => fn container =>
164              Const (@{const_name container},
165                    fastype_of t --> @{typ "bool \<Rightarrow> bool"}) $
166                t $ container)
167        (rev ts) @{term "True"}
168
169\<comment>\<open>
170  Retrieve annotation list
171\<close>
172fun dest_term_container
173      (Const (@{const_name container}, _) $ x $ list) =
174          x :: dest_term_container list
175  | dest_term_container _ = []
176
177\<comment>\<open>
178  Attach some terms to a proof state, by "hiding" them in the protected goal.
179\<close>
180fun attach_proof_annotations ctxt terms st =
181  let
182    val container = make_term_container terms
183    (* FIXME: this might affect st's maxidx *)
184    val add_eqn =
185          Thm.instantiate
186            ([],
187             [((("P", 0), @{typ prop}), cconcl_of st),
188              ((("xs", 0), @{typ bool}), Thm.cterm_of ctxt container)])
189            @{thm proof_state_add}
190  in
191    rewrite_state_concl add_eqn st
192  end
193
194\<comment>\<open>
195  Retrieve attached terms from a proof state
196\<close>
197fun detach_proof_annotations st =
198  let
199    val st_concl = cconcl_of st
200    val (ccontainer', real_concl) = Thm.dest_implies st_concl
201    val ccontainer =
202          ccontainer'
203          |> Thm.dest_arg (* strip Trueprop *)
204          |> Thm.dest_arg \<comment>\<open>strip outer @{term "container True"}\<close>
205    val terms =
206          ccontainer
207          |> Thm.term_of
208          |> dest_term_container
209    val remove_eqn =
210          Thm.instantiate
211            ([],
212             [((("P", 0), @{typ prop}), real_concl),
213              ((("xs", 0), @{typ bool}), ccontainer)])
214            @{thm proof_state_remove}
215  in
216    (terms, rewrite_state_concl remove_eqn st)
217  end
218
219\<comment> \<open>
220  Attaches the given terms to the given thm by stashing them as a new @{term
221  "container"} premise, *after* all the existing premises (this minimises
222  disruption when the rule is used with things like `erule`).
223\<close>
224fun attach_rule_annotations ctxt terms thm =
225  let
226    val container = make_term_container terms
227    (* FIXME: this might affect thm's maxidx *)
228    val add_eqn =
229          Thm.instantiate
230            ([],
231             [((("P", 0), @{typ prop}), Thm.cconcl_of thm),
232              ((("xs", 0), @{typ bool}), Thm.cterm_of ctxt container)])
233            @{thm rule_add}
234  in
235    rewrite_state_concl add_eqn thm
236  end
237
238\<comment> \<open>
239  Finds all the variables and type variables in the given thm,
240  then uses `attach` to stash them in a @{const "container"} within
241  the thm.
242
243  Returns a tuple containing the variables and type variables which were attached this way.
244\<close>
245fun annotate_with_vars_using (attach: Proof.context -> term list -> thm -> thm) ctxt thm =
246  let
247    val tvars = type_vars_of_term (Thm.prop_of thm) |> map TVar
248    val tvar_carriers = map (fn tvar => Const (@{const_name undefined}, tvar)) tvars
249    val vars = vars_of_term (Thm.prop_of thm) |> map Var
250    val annotated_rule = attach ctxt (vars @ tvar_carriers) thm
251  in ((vars, tvars), annotated_rule) end
252
253val annotate_rule = annotate_with_vars_using attach_rule_annotations
254val annotate_proof_state = annotate_with_vars_using attach_proof_annotations
255
256fun split_and_zip_instantiations (vars, tvars) (bounds, insts): instantiations =
257  let
258    val (var_insts, tvar_insts) = chop (length vars) insts
259    val tvar_insts' = map (TermExtras.drop_binders (length bounds) o fastype_of) tvar_insts
260  in {
261    bounds = bounds,
262    terms = vars ~~ var_insts,
263    typs = tvars ~~ tvar_insts'
264  } end
265
266\<comment>\<open>
267  Matches subgoals of the form:
268
269  @{term "\<And>A B C. X \<Longrightarrow> Y \<Longrightarrow> Z \<Longrightarrow> container True data"}
270
271  Extracts the instantiation variables from `?data`, and re-applies the surrounding
272  meta abstractions (in this case `\<And>A B C`).
273\<close>
274fun dest_instantiation_container_subgoal t =
275    let
276      val (vars, goal) = t |> TermExtras.strip_all
277      val goal = goal |> Logic.strip_imp_concl
278    in
279      case goal of
280        @{term_pat "Trueprop (container True ?data)"} =>
281            dest_term_container data
282            |> map (fn t => Logic.rlist_abs (rev vars, t)) (* reapply variables *)
283            |> pair vars
284            |> SOME
285      | _ => NONE
286    end
287
288\<comment>\<open>
289  Finds the first subgoal with a @{term container} conclusion. Extracts the data from
290  the container and removes the subgoal.
291\<close>
292fun detach_rule_result_annotations ctxt st =
293  let
294    val (idx, data) =
295        st
296        |> Thm.prems_of
297        |> Library.get_index dest_instantiation_container_subgoal
298        |> OptionExtras.get_or_else (fn () => error "No container subgoal!")
299    val st' =
300        st
301        |> resolve_tac ctxt @{thms elim} (idx + 1)
302        |> Seq.hd
303  in
304    (data, st')
305  end
306
307\<comment> \<open>
308  Instantiate subterms of a given term, using the supplied var_insts. A
309  complication is that to deal with bound variables, lambda terms might have
310  been inserted to the instantiations. To handle this, we first generate some
311  fresh free variables, apply them to the lambdas, do the substitution,
312  re-abstract the frees, and then clean up any inner applications.
313
314  subgoal: @{term "\<And>x::int. foo (\<lambda>a. a::'e) (\<lambda>a. a + x) (0::nat)"},
315  rule: @{term "foo ((f::'d \<Rightarrow> 'a \<Rightarrow> 'a) y) (g::'b \<Rightarrow> 'b) (0::'c::zero)"}, and
316  instantiations: {bounds: [("x", int)],
317                   terms: [(?f, \<lambda>x a b. b), (?g, \<lambda>x a. x + a), (?y, \<lambda>x. ?y x)],
318                   typs: [(?'a, 'e), (?'b, int), (?'c, nat)]},
319  this leads to
320  vars: [("x", int)],
321  var_insts: [(?f, \<lambda>a b. b), (?g, \<lambda>a. x + a), (?y, ?y x)]
322  subst_free: "foo ((\<lambda>a b. b) (?y x)) (\<lambda>a. a + x) 0"
323  absfree: "\<lambda>x. foo ((\<lambda>a b. b) (?y x)) (\<lambda>a. a + x) 0"
324  beta_norm: @{term "\<lambda>x. foo (\<lambda>a. a) (\<lambda>a. a + x) 0"}
325  abs_all: @{term "\<And>x. foo (\<lambda>a. a) (\<lambda>a. a + x) 0"}
326\<close>
327fun instantiate_terms ctxt bounds var_insts term =
328  let
329    val vars = Variable.variant_frees ctxt (term :: map #2 var_insts) bounds
330    fun var_inst_beta term term' =
331      (term, Term.betapplys (term', map Free vars))
332    val var_insts' = map (uncurry var_inst_beta) var_insts
333  in term
334    |> Term.subst_free var_insts'
335    |> fold Term.absfree vars
336    |> Envir.beta_norm
337    |> TermExtras.abs_all (length bounds)
338  end
339
340\<comment> \<open>
341  Instantiate subtypes of a given term, using the supplied tvar_insts. Similarly
342  to above, to deal with bound variables we first need to drop any binders
343  that had been added to the instantiations.
344\<close>
345fun instantiate_types ctxt bounds_num tvar_insts term =
346  let
347    fun instantiateT tvar_inst typ =
348      let
349        val tyenv = Sign.typ_match (Proof_Context.theory_of ctxt) tvar_inst Vartab.empty
350        val S = Vartab.dest tyenv
351        val S' = map (fn (s,(t,u)) => ((s,t),u)) S
352      in Term_Subst.instantiateT S' typ
353      end
354  in fold (fn typs => Term.map_types (instantiateT typs)) tvar_insts term
355  end
356
357\<comment> \<open>
358  Instantiate a given thm with the supplied instantiations, returning a term.
359\<close>
360fun instantiate_thm ctxt thm {bounds, terms as var_insts, typs as tvar_insts} =
361  Thm.prop_of thm
362  |> instantiate_terms ctxt bounds var_insts
363  |> instantiate_types ctxt (length bounds) tvar_insts
364
365fun filtered_instantiation_lines ctxt {bounds, terms, typs} =
366  let
367    val vars_lines =
368        map (fn (var, inst) =>
369          if var = inst then "" (* don't show unchanged *) else
370              "  " ^ Syntax.string_of_term ctxt var ^ "  =>  " ^
371              Syntax.string_of_term ctxt (TermExtras.abs_all (length bounds) inst) ^ "\n")
372        terms
373    val tvars_lines =
374        map (fn (tvar, inst) =>
375          if tvar = inst then "" (* don't show unchanged *) else
376              "  " ^ Syntax.string_of_typ ctxt tvar ^ "  =>  " ^
377              Syntax.string_of_typ ctxt inst ^ "\n")
378        typs
379  in
380    vars_lines @ tvars_lines
381  end
382
383\<comment>\<open>
384  Default callback for black-box method tracing. Prints nontrivial instantiations to tracing output
385  with the given title line.
386\<close>
387fun default_report ctxt title insts =
388  let
389    val all_insts = String.concat (filtered_instantiation_lines ctxt insts)
390  (* TODO: add a quiet flag, to suppress output when nothing was instantiated *)
391  in title ^ "\n" ^ (if all_insts = "" then "  (no instantiations)\n" else all_insts)
392     |> tracing
393  end
394
395\<comment> \<open>
396  Default callback for tracing rule applications. Prints nontrivial
397  instantiations to tracing output with the given title line. Separates
398  instantiations of rule variables and goal variables.
399\<close>
400fun default_rule_report ctxt title rule_insts proof_insts =
401  let
402    val rule_lines = String.concat (filtered_instantiation_lines ctxt rule_insts)
403    val rule_lines =
404        if rule_lines = ""
405        then "(no rule instantiations)\n"
406        else "rule instantiations:\n" ^ rule_lines;
407    val proof_lines = String.concat (filtered_instantiation_lines ctxt proof_insts)
408    val proof_lines =
409        if proof_lines = ""
410        then "(no goal instantiations)\n"
411        else "goal instantiations:\n" ^ proof_lines;
412  in title ^ "\n" ^ rule_lines ^ "\n" ^ proof_lines |> tracing  end
413
414\<comment> \<open>
415  `trace_schematic_insts_tac ctxt callback tactic thm idx` does the following:
416
417  - Produce a @{term container}-annotated version of `thm`.
418  - Runs `tactic` on subgoal `idx`, using the annotated version of `thm`.
419  - If the tactic succeeds, call `callback` with the rule instantiations and the goal
420    instantiations, in that order.
421\<close>
422fun trace_schematic_insts_tac
423    ctxt
424    (callback: instantiations -> instantiations -> unit)
425    (tactic: thm -> int -> tactic)
426    thm idx st =
427  let
428    val (rule_vars, annotated_rule) = annotate_rule ctxt thm
429    val (proof_vars, annotated_proof_state) = annotate_proof_state ctxt st
430    val st = tactic annotated_rule idx annotated_proof_state
431  in
432    st |> Seq.map (fn st =>
433      let
434        val (rule_terms, st) = detach_rule_result_annotations ctxt st
435        val (proof_terms, st) = detach_proof_annotations st
436        val rule_insts = split_and_zip_instantiations rule_vars rule_terms
437        val proof_insts = split_and_zip_instantiations proof_vars ([], proof_terms)
438        val () = callback rule_insts proof_insts
439      in
440        st
441      end
442    )
443  end
444
445\<comment>\<open>
446  ML interface, calls the supplied function with schematic unifications
447  (will be given all variables, including those that haven't been instantiated).
448\<close>
449fun trace_schematic_insts (method: Method.method) callback
450  = fn facts => fn (ctxt, st) =>
451    let
452      val (vars, annotated_st) = annotate_proof_state ctxt st
453    in (* Run the method *)
454      method facts (ctxt, annotated_st)
455      |> Seq.map_result (fn (ctxt', annotated_st') => let
456            (* Retrieve the stashed list, now with unifications *)
457            val (annotations, st') = detach_proof_annotations annotated_st'
458            val insts = split_and_zip_instantiations vars ([], annotations)
459            (* Report the list *)
460            val _ = callback insts
461         in (ctxt', st') end)
462    end
463
464end
465\<close>
466end
467
468method_setup trace_schematic_insts = \<open>
469  let
470    open Trace_Schematic_Insts
471  in
472    (Scan.option (Scan.lift Parse.liberal_name) -- Method.text_closure) >>
473    (fn (maybe_title, method_text) => fn ctxt =>
474      trace_schematic_insts
475          (Method.evaluate method_text ctxt)
476          (default_report ctxt
477              (Option.getOpt (maybe_title, "trace_schematic_insts:")))
478      |> skip_dummy_state
479    )
480  end
481\<close> "Method combinator to trace schematic variable and type instantiations"
482
483end
484