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