Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: mirabelle.pl Sprache: Shell

Original von: Isabelle^©

#
# Author: Jasmin Blanchette and Sascha Boehme
#
# Testing tool for automated proof tools.
#

use File::Basename;

# environment

my $isabelle_home = $ENV{'ISABELLE_HOME'};
my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
my $mirabelle_dir = $ENV{'MIRABELLE_DIR'};
my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
my $be_quiet = $ENV{'MIRABELLE_QUIET'};
my $user_setup_file = $ENV{'MIRABELLE_SETUP_FILE'};
my $actions = $ENV{'MIRABELLE_ACTIONS'};

my $mirabelle_thy = $mirabelle_home . "/Mirabelle";

# argument

my $thy_file = $ARGV[0];

my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
my $rand_suffix = join('', map { ('a'..'z')[rand(26)] } 1 .. 10);
my $new_thy_name = $thy_name . "_Mirabelle_" . $rand_suffix;
my $new_thy_file = $path . "/" . $new_thy_name . $ext;

# setup

my $setup_file;
my $setup_full_name;

if (-e $user_setup_file) {
  $setup_file = undef;
  my ($name, $path, $ext) = fileparse($user_setup_file, ".thy");
  $setup_full_name = $path . "/" . $name;
}
else {

my $start_line = "0";
my $end_line = "~1";
if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) {
  $thy_file = $1;
  $start_line = $2;
  $end_line = $3;
}

my $setup_thy_name = $thy_name . "_Setup";
my $setup_file = $output_path . "/" . $setup_thy_name . ".thy";
my $log_file = $output_path . "/" . $thy_name . ".log";

my @action_files;
my @action_names;
foreach (split(/:/, $actions)) {
  if (m/([^[]*)/) {
    push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\"";
    push @action_names, $1;
  }
}
my $tools = "";
if ($#action_files >= 0) {
  # uniquify
  my $s = join ("\n", @action_files);
  my @action_files = split(/\n/, $s . "\n" . $s);
  %action_files = sort(@action_files);
  $tools = join("", map { "ML_file " . $_ . "\n" } (sort(keys(%action_files))));
}

open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";

print SETUP_FILE <<END;
theory "$setup_thy_name"
imports "$mirabelle_thy" "$mirabelle_theory"
begin

$tools

setup {*
  Config.put_global Mirabelle.logfile "$log_file" #>
  Config.put_global Mirabelle.timeout $timeout #>
  Config.put_global Mirabelle.start_line $start_line #>
  Config.put_global Mirabelle.end_line $end_line
*}

END

@action_list = split(/:/, $actions);

foreach (reverse(@action_list)) {
  if (m/([^[]*)(?:\[(.*)\])?/) {
    my ($name, $settings_str) = ($1, $2 || "");
    $name =~ s/^([a-z])/\U$1/;
    print SETUP_FILE "setup {* Mirabelle_$name.invoke [";
    my $sep = "";
    foreach (split(/,/, $settings_str)) {
      if (m/\s*([^=]*)\s*=\s*(.*)\s*/) {
        print SETUP_FILE "$sep(\"$1\", \"$2\")";
        $sep = ", ";
      }
      elsif (m/\s*(.*)\s*/) {
        print SETUP_FILE "$sep(\"$1\", \"\")";
        $sep = ", ";
      }
    }
    print SETUP_FILE "] *}\n";
  }
}

print SETUP_FILE "\nend";
close SETUP_FILE;

$setup_full_name = $output_path . "/" . $setup_thy_name;

open(LOG_FILE, ">$log_file");
print LOG_FILE "Run of $new_thy_file with:\n";
foreach $action  (@action_list) {
  print LOG_FILE " $action\n";
}
close(LOG_FILE);

}

# modify target theory file

open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'";
my @lines = <OLD_FILE>;
close(OLD_FILE);

my $setup_import = substr("\"$setup_full_name\"" . (" " x 1000), 0, 1000);

my $thy_text = join("", @lines);
my $old_len = length($thy_text);
$thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g;
$thy_text =~ s/\b$thy_name\./$new_thy_name./g;
$thy_text =~ s/(imports)(\s+)/$1 $setup_import$2/g;
die "No 'imports' found" if length($thy_text) == $old_len;

open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'";
print NEW_FILE $thy_text;
close(NEW_FILE);

# run isabelle

my $quiet = "";
my $output_log = 1;
if (defined $be_quiet and $be_quiet ne "") {
  $quiet = " > /dev/null 2>&1";
  $output_log = 0;
}

if ($output_log) { print "Mirabelle: $thy_file\n"; }

my $cmd =
  "isabelle process -o quick_and_dirty -o threads=1" .
  " -T \"$path/$new_thy_name\" " .
  ($mirabelle_dir ? "-d " . $mirabelle_dir . " " : "") .
  "-l $mirabelle_logic" . $quiet;
my $result = system "bash", "-c", $cmd;

if ($output_log) {
  my $outcome = ($result ? "failure" : "success");
  print "\nFinished: $thy_file [$outcome]\n";
}

# cleanup

if (defined $setup_file) {
  unlink $setup_file;
}
unlink $new_thy_file;

exit ($result ? 1 : 0);

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.