1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML Tue Feb 21 13:15:25 2012 +0100
1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Tue Feb 21 13:19:16 2012 +0100
1.3 @@ -50,6 +50,7 @@
1.4 defs: (binding * thm) list,
1.5 types: fdl_type tab,
1.6 funs: (string list * string) tab,
1.7 + pfuns: ((string list * string) option * term) Symtab.table,
1.8 ids: (term * string) Symtab.table * Name.context,
1.9 proving: bool,
1.10 vcs: (string * thm list option *
1.11 @@ -324,7 +325,8 @@
1.12 case check_enum els' cs of
1.13 NONE => (thy, tyname)
1.14 | SOME msg => assoc_ty_err thy T s msg
1.15 - end));
1.16 + end)
1.17 + | SOME T => assoc_ty_err thy T s "is not a datatype");
1.18 val cs = map Const (the (Datatype.get_constrs thy' tyname));
1.19 in
1.20 ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
1.21 @@ -725,11 +727,14 @@
1.22
1.23 fun upd_option x y = if is_some x then x else y;
1.24
1.25 +fun unprefix_pfun "" s = s
1.26 + | unprefix_pfun prfx s =
1.27 + let val (prfx', s') = strip_prfx s
1.28 + in if prfx = prfx' then s' else s end;
1.29 +
1.30 fun check_pfuns_types thy prfx funs =
1.31 Symtab.map (fn s => fn (optty, t) =>
1.32 - let val optty' = lookup funs
1.33 - (if prfx = "" then s
1.34 - else unprefix (prfx ^ "__") s handle Fail _ => s)
1.35 + let val optty' = lookup funs (unprefix_pfun prfx s)
1.36 in
1.37 (check_pfun_type thy prfx s t optty optty';
1.38 (NONE |> upd_option optty |> upd_option optty', t))
1.39 @@ -742,11 +747,15 @@
1.40 (Pretty.big_list "The following verification conditions have not been proved:"
1.41 (map Pretty.str names)))
1.42
1.43 -fun set_env (env as {funs, prefix, ...}) thy = VCs.map (fn
1.44 +fun set_env ctxt defs types funs ids vcs path prefix thy = VCs.map (fn
1.45 {pfuns, type_map, env = NONE} =>
1.46 - {pfuns = check_pfuns_types thy prefix funs pfuns,
1.47 + {pfuns = pfuns,
1.48 type_map = type_map,
1.49 - env = SOME env}
1.50 + env = SOME
1.51 + {ctxt = ctxt, defs = defs, types = types, funs = funs,
1.52 + pfuns = check_pfuns_types thy prefix funs pfuns,
1.53 + ids = ids, proving = false, vcs = vcs, path = path,
1.54 + prefix = prefix}}
1.55 | _ => err_unfinished ()) thy;
1.56
1.57 fun mk_pat s = (case Int.fromString s of
1.58 @@ -786,33 +795,44 @@
1.59 (tab, ctxt'))
1.60 end;
1.61
1.62 +fun map_pfuns f {pfuns, type_map, env} =
1.63 + {pfuns = f pfuns, type_map = type_map, env = env}
1.64 +
1.65 +fun map_pfuns_env f {pfuns, type_map,
1.66 + env = SOME {ctxt, defs, types, funs, pfuns = pfuns_env,
1.67 + ids, proving, vcs, path, prefix}} =
1.68 + if proving then err_unfinished ()
1.69 + else
1.70 + {pfuns = pfuns, type_map = type_map,
1.71 + env = SOME {ctxt = ctxt, defs = defs, types = types, funs = funs,
1.72 + pfuns = f pfuns_env, ids = ids, proving = false, vcs = vcs,
1.73 + path = path, prefix = prefix}};
1.74 +
1.75 fun add_proof_fun prep (s, (optty, raw_t)) thy =
1.76 - VCs.map (fn
1.77 - {env = SOME {proving = true, ...}, ...} => err_unfinished ()
1.78 - | {pfuns, type_map, env} =>
1.79 - let
1.80 - val (optty', prfx) = (case env of
1.81 - SOME {funs, prefix, ...} => (lookup funs s, prefix)
1.82 - | NONE => (NONE, ""));
1.83 - val optty'' = NONE |> upd_option optty |> upd_option optty';
1.84 - val t = prep (Option.map (pfun_type thy prfx) optty'') raw_t;
1.85 - val _ = (case fold_aterms (fn u =>
1.86 - if is_Var u orelse is_Free u then insert (op =) u else I) t [] of
1.87 - [] => ()
1.88 - | ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^
1.89 - "\nto be associated with proof function " ^ s ^
1.90 - " contains free variable(s) " ^
1.91 - commas (map (Syntax.string_of_term_global thy) ts)));
1.92 - in
1.93 - (check_pfun_type thy prfx s t optty optty';
1.94 - if is_some optty'' orelse is_none env then
1.95 - {pfuns = Symtab.update_new (s, (optty'', t)) pfuns,
1.96 - type_map = type_map,
1.97 - env = env}
1.98 - handle Symtab.DUP _ => error ("Proof function " ^ s ^
1.99 - " already associated with function")
1.100 - else error ("Undeclared proof function " ^ s))
1.101 - end) thy;
1.102 + VCs.map (fn data as {env, ...} =>
1.103 + let
1.104 + val (optty', prfx, map_pf) = (case env of
1.105 + SOME {funs, prefix, ...} =>
1.106 + (lookup funs (unprefix_pfun prefix s),
1.107 + prefix, map_pfuns_env)
1.108 + | NONE => (NONE, "", map_pfuns));
1.109 + val optty'' = NONE |> upd_option optty |> upd_option optty';
1.110 + val t = prep (Option.map (pfun_type thy prfx) optty'') raw_t;
1.111 + val _ = (case fold_aterms (fn u =>
1.112 + if is_Var u orelse is_Free u then insert (op =) u else I) t [] of
1.113 + [] => ()
1.114 + | ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^
1.115 + "\nto be associated with proof function " ^ s ^
1.116 + " contains free variable(s) " ^
1.117 + commas (map (Syntax.string_of_term_global thy) ts)));
1.118 + in
1.119 + (check_pfun_type thy prfx s t optty optty';
1.120 + if is_some optty'' orelse is_none env then
1.121 + map_pf (Symtab.update_new (s, (optty'', t))) data
1.122 + handle Symtab.DUP _ => error ("Proof function " ^ s ^
1.123 + " already associated with function")
1.124 + else error ("Undeclared proof function " ^ s))
1.125 + end) thy;
1.126
1.127 fun add_type (s, T as Type (tyname, Ts)) thy =
1.128 thy |>
1.129 @@ -842,7 +862,7 @@
1.130
1.131 fun lookup_vc thy name =
1.132 (case VCs.get thy of
1.133 - {env = SOME {vcs, types, funs, ids, ctxt, prefix, ...}, pfuns, ...} =>
1.134 + {env = SOME {vcs, types, funs, pfuns, ids, ctxt, prefix, ...}, ...} =>
1.135 (case VCtab.lookup vcs name of
1.136 SOME vc =>
1.137 let val (pfuns', ctxt', ids') =
1.138 @@ -852,7 +872,7 @@
1.139 | _ => NONE);
1.140
1.141 fun get_vcs thy = (case VCs.get thy of
1.142 - {env = SOME {vcs, types, funs, ids, ctxt, defs, prefix, ...}, pfuns, ...} =>
1.143 + {env = SOME {vcs, types, funs, pfuns, ids, ctxt, defs, prefix, ...}, ...} =>
1.144 let val (pfuns', ctxt', ids') =
1.145 declare_missing_pfuns thy prefix funs pfuns vcs ids
1.146 in
1.147 @@ -864,11 +884,13 @@
1.148
1.149 fun mark_proved name thms = VCs.map (fn
1.150 {pfuns, type_map,
1.151 - env = SOME {ctxt, defs, types, funs, ids, vcs, path, prefix, ...}} =>
1.152 + env = SOME {ctxt, defs, types, funs, pfuns = pfuns_env,
1.153 + ids, vcs, path, prefix, ...}} =>
1.154 {pfuns = pfuns,
1.155 type_map = type_map,
1.156 env = SOME {ctxt = ctxt, defs = defs,
1.157 - types = types, funs = funs, ids = ids,
1.158 + types = types, funs = funs, pfuns = pfuns_env,
1.159 + ids = ids,
1.160 proving = true,
1.161 vcs = VCtab.map_entry name (fn (trace, _, ps, cs) =>
1.162 (trace, SOME thms, ps, cs)) vcs,
1.163 @@ -1024,8 +1046,7 @@
1.164 Element.Notes ("", [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]
1.165
1.166 in
1.167 - set_env {ctxt = ctxt, defs = defs', types = types, funs = funs,
1.168 - ids = ids, proving = false, vcs = vcs', path = path, prefix = prfx} thy'
1.169 + set_env ctxt defs' types funs ids vcs' path prfx thy'
1.170 end;
1.171
1.172 end;