1#!/usr/bin/env bash 2# 3# make_tptp_parser - Runs ML-Yacc to generate TPTP parser and makes it 4# Isabelle-friendly. 5# 6# This code is based on that used in src/Tools/Metis to adapt Metis for 7# use in Isabelle. 8 9INTERMEDIATE_FILES="tptp.yacc.sig tptp.lex.sml tptp.yacc.sml" 10 11echo "Cleaning" 12rm -f tptp_lexyacc.ML 13echo "Generating lexer and parser" 14ml-lex tptp.lex && ml-yacc tptp.yacc 15echo "Generating tptp_lexyacc.ML" 16( 17 cat <<EOF 18 19(******************************************************************) 20(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) 21(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) 22(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *) 23(******************************************************************) 24 25(* 26 This file is produced from the parser generated by ML-Yacc from the 27 source files tptp.lex and tptp.yacc. 28*) 29EOF 30 31for FILE in $INTERMEDIATE_FILES 32do 33 perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \ 34 -e 's/Unsafe\.(.*)/\1/g;' \ 35 -e 's/\b(Char\.ord\()CharVector\.sub\b/\1String\.sub/g;' $FILE 36done 37) | expand -t8 > tptp_lexyacc.ML 38 39rm -f $INTERMEDIATE_FILES tptp.yacc.desc 40