prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
eliminated old-style structure aliases K = Keyword, P = Parse;
(* Title: HOL/Boogie/Tools/boogie_commands.ML
Author: Sascha Boehme, TU Muenchen
Isar commands to create a Boogie environment simulation.
*)
signature BOOGIE_COMMANDS =
sig
val setup: theory -> theory
end
structure Boogie_Commands: BOOGIE_COMMANDS =
struct
(* commands *)
fun boogie_open ((quiet, base_name), offsets) thy =
let
val path = Path.explode (base_name ^ ".b2i")
val _ = File.exists path orelse
error ("Unable to find file " ^ quote (Path.implode path))
val _ = Boogie_VCs.is_closed thy orelse
error ("Found the beginning of a new Boogie environment, " ^
"but another Boogie environment is still open.")
in Boogie_Loader.load_b2i (not quiet) offsets path thy end
datatype vc_opts =
VC_Complete |
VC_Take of int list * (bool * string list) option |
VC_Only of string list |
VC_Without of string list |
VC_Examine of string list |
VC_Single of string
fun get_vc thy vc_name =
(case Boogie_VCs.lookup thy vc_name of
SOME vc => vc
| NONE =>
(case AList.lookup (op =) (Boogie_VCs.state_of thy) vc_name of
SOME Boogie_VCs.Proved => error ("The verification condition " ^
quote vc_name ^ " has already been proved.")
| _ => error ("There is no verification condition " ^
quote vc_name ^ ".")))
local
fun split_goal t =
(case Boogie_Tactics.split t of
[tp] => tp
| _ => error "Multiple goals.")
fun single_prep t =
let
val (us, u) = split_goal t
val assms = [((@{binding vc_trace}, []), map (rpair []) us)]
in
pair [u] o snd o ProofContext.add_assms_i Assumption.assume_export assms
end
fun single_prove goal ctxt thm =
Goal.prove ctxt [] [] goal (fn {context, ...} => HEADGOAL (
Boogie_Tactics.split_tac
THEN' Boogie_Tactics.drop_assert_at_tac
THEN' SUBPROOF (fn _ => Tactic.rtac thm 1) context))
in
fun boogie_vc (vc_name, vc_opts) thy =
let
val vc = get_vc thy vc_name
fun extract vc l =
(case Boogie_VCs.extract vc l of
SOME vc' => vc'
| NONE => error ("There is no assertion to be proved with label " ^
quote l ^ "."))
val vcs =
(case vc_opts of
VC_Complete => [vc]
| VC_Take (ps, NONE) => [Boogie_VCs.paths_and ps [] vc]
| VC_Take (ps, SOME (true, ls)) => [Boogie_VCs.paths_and ps ls vc]
| VC_Take (ps, SOME (false, ls)) => [Boogie_VCs.paths_without ps ls vc]
| VC_Only ls => [Boogie_VCs.only ls vc]
| VC_Without ls => [Boogie_VCs.without ls vc]
| VC_Examine ls => map (extract vc) ls
| VC_Single l => [extract vc l])
val ts = map Boogie_VCs.prop_of_vc vcs
val (prepare, finish) =
(case vc_opts of
VC_Single _ => (single_prep (hd ts), single_prove (hd ts))
| _ => (pair ts, K I))
val discharge = fold (Boogie_VCs.discharge o pair vc_name)
fun after_qed [thms] = ProofContext.theory (discharge (vcs ~~ thms))
| after_qed _ = I
in
ProofContext.init_global thy
|> fold Variable.auto_fixes ts
|> (fn ctxt1 => ctxt1
|> prepare
|-> (fn us => fn ctxt2 => ctxt2
|> Proof.theorem NONE (fn thmss => fn ctxt =>
let val export = map (finish ctxt1) o ProofContext.export ctxt ctxt2
in after_qed (map export thmss) ctxt end) [map (rpair []) us]))
end
end
fun write_list head =
map Pretty.str o sort (dict_ord string_ord o pairself explode) #>
Pretty.writeln o Pretty.big_list head
fun parens s = "(" ^ s ^ ")"
fun boogie_status thy =
let
fun string_of_state Boogie_VCs.Proved = "proved"
| string_of_state Boogie_VCs.NotProved = "not proved"
| string_of_state Boogie_VCs.PartiallyProved = "partially proved"
in
Boogie_VCs.state_of thy
|> map (fn (name, proved) => name ^ " " ^ parens (string_of_state proved))
|> write_list "Boogie verification conditions:"
end
fun boogie_status_vc full vc_name thy =
let
fun pretty tag s = s ^ " " ^ parens tag
val (not_proved, proved) = Boogie_VCs.state_of_vc thy vc_name
in
if full
then write_list ("Assertions of Boogie verification condition " ^
quote vc_name ^ ":")
(map (pretty "proved") proved @ map (pretty "not proved") not_proved)
else write_list ("Unproved assertions of Boogie verification condition " ^
quote vc_name ^ ":") not_proved
end
fun boogie_status_vc_paths full vc_name thy =
let
fun labels ls = Pretty.blk (0, Pretty.breaks (map Pretty.str ls))
fun pp (i, ns) =
if full
then
[Pretty.big_list ("Path " ^ string_of_int (i+1) ^ ":")
[labels (map (fn (n, true) => n | (n, _) => parens n) ns)]]
else
let val ns' = map_filter (fn (n, true) => SOME n | _ => NONE) ns
in
if null ns' then []
else
[Pretty.big_list ("Unproved assertions of path " ^
string_of_int (i+1) ^ ":") [labels ns']]
end
in
Pretty.writeln
(Pretty.big_list
("Paths of Boogie verification condition " ^ quote vc_name ^ ":")
(flat (map_index pp (Boogie_VCs.path_names_of (get_vc thy vc_name)))))
end
local
fun trying s = tracing ("Trying " ^ s ^ " ...")
fun success_on s = tracing ("Succeeded on " ^ s ^ ".")
fun failure_on s c = tracing ("Failed on " ^ s ^ c)
fun string_of_asserts vc = space_implode ", " (fst (Boogie_VCs.names_of vc))
fun string_of_path (i, n) =
"path " ^ string_of_int i ^ " of " ^ string_of_int n
fun itemize_paths ps =
let val n = length ps
in fst (fold_map (fn p => fn i => (((i, n), p), i+1)) ps 1) end
fun par_map f = flat o Par_List.map f
fun divide f vc =
let val n = Boogie_VCs.size_of vc
in
if n <= 1 then fst (Boogie_VCs.names_of vc)
else
let val (vc1, vc2) = the (Boogie_VCs.split_path (n div 2) vc)
in par_map f [vc1, vc2] end
end
fun prove thy meth vc =
ProofContext.init_global thy
|> Proof.theorem NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
|> Proof.apply meth
|> Seq.hd
|> Proof.global_done_proof
in
fun boogie_narrow_vc (quick, timeout) vc_name meth thy =
let
fun tp t = TimeLimit.timeLimit (Time.fromSeconds t) (prove thy meth)
fun try_vc t (tag, split_tag) split vc = (trying tag;
(case try (tp t) vc of
SOME _ => (success_on tag; [])
| NONE => (failure_on tag split_tag; split vc)))
fun some_asserts vc =
let
val (t, sep) = if Boogie_VCs.size_of vc = 1 then (timeout, ".")
else (quick, ", further splitting ...")
in try_vc t (string_of_asserts vc, sep) (divide some_asserts) vc end
fun single_path p =
try_vc quick (string_of_path p, ", splitting into assertions ...")
(divide some_asserts)
val complete_vc =
try_vc quick ("full goal", ", splitting into paths ...")
(par_map (uncurry single_path) o itemize_paths o Boogie_VCs.paths_of)
val unsolved = complete_vc (get_vc thy vc_name)
in
if null unsolved
then writeln ("Completely solved Boogie verification condition " ^
quote vc_name ^ ".")
else write_list ("Unsolved assertions of Boogie verification condition " ^
quote vc_name ^ ":") unsolved
end
fun boogie_scan_vc timeout vc_name meth thy =
let
val tp = TimeLimit.timeLimit (Time.fromSeconds timeout) (prove thy meth)
val vc = get_vc thy vc_name
fun prove_assert name =
(trying name; tp (the (Boogie_VCs.extract vc name)))
val find_first_failure = find_first (is_none o try prove_assert)
in
(case find_first_failure (fst (Boogie_VCs.names_of vc)) of
SOME name => writeln ("failed on " ^ quote name)
| NONE => writeln "succeeded")
end
end
fun boogie_end thy =
let
fun not_proved (_, Boogie_VCs.Proved) = NONE
| not_proved (name, _) = SOME name
val unproved = map_filter not_proved (Boogie_VCs.state_of thy)
in
if null unproved then Boogie_VCs.close thy
else error (Pretty.string_of (Pretty.big_list
"The following verification conditions have not been proved:"
(map Pretty.str unproved)))
end
(* syntax and setup *)
fun scan_val n f = Args.$$$ n -- Args.colon |-- f
fun scan_arg f = Args.parens f
fun scan_opt n = Scan.optional (scan_arg (Args.$$$ n >> K true)) false
val vc_offsets = Scan.optional (Args.bracks (Parse.list1
(Parse.string --| Args.colon -- Parse.nat))) []
val _ =
Outer_Syntax.command "boogie_open"
"Open a new Boogie environment and load a Boogie-generated .b2i file."
Keyword.thy_decl
(scan_opt "quiet" -- Parse.name -- vc_offsets >>
(Toplevel.theory o boogie_open))
val vc_name = Parse.name
val vc_label = Parse.name
val vc_labels = Scan.repeat1 vc_label
val vc_paths =
Parse.nat -- (Args.$$$ "-" |-- Parse.nat) >> (op upto) ||
Parse.nat >> single
val vc_opts =
scan_arg
(scan_val "assertion" vc_label >> VC_Single ||
scan_val "examine" vc_labels >> VC_Examine ||
scan_val "take" ((Parse.list vc_paths >> flat) -- Scan.option (
scan_val "without" vc_labels >> pair false ||
scan_val "and_also" vc_labels >> pair true) >> VC_Take) ||
scan_val "only" vc_labels >> VC_Only ||
scan_val "without" vc_labels >> VC_Without) ||
Scan.succeed VC_Complete
val _ =
Outer_Syntax.command "boogie_vc"
"Enter into proof mode for a specific verification condition."
Keyword.thy_goal
(vc_name -- vc_opts >> (fn args =>
(Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
val quick_timeout = 5
val default_timeout = 20
fun timeout name = Scan.optional (scan_val name Parse.nat)
val status_test =
scan_arg (
Args.$$$ "scan" |-- timeout "timeout" quick_timeout >> boogie_scan_vc ||
Args.$$$ "narrow" |-- timeout "step_timeout" quick_timeout --
timeout "final_timeout" default_timeout >> boogie_narrow_vc) --
vc_name -- Method.parse >>
(fn ((f, vc_name), meth) => f vc_name meth)
val status_vc =
(scan_arg
(Args.$$$ "full" |--
(Args.$$$ "paths" >> K (boogie_status_vc_paths true) ||
Scan.succeed (boogie_status_vc true)) ||
Args.$$$ "paths" >> K (boogie_status_vc_paths false)) ||
Scan.succeed (boogie_status_vc false)) --
vc_name >> (fn (f, vc_name) => f vc_name)
fun status_cmd f = Toplevel.no_timing o Toplevel.keep (fn state =>
f (Toplevel.theory_of state))
val _ =
Outer_Syntax.improper_command "boogie_status"
"Show the name and state of all loaded verification conditions."
Keyword.diag
(status_test >> status_cmd ||
status_vc >> status_cmd ||
Scan.succeed (status_cmd boogie_status))
val _ =
Outer_Syntax.command "boogie_end"
"Close the current Boogie environment."
Keyword.thy_decl
(Scan.succeed (Toplevel.theory boogie_end))
val setup = Theory.at_end (fn thy =>
let
val _ = Boogie_VCs.is_closed thy
orelse error ("Found the end of the theory, " ^
"but the last Boogie environment is still open.")
in NONE end)
end