author  wenzelm 
Tue, 13 Feb 2001 16:31:18 +0100  
changeset 11109  ce1cefc6c14c 
parent 9789  7e5e6c47c0b5 
child 14981  e73f8140af78 
permissions  rwrr 
5213
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

1 
# 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

2 
# $Id$ 
9789  3 
# Author: Markus Wenzel, TU Muenchen 
4 
# License: GPL (GNU GENERAL PUBLIC LICENSE) 

5213
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

5 
# 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

6 
# fixdatatype.pl  adapt theories and proof scripts to new datatype package 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

7 
# 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

8 

0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

9 
sub fixdatatype { 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

10 
my ($file) = @_; 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

11 

0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

12 
open (FILE, $file)  die $!; 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

13 
undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

14 
close FILE  die $!; 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

15 

0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

16 
$_ = $text; 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

17 

0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

18 
## convert split_type_case[_asm] to type.split[_asm] 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

19 
s/([^"])\bsplit_([\w]+)_case\b/$1$2.split/sg; 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

20 
s/([^"])\bsplit_([\w]+)_case_asm\b/$1$2.split_asm/sg; 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

21 

0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

22 
## delete function name and type after "primrec" 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

23 
s/\bprimrec\b\s+([\w]+"[^"]+")\s+([\w\.]+)/primrec/sg; 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

24 

0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

25 
## replace specific induct_tac by generic induct_tac 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

26 
s/[\w\.]+\.induct_tac/induct_tac/sg; 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

27 

8444  28 
## replace res_inst_tac ... natE by case_tac 
29 
s/\bres_inst_tac\b\s*\[\s*\(\s*"[^"]+"\s*,\s*("[^"]+")\s*\)\s*\]\s*natE\b/case_tac $1/sg; 

5213
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

30 

0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

31 
$result = $_; 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

32 

0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

33 
if ($text ne $result) { 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

34 
print STDERR "fixing $file\n"; 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

35 
if (! f "$file~~") { 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

36 
rename $file, "$file~~"  die $!; 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

37 
} 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

38 
open (FILE, "> $file")  die $!; 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

39 
print FILE $result; 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

40 
close FILE  die $!; 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

41 
} 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

42 
} 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

43 

0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

44 

0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

45 
## main 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

46 

0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

47 
foreach $file (@ARGV) { 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

48 
eval { &fixdatatype($file); }; 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

49 
if ($@) { print STDERR "*** fixdatatype $file: ", $@, "\n"; } 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

50 
} 