src/HOL/Boogie/Tools/boogie_commands.ML

merged verification condition structure and term representation in one datatype,
extended the set of operations on verification conditions (retrieve more information, advanced splitting of paths),
simplified discharging of verification conditions (due to improved datatype),
added variantions of commands (extract different parts of verification conditions, scan until first "hard" assertion)

(*  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) 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) 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 

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 ^ ".")))

fun boogie_vc (vc_name, vc_opts) lthy =
  let
    val thy = ProofContext.theory_of lthy
    val vc = get_vc thy vc_name

    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_filter (Boogie_VCs.extract vc) ls)
    val ts = map Boogie_VCs.prop_of_vc vcs

    val discharge = fold (Boogie_VCs.discharge o pair vc_name)
    fun after_qed [thms] = Local_Theory.theory (discharge (vcs ~~ thms))
      | after_qed _ = I
  in
    lthy
    |> fold Variable.auto_fixes ts
    |> Proof.theorem_i NONE after_qed [map (rpair []) ts]
  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 thy
    |> Proof.theorem_i NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
    |> Proof.apply meth
    |> Seq.hd
    |> Proof.global_done_proof
in
fun boogie_narrow_vc timeout vc_name meth thy =
  let
    val tp = TimeLimit.timeLimit (Time.fromSeconds timeout) (prove thy meth)

    fun try_vc (tag, split_tag) split vc = (trying tag;
      (case try tp vc of
        SOME _ => (success_on tag; [])
      | NONE => (failure_on tag split_tag; split vc)))

    fun some_asserts vc =
      try_vc (string_of_asserts vc,
        if Boogie_VCs.size_of vc = 1 then "." else ", further splitting ...")
        (divide some_asserts) vc

    fun single_path p =
      try_vc (string_of_path p, ", splitting into assertions ...")
        (divide some_asserts)

    val complete_vc =
      try_vc ("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 _ =
  OuterSyntax.command "boogie_open"
    "Open a new Boogie environment and load a Boogie-generated .b2i file."
    OuterKeyword.thy_decl
    (scan_opt "quiet" -- OuterParse.name >> (Toplevel.theory o boogie_open))


val vc_name = OuterParse.name

val vc_labels = Scan.repeat1 OuterParse.name

val vc_paths =
  OuterParse.nat -- (Args.$$$ "-" |-- OuterParse.nat) >> (op upto) ||
  OuterParse.nat >> single

val vc_opts =
  scan_arg
   (scan_val "examine" vc_labels >> VC_Examine ||
    scan_val "take" ((OuterParse.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 _ =
  OuterSyntax.command "boogie_vc"
    "Enter into proof mode for a specific verification condition."
    OuterKeyword.thy_goal
    (vc_name -- vc_opts >> (fn args =>
      (Toplevel.print o Toplevel.local_theory_to_proof NONE (boogie_vc args))))


val default_timeout = 5

val status_test =
  scan_arg (
    (Args.$$$ "scan" >> K boogie_scan_vc ||
     Args.$$$ "narrow" >> K boogie_narrow_vc) --
    Scan.optional (scan_val "timeout" OuterParse.nat) default_timeout) --
  vc_name -- Method.parse >>
  (fn (((f, timeout), vc_name), meth) => f timeout 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 _ =
  OuterSyntax.improper_command "boogie_status"
    "Show the name and state of all loaded verification conditions."
    OuterKeyword.diag
    (status_test >> status_cmd ||
     status_vc >> status_cmd ||
     Scan.succeed (status_cmd boogie_status))


val _ =
  OuterSyntax.command "boogie_end"
    "Close the current Boogie environment."
    OuterKeyword.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