#!/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: