Quelle make_tptp_parser Sprache: Isabelle

#!/usr/bin/env bash
#
# make_tptp_parser - Runs ML-Yacc to generate TPTP parser and makes it
#                    Isabelle-friendly.
#
# This code is based on that used in src/Tools/Metis to adapt Metis for
# use in Isabelle.

INTERMEDIATE_FILES="tptp.yacc.sig tptp.lex.sml tptp.yacc.sml"

echo "Cleaning"
rm -f tptp_lexyacc.ML
echo "Generating lexer and parser"
ml-lex tptp.lex && ml-yacc tptp.yacc
echo "Generating tptp_lexyacc.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 *)
(******************************************************************)

(*
  This file is produced from the parser generated by ML-Yacc from the
  source files tptp.lex and tptp.yacc.
*)
EOF

for FILE in $INTERMEDIATE_FILES
do
  perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \
          -e 's/Unsafe\.(.*)/\1/g;' \
          -e 's/\b(Char\.ord\()CharVector\.sub\b/\1String\.sub/g;' $FILE
done
) | expand -t8 > tptp_lexyacc.ML

rm -f $INTERMEDIATE_FILES tptp.yacc.desc

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.