lib/Tools/update_op

tuned signature;

#!/usr/bin/env bash
#
# Author: Tobias Nipkow, TU Muenchen
#
# DESCRIPTION: update "op _" syntax

## diagnostics

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
  echo
  echo "  Options are:"
  echo "    -m           ignore .ML files"
  echo
  echo "  Update the old \"op _\" syntax in theory and ML files."
  echo
  exit 1
}


IGNORE_ML=""

while getopts "m" OPT
do
  case "$OPT" in
    m)
      IGNORE_ML="true"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))

DIR="."
if [ -n "$1" ]; then
  DIR="$1"
fi

read -r -d '' THY_SCRIPT <<'EOF'
# op [^]\<^bsub>*\<^esub> -> ([^]\<^bsub>*\<^esub>)
s/\([^a-zA-Z0-9_?']\)op [ ]*\(\[\^\]\\<\^bsub>[^\\]*\\<\^esub>\)/\1(\2)/g
# op *XY -> ( *XY)
s/\([^a-zA-Z0-9_?']\)op[ ]*\*\([a-zA-Z][a-zA-Z]\)/\1( \*\2)/g
# op *X -> ( *X)
s/\([^a-zA-Z0-9_?']\)op[ ]*\*\([a-zA-Z]\)/\1( \*\2)/g
# op *R -> ( *R)
s/\([^a-zA-Z0-9_?']\)op[ ]*\(\*\\<^sub>[a-zA-Z]\)/\1( \2)/g
# op *\<cdot> -> ( *\<cdot>)
s/\([^a-zA-Z0-9_?']\)op[ ]*\(\*\\<cdot>\)/\1( \2)/g
# op ** -> ( ** )
s/\([^a-zA-Z0-9_?']\)op[ ]*\*\*/\1( \*\* )/g
# op * -> ( * )
s/\([^a-zA-Z0-9_?']\)op[ ]*\*/\1( \* )/g
# (op +) -> (+)
s/(op [ ]*\([^ )("][^ )(",]*\))/(\1)/g
# (op + -> ((+)
s/(op [ ]*\([^ )(",]*\)\([^)]\)/((\1)\2/g
# op + -> (+)
s/\([^a-zA-Z0-9_?']\)op [ ]*\([^ )(",:]*\)::/\1(\2)::/g
s/\([^a-zA-Z0-9_?']\)op [ ]*\([^ )(",]*\)/\1(\2)/g
# op+ -> (+)
s/\([^a-zA-Z0-9_?']\)op\(\\<[a-zA-Z0-9]*>\)/\1(\2)/g
s/\([^a-zA-Z0-9_?']\)op\([^a-zA-Z0-9_? )("\][^ )(",:]*\)::/\1(\2)::/g
s/\([^a-zA-Z0-9_?']\)op\([^a-zA-Z0-9_? )("\][^ )(",]*\)/\1(\2)/g
EOF

read -r -d '' ML_SCRIPT <<'EOF'
# op * -> ( * )
s/"\(.*\)\([^a-zA-Z0-9_]\)op[ ]*\*/"\1\2( \* )/g
s/"op[ ]*\*/"( \* )/g
# (op +) -> (+)
s/"\(.*\)(op [ ]*\([^ )("][^ )("]*\))/"\1(\2)/g
s/(op [ ]*\([^ )("][^ )("]*\))\(.*\)"/(\1)\2"/g
# (op + -> ((+)
s/"\(.*\)(op [ ]*\([^ )("]*\)\([^)]\)/"\1((\2)\3/g
# op + -> (+)
s/"\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)/"\1\2(\3)/g
s/"op [ ]*\([^ )("]*\)/"(\1)/g
# op+ -> (+)
s/"\(.*\)\([^a-zA-Z0-9_]\)op\([^a-zA-Z0-9_ )("][^ )("]*\)/"\1\2(\3)/g
s/"op\([^a-zA-Z0-9_ )("][^ )("]*\)/"(\1)/g
# is there \<...\> on the line (indicating Isabelle source):
s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op \*/\\<\1>\2\3( * )/g
s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)\\<close>/\\<\1>\2\3(\4)\\<close>/g
s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)/\\<\1>\2\3(\4)/g
s/\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)\(.*\)\\<\([^>]*\)>/\1(\2)\3\\<\4>/g
EOF

find "$DIR" -name "*.thy" -exec sed '-i~~' -e "$THY_SCRIPT" {} \;

[ "$IGNORE_ML" = "true" ] || find "$DIR" -name "*.ML" -exec sed '-i~~' -e "$ML_SCRIPT" {} \;