src/Tools/Metis/make_metis

tuning

#!/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
(*
   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 $(cat "$THIS/FILES")
  do
    echo
    echo "(**** Original file: $FILE ****)"
    echo
    echo -e "$FILE" >&2
    "$THIS/scripts/mlpp" -c polyml "src/$FILE" | \
    perl -p -e \
's/type name$/type name = string/;'\
's/\bref\b/Unsynchronized.ref/g;'\
's/\bPolyML.pointerEq\b/pointer_eq/g;'\
's/(?<!\.)\bexplode\b/String.explode/g;'\
's/(?<!\.)\bimplode\b/String.implode/g;'\
's/(?<!\.)\bprint\b/TextIO.print/g;'\
's/\bRL\b/Metis_RL/g;'\
"`grep "^\(signature\|structure\|functor\)" src/*.{sig,sml} | \
  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