<commit_before>#
# Author: <NAME> and <NAME>
#
# Testing tool for automated proof tools.
#

use File::Basename;

# environment

my $isabelle_home = $ENV{'ISABELLE_HOME'};
my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
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 $actions = $ENV{'MIRABELLE_ACTIONS'};

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


# arguments

my $thy_file = $ARGV[0];
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 ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
my $new_thy_name = $thy_name . "_Mirabelle";
my $new_thy_file = $output_path . "/" . $new_thy_name . $ext;


# setup

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 = "uses " . join(" ", 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"
$tools
begin

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

foreach (reverse(split(/:/, $actions))) {
  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;


# modify target theory file

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

my $thy_text = join("", @lines);
my $old_len = length($thy_text);<commit_msg>better parsing of options, in case the value has '='<commit_after>#
# Author: <NAME> and <NAME>
#
# Testing tool for automated proof tools.
#

use File::Basename;

# environment

my $isabelle_home = $ENV{'ISABELLE_HOME'};
my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
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 $actions = $ENV{'MIRABELLE_ACTIONS'};

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


# arguments

my $thy_file = $ARGV[0];
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 ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
my $new_thy_name = $thy_name . "_Mirabelle";
my $new_thy_file = $output_path . "/" . $new_thy_name . $ext;


# setup

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 = "uses " . join(" ", 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"
$tools
begin

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

foreach (reverse(split(/:/, $actions))) {
  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;


# modify target theory file

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

my $thy_text = join("", @lines);
my $old_len = length($thy_text);
{'fraction_non_alphanumeric': 0.22574148663493226, 'fraction_numerical': 0.006957158549981692, 'mean_word_length': 3.934959349593496, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 19, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1072906', 'n_tokens_mistral': 2309, 'n_tokens_neox': 2271, 'n_words': 460}