src/Tools/Metis/make-metis

explicit indication of Unsynchronized.ref;

#!/usr/bin/env bash
#
# make-metis - turn original Metis files into Isabelle ML source.
#
# Structure declarations etc. are made local by wrapping into a
# collective structure Metis.  Signature and functor definitions are
# global!

THIS=$(cd "$(dirname "$0")"; echo $PWD)

(
  cat <<EOF
(******************************************************************)
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
(******************************************************************)

print_depth 0;

structure Metis = struct structure Word = Word structure Array = Array end;
EOF

  for FILE in $(cat "$THIS/src/FILES")
  do
    echo
    echo "(**** Original file: $FILE ****)"
    echo
    if [ "$(basename "$FILE" .sig)" != "$FILE" ]
    then
      echo -e "$FILE (global)" >&2
      "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
      perl -p -e 's/\b([A-Za-z]+\.[A-Za-z]+)/Metis.\1/g;' -e 's/\bfrag\b/Metis.frag/;' | \
      perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
    elif fgrep -q functor "src/$FILE"
    then
      "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
      perl -p -e 's/ union / op union /g;' -e 's/ subset / op subset /g;' | \
      perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
    else
      echo -e "$FILE (local)" >&2
      echo "structure Metis = struct open Metis"
      cat < "metis_env.ML"
      "$THIS/scripts/mlpp" -c isabelle "src/$FILE" | \
      perl -p -e 's/\bref\b/Unsynchronized.ref/g;'
      echo "end;"
    fi
  done

  echo "print_depth 10;"

) > metis.ML