|
1 #!/usr/bin/env perl -w |
|
2 # |
|
3 # $Id$ |
|
4 # Author: Florian Haftmann, TUM |
|
5 # |
|
6 # DESCRIPTION: migrates theory header (of new-style theories) to non-deprecated syntax |
|
7 |
|
8 use strict; |
|
9 use File::Find; |
|
10 use File::Basename; |
|
11 use File::Copy; |
|
12 |
|
13 # configuration |
|
14 my @suffices = ('\.thy'); |
|
15 my $backupsuffix = '~~'; |
|
16 |
|
17 # migrator function |
|
18 sub fixheaders { |
|
19 |
|
20 my ($file) = @_; |
|
21 |
|
22 open(ISTREAM, $file) or die $!; |
|
23 my @content = <ISTREAM>; |
|
24 close ISTREAM or die $!; |
|
25 my $content = join("", @content); |
|
26 $_ = $content; |
|
27 if (m!^theory!cgoms) { |
|
28 my $prelude = $`; |
|
29 my $thyheader = "theory"; |
|
30 $thyheader .= skip_wscomment(); |
|
31 if (m!\G(\S+)!cgoms) { |
|
32 $thyheader .= $1; |
|
33 $thyheader .= skip_wscomment(); |
|
34 if (m!\G(?:imports|=)!cgoms) { |
|
35 $thyheader .= "imports"; |
|
36 $thyheader .= skip_wscomment() || " "; |
|
37 while (m/\G(?!uses|files|begin|:)/cgoms && m!\G(?:[\w_]+|"[^"]+")!cgoms) { |
|
38 $thyheader .= $&; |
|
39 $thyheader .= skip_wscomment(); |
|
40 if (m!\G\+!cgoms) { |
|
41 m!\G ?!cgoms; |
|
42 } |
|
43 $thyheader .= skip_wscomment(); |
|
44 } |
|
45 } |
|
46 if (m!\G(?:files|uses)!cgoms) { |
|
47 $thyheader .= "uses"; |
|
48 $thyheader .= skip_wscomment(); |
|
49 while (m/\G(?!begin|:)/cgoms && m!\G(\("[^"]+"\)|"[^"]+"|[^"\s]+)!cgoms) { |
|
50 $thyheader .= $&; |
|
51 $thyheader .= skip_wscomment(); |
|
52 } |
|
53 } |
|
54 |
|
55 if (m!\G(?:begin|:)!cgoms) { |
|
56 my $postlude = $'; |
|
57 if ($& eq ":") { |
|
58 $thyheader .= " "; |
|
59 } |
|
60 $thyheader .= "begin"; |
|
61 my $newcontent = "$prelude$thyheader$postlude"; |
|
62 if ($content ne $newcontent) { |
|
63 print STDERR "fixing $file\n"; |
|
64 my $backupfile = "$file$backupsuffix"; |
|
65 if (! -f $backupfile) { |
|
66 rename $file, $backupfile or die $!; |
|
67 } |
|
68 open(OSTREAM, ">$file") or die $!; |
|
69 print OSTREAM $newcontent; |
|
70 close(OSTREAM) or die $!; |
|
71 } |
|
72 } |
|
73 } |
|
74 } |
|
75 |
|
76 } |
|
77 |
|
78 # utility functions |
|
79 sub skip_wscomment { |
|
80 my $commentlevel = 0; |
|
81 my @skipped = (); |
|
82 while () { |
|
83 if (m!\G\(\*!cgoms) { |
|
84 push(@skipped, $&); |
|
85 $commentlevel++; |
|
86 } elsif ($commentlevel > 0) { |
|
87 if (m!\G\*\)!cgoms) { |
|
88 push(@skipped, $&); |
|
89 $commentlevel--; |
|
90 } elsif (m/\G(?: |
|
91 \*(?!\))|\((?!\*)|[^(*] |
|
92 )*/cgomsx) { |
|
93 push(@skipped, $&); |
|
94 } else { |
|
95 die "probably incorrectly nested comment"; |
|
96 } |
|
97 } elsif (m!\G\s+!cgoms) { |
|
98 push(@skipped, $&); |
|
99 } else { |
|
100 return join('', @skipped); |
|
101 } |
|
102 } |
|
103 } |
|
104 |
|
105 # main |
|
106 foreach my $file (@ARGV) { |
|
107 eval { |
|
108 fixheaders($file); |
|
109 }; |
|
110 if ($@) { |
|
111 print STDERR "*** fixheaders $file: ", $@, "\n"; |
|
112 } |
|
113 } |