398 lines
13 KiB
Plaintext
398 lines
13 KiB
Plaintext
(*
|
|
* Copyright 2014, NICTA
|
|
*
|
|
* This software may be distributed and modified according to the terms of
|
|
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
|
* See "LICENSE_BSD2.txt" for details.
|
|
*
|
|
* @TAG(NICTA_BSD)
|
|
*
|
|
* Base of autolevity.
|
|
* Needs to be installed to track command start/end locations
|
|
*)
|
|
|
|
theory AutoLevity_Base
|
|
imports Main Apply_Trace
|
|
keywords "levity_tag" :: thy_decl
|
|
begin
|
|
|
|
|
|
ML \<open>
|
|
fun is_simp (_: Proof.context) (_: thm) = true
|
|
\<close>
|
|
|
|
ML \<open>
|
|
val is_simp_installed = is_some (
|
|
try (ML_Context.eval ML_Compiler.flags @{here})
|
|
(ML_Lex.read_pos @{here} "val is_simp = Raw_Simplifier.is_simp"));
|
|
\<close>
|
|
|
|
ML\<open>
|
|
(* Describing a ordering on Position.T. Optionally we compare absolute document position, or
|
|
just line numbers. Somewhat complicated by the fact that jEdit positions don't have line or
|
|
file identifiers. *)
|
|
|
|
fun pos_ord use_offset (pos1, pos2) =
|
|
let
|
|
fun get_offset pos = if use_offset then Position.offset_of pos else SOME 0;
|
|
|
|
fun get_props pos =
|
|
(SOME (Position.file_of pos |> the,
|
|
(Position.line_of pos |> the,
|
|
get_offset pos |> the)), NONE)
|
|
handle Option => (NONE, Position.parse_id pos)
|
|
|
|
val props1 = get_props pos1;
|
|
val props2 = get_props pos2;
|
|
|
|
in prod_ord
|
|
(option_ord (prod_ord string_ord (prod_ord int_ord int_ord)))
|
|
(option_ord (int_ord))
|
|
(props1, props2) end
|
|
|
|
structure Postab = Table(type key = Position.T val ord = (pos_ord false));
|
|
structure Postab_strict = Table(type key = Position.T val ord = (pos_ord true));
|
|
|
|
|
|
signature AUTOLEVITY_BASE =
|
|
sig
|
|
type extras = {levity_tag : string option, subgoals : int}
|
|
|
|
|
|
|
|
val get_transactions : unit -> ((string * extras) Postab_strict.table * string list Postab_strict.table) Symtab.table;
|
|
|
|
val get_applys : unit -> ((string * string list) list) Postab_strict.table Symtab.table;
|
|
|
|
val add_attribute_test: string -> (Proof.context -> thm -> bool) -> theory -> theory;
|
|
|
|
val attribs_of: Proof.context -> thm -> string list;
|
|
|
|
val used_facts: Proof.context option -> thm -> (string * thm) list;
|
|
val used_facts_attribs: Proof.context -> thm -> (string * string list) list;
|
|
|
|
(* Install toplevel hook for tracking command positions. *)
|
|
|
|
val setup_command_hook: {trace_apply : bool} -> theory -> theory;
|
|
|
|
(* Used to trace the dependencies of all apply statements.
|
|
They are set up by setup_command_hook if the appropriate hooks in the "Proof"
|
|
module exist. *)
|
|
|
|
val pre_apply_hook: Proof.context -> Method.text -> thm -> thm;
|
|
val post_apply_hook: Proof.context -> Method.text -> thm -> thm -> thm;
|
|
|
|
|
|
end;
|
|
|
|
|
|
|
|
|
|
structure AutoLevity_Base : AUTOLEVITY_BASE =
|
|
struct
|
|
|
|
val applys = Synchronized.var "applys"
|
|
(Symtab.empty : (((string * string list) list) Postab_strict.table) Symtab.table)
|
|
|
|
fun get_applys () = Synchronized.value applys;
|
|
|
|
type extras = {levity_tag : string option, subgoals : int}
|
|
|
|
|
|
val transactions = Synchronized.var "hook"
|
|
(Symtab.empty : ((string * extras) Postab_strict.table * ((string list) Postab_strict.table)) Symtab.table);
|
|
|
|
fun get_transactions () =
|
|
Synchronized.value transactions;
|
|
|
|
|
|
structure Data = Theory_Data
|
|
(
|
|
type T = (bool *
|
|
string option *
|
|
(Proof.context -> thm -> bool) Symtab.table); (* command_hook * levity tag * attribute tests *)
|
|
val empty = (false, NONE, Symtab.empty);
|
|
val extend = I;
|
|
fun merge (((b1, _, tab), (b2, _, tab')) : T * T) = (b1 orelse b2, NONE, Symtab.merge (fn _ => true) (tab, tab'));
|
|
);
|
|
|
|
val set_command_hook_flag = Data.map (@{apply 3(1)} (fn _ => true));
|
|
val get_command_hook_flag = #1 o Data.get
|
|
|
|
fun set_levity_tag tag = Data.map (@{apply 3(2)} (fn _ => tag));
|
|
val get_levity_tag = #2 o Data.get
|
|
|
|
fun update_attrib_tab f = Data.map (@{apply 3(3)} f);
|
|
|
|
|
|
fun add_attribute_test nm f =
|
|
let
|
|
val f' = (fn ctxt => fn thm => the_default false (try (f ctxt) thm))
|
|
in update_attrib_tab (Symtab.update_new (nm,f')) end;
|
|
|
|
val get_attribute_tests = Symtab.dest o #3 o Data.get;
|
|
|
|
(* Internal fact names get the naming scheme "foo_3" to indicate the third
|
|
member of the multi-thm "foo". We need to do some work to guess if
|
|
such a fact refers to an indexed multi-thm or a real fact named "foo_3" *)
|
|
|
|
fun get_ref_from_nm' nm =
|
|
let
|
|
val exploded = space_explode "_" nm;
|
|
val base = List.take (exploded, (length exploded) - 1) |> space_implode "_"
|
|
val idx = List.last exploded |> Int.fromString;
|
|
in if is_some idx andalso base <> "" then SOME (base, the idx) else NONE end
|
|
|
|
fun get_ref_from_nm nm = Option.join (try get_ref_from_nm' nm);
|
|
|
|
fun maybe_nth l = try (curry List.nth l)
|
|
|
|
|
|
|
|
fun fact_from_derivation ctxt xnm =
|
|
let
|
|
|
|
val facts = Proof_Context.facts_of ctxt;
|
|
(* TODO: Check that exported local fact is equivalent to external one *)
|
|
|
|
val idx_result =
|
|
let
|
|
val (name', idx) = get_ref_from_nm xnm |> the;
|
|
val entry = try (Facts.retrieve (Context.Proof ctxt) facts) (name', Position.none) |> the;
|
|
val thm = maybe_nth (#thms entry) (idx - 1) |> the;
|
|
in SOME thm end handle Option => NONE;
|
|
|
|
fun non_idx_result () =
|
|
let
|
|
val entry = try (Facts.retrieve (Context.Proof ctxt) facts) (xnm, Position.none) |> the;
|
|
val thm = try the_single (#thms entry) |> the;
|
|
in SOME thm end handle Option => NONE;
|
|
|
|
in
|
|
case idx_result of
|
|
SOME thm => SOME thm
|
|
| NONE => non_idx_result ()
|
|
end
|
|
|
|
(* Local facts (from locales) aren't marked in proof bodies, we only
|
|
see their external variants. We guess the local name from the external one
|
|
(i.e. "Theory_Name.Locale_Name.foo" -> "foo")
|
|
|
|
This is needed to perform localized attribute tests (e.g.. is this locale assumption marked as simp?) *)
|
|
|
|
(* TODO: extend_locale breaks this naming scheme by adding the "chunk" qualifier. This can
|
|
probably just be handled as a special case *)
|
|
|
|
fun most_local_fact_of ctxt xnm =
|
|
let
|
|
val local_name = try (fn xnm => Long_Name.explode xnm |> tl |> tl |> Long_Name.implode) xnm |> the;
|
|
in SOME (fact_from_derivation ctxt local_name |> the) end handle Option =>
|
|
fact_from_derivation ctxt xnm;
|
|
|
|
|
|
(* We recursively descend into the proof body to find dependent facts.
|
|
We skip over empty derivations or facts that we fail to find, but recurse
|
|
into their dependents. This ensures that an attempt to re-build the proof dependencies
|
|
graph will result in a connected graph. *)
|
|
|
|
fun thms_of (PBody {thms,...}) = thms
|
|
|
|
fun proof_body_descend' f get_fact (ident,(nm,_ , body)) deptab =
|
|
(if not (f nm) then
|
|
(Inttab.update_new (ident, SOME (nm, get_fact nm |> the)) deptab handle Inttab.DUP _ => deptab)
|
|
else raise Option) handle Option =>
|
|
((fold (proof_body_descend' f get_fact) (thms_of (Future.join body))
|
|
(Inttab.update_new (ident, NONE) deptab)) handle Inttab.DUP _ => deptab)
|
|
|
|
|
|
fun used_facts' f get_fact thm =
|
|
let
|
|
val body = thms_of (Thm.proof_body_of thm);
|
|
|
|
in fold (proof_body_descend' f get_fact) body Inttab.empty end
|
|
|
|
fun used_facts opt_ctxt thm =
|
|
let
|
|
val nm = Thm.get_name_hint thm;
|
|
val get_fact = case opt_ctxt of
|
|
SOME ctxt => most_local_fact_of ctxt
|
|
| NONE => (fn _ => SOME Drule.dummy_thm);
|
|
in
|
|
used_facts' (fn nm' => nm' = "" orelse nm' = nm) get_fact thm
|
|
|> Inttab.dest |> map_filter snd
|
|
end
|
|
|
|
fun attribs_of ctxt =
|
|
let
|
|
val tests = get_attribute_tests (Proof_Context.theory_of ctxt)
|
|
|> map (apsnd (fn test => test ctxt));
|
|
|
|
in (fn t => map_filter (fn (testnm, test) => if test t then SOME testnm else NONE) tests) end;
|
|
|
|
fun used_facts_attribs ctxt thm =
|
|
let
|
|
val fact_nms = used_facts (SOME ctxt) thm;
|
|
|
|
val attribs_of = attribs_of ctxt;
|
|
|
|
in map (apsnd attribs_of) fact_nms end
|
|
|
|
(* We identify "apply" applications by the document position of their corresponding method.
|
|
We can only get a document position out of "real" methods, so internal methods
|
|
(i.e. Method.Basic) won't have a position.*)
|
|
|
|
fun get_pos_of_text' (Method.Source src) = SOME (snd (Token.name_of_src src))
|
|
| get_pos_of_text' (Method.Combinator (_, _, texts)) = get_first get_pos_of_text' texts
|
|
| get_pos_of_text' _ = NONE
|
|
|
|
(* We only want to apply our hooks in batch mode, so we test if our position has a line number
|
|
(in jEdit it will only have an id number) *)
|
|
|
|
fun get_pos_of_text text = case get_pos_of_text' text of
|
|
SOME pos => if is_some (Position.line_of pos) then SOME pos else NONE
|
|
| NONE => NONE
|
|
|
|
(* Clear the theorem dependencies using the apply_trace oracle, then
|
|
pick up the new ones after the apply step is finished. *)
|
|
|
|
fun pre_apply_hook ctxt text thm =
|
|
case get_pos_of_text text of NONE => thm
|
|
| SOME _ =>
|
|
if Apply_Trace.can_clear (Proof_Context.theory_of ctxt)
|
|
then Apply_Trace.clear_deps thm
|
|
else thm;
|
|
|
|
|
|
val post_apply_hook = (fn ctxt => fn text => fn pre_thm => fn post_thm =>
|
|
case get_pos_of_text text of NONE => post_thm
|
|
| SOME pos => if Apply_Trace.can_clear (Proof_Context.theory_of ctxt) then
|
|
(let
|
|
val thy_nm = Context.theory_name (Thm.theory_of_thm post_thm);
|
|
|
|
val used_facts = the_default [] (try (used_facts_attribs ctxt) post_thm);
|
|
val _ =
|
|
Synchronized.change applys
|
|
(Symtab.map_default
|
|
(thy_nm, Postab_strict.empty) (Postab_strict.update (pos, used_facts)))
|
|
|
|
(* We want to keep our old theorem dependencies around, so we put them back into
|
|
the goal thm when we are done *)
|
|
|
|
val post_thm' = post_thm
|
|
|> Apply_Trace.join_deps pre_thm
|
|
|
|
in post_thm' end)
|
|
else post_thm)
|
|
|
|
(* The Proof hooks need to be patched in to track apply dependencies, but the rest of levity
|
|
can work without them. Here we graciously fail if the hook interface is missing *)
|
|
|
|
fun setup_pre_apply_hook () =
|
|
try (ML_Context.eval ML_Compiler.flags @{here})
|
|
(ML_Lex.read_pos @{here} "Proof.set_pre_apply_hook AutoLevity_Base.pre_apply_hook");
|
|
|
|
fun setup_post_apply_hook () =
|
|
try (ML_Context.eval ML_Compiler.flags @{here})
|
|
(ML_Lex.read_pos @{here} "Proof.set_post_apply_hook AutoLevity_Base.post_apply_hook");
|
|
|
|
(* This command is treated specially by AutoLevity_Theory_Report. The command executed directly
|
|
after this one will be tagged with the given tag *)
|
|
|
|
val _ =
|
|
Outer_Syntax.command @{command_keyword levity_tag} "tag for levity"
|
|
(Parse.string >> (fn str =>
|
|
Toplevel.local_theory NONE NONE
|
|
(Local_Theory.raw_theory (set_levity_tag (SOME str)))))
|
|
|
|
fun get_subgoals' state =
|
|
let
|
|
val proof_state = Toplevel.proof_of state;
|
|
val {goal, ...} = Proof.raw_goal proof_state;
|
|
in Thm.nprems_of goal end
|
|
|
|
fun get_subgoals state = the_default ~1 (try get_subgoals' state);
|
|
|
|
fun setup_toplevel_command_hook () =
|
|
Toplevel.add_hook (fn transition => fn start_state => fn end_state =>
|
|
let val name = Toplevel.name_of transition
|
|
val pos = Toplevel.pos_of transition;
|
|
val thy = Toplevel.theory_of start_state;
|
|
val thynm = Context.theory_name thy;
|
|
val end_thy = Toplevel.theory_of end_state;
|
|
in
|
|
if name = "clear_deps" orelse name = "dummy_apply" orelse Position.line_of pos = NONE then () else
|
|
(let
|
|
|
|
val levity_input = if name = "levity_tag" then get_levity_tag end_thy else NONE;
|
|
|
|
val subgoals = get_subgoals start_state;
|
|
|
|
val entry = {levity_tag = levity_input, subgoals = subgoals}
|
|
|
|
val _ =
|
|
Synchronized.change transactions
|
|
(Symtab.map_default (thynm, (Postab_strict.empty, Postab_strict.empty))
|
|
(apfst (Postab_strict.update (pos, (name, entry)))))
|
|
in () end) handle e => if Exn.is_interrupt e then Exn.reraise e else
|
|
Synchronized.change transactions
|
|
(Symtab.map_default (thynm, (Postab_strict.empty, Postab_strict.empty))
|
|
(apsnd (Postab_strict.map_default (pos, []) (cons (@{make_string} e)))))
|
|
end)
|
|
|
|
fun setup_attrib_tests theory = if not (is_simp_installed) then
|
|
error "Missing interface into Raw_Simplifier. Can't trace apply statements with unpatched isabelle."
|
|
else
|
|
let
|
|
fun is_first_cong ctxt thm =
|
|
let
|
|
val simpset = Raw_Simplifier.internal_ss (Raw_Simplifier.simpset_of ctxt);
|
|
val (congs, _) = #congs simpset;
|
|
val cong_thm = #mk_cong (#mk_rews simpset) ctxt thm;
|
|
in
|
|
case (find_first (fn (_, thm') => Thm.eq_thm_prop (cong_thm, thm')) congs) of
|
|
SOME (nm, _) =>
|
|
Thm.eq_thm_prop (find_first (fn (nm', _) => nm' = nm) congs |> the |> snd, cong_thm)
|
|
| NONE => false
|
|
end
|
|
|
|
fun is_classical proj ctxt thm =
|
|
let
|
|
val intros = proj (Classical.claset_of ctxt |> Classical.rep_cs);
|
|
val results = Item_Net.retrieve intros (Thm.full_prop_of thm);
|
|
in exists (fn (thm', _, _) => Thm.eq_thm_prop (thm',thm)) results end
|
|
in
|
|
theory
|
|
|> add_attribute_test "simp" is_simp
|
|
|> add_attribute_test "cong" is_first_cong
|
|
|> add_attribute_test "intro" (is_classical #unsafeIs)
|
|
|> add_attribute_test "intro!" (is_classical #safeIs)
|
|
|> add_attribute_test "elim" (is_classical #unsafeEs)
|
|
|> add_attribute_test "elim!" (is_classical #safeEs)
|
|
|> add_attribute_test "dest" (fn ctxt => fn thm => is_classical #unsafeEs ctxt (Tactic.make_elim thm))
|
|
|> add_attribute_test "dest!" (fn ctxt => fn thm => is_classical #safeEs ctxt (Tactic.make_elim thm))
|
|
end
|
|
|
|
|
|
fun setup_command_hook {trace_apply, ...} theory =
|
|
if get_command_hook_flag theory then theory else
|
|
let
|
|
val _ = if trace_apply then
|
|
(the (setup_pre_apply_hook ());
|
|
the (setup_post_apply_hook ()))
|
|
handle Option => error "Missing interface into Proof module. Can't trace apply statements with unpatched isabelle"
|
|
else ()
|
|
|
|
val _ = setup_toplevel_command_hook ();
|
|
|
|
val theory' = theory
|
|
|> trace_apply ? setup_attrib_tests
|
|
|> set_command_hook_flag
|
|
|
|
in theory' end;
|
|
|
|
|
|
end
|
|
\<close>
|
|
|
|
end
|