author  paulson 
Mon, 16 Nov 1998 10:36:30 +0100  
changeset 5865  2303f5a3036d 
parent 5324  ec84178243ff 
child 7491  95a4af0e10a7 
permissions  rwrr 
4417  1 
# 
2 
# $Id$ 

3 
# 

4 
# expandshort.pl  expand shorthand goal commands 

5 
# 

4478
9c5a0eef74ff
More restrictive patterns to prevent changing comments
paulson
parents:
4417
diff
changeset

6 
# in "be ... i;" > "by (etac ... i);" the "..." phrase is not allowed to 
9c5a0eef74ff
More restrictive patterns to prevent changing comments
paulson
parents:
4417
diff
changeset

7 
# contain punctuation. Otherwise, comments can be affected! 
5324
ec84178243ff
Now allows "." in rule names, with special treatment for "be"
paulson
parents:
4592
diff
changeset

8 
# a special case is made to detect be alpha.alpha digits 
4417  9 

10 
sub expandshort { 

11 
my ($file) = @_; 

12 

13 
open (FILE, $file)  die $!; 

14 
undef $/; $text = <FILE>; $/ = "\n"; # slurp whole file 

15 
close FILE  die $!; 

16 

17 
$_ = $text; 

18 

19 
s/\bsafe_tac *\(claset *\( *\) *\)/Safe_tac/sg; 

4592  20 
s/ *\(Safe_tac\) *([09]+)/ Safe_tac $1/sg; 
4417  21 
s/ *\(Safe_tac\)/ Safe_tac/sg; 
22 
s/\bby\(/by (/sg; 

4592  23 
s/\bba\b *(\d+);/by (assume_tac $1);/sg; 
5324
ec84178243ff
Now allows "." in rule names, with special treatment for "be"
paulson
parents:
4592
diff
changeset

24 
s/\bbr\b *([^;*!]*) (\d+);/by (rtac $1 $2);/sg; 
ec84178243ff
Now allows "." in rule names, with special treatment for "be"
paulson
parents:
4592
diff
changeset

25 
s/\bbrs\b *([^;*!]*) (\d+);/by (resolve_tac $1 $2);/sg; 
ec84178243ff
Now allows "." in rule names, with special treatment for "be"
paulson
parents:
4592
diff
changeset

26 
s/\bbd\b *([^;*!]*) (\d+);/by (dtac $1 $2);/sg; 
ec84178243ff
Now allows "." in rule names, with special treatment for "be"
paulson
parents:
4592
diff
changeset

27 
s/\bbds\b *([^;*!]*) (\d+);/by (dresolve_tac $1 $2);/sg; 
4592  28 
s/\bbe\b *([^;.*!]*) (\d+);/by (etac $1 $2);/sg; 
5324
ec84178243ff
Now allows "." in rule names, with special treatment for "be"
paulson
parents:
4592
diff
changeset

29 
s/\bbe\b *(\w+\.\w+) (\d+);/by (etac $1 $2);/sg; 
ec84178243ff
Now allows "." in rule names, with special treatment for "be"
paulson
parents:
4592
diff
changeset

30 
s/\bbes\b *([^;*!]*) (\d+);/by (eresolve_tac $1 $2);/sg; 
ec84178243ff
Now allows "." in rule names, with special treatment for "be"
paulson
parents:
4592
diff
changeset

31 
s/\bbw\b *([^;*!]*);/by (rewtac $1);/sg; 
ec84178243ff
Now allows "." in rule names, with special treatment for "be"
paulson
parents:
4592
diff
changeset

32 
s/\bbws\b *([^;*!]*);/by (rewrite_goals_tac $1);/sg; 
4478
9c5a0eef74ff
More restrictive patterns to prevent changing comments
paulson
parents:
4417
diff
changeset

33 
s/\bauto *\(\)/by Auto_tac/sg; 
4592  34 
s/dresolve_tac *\[(\w+)\] */dtac $1 /sg; 
35 
s/eresolve_tac *\[(\w+)\] */etac $1 /sg; 

36 
s/resolve_tac *\[(\w+)\] */rtac $1 /sg; 

37 
s/rewrite_goals_tac *\[(\w+)\]( *)/rewtac $1$2/sg; 

38 
s/rtac *\((\w+)\s+RS\s+ssubst\)\s+/stac $1 /sg; 

4417  39 

40 
$result = $_; 

41 

42 
if ($text ne $result) { 

43 
print STDERR "expanding $file\n"; 

44 
if (! f "$file~~") { 

45 
rename $file, "$file~~"  die $!; 

46 
} 

47 
open (FILE, "> $file")  die $!; 

48 
print FILE $result; 

49 
close FILE  die $!; 

50 
} 

51 
} 

52 

53 

54 
## main 

55 

56 
foreach $file (@ARGV) { 

57 
eval { &expandshort($file); }; 

58 
if ($@) { print STDERR "*** expandshort $file: ", $@, "\n"; } 

59 
} 