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