author | wenzelm |
Fri, 13 May 2016 20:24:10 +0200 | |
changeset 63092 | a949b2a5f51d |
parent 62969 | 9f394a16c557 |
child 63093 | 3081f7719df7 |
permissions | -rw-r--r-- |
41561 | 1 |
(* Title: HOL/SPARK/Tools/spark_commands.ML |
2 |
Author: Stefan Berghofer |
|
3 |
Copyright: secunet Security Networks AG |
|
4 |
||
5 |
Isar commands for handling SPARK/Ada verification conditions. |
|
6 |
*) |
|
56798
939e88e79724
Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents:
56334
diff
changeset
|
7 |
|
55789 | 8 |
structure SPARK_Commands: sig end = |
41561 | 9 |
struct |
10 |
||
56798
939e88e79724
Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents:
56334
diff
changeset
|
11 |
fun spark_open header (files, prfx) thy = |
48908
713f24d7a40f
added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents:
48167
diff
changeset
|
12 |
let |
55788
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
51658
diff
changeset
|
13 |
val ([{src_path, lines = vc_lines, pos = vc_pos, ...}: Token.file, |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
51658
diff
changeset
|
14 |
{lines = fdl_lines, pos = fdl_pos, ...}, |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
51658
diff
changeset
|
15 |
{lines = rls_lines, pos = rls_pos, ...}], thy') = files thy; |
56208 | 16 |
val base = fst (Path.split_ext (File.full_path (Resources.master_directory thy') src_path)); |
48908
713f24d7a40f
added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents:
48167
diff
changeset
|
17 |
in |
713f24d7a40f
added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents:
48167
diff
changeset
|
18 |
SPARK_VCs.set_vcs |
55788
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
51658
diff
changeset
|
19 |
(snd (Fdl_Parser.parse_declarations fdl_pos (cat_lines fdl_lines))) |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
51658
diff
changeset
|
20 |
(Fdl_Parser.parse_rules rls_pos (cat_lines rls_lines)) |
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
51658
diff
changeset
|
21 |
(snd (Fdl_Parser.parse_vcs header vc_pos (cat_lines vc_lines))) |
48908
713f24d7a40f
added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents:
48167
diff
changeset
|
22 |
base prfx thy' |
713f24d7a40f
added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents:
48167
diff
changeset
|
23 |
end; |
713f24d7a40f
added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents:
48167
diff
changeset
|
24 |
|
41561 | 25 |
fun add_proof_fun_cmd pf thy = |
42361 | 26 |
let val ctxt = Proof_Context.init_global thy |
41561 | 27 |
in SPARK_VCs.add_proof_fun |
28 |
(fn optT => Syntax.parse_term ctxt #> |
|
29 |
the_default I (Option.map Type.constraint optT) #> |
|
30 |
Syntax.check_term ctxt) pf thy |
|
31 |
end; |
|
32 |
||
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
43702
diff
changeset
|
33 |
fun add_spark_type_cmd (s, (raw_typ, cmap)) thy = |
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
43702
diff
changeset
|
34 |
SPARK_VCs.add_type (s, (Syntax.read_typ_global thy raw_typ, cmap)) thy; |
42356
e8777e3ea6ef
Added command for associating user-defined types with SPARK types.
berghofe
parents:
42003
diff
changeset
|
35 |
|
41561 | 36 |
fun get_vc thy vc_name = |
48167 | 37 |
(case SPARK_VCs.lookup_vc thy false vc_name of |
41561 | 38 |
SOME (ctxt, (_, proved, ctxt', stmt)) => |
41896
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41887
diff
changeset
|
39 |
if is_some proved then |
41561 | 40 |
error ("The verification condition " ^ |
41 |
quote vc_name ^ " has already been proved.") |
|
42 |
else (ctxt @ [ctxt'], stmt) |
|
43 |
| NONE => error ("There is no verification condition " ^ |
|
44 |
quote vc_name ^ ".")); |
|
45 |
||
46 |
fun prove_vc vc_name lthy = |
|
47 |
let |
|
42361 | 48 |
val thy = Proof_Context.theory_of lthy; |
41561 | 49 |
val (ctxt, stmt) = get_vc thy vc_name |
50 |
in |
|
63092 | 51 |
Specification.theorem true Thm.theoremK NONE |
41896
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41887
diff
changeset
|
52 |
(fn thmss => (Local_Theory.background_theory |
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41887
diff
changeset
|
53 |
(SPARK_VCs.mark_proved vc_name (flat thmss)))) |
50787
065c684130ad
disable interactive mode of Specification.theorem with its slow printing of results;
wenzelm
parents:
49444
diff
changeset
|
54 |
(Binding.name vc_name, []) [] ctxt stmt false lthy |
41561 | 55 |
end; |
56 |
||
41896
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41887
diff
changeset
|
57 |
fun string_of_status NONE = "(unproved)" |
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41887
diff
changeset
|
58 |
| string_of_status (SOME _) = "(proved)"; |
41561 | 59 |
|
51658
21c10672633b
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
50787
diff
changeset
|
60 |
fun show_status thy (p, f) = |
41561 | 61 |
let |
48167 | 62 |
val (context, defs, vcs) = SPARK_VCs.get_vcs thy true; |
41561 | 63 |
|
64 |
val vcs' = AList.coalesce (op =) (map_filter |
|
65 |
(fn (name, (trace, status, ctxt, stmt)) => |
|
66 |
if p status then |
|
67 |
SOME (trace, (name, status, ctxt, stmt)) |
|
68 |
else NONE) vcs); |
|
69 |
||
51658
21c10672633b
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
50787
diff
changeset
|
70 |
val ctxt = thy |> |
42361 | 71 |
Proof_Context.init_global |> |
41561 | 72 |
Context.proof_map (fold Element.init context) |
73 |
in |
|
41592 | 74 |
[Pretty.str "Context:", |
75 |
Pretty.chunks (maps (Element.pretty_ctxt ctxt) context), |
|
41561 | 76 |
|
41592 | 77 |
Pretty.str "Definitions:", |
43547
f3a8476285c6
clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
wenzelm
parents:
42396
diff
changeset
|
78 |
Pretty.chunks (map (fn (b, th) => Pretty.block |
f3a8476285c6
clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
wenzelm
parents:
42396
diff
changeset
|
79 |
[Binding.pretty b, Pretty.str ":", |
41561 | 80 |
Pretty.brk 1, |
61268 | 81 |
Thm.pretty_thm ctxt th]) |
41592 | 82 |
defs), |
41561 | 83 |
|
41592 | 84 |
Pretty.str "Verification conditions:", |
85 |
Pretty.chunks2 (maps (fn (trace, vcs'') => |
|
41561 | 86 |
Pretty.str trace :: |
87 |
map (fn (name, status, context', stmt) => |
|
88 |
Pretty.big_list (name ^ " " ^ f status) |
|
89 |
(Element.pretty_ctxt ctxt context' @ |
|
41592 | 90 |
Element.pretty_stmt ctxt stmt)) vcs'') vcs')] |> |
56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
56208
diff
changeset
|
91 |
Pretty.writeln_chunks2 |
51658
21c10672633b
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
50787
diff
changeset
|
92 |
end; |
41561 | 93 |
|
94 |
val _ = |
|
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59927
diff
changeset
|
95 |
Outer_Syntax.command @{command_keyword spark_open_vcg} |
48908
713f24d7a40f
added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents:
48167
diff
changeset
|
96 |
"open a new SPARK environment and load a SPARK-generated .vcg file" |
56798
939e88e79724
Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents:
56334
diff
changeset
|
97 |
(Resources.provide_parse_files "spark_open_vcg" -- Parse.parname |
48908
713f24d7a40f
added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents:
48167
diff
changeset
|
98 |
>> (Toplevel.theory o spark_open Fdl_Lexer.vcg_header)); |
713f24d7a40f
added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents:
48167
diff
changeset
|
99 |
|
713f24d7a40f
added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents:
48167
diff
changeset
|
100 |
val _ = |
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59927
diff
changeset
|
101 |
Outer_Syntax.command @{command_keyword spark_open} |
48908
713f24d7a40f
added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents:
48167
diff
changeset
|
102 |
"open a new SPARK environment and load a SPARK-generated .siv file" |
56798
939e88e79724
Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents:
56334
diff
changeset
|
103 |
(Resources.provide_parse_files "spark_open" -- Parse.parname |
48908
713f24d7a40f
added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
wenzelm
parents:
48167
diff
changeset
|
104 |
>> (Toplevel.theory o spark_open Fdl_Lexer.siv_header)); |
41561 | 105 |
|
106 |
val pfun_type = Scan.option |
|
107 |
(Args.parens (Parse.list1 Parse.name) --| Args.colon -- Parse.name); |
|
108 |
||
109 |
val _ = |
|
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59927
diff
changeset
|
110 |
Outer_Syntax.command @{command_keyword spark_proof_functions} |
41586 | 111 |
"associate SPARK proof functions with terms" |
41561 | 112 |
(Scan.repeat1 (Parse.name -- (pfun_type --| Args.$$$ "=" -- Parse.term)) >> |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46725
diff
changeset
|
113 |
(Toplevel.theory o fold add_proof_fun_cmd)); |
41561 | 114 |
|
115 |
val _ = |
|
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59927
diff
changeset
|
116 |
Outer_Syntax.command @{command_keyword spark_types} |
42356
e8777e3ea6ef
Added command for associating user-defined types with SPARK types.
berghofe
parents:
42003
diff
changeset
|
117 |
"associate SPARK types with types" |
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
43702
diff
changeset
|
118 |
(Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ -- |
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
43702
diff
changeset
|
119 |
Scan.optional (Args.parens (Parse.list1 |
62969 | 120 |
(Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.name)))) [])) >> |
42356
e8777e3ea6ef
Added command for associating user-defined types with SPARK types.
berghofe
parents:
42003
diff
changeset
|
121 |
(Toplevel.theory o fold add_spark_type_cmd)); |
e8777e3ea6ef
Added command for associating user-defined types with SPARK types.
berghofe
parents:
42003
diff
changeset
|
122 |
|
e8777e3ea6ef
Added command for associating user-defined types with SPARK types.
berghofe
parents:
42003
diff
changeset
|
123 |
val _ = |
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59927
diff
changeset
|
124 |
Outer_Syntax.local_theory_to_proof @{command_keyword spark_vc} |
41586 | 125 |
"enter into proof mode for a specific verification condition" |
59927 | 126 |
(Parse.name >> prove_vc); |
41561 | 127 |
|
128 |
val _ = |
|
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59927
diff
changeset
|
129 |
Outer_Syntax.command @{command_keyword spark_status} |
41586 | 130 |
"show the name and state of all loaded verification conditions" |
41561 | 131 |
(Scan.optional |
132 |
(Args.parens |
|
41896
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41887
diff
changeset
|
133 |
( Args.$$$ "proved" >> K (is_some, K "") |
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41887
diff
changeset
|
134 |
|| Args.$$$ "unproved" >> K (is_none, K ""))) |
51658
21c10672633b
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
50787
diff
changeset
|
135 |
(K true, string_of_status) >> (fn args => |
21c10672633b
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
50787
diff
changeset
|
136 |
Toplevel.keep (fn state => show_status (Toplevel.theory_of state) args))) |
41561 | 137 |
|
138 |
val _ = |
|
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59927
diff
changeset
|
139 |
Outer_Syntax.command @{command_keyword spark_end} |
41586 | 140 |
"close the current SPARK environment" |
48167 | 141 |
(Scan.optional (@{keyword "("} |-- Parse.!!! |
142 |
(Parse.reserved "incomplete" --| @{keyword ")"}) >> K true) false >> |
|
143 |
(Toplevel.theory o SPARK_VCs.close)); |
|
41561 | 144 |
|
55789 | 145 |
val _ = Theory.setup (Theory.at_end (fn thy => |
41561 | 146 |
let |
147 |
val _ = SPARK_VCs.is_closed thy |
|
56798
939e88e79724
Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents:
56334
diff
changeset
|
148 |
orelse error ("Found the end of the theory, " ^ |
41561 | 149 |
"but the last SPARK environment is still open.") |
55789 | 150 |
in NONE end)); |
41561 | 151 |
|
152 |
end; |