lib/scripts/convert.pl
author wenzelm
Fri, 19 Jan 2001 11:53:21 +0100
changeset 10939 fe14e54594a3
child 10972 af160f8d3bd7
permissions -rw-r--r--
convert legacy tactic scripts to Isabelle/Isar tactic emulation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10939
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     1
#
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     2
# $Id$
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     3
# Author: David von Oheimb, TU Muenchen
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     4
# License: GPL (GNU GENERAL PUBLIC LICENSE)
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     5
#
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     6
# convert.pl - convert legacy tactic scripts to Isabelle/Isar tactic
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     7
#   emulation using heuristics - leaves unrecognized patterns unchanged
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     8
#   produces from each input file (on the command line) a new file with
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
     9
#   ".thy" appended
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    10
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    11
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    12
sub thmlist {
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    13
  my $s = shift;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    14
  $s =~ s/^\[(.*)\]$/$1/sg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    15
  $s =~ s/, +/ /g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    16
  $s =~ s/,/ /g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    17
  $s;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    18
}
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    19
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    20
sub process_tac {
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    21
  my $t = shift;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    22
  my $simpmodmod = ($t =~ m/auto_tac|force_tac|clarsimp_tac/) ? "simp " : "";
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    23
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    24
  $_ = $t;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    25
  s/Blast_tac *1/blast/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    26
  s/Fast_tac *1/fast/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    27
  s/Slow_tac *1/slow/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    28
  s/Best_tac *1/best/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    29
  s/Safe_tac/safe/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    30
  s/Clarify_tac *1/clarify/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    31
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    32
  s/blast_tac *\( *claset *\( *\) *(.*?)\) *1/blast $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    33
  s/fast_tac *\( *claset *\( *\) *(.*?)\) *1/fast $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    34
  s/slow_tac *\( *claset *\( *\) *(.*?)\) *1/slow $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    35
  s/best_tac *\( *claset *\( *\) *(.*?)\) *1/best $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    36
  s/safe_tac *\( *claset *\( *\) *(.*?)\) */safe $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    37
  s/clarify_tac *\( *claset *\( *\) *(.*?)\) *1/clarify $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    38
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    39
  s/Auto_tac/auto/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    40
  s/Force_tac *1/force/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    41
  s/Clarsimp_tac *1/clarsimp/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    42
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    43
  s/auto_tac *\( *claset *\( *\) *(.*?), *simpset *\( *\) *(.*?)\) */auto$1$2/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    44
  s/force_tac *\( *claset *\( *\) *(.*?), *simpset *\( *\) *(.*?)\) *1/force$1$2/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    45
  s/clarsimp_tac *\( *claset *\( *\) *(.*?), *simpset *\( *\) *(.*?)\) *1/clarsimp$1$2/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    46
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    47
  s/Simp_tac *1/simp (no_asm)/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    48
  s/Asm_simp_tac *1/simp (no_asm_simp)/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    49
  s/Full_simp_tac_tac *1/simp (no_asm_use)/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    50
  s/Asm_full_simp_tac_tac *1/simp/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    51
  s/ALLGOALS *Asm_full_simp_tac/simp_all/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    52
  s/ALLGOALS *Simp_tac/simp_all (no_asm)/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    53
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    54
  s/atac *1/assumption/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    55
  s/hypsubst_tac *1/hypsubst/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    56
  s/arith_tac *1/arith/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    57
  s/strip_tac *1/intro strip/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    58
  s/split_all_tac *1/simp (no_asm_simp) only: split_tupled_all/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    59
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    60
  s/rotate_tac *(\d+) *1/rotate_tac $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    61
  s/rotate_tac *(\d+) *(\d+)/rotate_tac [$2] $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    62
  s/case_tac *(\".*\") *1/case_tac $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    63
  s/case_tac *(\".*\") *(\d+)/case_tac [$2] $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    64
  s/induct_tac *(\".*\") *1/induct_tac $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    65
  s/induct_tac *(\".*\") *(\d+)/induct_tac [$2] $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    66
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    67
  s/stac (\w+) +1/subst $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    68
  s/rtac (\w+) +1/rule $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    69
  s/rtac (\w+) +(\d+)/rule_tac [$2] $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    70
  s/dtac (\w+) +1/drule $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    71
  s/dtac (\w+) +(\d+)/drule_tac [$2] $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    72
  s/etac (\w+) +1/erule $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    73
  s/etac (\w+) +(\d+)/erule_tac [$2] $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    74
  s/ftac (\w+) +1/frule $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    75
  s/rfac (\w+) +(\d+)/frule_tac [$2] $1/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    76
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    77
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    78
  s/THEN/,/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    79
  s/ORELSE/|/g;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    80
  s/fold_goals_tac *(\[[\w\s,]*\]|[\w]+)/"fold ".thmlist($1)/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    81
  s/rewrite_goals_tac *(\[[\w\s,]*\]|[\w]+)/"unfold ".thmlist($1)/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    82
  s/cut_facts_tac *(\[[\w\s,]*\]|[\w]+)/"insert ".thmlist($1)/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    83
  s/EVERY *(\[[\w\s,]*\]|[\w]+)/thmlist($1)/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    84
  s/addIs *(\[[\w\s,]*\]|[\w]+)/" intro: ".thmlist($1)/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    85
  s/addSIs *(\[[\w\s,]*\]|[\w]+)/" intro!: ".thmlist($1)/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    86
  s/addEs *(\[[\w\s,]*\]|[\w]+)/" elim: ".thmlist($1)/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    87
  s/addSEs *(\[[\w\s,]*\]|[\w]+)/" elim!: ".thmlist($1)/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    88
  s/addDs *(\[[\w\s,]*\]|[\w]+)/" dest: ".thmlist($1)/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    89
  s/addSDs *(\[[\w\s,]*\]|[\w]+)/" dest!: ".thmlist($1)/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    90
  s/delrules *(\[[\w\s,]*\]|[\w]+)/" del: ".thmlist($1)/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    91
  s/addsimps *(\[[\w\s,]*\]|[\w]+)/" $simpmodmod"."add: ".thmlist($1)/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    92
  s/delsimps *(\[[\w\s,]*\]|[\w]+)/" $simpmodmod"."del: ".thmlist($1)/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    93
  s/addcongs *(\[[\w\s,]*\]|[\w]+)/" cong add: ".thmlist($1)/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    94
  s/delcongs *(\[[\w\s,]*\]|[\w]+)/" cong del: ".thmlist($1)/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    95
  s/addsplits *(\[[\w\s,]*\]|[\w]+)/" split add: ".thmlist($1)/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    96
  s/delsplits *(\[[\w\s,]*\]|[\w]+)/" split del: ".thmlist($1)/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    97
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    98
  s/^\s*(.*)\s*$/$1/s;     # remove enclosing whitespace
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
    99
  s/^\(\s*([\w]+)\s*\)$/$1/; # remove enclosing parentheses around atoms
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   100
  s/^([a-zA-Z])/ $1/; # add space if required
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   101
  $_;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   102
}
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   103
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   104
sub thmname { "@@" . ++$thmcount . "@@"; }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   105
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   106
sub backpatch_thmnames {
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   107
  if($oldargv ne "") {
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   108
    select(STDOUT);
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   109
    close(ARGVOUT);
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   110
    open(TMPW, '>'.$finalfile);
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   111
    open TMPR,$tmpfile or die "Can't find tmp file $tmp: $!\n";
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   112
    while(<TMPR>) {
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   113
      s/@@(\d+)@@/$thmnames[$1]/eg;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   114
      print TMPW $_;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   115
    }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   116
    system("rm " . $oldargv . '.thy~~');
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   117
  }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   118
}
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   119
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   120
sub done {
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   121
  my $name = shift;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   122
  my $attr = shift;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   123
  $thmnames[$thmcount] = $name.$attr;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   124
  "done";
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   125
}
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   126
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   127
$next = "nonempty";
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   128
while (<>) { # main loop
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   129
  if ($ARGV ne $oldargv) {
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   130
    $x=$_; backpatch_thmnames; $_=$x;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   131
    $thmcount=0;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   132
    $finalfile = "$ARGV" . '.thy';
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   133
    $tmpfile = $finalfile . '~~';
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   134
    open(ARGVOUT, '>'.$tmpfile);
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   135
    select(ARGVOUT);
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   136
    $oldargv = $ARGV;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   137
  }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   138
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   139
 nl:
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   140
  if(!(s/;\s*?(\n?)$/$1/s)) {# no end_of_ML_command marker
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   141
    $next = <>; $_ = $_ . $next;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   142
    if($next) { goto nl; }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   143
  }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   144
  s/\\(\s*\n\s*)\\/ $1 /g; # remove backslashes escaping newlines
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   145
 nlc:
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   146
  m/^(\s*)(.*?)(\s*)$/s;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   147
  $head=$1; $line=$2; $tail=$3;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   148
  print $head; $_=$2.$tail;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   149
  if ($line =~ m/^\(\*/) { # start comment
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   150
    while (($i = index $_,"*)") == -1) { # no end comment
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   151
      print $_;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   152
      $_ = <>;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   153
    }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   154
    print substr $_,0,$i+2;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   155
    $_ = substr $_,$i+2;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   156
    goto nlc;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   157
  }
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   158
  $_=$line;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   159
  s/^Goalw *(\[[\w\s,]*\]|[\w]+) *(.+)/
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   160
    "lemma ".thmname().": $2$head"."apply (unfold ".thmlist($1).")"/se;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   161
  s/^Goal *(.+)/"lemma ".thmname().": $1"/se;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   162
  s/^qed_spec_mp *\"(.*?)\"/done($1," [rule_format (no_asm)]")/se;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   163
  s/^qed *\"(.*?)\"/done($1,"")/se;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   164
  s/^bind_thm *\( *\"(.*?)\" *, *(.*?result *\( *\).*?) *\) *$/done($1,"[?? $2 ??] ")/se;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   165
  s/^by(\s*)(.*)$/"apply$1".process_tac($2)/se;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   166
  print "$_$tail";
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   167
  if(!$next) { last; } # prevents reading finally from stdin (thru <>)!
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   168
}
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   169
backpatch_thmnames;
fe14e54594a3 convert legacy tactic scripts to Isabelle/Isar tactic emulation;
wenzelm
parents:
diff changeset
   170
select(STDOUT);