equal
deleted
inserted
replaced
9 # environment |
9 # environment |
10 |
10 |
11 my $isabelle_home = $ENV{'ISABELLE_HOME'}; |
11 my $isabelle_home = $ENV{'ISABELLE_HOME'}; |
12 my $mirabelle_home = $ENV{'MIRABELLE_HOME'}; |
12 my $mirabelle_home = $ENV{'MIRABELLE_HOME'}; |
13 my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'}; |
13 my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'}; |
|
14 my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'}; |
14 my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'}; |
15 my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'}; |
15 my $verbose = $ENV{'MIRABELLE_VERBOSE'}; |
16 my $verbose = $ENV{'MIRABELLE_VERBOSE'}; |
16 my $timeout = $ENV{'MIRABELLE_TIMEOUT'}; |
17 my $timeout = $ENV{'MIRABELLE_TIMEOUT'}; |
17 |
18 |
18 my $mirabelle_thy = $mirabelle_home . "/Mirabelle"; |
19 my $mirabelle_thy = $mirabelle_home . "/Mirabelle"; |
39 |
40 |
40 my $setup_thy_name = $thy_name . "_Setup"; |
41 my $setup_thy_name = $thy_name . "_Setup"; |
41 my $setup_file = $output_path . "/" . $setup_thy_name . ".thy"; |
42 my $setup_file = $output_path . "/" . $setup_thy_name . ".thy"; |
42 my $log_file = $output_path . "/" . $thy_name . ".log"; |
43 my $log_file = $output_path . "/" . $thy_name . ".log"; |
43 |
44 |
|
45 my @action_files; |
|
46 foreach (split(/:/, $actions)) { |
|
47 if (m/([^[]*)/) { |
|
48 push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\""; |
|
49 } |
|
50 } |
|
51 my $tools = ""; |
|
52 if ($#action_files >= 0) { |
|
53 $tools = "uses " . join(" ", @action_files); |
|
54 } |
|
55 |
44 open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'"; |
56 open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'"; |
45 |
57 |
46 print SETUP_FILE <<END; |
58 print SETUP_FILE <<END; |
47 theory "$setup_thy_name" |
59 theory "$setup_thy_name" |
48 imports "$mirabelle_thy" |
60 imports "$mirabelle_thy" "$mirabelle_theory" |
|
61 $tools |
49 begin |
62 begin |
50 |
63 |
51 setup {* |
64 setup {* |
52 Mirabelle.set_logfile "$log_file" #> |
65 Mirabelle.set_logfile "$log_file" #> |
53 Config.put_thy Mirabelle.timeout $timeout #> |
66 Config.put_thy Mirabelle.timeout $timeout #> |
59 END |
72 END |
60 |
73 |
61 foreach (split(/:/, $actions)) { |
74 foreach (split(/:/, $actions)) { |
62 if (m/([^[]*)(?:\[(.*)\])?/) { |
75 if (m/([^[]*)(?:\[(.*)\])?/) { |
63 my ($name, $settings_str) = ($1, $2 || ""); |
76 my ($name, $settings_str) = ($1, $2 || ""); |
64 print SETUP_FILE "setup {* Mirabelle.invoke \"$name\" ["; |
77 $name =~ s/^([a-z])/\U$1/; |
|
78 print SETUP_FILE "setup {* Mirabelle_$name.invoke ["; |
65 my $sep = ""; |
79 my $sep = ""; |
66 foreach (split(/,/, $settings_str)) { |
80 foreach (split(/,/, $settings_str)) { |
67 if (m/\s*(.*)\s*=\s*(.*)\s*/) { |
81 if (m/\s*(.*)\s*=\s*(.*)\s*/) { |
68 print SETUP_FILE "$sep(\"$1\", \"$2\")"; |
82 print SETUP_FILE "$sep(\"$1\", \"$2\")"; |
69 $sep = ", "; |
83 $sep = ", "; |