Admin/isa-migrate

migrated theory headers to new format

#!/usr/bin/env perl
#
# $Id$
# Author: Florian Haftmann, TUM
#
# A generic framework script for simple theory file migrations
# (under developement)
#

use strict;
use File::Find;
use File::Basename;
use File::Copy;

# configuration
my @suffices = ('\.thy');
my $backupext = '.bak';

# migrator lookup hash
my %migrators = (
    id => sub {
        my ($file, @content) = @_;
    },
    thyheader => sub {
        my ($file, @content) = @_;
        #~ my $diag = 1;
        my $diag = 0;
        $_ = join("", @content);
        if (m!^theory!cgoms) {
            my $prelude = $`;
            my $thyheader = "theory";
            $thyheader .= skip_wscomment();
            if (m!\G(\S+)!cgoms) {
                $thyheader .= $1;
                $thyheader .= skip_wscomment();
                $diag and print "--->\n(1)>>>$thyheader<<<\n<---\n";
                if (m!\G(?:imports|=)!cgoms) {
                    $thyheader .= "imports";
                    $thyheader .= skip_wscomment() || " ";
                    $diag and print "--->\n(2)>>>$thyheader<<<\n<---\n";
                    while (m/\G(?!uses|files|begin|:)/cgoms && m!\G(?:[\w_]+|"[^"]+")!cgoms) {
                        $diag and print "--->\n(3)>>>$&<<<\n<---\n";
                        $thyheader .= $&;
                        $thyheader .= skip_wscomment();
                        if (m!\G\+!cgoms) {
                            m!\G ?!cgoms;
                        }
                        $thyheader .= skip_wscomment();
                        #~ if (m/\G(?!uses|files|begin|:)/cgoms) { print '!!!'; }
                        #~ if (m!\G[\w_]+!cgoms) { print '§§§'; }
                    }
                    $diag and print "--->\n(4)>>>$thyheader<<<\n<---\n";
                }
                #~ m!\G.{19}!cgoms;
                #~ print "***$&\n";
                #~ die;
                if (m!\G(?:files|uses)!cgoms) {
                    $thyheader .= "uses";
                    $thyheader .= skip_wscomment();
                    $diag and print "--->\n(5)>>>$thyheader<<<\n<---\n";
                    while (m/\G(?!begin|:)/cgoms && m!\G(\("[^"]+"\)|"[^"]+"|[^"\s]+)!cgoms) {
                        $diag and print "--->\n(6)>>>$&<<<\n<---\n";
                        $thyheader .= $&;
                        $thyheader .= skip_wscomment();
                    }
                    $diag and print "--->\n(7)>>>$thyheader<<<\n<---\n";
                }
                

                if (m!\G(?:begin|:)!cgoms) {
                    my $postlude = $';
                    if ($& eq ":") {
                        $thyheader .= " ";
                    }
                    $thyheader .=  "begin";
                    # do replacement here
                    if ($diag) {
                        print "$file:\n$thyheader\n\n";
                    } else {
                        open(OSTREAM, ">$file") or die("error opening $file");
                        print OSTREAM "$prelude$thyheader$postlude";
                        close(OSTREAM);
                    }
                }
            }
        }
    }
);

# utility functions
sub skip_wscomment {
    my $commentlevel = 0;
    my @skipped = ();
    while () {
        if (m!\G\(\*!cgoms) {
            push(@skipped, $&);
            $commentlevel++;
        } elsif ($commentlevel > 0) {
            if (m!\G\*\)!cgoms) {
                push(@skipped, $&);
                $commentlevel--;
            } elsif (m/\G(?:
                        \*(?!\))|\((?!\*)|[^(*]
                       )*/cgomsx) {
                push(@skipped, $&);
            } else {
                die ("probably incorrectly nested comment");
            }
        } elsif (m!\G\s+!cgoms) {
            push(@skipped, $&);
        } else {
            return join('', @skipped);
        }
    }
}

# process dir tree
sub process_tree {
    my ($root, $migrator, $backupext) = @_;
    find(sub { process($_, $migrator, $backupext) }, $root);
}

# process single file
sub process {
    my ($file, $migrator, $backupext) = @_;
    my ($basename, $dirname, $ext) = fileparse($file, @suffices);
    #~ print "$file\n";
    if ($ext) {
        open(ISTREAM, $file) or die("error opening $file");
        my @content = <ISTREAM>;
        close ISTREAM;
        if ($backupext) {
            copy($file, "$file$backupext");
        }
        print "Migrating $file...\n";
        &$migrator($file, @content);
    }
}

# first argument: migrator name
my $migrator = $migrators{shift @ARGV};
$migrator or die ("invalid migrator name");
# other arguments: files or trees
foreach my $fileloc (@ARGV) {
    -e $fileloc or die ("no file $fileloc");
}
foreach my $fileloc (@ARGV) {
    if (-d $fileloc) {
        process_tree($fileloc, $migrator, $backupext);
    } else {
        process($fileloc, $migrator, $backupext);
    }
}

#!!! example file: