added fixheaders
authorhaftmann
Mon Jun 20 11:30:44 2005 +0200 (2005-06-20)
changeset 16471c487e7e8865f
parent 16470 051db5bb21b5
child 16472 40c4653a30d5
added fixheaders
lib/Tools/fixheaders
lib/scripts/fixheaders.pl
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/Tools/fixheaders	Mon Jun 20 11:30:44 2005 +0200
     1.3 @@ -0,0 +1,40 @@
     1.4 +#!/usr/bin/env bash
     1.5 +#
     1.6 +# $Id$
     1.7 +# Author: Florian Haftmann, TUM
     1.8 +#
     1.9 +# DESCRIPTION: migrates theory header (of new-style theories) to non-deprecated syntax
    1.10 +
    1.11 +
    1.12 +## diagnostics
    1.13 +
    1.14 +PRG="$(basename "$0")"
    1.15 +
    1.16 +function usage()
    1.17 +{
    1.18 +  echo
    1.19 +  echo "Usage: $PRG [FILES|DIRS...]"
    1.20 +  echo
    1.21 +  echo "  Recursively find .thy files, patching them to ensure that"
    1.22 +  echo "  theory headers (of new-style theories) are in non-deprecated format."
    1.23 +  echo
    1.24 +  echo "  Renames old versions of FILES by appending \"~~\"."
    1.25 +  echo
    1.26 +  exit 1
    1.27 +}
    1.28 +
    1.29 +
    1.30 +## process command line
    1.31 +
    1.32 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    1.33 +
    1.34 +SPECS="$@"; shift "$#"
    1.35 +
    1.36 +
    1.37 +## main
    1.38 +
    1.39 +#set by configure
    1.40 +AUTO_PERL=perl
    1.41 +
    1.42 +find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
    1.43 +  xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixheaders.pl"
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/lib/scripts/fixheaders.pl	Mon Jun 20 11:30:44 2005 +0200
     2.3 @@ -0,0 +1,113 @@
     2.4 +#!/usr/bin/env perl -w
     2.5 +#
     2.6 +# $Id$
     2.7 +# Author: Florian Haftmann, TUM
     2.8 +#
     2.9 +# DESCRIPTION: migrates theory header (of new-style theories) to non-deprecated syntax
    2.10 +
    2.11 +use strict;
    2.12 +use File::Find;
    2.13 +use File::Basename;
    2.14 +use File::Copy;
    2.15 +
    2.16 +# configuration
    2.17 +my @suffices = ('\.thy');
    2.18 +my $backupsuffix = '~~';
    2.19 +
    2.20 +# migrator function
    2.21 +sub fixheaders {
    2.22 +
    2.23 +    my ($file) = @_;
    2.24 +
    2.25 +    open(ISTREAM, $file) or die $!;
    2.26 +    my @content = <ISTREAM>;
    2.27 +    close ISTREAM or die $!;
    2.28 +    my $content = join("", @content);
    2.29 +    $_ = $content;
    2.30 +    if (m!^theory!cgoms) {
    2.31 +        my $prelude = $`;
    2.32 +        my $thyheader = "theory";
    2.33 +        $thyheader .= skip_wscomment();
    2.34 +        if (m!\G(\S+)!cgoms) {
    2.35 +            $thyheader .= $1;
    2.36 +            $thyheader .= skip_wscomment();
    2.37 +            if (m!\G(?:imports|=)!cgoms) {
    2.38 +                $thyheader .= "imports";
    2.39 +                $thyheader .= skip_wscomment() || " ";
    2.40 +                while (m/\G(?!uses|files|begin|:)/cgoms && m!\G(?:[\w_]+|"[^"]+")!cgoms) {
    2.41 +                    $thyheader .= $&;
    2.42 +                    $thyheader .= skip_wscomment();
    2.43 +                    if (m!\G\+!cgoms) {
    2.44 +                        m!\G ?!cgoms;
    2.45 +                    }
    2.46 +                    $thyheader .= skip_wscomment();
    2.47 +                }
    2.48 +            }
    2.49 +            if (m!\G(?:files|uses)!cgoms) {
    2.50 +                $thyheader .= "uses";
    2.51 +                $thyheader .= skip_wscomment();
    2.52 +                while (m/\G(?!begin|:)/cgoms && m!\G(\("[^"]+"\)|"[^"]+"|[^"\s]+)!cgoms) {
    2.53 +                    $thyheader .= $&;
    2.54 +                    $thyheader .= skip_wscomment();
    2.55 +                }
    2.56 +            }
    2.57 +
    2.58 +            if (m!\G(?:begin|:)!cgoms) {
    2.59 +                my $postlude = $';
    2.60 +                if ($& eq ":") {
    2.61 +                    $thyheader .= " ";
    2.62 +                }
    2.63 +                $thyheader .=  "begin";
    2.64 +                my $newcontent = "$prelude$thyheader$postlude";
    2.65 +                if ($content ne $newcontent) {
    2.66 +                    print STDERR "fixing $file\n";
    2.67 +                    my $backupfile = "$file$backupsuffix";
    2.68 +                    if (! -f $backupfile) {
    2.69 +                        rename $file, $backupfile or die $!;
    2.70 +                    }
    2.71 +                    open(OSTREAM, ">$file") or die $!;
    2.72 +                    print OSTREAM $newcontent;
    2.73 +                    close(OSTREAM) or die $!;
    2.74 +                }
    2.75 +            }
    2.76 +        }
    2.77 +    }
    2.78 +
    2.79 +}
    2.80 +
    2.81 +# utility functions
    2.82 +sub skip_wscomment {
    2.83 +    my $commentlevel = 0;
    2.84 +    my @skipped = ();
    2.85 +    while () {
    2.86 +        if (m!\G\(\*!cgoms) {
    2.87 +            push(@skipped, $&);
    2.88 +            $commentlevel++;
    2.89 +        } elsif ($commentlevel > 0) {
    2.90 +            if (m!\G\*\)!cgoms) {
    2.91 +                push(@skipped, $&);
    2.92 +                $commentlevel--;
    2.93 +            } elsif (m/\G(?:
    2.94 +                        \*(?!\))|\((?!\*)|[^(*]
    2.95 +                       )*/cgomsx) {
    2.96 +                push(@skipped, $&);
    2.97 +            } else {
    2.98 +                die "probably incorrectly nested comment";
    2.99 +            }
   2.100 +        } elsif (m!\G\s+!cgoms) {
   2.101 +            push(@skipped, $&);
   2.102 +        } else {
   2.103 +            return join('', @skipped);
   2.104 +        }
   2.105 +    }
   2.106 +}
   2.107 +
   2.108 +# main
   2.109 +foreach my $file (@ARGV) {
   2.110 +    eval {
   2.111 +        fixheaders($file);
   2.112 +    };
   2.113 +    if ($@) {
   2.114 +        print STDERR "*** fixheaders $file: ", $@, "\n";
   2.115 +    }
   2.116 +}