1 #!/usr/bin/perl -s- # -*-Perl-*- |
|
2 |
|
3 #--------------------------------------------------------------------- |
|
4 #The following script file is useful to convert old theory files into a |
|
5 #style consistent with new naming conventions. Now, the names of the |
|
6 #files must be the same as the names of the theories they define (with |
|
7 #a ".thy" suffix) and corresponding ML files must also be renamed. |
|
8 # |
|
9 #To make this renaming easier, the following perl script can be used. |
|
10 #It traverses the given directory recursively. For each file of the |
|
11 #form abc.thy, this script does the following steps: |
|
12 # |
|
13 #1. Reads the file and grabs the first identifier, say Abc (skipping comments |
|
14 # (*...*) and white space). |
|
15 #2. Outputs the commands needed to rename the file abc.thy to Abc.thy, |
|
16 # including the appropriate CVS commands. |
|
17 #3. If abc.ML also exists, it outputs appropriate commands to rename it |
|
18 # to Abc.ML. |
|
19 # |
|
20 #These commands can be put into a file, which can then be executed. |
|
21 #If you are not using cvs, use "grep" to extract just the "mv" commands. |
|
22 # |
|
23 # - Sara Kalvala |
|
24 # (sk@cl.cam.ac.uk) |
|
25 #--------------------------------------------------------------------- |
|
26 |
|
27 open(MATCH_FILES, "find . -name \"*thy\" -print |"); |
|
28 |
|
29 foreach $each_match (<MATCH_FILES>) { |
|
30 chop($each_match); |
|
31 if($each_match =~ /(.*\/)(\w*)\.thy/) {$dirpart = $1;} |
|
32 else {print "something wrong with finding path!\n"; |
|
33 $dirpart = "";} |
|
34 open (CONTENTS, $each_match); |
|
35 @readit = <CONTENTS>; |
|
36 chop(@readit); $oneline = join(" ",@readit); |
|
37 $oneline =~ s/\(\*([^\*]|(\*[^\)]))*\*\)//g ; |
|
38 # comments: have to remove strings of anything but stars or stars |
|
39 # followed by anything but right parenthesis |
|
40 if($oneline =~ /\s*([^ ]*)\s*=.*/) |
|
41 {$th_name = $1; |
|
42 $new_name = $dirpart . $th_name . ".thy"; |
|
43 print "mv -i $each_match $new_name \n"; |
|
44 print "cvs rm $each_match ; cvs add $new_name \n"; |
|
45 # for ML files |
|
46 $each_ML = $each_match; |
|
47 $each_ML =~ s/.thy/.ML/; |
|
48 if (-e $each_ML) { $new_ML = $dirpart . $th_name . ".ML"; |
|
49 print "mv -i $each_ML $new_ML \n"; |
|
50 print "cvs rm $each_ML ; cvs add $new_ML \n";}} |
|
51 else {print "something wrong with format of theory file!\n";} |
|
52 } |
|
53 |
|