lib/scripts/fixheaders.pl
author wenzelm
Mon, 20 Nov 2006 23:47:10 +0100
changeset 21426 87ac12bed1ab
parent 18125 50e63c68768f
permissions -rw-r--r--
converted legacy ML scripts;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16703
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
     1
#
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
     2
# $Id$
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
     3
# Author: Florian Haftmann, TUM
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
     4
#
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
     5
# fixheaders.pl - turn Isar theory headers into imports-uses-begin format
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
     6
#
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
     7
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
     8
use strict;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
     9
use File::Find;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    10
use File::Basename;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    11
use File::Copy;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    12
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    13
# configuration
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    14
my @suffices = ('\.thy');
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    15
my $backupsuffix = '~~';
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    16
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    17
# migrator function
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    18
sub fixheaders {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    19
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    20
    my ($file) = @_;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    21
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    22
    open(ISTREAM, $file) or die $!;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    23
    my @content = <ISTREAM>;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    24
    close ISTREAM or die $!;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    25
    my $content = join("", @content);
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    26
    $_ = $content;
18125
50e63c68768f allowing indentation of 'theory' keyword
haftmann
parents: 16703
diff changeset
    27
    if (m!^(\s*theory)!cgoms) {
16703
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    28
        my $prelude = $`;
18125
50e63c68768f allowing indentation of 'theory' keyword
haftmann
parents: 16703
diff changeset
    29
        my $thyheader = $1;
16703
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    30
        $thyheader .= skip_wscomment();
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    31
        if (m!\G(\S+)!cgoms) {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    32
            $thyheader .= $1;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    33
            $thyheader .= skip_wscomment();
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    34
            if (m!\G(?:imports|=)!cgoms) {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    35
                $thyheader .= "imports";
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    36
                $thyheader .= skip_wscomment() || " ";
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    37
                while (m/\G(?!uses|files|begin|:)/cgoms && m!\G(?:[\w_]+|"[^"]+")!cgoms) {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    38
                    $thyheader .= $&;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    39
                    $thyheader .= skip_wscomment();
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    40
                    if (m!\G\+!cgoms) {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    41
                        m!\G ?!cgoms;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    42
                    }
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    43
                    $thyheader .= skip_wscomment();
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    44
                }
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    45
            }
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    46
            if (m!\G(?:files|uses)!cgoms) {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    47
                $thyheader .= "uses";
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    48
                $thyheader .= skip_wscomment();
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    49
                while (m/\G(?!begin|:)/cgoms && m!\G(\("[^"]+"\)|"[^"]+"|[^"\s]+)!cgoms) {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    50
                    $thyheader .= $&;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    51
                    $thyheader .= skip_wscomment();
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    52
                }
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    53
            }
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    54
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    55
            if (m!\G(?:begin|:)!cgoms) {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    56
                my $postlude = $';
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    57
                if ($& eq ":") {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    58
                    $thyheader .= " ";
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    59
                }
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    60
                $thyheader .=  "begin";
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    61
                my $newcontent = "$prelude$thyheader$postlude";
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    62
                if ($content ne $newcontent) {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    63
                    print STDERR "fixing $file\n";
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    64
                    my $backupfile = "$file$backupsuffix";
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    65
                    if (! -f $backupfile) {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    66
                        rename $file, $backupfile or die $!;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    67
                    }
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    68
                    open(OSTREAM, ">$file") or die $!;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    69
                    print OSTREAM $newcontent;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    70
                    close(OSTREAM) or die $!;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    71
                }
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    72
            }
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    73
        }
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    74
    }
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    75
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    76
}
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    77
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    78
# utility functions
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    79
sub skip_wscomment {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    80
    my $commentlevel = 0;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    81
    my @skipped = ();
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    82
    while () {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    83
        if (m!\G\(\*!cgoms) {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    84
            push(@skipped, $&);
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    85
            $commentlevel++;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    86
        } elsif ($commentlevel > 0) {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    87
            if (m!\G\*\)!cgoms) {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    88
                push(@skipped, $&);
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    89
                $commentlevel--;
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    90
            } elsif (m/\G(?:
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    91
                        \*(?!\))|\((?!\*)|[^(*]
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    92
                       )*/cgomsx) {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    93
                push(@skipped, $&);
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    94
            } else {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    95
                die "probably incorrectly nested comment";
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    96
            }
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    97
        } elsif (m!\G\s+!cgoms) {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    98
            push(@skipped, $&);
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
    99
        } else {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
   100
            return join('', @skipped);
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
   101
        }
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
   102
    }
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
   103
}
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
   104
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
   105
# main
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
   106
foreach my $file (@ARGV) {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
   107
    eval {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
   108
        fixheaders($file);
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
   109
    };
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
   110
    if ($@) {
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
   111
        print STDERR "*** fixheaders $file: ", $@, "\n";
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
   112
    }
40a0b3187807 changed file permissions;
wenzelm
parents:
diff changeset
   113
}