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