1 #!/usr/bin/perl -w |
|
2 |
|
3 use strict; |
|
4 use File::Basename; |
|
5 |
|
6 # Taken from http://www.skywayradio.com/tech/perl/trim_blanks.html |
|
7 sub trim { |
|
8 my @out = @_; |
|
9 for (@out) { |
|
10 s/^\s+//; |
|
11 s/\s+$//; |
|
12 } |
|
13 return wantarray ? @out : $out[0]; |
|
14 } |
|
15 |
|
16 sub quote { |
|
17 my $str = pop; |
|
18 return "\"" . $str . "\""; |
|
19 } |
|
20 |
|
21 sub print_usage_and_quit { |
|
22 print STDERR "Usage: mirabelle actions file1.thy...\n" . |
|
23 " actions: action1:...:actionN\n" . |
|
24 " action: name or name[key1=value1,...,keyM=valueM]\n"; |
|
25 exit 1; |
|
26 } |
|
27 |
|
28 my $num_args = $#ARGV + 1; |
|
29 if ($num_args < 2) { |
|
30 print_usage_and_quit(); |
|
31 } |
|
32 |
|
33 my @action_names; |
|
34 my @action_settings; |
|
35 |
|
36 foreach (split(/:/, $ARGV[0])) { |
|
37 my %settings; |
|
38 |
|
39 $_ =~ /([^[]*)(?:\[(.*)\])?/; |
|
40 my ($name, $settings_str) = ($1, $2 || ""); |
|
41 my @setting_strs = split(/,/, $settings_str); |
|
42 foreach (@setting_strs) { |
|
43 $_ =~ /(.*)=(.*)/; |
|
44 my $key = $1; |
|
45 my $value = $2; |
|
46 $settings{trim($key)} = trim($value); |
|
47 } |
|
48 |
|
49 push @action_names, trim($name); |
|
50 push @action_settings, \%settings; |
|
51 } |
|
52 |
|
53 my $output_path = "/tmp/mirabelle"; # FIXME: generate path |
|
54 my $mirabellesetup_thy_name = $output_path . "/MirabelleSetup"; |
|
55 my $mirabellesetup_file = $mirabellesetup_thy_name . ".thy"; |
|
56 my $mirabelle_log_file = $output_path . "/mirabelle.log"; |
|
57 |
|
58 mkdir $output_path, 0755; |
|
59 |
|
60 open(FILE, ">$mirabellesetup_file") |
|
61 || die "Could not create file '$mirabellesetup_file'"; |
|
62 |
|
63 my $invoke_lines; |
|
64 |
|
65 for my $i (0 .. $#action_names) { |
|
66 my $settings_str = ""; |
|
67 my $settings = $action_settings[$i]; |
|
68 my $key; |
|
69 my $value; |
|
70 |
|
71 while (($key, $value) = each(%$settings)) { |
|
72 $settings_str .= "(" . quote ($key) . ", " . quote ($value) . "), "; |
|
73 } |
|
74 $settings_str =~ s/, $//; |
|
75 |
|
76 $invoke_lines .= "setup {* Mirabelle.invoke \"$action_names[$i]\" "; |
|
77 $invoke_lines .= "[$settings_str] *}\n" |
|
78 } |
|
79 |
|
80 print FILE <<EOF; |
|
81 theory MirabelleSetup |
|
82 imports Mirabelle |
|
83 begin |
|
84 |
|
85 setup {* Mirabelle.set_logfile "$mirabelle_log_file" *} |
|
86 |
|
87 $invoke_lines |
|
88 |
|
89 end |
|
90 EOF |
|
91 |
|
92 my $root_text = ""; |
|
93 my @new_thy_files; |
|
94 |
|
95 for my $i (1 .. $num_args - 1) { |
|
96 my $old_thy_file = $ARGV[$i]; |
|
97 my ($base, $dir, $ext) = fileparse($old_thy_file, "\.thy"); |
|
98 my $new_thy_name = $base . "Mirabelle"; |
|
99 my $new_thy_file = $dir . $new_thy_name . $ext; |
|
100 |
|
101 open(OLD_FILE, "<$old_thy_file") |
|
102 || die "Cannot open file $old_thy_file"; |
|
103 my @lines = <OLD_FILE>; |
|
104 close(OLD_FILE); |
|
105 |
|
106 my $thy_text = join("", @lines); |
|
107 my $old_len = length($thy_text); |
|
108 $thy_text =~ s/\btheory\b[^\n]*\s*\bimports\s/theory $new_thy_name\nimports "$mirabellesetup_thy_name" /gm; |
|
109 die "No 'imports' found" if length($thy_text) == $old_len; |
|
110 |
|
111 open(NEW_FILE, ">$new_thy_file"); |
|
112 print NEW_FILE $thy_text; |
|
113 close(NEW_FILE); |
|
114 |
|
115 $root_text .= "use_thy \"" . $dir . $new_thy_name . "\";\n"; |
|
116 |
|
117 push @new_thy_files, $new_thy_file; |
|
118 } |
|
119 |
|
120 my $root_file = "ROOT_mirabelle.ML"; |
|
121 open(ROOT_FILE, ">$root_file") || die "Cannot open file $root_file"; |
|
122 print ROOT_FILE $root_text; |
|
123 close(ROOT_FILE); |
|
124 |
|
125 system "isabelle-process -e 'use \"ROOT_mirabelle.ML\";' -f -q HOL"; |
|
126 |
|
127 # unlink $mirabellesetup_file; |
|
128 unlink $root_file; |
|
129 unlink @new_thy_files; |
|