#!/usr/bin/env bash

#

# make_mlyacclib - Generates Isabelle-friendly version of ML-Yacc's library.

#

# This code is based on that used in src/Tools/Metis to adapt Metis for

# use in Isabelle.

MLYACCDIR=./ml-yacc

MLYACCLIB_FILES="base.sig join.sml lrtable.sml stream.sml parser2.sml"

echo "Cleaning"

rm -f ml_yacc_lib.ML

echo "Generating ml_yacc_lib.ML"

(

  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;

(*

  This file is generated from the contents of ML-Yacc's lib directory.

  ML-Yacc's COPYRIGHT-file contents follow:

EOF

  perl -pe 'print "  ";' ml-yacc/COPYRIGHT

  echo "*)"

for FILE in $MLYACCLIB_FILES

do

  echo

  echo "(**** Original file: $FILE ****)"

  echo

  echo -e "  $FILE" >&2

  perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \

          -e 's/Unsafe\.(.*)/\1/g;' \

          -e 's/\bconcat\b/String.concat/g;' \

          -e 's/(?<!List\.)foldr\b/List.foldr/g;' \

          -e 's/\bfoldl\b/List.foldl/g;' \

          -e 's/val print = fn s => TextIO\.output\(TextIO\.stdOut,s\)$//g;' \

          -e 's/\bprint\b/TextIO.print/g;' \

          $MLYACCDIR/lib/$FILE

  done

  cat <<EOF

;

print_depth 10;

EOF

) > ml_yacc_lib.ML