Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: make_tptp_parser Sprache: Scala

Original von: 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.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.