1 (* Title: HOL/SPARK/Tools/spark_vcs.ML
2 Author: Stefan Berghofer
3 Copyright: secunet Security Networks AG
5 Store for verification conditions generated by SPARK/Ada.
10 val set_vcs: Fdl_Parser.decls -> Fdl_Parser.rules ->
11 (string * string) * Fdl_Parser.vcs -> Path.T -> string -> theory -> theory
12 val add_proof_fun: (typ option -> 'a -> term) ->
13 string * ((string list * string) option * 'a) ->
15 val add_type: string * (typ * (string * string) list) -> theory -> theory
16 val lookup_vc: theory -> bool -> string -> (Element.context_i list *
17 (string * thm list option * Element.context_i * Element.statement_i)) option
18 val get_vcs: theory -> bool ->
19 Element.context_i list * (binding * thm) list * (string *
20 (string * thm list option * Element.context_i * Element.statement_i)) list
21 val mark_proved: string -> thm list -> theory -> theory
22 val close: bool -> theory -> theory
23 val is_closed: theory -> bool
26 structure SPARK_VCs: SPARK_VCS =
34 fun err_unfinished () = error "An unfinished SPARK environment is still open."
36 val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode;
38 val name_ord = prod_ord string_ord (option_ord int_ord) o
39 apply2 (strip_number ##> Int.fromString);
41 structure VCtab = Table(type key = string val ord = name_ord);
43 structure VCs = Theory_Data
46 {pfuns: ((string list * string) option * term) Symtab.table,
47 type_map: (typ * (string * string) list) Symtab.table,
49 {ctxt: Element.context_i list,
50 defs: (binding * thm) list,
52 funs: (string list * string) tab,
53 pfuns: ((string list * string) option * term) Symtab.table,
54 ids: (term * string) Symtab.table * Name.context,
56 vcs: (string * thm list option *
57 (string * expr) list * (string * expr) list) VCtab.table,
59 prefix: string} option}
60 val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE}
62 fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},
63 {pfuns = pfuns2, type_map = type_map2, env = NONE}) =
64 {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),
65 type_map = Symtab.merge (op =) (type_map1, type_map2),
67 | merge _ = err_unfinished ()
73 val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode;
75 val lcase_eq = (op =) o apply2 (to_lower o Long_Name.base_name);
77 fun lookup_prfx "" tab s = Symtab.lookup tab s
78 | lookup_prfx prfx tab s = (case Symtab.lookup tab s of
79 NONE => Symtab.lookup tab (prfx ^ "__" ^ s)
84 fun strip ys [] = ("", implode ys)
85 | strip ys ("_" :: "_" :: xs) = (implode (rev xs), implode ys)
86 | strip ys (x :: xs) = strip (x :: ys) xs
87 in strip [] (rev (raw_explode s)) end;
89 fun unprefix_pfun "" s = s
90 | unprefix_pfun prfx s =
91 let val (prfx', s') = strip_prfx s
92 in if prfx = prfx' then s' else s end;
95 let val T = fastype_of t
96 in Const (s, T --> T) $ t end;
100 val setT = fastype_of t;
101 val T = HOLogic.dest_setT setT;
102 val U = HOLogic.dest_setT (fastype_of u)
104 Const (\<^const_name>\<open>Sigma\<close>, setT --> (T --> HOLogic.mk_setT U) -->
105 HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)
108 fun get_type thy prfx ty =
109 let val {type_map, ...} = VCs.get thy
110 in lookup_prfx prfx type_map ty end;
112 fun mk_type' _ _ "integer" = (HOLogic.intT, [])
113 | mk_type' _ _ "boolean" = (HOLogic.boolT, [])
114 | mk_type' thy prfx ty =
115 (case get_type thy prfx ty of
117 (Syntax.check_typ (Proof_Context.init_global thy)
118 (Type (Sign.full_name thy (Binding.name ty), [])),
122 fun mk_type thy prfx ty = fst (mk_type' thy prfx ty);
124 val booleanN = "boolean";
125 val integerN = "integer";
127 fun define_overloaded (def_name, eq) lthy =
129 val ((c, _), rhs) = eq |> Syntax.check_term lthy |>
130 Logic.dest_equals |>> dest_Free;
131 val ((_, (_, thm)), lthy') = Local_Theory.define
132 ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs)) lthy
133 val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
134 val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm
135 in (thm', lthy') end;
137 fun strip_underscores s =
138 strip_underscores (unsuffix "_" s) handle Fail _ => s;
141 unsuffix "~" s ^ "_init" handle Fail _ => s;
143 val mangle_name = strip_underscores #> strip_tilde;
145 fun mk_variables thy prfx xs ty (tab, ctxt) =
147 val T = mk_type thy prfx ty;
148 val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt;
149 val zs = map (Free o rpair T) ys;
150 in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
152 fun get_record_info thy T = (case Record.dest_recTs T of
153 [(tyname, [\<^typ>\<open>unit\<close>])] =>
154 Record.get_info thy (Long_Name.qualifier tyname)
157 fun find_field [] fname fields =
158 find_first (curry lcase_eq fname o fst) fields
159 | find_field cmap fname fields =
160 (case AList.lookup (op =) cmap fname of
162 | SOME fname' => SOME (fname', the (AList.lookup (op =) fields fname')));
164 fun find_field' fname = get_first (fn (flds, fldty) =>
165 if member (op =) flds fname then SOME fldty else NONE);
167 fun assoc_ty_err thy T s msg =
168 error ("Type " ^ Syntax.string_of_typ_global thy T ^
169 " associated with SPARK type " ^ s ^ "\n" ^ msg);
172 (** generate properties of enumeration types **)
174 fun add_enum_type tyname tyname' thy =
176 val {case_name, ...} = the (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] tyname');
177 val cs = map Const (the (BNF_LFP_Compat.get_constrs thy tyname'));
179 val T = Type (tyname', []);
180 val p = Const (\<^const_name>\<open>pos\<close>, T --> HOLogic.intT);
181 val v = Const (\<^const_name>\<open>val\<close>, HOLogic.intT --> T);
182 val card = Const (\<^const_name>\<open>card\<close>,
183 HOLogic.mk_setT T --> HOLogic.natT) $ HOLogic.mk_UNIV T;
185 fun mk_binrel_def s f = Logic.mk_equals
186 (Const (s, T --> T --> HOLogic.boolT),
187 Abs ("x", T, Abs ("y", T,
188 Const (s, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $
189 (f $ Bound 1) $ (f $ Bound 0))));
191 val (((def1, def2), def3), lthy) = thy |>
193 Class.instantiation ([tyname'], [], \<^sort>\<open>spark_enum\<close>) |>
195 define_overloaded ("pos_" ^ tyname ^ "_def", Logic.mk_equals
197 list_comb (Const (case_name, replicate k HOLogic.intT @
198 [T] ---> HOLogic.intT),
199 map (HOLogic.mk_number HOLogic.intT) (0 upto k - 1)))) ||>>
201 define_overloaded ("less_eq_" ^ tyname ^ "_def",
202 mk_binrel_def \<^const_name>\<open>less_eq\<close> p) ||>>
203 define_overloaded ("less_" ^ tyname ^ "_def",
204 mk_binrel_def \<^const_name>\<open>less\<close> p);
206 val UNIV_eq = Goal.prove lthy [] []
207 (HOLogic.mk_Trueprop (HOLogic.mk_eq
208 (HOLogic.mk_UNIV T, HOLogic.mk_set T cs)))
209 (fn {context = ctxt, ...} =>
210 resolve_tac ctxt @{thms subset_antisym} 1 THEN
211 resolve_tac ctxt @{thms subsetI} 1 THEN
212 Old_Datatype_Aux.exh_tac ctxt (K (#exhaust (BNF_LFP_Compat.the_info
213 (Proof_Context.theory_of ctxt) [BNF_LFP_Compat.Keep_Nesting] tyname'))) 1 THEN
214 ALLGOALS (asm_full_simp_tac ctxt));
216 val finite_UNIV = Goal.prove lthy [] []
217 (HOLogic.mk_Trueprop (Const (\<^const_name>\<open>finite\<close>,
218 HOLogic.mk_setT T --> HOLogic.boolT) $ HOLogic.mk_UNIV T))
219 (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1);
221 val card_UNIV = Goal.prove lthy [] []
222 (HOLogic.mk_Trueprop (HOLogic.mk_eq
223 (card, HOLogic.mk_number HOLogic.natT k)))
224 (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1);
226 val range_pos = Goal.prove lthy [] []
227 (HOLogic.mk_Trueprop (HOLogic.mk_eq
228 (Const (\<^const_name>\<open>image\<close>, (T --> HOLogic.intT) -->
229 HOLogic.mk_setT T --> HOLogic.mk_setT HOLogic.intT) $
230 p $ HOLogic.mk_UNIV T,
231 Const (\<^const_name>\<open>atLeastLessThan\<close>, HOLogic.intT -->
232 HOLogic.intT --> HOLogic.mk_setT HOLogic.intT) $
233 HOLogic.mk_number HOLogic.intT 0 $
234 (\<^term>\<open>int\<close> $ card))))
235 (fn {context = ctxt, ...} =>
236 simp_tac (ctxt addsimps [card_UNIV]) 1 THEN
237 simp_tac (ctxt addsimps [UNIV_eq, def1]) 1 THEN
238 resolve_tac ctxt @{thms subset_antisym} 1 THEN
240 resolve_tac ctxt @{thms subsetI} 1 THEN
241 asm_full_simp_tac (ctxt addsimps @{thms interval_expand}
242 delsimps @{thms atLeastLessThan_iff}) 1);
245 Class.prove_instantiation_instance (fn ctxt =>
246 Class.intro_classes_tac ctxt [] THEN
247 resolve_tac ctxt [finite_UNIV] 1 THEN
248 resolve_tac ctxt [range_pos] 1 THEN
249 simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def3]) 1 THEN
250 simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def2]) 1) lthy;
252 val (pos_eqs, val_eqs) = split_list (map_index (fn (i, c) =>
254 val n = HOLogic.mk_number HOLogic.intT i;
255 val th = Goal.prove lthy' [] []
256 (HOLogic.mk_Trueprop (HOLogic.mk_eq (p $ c, n)))
257 (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [def1]) 1);
258 val th' = Goal.prove lthy' [] []
259 (HOLogic.mk_Trueprop (HOLogic.mk_eq (v $ n, c)))
260 (fn {context = ctxt, ...} =>
261 resolve_tac ctxt [@{thm inj_pos} RS @{thm injD}] 1 THEN
262 simp_tac (ctxt addsimps [@{thm pos_val}, range_pos, card_UNIV, th]) 1)
263 in (th, th') end) cs);
265 val first_el = Goal.prove lthy' [] []
266 (HOLogic.mk_Trueprop (HOLogic.mk_eq
267 (Const (\<^const_name>\<open>first_el\<close>, T), hd cs)))
268 (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [@{thm first_el_def}, hd val_eqs]) 1);
270 val last_el = Goal.prove lthy' [] []
271 (HOLogic.mk_Trueprop (HOLogic.mk_eq
272 (Const (\<^const_name>\<open>last_el\<close>, T), List.last cs)))
273 (fn {context = ctxt, ...} =>
274 simp_tac (ctxt addsimps [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1);
278 ((Binding.name (tyname ^ "_card"), @{attributes [simp]}), [card_UNIV]) ||>>
280 ((Binding.name (tyname ^ "_pos"), @{attributes [simp]}), pos_eqs) ||>>
282 ((Binding.name (tyname ^ "_val"), @{attributes [simp]}), val_eqs) ||>>
284 ((Binding.name (tyname ^ "_first_el"), @{attributes [simp]}), [first_el]) ||>>
286 ((Binding.name (tyname ^ "_last_el"), @{attributes [simp]}), [last_el]) |> snd |>
287 Local_Theory.exit_global
291 fun check_no_assoc thy prfx s = case get_type thy prfx s of
293 | SOME _ => error ("Cannot associate a type with " ^ s ^
294 "\nsince it is no record or enumeration type");
296 fun check_enum [] [] = NONE
297 | check_enum els [] = SOME ("has no element(s) " ^ commas els)
298 | check_enum [] cs = SOME ("has extra element(s) " ^
299 commas (map (Long_Name.base_name o fst) cs))
300 | check_enum (el :: els) ((cname, _) :: cs) =
301 if lcase_eq (el, cname) then check_enum els cs
302 else SOME ("either has no element " ^ el ^
303 " or it is at the wrong position");
305 fun invert_map [] = I
307 map (apfst (the o AList.lookup (op =) (map swap cmap)));
309 fun add_type_def prfx (s, Basic_Type ty) (ids, thy) =
310 (check_no_assoc thy prfx s;
312 Typedecl.abbrev_global (Binding.name s, [], NoSyn)
313 (mk_type thy prfx ty) thy |> snd))
315 | add_type_def prfx (s, Enum_Type els) ((tab, ctxt), thy) =
317 val (thy', tyname) = (case get_type thy prfx s of
320 val tyb = Binding.name s;
321 val tyname = Sign.full_name thy tyb
324 BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Keep_Nesting]
326 map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
327 add_enum_type s tyname,
330 | SOME (T as Type (tyname, []), cmap) =>
331 (case BNF_LFP_Compat.get_constrs thy tyname of
332 NONE => assoc_ty_err thy T s "is not a datatype"
334 let val (prfx', _) = strip_prfx s
336 case check_enum (map (unprefix_pfun prfx') els)
337 (invert_map cmap cs) of
338 NONE => (thy, tyname)
339 | SOME msg => assoc_ty_err thy T s msg
341 | SOME (T, _) => assoc_ty_err thy T s "is not a datatype");
342 val cs = map Const (the (BNF_LFP_Compat.get_constrs thy' tyname));
344 ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
345 fold Name.declare els ctxt),
349 | add_type_def prfx (s, Array_Type (argtys, resty)) (ids, thy) =
350 (check_no_assoc thy prfx s;
352 Typedecl.abbrev_global (Binding.name s, [], NoSyn)
353 (foldr1 HOLogic.mk_prodT (map (mk_type thy prfx) argtys) -->
354 mk_type thy prfx resty) thy |> snd))
356 | add_type_def prfx (s, Record_Type fldtys) (ids, thy) =
358 let val fldTs = maps (fn (flds, ty) =>
359 map (rpair (mk_type thy prfx ty)) flds) fldtys
360 in case get_type thy prfx s of
362 Record.add_record {overloaded = false} ([], Binding.name s) NONE
363 (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy
365 (case get_record_info thy rT of
366 NONE => assoc_ty_err thy rT s "is not a record type"
367 | SOME {fields, ...} =>
368 let val fields' = invert_map cmap fields
370 (case subtract (lcase_eq o apply2 fst) fldTs fields' of
372 | flds => assoc_ty_err thy rT s ("has extra field(s) " ^
373 commas (map (Long_Name.base_name o fst) flds));
375 case AList.lookup lcase_eq fields' fld of
376 NONE => assoc_ty_err thy rT s ("has no field " ^ fld)
377 | SOME U => T = U orelse assoc_ty_err thy rT s
379 fld ^ " whose type\n" ^
380 Syntax.string_of_typ_global thy U ^
381 "\ndoes not match declared type\n" ^
382 Syntax.string_of_typ_global thy T)) fldTs;
387 | add_type_def prfx (s, Pending_Type) (ids, thy) =
389 case get_type thy prfx s of
391 | NONE => Typedecl.typedecl_global {final = true} (Binding.name s, [], NoSyn) thy |> snd);
394 fun term_of_expr thy prfx types pfuns =
396 fun tm_of vs (Funct ("->", [e, e'])) =
397 (HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
399 | tm_of vs (Funct ("<->", [e, e'])) =
400 (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
402 | tm_of vs (Funct ("or", [e, e'])) =
403 (HOLogic.mk_disj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
405 | tm_of vs (Funct ("and", [e, e'])) =
406 (HOLogic.mk_conj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
408 | tm_of vs (Funct ("not", [e])) =
409 (HOLogic.mk_not (fst (tm_of vs e)), booleanN)
411 | tm_of vs (Funct ("=", [e, e'])) =
412 (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
414 | tm_of vs (Funct ("<>", [e, e'])) = (HOLogic.mk_not
415 (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e'))), booleanN)
417 | tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
418 (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
420 | tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
421 (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
423 | tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
424 (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
426 | tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
427 (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
429 | tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>plus\<close>
430 (fst (tm_of vs e), fst (tm_of vs e')), integerN)
432 | tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>minus\<close>
433 (fst (tm_of vs e), fst (tm_of vs e')), integerN)
435 | tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>times\<close>
436 (fst (tm_of vs e), fst (tm_of vs e')), integerN)
438 | tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>divide\<close>
439 (fst (tm_of vs e), fst (tm_of vs e')), integerN)
441 | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>sdiv\<close>
442 (fst (tm_of vs e), fst (tm_of vs e')), integerN)
444 | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>modulo\<close>
445 (fst (tm_of vs e), fst (tm_of vs e')), integerN)
447 | tm_of vs (Funct ("-", [e])) =
448 (mk_unop \<^const_name>\<open>uminus\<close> (fst (tm_of vs e)), integerN)
450 | tm_of vs (Funct ("**", [e, e'])) =
451 (Const (\<^const_name>\<open>power\<close>, HOLogic.intT --> HOLogic.natT -->
452 HOLogic.intT) $ fst (tm_of vs e) $
453 (\<^const>\<open>nat\<close> $ fst (tm_of vs e')), integerN)
455 | tm_of (tab, _) (Ident s) =
456 (case Symtab.lookup tab s of
458 | NONE => (case lookup_prfx prfx pfuns s of
459 SOME (SOME ([], resty), t) => (t, resty)
460 | _ => error ("Undeclared identifier " ^ s)))
462 | tm_of _ (Number i) = (HOLogic.mk_number HOLogic.intT i, integerN)
464 | tm_of vs (Quantifier (s, xs, ty, e)) =
466 val (ys, vs') = mk_variables thy prfx xs ty vs;
468 "for_all" => HOLogic.mk_all
469 | "for_some" => HOLogic.mk_exists)
471 (fold_rev (fn Free (x, T) => fn t => q (x, T, t))
472 ys (fst (tm_of vs' e)),
476 | tm_of vs (Funct (s, es)) =
478 (* record field selection *)
479 (case try (unprefix "fld_") s of
480 SOME fname => (case es of
483 val (t, rcdty) = tm_of vs e;
484 val (rT, cmap) = mk_type' thy prfx rcdty
485 in case (get_record_info thy rT, lookup types rcdty) of
486 (SOME {fields, ...}, SOME (Record_Type fldtys)) =>
487 (case (find_field cmap fname fields,
488 find_field' fname fldtys) of
489 (SOME (fname', fT), SOME fldty) =>
490 (Const (fname', rT --> fT) $ t, fldty)
491 | _ => error ("Record " ^ rcdty ^
492 " has no field named " ^ fname))
493 | _ => error (rcdty ^ " is not a record type")
495 | _ => error ("Function " ^ s ^ " expects one argument"))
498 (* record field update *)
499 (case try (unprefix "upf_") s of
500 SOME fname => (case es of
503 val (t, rcdty) = tm_of vs e;
504 val (rT, cmap) = mk_type' thy prfx rcdty;
505 val (u, fldty) = tm_of vs e';
506 val fT = mk_type thy prfx fldty
507 in case get_record_info thy rT of
508 SOME {fields, ...} =>
509 (case find_field cmap fname fields of
512 (Const (fname' ^ "_update",
513 (fT --> fT) --> rT --> rT) $
514 Abs ("x", fT, u) $ t,
516 else error ("Type\n" ^
517 Syntax.string_of_typ_global thy fT ^
518 "\ndoes not match type\n" ^
519 Syntax.string_of_typ_global thy fU ^
520 "\nof field " ^ fname)
521 | NONE => error ("Record " ^ rcdty ^
522 " has no field named " ^ fname))
523 | _ => error (rcdty ^ " is not a record type")
525 | _ => error ("Function " ^ s ^ " expects two arguments"))
528 (* enumeration type to integer *)
529 (case try (unsuffix "__pos") s of
530 SOME tyname => (case es of
531 [e] => (Const (\<^const_name>\<open>pos\<close>,
532 mk_type thy prfx tyname --> HOLogic.intT) $ fst (tm_of vs e),
534 | _ => error ("Function " ^ s ^ " expects one argument"))
537 (* integer to enumeration type *)
538 (case try (unsuffix "__val") s of
539 SOME tyname => (case es of
540 [e] => (Const (\<^const_name>\<open>val\<close>,
541 HOLogic.intT --> mk_type thy prfx tyname) $ fst (tm_of vs e),
543 | _ => error ("Function " ^ s ^ " expects one argument"))
546 (* successor / predecessor of enumeration type element *)
547 if s = "succ" orelse s = "pred" then (case es of
550 val (t, tyname) = tm_of vs e;
551 val T = mk_type thy prfx tyname
553 (if s = "succ" then \<^const_name>\<open>succ\<close>
554 else \<^const_name>\<open>pred\<close>, T --> T) $ t, tyname)
556 | _ => error ("Function " ^ s ^ " expects one argument"))
558 (* user-defined proof function *)
560 (case lookup_prfx prfx pfuns s of
561 SOME (SOME (_, resty), t) =>
562 (list_comb (t, map (fst o tm_of vs) es), resty)
563 | _ => error ("Undeclared proof function " ^ s))))))
565 | tm_of vs (Element (e, es)) =
566 let val (t, ty) = tm_of vs e
567 in case lookup types ty of
568 SOME (Array_Type (_, elty)) =>
569 (t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es), elty)
570 | _ => error (ty ^ " is not an array type")
573 | tm_of vs (Update (e, es, e')) =
574 let val (t, ty) = tm_of vs e
575 in case lookup types ty of
576 SOME (Array_Type (idxtys, elty)) =>
578 val T = foldr1 HOLogic.mk_prodT
579 (map (mk_type thy prfx) idxtys);
580 val U = mk_type thy prfx elty;
583 (Const (\<^const_name>\<open>fun_upd\<close>, fT --> T --> U --> fT) $
584 t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $
588 | _ => error (ty ^ " is not an array type")
591 | tm_of vs (Record (s, flds)) =
593 val (T, cmap) = mk_type' thy prfx s;
594 val {extension = (ext_name, _), fields, ...} =
595 (case get_record_info thy T of
596 NONE => error (s ^ " is not a record type")
597 | SOME info => info);
598 val flds' = map (apsnd (tm_of vs)) flds;
599 val fnames = fields |> invert_map cmap |>
600 map (Long_Name.base_name o fst);
601 val fnames' = map fst flds;
602 val (fvals, ftys) = split_list (map (fn s' =>
603 case AList.lookup lcase_eq flds' s' of
604 SOME fval_ty => fval_ty
605 | NONE => error ("Field " ^ s' ^ " missing in record " ^ s))
607 val _ = (case subtract lcase_eq fnames fnames' of
609 | xs => error ("Extra field(s) " ^ commas xs ^
611 val _ = (case duplicates (op =) fnames' of
613 | xs => error ("Duplicate field(s) " ^ commas xs ^
618 map (mk_type thy prfx) ftys @ [HOLogic.unitT] ---> T),
619 fvals @ [HOLogic.unit]),
623 | tm_of vs (Array (s, default, assocs)) =
624 (case lookup types s of
625 SOME (Array_Type (idxtys, elty)) =>
627 val Ts = map (mk_type thy prfx) idxtys;
628 val T = foldr1 HOLogic.mk_prodT Ts;
629 val U = mk_type thy prfx elty;
630 fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]
631 | mk_idx' T (e, SOME e') = Const (\<^const_name>\<open>atLeastAtMost\<close>,
632 T --> T --> HOLogic.mk_setT T) $
633 fst (tm_of vs e) $ fst (tm_of vs e');
635 if length Ts <> length idx then
636 error ("Arity mismatch in construction of array " ^ s)
637 else foldr1 mk_times (map2 mk_idx' Ts idx);
638 fun mk_upd (idxs, e) t =
639 if length idxs = 1 andalso forall (is_none o snd) (hd idxs)
641 Const (\<^const_name>\<open>fun_upd\<close>, (T --> U) -->
642 T --> U --> T --> U) $ t $
643 foldl1 HOLogic.mk_prod
644 (map (fst o tm_of vs o fst) (hd idxs)) $
647 Const (\<^const_name>\<open>fun_upds\<close>, (T --> U) -->
648 HOLogic.mk_setT T --> U --> T --> U) $ t $
649 foldl1 (HOLogic.mk_binop \<^const_name>\<open>sup\<close>)
655 SOME e => Abs ("x", T, fst (tm_of vs e))
656 | NONE => Const (\<^const_name>\<open>undefined\<close>, T --> U)),
659 | _ => error (s ^ " is not an array type"))
664 fun term_of_rule thy prfx types pfuns ids rule =
665 let val tm_of = fst o term_of_expr thy prfx types pfuns ids
667 Inference_Rule (es, e) => Logic.list_implies
668 (map (HOLogic.mk_Trueprop o tm_of) es, HOLogic.mk_Trueprop (tm_of e))
669 | Substitution_Rule (es, e, e') => Logic.list_implies
670 (map (HOLogic.mk_Trueprop o tm_of) es,
671 HOLogic.mk_Trueprop (HOLogic.mk_eq (tm_of e, tm_of e')))
675 val builtin = Symtab.make (map (rpair ())
676 ["->", "<->", "or", "and", "not", "=", "<>", "<", ">", "<=", ">=",
677 "+", "-", "*", "/", "div", "mod", "**"]);
679 fun complex_expr (Number _) = false
680 | complex_expr (Ident _) = false
681 | complex_expr (Funct (s, es)) =
682 not (Symtab.defined builtin s) orelse exists complex_expr es
683 | complex_expr (Quantifier (_, _, _, e)) = complex_expr e
684 | complex_expr _ = true;
686 fun complex_rule (Inference_Rule (es, e)) =
687 complex_expr e orelse exists complex_expr es
688 | complex_rule (Substitution_Rule (es, e, e')) =
689 complex_expr e orelse complex_expr e' orelse
690 exists complex_expr es;
693 Symtab.defined builtin orf
694 can (unprefix "fld_") orf can (unprefix "upf_") orf
695 can (unsuffix "__pos") orf can (unsuffix "__val") orf
696 equal "succ" orf equal "pred";
698 fun fold_opt f = the_default I o Option.map f;
699 fun fold_pair f g (x, y) = f x #> g y;
701 fun fold_expr f g (Funct (s, es)) = f s #> fold (fold_expr f g) es
702 | fold_expr f g (Ident s) = g s
703 | fold_expr f g (Number _) = I
704 | fold_expr f g (Quantifier (_, _, _, e)) = fold_expr f g e
705 | fold_expr f g (Element (e, es)) =
706 fold_expr f g e #> fold (fold_expr f g) es
707 | fold_expr f g (Update (e, es, e')) =
708 fold_expr f g e #> fold (fold_expr f g) es #> fold_expr f g e'
709 | fold_expr f g (Record (_, flds)) = fold (fold_expr f g o snd) flds
710 | fold_expr f g (Array (_, default, assocs)) =
711 fold_opt (fold_expr f g) default #>
713 (fold (fold (fold_pair
714 (fold_expr f g) (fold_opt (fold_expr f g)))))
715 (fold_expr f g)) assocs;
717 fun add_expr_pfuns funs = fold_expr
718 (fn s => if is_pfun s then I else insert (op =) s)
719 (fn s => if is_none (lookup funs s) then I else insert (op =) s);
721 val add_expr_idents = fold_expr (K I) (insert (op =));
723 fun pfun_type thy prfx (argtys, resty) =
724 map (mk_type thy prfx) argtys ---> mk_type thy prfx resty;
726 fun check_pfun_type thy prfx s t optty1 optty2 =
728 val T = fastype_of t;
730 let val U = pfun_type thy prfx ty
734 Syntax.string_of_typ_global thy T ^
736 Syntax.string_of_term_global thy t ^
737 " associated with proof function " ^ s ^
738 "\ndoes not match declared type\n" ^
739 Syntax.string_of_typ_global thy U)
741 in (Option.map check optty1; Option.map check optty2; ()) end;
743 fun upd_option x y = if is_some x then x else y;
745 fun check_pfuns_types thy prfx funs =
746 Symtab.map (fn s => fn (optty, t) =>
747 let val optty' = lookup funs (unprefix_pfun prfx s)
749 (check_pfun_type thy prfx s t optty optty';
750 (NONE |> upd_option optty |> upd_option optty', t))
756 fun pp_vcs msg vcs = Pretty.big_list msg (map (Pretty.str o fst) vcs);
758 fun pp_open_vcs [] = Pretty.str "All verification conditions have been proved."
759 | pp_open_vcs vcs = pp_vcs
760 "The following verification conditions remain to be proved:" vcs;
762 fun partition_vcs vcs = VCtab.fold_rev
763 (fn (name, (trace, SOME thms, ps, cs)) =>
764 apfst (cons (name, (trace, thms, ps, cs)))
765 | (name, (trace, NONE, ps, cs)) =>
766 apsnd (cons (name, (trace, ps, cs))))
769 fun insert_break prt = Pretty.blk (0, [Pretty.fbrk, prt]);
771 fun print_open_vcs f vcs =
772 (Pretty.writeln (f (pp_open_vcs (snd (partition_vcs vcs)))); vcs);
774 fun set_env ctxt defs types funs ids vcs path prefix thy = VCs.map (fn
775 {pfuns, type_map, env = NONE} =>
779 {ctxt = ctxt, defs = defs, types = types, funs = funs,
780 pfuns = check_pfuns_types thy prefix funs pfuns,
781 ids = ids, proving = false, vcs = print_open_vcs I vcs, path = path,
783 | _ => err_unfinished ()) thy;
785 fun mk_pat s = (case Int.fromString s of
786 SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))]
787 | NONE => error ("Bad conclusion identifier: C" ^ s));
789 fun mk_vc thy prfx types pfuns ids name_concl (tr, proved, ps, cs) =
791 HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids
794 Element.Assumes (map (fn (s', e) =>
795 ((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps),
796 Element.Shows (map (fn (s', e) =>
797 (if name_concl then (Binding.name ("C" ^ s'), [])
798 else Binding.empty_atts,
799 [(prop_of e, mk_pat s')])) cs))
803 VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs;
805 fun pfuns_of_vcs prfx funs pfuns vcs =
806 fold_vcs (add_expr_pfuns funs o snd) vcs [] |>
807 filter (is_none o lookup_prfx prfx pfuns);
809 fun declare_missing_pfuns thy prfx funs pfuns vcs (tab, ctxt) =
811 val (fs, (tys, Ts)) =
812 pfuns_of_vcs prfx funs pfuns vcs |>
813 map_filter (fn s => lookup funs s |>
814 Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |>
815 split_list ||> split_list;
816 val (fs', ctxt') = fold_map Name.variant fs ctxt
818 (fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns,
819 Element.Fixes (map2 (fn s => fn T =>
820 (Binding.name s, SOME T, NoSyn)) fs' Ts),
824 fun map_pfuns f {pfuns, type_map, env} =
825 {pfuns = f pfuns, type_map = type_map, env = env}
827 fun map_pfuns_env f {pfuns, type_map,
828 env = SOME {ctxt, defs, types, funs, pfuns = pfuns_env,
829 ids, proving, vcs, path, prefix}} =
830 if proving then err_unfinished ()
832 {pfuns = pfuns, type_map = type_map,
833 env = SOME {ctxt = ctxt, defs = defs, types = types, funs = funs,
834 pfuns = f pfuns_env, ids = ids, proving = false, vcs = vcs,
835 path = path, prefix = prefix}};
837 fun add_proof_fun prep (s, (optty, raw_t)) thy =
838 VCs.map (fn data as {env, ...} =>
840 val (optty', prfx, map_pf) = (case env of
841 SOME {funs, prefix, ...} =>
842 (lookup funs (unprefix_pfun prefix s),
843 prefix, map_pfuns_env)
844 | NONE => (NONE, "", map_pfuns));
845 val optty'' = NONE |> upd_option optty |> upd_option optty';
846 val t = prep (Option.map (pfun_type thy prfx) optty'') raw_t;
847 val _ = (case fold_aterms (fn u =>
848 if is_Var u orelse is_Free u then insert (op =) u else I) t [] of
850 | ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^
851 "\nto be associated with proof function " ^ s ^
852 " contains free variable(s) " ^
853 commas (map (Syntax.string_of_term_global thy) ts)));
855 (check_pfun_type thy prfx s t optty optty';
856 if is_some optty'' orelse is_none env then
857 map_pf (Symtab.update_new (s, (optty'', t))) data
858 handle Symtab.DUP _ => error ("Proof function " ^ s ^
859 " already associated with function")
860 else error ("Undeclared proof function " ^ s))
863 fun check_mapping _ _ [] _ = ()
864 | check_mapping err s cmap cs =
865 (case duplicates (op = o apply2 fst) cmap of
866 [] => (case duplicates (op = o apply2 snd) cmap of
867 [] => (case subtract (op = o apsnd snd) cs cmap of
868 [] => (case subtract (op = o apfst snd) cmap cs of
870 | zs => err ("has extra " ^ s ^ "(s) " ^ commas zs))
871 | zs => err ("does not have " ^ s ^ "(s) " ^
872 commas (map snd zs)))
873 | zs => error ("Several SPARK names are mapped to " ^
874 commas (map snd zs)))
875 | zs => error ("The SPARK names " ^ commas (map fst zs) ^
876 " are mapped to more than one name"));
878 fun add_type (s, (T as Type (tyname, Ts), cmap)) thy =
879 let val cmap' = map (apsnd (Sign.intern_const thy)) cmap
883 {env = SOME _, ...} => err_unfinished ()
884 | {pfuns, type_map, env} =>
886 type_map = Symtab.update_new (s, (T, cmap')) type_map,
888 handle Symtab.DUP _ => error ("SPARK type " ^ s ^
889 " already associated with type")) |>
891 case BNF_LFP_Compat.get_constrs thy' tyname of
892 NONE => (case get_record_info thy' T of
894 | SOME {fields, ...} =>
895 (check_mapping (assoc_ty_err thy' T s) "field"
896 cmap' (map fst fields);
901 (fn (_, Type (_, [])) => ()
902 | (cname, _) => assoc_ty_err thy' T s
903 ("has illegal constructor " ^
904 Long_Name.base_name cname)) cs;
905 check_mapping (assoc_ty_err thy' T s) "constructor"
907 add_enum_type s tyname thy')
908 else assoc_ty_err thy' T s "is illegal")
910 | add_type (s, (T, _)) thy = assoc_ty_err thy T s "is illegal";
912 val is_closed = is_none o #env o VCs.get;
914 fun lookup_vc thy name_concl name =
916 {env = SOME {vcs, types, funs, pfuns, ids, ctxt, prefix, ...}, ...} =>
917 (case VCtab.lookup vcs name of
919 let val (pfuns', ctxt', ids') =
920 declare_missing_pfuns thy prefix funs pfuns vcs ids
922 SOME (ctxt @ [ctxt'],
923 mk_vc thy prefix types pfuns' ids' name_concl vc)
928 fun get_vcs thy name_concl = (case VCs.get thy of
929 {env = SOME {vcs, types, funs, pfuns, ids, ctxt, defs, prefix, ...}, ...} =>
930 let val (pfuns', ctxt', ids') =
931 declare_missing_pfuns thy prefix funs pfuns vcs ids
933 (ctxt @ [ctxt'], defs,
935 map (apsnd (mk_vc thy prefix types pfuns' ids' name_concl)))
937 | _ => ([], [], []));
939 fun mark_proved name thms = VCs.map (fn
941 env = SOME {ctxt, defs, types, funs, pfuns = pfuns_env,
942 ids, vcs, path, prefix, ...}} =>
945 env = SOME {ctxt = ctxt, defs = defs,
946 types = types, funs = funs, pfuns = pfuns_env,
949 vcs = print_open_vcs insert_break (VCtab.map_entry name
950 (fn (trace, _, ps, cs) => (trace, SOME thms, ps, cs)) vcs),
955 fun close incomplete thy =
956 thy |> VCs.map (fn {pfuns, type_map, env} =>
958 NONE => error "No SPARK environment is currently open"
959 | SOME {vcs, path, ...} =>
961 val (proved, unproved) = partition_vcs vcs;
962 val _ = Thm.consolidate (maps (#2 o snd) proved);
963 val (proved', proved'') =
964 List.partition (fn (_, (_, thms, _, _)) => Thm_Deps.has_skip_proof thms) proved;
966 if null unproved then ()
967 else (if incomplete then warning else error) (Pretty.string_of (pp_open_vcs unproved));
969 if null proved' then ()
970 else warning (Pretty.string_of (pp_vcs
971 "The following VCs are not marked as proved \
972 \because their proofs contain oracles:" proved'));
973 val prv_path = Path.ext "prv" path;
975 Export.export thy (Path.binding (prv_path, Position.none))
976 (proved'' |> map (fn (s, _) =>
977 XML.Text (snd (strip_number s) ^ " -- proved by " ^ Distribution.version ^ "\n")));
978 in {pfuns = pfuns, type_map = type_map, env = NONE} end))
982 (** set up verification conditions **)
984 fun partition_opt f =
986 fun part ys zs [] = (rev ys, rev zs)
987 | part ys zs (x :: xs) = (case f x of
988 SOME y => part (y :: ys) zs xs
989 | NONE => part ys (x :: zs) xs)
992 fun dest_def (id, (Substitution_Rule ([], Ident s, rhs))) = SOME (id, (s, rhs))
995 fun mk_rulename (s, i) = Binding.name (s ^ string_of_int i);
997 fun add_const prfx (s, ty) ((tab, ctxt), thy) =
999 val T = mk_type thy prfx ty;
1000 val b = Binding.name s;
1001 val c = Const (Sign.full_name thy b, T)
1004 ((Symtab.update (s, (c, ty)) tab, Name.declare s ctxt),
1005 Sign.add_consts [(b, T, NoSyn)] thy))
1008 fun add_def prfx types pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) =
1009 (case lookup consts s of
1012 val (t, ty') = term_of_expr thy prfx types pfuns ids e;
1013 val T = mk_type thy prfx ty;
1014 val T' = mk_type thy prfx ty';
1015 val _ = T = T' orelse
1016 error ("Declared type " ^ ty ^ " of " ^ s ^
1017 "\ndoes not match type " ^ ty' ^ " in definition");
1018 val id' = mk_rulename id;
1019 val ((t', (_, th)), lthy') = Named_Target.theory_init thy
1020 |> Specification.definition NONE [] []
1021 ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t)));
1023 Proof_Context.export_morphism lthy'
1024 (Proof_Context.init_global (Proof_Context.theory_of lthy'));
1026 ((id', Morphism.thm phi th),
1027 ((Symtab.update (s, (Morphism.term phi t', ty)) tab, Name.declare s ctxt),
1028 Local_Theory.exit_global lthy'))
1030 | NONE => error ("Undeclared constant " ^ s));
1032 fun add_var prfx (s, ty) (ids, thy) =
1033 let val ([Free p], ids') = mk_variables thy prfx [s] ty ids
1034 in (p, (ids', thy)) end;
1036 fun add_init_vars prfx vcs (ids_thy as ((tab, _), _)) =
1037 fold_map (add_var prfx)
1039 (fn s => case try (unsuffix "~") s of
1040 SOME s' => (case Symtab.lookup tab s' of
1041 SOME (_, ty) => SOME (s, ty)
1042 | NONE => error ("Undeclared identifier " ^ s'))
1044 (fold_vcs (add_expr_idents o snd) vcs []))
1047 fun is_trivial_vc ([], [(_, Ident "true")]) = true
1048 | is_trivial_vc _ = false;
1050 fun rulenames rules = commas
1051 (map (fn ((s, i), _) => s ^ "(" ^ string_of_int i ^ ")") rules);
1053 (* sort definitions according to their dependency *)
1054 fun sort_defs _ _ _ _ [] sdefs = rev sdefs
1055 | sort_defs prfx funs pfuns consts defs sdefs =
1056 (case find_first (fn (_, (_, e)) =>
1057 forall (is_some o lookup_prfx prfx pfuns)
1058 (add_expr_pfuns funs e []) andalso
1060 member (fn (s, (_, (s', _))) => s = s') sdefs id orelse
1062 (add_expr_idents e [])) defs of
1063 SOME d => sort_defs prfx funs pfuns consts
1064 (remove (op =) d defs) (d :: sdefs)
1065 | NONE => error ("Bad definitions: " ^ rulenames defs));
1069 {files = fn, header = fn, prfx = ""} (line 14 of "/usr/local/isabisac/src/HOL/SPARK/Tools/spark_commands.ML")
1070 {lin1 = ===== g_c_d.fdl =====
1072 ({("integer__last", "integer"), ("integer__size", "integer"), ("natural__last", "integer"), ("natural__size", "integer"), ("integer__first", "integer"), ("natural__first", "integer"),
1073 ("integer__base__last", "integer"), ("natural__base__last", "integer"), ("integer__base__first", "integer"), ("natural__base__first", "integer")},
1074 [("integer__size", "integer"), ("integer__last", "integer"), ("integer__first", "integer"), ("natural__size", "integer"), ("natural__last", "integer"), ("natural__first", "integer"),
1075 ("integer__base__last", "integer"), ("integer__base__first", "integer"), ("natural__base__last", "integer"), ("natural__base__first", "integer")]),
1076 funs = ({("gcd", (["integer", "integer"], "integer")), ("round__", (["real"], "integer"))}, [("gcd", (["integer", "integer"], "integer")), ("round__", (["real"], "integer"))]), types = ({}, []), vars =
1077 ({("c", "integer"), ("d", "integer"), ("m", "integer"), ("n", "integer")}, [("d", "integer"), ("c", "integer"), ("n", "integer"), ("m", "integer")])},
1078 lin2 = ===== g_c_d.rls =====
1079 ([(("g_c_d_rules", 1), Inference_Rule ([], Funct (">=", [Ident "integer__size", Number 0]))), (("g_c_d_rules", 2), Substitution_Rule ([], Ident "integer__first", Funct ("-", [Number 2147483648]))),
1080 (("g_c_d_rules", 3), Substitution_Rule ([], Ident "integer__last", Number 2147483647)), (("g_c_d_rules", 4), Substitution_Rule ([], Ident "integer__base__first", Funct ("-", [Number 2147483648]))),
1081 (("g_c_d_rules", 5), Substitution_Rule ([], Ident "integer__base__last", Number 2147483647)), (("g_c_d_rules", 6), Inference_Rule ([], Funct (">=", [Ident "natural__size", Number 0]))),
1082 (("g_c_d_rules", 7), Substitution_Rule ([], Ident "natural__first", Number 0)), (("g_c_d_rules", 8), Substitution_Rule ([], Ident "natural__last", Number 2147483647)),
1083 (("g_c_d_rules", 9), Substitution_Rule ([], Ident "natural__base__first", Funct ("-", [Number 2147483648]))), (("g_c_d_rules", 10), Substitution_Rule ([], Ident "natural__base__last", Number 2147483647))],
1084 [("g_c_d_rules", [(Ident "X", [("X", "any")]), (Funct ("<=", [Ident "X", Ident "Y"]), [("X", "ire"), ("Y", "ire")]), (Funct (">=", [Ident "X", Ident "Y"]), [("X", "ire"), ("Y", "ire")])])]),
1085 lin3 = ===== g_c_d.siv =====
1086 (("procedure", "Greatest_Common_Divisor.G_C_D"),
1087 [("path(s) from start to run-time check associated with statement of line 8", [("procedure_g_c_d_1", ([], [("1", Ident "true")]))]),
1088 ("path(s) from start to run-time check associated with statement of line 8", [("procedure_g_c_d_2", ([], [("1", Ident "true")]))]),
1089 ("path(s) from start to assertion of line 10", [("procedure_g_c_d_3", ([], [("1", Ident "true")]))]),
1090 ("path(s) from assertion of line 10 to assertion of line 10",
1091 [("procedure_g_c_d_4",
1092 ([("1", Funct (">=", [Ident "c", Number 0])), ("2", Funct (">", [Ident "d", Number 0])), ("3", Funct ("=", [Funct ("gcd", [Ident "c", Ident "d"]), Funct ("gcd", [Ident "m", Ident "n"])])),
1093 ("4", Funct (">=", [Ident "m", Number 0])), ("5", Funct ("<=", [Ident "m", Number 2147483647])), ("6", Funct ("<=", [Ident "n", Number 2147483647])), ("7", Funct (">", [Ident "n", Number 0])),
1094 ("8", Funct ("<=", [Ident "c", Number 2147483647])), ("9", Funct ("<=", [Ident "...", ...])), ("10", Funct ("...", [...])), ("11", Funct ("...", [...])), ("...", ...), ...],
1095 [("1", Funct (">", [Funct ("-", [Ident "c", Funct ("*", [Funct ("div", [Ident "c", Ident "..."]), Ident "d"])]), Number 0])),
1096 ("2", Funct ("=", [Funct ("gcd", [Ident "d", Funct ("-", [Ident "c", Funct ("...", [...])])]), Funct ("gcd", [Ident "m", Ident "n"])]))]))]),
1097 ("path(s) from assertion of line 10 to run-time check associated with \n statement of line 11", [("procedure_g_c_d_5", ([], [("1", Ident "true")]))]),
1098 ("path(s) from assertion of line 10 to run-time check associated with \n statement of line 12", [("procedure_g_c_d_6", ([], [("1", Ident "true")]))]),
1099 ("path(s) from assertion of line 10 to run-time check associated with \n statement of line 12", [("procedure_g_c_d_7", ([], [("1", Ident "true")]))]),
1100 ("path(s) from start to run-time check associated with statement of line 14", [("procedure_g_c_d_8", ([], [("1", Ident "true")]))]),
1101 ("path(s) from assertion of line 10 to run-time check associated with \n statement of line 14", [("procedure_g_c_d_9", ([], [("1", Ident "true")]))]),
1102 ("path(s) from start to finish", [("procedure_g_c_d_10", ([], [("1", Ident "true")]))]),
1103 ("path(s) from assertion of line 10 to finish",
1104 [("procedure_g_c_d_11",
1105 ([("1", Funct (">=", [Ident "c", Number 0])), ("2", Funct (">", [Ident "...", ...])), ("3", Funct ("...", [...])), ("4", Funct ("...", [...])), ("...", ...), ...],
1106 [("1", Funct ("=", [Ident "d", Funct ("...", [...])]))]))])])} (line 20 of "/usr/local/isabisac/src/HOL/SPARK/Tools/spark_commands.ML")
1109 fun set_vcs ({types, vars, consts, funs} : decls)
1110 (rules, _) ((_, ident), vcs) path opt_prfx thy =
1113 if opt_prfx = "" then
1114 space_implode "__" (Long_Name.explode (Long_Name.qualifier ident))
1116 val prfx = to_lower prfx';
1117 val {pfuns, ...} = VCs.get thy;
1118 val (defs, rules') = partition_opt dest_def rules;
1120 subtract (fn ((_, (s, _)), (s', _)) => s = s') defs (items consts);
1121 (* ignore all complex rules in rls files *)
1122 val (rules'', other_rules) =
1123 List.partition (complex_rule o snd) rules';
1124 val _ = if null rules'' then ()
1125 else warning ("Ignoring rules: " ^ rulenames rules'');
1127 val vcs' = VCtab.make (maps (fn (tr, vcs) =>
1128 map (fn (s, (ps, cs)) => (s, (tr, NONE, ps, cs)))
1129 (filter_out (is_trivial_vc o snd) vcs)) vcs);
1131 val _ = (case filter_out (is_some o lookup funs)
1132 (pfuns_of_vcs prfx funs pfuns vcs') of
1134 | fs => error ("Undeclared proof function(s) " ^ commas fs));
1136 val (((defs', vars''), ivars), (ids, thy')) =
1138 Symtab.update ("false", (\<^term>\<open>False\<close>, booleanN)) |>
1139 Symtab.update ("true", (\<^term>\<open>True\<close>, booleanN)),
1141 thy |> Sign.add_path
1142 ((if prfx' = "" then "" else prfx' ^ "__") ^ Long_Name.base_name ident)) |>
1143 fold (add_type_def prfx) (items types) |>
1144 fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>
1146 fold_map (add_def prfx types pfuns consts)
1147 (sort_defs prfx funs pfuns (Symtab.defined tab) defs []) ||>>
1148 fold_map (add_var prfx) (items vars) ||>>
1149 add_init_vars prfx vcs');
1152 [Element.Fixes (map (fn (s, T) =>
1153 (Binding.name s, SOME T, NoSyn)) (vars'' @ ivars)),
1154 Element.Assumes (map (fn (id, rl) =>
1155 ((mk_rulename id, []),
1156 [(term_of_rule thy' prfx types pfuns ids rl, [])]))
1158 Element.Notes ("", [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]
1161 set_env ctxt defs' types funs ids vcs' path prfx thy'