lib/scripts/convert.pl

further minor improvements

#
# $Id$
# Author: David von Oheimb, TU Muenchen
# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
# convert.pl - convert legacy tactic scripts to Isabelle/Isar tactic
#   emulation using heuristics - leaves unrecognized patterns unchanged
#   produces from each input file (on the command line) a new file with
#   ".thy" appended and renames the original input file by appending "~0~"


sub thmlist {
  my $s = shift;
  $s =~ s/^\[(.*)\]$/$1/sg;
  $s =~ s/, +/ /g;
  $s =~ s/,/ /g;
  $s;
}

sub process_tac {
  my $lead = shift;
  my $t = shift;
  my $simpmodmod = ($t =~ m/auto_tac|force_tac|clarsimp_tac/) ? "simp " : "";

  $_ = $t;
  s/\s+/ /sg;             # remove multiple whitespace
  s/\s/ /sg;              # substitute all remaining tabs and newlines by space
  s/\( /\(/g; s/ \)/\)/g; # remove leading and trailing space inside parentheses
  s/\[ /\[/g; s/ \]/\]/g; # remove leading and trailing space inside sq brackets
  s/ ?\( ?\)/\(\)/g;      # remove space before and inside empty tuples
  s/\(\)([^ ])/\(\) $1/g; # possibly add space after empty tuples

  s/Blast_tac 1/blast/g;
  s/Fast_tac 1/fast/g;
  s/Slow_tac 1/slow/g;
  s/Best_tac 1/best/g;
  s/Safe_tac/safe/g;
  s/Clarify_tac 1/clarify/g;

  s/blast_tac \(claset\(\) (.*?)\) 1/blast $1/g;
  s/fast_tac \(claset\(\) (.*?)\) 1/fast $1/g;
  s/slow_tac \(claset\(\) (.*?)\) 1/slow $1/g;
  s/best_tac \(claset\(\) (.*?)\) 1/best $1/g;
  s/safe_tac \(claset\(\) (.*?)\)/safe $1/g;
  s/clarify_tac \(claset\(\) (.*?)\) 1/clarify $1/g;

  s/Auto_tac/auto/g;
  s/Force_tac 1/force/g;
  s/Clarsimp_tac 1/clarsimp/g;

  s/auto_tac \(claset\(\) (.*?), *simpset\(\) (.*?)\)/auto $1 $2/g;
  s/force_tac \(claset\(\) (.*?), *simpset\(\) (.*?)\) 1/force $1 $2/g;
  s/clarsimp_tac \(claset\(*\) (.*?), *simpset\(\) (.*?)\) 1/clarsimp $1 $2/g;

  s/Asm_full_simp_tac 1/simp/g;
  s/Full_simp_tac 1/simp (no_asm_use)/g;
  s/Asm_simp_tac 1/simp (no_asm_simp)/g;
  s/Simp_tac 1/simp (no_asm)/g;
  s/ALLGOALS Asm_full_simp_tac/simp_all/g;
  s/ALLGOALS Full_simp_tac 1/simp_all (no_asm_use)/g;
  s/ALLGOALS Asm_simp_tac 1/simp_all (no_asm_simp)/g;
  s/ALLGOALS Simp_tac/simp_all (no_asm)/g;

  s/asm_full_simp_tac \(simpset\(\) (.*?)\) 1/simp $1/g;
  s/full_simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm_use) $1/g;
  s/asm_simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm_simp) $1/g;
  s/simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm) $1/g;
  s/ALLGOALS \(asm_full_simp_tac \(simpset\(\) (.*?)\)\)/simp_all $1/g;
  s/ALLGOALS \(full_simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm_use) $1/g;
  s/ALLGOALS \(asm_simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm_simp) $1/g;
  s/ALLGOALS \(simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm) $1/g;

  s/atac 1/assumption/g;
  s/atac (\d+)/tactic \"assume_tac $1\"/g;
  s/^mp_tac 1/erule (1) notE impE/g;
  s/^mp_tac (\d+)/erule_tac [$1] notE impE, tactic \"assume_tac $1\"/g;

  s/hypsubst_tac 1/hypsubst/g;
  s/arith_tac 1/arith/g;
  s/strip_tac 1/intro strip/g;
  s/split_all_tac 1/simp (no_asm_simp) only: split_tupled_all/g;

  s/rotate_tac (\d+) 1/rotate_tac $1/g;
  s/rotate_tac (\d+) (\d+)/rotate_tac [$2] $1/g;
  s/rotate_tac (~\d+) 1/rotate_tac -$1/g;
  s/rotate_tac (~\d+) (\d+)/rotate_tac [$2] -$1/g;
  s/rename_tac (\".*?\") 1/rename_tac $1/g;
  s/rename_tac (\".*?\") (\d+)/rename_tac [$2] $1/g;
  s/case_tac (\".*?\") 1/case_tac $1/g;
  s/case_tac (\".*?\") (\d+)/case_tac [$2] $1/g;
  s/induct_tac (\".*?\") 1/induct_tac $1/g;
  s/induct_tac (\".*?\") (\d+)/induct_tac [$2] $1/g;
  s/subgoal_tac (\".*?\") 1/subgoal_tac $1/g;
  s/subgoal_tac (\".*?\") (\d+)/subgoal_tac [$2] $1/g;
  s/thin_tac (\".*?\") *1/erule_tac V = $1 in thin_rl/g;
  s/thin_tac (\".*?\") *(\d+)/erule_tac [$2] V = $1 in thin_rl/g;

  s/THEN /, /g;
  s/ORELSE/|/g;
  s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3, THEN $4, THEN $5\]/g;
  s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3, THEN $4, THEN $5\]/g;
  s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3, THEN $4\]/g;
  s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3, THEN $4\]/g;
  s/\(([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2, THEN $3\]/g;
  s/([\w\'\.]+) RS ([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2, THEN $3\]/g;
  s/\(([\w\'\.]+) RS ([\w\'\.]+)\)/$1 \[THEN $2\]/g;
  s/([\w\'\.]+) RS ([\w\'\.]+)/$1 \[THEN $2\]/g;

  s/rewtac ([\w\'\. \[,\]]+)/unfold $1/g;
  s/stac ([\w\'\. \[,\]]+?) 1/subst $1/g;
  s/rtac ([\w\'\. \[,\]]+?) 1/rule $1/g;
  s/rtac ([\w\'\. \[,\]]+?) (\d+)/rule_tac [$2] $1/g;
  s/res_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\. \[,\]]+?) 1/rule_tac $1 = $2 in $3/g;
  s/dtac ([\w\'\. \[,\]]+?) 1/drule $1/g;
  s/dtac ([\w\'\. \[,\]]+?) (\d+)/drule_tac [$2] $1/g;
  s/dres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\. \[,\]]+?) 1/drule_tac $1 = $2 in $3/g;
  s/datac ([\w\'\. \[,\]]+?) (\d+) 1/drule ($2) $1/g;
  s/etac ([\w\'\. \[,\]]+?) 1/erule $1/g;
  s/etac ([\w\'\. \[,\]]+?) (\d+)/erule_tac [$2] $1/g;
  s/eres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\. \[,\]]+?) 1/erule_tac $1 = $2 in $3/g;
  s/eatac ([\w\'\. \[,\]]+?) (\d+) 1/erule ($2) $1/g;
  s/forward_tac \[([\w\'\. \[,\]]+)\] 1/frule $1/g;
  s/forward_tac \[([\w\'\. \[,\]]+)\] (\d+)/frule_tac [$2] $1/g;
  s/ftac ([\w\'\. \[,\]]+?) 1/frule $1/g;
  s/ftac ([\w\'\. \[,\]]+?) (\d+)/frule_tac [$2] $1/g;
  s/forw_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\'\. \[,\]]+?) 1/frule_tac $1 = $2 in $3/g;
  s/fatac ([\w\'\. \[,\]]+?) (\d+) 1/frule ($2) $1/g;


  s/fold_goals_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"fold ".thmlist($1)/eg;
  s/rewrite_goals_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"unfold ".thmlist($1)/eg;
  s/cut_facts_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+) 1/"cut_tac ".thmlist($1)/eg;
  s/resolve_tac *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+) 1/"rule ".thmlist($1)/eg;

  s/addIs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"intro: ".thmlist($1)/eg;
  s/addSIs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"intro!: ".thmlist($1)/eg;
  s/addEs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"elim: ".thmlist($1)/eg;
  s/addSEs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"elim!: ".thmlist($1)/eg;
  s/addDs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"dest: ".thmlist($1)/eg;
  s/addSDs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"dest!: ".thmlist($1)/eg;
  s/delrules *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"del: ".thmlist($1)/eg;
  s/addsimps *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"$simpmodmod"."add: ".thmlist($1)/eg;
  s/delsimps *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"$simpmodmod"."del: ".thmlist($1)/eg;
  s/addcongs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"cong add: ".thmlist($1)/eg;
  s/delcongs *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"cong del: ".thmlist($1)/eg;
  s/addsplits *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"split add: ".thmlist($1)/eg;
  s/delsplits *(\[[\w\'\. ,]*\]|[\w\'\. \[,\]]+)/"split del: ".thmlist($1)/eg;

  s/ +/ /g;                       # remove multiple whitespace
  s/\( /\(/; s/ \)/\)/g;  # remove leading and trailing space inside parentheses
  s/^ *(.*?) *$/$1/s;             # remove enclosing whitespace
  s/^([a-zA-Z])/ $1/ if (!($lead =~ m/[\s\(]$/)); # add space if required
  $_;
}

sub thmname { "@@" . ++$thmcount . "@@"; }

sub backpatch_thmnames {
  if($currfile ne "") {
    select(STDOUT);
    close(ARGVOUT);
    open(TMPW, '>'.$finalfile);
    open TMPR,$tmpfile or die "Can't find tmp file $tmp: $!\n";
    while(<TMPR>) {
      s/@@(\d+)@@/$thmnames[$1]/eg;
      print TMPW $_;
    }
    system("mv $currfile $currfile~0~");
    system("rm $tmpfile");
  }
}

sub done {
  my $name = shift;
  my $attr = shift;
  $thmnames[$thmcount] = $name.$attr;
  "done";
}

$currfile = "";
$next = "nonempty";
while (<>) { # main loop
  if ($ARGV ne $currfile) {
    $x=$_; backpatch_thmnames; $_=$x;
    $currfile = $ARGV;
    $thmcount=0;
    $finalfile = "$currfile.thy";
    $tmpfile   = "$finalfile.~0~";
    open(ARGVOUT, '>'.$tmpfile);
    select(ARGVOUT);
  }

 nl:
  if(!(s/;\s*?(\n?)$/$1/s)) {# no end_of_ML_command marker
    $next = <>; $_ = $_ . $next;
    if($next) { goto nl; }
  }
  s/\\(\s*\n\s*)\\/ $1 /g; # remove backslashes escaping newlines
 nlc:
  m/^(\s*)(.*?)(\s*)$/s;
  $head=$1; $line=$2; $tail=$3;
  $tail =~ s/\s+\n/\n/sg;  # remove trailing whitespace at end of lines
  print $head; $_=$2.$tail;
  if ($line =~ m/^\(\*/) { # start comment
    while (($i = index $_,"*)") == -1) { # no end comment
      print $_;
      $_ = <>;
    }
    print substr $_,0,$i+2;
    $_ = substr $_,$i+2;
    goto nlc;
  }
  $_=$line;
  s/^Goalw *(\[[\w\'\.\s,]*\]|[\w\'\. \[,\]]+) *(.+)/
    "lemma ".thmname().": $2$head"."apply (unfold ".thmlist($1).")"/se;
  s/^Goal *(.+)/"lemma ".thmname().": $1"/se;
  s/ goal/"(*".thmname()."*) goal"/se; # ugly old-style goals
  s/^qed_spec_mp *\"(.*?)\"/done($1," [rule_format (no_asm)]")/se;
  s/^qed *\"(.*?)\"/done($1,"")/se;
  s/^bind_thm *\( *\"(.*?)\" *, *(.*?result *\( *\).*?) *\) *$/done($1,"[?? $2 ??] ")/se;
  s/^by(\s*\(?\s*)(.*?)\s*(\)?)\s*$/"apply$1".process_tac($1,$2).$3/se;
  s/^(apply +)\( *([\w\'\.]+)\s*\)\s*$/$1$2/;
                             # remove outermost parentheses if around atoms
  s/^Addsimps\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [simp]"/seg;
  s/^Delsimps\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [simp del]"/seg;
  s/^Addsplits\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [split]"/seg;
  s/^Delsplits\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [split del]"/seg;
  s/^AddIs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [intro]"/seg;
  s/^AddSIs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [intro!]"/seg;
  s/^AddEs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [elim]"/seg;
  s/^AddSEs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [elim!]"/seg;
  s/^AddDs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [dest]"/seg;
  s/^AddSDs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [dest!]"/seg;
  s/^AddIffs\s*\[\s*([\w\'\. \[,\]]*)\s*\]/"declare ".thmlist($1)." [iff]"/seg;
  print "$_$tail";
  if(!$next) { last; } # prevents reading finally from stdin (thru <>)!
}
backpatch_thmnames;
select(STDOUT);