lib/scripts/fixdatatype.pl
author wenzelm
Tue, 13 Feb 2001 16:31:18 +0100
changeset 11109 ce1cefc6c14c
parent 9789 7e5e6c47c0b5
child 14981 e73f8140af78
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5213
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
     1
#
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
     2
# $Id$
9789
wenzelm
parents: 8444
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
wenzelm
parents: 8444
diff changeset
     4
# License: GPL (GNU GENERAL PUBLIC LICENSE)
5213
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
     5
#
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
     6
# fixdatatype.pl - adapt theories and proof scripts to new datatype package
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
     7
#
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
     8
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
     9
sub fixdatatype {
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    10
    my ($file) = @_;
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    11
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    12
    open (FILE, $file) || die $!;
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    13
    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    14
    close FILE || die $!;
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    15
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    16
    $_ = $text;
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    17
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    18
    ## convert split_type_case[_asm] to type.split[_asm]
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    19
    s/([^"])\bsplit_([\w]+)_case\b/$1$2.split/sg;
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    20
    s/([^"])\bsplit_([\w]+)_case_asm\b/$1$2.split_asm/sg;
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    21
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    22
    ## delete function name and type after "primrec"
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    23
    s/\bprimrec\b\s+([\w]+|"[^"]+")\s+([\w\.]+)/primrec/sg;
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    24
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    25
    ## replace specific induct_tac by generic induct_tac
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    26
    s/[\w\.]+\.induct_tac/induct_tac/sg;
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    27
8444
8f8eb220d9aa replaced exhaust_tac by case_tac;
wenzelm
parents: 5213
diff changeset
    28
    ## replace res_inst_tac ... natE by case_tac
8f8eb220d9aa replaced exhaust_tac by case_tac;
wenzelm
parents: 5213
diff changeset
    29
    s/\bres_inst_tac\b\s*\[\s*\(\s*"[^"]+"\s*,\s*("[^"]+")\s*\)\s*\]\s*natE\b/case_tac $1/sg;
5213
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    30
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    31
    $result = $_;
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    32
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    33
    if ($text ne $result) {
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    34
        print STDERR "fixing $file\n";
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    35
        if (! -f "$file~~") {
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    36
            rename $file, "$file~~" || die $!;
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    37
        }
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    38
        open (FILE, "> $file") || die $!;
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    39
        print FILE $result;
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    40
        close FILE || die $!;
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    41
    }
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    42
}
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    43
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    44
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    45
## main
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    46
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    47
foreach $file (@ARGV) {
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    48
  eval { &fixdatatype($file); };
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    49
  if ($@) { print STDERR "*** fixdatatype $file: ", $@, "\n"; }
0aa62210e67c Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff changeset
    50
}