src/HOL/Mirabelle/lib/scripts/mirabelle.pl
author hoelzl
Tue Mar 26 12:20:58 2013 +0100 (2013-03-26)
changeset 51526 155263089e7b
parent 51293 05b1bbae748d
child 52059 2f970c7f722b
permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
boehmes@32382
     1
#
boehmes@32382
     2
# Author: Jasmin Blanchette and Sascha Boehme
boehmes@32382
     3
#
boehmes@32382
     4
# Testing tool for automated proof tools.
boehmes@32382
     5
#
boehmes@32382
     6
boehmes@32382
     7
use File::Basename;
boehmes@32382
     8
boehmes@32382
     9
# environment
boehmes@32382
    10
boehmes@32382
    11
my $isabelle_home = $ENV{'ISABELLE_HOME'};
boehmes@32382
    12
my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
boehmes@32382
    13
my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
boehmes@32385
    14
my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
boehmes@32382
    15
my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
boehmes@32382
    16
my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
boehmes@32521
    17
my $be_quiet = $ENV{'MIRABELLE_QUIET'};
boehmes@48703
    18
my $user_setup_file = $ENV{'MIRABELLE_SETUP_FILE'};
boehmes@32521
    19
my $actions = $ENV{'MIRABELLE_ACTIONS'};
boehmes@32382
    20
boehmes@32382
    21
my $mirabelle_thy = $mirabelle_home . "/Mirabelle";
boehmes@32382
    22
boehmes@32382
    23
boehmes@48703
    24
# argument
boehmes@32382
    25
boehmes@32521
    26
my $thy_file = $ARGV[0];
boehmes@48703
    27
boehmes@48703
    28
my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
boehmes@48703
    29
my $rand_suffix = join('', map { ('a'..'z')[rand(26)] } 1 .. 10);
boehmes@48703
    30
my $new_thy_name = $thy_name . "_Mirabelle_" . $rand_suffix;
boehmes@48703
    31
my $new_thy_file = $path . "/" . $new_thy_name . $ext;
boehmes@48703
    32
boehmes@48703
    33
boehmes@48703
    34
# setup
boehmes@48703
    35
boehmes@48703
    36
my $setup_file;
boehmes@48703
    37
my $setup_full_name;
boehmes@48703
    38
boehmes@48703
    39
if (-e $user_setup_file) {
boehmes@48703
    40
  $setup_file = undef;
boehmes@48703
    41
  my ($name, $path, $ext) = fileparse($user_setup_file, ".thy");
boehmes@48703
    42
  $setup_full_name = $path . "/" . $name;
boehmes@48703
    43
}
boehmes@48703
    44
else {
boehmes@48703
    45
boehmes@32382
    46
my $start_line = "0";
boehmes@32382
    47
my $end_line = "~1";
boehmes@32454
    48
if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) {
boehmes@32454
    49
  $thy_file = $1;
boehmes@32454
    50
  $start_line = $2;
boehmes@32454
    51
  $end_line = $3;
boehmes@32382
    52
}
boehmes@32382
    53
boehmes@32382
    54
my $setup_thy_name = $thy_name . "_Setup";
boehmes@32382
    55
my $setup_file = $output_path . "/" . $setup_thy_name . ".thy";
boehmes@32382
    56
my $log_file = $output_path . "/" . $thy_name . ".log";
boehmes@32382
    57
boehmes@32385
    58
my @action_files;
boehmes@32396
    59
my @action_names;
boehmes@32385
    60
foreach (split(/:/, $actions)) {
boehmes@32385
    61
  if (m/([^[]*)/) {
sultana@47730
    62
    push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\"";
boehmes@32396
    63
    push @action_names, $1;
boehmes@32385
    64
  }
boehmes@32385
    65
}
boehmes@32385
    66
my $tools = "";
boehmes@32385
    67
if ($#action_files >= 0) {
blanchet@38895
    68
  # uniquify
blanchet@38895
    69
  my $s = join ("\n", @action_files);
blanchet@38895
    70
  my @action_files = split(/\n/, $s . "\n" . $s);
blanchet@38895
    71
  %action_files = sort(@action_files);
wenzelm@51293
    72
  $tools = join("", map { "ML_file " . $_ . "\n" } (sort(keys(%action_files))));
boehmes@32385
    73
}
boehmes@32385
    74
boehmes@32382
    75
open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";
boehmes@32382
    76
boehmes@32382
    77
print SETUP_FILE <<END;
boehmes@32382
    78
theory "$setup_thy_name"
boehmes@32385
    79
imports "$mirabelle_thy" "$mirabelle_theory"
wenzelm@51293
    80
begin
wenzelm@51293
    81
boehmes@32385
    82
$tools
boehmes@32382
    83
sultana@46824
    84
setup {*
krauss@37378
    85
  Config.put_global Mirabelle.logfile "$log_file" #>
krauss@37378
    86
  Config.put_global Mirabelle.timeout $timeout #>
krauss@37378
    87
  Config.put_global Mirabelle.start_line $start_line #>
krauss@37378
    88
  Config.put_global Mirabelle.end_line $end_line
boehmes@32382
    89
*}
boehmes@32382
    90
boehmes@32382
    91
END
boehmes@32382
    92
sultana@46824
    93
@action_list = split(/:/, $actions);
sultana@46824
    94
sultana@46824
    95
foreach (reverse(@action_list)) {
boehmes@32382
    96
  if (m/([^[]*)(?:\[(.*)\])?/) {
boehmes@32382
    97
    my ($name, $settings_str) = ($1, $2 || "");
boehmes@32385
    98
    $name =~ s/^([a-z])/\U$1/;
boehmes@32385
    99
    print SETUP_FILE "setup {* Mirabelle_$name.invoke [";
boehmes@32382
   100
    my $sep = "";
boehmes@32382
   101
    foreach (split(/,/, $settings_str)) {
blanchet@41361
   102
      if (m/\s*([^=]*)\s*=\s*(.*)\s*/) {
boehmes@32382
   103
        print SETUP_FILE "$sep(\"$1\", \"$2\")";
boehmes@32382
   104
        $sep = ", ";
boehmes@32382
   105
      }
boehmes@32522
   106
      elsif (m/\s*(.*)\s*/) {
sultana@46824
   107
        print SETUP_FILE "$sep(\"$1\", \"\")";
sultana@46824
   108
        $sep = ", ";
boehmes@32522
   109
      }
boehmes@32382
   110
    }
boehmes@32382
   111
    print SETUP_FILE "] *}\n";
boehmes@32382
   112
  }
boehmes@32382
   113
}
boehmes@32382
   114
boehmes@32382
   115
print SETUP_FILE "\nend";
boehmes@32382
   116
close SETUP_FILE;
boehmes@32382
   117
boehmes@48703
   118
$setup_full_name = $output_path . "/" . $setup_thy_name;
boehmes@48703
   119
boehmes@48703
   120
open(LOG_FILE, ">$log_file");
boehmes@48703
   121
print LOG_FILE "Run of $new_thy_file with:\n";
boehmes@48703
   122
foreach $action  (@action_list) {
boehmes@48703
   123
  print LOG_FILE "  $action\n";
boehmes@48703
   124
}
boehmes@48703
   125
close(LOG_FILE);
boehmes@48703
   126
boehmes@48703
   127
}
boehmes@48703
   128
boehmes@32382
   129
boehmes@32382
   130
# modify target theory file
boehmes@32382
   131
boehmes@32382
   132
open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'";
boehmes@32382
   133
my @lines = <OLD_FILE>;
boehmes@32382
   134
close(OLD_FILE);
boehmes@32382
   135
boehmes@48703
   136
my $setup_import = substr("\"$setup_full_name\"" . (" " x 1000), 0, 1000);
blanchet@47728
   137
boehmes@32382
   138
my $thy_text = join("", @lines);
boehmes@32382
   139
my $old_len = length($thy_text);
boehmes@32395
   140
$thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g;
blanchet@47728
   141
$thy_text =~ s/(imports)(\s+)/$1 $setup_import$2/g;
boehmes@32382
   142
die "No 'imports' found" if length($thy_text) == $old_len;
boehmes@32382
   143
boehmes@32382
   144
open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'";
boehmes@32382
   145
print NEW_FILE $thy_text;
boehmes@32382
   146
close(NEW_FILE);
boehmes@32382
   147
boehmes@32382
   148
boehmes@32382
   149
# run isabelle
boehmes@32382
   150
boehmes@32521
   151
my $quiet = "";
boehmes@42070
   152
my $output_log = 1;
boehmes@32521
   153
if (defined $be_quiet and $be_quiet ne "") {
boehmes@32521
   154
  $quiet = " > /dev/null 2>&1";
boehmes@42070
   155
  $output_log = 0;
boehmes@32521
   156
}
boehmes@32382
   157
boehmes@42070
   158
if ($output_log) { print "Mirabelle: $thy_file\n"; }
boehmes@32498
   159
boehmes@32521
   160
my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
wenzelm@49549
   161
  "-e 'Unsynchronized.setmp Multithreading.max_threads 1 (Unsynchronized.setmp quick_and_dirty true use_thy) \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
boehmes@32521
   162
boehmes@48703
   163
if ($output_log) {
boehmes@48703
   164
  my $outcome = ($result ? "failure" : "success");
boehmes@48703
   165
  print "\nFinished:  $thy_file  [$outcome]\n";
boehmes@48703
   166
}
boehmes@32498
   167
boehmes@32498
   168
boehmes@32382
   169
# cleanup
boehmes@32382
   170
boehmes@48703
   171
if (defined $setup_file) {
boehmes@48703
   172
  unlink $setup_file;
boehmes@48703
   173
}
krauss@42033
   174
unlink $new_thy_file;
boehmes@32382
   175
krauss@42034
   176
exit ($result ? 1 : 0);