1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML Thu Jun 28 09:18:58 2012 +0200
1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Fri Jun 29 09:45:48 2012 +0200
1.3 @@ -13,13 +13,13 @@
1.4 string * ((string list * string) option * 'a) ->
1.5 theory -> theory
1.6 val add_type: string * (typ * (string * string) list) -> theory -> theory
1.7 - val lookup_vc: theory -> string -> (Element.context_i list *
1.8 + val lookup_vc: theory -> bool -> string -> (Element.context_i list *
1.9 (string * thm list option * Element.context_i * Element.statement_i)) option
1.10 - val get_vcs: theory ->
1.11 + val get_vcs: theory -> bool ->
1.12 Element.context_i list * (binding * thm) list * (string *
1.13 (string * thm list option * Element.context_i * Element.statement_i)) list
1.14 val mark_proved: string -> thm list -> theory -> theory
1.15 - val close: theory -> theory
1.16 + val close: bool -> theory -> theory
1.17 val is_closed: theory -> bool
1.18 end;
1.19
1.20 @@ -756,9 +756,23 @@
1.21
1.22 (** the VC store **)
1.23
1.24 -fun err_vcs names = error (Pretty.string_of
1.25 - (Pretty.big_list "The following verification conditions have not been proved:"
1.26 - (map Pretty.str names)))
1.27 +fun pp_vcs msg vcs = Pretty.big_list msg (map (Pretty.str o fst) vcs);
1.28 +
1.29 +fun pp_open_vcs [] = Pretty.str "All verification conditions have been proved."
1.30 + | pp_open_vcs vcs = pp_vcs
1.31 + "The following verification conditions remain to be proved:" vcs;
1.32 +
1.33 +fun partition_vcs vcs = VCtab.fold_rev
1.34 + (fn (name, (trace, SOME thms, ps, cs)) =>
1.35 + apfst (cons (name, (trace, thms, ps, cs)))
1.36 + | (name, (trace, NONE, ps, cs)) =>
1.37 + apsnd (cons (name, (trace, ps, cs))))
1.38 + vcs ([], []);
1.39 +
1.40 +fun insert_break prt = Pretty.blk (0, [Pretty.fbrk, prt]);
1.41 +
1.42 +fun print_open_vcs f vcs =
1.43 + (Pretty.writeln (f (pp_open_vcs (snd (partition_vcs vcs)))); vcs);
1.44
1.45 fun set_env ctxt defs types funs ids vcs path prefix thy = VCs.map (fn
1.46 {pfuns, type_map, env = NONE} =>
1.47 @@ -767,7 +781,7 @@
1.48 env = SOME
1.49 {ctxt = ctxt, defs = defs, types = types, funs = funs,
1.50 pfuns = check_pfuns_types thy prefix funs pfuns,
1.51 - ids = ids, proving = false, vcs = vcs, path = path,
1.52 + ids = ids, proving = false, vcs = print_open_vcs I vcs, path = path,
1.53 prefix = prefix}}
1.54 | _ => err_unfinished ()) thy;
1.55
1.56 @@ -775,7 +789,7 @@
1.57 SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))]
1.58 | NONE => error ("Bad conclusion identifier: C" ^ s));
1.59
1.60 -fun mk_vc thy prfx types pfuns ids (tr, proved, ps, cs) =
1.61 +fun mk_vc thy prfx types pfuns ids name_concl (tr, proved, ps, cs) =
1.62 let val prop_of =
1.63 HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids
1.64 in
1.65 @@ -783,7 +797,9 @@
1.66 Element.Assumes (map (fn (s', e) =>
1.67 ((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps),
1.68 Element.Shows (map (fn (s', e) =>
1.69 - (Attrib.empty_binding, [(prop_of e, mk_pat s')])) cs))
1.70 + (if name_concl then (Binding.name ("C" ^ s'), [])
1.71 + else Attrib.empty_binding,
1.72 + [(prop_of e, mk_pat s')])) cs))
1.73 end;
1.74
1.75 fun fold_vcs f vcs =
1.76 @@ -898,25 +914,28 @@
1.77
1.78 val is_closed = is_none o #env o VCs.get;
1.79
1.80 -fun lookup_vc thy name =
1.81 +fun lookup_vc thy name_concl name =
1.82 (case VCs.get thy of
1.83 {env = SOME {vcs, types, funs, pfuns, ids, ctxt, prefix, ...}, ...} =>
1.84 (case VCtab.lookup vcs name of
1.85 SOME vc =>
1.86 let val (pfuns', ctxt', ids') =
1.87 declare_missing_pfuns thy prefix funs pfuns vcs ids
1.88 - in SOME (ctxt @ [ctxt'], mk_vc thy prefix types pfuns' ids' vc) end
1.89 + in
1.90 + SOME (ctxt @ [ctxt'],
1.91 + mk_vc thy prefix types pfuns' ids' name_concl vc)
1.92 + end
1.93 | NONE => NONE)
1.94 | _ => NONE);
1.95
1.96 -fun get_vcs thy = (case VCs.get thy of
1.97 +fun get_vcs thy name_concl = (case VCs.get thy of
1.98 {env = SOME {vcs, types, funs, pfuns, ids, ctxt, defs, prefix, ...}, ...} =>
1.99 let val (pfuns', ctxt', ids') =
1.100 declare_missing_pfuns thy prefix funs pfuns vcs ids
1.101 in
1.102 (ctxt @ [ctxt'], defs,
1.103 VCtab.dest vcs |>
1.104 - map (apsnd (mk_vc thy prefix types pfuns' ids')))
1.105 + map (apsnd (mk_vc thy prefix types pfuns' ids' name_concl)))
1.106 end
1.107 | _ => ([], [], []));
1.108
1.109 @@ -930,25 +949,34 @@
1.110 types = types, funs = funs, pfuns = pfuns_env,
1.111 ids = ids,
1.112 proving = true,
1.113 - vcs = VCtab.map_entry name (fn (trace, _, ps, cs) =>
1.114 - (trace, SOME thms, ps, cs)) vcs,
1.115 + vcs = print_open_vcs insert_break (VCtab.map_entry name
1.116 + (fn (trace, _, ps, cs) => (trace, SOME thms, ps, cs)) vcs),
1.117 path = path,
1.118 prefix = prefix}}
1.119 | x => x);
1.120
1.121 -fun close thy =
1.122 +fun close incomplete thy =
1.123 thy |>
1.124 VCs.map (fn
1.125 {pfuns, type_map, env = SOME {vcs, path, ...}} =>
1.126 - (case VCtab.fold_rev (fn vc as (_, (_, p, _, _)) =>
1.127 - (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of
1.128 - (proved, []) =>
1.129 - (Thm.join_proofs (maps (the o #2 o snd) proved);
1.130 - File.write (Path.ext "prv" path)
1.131 - (implode (map (fn (s, _) => snd (strip_number s) ^
1.132 - " -- proved by " ^ Distribution.version ^ "\n") proved));
1.133 - {pfuns = pfuns, type_map = type_map, env = NONE})
1.134 - | (_, unproved) => err_vcs (map fst unproved))
1.135 + let
1.136 + val (proved, unproved) = partition_vcs vcs;
1.137 + val _ = Thm.join_proofs (maps (#2 o snd) proved);
1.138 + val (proved', proved'') = List.partition (fn (_, (_, thms, _, _)) =>
1.139 + exists (#oracle o Thm.status_of) thms) proved
1.140 + in
1.141 + (if null unproved then ()
1.142 + else (if incomplete then warning else error)
1.143 + (Pretty.string_of (pp_open_vcs unproved));
1.144 + if null proved' then ()
1.145 + else warning (Pretty.string_of (pp_vcs
1.146 + "The following VCs are not marked as proved \
1.147 + \because their proofs contain oracles:" proved'));
1.148 + File.write (Path.ext "prv" path)
1.149 + (implode (map (fn (s, _) => snd (strip_number s) ^
1.150 + " -- proved by " ^ Distribution.version ^ "\n") proved''));
1.151 + {pfuns = pfuns, type_map = type_map, env = NONE})
1.152 + end
1.153 | _ => error "No SPARK environment is currently open") |>
1.154 Sign.parent_path;
1.155