# HG changeset patch
# User berghofe
# Date 1329750598 -3600
# Node ID 8421b6cf2a333781407e2fb6b759fa4317c1f62b
# Parent  42298c5d33b10f6041b0051cae347596c324af37
Fixed bugs:
- set_env no longer modifies pfuns field in theory data record.
  Instead, a copy of this field is now contained in the env field.
- add_type_def now checks whether type associated with SPARK enumeration
  type is really a datatype with no parameters.
- check_pfuns_types now properly strips off prefixes of proof function names.

diff -r 42298c5d33b1 -r 8421b6cf2a33 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Feb 18 10:35:45 2012 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Feb 20 16:09:58 2012 +0100
@@ -50,6 +50,7 @@
         defs: (binding * thm) list,
         types: fdl_type tab,
         funs: (string list * string) tab,
+        pfuns: ((string list * string) option * term) Symtab.table,
         ids: (term * string) Symtab.table * Name.context,
         proving: bool,
         vcs: (string * thm list option *
@@ -324,7 +325,8 @@
                      case check_enum els' cs of
                        NONE => (thy, tyname)
                      | SOME msg => assoc_ty_err thy T s msg
-                   end));
+                   end)
+          | SOME T => assoc_ty_err thy T s "is not a datatype");
         val cs = map Const (the (Datatype.get_constrs thy' tyname));
       in
         ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
@@ -725,11 +727,14 @@
 
 fun upd_option x y = if is_some x then x else y;
 
+fun unprefix_pfun "" s = s
+  | unprefix_pfun prfx s =
+      let val (prfx', s') = strip_prfx s
+      in if prfx = prfx' then s' else s end;
+
 fun check_pfuns_types thy prfx funs =
   Symtab.map (fn s => fn (optty, t) =>
-   let val optty' = lookup funs
-     (if prfx = "" then s
-      else unprefix (prfx ^ "__") s handle Fail _ => s)
+   let val optty' = lookup funs (unprefix_pfun prfx s)
    in
      (check_pfun_type thy prfx s t optty optty';
       (NONE |> upd_option optty |> upd_option optty', t))
@@ -742,11 +747,15 @@
   (Pretty.big_list "The following verification conditions have not been proved:"
     (map Pretty.str names)))
 
-fun set_env (env as {funs, prefix, ...}) thy = VCs.map (fn
+fun set_env ctxt defs types funs ids vcs path prefix thy = VCs.map (fn
     {pfuns, type_map, env = NONE} =>
-      {pfuns = check_pfuns_types thy prefix funs pfuns,
+      {pfuns = pfuns,
        type_map = type_map,
-       env = SOME env}
+       env = SOME
+         {ctxt = ctxt, defs = defs, types = types, funs = funs,
+          pfuns = check_pfuns_types thy prefix funs pfuns,
+          ids = ids, proving = false, vcs = vcs, path = path,
+          prefix = prefix}}
   | _ => err_unfinished ()) thy;
 
 fun mk_pat s = (case Int.fromString s of
@@ -786,33 +795,44 @@
      (tab, ctxt'))
   end;
 
+fun map_pfuns f {pfuns, type_map, env} =
+  {pfuns = f pfuns, type_map = type_map, env = env}
+
+fun map_pfuns_env f {pfuns, type_map,
+      env = SOME {ctxt, defs, types, funs, pfuns = pfuns_env,
+        ids, proving, vcs, path, prefix}} =
+  if proving then err_unfinished ()
+  else
+    {pfuns = pfuns, type_map = type_map,
+     env = SOME {ctxt = ctxt, defs = defs, types = types, funs = funs,
+       pfuns = f pfuns_env, ids = ids, proving = false, vcs = vcs,
+       path = path, prefix = prefix}};
+
 fun add_proof_fun prep (s, (optty, raw_t)) thy =
-  VCs.map (fn
-      {env = SOME {proving = true, ...}, ...} => err_unfinished ()
-    | {pfuns, type_map, env} =>
-        let
-          val (optty', prfx) = (case env of
-              SOME {funs, prefix, ...} => (lookup funs s, prefix)
-            | NONE => (NONE, ""));
-          val optty'' = NONE |> upd_option optty |> upd_option optty';
-          val t = prep (Option.map (pfun_type thy prfx) optty'') raw_t;
-          val _ = (case fold_aterms (fn u =>
-              if is_Var u orelse is_Free u then insert (op =) u else I) t [] of
-              [] => ()
-            | ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^
-                "\nto be associated with proof function " ^ s ^
-                " contains free variable(s) " ^
-                commas (map (Syntax.string_of_term_global thy) ts)));
-        in
-          (check_pfun_type thy prfx s t optty optty';
-           if is_some optty'' orelse is_none env then
-             {pfuns = Symtab.update_new (s, (optty'', t)) pfuns,
-              type_map = type_map,
-              env = env}
-               handle Symtab.DUP _ => error ("Proof function " ^ s ^
-                 " already associated with function")
-           else error ("Undeclared proof function " ^ s))
-        end) thy;
+  VCs.map (fn data as {env, ...} =>
+    let
+      val (optty', prfx, map_pf) = (case env of
+          SOME {funs, prefix, ...} =>
+            (lookup funs (unprefix_pfun prefix s),
+             prefix, map_pfuns_env)
+        | NONE => (NONE, "", map_pfuns));
+      val optty'' = NONE |> upd_option optty |> upd_option optty';
+      val t = prep (Option.map (pfun_type thy prfx) optty'') raw_t;
+      val _ = (case fold_aterms (fn u =>
+          if is_Var u orelse is_Free u then insert (op =) u else I) t [] of
+          [] => ()
+        | ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^
+            "\nto be associated with proof function " ^ s ^
+            " contains free variable(s) " ^
+            commas (map (Syntax.string_of_term_global thy) ts)));
+    in
+      (check_pfun_type thy prfx s t optty optty';
+       if is_some optty'' orelse is_none env then
+         map_pf (Symtab.update_new (s, (optty'', t))) data
+           handle Symtab.DUP _ => error ("Proof function " ^ s ^
+             " already associated with function")
+       else error ("Undeclared proof function " ^ s))
+    end) thy;
 
 fun add_type (s, T as Type (tyname, Ts)) thy =
       thy |>
@@ -842,7 +862,7 @@
 
 fun lookup_vc thy name =
   (case VCs.get thy of
-    {env = SOME {vcs, types, funs, ids, ctxt, prefix, ...}, pfuns, ...} =>
+    {env = SOME {vcs, types, funs, pfuns, ids, ctxt, prefix, ...}, ...} =>
       (case VCtab.lookup vcs name of
          SOME vc =>
            let val (pfuns', ctxt', ids') =
@@ -852,7 +872,7 @@
   | _ => NONE);
 
 fun get_vcs thy = (case VCs.get thy of
-    {env = SOME {vcs, types, funs, ids, ctxt, defs, prefix, ...}, pfuns, ...} =>
+    {env = SOME {vcs, types, funs, pfuns, ids, ctxt, defs, prefix, ...}, ...} =>
       let val (pfuns', ctxt', ids') =
         declare_missing_pfuns thy prefix funs pfuns vcs ids
       in
@@ -864,11 +884,13 @@
 
 fun mark_proved name thms = VCs.map (fn
     {pfuns, type_map,
-     env = SOME {ctxt, defs, types, funs, ids, vcs, path, prefix, ...}} =>
+     env = SOME {ctxt, defs, types, funs, pfuns = pfuns_env,
+        ids, vcs, path, prefix, ...}} =>
       {pfuns = pfuns,
        type_map = type_map,
        env = SOME {ctxt = ctxt, defs = defs,
-         types = types, funs = funs, ids = ids,
+         types = types, funs = funs, pfuns = pfuns_env,
+         ids = ids,
          proving = true,
          vcs = VCtab.map_entry name (fn (trace, _, ps, cs) =>
            (trace, SOME thms, ps, cs)) vcs,
@@ -1024,8 +1046,7 @@
        Element.Notes ("", [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]
           
   in
-    set_env {ctxt = ctxt, defs = defs', types = types, funs = funs,
-      ids = ids, proving = false, vcs = vcs', path = path, prefix = prfx} thy'
+    set_env ctxt defs' types funs ids vcs' path prfx thy'
   end;
 
 end;