equal
deleted
inserted
replaced
17 structure Boogie_VCs: BOOGIE_VCS = |
17 structure Boogie_VCs: BOOGIE_VCS = |
18 struct |
18 struct |
19 |
19 |
20 fun err_vcs () = error "undischarged Boogie verification conditions found" |
20 fun err_vcs () = error "undischarged Boogie verification conditions found" |
21 |
21 |
22 structure VCs = TheoryDataFun |
22 structure VCs = Theory_Data |
23 ( |
23 ( |
24 type T = (Term.term * bool) Symtab.table option |
24 type T = (term * bool) Symtab.table option |
25 val empty = NONE |
25 val empty = NONE |
26 val copy = I |
|
27 val extend = I |
26 val extend = I |
28 fun merge _ (NONE, NONE) = NONE |
27 fun merge (NONE, NONE) = NONE |
29 | merge _ (_, _) = err_vcs () |
28 | merge _ = err_vcs () |
30 ) |
29 ) |
31 |
30 |
32 fun set vcs = VCs.map (fn |
31 fun set vcs = VCs.map (fn |
33 NONE => SOME (Symtab.make (map (apsnd (rpair false)) vcs)) |
32 NONE => SOME (Symtab.make (map (apsnd (rpair false)) vcs)) |
34 | SOME _ => err_vcs ()) |
33 | SOME _ => err_vcs ()) |