Properly treat proof functions with no arguments.
1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML Wed Apr 27 13:21:12 2011 +0200
1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Wed Apr 27 19:27:06 2011 +0200
1.3 @@ -440,7 +440,9 @@
1.4 | tm_of (tab, _) (Ident s) =
1.5 (case Symtab.lookup tab s of
1.6 SOME t_ty => t_ty
1.7 - | NONE => error ("Undeclared identifier " ^ s))
1.8 + | NONE => (case lookup_prfx prfx pfuns s of
1.9 + SOME (SOME ([], resty), t) => (t, resty)
1.10 + | _ => error ("Undeclared identifier " ^ s)))
1.11
1.12 | tm_of _ (Number i) = (HOLogic.mk_number HOLogic.intT i, integerN)
1.13
1.14 @@ -696,8 +698,9 @@
1.15 (fold_expr f g) (fold_opt (fold_expr f g)))))
1.16 (fold_expr f g)) assocs;
1.17
1.18 -val add_expr_pfuns = fold_expr
1.19 - (fn s => if is_pfun s then I else insert (op =) s) (K I);
1.20 +fun add_expr_pfuns funs = fold_expr
1.21 + (fn s => if is_pfun s then I else insert (op =) s)
1.22 + (fn s => if is_none (lookup funs s) then I else insert (op =) s);
1.23
1.24 val add_expr_idents = fold_expr (K I) (insert (op =));
1.25
1.26 @@ -765,14 +768,14 @@
1.27 fun fold_vcs f vcs =
1.28 VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs;
1.29
1.30 -fun pfuns_of_vcs prfx pfuns vcs =
1.31 - fold_vcs (add_expr_pfuns o snd) vcs [] |>
1.32 +fun pfuns_of_vcs prfx funs pfuns vcs =
1.33 + fold_vcs (add_expr_pfuns funs o snd) vcs [] |>
1.34 filter (is_none o lookup_prfx prfx pfuns);
1.35
1.36 fun declare_missing_pfuns thy prfx funs pfuns vcs (tab, ctxt) =
1.37 let
1.38 val (fs, (tys, Ts)) =
1.39 - pfuns_of_vcs prfx pfuns vcs |>
1.40 + pfuns_of_vcs prfx funs pfuns vcs |>
1.41 map_filter (fn s => lookup funs s |>
1.42 Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |>
1.43 split_list ||> split_list;
1.44 @@ -963,15 +966,16 @@
1.45 (map (fn ((s, i), _) => s ^ "(" ^ string_of_int i ^ ")") rules);
1.46
1.47 (* sort definitions according to their dependency *)
1.48 -fun sort_defs _ _ _ [] sdefs = rev sdefs
1.49 - | sort_defs prfx pfuns consts defs sdefs =
1.50 +fun sort_defs _ _ _ _ [] sdefs = rev sdefs
1.51 + | sort_defs prfx funs pfuns consts defs sdefs =
1.52 (case find_first (fn (_, (_, e)) =>
1.53 - forall (is_some o lookup_prfx prfx pfuns) (add_expr_pfuns e []) andalso
1.54 + forall (is_some o lookup_prfx prfx pfuns)
1.55 + (add_expr_pfuns funs e []) andalso
1.56 forall (fn id =>
1.57 member (fn (s, (_, (s', _))) => s = s') sdefs id orelse
1.58 consts id)
1.59 (add_expr_idents e [])) defs of
1.60 - SOME d => sort_defs prfx pfuns consts
1.61 + SOME d => sort_defs prfx funs pfuns consts
1.62 (remove (op =) d defs) (d :: sdefs)
1.63 | NONE => error ("Bad definitions: " ^ rulenames defs));
1.64
1.65 @@ -993,7 +997,7 @@
1.66 (filter_out (is_trivial_vc o snd) vcs)) vcs);
1.67
1.68 val _ = (case filter_out (is_some o lookup funs)
1.69 - (pfuns_of_vcs prfx pfuns vcs') of
1.70 + (pfuns_of_vcs prfx funs pfuns vcs') of
1.71 [] => ()
1.72 | fs => error ("Undeclared proof function(s) " ^ commas fs));
1.73
1.74 @@ -1007,7 +1011,7 @@
1.75 fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>
1.76 ids_thy |>
1.77 fold_map (add_def prfx types pfuns consts)
1.78 - (sort_defs prfx pfuns (Symtab.defined tab) defs []) ||>>
1.79 + (sort_defs prfx funs pfuns (Symtab.defined tab) defs []) ||>>
1.80 fold_map (add_var prfx) (items vars) ||>>
1.81 add_init_vars prfx vcs');
1.82