author  berghofe 
Thu, 30 Jul 1998 15:49:18 +0200  
changeset 5213  0aa62210e67c 
child 8444  8f8eb220d9aa 
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$ 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

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

4 
# 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

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

6 

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

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

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

9 

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

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

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

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

13 

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

14 
$_ = $text; 
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 
## 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

17 
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

18 
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

19 

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

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

21 
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

22 

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

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

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

25 

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

26 
## replace res_inst_tac ... natE by exhaust_tac 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

27 
s/\bres_inst_tac\b\s*\[\s*\(\s*"[^"]+"\s*,\s*("[^"]+")\s*\)\s*\]\s*natE\b/exhaust_tac $1/sg; 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

28 

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

29 
$result = $_; 
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 
if ($text ne $result) { 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

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

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

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

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

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

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

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

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

40 
} 
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 
## main 
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 
foreach $file (@ARGV) { 
0aa62210e67c
Script that adapts theories and proof scripts to new datatype package.
berghofe
parents:
diff
changeset

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

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

48 
} 