lib/Tools/expandshort
changeset 4416 c32a5c724263
parent 3007 e5efa177ee0c
child 4508 f102cb0140fe
equal deleted inserted replaced
4415:715e5e2064d8 4416:c32a5c724263
     8 PRG=$(basename $0)
     8 PRG=$(basename $0)
     9 
     9 
    10 function usage()
    10 function usage()
    11 {
    11 {
    12   echo
    12   echo
    13   echo "Usage: $PRG [FILES ...]"
    13   echo "Usage: $PRG [FILES|DIRS...]"
    14   echo
    14   echo
    15   echo "  Expand shorthand goal commands in FILES.  Also contracts uses of"
    15   echo "  Recursively find .ML files, expand shorthand goal commands."
    16   echo "  resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on"
    16   echo "  Also contracts uses of resolve_tac, dresolve_tac, eresolve_tac,"
    17   echo "  1-element lists; furthermore expands tabs, since they are now"
    17   echo "  rewrite_goals_tac on 1-element lists; furthermore expands tabs,"
    18   echo "  forbidden in ML string constants."
    18   echo "  since they are now forbidden in ML string constants."
    19   echo
    19   echo
    20   echo "  Renames old versions of FILES by appending \"~~\"."
    20   echo "  Renames old versions of files by appending \"~~\"."
    21   echo
    21   echo
    22   exit 1
    22   exit 1
    23 }
    23 }
    24 
    24 
    25 function fail()
    25 
    26 {
    26 ## process command line
    27   echo "$1" >&2
    27 
    28   exit 2
    28 [ $# -eq 0 -o "$1" = "-?" ] && usage
    29 }
    29 
       
    30 SPECS="$@"; shift $#
    30 
    31 
    31 
    32 
    32 ## main
    33 ## main
    33 
    34 
    34 [ "$1" = "-?" ] && usage
    35 PERL=$(type -path perl)
    35 
    36 if [ -z $PERL ]; then
    36 for f in "$@"
    37   echo "$PRG fatal error: no perl!?"
    37 do
    38 else
    38 echo Expanding shorthands in $f. \ Backup file is $f~~
    39   find $SPECS -name \*.ML -print | xargs $PERL $ISABELLE_HOME/lib/scripts/expandshort.pl
    39 if [ ! -s $f ]; then echo "File $f is EMPTY!!"; exit 1; fi
    40 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.