author | boehmes |
Fri, 21 Aug 2009 09:46:14 +0200 | |
changeset 32383 | 521065a499c6 |
parent 32382 | src/HOL/ex/Mirabelle/lib/scripts/mirabelle.pl@98674ac811c4 |
child 32385 | 594890623c46 |
permissions | -rw-r--r-- |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
1 |
# |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
2 |
# Author: Jasmin Blanchette and Sascha Boehme |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
3 |
# |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
4 |
# Testing tool for automated proof tools. |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
5 |
# |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
6 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
7 |
use File::Basename; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
8 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
9 |
# environment |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
10 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
11 |
my $isabelle_home = $ENV{'ISABELLE_HOME'}; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
12 |
my $mirabelle_home = $ENV{'MIRABELLE_HOME'}; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
13 |
my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'}; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
14 |
my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'}; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
15 |
my $verbose = $ENV{'MIRABELLE_VERBOSE'}; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
16 |
my $timeout = $ENV{'MIRABELLE_TIMEOUT'}; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
17 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
18 |
my $mirabelle_thy = $mirabelle_home . "/Mirabelle"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
19 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
20 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
21 |
# arguments |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
22 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
23 |
my $actions = $ARGV[0]; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
24 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
25 |
my $thy_file = $ARGV[1]; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
26 |
my $start_line = "0"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
27 |
my $end_line = "~1"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
28 |
if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) { # FIXME |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
29 |
my $thy_file = $1; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
30 |
my $start_line = $2; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
31 |
my $end_line = $3; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
32 |
} |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
33 |
my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy"); |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
34 |
my $new_thy_name = $thy_name . "_Mirabelle"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
35 |
my $new_thy_file = $output_path . "/" . $new_thy_name . $ext; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
36 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
37 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
38 |
# setup |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
39 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
40 |
my $setup_thy_name = $thy_name . "_Setup"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
41 |
my $setup_file = $output_path . "/" . $setup_thy_name . ".thy"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
42 |
my $log_file = $output_path . "/" . $thy_name . ".log"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
43 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
44 |
open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
45 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
46 |
print SETUP_FILE <<END; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
47 |
theory "$setup_thy_name" |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
48 |
imports "$mirabelle_thy" |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
49 |
begin |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
50 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
51 |
setup {* |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
52 |
Mirabelle.set_logfile "$log_file" #> |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
53 |
Config.put_thy Mirabelle.timeout $timeout #> |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
54 |
Config.put_thy Mirabelle.verbose $verbose #> |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
55 |
Config.put_thy Mirabelle.start_line $start_line #> |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
56 |
Config.put_thy Mirabelle.end_line $end_line |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
57 |
*} |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
58 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
59 |
END |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
60 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
61 |
foreach (split(/:/, $actions)) { |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
62 |
if (m/([^[]*)(?:\[(.*)\])?/) { |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
63 |
my ($name, $settings_str) = ($1, $2 || ""); |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
64 |
print SETUP_FILE "setup {* Mirabelle.invoke \"$name\" ["; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
65 |
my $sep = ""; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
66 |
foreach (split(/,/, $settings_str)) { |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
67 |
if (m/\s*(.*)\s*=\s*(.*)\s*/) { |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
68 |
print SETUP_FILE "$sep(\"$1\", \"$2\")"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
69 |
$sep = ", "; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
70 |
} |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
71 |
} |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
72 |
print SETUP_FILE "] *}\n"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
73 |
} |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
74 |
} |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
75 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
76 |
print SETUP_FILE "\nend"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
77 |
close SETUP_FILE; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
78 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
79 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
80 |
# modify target theory file |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
81 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
82 |
open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
83 |
my @lines = <OLD_FILE>; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
84 |
close(OLD_FILE); |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
85 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
86 |
my $thy_text = join("", @lines); |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
87 |
my $old_len = length($thy_text); |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
88 |
$thy_text =~ s/\btheory\b[^\n]*\s*\bimports\s/theory $new_thy_name\nimports "$setup_thy_name" /gm; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
89 |
die "No 'imports' found" if length($thy_text) == $old_len; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
90 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
91 |
open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
92 |
print NEW_FILE $thy_text; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
93 |
close(NEW_FILE); |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
94 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
95 |
my $root_file = "$output_path/ROOT_$thy_name.ML"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
96 |
open(ROOT_FILE, ">$root_file") || die "Cannot create file '$root_file'"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
97 |
print ROOT_FILE "use_thy \"$output_path/$new_thy_name\";\n"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
98 |
close(ROOT_FILE); |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
99 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
100 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
101 |
# run isabelle |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
102 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
103 |
my $r = system "$isabelle_home/bin/isabelle-process " . |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
104 |
"-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
105 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
106 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
107 |
# cleanup |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
108 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
109 |
unlink $root_file; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
110 |
unlink $new_thy_file; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
111 |
unlink $setup_file; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
112 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
113 |
exit $r; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
114 |