26 struct |
27 struct |
27 |
28 |
28 open Fdl_Parser; |
29 open Fdl_Parser; |
29 |
30 |
30 |
31 |
|
32 (** theory data **) |
|
33 |
|
34 fun err_unfinished () = error "An unfinished SPARK environment is still open." |
|
35 |
|
36 val strip_number = pairself implode o take_suffix Fdl_Lexer.is_digit o raw_explode; |
|
37 |
|
38 val name_ord = prod_ord string_ord (option_ord int_ord) o |
|
39 pairself (strip_number ##> Int.fromString); |
|
40 |
|
41 structure VCtab = Table(type key = string val ord = name_ord); |
|
42 |
|
43 structure VCs = Theory_Data |
|
44 ( |
|
45 type T = |
|
46 {pfuns: ((string list * string) option * term) Symtab.table, |
|
47 type_map: typ Symtab.table, |
|
48 env: |
|
49 {ctxt: Element.context_i list, |
|
50 defs: (binding * thm) list, |
|
51 types: fdl_type tab, |
|
52 funs: (string list * string) tab, |
|
53 ids: (term * string) Symtab.table * Name.context, |
|
54 proving: bool, |
|
55 vcs: (string * thm list option * |
|
56 (string * expr) list * (string * expr) list) VCtab.table, |
|
57 path: Path.T} option} |
|
58 val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE} |
|
59 val extend = I |
|
60 fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE}, |
|
61 {pfuns = pfuns2, type_map = type_map2, env = NONE}) = |
|
62 {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2), |
|
63 type_map = Symtab.merge (op =) (type_map1, type_map2), |
|
64 env = NONE} |
|
65 | merge _ = err_unfinished () |
|
66 ) |
|
67 |
|
68 |
31 (** utilities **) |
69 (** utilities **) |
|
70 |
|
71 val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode; |
|
72 |
|
73 val lcase_eq = (op =) o pairself (to_lower o Long_Name.base_name); |
32 |
74 |
33 fun mk_unop s t = |
75 fun mk_unop s t = |
34 let val T = fastype_of t |
76 let val T = fastype_of t |
35 in Const (s, T --> T) $ t end; |
77 in Const (s, T --> T) $ t end; |
36 |
78 |
42 in |
84 in |
43 Const (@{const_name Sigma}, setT --> (T --> HOLogic.mk_setT U) --> |
85 Const (@{const_name Sigma}, setT --> (T --> HOLogic.mk_setT U) --> |
44 HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u) |
86 HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u) |
45 end; |
87 end; |
46 |
88 |
|
89 fun get_type thy ty = |
|
90 let val {type_map, ...} = VCs.get thy |
|
91 in Symtab.lookup type_map ty end; |
|
92 |
47 fun mk_type _ "integer" = HOLogic.intT |
93 fun mk_type _ "integer" = HOLogic.intT |
48 | mk_type _ "boolean" = HOLogic.boolT |
94 | mk_type _ "boolean" = HOLogic.boolT |
49 | mk_type thy ty = Syntax.check_typ (ProofContext.init_global thy) |
95 | mk_type thy ty = |
50 (Type (Sign.full_name thy (Binding.name ty), [])); |
96 (case get_type thy ty of |
|
97 NONE => |
|
98 Syntax.check_typ (ProofContext.init_global thy) |
|
99 (Type (Sign.full_name thy (Binding.name ty), [])) |
|
100 | SOME T => T); |
51 |
101 |
52 val booleanN = "boolean"; |
102 val booleanN = "boolean"; |
53 val integerN = "integer"; |
103 val integerN = "integer"; |
54 |
|
55 fun mk_qual_name thy s s' = |
|
56 Sign.full_name thy (Binding.qualify true s (Binding.name s')); |
|
57 |
104 |
58 fun define_overloaded (def_name, eq) lthy = |
105 fun define_overloaded (def_name, eq) lthy = |
59 let |
106 let |
60 val ((c, _), rhs) = eq |> Syntax.check_term lthy |> |
107 val ((c, _), rhs) = eq |> Syntax.check_term lthy |> |
61 Logic.dest_equals |>> dest_Free; |
108 Logic.dest_equals |>> dest_Free; |
78 val T = mk_type thy ty; |
125 val T = mk_type thy ty; |
79 val (ys, ctxt') = Name.variants (map mangle_name xs) ctxt; |
126 val (ys, ctxt') = Name.variants (map mangle_name xs) ctxt; |
80 val zs = map (Free o rpair T) ys; |
127 val zs = map (Free o rpair T) ys; |
81 in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end; |
128 in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end; |
82 |
129 |
|
130 fun get_record_info thy T = (case Record.dest_recTs T of |
|
131 [(tyname, [@{typ unit}])] => |
|
132 Record.get_info thy (Long_Name.qualifier tyname) |
|
133 | _ => NONE); |
|
134 |
|
135 fun find_field fname = find_first (curry lcase_eq fname o fst); |
|
136 |
|
137 fun find_field' fname = get_first (fn (flds, fldty) => |
|
138 if member (op =) flds fname then SOME fldty else NONE); |
|
139 |
|
140 fun assoc_ty_err thy T s msg = |
|
141 error ("Type " ^ Syntax.string_of_typ_global thy T ^ |
|
142 " associated with SPARK type " ^ s ^ "\n" ^ msg); |
|
143 |
83 |
144 |
84 (** generate properties of enumeration types **) |
145 (** generate properties of enumeration types **) |
85 |
146 |
86 fun add_enum_type tyname els (tab, ctxt) thy = |
147 fun add_enum_type tyname tyname' thy = |
87 let |
148 let |
88 val tyb = Binding.name tyname; |
149 val {case_name, ...} = the (Datatype_Data.get_info thy tyname'); |
89 val tyname' = Sign.full_name thy tyb; |
150 val cs = map Const (the (Datatype_Data.get_constrs thy tyname')); |
|
151 val k = length cs; |
90 val T = Type (tyname', []); |
152 val T = Type (tyname', []); |
91 val case_name = mk_qual_name thy tyname (tyname ^ "_case"); |
|
92 val cs = map (fn s => Const (mk_qual_name thy tyname s, T)) els; |
|
93 val k = length els; |
|
94 val p = Const (@{const_name pos}, T --> HOLogic.intT); |
153 val p = Const (@{const_name pos}, T --> HOLogic.intT); |
95 val v = Const (@{const_name val}, HOLogic.intT --> T); |
154 val v = Const (@{const_name val}, HOLogic.intT --> T); |
96 val card = Const (@{const_name card}, |
155 val card = Const (@{const_name card}, |
97 HOLogic.mk_setT T --> HOLogic.natT) $ HOLogic.mk_UNIV T; |
156 HOLogic.mk_setT T --> HOLogic.natT) $ HOLogic.mk_UNIV T; |
98 |
157 |
193 [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1); |
249 [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1); |
194 |
250 |
195 val simp_att = [Attrib.internal (K Simplifier.simp_add)] |
251 val simp_att = [Attrib.internal (K Simplifier.simp_add)] |
196 |
252 |
197 in |
253 in |
198 ((fold (Symtab.update_new o apsnd (rpair tyname)) (els ~~ cs) tab, |
254 lthy' |> |
199 fold Name.declare els ctxt), |
255 Local_Theory.note |
200 lthy' |> |
256 ((Binding.name (tyname ^ "_card_UNIV"), simp_att), [card_UNIV]) ||>> |
201 Local_Theory.note |
257 Local_Theory.note |
202 ((Binding.name (tyname ^ "_card_UNIV"), simp_att), [card_UNIV]) ||>> |
258 ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>> |
203 Local_Theory.note |
259 Local_Theory.note |
204 ((Binding.name (tyname ^ "_pos"), simp_att), pos_eqs) ||>> |
260 ((Binding.name (tyname ^ "_val"), simp_att), val_eqs) ||>> |
205 Local_Theory.note |
261 Local_Theory.note |
206 ((Binding.name (tyname ^ "_val"), simp_att), val_eqs) ||>> |
262 ((Binding.name (tyname ^ "_first_el"), simp_att), [first_el]) ||>> |
207 Local_Theory.note |
263 Local_Theory.note |
208 ((Binding.name (tyname ^ "_first_el"), simp_att), [first_el]) ||>> |
264 ((Binding.name (tyname ^ "_last_el"), simp_att), [last_el]) |> snd |> |
209 Local_Theory.note |
265 Local_Theory.exit_global |
210 ((Binding.name (tyname ^ "_last_el"), simp_att), [last_el]) |> snd |> |
|
211 Local_Theory.exit_global) |
|
212 end; |
266 end; |
213 |
267 |
214 |
268 |
|
269 fun check_no_assoc thy s = case get_type thy s of |
|
270 NONE => () |
|
271 | SOME _ => error ("Cannot associate a type with " ^ s ^ |
|
272 "\nsince it is no record or enumeration type"); |
|
273 |
|
274 fun check_enum [] [] = NONE |
|
275 | check_enum els [] = SOME ("has no element(s) " ^ commas els) |
|
276 | check_enum [] cs = SOME ("has extra element(s) " ^ |
|
277 commas (map (Long_Name.base_name o fst) cs)) |
|
278 | check_enum (el :: els) ((cname, _) :: cs) = |
|
279 if lcase_eq (el, cname) then check_enum els cs |
|
280 else SOME ("either has no element " ^ el ^ |
|
281 " or it is at the wrong position"); |
|
282 |
215 fun add_type_def (s, Basic_Type ty) (ids, thy) = |
283 fun add_type_def (s, Basic_Type ty) (ids, thy) = |
216 (ids, |
284 (check_no_assoc thy s; |
217 Typedecl.abbrev_global (Binding.name s, [], NoSyn) |
285 (ids, |
218 (mk_type thy ty) thy |> snd) |
286 Typedecl.abbrev_global (Binding.name s, [], NoSyn) |
219 |
287 (mk_type thy ty) thy |> snd)) |
220 | add_type_def (s, Enum_Type els) (ids, thy) = add_enum_type s els ids thy |
288 |
|
289 | add_type_def (s, Enum_Type els) ((tab, ctxt), thy) = |
|
290 let |
|
291 val (thy', tyname) = (case get_type thy s of |
|
292 NONE => |
|
293 let |
|
294 val tyb = Binding.name s; |
|
295 val tyname = Sign.full_name thy tyb |
|
296 in |
|
297 (thy |> |
|
298 Datatype.add_datatype {strict = true, quiet = true} [s] |
|
299 [([], tyb, NoSyn, |
|
300 map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |> |
|
301 add_enum_type s tyname, |
|
302 tyname) |
|
303 end |
|
304 | SOME (T as Type (tyname, [])) => |
|
305 (case Datatype_Data.get_constrs thy tyname of |
|
306 NONE => assoc_ty_err thy T s "is not a datatype" |
|
307 | SOME cs => (case check_enum els cs of |
|
308 NONE => (thy, tyname) |
|
309 | SOME msg => assoc_ty_err thy T s msg))); |
|
310 val cs = map Const (the (Datatype_Data.get_constrs thy' tyname)) |
|
311 in |
|
312 ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab, |
|
313 fold Name.declare els ctxt), |
|
314 thy') |
|
315 end |
221 |
316 |
222 | add_type_def (s, Array_Type (argtys, resty)) (ids, thy) = |
317 | add_type_def (s, Array_Type (argtys, resty)) (ids, thy) = |
223 (ids, |
318 (check_no_assoc thy s; |
224 Typedecl.abbrev_global (Binding.name s, [], NoSyn) |
319 (ids, |
225 (foldr1 HOLogic.mk_prodT (map (mk_type thy) argtys) --> |
320 Typedecl.abbrev_global (Binding.name s, [], NoSyn) |
226 mk_type thy resty) thy |> snd) |
321 (foldr1 HOLogic.mk_prodT (map (mk_type thy) argtys) --> |
|
322 mk_type thy resty) thy |> snd)) |
227 |
323 |
228 | add_type_def (s, Record_Type fldtys) (ids, thy) = |
324 | add_type_def (s, Record_Type fldtys) (ids, thy) = |
229 (ids, |
325 (ids, |
230 Record.add_record true ([], Binding.name s) NONE |
326 let val fldTs = maps (fn (flds, ty) => |
231 (maps (fn (flds, ty) => |
327 map (rpair (mk_type thy ty)) flds) fldtys |
232 let val T = mk_type thy ty |
328 in case get_type thy s of |
233 in map (fn fld => (Binding.name fld, T, NoSyn)) flds |
329 NONE => |
234 end) fldtys) thy) |
330 Record.add_record true ([], Binding.name s) NONE |
|
331 (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy |
|
332 | SOME rT => |
|
333 (case get_record_info thy rT of |
|
334 NONE => assoc_ty_err thy rT s "is not a record type" |
|
335 | SOME {fields, ...} => |
|
336 (case subtract (lcase_eq o pairself fst) fldTs fields of |
|
337 [] => () |
|
338 | flds => assoc_ty_err thy rT s ("has extra field(s) " ^ |
|
339 commas (map (Long_Name.base_name o fst) flds)); |
|
340 map (fn (fld, T) => |
|
341 case AList.lookup lcase_eq fields fld of |
|
342 NONE => assoc_ty_err thy rT s ("has no field " ^ fld) |
|
343 | SOME U => T = U orelse assoc_ty_err thy rT s |
|
344 ("has field " ^ |
|
345 fld ^ " whose type\n" ^ |
|
346 Syntax.string_of_typ_global thy U ^ |
|
347 "\ndoes not match declared type\n" ^ |
|
348 Syntax.string_of_typ_global thy T)) fldTs; |
|
349 thy)) |
|
350 end) |
235 |
351 |
236 | add_type_def (s, Pending_Type) (ids, thy) = |
352 | add_type_def (s, Pending_Type) (ids, thy) = |
237 (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd); |
353 (check_no_assoc thy s; |
|
354 (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd)); |
238 |
355 |
239 |
356 |
240 fun term_of_expr thy types funs pfuns = |
357 fun term_of_expr thy types funs pfuns = |
241 let |
358 let |
242 fun tm_of vs (Funct ("->", [e, e'])) = |
359 fun tm_of vs (Funct ("->", [e, e'])) = |
321 |
438 |
322 (* record field selection *) |
439 (* record field selection *) |
323 (case try (unprefix "fld_") s of |
440 (case try (unprefix "fld_") s of |
324 SOME fname => (case es of |
441 SOME fname => (case es of |
325 [e] => |
442 [e] => |
326 let val (t, rcdty) = tm_of vs e |
443 let |
327 in case lookup types rcdty of |
444 val (t, rcdty) = tm_of vs e; |
328 SOME (Record_Type fldtys) => |
445 val rT = mk_type thy rcdty |
329 (case get_first (fn (flds, fldty) => |
446 in case (get_record_info thy rT, lookup types rcdty) of |
330 if member (op =) flds fname then SOME fldty |
447 (SOME {fields, ...}, SOME (Record_Type fldtys)) => |
331 else NONE) fldtys of |
448 (case (find_field fname fields, |
332 SOME fldty => |
449 find_field' fname fldtys) of |
333 (Const (mk_qual_name thy rcdty fname, |
450 (SOME (fname', fT), SOME fldty) => |
334 mk_type thy rcdty --> mk_type thy fldty) $ t, |
451 (Const (fname', rT --> fT) $ t, fldty) |
335 fldty) |
452 | _ => error ("Record " ^ rcdty ^ |
336 | NONE => error ("Record " ^ rcdty ^ |
|
337 " has no field named " ^ fname)) |
453 " has no field named " ^ fname)) |
338 | _ => error (rcdty ^ " is not a record type") |
454 | _ => error (rcdty ^ " is not a record type") |
339 end |
455 end |
340 | _ => error ("Function " ^ s ^ " expects one argument")) |
456 | _ => error ("Function " ^ s ^ " expects one argument")) |
341 | NONE => |
457 | NONE => |
347 let |
463 let |
348 val (t, rcdty) = tm_of vs e; |
464 val (t, rcdty) = tm_of vs e; |
349 val rT = mk_type thy rcdty; |
465 val rT = mk_type thy rcdty; |
350 val (u, fldty) = tm_of vs e'; |
466 val (u, fldty) = tm_of vs e'; |
351 val fT = mk_type thy fldty |
467 val fT = mk_type thy fldty |
352 in case lookup types rcdty of |
468 in case get_record_info thy rT of |
353 SOME (Record_Type fldtys) => |
469 SOME {fields, ...} => |
354 (case get_first (fn (flds, fldty) => |
470 (case find_field fname fields of |
355 if member (op =) flds fname then SOME fldty |
471 SOME (fname', fU) => |
356 else NONE) fldtys of |
472 if fT = fU then |
357 SOME fldty' => |
473 (Const (fname' ^ "_update", |
358 if fldty = fldty' then |
|
359 (Const (mk_qual_name thy rcdty (fname ^ "_update"), |
|
360 (fT --> fT) --> rT --> rT) $ |
474 (fT --> fT) --> rT --> rT) $ |
361 Abs ("x", fT, u) $ t, |
475 Abs ("x", fT, u) $ t, |
362 rcdty) |
476 rcdty) |
363 else error ("Type " ^ fldty ^ |
477 else error ("Type\n" ^ |
364 " does not match type " ^ fldty' ^ " of field " ^ |
478 Syntax.string_of_typ_global thy fT ^ |
365 fname) |
479 "\ndoes not match type\n" ^ |
|
480 Syntax.string_of_typ_global thy fU ^ |
|
481 "\nof field " ^ fname) |
366 | NONE => error ("Record " ^ rcdty ^ |
482 | NONE => error ("Record " ^ rcdty ^ |
367 " has no field named " ^ fname)) |
483 " has no field named " ^ fname)) |
368 | _ => error (rcdty ^ " is not a record type") |
484 | _ => error (rcdty ^ " is not a record type") |
369 end |
485 end |
370 | _ => error ("Function " ^ s ^ " expects two arguments")) |
486 | _ => error ("Function " ^ s ^ " expects two arguments")) |
429 end |
545 end |
430 | _ => error (ty ^ " is not an array type") |
546 | _ => error (ty ^ " is not an array type") |
431 end |
547 end |
432 |
548 |
433 | tm_of vs (Record (s, flds)) = |
549 | tm_of vs (Record (s, flds)) = |
434 (case lookup types s of |
550 let |
435 SOME (Record_Type fldtys) => |
551 val T = mk_type thy s; |
436 let |
552 val {extension = (ext_name, _), fields, ...} = |
437 val flds' = map (apsnd (tm_of vs)) flds; |
553 (case get_record_info thy T of |
438 val fnames = maps fst fldtys; |
554 NONE => error (s ^ " is not a record type") |
439 val fnames' = map fst flds; |
555 | SOME info => info); |
440 val (fvals, ftys) = split_list (map (fn s' => |
556 val flds' = map (apsnd (tm_of vs)) flds; |
441 case AList.lookup (op =) flds' s' of |
557 val fnames = map (Long_Name.base_name o fst) fields; |
442 SOME fval_ty => fval_ty |
558 val fnames' = map fst flds; |
443 | NONE => error ("Field " ^ s' ^ " missing in record " ^ s)) |
559 val (fvals, ftys) = split_list (map (fn s' => |
444 fnames); |
560 case AList.lookup lcase_eq flds' s' of |
445 val _ = (case subtract (op =) fnames fnames' of |
561 SOME fval_ty => fval_ty |
446 [] => () |
562 | NONE => error ("Field " ^ s' ^ " missing in record " ^ s)) |
447 | xs => error ("Extra field(s) " ^ commas xs ^ |
563 fnames); |
448 " in record " ^ s)); |
564 val _ = (case subtract lcase_eq fnames fnames' of |
449 val _ = (case duplicates (op =) fnames' of |
565 [] => () |
450 [] => () |
566 | xs => error ("Extra field(s) " ^ commas xs ^ |
451 | xs => error ("Duplicate field(s) " ^ commas xs ^ |
567 " in record " ^ s)); |
452 " in record " ^ s)) |
568 val _ = (case duplicates (op =) fnames' of |
453 in |
569 [] => () |
454 (list_comb |
570 | xs => error ("Duplicate field(s) " ^ commas xs ^ |
455 (Const (mk_qual_name thy s (s ^ "_ext"), |
571 " in record " ^ s)) |
456 map (mk_type thy) ftys @ [HOLogic.unitT] ---> |
572 in |
457 mk_type thy s), |
573 (list_comb |
458 fvals @ [HOLogic.unit]), |
574 (Const (ext_name, |
459 s) |
575 map (mk_type thy) ftys @ [HOLogic.unitT] ---> T), |
460 end |
576 fvals @ [HOLogic.unit]), |
461 | _ => error (s ^ " is not a record type")) |
577 s) |
|
578 end |
462 |
579 |
463 | tm_of vs (Array (s, default, assocs)) = |
580 | tm_of vs (Array (s, default, assocs)) = |
464 (case lookup types s of |
581 (case lookup types s of |
465 SOME (Array_Type (idxtys, elty)) => |
582 SOME (Array_Type (idxtys, elty)) => |
466 let |
583 let |
590 end); |
707 end); |
591 |
708 |
592 |
709 |
593 (** the VC store **) |
710 (** the VC store **) |
594 |
711 |
595 fun err_unfinished () = error "An unfinished SPARK environment is still open." |
|
596 |
|
597 fun err_vcs names = error (Pretty.string_of |
712 fun err_vcs names = error (Pretty.string_of |
598 (Pretty.big_list "The following verification conditions have not been proved:" |
713 (Pretty.big_list "The following verification conditions have not been proved:" |
599 (map Pretty.str names))) |
714 (map Pretty.str names))) |
600 |
715 |
601 val strip_number = pairself implode o take_suffix Fdl_Lexer.is_digit o raw_explode; |
|
602 |
|
603 val name_ord = prod_ord string_ord (option_ord int_ord) o |
|
604 pairself (strip_number ##> Int.fromString); |
|
605 |
|
606 structure VCtab = Table(type key = string val ord = name_ord); |
|
607 |
|
608 structure VCs = Theory_Data |
|
609 ( |
|
610 type T = |
|
611 {pfuns: ((string list * string) option * term) Symtab.table, |
|
612 env: |
|
613 {ctxt: Element.context_i list, |
|
614 defs: (binding * thm) list, |
|
615 types: fdl_type tab, |
|
616 funs: (string list * string) tab, |
|
617 ids: (term * string) Symtab.table * Name.context, |
|
618 proving: bool, |
|
619 vcs: (string * thm list option * |
|
620 (string * expr) list * (string * expr) list) VCtab.table, |
|
621 path: Path.T} option} |
|
622 val empty : T = {pfuns = Symtab.empty, env = NONE} |
|
623 val extend = I |
|
624 fun merge ({pfuns = pfuns1, env = NONE}, {pfuns = pfuns2, env = NONE}) = |
|
625 {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2), |
|
626 env = NONE} |
|
627 | merge _ = err_unfinished () |
|
628 ) |
|
629 |
|
630 fun set_env (env as {funs, ...}) thy = VCs.map (fn |
716 fun set_env (env as {funs, ...}) thy = VCs.map (fn |
631 {pfuns, env = NONE} => |
717 {pfuns, type_map, env = NONE} => |
632 {pfuns = check_pfuns_types thy funs pfuns, env = SOME env} |
718 {pfuns = check_pfuns_types thy funs pfuns, |
|
719 type_map = type_map, |
|
720 env = SOME env} |
633 | _ => err_unfinished ()) thy; |
721 | _ => err_unfinished ()) thy; |
634 |
722 |
635 fun mk_pat s = (case Int.fromString s of |
723 fun mk_pat s = (case Int.fromString s of |
636 SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))] |
724 SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))] |
637 | NONE => error ("Bad conclusion identifier: C" ^ s)); |
725 | NONE => error ("Bad conclusion identifier: C" ^ s)); |
670 end; |
758 end; |
671 |
759 |
672 fun add_proof_fun prep (s, (optty, raw_t)) thy = |
760 fun add_proof_fun prep (s, (optty, raw_t)) thy = |
673 VCs.map (fn |
761 VCs.map (fn |
674 {env = SOME {proving = true, ...}, ...} => err_unfinished () |
762 {env = SOME {proving = true, ...}, ...} => err_unfinished () |
675 | {pfuns, env} => |
763 | {pfuns, type_map, env} => |
676 let |
764 let |
677 val optty' = (case env of |
765 val optty' = (case env of |
678 SOME {funs, ...} => lookup funs s |
766 SOME {funs, ...} => lookup funs s |
679 | NONE => NONE); |
767 | NONE => NONE); |
680 val optty'' = NONE |> upd_option optty |> upd_option optty'; |
768 val optty'' = NONE |> upd_option optty |> upd_option optty'; |
681 val t = prep (Option.map (pfun_type thy) optty'') raw_t |
769 val t = prep (Option.map (pfun_type thy) optty'') raw_t; |
|
770 val _ = (case fold_aterms (fn u => |
|
771 if is_Var u orelse is_Free u then insert (op =) u else I) t [] of |
|
772 [] => () |
|
773 | ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^ |
|
774 "\nto be associated with proof function " ^ s ^ |
|
775 " contains free variable(s) " ^ |
|
776 commas (map (Syntax.string_of_term_global thy) ts))); |
682 in |
777 in |
683 (check_pfun_type thy s t optty optty'; |
778 (check_pfun_type thy s t optty optty'; |
684 if is_some optty'' orelse is_none env then |
779 if is_some optty'' orelse is_none env then |
685 {pfuns = Symtab.update_new (s, (optty'', t)) pfuns, |
780 {pfuns = Symtab.update_new (s, (optty'', t)) pfuns, |
|
781 type_map = type_map, |
686 env = env} |
782 env = env} |
687 handle Symtab.DUP _ => error ("Proof function " ^ s ^ |
783 handle Symtab.DUP _ => error ("Proof function " ^ s ^ |
688 " already associated with function") |
784 " already associated with function") |
689 else error ("Undeclared proof function " ^ s)) |
785 else error ("Undeclared proof function " ^ s)) |
690 end) thy; |
786 end) thy; |
691 |
787 |
|
788 fun add_type (s, T as Type (tyname, Ts)) thy = |
|
789 thy |> |
|
790 VCs.map (fn |
|
791 {env = SOME _, ...} => err_unfinished () |
|
792 | {pfuns, type_map, env} => |
|
793 {pfuns = pfuns, |
|
794 type_map = Symtab.update_new (s, T) type_map, |
|
795 env = env} |
|
796 handle Symtab.DUP _ => error ("SPARK type " ^ s ^ |
|
797 " already associated with type")) |> |
|
798 (fn thy' => |
|
799 case Datatype_Data.get_constrs thy' tyname of |
|
800 NONE => thy' |
|
801 | SOME cs => |
|
802 if null Ts then |
|
803 (map |
|
804 (fn (_, Type (_, [])) => () |
|
805 | (cname, _) => assoc_ty_err thy T s |
|
806 ("has illegal constructor " ^ |
|
807 Long_Name.base_name cname)) cs; |
|
808 add_enum_type s tyname thy') |
|
809 else assoc_ty_err thy T s "is illegal") |
|
810 | add_type (s, T) thy = assoc_ty_err thy T s "is illegal"; |
|
811 |
692 val is_closed = is_none o #env o VCs.get; |
812 val is_closed = is_none o #env o VCs.get; |
693 |
813 |
694 fun lookup_vc thy name = |
814 fun lookup_vc thy name = |
695 (case VCs.get thy of |
815 (case VCs.get thy of |
696 {env = SOME {vcs, types, funs, ids, ctxt, ...}, pfuns} => |
816 {env = SOME {vcs, types, funs, ids, ctxt, ...}, pfuns, ...} => |
697 (case VCtab.lookup vcs name of |
817 (case VCtab.lookup vcs name of |
698 SOME vc => |
818 SOME vc => |
699 let val (pfuns', ctxt', ids') = |
819 let val (pfuns', ctxt', ids') = |
700 declare_missing_pfuns thy funs pfuns vcs ids |
820 declare_missing_pfuns thy funs pfuns vcs ids |
701 in SOME (ctxt @ [ctxt'], mk_vc thy types funs pfuns' ids' vc) end |
821 in SOME (ctxt @ [ctxt'], mk_vc thy types funs pfuns' ids' vc) end |
702 | NONE => NONE) |
822 | NONE => NONE) |
703 | _ => NONE); |
823 | _ => NONE); |
704 |
824 |
705 fun get_vcs thy = (case VCs.get thy of |
825 fun get_vcs thy = (case VCs.get thy of |
706 {env = SOME {vcs, types, funs, ids, ctxt, defs, ...}, pfuns} => |
826 {env = SOME {vcs, types, funs, ids, ctxt, defs, ...}, pfuns, ...} => |
707 let val (pfuns', ctxt', ids') = |
827 let val (pfuns', ctxt', ids') = |
708 declare_missing_pfuns thy funs pfuns vcs ids |
828 declare_missing_pfuns thy funs pfuns vcs ids |
709 in |
829 in |
710 (ctxt @ [ctxt'], defs, |
830 (ctxt @ [ctxt'], defs, |
711 VCtab.dest vcs |> |
831 VCtab.dest vcs |> |
712 map (apsnd (mk_vc thy types funs pfuns' ids'))) |
832 map (apsnd (mk_vc thy types funs pfuns' ids'))) |
713 end |
833 end |
714 | _ => ([], [], [])); |
834 | _ => ([], [], [])); |
715 |
835 |
716 fun mark_proved name thms = VCs.map (fn |
836 fun mark_proved name thms = VCs.map (fn |
717 {pfuns, env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} => |
837 {pfuns, type_map, |
|
838 env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} => |
718 {pfuns = pfuns, |
839 {pfuns = pfuns, |
|
840 type_map = type_map, |
719 env = SOME {ctxt = ctxt, defs = defs, |
841 env = SOME {ctxt = ctxt, defs = defs, |
720 types = types, funs = funs, ids = ids, |
842 types = types, funs = funs, ids = ids, |
721 proving = true, |
843 proving = true, |
722 vcs = VCtab.map_entry name (fn (trace, _, ps, cs) => |
844 vcs = VCtab.map_entry name (fn (trace, _, ps, cs) => |
723 (trace, SOME thms, ps, cs)) vcs, |
845 (trace, SOME thms, ps, cs)) vcs, |
724 path = path}} |
846 path = path}} |
725 | x => x); |
847 | x => x); |
726 |
848 |
727 fun close thy = VCs.map (fn |
849 fun close thy = |
728 {pfuns, env = SOME {vcs, path, ...}} => |
850 thy |> |
729 (case VCtab.fold_rev (fn vc as (_, (_, p, _, _)) => |
851 VCs.map (fn |
730 (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of |
852 {pfuns, type_map, env = SOME {vcs, path, ...}} => |
731 (proved, []) => |
853 (case VCtab.fold_rev (fn vc as (_, (_, p, _, _)) => |
732 (Thm.join_proofs (maps (the o #2 o snd) proved); |
854 (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of |
733 File.write (Path.ext "prv" path) |
855 (proved, []) => |
734 (concat (map (fn (s, _) => snd (strip_number s) ^ |
856 (Thm.join_proofs (maps (the o #2 o snd) proved); |
735 " -- proved by " ^ Distribution.version ^ "\n") proved)); |
857 File.write (Path.ext "prv" path) |
736 {pfuns = pfuns, env = NONE}) |
858 (concat (map (fn (s, _) => snd (strip_number s) ^ |
737 | (_, unproved) => err_vcs (map fst unproved)) |
859 " -- proved by " ^ Distribution.version ^ "\n") proved)); |
738 | x => x) thy; |
860 {pfuns = pfuns, type_map = type_map, env = NONE}) |
|
861 | (_, unproved) => err_vcs (map fst unproved)) |
|
862 | _ => error "No SPARK environment is currently open") |> |
|
863 Sign.parent_path; |
739 |
864 |
740 |
865 |
741 (** set up verification conditions **) |
866 (** set up verification conditions **) |
742 |
867 |
743 fun partition_opt f = |
868 fun partition_opt f = |