lib/scripts/fixdatatype.pl
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 9789 7e5e6c47c0b5
permissions -rw-r--r--
Merged in license change from Isabelle2004
berghofe@5213
     1
#
berghofe@5213
     2
# $Id$
wenzelm@9789
     3
# Author: Markus Wenzel, TU Muenchen
berghofe@5213
     4
#
berghofe@5213
     5
# fixdatatype.pl - adapt theories and proof scripts to new datatype package
berghofe@5213
     6
#
berghofe@5213
     7
berghofe@5213
     8
sub fixdatatype {
berghofe@5213
     9
    my ($file) = @_;
berghofe@5213
    10
berghofe@5213
    11
    open (FILE, $file) || die $!;
berghofe@5213
    12
    undef $/; $text = <FILE>; $/ = "\n";         # slurp whole file
berghofe@5213
    13
    close FILE || die $!;
berghofe@5213
    14
berghofe@5213
    15
    $_ = $text;
berghofe@5213
    16
berghofe@5213
    17
    ## convert split_type_case[_asm] to type.split[_asm]
berghofe@5213
    18
    s/([^"])\bsplit_([\w]+)_case\b/$1$2.split/sg;
berghofe@5213
    19
    s/([^"])\bsplit_([\w]+)_case_asm\b/$1$2.split_asm/sg;
berghofe@5213
    20
berghofe@5213
    21
    ## delete function name and type after "primrec"
berghofe@5213
    22
    s/\bprimrec\b\s+([\w]+|"[^"]+")\s+([\w\.]+)/primrec/sg;
berghofe@5213
    23
berghofe@5213
    24
    ## replace specific induct_tac by generic induct_tac
berghofe@5213
    25
    s/[\w\.]+\.induct_tac/induct_tac/sg;
berghofe@5213
    26
wenzelm@8444
    27
    ## replace res_inst_tac ... natE by case_tac
wenzelm@8444
    28
    s/\bres_inst_tac\b\s*\[\s*\(\s*"[^"]+"\s*,\s*("[^"]+")\s*\)\s*\]\s*natE\b/case_tac $1/sg;
berghofe@5213
    29
berghofe@5213
    30
    $result = $_;
berghofe@5213
    31
berghofe@5213
    32
    if ($text ne $result) {
berghofe@5213
    33
        print STDERR "fixing $file\n";
berghofe@5213
    34
        if (! -f "$file~~") {
berghofe@5213
    35
            rename $file, "$file~~" || die $!;
berghofe@5213
    36
        }
berghofe@5213
    37
        open (FILE, "> $file") || die $!;
berghofe@5213
    38
        print FILE $result;
berghofe@5213
    39
        close FILE || die $!;
berghofe@5213
    40
    }
berghofe@5213
    41
}
berghofe@5213
    42
berghofe@5213
    43
berghofe@5213
    44
## main
berghofe@5213
    45
berghofe@5213
    46
foreach $file (@ARGV) {
berghofe@5213
    47
  eval { &fixdatatype($file); };
berghofe@5213
    48
  if ($@) { print STDERR "*** fixdatatype $file: ", $@, "\n"; }
berghofe@5213
    49
}