1.1 --- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Mon Mar 22 09:40:11 2010 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Mon Mar 22 09:46:04 2010 +0100
     1.3 @@ -27,6 +27,9 @@
     1.4    val state_of_vc: theory -> string -> string list * string list
     1.5    val close: theory -> theory
     1.6    val is_closed: theory -> bool
     1.7 +
     1.8 +  val rewrite_vcs: (theory -> term -> term) -> (theory -> thm -> thm) ->
     1.9 +    theory -> theory
    1.10  end
    1.11  
    1.12  structure Boogie_VCs: BOOGIE_VCS =
    1.13 @@ -252,30 +255,35 @@
    1.14  
    1.15  (* the VC store *)
    1.16  
    1.17 -fun err_vcs () = error "undischarged Boogie verification conditions found"
    1.18 +fun err_unfinished () = error "An unfinished Boogie environment is still open."
    1.19 +
    1.20 +fun err_vcs names = error (Pretty.string_of
    1.21 +  (Pretty.big_list "Undischarged Boogie verification conditions found:"
    1.22 +    (map Pretty.str names)))
    1.23  
    1.24  structure VCs = Theory_Data
    1.25  (
    1.26 -  type T = (vc * thm) Symtab.table option
    1.27 +  type T = ((vc * (term * thm)) Symtab.table * (theory -> thm -> thm)) option
    1.28    val empty = NONE
    1.29    val extend = I
    1.30    fun merge (NONE, NONE) = NONE
    1.31 -    | merge _ = err_vcs ()
    1.32 +    | merge _ = err_unfinished ()
    1.33  )
    1.34  
    1.35 -fun prep thy t = vc_of_term t |> (fn vc => (vc, thm_of thy vc))
    1.36 +fun prep thy = vc_of_term #> (fn vc => (vc, (prop_of_vc vc, thm_of thy vc)))
    1.37  
    1.38  fun set vcs thy = VCs.map (fn
    1.39 -    NONE => SOME (Symtab.make (map (apsnd (prep thy)) vcs))
    1.40 -  | SOME _ => err_vcs ()) thy
    1.41 +    NONE => SOME (Symtab.make (map (apsnd (prep thy)) vcs), K I)
    1.42 +  | SOME _ => err_unfinished ()) thy
    1.43  
    1.44  fun lookup thy name =
    1.45    (case VCs.get thy of
    1.46 -    SOME vcs => Option.map fst (Symtab.lookup vcs name)
    1.47 +    SOME (vcs, _) => Option.map fst (Symtab.lookup vcs name)
    1.48    | NONE => NONE)
    1.49  
    1.50  fun discharge (name, prf) =
    1.51 -  VCs.map (Option.map (Symtab.map_entry name (join prf)))
    1.52 +  let fun jn (vc, (t, thm)) = join prf (vc, thm) |> apsnd (pair t)
    1.53 +  in VCs.map (Option.map (apfst (Symtab.map_entry name jn))) end
    1.54  
    1.55  datatype state = Proved | NotProved | PartiallyProved
    1.56  
    1.57 @@ -284,21 +292,35 @@
    1.58      SOME vc => names_of vc
    1.59    | NONE => ([], []))
    1.60  
    1.61 +fun state_of_vc' (vc, _) =
    1.62 +  (case names_of vc of
    1.63 +    ([], _) => Proved
    1.64 +  | (_, []) => NotProved
    1.65 +  | (_, _) => PartiallyProved)
    1.66 +
    1.67  fun state_of thy =
    1.68    (case VCs.get thy of
    1.69 -    SOME vcs => Symtab.dest vcs |> map (apsnd (fst #> names_of #> (fn
    1.70 -        ([], _) => Proved
    1.71 -      | (_, []) => NotProved
    1.72 -      | (_, _) => PartiallyProved)))
    1.73 +    SOME (vcs, _) => map (apsnd state_of_vc') (Symtab.dest vcs)
    1.74    | NONE => [])
    1.75  
    1.76 +fun finished g (_, (t, thm)) = Thm.prop_of (g thm) aconv t
    1.77 +
    1.78  fun close thy = thy |> VCs.map (fn
    1.79 -    SOME _ =>
    1.80 -      if forall (fn (_, Proved) => true | _ => false) (state_of thy)
    1.81 -      then NONE
    1.82 -      else err_vcs ()
    1.83 +    SOME (vcs, g) =>
    1.84 +      let fun check vc = state_of_vc' vc = Proved andalso finished (g thy) vc
    1.85 +      in
    1.86 +        Symtab.dest vcs
    1.87 +        |> map_filter (fn (n, vc) => if check vc then NONE else SOME n)
    1.88 +        |> (fn names => if null names then NONE else err_vcs names)
    1.89 +      end
    1.90    | NONE => NONE)
    1.91  
    1.92  val is_closed = is_none o VCs.get
    1.93  
    1.94 +fun rewrite_vcs f g thy =
    1.95 +  let
    1.96 +    fun rewr (_, (t, _)) = vc_of_term (f thy t)
    1.97 +      |> (fn vc => (vc, (t, thm_of thy vc)))
    1.98 +  in VCs.map (Option.map (fn (vcs, _) => (Symtab.map rewr vcs, g))) thy end
    1.99 +
   1.100  end