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