adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

isabelle-2016: update Apply_Trace and fix to work in batch mode.

This commit is contained in:
Daniel Matichuk 2016-02-03 20:26:06 -08:00 committed by Matthew Brecknell
parent 1979590f7f
commit 2460f00ad8
2 changed files with 7 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
lib/Apply_Trace.thy
View File

@ -71,7 +71,7 @@ fun proof_body_descend' (_,("",_,body)) = fold (append o proof_body_descend') (t
fun used_facts thm = fold (append o proof_body_descend') (thms_of (Thm.proof_body_of thm)) []
fun raw_primitive_text f = Method.Basic (fn ctxt => (Method.METHOD (K (fn thm => Seq.single (f thm)))))
fun raw_primitive_text f = Method.Basic (fn _ => (Method.METHOD (K (fn thm => Seq.single (f thm)))))
(*Find local facts from new hyps*)
@ -130,7 +130,8 @@ end
fun method_error kind pos state =
Seq.single (Proof_Display.method_error kind pos (Proof.raw_goal state));
fun apply args f text = Proof.assert_backward #> refine args f text #> Seq.map_result (Proof.using_facts []);
fun apply args f text = Proof.assert_backward #> refine args f text #>
Seq.maps_results (Proof.apply ((raw_primitive_text I),(Position.none, Position.none)));
fun apply_results args f (text, range) =
Seq.APPEND (apply args f text, method_error "" (Position.set_range range));

7
lib/Apply_Trace_Cmd.thy
View File

@ -75,8 +75,8 @@ fun pretty_fact only_names ctxt (FoundName ((name, idx), thm)) =
SOME n => Pretty.str ("(" ^ string_of_int (n + 1) ^ ")")
| NONE => Pretty.str ""] @
(if only_names then []
else [Pretty.str ":",Pretty.brk 1, Display.pretty_thm ctxt thm]))
| pretty_fact only_names ctxt (UnknownName (name, prop)) =
else [Pretty.str ":",Pretty.brk 1, Thm.pretty_thm ctxt thm]))
| pretty_fact _ ctxt (UnknownName (name, prop)) =
Pretty.block
[Pretty.str name, Pretty.str "(?) :", Pretty.brk 1,
Syntax.unparse_term ctxt prop]
@ -100,7 +100,8 @@ let
val deps = case query of SOME (raw_query,pos) =>
let
val q = Find_Theorems.read_query (Position.advance_offset 1 pos) raw_query;
val pos' = perhaps (try (Position.advance_offset 1)) pos;
val q = Find_Theorems.read_query pos' raw_query;
val results = Find_Theorems.find_theorems_cmd ctxt (SOME thm) (SOME 1000000000) false q
|> snd
|> map fact_ref_to_name;