1.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML Thu Jun 28 09:18:58 2012 +0200
1.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML Fri Jun 29 09:45:48 2012 +0200
1.3 @@ -44,7 +44,7 @@
1.4 SPARK_VCs.add_type (s, (Syntax.read_typ_global thy raw_typ, cmap)) thy;
1.5
1.6 fun get_vc thy vc_name =
1.7 - (case SPARK_VCs.lookup_vc thy vc_name of
1.8 + (case SPARK_VCs.lookup_vc thy false vc_name of
1.9 SOME (ctxt, (_, proved, ctxt', stmt)) =>
1.10 if is_some proved then
1.11 error ("The verification condition " ^
1.12 @@ -71,7 +71,7 @@
1.13 let
1.14 val thy = Toplevel.theory_of state;
1.15
1.16 - val (context, defs, vcs) = SPARK_VCs.get_vcs thy;
1.17 + val (context, defs, vcs) = SPARK_VCs.get_vcs thy true;
1.18
1.19 val vcs' = AList.coalesce (op =) (map_filter
1.20 (fn (name, (trace, status, ctxt, stmt)) =>
1.21 @@ -144,7 +144,9 @@
1.22 val _ =
1.23 Outer_Syntax.command @{command_spec "spark_end"}
1.24 "close the current SPARK environment"
1.25 - (Scan.succeed (Toplevel.theory SPARK_VCs.close));
1.26 + (Scan.optional (@{keyword "("} |-- Parse.!!!
1.27 + (Parse.reserved "incomplete" --| @{keyword ")"}) >> K true) false >>
1.28 + (Toplevel.theory o SPARK_VCs.close));
1.29
1.30 val setup = Theory.at_end (fn thy =>
1.31 let
2.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML Thu Jun 28 09:18:58 2012 +0200
2.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Fri Jun 29 09:45:48 2012 +0200
2.3 @@ -13,13 +13,13 @@
2.4 string * ((string list * string) option * 'a) ->
2.5 theory -> theory
2.6 val add_type: string * (typ * (string * string) list) -> theory -> theory
2.7 - val lookup_vc: theory -> string -> (Element.context_i list *
2.8 + val lookup_vc: theory -> bool -> string -> (Element.context_i list *
2.9 (string * thm list option * Element.context_i * Element.statement_i)) option
2.10 - val get_vcs: theory ->
2.11 + val get_vcs: theory -> bool ->
2.12 Element.context_i list * (binding * thm) list * (string *
2.13 (string * thm list option * Element.context_i * Element.statement_i)) list
2.14 val mark_proved: string -> thm list -> theory -> theory
2.15 - val close: theory -> theory
2.16 + val close: bool -> theory -> theory
2.17 val is_closed: theory -> bool
2.18 end;
2.19
2.20 @@ -756,9 +756,23 @@
2.21
2.22 (** the VC store **)
2.23
2.24 -fun err_vcs names = error (Pretty.string_of
2.25 - (Pretty.big_list "The following verification conditions have not been proved:"
2.26 - (map Pretty.str names)))
2.27 +fun pp_vcs msg vcs = Pretty.big_list msg (map (Pretty.str o fst) vcs);
2.28 +
2.29 +fun pp_open_vcs [] = Pretty.str "All verification conditions have been proved."
2.30 + | pp_open_vcs vcs = pp_vcs
2.31 + "The following verification conditions remain to be proved:" vcs;
2.32 +
2.33 +fun partition_vcs vcs = VCtab.fold_rev
2.34 + (fn (name, (trace, SOME thms, ps, cs)) =>
2.35 + apfst (cons (name, (trace, thms, ps, cs)))
2.36 + | (name, (trace, NONE, ps, cs)) =>
2.37 + apsnd (cons (name, (trace, ps, cs))))
2.38 + vcs ([], []);
2.39 +
2.40 +fun insert_break prt = Pretty.blk (0, [Pretty.fbrk, prt]);
2.41 +
2.42 +fun print_open_vcs f vcs =
2.43 + (Pretty.writeln (f (pp_open_vcs (snd (partition_vcs vcs)))); vcs);
2.44
2.45 fun set_env ctxt defs types funs ids vcs path prefix thy = VCs.map (fn
2.46 {pfuns, type_map, env = NONE} =>
2.47 @@ -767,7 +781,7 @@
2.48 env = SOME
2.49 {ctxt = ctxt, defs = defs, types = types, funs = funs,
2.50 pfuns = check_pfuns_types thy prefix funs pfuns,
2.51 - ids = ids, proving = false, vcs = vcs, path = path,
2.52 + ids = ids, proving = false, vcs = print_open_vcs I vcs, path = path,
2.53 prefix = prefix}}
2.54 | _ => err_unfinished ()) thy;
2.55
2.56 @@ -775,7 +789,7 @@
2.57 SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))]
2.58 | NONE => error ("Bad conclusion identifier: C" ^ s));
2.59
2.60 -fun mk_vc thy prfx types pfuns ids (tr, proved, ps, cs) =
2.61 +fun mk_vc thy prfx types pfuns ids name_concl (tr, proved, ps, cs) =
2.62 let val prop_of =
2.63 HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids
2.64 in
2.65 @@ -783,7 +797,9 @@
2.66 Element.Assumes (map (fn (s', e) =>
2.67 ((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps),
2.68 Element.Shows (map (fn (s', e) =>
2.69 - (Attrib.empty_binding, [(prop_of e, mk_pat s')])) cs))
2.70 + (if name_concl then (Binding.name ("C" ^ s'), [])
2.71 + else Attrib.empty_binding,
2.72 + [(prop_of e, mk_pat s')])) cs))
2.73 end;
2.74
2.75 fun fold_vcs f vcs =
2.76 @@ -898,25 +914,28 @@
2.77
2.78 val is_closed = is_none o #env o VCs.get;
2.79
2.80 -fun lookup_vc thy name =
2.81 +fun lookup_vc thy name_concl name =
2.82 (case VCs.get thy of
2.83 {env = SOME {vcs, types, funs, pfuns, ids, ctxt, prefix, ...}, ...} =>
2.84 (case VCtab.lookup vcs name of
2.85 SOME vc =>
2.86 let val (pfuns', ctxt', ids') =
2.87 declare_missing_pfuns thy prefix funs pfuns vcs ids
2.88 - in SOME (ctxt @ [ctxt'], mk_vc thy prefix types pfuns' ids' vc) end
2.89 + in
2.90 + SOME (ctxt @ [ctxt'],
2.91 + mk_vc thy prefix types pfuns' ids' name_concl vc)
2.92 + end
2.93 | NONE => NONE)
2.94 | _ => NONE);
2.95
2.96 -fun get_vcs thy = (case VCs.get thy of
2.97 +fun get_vcs thy name_concl = (case VCs.get thy of
2.98 {env = SOME {vcs, types, funs, pfuns, ids, ctxt, defs, prefix, ...}, ...} =>
2.99 let val (pfuns', ctxt', ids') =
2.100 declare_missing_pfuns thy prefix funs pfuns vcs ids
2.101 in
2.102 (ctxt @ [ctxt'], defs,
2.103 VCtab.dest vcs |>
2.104 - map (apsnd (mk_vc thy prefix types pfuns' ids')))
2.105 + map (apsnd (mk_vc thy prefix types pfuns' ids' name_concl)))
2.106 end
2.107 | _ => ([], [], []));
2.108
2.109 @@ -930,25 +949,34 @@
2.110 types = types, funs = funs, pfuns = pfuns_env,
2.111 ids = ids,
2.112 proving = true,
2.113 - vcs = VCtab.map_entry name (fn (trace, _, ps, cs) =>
2.114 - (trace, SOME thms, ps, cs)) vcs,
2.115 + vcs = print_open_vcs insert_break (VCtab.map_entry name
2.116 + (fn (trace, _, ps, cs) => (trace, SOME thms, ps, cs)) vcs),
2.117 path = path,
2.118 prefix = prefix}}
2.119 | x => x);
2.120
2.121 -fun close thy =
2.122 +fun close incomplete thy =
2.123 thy |>
2.124 VCs.map (fn
2.125 {pfuns, type_map, env = SOME {vcs, path, ...}} =>
2.126 - (case VCtab.fold_rev (fn vc as (_, (_, p, _, _)) =>
2.127 - (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of
2.128 - (proved, []) =>
2.129 - (Thm.join_proofs (maps (the o #2 o snd) proved);
2.130 - File.write (Path.ext "prv" path)
2.131 - (implode (map (fn (s, _) => snd (strip_number s) ^
2.132 - " -- proved by " ^ Distribution.version ^ "\n") proved));
2.133 - {pfuns = pfuns, type_map = type_map, env = NONE})
2.134 - | (_, unproved) => err_vcs (map fst unproved))
2.135 + let
2.136 + val (proved, unproved) = partition_vcs vcs;
2.137 + val _ = Thm.join_proofs (maps (#2 o snd) proved);
2.138 + val (proved', proved'') = List.partition (fn (_, (_, thms, _, _)) =>
2.139 + exists (#oracle o Thm.status_of) thms) proved
2.140 + in
2.141 + (if null unproved then ()
2.142 + else (if incomplete then warning else error)
2.143 + (Pretty.string_of (pp_open_vcs unproved));
2.144 + if null proved' then ()
2.145 + else warning (Pretty.string_of (pp_vcs
2.146 + "The following VCs are not marked as proved \
2.147 + \because their proofs contain oracles:" proved'));
2.148 + File.write (Path.ext "prv" path)
2.149 + (implode (map (fn (s, _) => snd (strip_number s) ^
2.150 + " -- proved by " ^ Distribution.version ^ "\n") proved''));
2.151 + {pfuns = pfuns, type_map = type_map, env = NONE})
2.152 + end
2.153 | _ => error "No SPARK environment is currently open") |>
2.154 Sign.parent_path;
2.155