src/Tools/Metis/make_metis

explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
tuned;

#!/usr/bin/env bash
#
# make_metis - turn original Metis files into Isabelle ML source.
#
# Signatures, structures, and functors are renamed to have a "Metis_" prefix.
# A few other ad hoc transformations are performed to ensure that the sources
# compile within Isabelle on Poly/ML and SML/NJ.

THIS=$(cd "$(dirname "$0")"; echo $PWD)
make -f Makefile.FILES refresh_FILES
FILES=$(cat "$THIS/FILES")

(
  cat <<EOF
(*
   This file was generated by the "make_metis" script. The BSD License is used
   with Joe Hurd's kind permission. Extract from a September 13, 2010 email
   written by Joe Hurd:

       I hereby give permission to the Isabelle team to release Metis as part
       of Isabelle, with the Metis code covered under the Isabelle BSD
       license.
*)

(******************************************************************)
(* 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;

EOF

  for FILE in $FILES
  do
    echo
    echo "(**** Original file: $FILE ****)"
    echo
    echo -e "$FILE" >&2
    "$THIS/scripts/mlpp" -c polyml "$FILE" | \
    perl -p -e \
's/\bref\b/Unsynchronized.ref/g;'\
"`grep "^\(signature\|structure\|functor\)" $FILES | \
  sed "s/[^:]*:[a-z]* \([A-Za-z0-9_]*\).*/\1/" | \
  tr " " "\n" | \
  sort | \
  uniq | \
  sed 's/\(.*\)/s\/\\\\b\1\\\\b\/Metis_\1\/g;/'`"
  done

  cat <<EOF
;
print_depth 10;
EOF

) > metis.ML