1#!/usr/bin/env bash
2#
3# make_mlyacclib - Generates Isabelle-friendly version of ML-Yacc's library.
4#
5# This code is based on that used in src/Tools/Metis to adapt Metis for
6# use in Isabelle.
7
8MLYACCDIR=./ml-yacc
9MLYACCLIB_FILES="base.sig join.sml lrtable.sml stream.sml parser2.sml"
10
11echo "Cleaning"
12rm -f ml_yacc_lib.ML
13echo "Generating ml_yacc_lib.ML"
14(
15  cat <<EOF
16
17(******************************************************************)
18(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
19(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
20(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
21(******************************************************************)
22
23(*
24  This file is generated from the contents of ML-Yacc's lib directory.
25  ML-Yacc's COPYRIGHT-file contents follow:
26
27EOF
28  perl -pe 'print "  ";' ml-yacc/COPYRIGHT
29  echo "*)"
30
31for FILE in $MLYACCLIB_FILES
32do
33  echo
34  echo "(**** Original file: $FILE ****)"
35  echo
36  echo -e "  $FILE" >&2
37  perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \
38          -e 's/Unsafe\.(.*)/\1/g;' \
39          -e 's/\bconcat\b/String.concat/g;' \
40          -e 's/(?<!List\.)foldr\b/List.foldr/g;' \
41          -e 's/\bfoldl\b/List.foldl/g;' \
42          -e 's/val print = fn s => TextIO\.output\(TextIO\.stdOut,s\)$//g;' \
43          -e 's/\bprint\b/TextIO.print/g;' \
44          $MLYACCDIR/lib/$FILE
45  done
46
47  cat <<EOF
48;
49EOF
50
51) | expand -t8 > ml_yacc_lib.ML
52