--- a/src/HOL/SPARK/Tools/spark_commands.ML Thu Apr 14 15:04:42 2011 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Fri Apr 15 15:33:57 2011 +0200
@@ -27,7 +27,7 @@
SPARK_VCs.set_vcs
(snd (Fdl_Parser.parse_declarations (Path.position fdl_path) (File.read fdl_path)))
(Fdl_Parser.parse_rules (Path.position rls_path) (File.read rls_path))
- (snd (snd (Fdl_Parser.parse_vcs header (Path.position vc_path) (File.read vc_path))))
+ (snd (Fdl_Parser.parse_vcs header (Path.position vc_path) (File.read vc_path)))
base thy
end;
@@ -39,6 +39,9 @@
Syntax.check_term ctxt) pf thy
end;
+fun add_spark_type_cmd (s, raw_typ) thy =
+ SPARK_VCs.add_type (s, Syntax.read_typ_global thy raw_typ) thy;
+
fun get_vc thy vc_name =
(case SPARK_VCs.lookup_vc thy vc_name of
SOME (ctxt, (_, proved, ctxt', stmt)) =>
@@ -117,6 +120,13 @@
(Toplevel.theory o fold add_proof_fun_cmd));
val _ =
+ Outer_Syntax.command "spark_types"
+ "associate SPARK types with types"
+ Keyword.thy_decl
+ (Scan.repeat1 (Parse.name --| Args.$$$ "=" -- Parse.typ) >>
+ (Toplevel.theory o fold add_spark_type_cmd));
+
+val _ =
Outer_Syntax.command "spark_vc"
"enter into proof mode for a specific verification condition"
Keyword.thy_goal