src/HOL/Boogie/Tools/boogie_vcs.ML

final tuning;

(*  Title:      HOL/Boogie/Tools/boogie_vcs.ML
    Author:     Sascha Boehme, TU Muenchen

Store for Boogie's verification conditions.
*)

signature BOOGIE_VCS =
sig
  type vc
  val prop_of_vc: vc -> term
  val size_of: vc -> int
  val names_of: vc -> string list * string list
  val path_names_of: vc -> (string * bool) list list
  val paths_of: vc -> vc list
  val split_path: int -> vc -> (vc * vc) option
  val extract: vc -> string -> vc option
  val only: string list -> vc -> vc
  val without: string list -> vc -> vc
  val paths_and: int list -> string list -> vc -> vc
  val paths_without: int list -> string list -> vc -> vc

  datatype state = Proved | NotProved | PartiallyProved
  val set: (string * term) list -> theory -> theory
  val lookup: theory -> string -> vc option
  val discharge: string * (vc * thm) -> theory -> theory
  val state_of: theory -> (string * state) list
  val state_of_vc: theory -> string -> string list * string list
  val close: theory -> theory
  val is_closed: theory -> bool

  val rewrite_vcs: (theory -> term -> term) -> (theory -> thm -> thm) ->
    theory -> theory
end

structure Boogie_VCs: BOOGIE_VCS =
struct

fun app_both f g (x, y) = (f x, g y)
fun app_hd_tl f g = (fn [] => [] | x :: xs => f x :: map g xs)


(* abstract representation of verification conditions *)

datatype vc =
  Assume of term * vc |
  Assert of (string * term) * vc |
  Ignore of vc |
  Proved of string * vc |
  Choice of vc * vc |
  True

val assume = curry Assume and assert = curry Assert
and proved = curry Proved and choice = curry Choice
and choice' = curry (Choice o swap)

val vc_of_term =
  let
    fun vc_of @{term True} = NONE
      | vc_of (@{term assert_at} $ Free (n, _) $ t) =
          SOME (Assert ((n, t), True))
      | vc_of (@{term "op -->"} $ @{term True} $ u) = vc_of u
      | vc_of (@{term "op -->"} $ t $ u) =
          vc_of u |> Option.map (assume t)
      | vc_of (@{term "op &"} $ (@{term assert_at} $ Free (n, _) $ t) $ u) =
          SOME (vc_of u |> the_default True |> assert (n, t))
      | vc_of (@{term "op &"} $ t $ u) =
          (case (vc_of t, vc_of u) of
            (NONE, r) => r
          | (l, NONE) => l
          | (SOME lv, SOME rv) => SOME (Choice (lv, rv)))
      | vc_of t = raise TERM ("vc_of_term", [t])
  in the_default True o vc_of end

val prop_of_vc =
  let
    fun mk_conj t u = @{term "op &"} $ t $ u

    fun term_of (Assume (t, v)) = @{term "op -->"} $ t $ term_of v
      | term_of (Assert ((n, t), v)) =
          mk_conj (@{term assert_at} $ Free (n, @{typ bool}) $ t) (term_of v)
      | term_of (Ignore v) = term_of v
      | term_of (Proved (_, v)) = term_of v
      | term_of (Choice (lv, rv)) = mk_conj (term_of lv) (term_of rv)
      | term_of True = @{term True}
  in HOLogic.mk_Trueprop o term_of end


(* properties of verification conditions *)

fun size_of (Assume (_, v)) = size_of v
  | size_of (Assert (_, v)) = size_of v + 1
  | size_of (Ignore v) = size_of v
  | size_of (Proved (_, v)) = size_of v
  | size_of (Choice (lv, rv)) = size_of lv + size_of rv
  | size_of True = 0

val names_of =
  let
    fun add (Assume (_, v)) = add v
      | add (Assert ((n, _), v)) = apfst (cons n) #> add v
      | add (Ignore v) = add v
      | add (Proved (n, v)) = apsnd (cons n) #> add v
      | add (Choice (lv, rv)) = add lv #> add rv
      | add True = I
  in (fn vc => pairself rev (add vc ([], []))) end

fun path_names_of (Assume (_, v)) = path_names_of v
  | path_names_of (Assert ((n, _), v)) =
      path_names_of v
      |> app_hd_tl (cons (n, true)) (cons (n, false))
  | path_names_of (Ignore v) = path_names_of v
  | path_names_of (Proved (n, v)) = map (cons (n, false)) (path_names_of v)
  | path_names_of (Choice (lv, rv)) = path_names_of lv @ path_names_of rv
  | path_names_of True = [[]]

fun count_paths (Assume (_, v)) = count_paths v
  | count_paths (Assert (_, v)) = count_paths v
  | count_paths (Ignore v) = count_paths v
  | count_paths (Proved (_, v)) = count_paths v
  | count_paths (Choice (lv, rv)) = count_paths lv + count_paths rv
  | count_paths True = 1


(* extract parts of a verification condition *)

fun paths_of (Assume (t, v)) = paths_of v |> map (assume t)
  | paths_of (Assert (a, v)) = paths_of v |> app_hd_tl (assert a) Ignore
  | paths_of (Ignore v) = paths_of v |> map Ignore
  | paths_of (Proved (n, v)) = paths_of v |> app_hd_tl (proved n) Ignore
  | paths_of (Choice (lv, rv)) =
      map (choice' True) (paths_of lv) @ map (choice True) (paths_of rv)
  | paths_of True = [True]

fun prune f (Assume (t, v)) = Option.map (assume t) (prune f v)
  | prune f (Assert (a, v)) = f a v
  | prune f (Ignore v) = Option.map Ignore (prune f v)
  | prune f (Proved (n, v)) = Option.map (proved n) (prune f v)
  | prune f (Choice (lv, rv)) =
      (case (prune f lv, prune f rv) of
        (NONE, r) => r |> Option.map (choice True)
      | (l, NONE) => l |> Option.map (choice' True)
      | (SOME lv', SOME rv') => SOME (Choice (lv', rv')))
  | prune _ True = NONE

val split_path =
  let
    fun app f = Option.map (pairself f)

    fun split i (Assume (t, v)) = app (assume t) (split i v)
      | split i (Assert (a, v)) =
          if i > 1
          then Option.map (app_both (assert a) Ignore) (split (i-1) v)
          else Option.map (pair (Assert (a, True)))
            (prune (SOME o Assert oo pair) (Ignore v))
      | split i (Ignore v) = app Ignore (split i v)
      | split i (Proved (n, v)) = app (proved n) (split i v)
      | split i (Choice (v, True)) = app (choice' True) (split i v)
      | split i (Choice (True, v)) = app (choice True) (split i v)
      | split _ _ = NONE
  in split end

fun select_labels P =
  let
    fun assert (a as (n, _)) v =
      if P n then SOME (Assert (a, the_default True v))
      else Option.map Ignore v
    fun sel vc = prune (fn a => assert a o sel) vc
  in sel end

fun extract vc l = select_labels (equal l) vc
fun only ls = the_default True o select_labels (member (op =) ls)
fun without ls = the_default True o select_labels (not o member (op =) ls)

fun select_paths ps sub_select =
  let
    fun disjoint pp = null (inter (op =) ps pp)

    fun sel pp (Assume (t, v)) = Assume (t, sel pp v)
      | sel pp (Assert (a, v)) =
          if member (op =) ps (hd pp)
          then Assert (a, sel pp v)
          else Ignore (sel pp v)
      | sel pp (Ignore v) = Ignore (sel pp v)
      | sel pp (Proved (n, v)) = Proved (n, sel pp v)
      | sel pp (Choice (lv, rv)) =
          let val (lpp, rpp) = chop (count_paths lv) pp
          in
            if disjoint lpp then Choice (sub_select lv, sel rpp rv)
            else if disjoint rpp then Choice (sel lpp lv, sub_select rv)
            else Choice (sel lpp lv, sel rpp rv)
          end
      | sel _ True = True

    fun sel0 vc =
      let val pp = 1 upto count_paths vc
      in if disjoint pp then True else sel pp vc end
  in sel0 end

fun paths_and ps ls = select_paths ps (only ls)
fun paths_without ps ls = without ls o select_paths ps (K True)


(* discharge parts of a verification condition *)

local
  fun cprop_of thy t = Thm.cterm_of thy (HOLogic.mk_Trueprop t)
  fun imp_intr ct thm = Thm.implies_intr ct thm COMP_INCR @{thm impI}
  fun imp_elim th thm = @{thm mp} OF [thm, th]
  fun conj1 thm = @{thm conjunct1} OF [thm]
  fun conj2 thm = @{thm conjunct2} OF [thm]
  fun conj_intr lth rth = @{thm conjI} OF [lth, rth]
in
fun thm_of thy (Assume (t, v)) = imp_intr (cprop_of thy t) (thm_of thy v)
  | thm_of thy (Assert (_, v)) = thm_of thy v
  | thm_of thy (Ignore v) = thm_of thy v
  | thm_of thy (Proved (_, v)) = thm_of thy v
  | thm_of thy (Choice (lv, rv)) = conj_intr (thm_of thy lv) (thm_of thy rv)
  | thm_of _ True = @{thm TrueI}

fun join (Assume (_, pv), pthm) (Assume (t, v), thm) =
      let
        val mk_prop = Thm.capply @{cterm Trueprop}
        val ct = Thm.cprop_of thm |> Thm.dest_arg |> Thm.dest_arg1 |> mk_prop
        val th = Thm.assume ct
        val (v', thm') = join (pv, imp_elim th pthm) (v, imp_elim th thm)
      in (Assume (t, v'), imp_intr ct thm') end
  | join (Assert ((pn, pt), pv), pthm) (Assert ((n, t), v), thm) =
      let val pthm1 = conj1 pthm
      in
        if pn = n andalso pt aconv t
        then
          let val (v', thm') = join (pv, conj2 pthm) (v, thm)
          in (Proved (n, v'), conj_intr pthm1 thm') end
        else raise THM ("join: not matching", 1, [thm, pthm])
      end
  | join (Ignore pv, pthm) (Assert (a, v), thm) =
      join (pv, pthm) (v, thm) |>> assert a
  | join (Proved (_, pv), pthm) (Proved (n, v), thm) =
      let val (v', thm') = join (pv, pthm) (v, conj2 thm)
      in (Proved (n, v'), conj_intr (conj1 thm) thm') end
  | join (Ignore pv, pthm) (Proved (n, v), thm) =
      let val (v', thm') = join (pv, pthm) (v, conj2 thm)
      in (Proved (n, v'), conj_intr (conj1 thm) thm') end
  | join (Choice (plv, prv), pthm) (Choice (lv, rv), thm) =
      let
        val (lv', lthm) = join (plv, conj1 pthm) (lv, conj1 thm)
        val (rv', rthm) = join (prv, conj2 pthm) (rv, conj2 thm)
      in (Choice (lv', rv'), conj_intr lthm rthm) end
  | join (True, pthm) (v, thm) =
      if Thm.prop_of pthm aconv @{prop True} then (v, thm)
      else raise THM ("join: not True", 1, [pthm])
  | join (_, pthm) (_, thm) = raise THM ("join: not matching", 1, [thm, pthm])
end


(* the VC store *)

fun err_unfinished () = error "An unfinished Boogie environment is still open."

fun err_vcs names = error (Pretty.string_of
  (Pretty.big_list "Undischarged Boogie verification conditions found:"
    (map Pretty.str names)))

structure VCs = Theory_Data
(
  type T = ((vc * (term * thm)) Symtab.table * (theory -> thm -> thm)) option
  val empty = NONE
  val extend = I
  fun merge (NONE, NONE) = NONE
    | merge _ = err_unfinished ()
)

fun prep thy = vc_of_term #> (fn vc => (vc, (prop_of_vc vc, thm_of thy vc)))

fun set vcs thy = VCs.map (fn
    NONE => SOME (Symtab.make (map (apsnd (prep thy)) vcs), K I)
  | SOME _ => err_unfinished ()) thy

fun lookup thy name =
  (case VCs.get thy of
    SOME (vcs, _) => Option.map fst (Symtab.lookup vcs name)
  | NONE => NONE)

fun discharge (name, prf) =
  let fun jn (vc, (t, thm)) = join prf (vc, thm) |> apsnd (pair t)
  in VCs.map (Option.map (apfst (Symtab.map_entry name jn))) end

datatype state = Proved | NotProved | PartiallyProved

fun state_of_vc thy name =
  (case lookup thy name of
    SOME vc => names_of vc
  | NONE => ([], []))

fun state_of_vc' (vc, _) =
  (case names_of vc of
    ([], _) => Proved
  | (_, []) => NotProved
  | (_, _) => PartiallyProved)

fun state_of thy =
  (case VCs.get thy of
    SOME (vcs, _) => map (apsnd state_of_vc') (Symtab.dest vcs)
  | NONE => [])

fun finished g (_, (t, thm)) = Thm.prop_of (g thm) aconv t

fun close thy = thy |> VCs.map (fn
    SOME (vcs, g) =>
      let fun check vc = state_of_vc' vc = Proved andalso finished (g thy) vc
      in
        Symtab.dest vcs
        |> map_filter (fn (n, vc) => if check vc then NONE else SOME n)
        |> (fn names => if null names then NONE else err_vcs names)
      end
  | NONE => NONE)

val is_closed = is_none o VCs.get

fun rewrite_vcs f g thy =
  let
    fun rewr (_, (t, _)) = vc_of_term (f thy t)
      |> (fn vc => (vc, (t, thm_of thy vc)))
  in VCs.map (Option.map (fn (vcs, _) => (Symtab.map rewr vcs, g))) thy end

end