#!/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.
unset CDPATH
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 Leslie-Hurd's kind permission. Extract from a September 13, 2010
email written by him:
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 *)
(******************************************************************)
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
;
EOF
) > metis.ML