author | berghofe |
Tue, 28 Feb 2012 11:10:09 +0100 | |
changeset 46725 | d34ec0512dfb |
parent 43702 | 24fb44c1086a |
child 46961 | 5c6955f487e5 |
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 |
*) |
|
7 |
||
8 |
signature SPARK_COMMANDS = |
|
9 |
sig |
|
10 |
val setup: theory -> theory |
|
11 |
end |
|
12 |
||
13 |
structure SPARK_Commands: SPARK_COMMANDS = |
|
14 |
struct |
|
15 |
||
43702
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43547
diff
changeset
|
16 |
(* FIXME proper Thy_Load.use_file, also for fdl_path and rls_path (!?) *) |
42396
0869ce2006eb
Package prefix is now taken into account when looking up user-defined
berghofe
parents:
42361
diff
changeset
|
17 |
fun spark_open (vc_name, prfx) thy = |
41561 | 18 |
let |
43702
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43547
diff
changeset
|
19 |
val ((vc_path, vc_id), vc_text) = Thy_Load.load_file thy (Path.explode vc_name); |
41887
ececcbd08d35
simplified Thy_Info.check_file -- discontinued load path;
wenzelm
parents:
41592
diff
changeset
|
20 |
val (base, header) = |
ececcbd08d35
simplified Thy_Info.check_file -- discontinued load path;
wenzelm
parents:
41592
diff
changeset
|
21 |
(case Path.split_ext vc_path of |
41561 | 22 |
(base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ()) |
23 |
| (base, "siv") => (base, Fdl_Lexer.siv_header >> K ()) |
|
24 |
| _ => error "File name must end with .vcg or .siv"); |
|
25 |
val fdl_path = Path.ext "fdl" base; |
|
26 |
val rls_path = Path.ext "rls" base; |
|
27 |
in |
|
28 |
SPARK_VCs.set_vcs |
|
41948 | 29 |
(snd (Fdl_Parser.parse_declarations (Path.position fdl_path) (File.read fdl_path))) |
30 |
(Fdl_Parser.parse_rules (Path.position rls_path) (File.read rls_path)) |
|
43702
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43547
diff
changeset
|
31 |
(snd (Fdl_Parser.parse_vcs header (Path.position vc_path) vc_text)) |
42396
0869ce2006eb
Package prefix is now taken into account when looking up user-defined
berghofe
parents:
42361
diff
changeset
|
32 |
base prfx thy |
41561 | 33 |
end; |
34 |
||
35 |
fun add_proof_fun_cmd pf thy = |
|
42361 | 36 |
let val ctxt = Proof_Context.init_global thy |
41561 | 37 |
in SPARK_VCs.add_proof_fun |
38 |
(fn optT => Syntax.parse_term ctxt #> |
|
39 |
the_default I (Option.map Type.constraint optT) #> |
|
40 |
Syntax.check_term ctxt) pf thy |
|
41 |
end; |
|
42 |
||
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
43702
diff
changeset
|
43 |
fun add_spark_type_cmd (s, (raw_typ, cmap)) thy = |
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
43702
diff
changeset
|
44 |
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
|
45 |
|
41561 | 46 |
fun get_vc thy vc_name = |
47 |
(case SPARK_VCs.lookup_vc thy vc_name of |
|
48 |
SOME (ctxt, (_, proved, ctxt', stmt)) => |
|
41896
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41887
diff
changeset
|
49 |
if is_some proved then |
41561 | 50 |
error ("The verification condition " ^ |
51 |
quote vc_name ^ " has already been proved.") |
|
52 |
else (ctxt @ [ctxt'], stmt) |
|
53 |
| NONE => error ("There is no verification condition " ^ |
|
54 |
quote vc_name ^ ".")); |
|
55 |
||
56 |
fun prove_vc vc_name lthy = |
|
57 |
let |
|
42361 | 58 |
val thy = Proof_Context.theory_of lthy; |
41561 | 59 |
val (ctxt, stmt) = get_vc thy vc_name |
60 |
in |
|
61 |
Specification.theorem Thm.theoremK NONE |
|
41896
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41887
diff
changeset
|
62 |
(fn thmss => (Local_Theory.background_theory |
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41887
diff
changeset
|
63 |
(SPARK_VCs.mark_proved vc_name (flat thmss)))) |
41561 | 64 |
(Binding.name vc_name, []) ctxt stmt true lthy |
65 |
end; |
|
66 |
||
41896
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41887
diff
changeset
|
67 |
fun string_of_status NONE = "(unproved)" |
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41887
diff
changeset
|
68 |
| string_of_status (SOME _) = "(proved)"; |
41561 | 69 |
|
70 |
fun show_status (p, f) = Toplevel.no_timing o Toplevel.keep (fn state => |
|
71 |
let |
|
72 |
val thy = Toplevel.theory_of state; |
|
73 |
||
74 |
val (context, defs, vcs) = SPARK_VCs.get_vcs thy; |
|
75 |
||
76 |
val vcs' = AList.coalesce (op =) (map_filter |
|
77 |
(fn (name, (trace, status, ctxt, stmt)) => |
|
78 |
if p status then |
|
79 |
SOME (trace, (name, status, ctxt, stmt)) |
|
80 |
else NONE) vcs); |
|
81 |
||
82 |
val ctxt = state |> |
|
83 |
Toplevel.theory_of |> |
|
42361 | 84 |
Proof_Context.init_global |> |
41561 | 85 |
Context.proof_map (fold Element.init context) |
86 |
in |
|
41592 | 87 |
[Pretty.str "Context:", |
88 |
Pretty.chunks (maps (Element.pretty_ctxt ctxt) context), |
|
41561 | 89 |
|
41592 | 90 |
Pretty.str "Definitions:", |
43547
f3a8476285c6
clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
wenzelm
parents:
42396
diff
changeset
|
91 |
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
|
92 |
[Binding.pretty b, Pretty.str ":", |
41561 | 93 |
Pretty.brk 1, |
94 |
Display.pretty_thm ctxt th]) |
|
41592 | 95 |
defs), |
41561 | 96 |
|
41592 | 97 |
Pretty.str "Verification conditions:", |
98 |
Pretty.chunks2 (maps (fn (trace, vcs'') => |
|
41561 | 99 |
Pretty.str trace :: |
100 |
map (fn (name, status, context', stmt) => |
|
101 |
Pretty.big_list (name ^ " " ^ f status) |
|
102 |
(Element.pretty_ctxt ctxt context' @ |
|
41592 | 103 |
Element.pretty_stmt ctxt stmt)) vcs'') vcs')] |> |
104 |
Pretty.chunks2 |> Pretty.writeln |
|
41561 | 105 |
end); |
106 |
||
107 |
val _ = |
|
108 |
Outer_Syntax.command "spark_open" |
|
41586 | 109 |
"open a new SPARK environment and load a SPARK-generated .vcg or .siv file" |
41561 | 110 |
Keyword.thy_decl |
42396
0869ce2006eb
Package prefix is now taken into account when looking up user-defined
berghofe
parents:
42361
diff
changeset
|
111 |
(Parse.name -- Parse.parname >> (Toplevel.theory o spark_open)); |
41561 | 112 |
|
113 |
val pfun_type = Scan.option |
|
114 |
(Args.parens (Parse.list1 Parse.name) --| Args.colon -- Parse.name); |
|
115 |
||
116 |
val _ = |
|
117 |
Outer_Syntax.command "spark_proof_functions" |
|
41586 | 118 |
"associate SPARK proof functions with terms" |
41561 | 119 |
Keyword.thy_decl |
120 |
(Scan.repeat1 (Parse.name -- (pfun_type --| Args.$$$ "=" -- Parse.term)) >> |
|
121 |
(Toplevel.theory o fold add_proof_fun_cmd)); |
|
122 |
||
123 |
val _ = |
|
42356
e8777e3ea6ef
Added command for associating user-defined types with SPARK types.
berghofe
parents:
42003
diff
changeset
|
124 |
Outer_Syntax.command "spark_types" |
e8777e3ea6ef
Added command for associating user-defined types with SPARK types.
berghofe
parents:
42003
diff
changeset
|
125 |
"associate SPARK types with types" |
e8777e3ea6ef
Added command for associating user-defined types with SPARK types.
berghofe
parents:
42003
diff
changeset
|
126 |
Keyword.thy_decl |
46725
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
43702
diff
changeset
|
127 |
(Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ -- |
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
43702
diff
changeset
|
128 |
Scan.optional (Args.parens (Parse.list1 |
d34ec0512dfb
Added infrastructure for mapping SPARK field / constructor names
berghofe
parents:
43702
diff
changeset
|
129 |
(Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.xname)))) [])) >> |
42356
e8777e3ea6ef
Added command for associating user-defined types with SPARK types.
berghofe
parents:
42003
diff
changeset
|
130 |
(Toplevel.theory o fold add_spark_type_cmd)); |
e8777e3ea6ef
Added command for associating user-defined types with SPARK types.
berghofe
parents:
42003
diff
changeset
|
131 |
|
e8777e3ea6ef
Added command for associating user-defined types with SPARK types.
berghofe
parents:
42003
diff
changeset
|
132 |
val _ = |
41561 | 133 |
Outer_Syntax.command "spark_vc" |
41586 | 134 |
"enter into proof mode for a specific verification condition" |
41561 | 135 |
Keyword.thy_goal |
136 |
(Parse.name >> (fn name => |
|
137 |
(Toplevel.print o Toplevel.local_theory_to_proof NONE (prove_vc name)))); |
|
138 |
||
139 |
val _ = |
|
140 |
Outer_Syntax.improper_command "spark_status" |
|
41586 | 141 |
"show the name and state of all loaded verification conditions" |
41561 | 142 |
Keyword.diag |
143 |
(Scan.optional |
|
144 |
(Args.parens |
|
41896
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41887
diff
changeset
|
145 |
( Args.$$$ "proved" >> K (is_some, K "") |
582cccdda0ed
spark_end now joins proofs of VCs before writing *.prv file.
berghofe
parents:
41887
diff
changeset
|
146 |
|| Args.$$$ "unproved" >> K (is_none, K ""))) |
41561 | 147 |
(K true, string_of_status) >> show_status); |
148 |
||
149 |
val _ = |
|
150 |
Outer_Syntax.command "spark_end" |
|
41586 | 151 |
"close the current SPARK environment" |
41561 | 152 |
Keyword.thy_decl |
153 |
(Scan.succeed (Toplevel.theory SPARK_VCs.close)); |
|
154 |
||
155 |
val setup = Theory.at_end (fn thy => |
|
156 |
let |
|
157 |
val _ = SPARK_VCs.is_closed thy |
|
158 |
orelse error ("Found the end of the theory, " ^ |
|
159 |
"but the last SPARK environment is still open.") |
|
160 |
in NONE end); |
|
161 |
||
162 |
end; |