1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Sat Jan 15 12:35:29 2011 +0100
1.3 @@ -0,0 +1,870 @@
1.4 +(* Title: HOL/SPARK/Tools/spark_vcs.ML
1.5 + Author: Stefan Berghofer
1.6 + Copyright: secunet Security Networks AG
1.7 +
1.8 +Store for verification conditions generated by SPARK/Ada.
1.9 +*)
1.10 +
1.11 +signature SPARK_VCS =
1.12 +sig
1.13 + val set_vcs: Fdl_Parser.decls -> Fdl_Parser.rules -> Fdl_Parser.vcs ->
1.14 + Path.T -> theory -> theory
1.15 + val add_proof_fun: (typ option -> 'a -> term) ->
1.16 + string * ((string list * string) option * 'a) ->
1.17 + theory -> theory
1.18 + val lookup_vc: theory -> string -> (Element.context_i list *
1.19 + (string * bool * Element.context_i * Element.statement_i)) option
1.20 + val get_vcs: theory ->
1.21 + Element.context_i list * (binding * thm) list *
1.22 + (string * (string * bool * Element.context_i * Element.statement_i)) list
1.23 + val mark_proved: string -> theory -> theory
1.24 + val close: theory -> theory
1.25 + val is_closed: theory -> bool
1.26 +end;
1.27 +
1.28 +structure SPARK_VCs: SPARK_VCS =
1.29 +struct
1.30 +
1.31 +open Fdl_Parser;
1.32 +
1.33 +
1.34 +(** utilities **)
1.35 +
1.36 +fun mk_unop s t =
1.37 + let val T = fastype_of t
1.38 + in Const (s, T --> T) $ t end;
1.39 +
1.40 +fun mk_times (t, u) =
1.41 + let
1.42 + val setT = fastype_of t;
1.43 + val T = HOLogic.dest_setT setT;
1.44 + val U = HOLogic.dest_setT (fastype_of u)
1.45 + in
1.46 + Const (@{const_name Sigma}, setT --> (T --> HOLogic.mk_setT U) -->
1.47 + HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)
1.48 + end;
1.49 +
1.50 +fun mk_type _ "integer" = HOLogic.intT
1.51 + | mk_type _ "boolean" = HOLogic.boolT
1.52 + | mk_type thy ty = Syntax.check_typ (ProofContext.init_global thy)
1.53 + (Type (Sign.full_name thy (Binding.name ty), []));
1.54 +
1.55 +val booleanN = "boolean";
1.56 +val integerN = "integer";
1.57 +
1.58 +fun mk_qual_name thy s s' =
1.59 + Sign.full_name thy (Binding.qualify true s (Binding.name s'));
1.60 +
1.61 +fun define_overloaded (def_name, eq) lthy =
1.62 + let
1.63 + val ((c, _), rhs) = eq |> Syntax.check_term lthy |>
1.64 + Logic.dest_equals |>> dest_Free;
1.65 + val ((_, (_, thm)), lthy') = Local_Theory.define
1.66 + ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs)) lthy
1.67 + val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy');
1.68 + val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm
1.69 + in (thm', lthy') end;
1.70 +
1.71 +fun strip_underscores s =
1.72 + strip_underscores (unsuffix "_" s) handle Fail _ => s;
1.73 +
1.74 +fun strip_tilde s =
1.75 + unsuffix "~" s ^ "_init" handle Fail _ => s;
1.76 +
1.77 +val mangle_name = strip_underscores #> strip_tilde;
1.78 +
1.79 +fun mk_variables thy xs ty (tab, ctxt) =
1.80 + let
1.81 + val T = mk_type thy ty;
1.82 + val (ys, ctxt') = Name.variants (map mangle_name xs) ctxt;
1.83 + val zs = map (Free o rpair T) ys;
1.84 + in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
1.85 +
1.86 +
1.87 +(** generate properties of enumeration types **)
1.88 +
1.89 +fun add_enum_type tyname els (tab, ctxt) thy =
1.90 + let
1.91 + val tyb = Binding.name tyname;
1.92 + val tyname' = Sign.full_name thy tyb;
1.93 + val T = Type (tyname', []);
1.94 + val case_name = mk_qual_name thy tyname (tyname ^ "_case");
1.95 + val cs = map (fn s => Const (mk_qual_name thy tyname s, T)) els;
1.96 + val k = length els;
1.97 + val p = Const (@{const_name pos}, T --> HOLogic.intT);
1.98 + val v = Const (@{const_name val}, HOLogic.intT --> T);
1.99 + val card = Const (@{const_name card},
1.100 + HOLogic.mk_setT T --> HOLogic.natT) $ HOLogic.mk_UNIV T;
1.101 +
1.102 + fun mk_binrel_def s f = Logic.mk_equals
1.103 + (Const (s, T --> T --> HOLogic.boolT),
1.104 + Abs ("x", T, Abs ("y", T,
1.105 + Const (s, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $
1.106 + (f $ Bound 1) $ (f $ Bound 0))));
1.107 +
1.108 + val (((def1, def2), def3), lthy) = thy |>
1.109 + Datatype.add_datatype {strict = true, quiet = true} [tyname]
1.110 + [([], tyb, NoSyn,
1.111 + map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
1.112 +
1.113 + Class.instantiation ([tyname'], [], @{sort enum}) |>
1.114 +
1.115 + define_overloaded ("pos_" ^ tyname ^ "_def", Logic.mk_equals
1.116 + (p,
1.117 + list_comb (Const (case_name, replicate k HOLogic.intT @
1.118 + [T] ---> HOLogic.intT),
1.119 + map (HOLogic.mk_number HOLogic.intT) (0 upto k - 1)))) ||>>
1.120 +
1.121 + define_overloaded ("less_eq_" ^ tyname ^ "_def",
1.122 + mk_binrel_def @{const_name less_eq} p) ||>>
1.123 + define_overloaded ("less_" ^ tyname ^ "_def",
1.124 + mk_binrel_def @{const_name less} p);
1.125 +
1.126 + val UNIV_eq = Goal.prove lthy [] []
1.127 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
1.128 + (HOLogic.mk_UNIV T, HOLogic.mk_set T cs)))
1.129 + (fn _ =>
1.130 + rtac @{thm subset_antisym} 1 THEN
1.131 + rtac @{thm subsetI} 1 THEN
1.132 + Datatype_Aux.exh_tac (K (#exhaust (Datatype_Data.the_info
1.133 + (ProofContext.theory_of lthy) tyname'))) 1 THEN
1.134 + ALLGOALS (asm_full_simp_tac (simpset_of lthy)));
1.135 +
1.136 + val finite_UNIV = Goal.prove lthy [] []
1.137 + (HOLogic.mk_Trueprop (Const (@{const_name finite},
1.138 + HOLogic.mk_setT T --> HOLogic.boolT) $ HOLogic.mk_UNIV T))
1.139 + (fn _ => simp_tac (simpset_of lthy addsimps [UNIV_eq]) 1);
1.140 +
1.141 + val card_UNIV = Goal.prove lthy [] []
1.142 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
1.143 + (card, HOLogic.mk_number HOLogic.natT k)))
1.144 + (fn _ => simp_tac (simpset_of lthy addsimps [UNIV_eq]) 1);
1.145 +
1.146 + val range_pos = Goal.prove lthy [] []
1.147 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
1.148 + (Const (@{const_name image}, (T --> HOLogic.intT) -->
1.149 + HOLogic.mk_setT T --> HOLogic.mk_setT HOLogic.intT) $
1.150 + p $ HOLogic.mk_UNIV T,
1.151 + Const (@{const_name atLeastLessThan}, HOLogic.intT -->
1.152 + HOLogic.intT --> HOLogic.mk_setT HOLogic.intT) $
1.153 + HOLogic.mk_number HOLogic.intT 0 $
1.154 + (@{term int} $ card))))
1.155 + (fn _ =>
1.156 + simp_tac (simpset_of lthy addsimps [card_UNIV]) 1 THEN
1.157 + simp_tac (simpset_of lthy addsimps [UNIV_eq, def1]) 1 THEN
1.158 + rtac @{thm subset_antisym} 1 THEN
1.159 + simp_tac (simpset_of lthy) 1 THEN
1.160 + rtac @{thm subsetI} 1 THEN
1.161 + asm_full_simp_tac (simpset_of lthy addsimps @{thms interval_expand}
1.162 + delsimps @{thms atLeastLessThan_iff}) 1);
1.163 +
1.164 + val lthy' =
1.165 + Class.prove_instantiation_instance (fn _ =>
1.166 + Class.intro_classes_tac [] THEN
1.167 + rtac finite_UNIV 1 THEN
1.168 + rtac range_pos 1 THEN
1.169 + simp_tac (HOL_basic_ss addsimps [def3]) 1 THEN
1.170 + simp_tac (HOL_basic_ss addsimps [def2]) 1) lthy;
1.171 +
1.172 + val (pos_eqs, val_eqs) = split_list (map_index (fn (i, c) =>
1.173 + let
1.174 + val n = HOLogic.mk_number HOLogic.intT i;
1.175 + val th = Goal.prove lthy' [] []
1.176 + (HOLogic.mk_Trueprop (HOLogic.mk_eq (p $ c, n)))
1.177 + (fn _ => simp_tac (simpset_of lthy' addsimps [def1]) 1);
1.178 + val th' = Goal.prove lthy' [] []
1.179 + (HOLogic.mk_Trueprop (HOLogic.mk_eq (v $ n, c)))
1.180 + (fn _ =>
1.181 + rtac (@{thm inj_pos} RS @{thm injD}) 1 THEN
1.182 + simp_tac (simpset_of lthy' addsimps
1.183 + [@{thm pos_val}, range_pos, card_UNIV, th]) 1)
1.184 + in (th, th') end) cs);
1.185 +
1.186 + val first_el = Goal.prove lthy' [] []
1.187 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
1.188 + (Const (@{const_name first_el}, T), hd cs)))
1.189 + (fn _ => simp_tac (simpset_of lthy' addsimps
1.190 + [@{thm first_el_def}, hd val_eqs]) 1);
1.191 +
1.192 + val last_el = Goal.prove lthy' [] []
1.193 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
1.194 + (Const (@{const_name last_el}, T), List.last cs)))
1.195 + (fn _ => simp_tac (simpset_of lthy' addsimps
1.196 + [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1);
1.197 +
1.198 + val simp_att = [Attrib.internal (K Simplifier.simp_add)]
1.199 +
1.200 + in
1.201 + ((fold (Symtab.update_new o apsnd (rpair tyname)) (els ~~ cs) tab,
1.202 + fold Name.declare els ctxt),
1.203 + lthy' |>
1.204 + Local_Theory.note
1.205 + ((Binding.name (tyname ^ "_card_UNIV"), simp_att), [card_UNIV]) ||>>
1.206 + Local_Theory.note
1.207 + ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>>
1.208 + Local_Theory.note
1.209 + ((Binding.name (tyname ^ "_val"), simp_att), val_eqs) ||>>
1.210 + Local_Theory.note
1.211 + ((Binding.name (tyname ^ "_first_el"), simp_att), [first_el]) ||>>
1.212 + Local_Theory.note
1.213 + ((Binding.name (tyname ^ "_last_el"), simp_att), [last_el]) |> snd |>
1.214 + Local_Theory.exit_global)
1.215 + end;
1.216 +
1.217 +
1.218 +fun add_type_def (s, Basic_Type ty) (ids, thy) =
1.219 + (ids,
1.220 + Typedecl.abbrev_global (Binding.name s, [], NoSyn)
1.221 + (mk_type thy ty) thy |> snd)
1.222 +
1.223 + | add_type_def (s, Enum_Type els) (ids, thy) = add_enum_type s els ids thy
1.224 +
1.225 + | add_type_def (s, Array_Type (argtys, resty)) (ids, thy) =
1.226 + (ids,
1.227 + Typedecl.abbrev_global (Binding.name s, [], NoSyn)
1.228 + (foldr1 HOLogic.mk_prodT (map (mk_type thy) argtys) -->
1.229 + mk_type thy resty) thy |> snd)
1.230 +
1.231 + | add_type_def (s, Record_Type fldtys) (ids, thy) =
1.232 + (ids,
1.233 + Record.add_record true ([], Binding.name s) NONE
1.234 + (maps (fn (flds, ty) =>
1.235 + let val T = mk_type thy ty
1.236 + in map (fn fld => (Binding.name fld, T, NoSyn)) flds
1.237 + end) fldtys) thy)
1.238 +
1.239 + | add_type_def (s, Pending_Type) (ids, thy) =
1.240 + (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd);
1.241 +
1.242 +
1.243 +fun term_of_expr thy types funs pfuns =
1.244 + let
1.245 + fun tm_of vs (Funct ("->", [e, e'])) =
1.246 + (HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
1.247 +
1.248 + | tm_of vs (Funct ("<->", [e, e'])) =
1.249 + (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
1.250 +
1.251 + | tm_of vs (Funct ("or", [e, e'])) =
1.252 + (HOLogic.mk_disj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
1.253 +
1.254 + | tm_of vs (Funct ("and", [e, e'])) =
1.255 + (HOLogic.mk_conj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
1.256 +
1.257 + | tm_of vs (Funct ("not", [e])) =
1.258 + (HOLogic.mk_not (fst (tm_of vs e)), booleanN)
1.259 +
1.260 + | tm_of vs (Funct ("=", [e, e'])) =
1.261 + (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
1.262 +
1.263 + | tm_of vs (Funct ("<>", [e, e'])) = (HOLogic.mk_not
1.264 + (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e'))), booleanN)
1.265 +
1.266 + | tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel @{const_name less}
1.267 + (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
1.268 +
1.269 + | tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel @{const_name less}
1.270 + (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
1.271 +
1.272 + | tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel @{const_name less_eq}
1.273 + (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
1.274 +
1.275 + | tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel @{const_name less_eq}
1.276 + (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
1.277 +
1.278 + | tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop @{const_name plus}
1.279 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
1.280 +
1.281 + | tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop @{const_name minus}
1.282 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
1.283 +
1.284 + | tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop @{const_name times}
1.285 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
1.286 +
1.287 + | tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop @{const_name divide}
1.288 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
1.289 +
1.290 + | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop @{const_name sdiv}
1.291 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
1.292 +
1.293 + | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name smod}
1.294 + (fst (tm_of vs e), fst (tm_of vs e')), integerN)
1.295 +
1.296 + | tm_of vs (Funct ("-", [e])) =
1.297 + (mk_unop @{const_name uminus} (fst (tm_of vs e)), integerN)
1.298 +
1.299 + | tm_of vs (Funct ("**", [e, e'])) =
1.300 + (Const (@{const_name power}, HOLogic.intT --> HOLogic.natT -->
1.301 + HOLogic.intT) $ fst (tm_of vs e) $
1.302 + (@{const nat} $ fst (tm_of vs e')), integerN)
1.303 +
1.304 + | tm_of (tab, _) (Ident s) =
1.305 + (case Symtab.lookup tab s of
1.306 + SOME t_ty => t_ty
1.307 + | NONE => error ("Undeclared identifier " ^ s))
1.308 +
1.309 + | tm_of _ (Number i) = (HOLogic.mk_number HOLogic.intT i, integerN)
1.310 +
1.311 + | tm_of vs (Quantifier (s, xs, ty, e)) =
1.312 + let
1.313 + val (ys, vs') = mk_variables thy xs ty vs;
1.314 + val q = (case s of
1.315 + "for_all" => HOLogic.mk_all
1.316 + | "for_some" => HOLogic.mk_exists)
1.317 + in
1.318 + (fold_rev (fn Free (x, T) => fn t => q (x, T, t))
1.319 + ys (fst (tm_of vs' e)),
1.320 + booleanN)
1.321 + end
1.322 +
1.323 + | tm_of vs (Funct (s, es)) =
1.324 +
1.325 + (* record field selection *)
1.326 + (case try (unprefix "fld_") s of
1.327 + SOME fname => (case es of
1.328 + [e] =>
1.329 + let val (t, rcdty) = tm_of vs e
1.330 + in case lookup types rcdty of
1.331 + SOME (Record_Type fldtys) =>
1.332 + (case get_first (fn (flds, fldty) =>
1.333 + if member (op =) flds fname then SOME fldty
1.334 + else NONE) fldtys of
1.335 + SOME fldty =>
1.336 + (Const (mk_qual_name thy rcdty fname,
1.337 + mk_type thy rcdty --> mk_type thy fldty) $ t,
1.338 + fldty)
1.339 + | NONE => error ("Record " ^ rcdty ^
1.340 + " has no field named " ^ fname))
1.341 + | _ => error (rcdty ^ " is not a record type")
1.342 + end
1.343 + | _ => error ("Function " ^ s ^ " expects one argument"))
1.344 + | NONE =>
1.345 +
1.346 + (* record field update *)
1.347 + (case try (unprefix "upf_") s of
1.348 + SOME fname => (case es of
1.349 + [e, e'] =>
1.350 + let
1.351 + val (t, rcdty) = tm_of vs e;
1.352 + val rT = mk_type thy rcdty;
1.353 + val (u, fldty) = tm_of vs e';
1.354 + val fT = mk_type thy fldty
1.355 + in case lookup types rcdty of
1.356 + SOME (Record_Type fldtys) =>
1.357 + (case get_first (fn (flds, fldty) =>
1.358 + if member (op =) flds fname then SOME fldty
1.359 + else NONE) fldtys of
1.360 + SOME fldty' =>
1.361 + if fldty = fldty' then
1.362 + (Const (mk_qual_name thy rcdty (fname ^ "_update"),
1.363 + (fT --> fT) --> rT --> rT) $
1.364 + Abs ("x", fT, u) $ t,
1.365 + rcdty)
1.366 + else error ("Type " ^ fldty ^
1.367 + " does not match type " ^ fldty' ^ " of field " ^
1.368 + fname)
1.369 + | NONE => error ("Record " ^ rcdty ^
1.370 + " has no field named " ^ fname))
1.371 + | _ => error (rcdty ^ " is not a record type")
1.372 + end
1.373 + | _ => error ("Function " ^ s ^ " expects two arguments"))
1.374 + | NONE =>
1.375 +
1.376 + (* enumeration type to integer *)
1.377 + (case try (unsuffix "__pos") s of
1.378 + SOME tyname => (case es of
1.379 + [e] => (Const (@{const_name pos},
1.380 + mk_type thy tyname --> HOLogic.intT) $ fst (tm_of vs e), integerN)
1.381 + | _ => error ("Function " ^ s ^ " expects one argument"))
1.382 + | NONE =>
1.383 +
1.384 + (* integer to enumeration type *)
1.385 + (case try (unsuffix "__val") s of
1.386 + SOME tyname => (case es of
1.387 + [e] => (Const (@{const_name val},
1.388 + HOLogic.intT --> mk_type thy tyname) $ fst (tm_of vs e), tyname)
1.389 + | _ => error ("Function " ^ s ^ " expects one argument"))
1.390 + | NONE =>
1.391 +
1.392 + (* successor / predecessor of enumeration type element *)
1.393 + if s = "succ" orelse s = "pred" then (case es of
1.394 + [e] =>
1.395 + let
1.396 + val (t, tyname) = tm_of vs e;
1.397 + val T = mk_type thy tyname
1.398 + in (Const
1.399 + (if s = "succ" then @{const_name succ}
1.400 + else @{const_name pred}, T --> T) $ t, tyname)
1.401 + end
1.402 + | _ => error ("Function " ^ s ^ " expects one argument"))
1.403 +
1.404 + (* user-defined proof function *)
1.405 + else
1.406 + (case Symtab.lookup pfuns s of
1.407 + SOME (SOME (_, resty), t) =>
1.408 + (list_comb (t, map (fst o tm_of vs) es), resty)
1.409 + | _ => error ("Undeclared proof function " ^ s))))))
1.410 +
1.411 + | tm_of vs (Element (e, es)) =
1.412 + let val (t, ty) = tm_of vs e
1.413 + in case lookup types ty of
1.414 + SOME (Array_Type (_, elty)) =>
1.415 + (t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es), elty)
1.416 + | _ => error (ty ^ " is not an array type")
1.417 + end
1.418 +
1.419 + | tm_of vs (Update (e, es, e')) =
1.420 + let val (t, ty) = tm_of vs e
1.421 + in case lookup types ty of
1.422 + SOME (Array_Type (idxtys, elty)) =>
1.423 + let
1.424 + val T = foldr1 HOLogic.mk_prodT (map (mk_type thy) idxtys);
1.425 + val U = mk_type thy elty;
1.426 + val fT = T --> U
1.427 + in
1.428 + (Const (@{const_name fun_upd}, fT --> T --> U --> fT) $
1.429 + t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $
1.430 + fst (tm_of vs e'),
1.431 + ty)
1.432 + end
1.433 + | _ => error (ty ^ " is not an array type")
1.434 + end
1.435 +
1.436 + | tm_of vs (Record (s, flds)) =
1.437 + (case lookup types s of
1.438 + SOME (Record_Type fldtys) =>
1.439 + let
1.440 + val flds' = map (apsnd (tm_of vs)) flds;
1.441 + val fnames = maps fst fldtys;
1.442 + val fnames' = map fst flds;
1.443 + val (fvals, ftys) = split_list (map (fn s' =>
1.444 + case AList.lookup (op =) flds' s' of
1.445 + SOME fval_ty => fval_ty
1.446 + | NONE => error ("Field " ^ s' ^ " missing in record " ^ s))
1.447 + fnames);
1.448 + val _ = (case subtract (op =) fnames fnames' of
1.449 + [] => ()
1.450 + | xs => error ("Extra field(s) " ^ commas xs ^
1.451 + " in record " ^ s));
1.452 + val _ = (case duplicates (op =) fnames' of
1.453 + [] => ()
1.454 + | xs => error ("Duplicate field(s) " ^ commas xs ^
1.455 + " in record " ^ s))
1.456 + in
1.457 + (list_comb
1.458 + (Const (mk_qual_name thy s (s ^ "_ext"),
1.459 + map (mk_type thy) ftys @ [HOLogic.unitT] --->
1.460 + mk_type thy s),
1.461 + fvals @ [HOLogic.unit]),
1.462 + s)
1.463 + end
1.464 + | _ => error (s ^ " is not a record type"))
1.465 +
1.466 + | tm_of vs (Array (s, default, assocs)) =
1.467 + (case lookup types s of
1.468 + SOME (Array_Type (idxtys, elty)) =>
1.469 + let
1.470 + val Ts = map (mk_type thy) idxtys;
1.471 + val T = foldr1 HOLogic.mk_prodT Ts;
1.472 + val U = mk_type thy elty;
1.473 + fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]
1.474 + | mk_idx' T (e, SOME e') = Const (@{const_name atLeastAtMost},
1.475 + T --> T --> HOLogic.mk_setT T) $
1.476 + fst (tm_of vs e) $ fst (tm_of vs e');
1.477 + fun mk_idx idx =
1.478 + if length Ts <> length idx then
1.479 + error ("Arity mismatch in construction of array " ^ s)
1.480 + else foldr1 mk_times (map2 mk_idx' Ts idx);
1.481 + fun mk_upd (idxs, e) t =
1.482 + if length idxs = 1 andalso forall (is_none o snd) (hd idxs)
1.483 + then
1.484 + Const (@{const_name fun_upd}, (T --> U) -->
1.485 + T --> U --> T --> U) $ t $
1.486 + foldl1 HOLogic.mk_prod
1.487 + (map (fst o tm_of vs o fst) (hd idxs)) $
1.488 + fst (tm_of vs e)
1.489 + else
1.490 + Const (@{const_name fun_upds}, (T --> U) -->
1.491 + HOLogic.mk_setT T --> U --> T --> U) $ t $
1.492 + foldl1 (HOLogic.mk_binop @{const_name sup})
1.493 + (map mk_idx idxs) $
1.494 + fst (tm_of vs e)
1.495 + in
1.496 + (fold mk_upd assocs
1.497 + (case default of
1.498 + SOME e => Abs ("x", T, fst (tm_of vs e))
1.499 + | NONE => Const (@{const_name undefined}, T --> U)),
1.500 + s)
1.501 + end
1.502 + | _ => error (s ^ " is not an array type"))
1.503 +
1.504 + in tm_of end;
1.505 +
1.506 +
1.507 +fun term_of_rule thy types funs pfuns ids rule =
1.508 + let val tm_of = fst o term_of_expr thy types funs pfuns ids
1.509 + in case rule of
1.510 + Inference_Rule (es, e) => Logic.list_implies
1.511 + (map (HOLogic.mk_Trueprop o tm_of) es, HOLogic.mk_Trueprop (tm_of e))
1.512 + | Substitution_Rule (es, e, e') => Logic.list_implies
1.513 + (map (HOLogic.mk_Trueprop o tm_of) es,
1.514 + HOLogic.mk_Trueprop (HOLogic.mk_eq (tm_of e, tm_of e')))
1.515 + end;
1.516 +
1.517 +
1.518 +val builtin = Symtab.make (map (rpair ())
1.519 + ["->", "<->", "or", "and", "not", "=", "<>", "<", ">", "<=", ">=",
1.520 + "+", "-", "*", "/", "div", "mod", "**"]);
1.521 +
1.522 +fun complex_expr (Number _) = false
1.523 + | complex_expr (Ident _) = false
1.524 + | complex_expr (Funct (s, es)) =
1.525 + not (Symtab.defined builtin s) orelse exists complex_expr es
1.526 + | complex_expr (Quantifier (_, _, _, e)) = complex_expr e
1.527 + | complex_expr _ = true;
1.528 +
1.529 +fun complex_rule (Inference_Rule (es, e)) =
1.530 + complex_expr e orelse exists complex_expr es
1.531 + | complex_rule (Substitution_Rule (es, e, e')) =
1.532 + complex_expr e orelse complex_expr e' orelse
1.533 + exists complex_expr es;
1.534 +
1.535 +val is_pfun =
1.536 + Symtab.defined builtin orf
1.537 + can (unprefix "fld_") orf can (unprefix "upf_") orf
1.538 + can (unsuffix "__pos") orf can (unsuffix "__val") orf
1.539 + equal "succ" orf equal "pred";
1.540 +
1.541 +fun fold_opt f = the_default I o Option.map f;
1.542 +fun fold_pair f g (x, y) = f x #> g y;
1.543 +
1.544 +fun fold_expr f g (Funct (s, es)) = f s #> fold (fold_expr f g) es
1.545 + | fold_expr f g (Ident s) = g s
1.546 + | fold_expr f g (Number _) = I
1.547 + | fold_expr f g (Quantifier (_, _, _, e)) = fold_expr f g e
1.548 + | fold_expr f g (Element (e, es)) =
1.549 + fold_expr f g e #> fold (fold_expr f g) es
1.550 + | fold_expr f g (Update (e, es, e')) =
1.551 + fold_expr f g e #> fold (fold_expr f g) es #> fold_expr f g e'
1.552 + | fold_expr f g (Record (_, flds)) = fold (fold_expr f g o snd) flds
1.553 + | fold_expr f g (Array (_, default, assocs)) =
1.554 + fold_opt (fold_expr f g) default #>
1.555 + fold (fold_pair
1.556 + (fold (fold (fold_pair
1.557 + (fold_expr f g) (fold_opt (fold_expr f g)))))
1.558 + (fold_expr f g)) assocs;
1.559 +
1.560 +val add_expr_pfuns = fold_expr
1.561 + (fn s => if is_pfun s then I else insert (op =) s) (K I);
1.562 +
1.563 +val add_expr_idents = fold_expr (K I) (insert (op =));
1.564 +
1.565 +fun pfun_type thy (argtys, resty) =
1.566 + map (mk_type thy) argtys ---> mk_type thy resty;
1.567 +
1.568 +fun check_pfun_type thy s t optty1 optty2 =
1.569 + let
1.570 + val T = fastype_of t;
1.571 + fun check ty =
1.572 + let val U = pfun_type thy ty
1.573 + in
1.574 + T = U orelse
1.575 + error ("Type\n" ^
1.576 + Syntax.string_of_typ_global thy T ^
1.577 + "\nof function " ^
1.578 + Syntax.string_of_term_global thy t ^
1.579 + " associated with proof function " ^ s ^
1.580 + "\ndoes not match declared type\n" ^
1.581 + Syntax.string_of_typ_global thy U)
1.582 + end
1.583 + in (Option.map check optty1; Option.map check optty2; ()) end;
1.584 +
1.585 +fun upd_option x y = if is_some x then x else y;
1.586 +
1.587 +fun check_pfuns_types thy funs =
1.588 + Symtab.map (fn s => fn (optty, t) =>
1.589 + let val optty' = lookup funs s
1.590 + in
1.591 + (check_pfun_type thy s t optty optty';
1.592 + (NONE |> upd_option optty |> upd_option optty', t))
1.593 + end);
1.594 +
1.595 +
1.596 +(** the VC store **)
1.597 +
1.598 +fun err_unfinished () = error "An unfinished SPARK environment is still open."
1.599 +
1.600 +fun err_vcs names = error (Pretty.string_of
1.601 + (Pretty.big_list "The following verification conditions have not been proved:"
1.602 + (map Pretty.str names)))
1.603 +
1.604 +val strip_number = pairself implode o take_suffix Fdl_Lexer.is_digit o raw_explode;
1.605 +
1.606 +val name_ord = prod_ord string_ord (option_ord int_ord) o
1.607 + pairself (strip_number ##> Int.fromString);
1.608 +
1.609 +structure VCtab = Table(type key = string val ord = name_ord);
1.610 +
1.611 +structure VCs = Theory_Data
1.612 +(
1.613 + type T =
1.614 + {pfuns: ((string list * string) option * term) Symtab.table,
1.615 + env:
1.616 + {ctxt: Element.context_i list,
1.617 + defs: (binding * thm) list,
1.618 + types: fdl_type tab,
1.619 + funs: (string list * string) tab,
1.620 + ids: (term * string) Symtab.table * Name.context,
1.621 + proving: bool,
1.622 + vcs: (string * bool *
1.623 + (string * expr) list * (string * expr) list) VCtab.table,
1.624 + path: Path.T} option}
1.625 + val empty : T = {pfuns = Symtab.empty, env = NONE}
1.626 + val extend = I
1.627 + fun merge ({pfuns = pfuns1, env = NONE}, {pfuns = pfuns2, env = NONE}) =
1.628 + {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),
1.629 + env = NONE}
1.630 + | merge _ = err_unfinished ()
1.631 +)
1.632 +
1.633 +fun set_env (env as {funs, ...}) thy = VCs.map (fn
1.634 + {pfuns, env = NONE} =>
1.635 + {pfuns = check_pfuns_types thy funs pfuns, env = SOME env}
1.636 + | _ => err_unfinished ()) thy;
1.637 +
1.638 +fun mk_pat s = (case Int.fromString s of
1.639 + SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))]
1.640 + | NONE => error ("Bad conclusion identifier: C" ^ s));
1.641 +
1.642 +fun mk_vc thy types funs pfuns ids (tr, proved, ps, cs) =
1.643 + let val prop_of =
1.644 + HOLogic.mk_Trueprop o fst o term_of_expr thy types funs pfuns ids
1.645 + in
1.646 + (tr, proved,
1.647 + Element.Assumes (map (fn (s', e) =>
1.648 + ((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps),
1.649 + Element.Shows (map (fn (s', e) =>
1.650 + (Attrib.empty_binding, [(prop_of e, mk_pat s')])) cs))
1.651 + end;
1.652 +
1.653 +fun fold_vcs f vcs =
1.654 + VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs;
1.655 +
1.656 +fun pfuns_of_vcs pfuns vcs =
1.657 + fold_vcs (add_expr_pfuns o snd) vcs [] |>
1.658 + filter_out (Symtab.defined pfuns);
1.659 +
1.660 +fun declare_missing_pfuns thy funs pfuns vcs (tab, ctxt) =
1.661 + let
1.662 + val (fs, (tys, Ts)) =
1.663 + pfuns_of_vcs pfuns vcs |>
1.664 + map_filter (fn s => lookup funs s |>
1.665 + Option.map (fn ty => (s, (SOME ty, pfun_type thy ty)))) |>
1.666 + split_list ||> split_list;
1.667 + val (fs', ctxt') = Name.variants fs ctxt
1.668 + in
1.669 + (fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns,
1.670 + Element.Fixes (map2 (fn s => fn T =>
1.671 + (Binding.name s, SOME T, NoSyn)) fs' Ts),
1.672 + (tab, ctxt'))
1.673 + end;
1.674 +
1.675 +fun add_proof_fun prep (s, (optty, raw_t)) thy =
1.676 + VCs.map (fn
1.677 + {env = SOME {proving = true, ...}, ...} => err_unfinished ()
1.678 + | {pfuns, env} =>
1.679 + let
1.680 + val optty' = (case env of
1.681 + SOME {funs, ...} => lookup funs s
1.682 + | NONE => NONE);
1.683 + val optty'' = NONE |> upd_option optty |> upd_option optty';
1.684 + val t = prep (Option.map (pfun_type thy) optty'') raw_t
1.685 + in
1.686 + (check_pfun_type thy s t optty optty';
1.687 + if is_some optty'' orelse is_none env then
1.688 + {pfuns = Symtab.update_new (s, (optty'', t)) pfuns,
1.689 + env = env}
1.690 + handle Symtab.DUP _ => error ("Proof function " ^ s ^
1.691 + " already associated with function")
1.692 + else error ("Undeclared proof function " ^ s))
1.693 + end) thy;
1.694 +
1.695 +val is_closed = is_none o #env o VCs.get;
1.696 +
1.697 +fun lookup_vc thy name =
1.698 + (case VCs.get thy of
1.699 + {env = SOME {vcs, types, funs, ids, ctxt, ...}, pfuns} =>
1.700 + (case VCtab.lookup vcs name of
1.701 + SOME vc =>
1.702 + let val (pfuns', ctxt', ids') =
1.703 + declare_missing_pfuns thy funs pfuns vcs ids
1.704 + in SOME (ctxt @ [ctxt'], mk_vc thy types funs pfuns' ids' vc) end
1.705 + | NONE => NONE)
1.706 + | _ => NONE);
1.707 +
1.708 +fun get_vcs thy = (case VCs.get thy of
1.709 + {env = SOME {vcs, types, funs, ids, ctxt, defs, ...}, pfuns} =>
1.710 + let val (pfuns', ctxt', ids') =
1.711 + declare_missing_pfuns thy funs pfuns vcs ids
1.712 + in
1.713 + (ctxt @ [ctxt'], defs,
1.714 + VCtab.dest vcs |>
1.715 + map (apsnd (mk_vc thy types funs pfuns' ids')))
1.716 + end
1.717 + | _ => ([], [], []));
1.718 +
1.719 +fun mark_proved name = VCs.map (fn
1.720 + {pfuns, env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} =>
1.721 + {pfuns = pfuns,
1.722 + env = SOME {ctxt = ctxt, defs = defs,
1.723 + types = types, funs = funs, ids = ids,
1.724 + proving = true,
1.725 + vcs = VCtab.map_entry name (fn (trace, _, ps, cs) =>
1.726 + (trace, true, ps, cs)) vcs,
1.727 + path = path}}
1.728 + | x => x);
1.729 +
1.730 +fun close thy = VCs.map (fn
1.731 + {pfuns, env = SOME {vcs, path, ...}} =>
1.732 + (case VCtab.fold_rev (fn (s, (_, p, _, _)) =>
1.733 + (if p then apfst else apsnd) (cons s)) vcs ([], []) of
1.734 + (proved, []) =>
1.735 + (File.write (Path.ext "prv" path)
1.736 + (concat (map (fn s => snd (strip_number s) ^
1.737 + " -- proved by " ^ Distribution.version ^ "\n") proved));
1.738 + {pfuns = pfuns, env = NONE})
1.739 + | (_, unproved) => err_vcs unproved)
1.740 + | x => x) thy;
1.741 +
1.742 +
1.743 +(** set up verification conditions **)
1.744 +
1.745 +fun partition_opt f =
1.746 + let
1.747 + fun part ys zs [] = (rev ys, rev zs)
1.748 + | part ys zs (x :: xs) = (case f x of
1.749 + SOME y => part (y :: ys) zs xs
1.750 + | NONE => part ys (x :: zs) xs)
1.751 + in part [] [] end;
1.752 +
1.753 +fun dest_def (id, (Substitution_Rule ([], Ident s, rhs))) = SOME (id, (s, rhs))
1.754 + | dest_def _ = NONE;
1.755 +
1.756 +fun mk_rulename (s, i) = Binding.name (s ^ string_of_int i);
1.757 +
1.758 +fun add_const (s, ty) ((tab, ctxt), thy) =
1.759 + let
1.760 + val T = mk_type thy ty;
1.761 + val b = Binding.name s;
1.762 + val c = Const (Sign.full_name thy b, T)
1.763 + in
1.764 + (c,
1.765 + ((Symtab.update (s, (c, ty)) tab, Name.declare s ctxt),
1.766 + Sign.add_consts_i [(b, T, NoSyn)] thy))
1.767 + end;
1.768 +
1.769 +fun add_def types funs pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) =
1.770 + (case lookup consts s of
1.771 + SOME ty =>
1.772 + let
1.773 + val (t, ty') = term_of_expr thy types funs pfuns ids e;
1.774 + val _ = ty = ty' orelse
1.775 + error ("Declared type " ^ ty ^ " of " ^ s ^
1.776 + "\ndoes not match type " ^ ty' ^ " in definition");
1.777 + val id' = mk_rulename id;
1.778 + val lthy = Named_Target.theory_init thy;
1.779 + val ((t', (_, th)), lthy') = Specification.definition
1.780 + (NONE, ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq
1.781 + (Free (s, mk_type thy ty), t)))) lthy;
1.782 + val phi = ProofContext.export_morphism lthy' lthy
1.783 + in
1.784 + ((id', Morphism.thm phi th),
1.785 + ((Symtab.update (s, (Morphism.term phi t', ty)) tab,
1.786 + Name.declare s ctxt),
1.787 + Local_Theory.exit_global lthy'))
1.788 + end
1.789 + | NONE => error ("Undeclared constant " ^ s));
1.790 +
1.791 +fun add_var (s, ty) (ids, thy) =
1.792 + let val ([Free p], ids') = mk_variables thy [s] ty ids
1.793 + in (p, (ids', thy)) end;
1.794 +
1.795 +fun add_init_vars vcs (ids_thy as ((tab, _), _)) =
1.796 + fold_map add_var
1.797 + (map_filter
1.798 + (fn s => case try (unsuffix "~") s of
1.799 + SOME s' => (case Symtab.lookup tab s' of
1.800 + SOME (_, ty) => SOME (s, ty)
1.801 + | NONE => error ("Undeclared identifier " ^ s'))
1.802 + | NONE => NONE)
1.803 + (fold_vcs (add_expr_idents o snd) vcs []))
1.804 + ids_thy;
1.805 +
1.806 +fun is_trivial_vc ([], [(_, Ident "true")]) = true
1.807 + | is_trivial_vc _ = false;
1.808 +
1.809 +fun rulenames rules = commas
1.810 + (map (fn ((s, i), _) => s ^ "(" ^ string_of_int i ^ ")") rules);
1.811 +
1.812 +(* sort definitions according to their dependency *)
1.813 +fun sort_defs _ _ [] sdefs = rev sdefs
1.814 + | sort_defs pfuns consts defs sdefs =
1.815 + (case find_first (fn (_, (_, e)) =>
1.816 + forall (Symtab.defined pfuns) (add_expr_pfuns e []) andalso
1.817 + forall (fn id =>
1.818 + member (fn (s, (_, (s', _))) => s = s') sdefs id orelse
1.819 + member (fn (s, (s', _)) => s = s') consts id)
1.820 + (add_expr_idents e [])) defs of
1.821 + SOME d => sort_defs pfuns consts
1.822 + (remove (op =) d defs) (d :: sdefs)
1.823 + | NONE => error ("Bad definitions: " ^ rulenames defs));
1.824 +
1.825 +fun set_vcs ({types, vars, consts, funs} : decls) (rules, _) vcs path thy =
1.826 + let
1.827 + val {pfuns, ...} = VCs.get thy;
1.828 + val (defs', rules') = partition_opt dest_def rules;
1.829 + val consts' =
1.830 + subtract (fn ((_, (s, _)), (s', _)) => s = s') defs' (items consts);
1.831 + val defs = sort_defs pfuns consts' defs' [];
1.832 + (* ignore all complex rules in rls files *)
1.833 + val (rules'', other_rules) =
1.834 + List.partition (complex_rule o snd) rules';
1.835 + val _ = if null rules'' then ()
1.836 + else warning ("Ignoring rules: " ^ rulenames rules'');
1.837 +
1.838 + val vcs' = VCtab.make (maps (fn (tr, vcs) =>
1.839 + map (fn (s, (ps, cs)) => (s, (tr, false, ps, cs)))
1.840 + (filter_out (is_trivial_vc o snd) vcs)) vcs);
1.841 +
1.842 + val _ = (case filter_out (is_some o lookup funs)
1.843 + (pfuns_of_vcs pfuns vcs') of
1.844 + [] => ()
1.845 + | fs => error ("Undeclared proof function(s) " ^ commas fs));
1.846 +
1.847 + val (((defs', vars''), ivars), (ids, thy')) =
1.848 + ((Symtab.empty |>
1.849 + Symtab.update ("false", (HOLogic.false_const, booleanN)) |>
1.850 + Symtab.update ("true", (HOLogic.true_const, booleanN)),
1.851 + Name.context), thy) |>
1.852 + fold add_type_def (items types) |>
1.853 + fold (snd oo add_const) consts' |>
1.854 + fold_map (add_def types funs pfuns consts) defs ||>>
1.855 + fold_map add_var (items vars) ||>>
1.856 + add_init_vars vcs';
1.857 +
1.858 + val ctxt =
1.859 + [Element.Fixes (map (fn (s, T) =>
1.860 + (Binding.name s, SOME T, NoSyn)) (vars'' @ ivars)),
1.861 + Element.Assumes (map (fn (id, rl) =>
1.862 + ((mk_rulename id, []),
1.863 + [(term_of_rule thy' types funs pfuns ids rl, [])]))
1.864 + other_rules),
1.865 + Element.Notes (Thm.definitionK,
1.866 + [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]
1.867 +
1.868 + in
1.869 + set_env {ctxt = ctxt, defs = defs', types = types, funs = funs,
1.870 + ids = ids, proving = false, vcs = vcs', path = path} thy'
1.871 + end;
1.872 +
1.873 +end;