conv-theory-files.pl
author nipkow
Tue May 09 22:10:08 1995 +0200 (1995-05-09)
changeset 1114 c8dfb56a7e95
parent 436 0cdc840297bb
permissions -rwxr-xr-x
Prod is now a parent of Lfp.
Added thm induct2 to Lfp.
Changed the way patterns in abstractions are pretty printed.
It has become simpler now but fails if split has more than one argument
because then the ast-translation does not match.
     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