debugging and extensions
authoroheimb
Wed Jan 24 17:53:01 2001 +0100 (2001-01-24)
changeset 10972af160f8d3bd7
parent 10971 6852682eaf16
child 10973 5b0d04078d2a
debugging and extensions
lib/scripts/convert.pl
     1.1 --- a/lib/scripts/convert.pl	Wed Jan 24 12:29:10 2001 +0100
     1.2 +++ b/lib/scripts/convert.pl	Wed Jan 24 17:53:01 2001 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  # convert.pl - convert legacy tactic scripts to Isabelle/Isar tactic
     1.5  #   emulation using heuristics - leaves unrecognized patterns unchanged
     1.6  #   produces from each input file (on the command line) a new file with
     1.7 -#   ".thy" appended
     1.8 +#   ".thy" appended and renames the original input file by appending "~0~"
     1.9  
    1.10  
    1.11  sub thmlist {
    1.12 @@ -17,94 +17,141 @@
    1.13    $s;
    1.14  }
    1.15  
    1.16 +sub mult_assumption {
    1.17 +  my $n = shift;
    1.18 +  my $r = "";
    1.19 +  for($i=0; $i<$n; $i++) { $r = $r.", assumption"; }
    1.20 +  $r;
    1.21 +}
    1.22 +
    1.23  sub process_tac {
    1.24 +  my $lead = shift;
    1.25    my $t = shift;
    1.26    my $simpmodmod = ($t =~ m/auto_tac|force_tac|clarsimp_tac/) ? "simp " : "";
    1.27  
    1.28    $_ = $t;
    1.29 -  s/Blast_tac *1/blast/g;
    1.30 -  s/Fast_tac *1/fast/g;
    1.31 -  s/Slow_tac *1/slow/g;
    1.32 -  s/Best_tac *1/best/g;
    1.33 -  s/Safe_tac/safe/g;
    1.34 -  s/Clarify_tac *1/clarify/g;
    1.35 +  s/\s+/ /sg;             # remove multiple whitespace
    1.36 +  s/\s/ /sg;              # substitute all remaining tabs and newlines by space
    1.37 +  s/\( /\(/g; s/ \)/\)/g; # remove leading and trailing space inside parentheses
    1.38 +  s/\[ /\[/g; s/ \]/\]/g; # remove leading and trailing space inside sq brackets
    1.39 +  s/ ?\( ?\)/\(\)/g;      # remove space before and inside empty tuples
    1.40 +  s/\(\)([^ ])/\(\) $1/g; # possibly add space after empty tuples
    1.41  
    1.42 -  s/blast_tac *\( *claset *\( *\) *(.*?)\) *1/blast $1/g;
    1.43 -  s/fast_tac *\( *claset *\( *\) *(.*?)\) *1/fast $1/g;
    1.44 -  s/slow_tac *\( *claset *\( *\) *(.*?)\) *1/slow $1/g;
    1.45 -  s/best_tac *\( *claset *\( *\) *(.*?)\) *1/best $1/g;
    1.46 -  s/safe_tac *\( *claset *\( *\) *(.*?)\) */safe $1/g;
    1.47 -  s/clarify_tac *\( *claset *\( *\) *(.*?)\) *1/clarify $1/g;
    1.48 +  s/Blast_tac 1/blast/g;
    1.49 +  s/Fast_tac 1/fast/g;
    1.50 +  s/Slow_tac 1/slow/g;
    1.51 +  s/Best_tac 1/best/g;
    1.52 +  s/Safe_tac/safe/g;
    1.53 +  s/Clarify_tac 1/clarify/g;
    1.54 +
    1.55 +  s/blast_tac \(claset\(\) (.*?)\) 1/blast $1/g;
    1.56 +  s/fast_tac \(claset\(\) (.*?)\) 1/fast $1/g;
    1.57 +  s/slow_tac \(claset\(\) (.*?)\) 1/slow $1/g;
    1.58 +  s/best_tac \(claset\(\) (.*?)\) 1/best $1/g;
    1.59 +  s/safe_tac \(claset\(\) (.*?)\)/safe $1/g;
    1.60 +  s/clarify_tac \(claset\(\) (.*?)\) 1/clarify $1/g;
    1.61  
    1.62    s/Auto_tac/auto/g;
    1.63 -  s/Force_tac *1/force/g;
    1.64 -  s/Clarsimp_tac *1/clarsimp/g;
    1.65 +  s/Force_tac 1/force/g;
    1.66 +  s/Clarsimp_tac 1/clarsimp/g;
    1.67  
    1.68 -  s/auto_tac *\( *claset *\( *\) *(.*?), *simpset *\( *\) *(.*?)\) */auto$1$2/g;
    1.69 -  s/force_tac *\( *claset *\( *\) *(.*?), *simpset *\( *\) *(.*?)\) *1/force$1$2/g;
    1.70 -  s/clarsimp_tac *\( *claset *\( *\) *(.*?), *simpset *\( *\) *(.*?)\) *1/clarsimp$1$2/g;
    1.71 +  s/auto_tac \(claset\(\) (.*?), *simpset\(\) (.*?)\)/auto $1 $2/g;
    1.72 +  s/force_tac \(claset\(\) (.*?), *simpset\(\) (.*?)\) 1/force $1 $2/g;
    1.73 +  s/clarsimp_tac \(claset\(*\) (.*?), *simpset\(\) (.*?)\) 1/clarsimp $1 $2/g;
    1.74  
    1.75 -  s/Simp_tac *1/simp (no_asm)/g;
    1.76 -  s/Asm_simp_tac *1/simp (no_asm_simp)/g;
    1.77 -  s/Full_simp_tac_tac *1/simp (no_asm_use)/g;
    1.78 -  s/Asm_full_simp_tac_tac *1/simp/g;
    1.79 -  s/ALLGOALS *Asm_full_simp_tac/simp_all/g;
    1.80 -  s/ALLGOALS *Simp_tac/simp_all (no_asm)/g;
    1.81 +  s/Asm_full_simp_tac 1/simp/g;
    1.82 +  s/Full_simp_tac 1/simp (no_asm_use)/g;
    1.83 +  s/Asm_simp_tac 1/simp (no_asm_simp)/g;
    1.84 +  s/Simp_tac 1/simp (no_asm)/g;
    1.85 +  s/ALLGOALS Asm_full_simp_tac/simp_all/g;
    1.86 +  s/ALLGOALS Full_simp_tac 1/simp_all (no_asm_use)/g;
    1.87 +  s/ALLGOALS Asm_simp_tac 1/simp_all (no_asm_simp)/g;
    1.88 +  s/ALLGOALS Simp_tac/simp_all (no_asm)/g;
    1.89 +
    1.90 +  s/asm_full_simp_tac \(simpset\(\) (.*?)\) 1/simp $1/g;
    1.91 +  s/full_simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm_use) $1/g;
    1.92 +  s/asm_simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm_simp) $1/g;
    1.93 +  s/simp_tac \(simpset\(\) (.*?)\) 1/simp (no_asm) $1/g;
    1.94 +  s/ALLGOALS \(asm_full_simp_tac \(simpset\(\) (.*?)\)\)/simp_all $1/g;
    1.95 +  s/ALLGOALS \(full_simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm_use) $1/g;
    1.96 +  s/ALLGOALS \(asm_simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm_simp) $1/g;
    1.97 +  s/ALLGOALS \(simp_tac \(simpset\(\) (.*?)\)\)/simp_all (no_asm) $1/g;
    1.98 +
    1.99 +  s/atac 1/assumption/g;
   1.100 +  s/hypsubst_tac 1/hypsubst/g;
   1.101 +  s/arith_tac 1/arith/g;
   1.102 +  s/strip_tac 1/intro strip/g;
   1.103 +  s/split_all_tac 1/simp (no_asm_simp) only: split_tupled_all/g;
   1.104  
   1.105 -  s/atac *1/assumption/g;
   1.106 -  s/hypsubst_tac *1/hypsubst/g;
   1.107 -  s/arith_tac *1/arith/g;
   1.108 -  s/strip_tac *1/intro strip/g;
   1.109 -  s/split_all_tac *1/simp (no_asm_simp) only: split_tupled_all/g;
   1.110 +  s/rotate_tac ([~\d]+) 1/rotate_tac $1/g;
   1.111 +  s/rotate_tac ([~\d]+) (\d+)/rotate_tac [$2] $1/g;
   1.112 +  s/rename_tac *(\".*?\") *1/rename_tac $1/g;
   1.113 +  s/rename_tac *(\".*?\") *(\d+)/rename_tac [$2] $1/g;
   1.114 +  s/case_tac *(\".*?\") *1/case_tac $1/g;
   1.115 +  s/case_tac *(\".*?\") *(\d+)/case_tac [$2] $1/g;
   1.116 +  s/induct_tac *(\".*?\") *1/induct_tac $1/g;
   1.117 +  s/induct_tac *(\".*?\") *(\d+)/induct_tac [$2] $1/g;
   1.118 +  s/subgoal_tac *(\".*?\") *1/subgoal_tac $1/g;
   1.119 +  s/subgoal_tac *(\".*?\") *(\d+)/subgoal_tac [$2] $1/g;
   1.120 +  s/thin_tac *(\".*?\") *1/erule_tac P = $1 thin_rl/g;
   1.121 +  s/thin_tac *(\".*?\") *(\d+)/erule_tac [$2] P = $1/g;
   1.122  
   1.123 -  s/rotate_tac *(\d+) *1/rotate_tac $1/g;
   1.124 -  s/rotate_tac *(\d+) *(\d+)/rotate_tac [$2] $1/g;
   1.125 -  s/case_tac *(\".*\") *1/case_tac $1/g;
   1.126 -  s/case_tac *(\".*\") *(\d+)/case_tac [$2] $1/g;
   1.127 -  s/induct_tac *(\".*\") *1/induct_tac $1/g;
   1.128 -  s/induct_tac *(\".*\") *(\d+)/induct_tac [$2] $1/g;
   1.129 -
   1.130 -  s/stac (\w+) +1/subst $1/g;
   1.131 -  s/rtac (\w+) +1/rule $1/g;
   1.132 -  s/rtac (\w+) +(\d+)/rule_tac [$2] $1/g;
   1.133 -  s/dtac (\w+) +1/drule $1/g;
   1.134 -  s/dtac (\w+) +(\d+)/drule_tac [$2] $1/g;
   1.135 -  s/etac (\w+) +1/erule $1/g;
   1.136 -  s/etac (\w+) +(\d+)/erule_tac [$2] $1/g;
   1.137 -  s/ftac (\w+) +1/frule $1/g;
   1.138 -  s/rfac (\w+) +(\d+)/frule_tac [$2] $1/g;
   1.139 +  s/stac ([\w\.]+) 1/subst $1/g;
   1.140 +  s/rtac ([\w\.]+) 1/rule $1/g;
   1.141 +  s/rtac ([\w\.]+) (\d+)/rule_tac [$2] $1/g;
   1.142 +  s/res_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\.]+) 1/rule_tac $1 = $2 $3/g;
   1.143 +  s/ratac ([\w\.]+) (\d+) 1/"rule $1".mult_assumption($2)/eg;
   1.144 +  s/dtac ([\w\.]+) 1/drule $1/g;
   1.145 +  s/dtac ([\w\.]+) (\d+)/drule_tac [$2] $1/g;
   1.146 +  s/dres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\.]+) 1/drule_tac $1 = $2 $3/g;
   1.147 +  s/datac ([\w\.]+) (\d+) 1/"drule $1".mult_assumption($2)/eg;
   1.148 +  s/etac ([\w\.]+) 1/erule $1/g;
   1.149 +  s/etac ([\w\.]+) (\d+)/erule_tac [$2] $1/g;
   1.150 +  s/eres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\.]+) 1/erule_tac $1 = $2 $3/g;
   1.151 +  s/eatac ([\w\.]+) (\d+) 1/"erule $1".mult_assumption($2)/eg;
   1.152 +  s/forward_tac \[([\w\.]+)\] 1/frule $1/g;
   1.153 +  s/ftac ([\w\.]+) 1/frule $1/g;
   1.154 +  s/ftac ([\w\.]+) (\d+)/frule_tac [$2] $1/g;
   1.155 +  s/forw_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\.]+) 1/frule_tac $1 = $2 $3/g;
   1.156 +  s/fatac ([\w\.]+) (\d+) 1/"frule $1".mult_assumption($2)/eg;
   1.157  
   1.158  
   1.159 -  s/THEN/,/g;
   1.160 +  s/THEN /, /g;
   1.161    s/ORELSE/|/g;
   1.162 -  s/fold_goals_tac *(\[[\w\s,]*\]|[\w]+)/"fold ".thmlist($1)/eg;
   1.163 -  s/rewrite_goals_tac *(\[[\w\s,]*\]|[\w]+)/"unfold ".thmlist($1)/eg;
   1.164 -  s/cut_facts_tac *(\[[\w\s,]*\]|[\w]+)/"insert ".thmlist($1)/eg;
   1.165 -  s/EVERY *(\[[\w\s,]*\]|[\w]+)/thmlist($1)/eg;
   1.166 -  s/addIs *(\[[\w\s,]*\]|[\w]+)/" intro: ".thmlist($1)/eg;
   1.167 -  s/addSIs *(\[[\w\s,]*\]|[\w]+)/" intro!: ".thmlist($1)/eg;
   1.168 -  s/addEs *(\[[\w\s,]*\]|[\w]+)/" elim: ".thmlist($1)/eg;
   1.169 -  s/addSEs *(\[[\w\s,]*\]|[\w]+)/" elim!: ".thmlist($1)/eg;
   1.170 -  s/addDs *(\[[\w\s,]*\]|[\w]+)/" dest: ".thmlist($1)/eg;
   1.171 -  s/addSDs *(\[[\w\s,]*\]|[\w]+)/" dest!: ".thmlist($1)/eg;
   1.172 -  s/delrules *(\[[\w\s,]*\]|[\w]+)/" del: ".thmlist($1)/eg;
   1.173 -  s/addsimps *(\[[\w\s,]*\]|[\w]+)/" $simpmodmod"."add: ".thmlist($1)/eg;
   1.174 -  s/delsimps *(\[[\w\s,]*\]|[\w]+)/" $simpmodmod"."del: ".thmlist($1)/eg;
   1.175 -  s/addcongs *(\[[\w\s,]*\]|[\w]+)/" cong add: ".thmlist($1)/eg;
   1.176 -  s/delcongs *(\[[\w\s,]*\]|[\w]+)/" cong del: ".thmlist($1)/eg;
   1.177 -  s/addsplits *(\[[\w\s,]*\]|[\w]+)/" split add: ".thmlist($1)/eg;
   1.178 -  s/delsplits *(\[[\w\s,]*\]|[\w]+)/" split del: ".thmlist($1)/eg;
   1.179 +  s/fold_goals_tac *(\[[\w\. ,]*\]|[\w\.]+)/"fold ".thmlist($1)/eg;
   1.180 +  s/rewrite_goals_tac *(\[[\w\. ,]*\]|[\w\.]+)/"unfold ".thmlist($1)/eg;
   1.181 +  s/cut_facts_tac *(\[[\w\. ,]*\]|[\w\.]+) 1/"cut_tac ".thmlist($1)/eg;
   1.182 +  s/resolve_tac *(\[[\w\. ,]*\]|[\w\.]+) 1/"rule ".thmlist($1)/eg;
   1.183 +  s/EVERY *(\[[\w\. ,]*\]|[\w\.]+)/thmlist($1)/eg;
   1.184  
   1.185 -  s/^\s*(.*)\s*$/$1/s;     # remove enclosing whitespace
   1.186 -  s/^\(\s*([\w]+)\s*\)$/$1/; # remove enclosing parentheses around atoms
   1.187 -  s/^([a-zA-Z])/ $1/; # add space if required
   1.188 +  s/addIs *(\[[\w\. ,]*\]|[\w\.]+)/"intro: ".thmlist($1)/eg;
   1.189 +  s/addSIs *(\[[\w\. ,]*\]|[\w\.]+)/"intro!: ".thmlist($1)/eg;
   1.190 +  s/addEs *(\[[\w\. ,]*\]|[\w\.]+)/"elim: ".thmlist($1)/eg;
   1.191 +  s/addSEs *(\[[\w\. ,]*\]|[\w\.]+)/"elim!: ".thmlist($1)/eg;
   1.192 +  s/addDs *(\[[\w\. ,]*\]|[\w\.]+)/"dest: ".thmlist($1)/eg;
   1.193 +  s/addSDs *(\[[\w\. ,]*\]|[\w\.]+)/"dest!: ".thmlist($1)/eg;
   1.194 +  s/delrules *(\[[\w\. ,]*\]|[\w\.]+)/"del: ".thmlist($1)/eg;
   1.195 +  s/addsimps *(\[[\w\. ,]*\]|[\w\.]+)/"$simpmodmod"."add: ".thmlist($1)/eg;
   1.196 +  s/delsimps *(\[[\w\. ,]*\]|[\w\.]+)/"$simpmodmod"."del: ".thmlist($1)/eg;
   1.197 +  s/addcongs *(\[[\w\. ,]*\]|[\w\.]+)/"cong add: ".thmlist($1)/eg;
   1.198 +  s/delcongs *(\[[\w\. ,]*\]|[\w\.]+)/"cong del: ".thmlist($1)/eg;
   1.199 +  s/addsplits *(\[[\w\. ,]*\]|[\w\.]+)/"split add: ".thmlist($1)/eg;
   1.200 +  s/delsplits *(\[[\w\. ,]*\]|[\w\.]+)/"split del: ".thmlist($1)/eg;
   1.201 +
   1.202 +  s/([\w\.]+) RS ([\w\.]+)/$1 \[THEN $2\]/g;
   1.203 +
   1.204 +  s/ +/ /g;                  # remove multiple whitespace
   1.205 +  s/\( /\(/; s/ \)/\)/g;  # remove leading and trailing space inside parentheses
   1.206 +  s/^ *(.*?) *$/$1/s;        # remove enclosing whitespace
   1.207 +  s/^\( *([\w\.]+) *\)$/$1/; # remove outermost parentheses if around atoms
   1.208 +  s/^([a-zA-Z])/ $1/ if (!($lead =~ m/[\s\(]$/)); # add space if required
   1.209    $_;
   1.210  }
   1.211  
   1.212  sub thmname { "@@" . ++$thmcount . "@@"; }
   1.213  
   1.214  sub backpatch_thmnames {
   1.215 -  if($oldargv ne "") {
   1.216 +  if($currfile ne "") {
   1.217      select(STDOUT);
   1.218      close(ARGVOUT);
   1.219      open(TMPW, '>'.$finalfile);
   1.220 @@ -113,7 +160,8 @@
   1.221        s/@@(\d+)@@/$thmnames[$1]/eg;
   1.222        print TMPW $_;
   1.223      }
   1.224 -    system("rm " . $oldargv . '.thy~~');
   1.225 +    system("mv $currfile $currfile.~0~");
   1.226 +    system("rm $tmpfile");
   1.227    }
   1.228  }
   1.229  
   1.230 @@ -126,14 +174,14 @@
   1.231  
   1.232  $next = "nonempty";
   1.233  while (<>) { # main loop
   1.234 -  if ($ARGV ne $oldargv) {
   1.235 +  if ($ARGV ne $currfile) {
   1.236      $x=$_; backpatch_thmnames; $_=$x;
   1.237 +    $currfile = $ARGV;
   1.238      $thmcount=0;
   1.239 -    $finalfile = "$ARGV" . '.thy';
   1.240 -    $tmpfile = $finalfile . '~~';
   1.241 +    $finalfile = "$currfile.thy";
   1.242 +    $tmpfile   = "$finalfile.~0~";
   1.243      open(ARGVOUT, '>'.$tmpfile);
   1.244      select(ARGVOUT);
   1.245 -    $oldargv = $ARGV;
   1.246    }
   1.247  
   1.248   nl:
   1.249 @@ -145,6 +193,7 @@
   1.250   nlc:
   1.251    m/^(\s*)(.*?)(\s*)$/s;
   1.252    $head=$1; $line=$2; $tail=$3;
   1.253 +  $tail =~ s/\s+\n/\n/sg;  # remove trailing whitespace at end of lines
   1.254    print $head; $_=$2.$tail;
   1.255    if ($line =~ m/^\(\*/) { # start comment
   1.256      while (($i = index $_,"*)") == -1) { # no end comment
   1.257 @@ -156,13 +205,14 @@
   1.258      goto nlc;
   1.259    }
   1.260    $_=$line;
   1.261 -  s/^Goalw *(\[[\w\s,]*\]|[\w]+) *(.+)/
   1.262 +  s/^Goalw *(\[[\w\.\s,]*\]|[\w\.]+) *(.+)/
   1.263      "lemma ".thmname().": $2$head"."apply (unfold ".thmlist($1).")"/se;
   1.264    s/^Goal *(.+)/"lemma ".thmname().": $1"/se;
   1.265 +  s/ goal/"(*".thmname()."*) goal"/se; # ugly old-style goals
   1.266    s/^qed_spec_mp *\"(.*?)\"/done($1," [rule_format (no_asm)]")/se;
   1.267    s/^qed *\"(.*?)\"/done($1,"")/se;
   1.268    s/^bind_thm *\( *\"(.*?)\" *, *(.*?result *\( *\).*?) *\) *$/done($1,"[?? $2 ??] ")/se;
   1.269 -  s/^by(\s*)(.*)$/"apply$1".process_tac($2)/se;
   1.270 +  s/^by(\s*\(?\s*)(.*?)$/"apply$1".process_tac($1,$2)/se;
   1.271    print "$_$tail";
   1.272    if(!$next) { last; } # prevents reading finally from stdin (thru <>)!
   1.273  }