lib/Tools/expandshort
author wenzelm
Tue, 22 Apr 1997 11:37:12 +0200
changeset 3007 e5efa177ee0c
parent 2588 b472d703fa06
child 4416 c32a5c724263
permissions -rwxr-xr-x
removed -norc;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3007
e5efa177ee0c removed -norc;
wenzelm
parents: 2588
diff changeset
     1
#!/bin/bash
2546
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
     2
#
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
     3
# $Id$
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
     4
#
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: expand shorthand goal commands
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
     6
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
     7
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
     8
PRG=$(basename $0)
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
     9
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    10
function usage()
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    11
{
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    12
  echo
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    13
  echo "Usage: $PRG [FILES ...]"
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    14
  echo
2547
wenzelm
parents: 2546
diff changeset
    15
  echo "  Expand shorthand goal commands in FILES.  Also contracts uses of"
wenzelm
parents: 2546
diff changeset
    16
  echo "  resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on"
wenzelm
parents: 2546
diff changeset
    17
  echo "  1-element lists; furthermore expands tabs, since they are now"
2588
b472d703fa06 improved usage msg;
wenzelm
parents: 2547
diff changeset
    18
  echo "  forbidden in ML string constants."
2546
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    19
  echo
2547
wenzelm
parents: 2546
diff changeset
    20
  echo "  Renames old versions of FILES by appending \"~~\"."
2546
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    21
  echo
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    22
  exit 1
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    23
}
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    24
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    25
function fail()
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    26
{
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    27
  echo "$1" >&2
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    28
  exit 2
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    29
}
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    30
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    31
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    32
## main
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    33
2547
wenzelm
parents: 2546
diff changeset
    34
[ "$1" = "-?" ] && usage
wenzelm
parents: 2546
diff changeset
    35
2546
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    36
for f in "$@"
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    37
do
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    38
echo Expanding shorthands in $f. \ Backup file is $f~~
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    39
if [ ! -s $f ]; then echo "File $f is EMPTY!!"; exit 1; fi
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    40
mv $f $f~~; sed -e '
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    41
s/\<by(/by (/
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    42
s/\<ba \([0-9][0-9]*\);/by (assume_tac \1);/
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    43
s/\<br \([^;]*\) \([0-9][0-9]*\);/by (rtac \1 \2);/
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    44
s/\<brs \([^;]*\) \([0-9][0-9]*\);/by (resolve_tac \1 \2);/
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    45
s/\<bd \([^;]*\) \([0-9][0-9]*\);/by (dtac \1 \2);/
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    46
s/\<bds \([^;]*\) \([0-9][0-9]*\);/by (dresolve_tac \1 \2);/
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    47
s/\<be \([^;]*\) \([0-9][0-9]*\);/by (etac \1 \2);/
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    48
s/\<bes \([^;]*\) \([0-9][0-9]*\);/by (eresolve_tac \1 \2);/
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    49
s/\<bw \([^;]*\);/by (rewtac \1);/
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    50
s/\<bws \([^;]*\);/by (rewrite_goals_tac \1);/
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    51
s/\<auto *()/by (Auto_tac())/
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    52
s/dresolve_tac *\[\([a-zA-Z0-9_]*\)\] */dtac \1 /g
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    53
s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    54
s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    55
s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    56
s/rtac *(\([a-zA-Z0-9_]*\)  *RS  *ssubst)  */stac \1 /g
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    57
' $f~~ | expand > $f
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    58
done
866957616069 expand shorthand goal commands;
wenzelm
parents:
diff changeset
    59
echo Finished.