src/HOL/TPTP/TPTP_Parser/tptp.lex
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47358 26c4e431ef05
child 47689 f5c05e51668f
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     1
(*  Title:      HOL/TPTP/TPTP_Parser/tptp.lex
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     2
    Author:     Nik Sultana, Cambridge University Computer Laboratory
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     3
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     4
 Notes:
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     5
 * Omit %full in definitions to restrict alphabet to ascii.
47358
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
     6
 * Could include %posarg to ensure that we'd start counting character positions
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
     7
   from 0, but it would punish performance.
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     8
 * %s AF F COMMENT; -- could improve by making stateful.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     9
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    10
 Acknowledgements:
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    11
 * Geoff Sutcliffe for help with TPTP.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    12
 * Timothy Bourke for his tips on getting ML-Yacc working with Poly/ML.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    13
 * An early version of this was ported from the specification shipped with
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    14
   Leo-II, written by Frank Theiss.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    15
 * Some boilerplate bits were taken from the ml-yacc/ml-lex manual by Roger Price.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    16
 * Jasmin Blanchette and Makarius Wenzel for help with Isabelle integration.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    17
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    18
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    19
structure T = Tokens
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    20
type pos = int             (* Position in file *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    21
type lineNo = int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    22
type svalue = T.svalue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    23
type ('a,'b) token = ('a,'b) T.token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    24
type lexresult = (svalue,pos) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    25
type lexarg = string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    26
type arg = lexarg
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    27
val col = ref 0;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    28
val linep = ref 1;         (* Line pointer *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    29
val eolpos = ref 0;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    30
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    31
val badCh : string * string * int * int -> unit = fn
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    32
    (file_name, bad, line, col) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    33
    TextIO.output(TextIO.stdOut, file_name ^ "["
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    34
          ^ Int.toString line ^ "." ^ Int.toString col
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    35
          ^ "] Invalid character \"" ^ bad ^ "\"\n");
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    36
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    37
val eof = fn file_name =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    38
  let
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    39
    val result = T.EOF (!linep,!col);
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    40
    val _ = linep := 0;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    41
  in result end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    42
(*here could check whether file ended prematurely:
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    43
 see if have open brackets, or if we're in some state other than INITIAL*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    44
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    45
val count_commentlines : string -> unit = fn str =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    46
  let
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    47
    val str' = String.explode str
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    48
    val newlines = List.filter (fn x => x = #"\n") str'
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    49
  in linep := (!linep) + (List.length newlines) end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    50
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    51
%%
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    52
%header (functor TPTPLexFun(structure Tokens: TPTP_TOKENS));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    53
%arg (file_name:string);
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    54
47358
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    55
percentage_sign           = "%";
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    56
double_quote              = ["];
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    57
do_char                   = ([^"]|[\\]["\\]);
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    58
single_quote              = ['];
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    59
sq_char                   = ([\040-\041\043-\126]|[\\]['\\]);
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    60
sign                      = [+-];
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    61
dot                       = [.];
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    62
exponent                  = [Ee];
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    63
slash                     = [/];
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    64
zero_numeric              = [0];
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    65
non_zero_numeric          = [1-9];
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    66
numeric                   = [0-9];
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    67
lower_alpha               = [a-z];
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    68
upper_alpha               = [A-Z];
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    69
alpha_numeric             = ({lower_alpha}|{upper_alpha}|{numeric}|_);
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    70
dollar                    = \$;
47358
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    71
printable_char            = .;
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    72
viewable_char             = [.\n];
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    73
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    74
dot_decimal               = {dot}{numeric}+;
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    75
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    76
ddollar                   = \$\$;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    77
unsigned_integer          = {numeric}+;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    78
divide                    = [/];
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    79
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    80
signed_integer            = {sign}{unsigned_integer};
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    81
exp_suffix                = {exponent}({signed_integer}|{unsigned_integer});
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    82
real                      = ({signed_integer}|{unsigned_integer}){dot_decimal}{exp_suffix}?;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    83
rational                  = ({signed_integer}|{unsigned_integer}){divide}{unsigned_integer};
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    84
47358
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    85
lower_word                = {lower_alpha}{alpha_numeric}*;
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    86
upper_word                = {upper_alpha}{alpha_numeric}*;
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    87
dollar_dollar_word        = {ddollar}{lower_word};
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    88
dollar_word               = {dollar}{lower_word};
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    89
47358
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    90
distinct_object           = {double_quote}{do_char}+{double_quote};
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    91
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    92
ws                        = ([\ ]|[\t]);
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    93
single_quoted             = {single_quote}({alpha_numeric}|{sq_char}|{ws})+{single_quote};
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    94
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    95
system_comment_one        = [%][\ ]*{ddollar}[_]*;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    96
system_comment_multi      = [/][\*][\ ]*(ddollar)([^\*]*[\*][\*]*[^/\*])*[^\*]*[\*][\*]*[/];
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    97
system_comment            = (system_comment_one)|(system_comment_multi);
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    98
47358
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
    99
comment_line              = {percentage_sign}[^\n]*;
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   100
comment_block             = [/][\*]([^\*]*[\*]+[^/\*])*[^\*]*[\*]+[/];
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   101
comment                   = ({comment_line}|{comment_block})+;
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   102
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   103
eol                       = ("\013\010"|"\010"|"\013");
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   104
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   105
%%
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   106
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   107
{ws}*           => (col:=(!col)+size yytext; continue () );
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   108
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   109
{eol}           => (linep:=(!linep)+1;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   110
                   eolpos:=yypos+size yytext; continue ());
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   111
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   112
"&"             => (col:=yypos-(!eolpos); T.AMPERSAND(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   113
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   114
"@+"            => (col:=yypos-(!eolpos); T.INDEF_CHOICE(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   115
"@-"            => (col:=yypos-(!eolpos); T.DEFIN_CHOICE(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   116
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   117
"!!"            => (col:=yypos-(!eolpos); T.OPERATOR_FORALL(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   118
"??"            => (col:=yypos-(!eolpos); T.OPERATOR_EXISTS(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   119
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   120
"@"             => (col:=yypos-(!eolpos); T.AT_SIGN(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   121
"^"             => (col:=yypos-(!eolpos); T.CARET(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   122
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   123
":"             => (col:=yypos-(!eolpos); T.COLON(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   124
","             => (col:=yypos-(!eolpos); T.COMMA(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   125
"="             => (col:=yypos-(!eolpos); T.EQUALS(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   126
"!"             => (col:=yypos-(!eolpos); T.EXCLAMATION(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   127
":="            => (col:=yypos-(!eolpos); T.LET(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   128
">"             => (col:=yypos-(!eolpos); T.ARROW(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   129
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   130
"<="            => (col:=yypos-(!eolpos); T.FI(!linep,!col));
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   131
"<=>"           => (col:=yypos-(!eolpos); T.IFF(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   132
"=>"            => (col:=yypos-(!eolpos); T.IMPLIES(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   133
"["             => (col:=yypos-(!eolpos); T.LBRKT(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   134
"("             => (col:=yypos-(!eolpos); T.LPAREN(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   135
"->"            => (col:=yypos-(!eolpos); T.MAP_TO(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   136
"--"            => (col:=yypos-(!eolpos); T.MMINUS(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   137
"~&"            => (col:=yypos-(!eolpos); T.NAND(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   138
"!="            => (col:=yypos-(!eolpos); T.NEQUALS(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   139
"<~>"           => (col:=yypos-(!eolpos); T.XOR(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   140
"~|"            => (col:=yypos-(!eolpos); T.NOR(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   141
"."             => (col:=yypos-(!eolpos); T.PERIOD(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   142
"++"            => (col:=yypos-(!eolpos); T.PPLUS(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   143
"?"             => (col:=yypos-(!eolpos); T.QUESTION(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   144
"]"             => (col:=yypos-(!eolpos); T.RBRKT(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   145
")"             => (col:=yypos-(!eolpos); T.RPAREN(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   146
"~"             => (col:=yypos-(!eolpos); T.TILDE(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   147
"|"             => (col:=yypos-(!eolpos); T.VLINE(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   148
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   149
{distinct_object}    => (col:=yypos-(!eolpos); T.DISTINCT_OBJECT(yytext,!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   150
{rational}           => (col:=yypos-(!eolpos); T.RATIONAL(yytext,!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   151
{real}               => (col:=yypos-(!eolpos); T.REAL(yytext,!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   152
{signed_integer}     => (col:=yypos-(!eolpos); T.SIGNED_INTEGER(yytext,!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   153
{unsigned_integer}   => (col:=yypos-(!eolpos); T.UNSIGNED_INTEGER(yytext,!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   154
{dot_decimal}        => (col:=yypos-(!eolpos); T.DOT_DECIMAL(yytext,!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   155
{single_quoted}      => (col:=yypos-(!eolpos); T.SINGLE_QUOTED(yytext,!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   156
{upper_word}         => (col:=yypos-(!eolpos); T.UPPER_WORD(yytext,!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   157
{comment}            => (col:=yypos-(!eolpos); count_commentlines yytext;T.COMMENT(yytext,!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   158
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   159
"thf"          => (col:=yypos-(!eolpos); T.THF(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   160
"fof"          => (col:=yypos-(!eolpos); T.FOF(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   161
"cnf"          => (col:=yypos-(!eolpos); T.CNF(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   162
"tff"          => (col:=yypos-(!eolpos); T.TFF(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   163
"include"      => (col:=yypos-(!eolpos); T.INCLUDE(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   164
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   165
"$thf"          => (col:=yypos-(!eolpos); T.DTHF(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   166
"$fof"          => (col:=yypos-(!eolpos); T.DFOF(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   167
"$cnf"          => (col:=yypos-(!eolpos); T.DCNF(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   168
"$fot"          => (col:=yypos-(!eolpos); T.DFOT(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   169
"$tff"          => (col:=yypos-(!eolpos); T.DTFF(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   170
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   171
"$ite_f"        => (col:=yypos-(!eolpos); T.ITE_F(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   172
"$ite_t"        => (col:=yypos-(!eolpos); T.ITE_T(!linep,!col));
47357
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   173
"$let_tf"        => (col:=yypos-(!eolpos); T.LET_TF(!linep,!col));
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   174
"$let_ff"        => (col:=yypos-(!eolpos); T.LET_FF(!linep,!col));
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   175
"$let_ft"        => (col:=yypos-(!eolpos); T.LET_FT(!linep,!col));
15e579392a68 refactored tptp yacc to bring close to official spec;
sultana
parents: 46844
diff changeset
   176
"$let_tt"        => (col:=yypos-(!eolpos); T.LET_TT(!linep,!col));
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   177
47358
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   178
{lower_word}   => (col:=yypos-(!eolpos); T.LOWER_WORD(yytext,!linep,!col));
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   179
{dollar_word}  => (col:=yypos-(!eolpos); T.DOLLAR_WORD(yytext,!linep,!col));
26c4e431ef05 refactored tptp lex;
sultana
parents: 47357
diff changeset
   180
{dollar_dollar_word}  => (col:=yypos-(!eolpos); T.DOLLAR_DOLLAR_WORD(yytext,!linep,!col));
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   181
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   182
"+"           => (col:=yypos-(!eolpos); T.PLUS(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   183
"*"           => (col:=yypos-(!eolpos); T.TIMES(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   184
"-->"         => (col:=yypos-(!eolpos); T.GENTZEN_ARROW(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   185
"<<"          => (col:=yypos-(!eolpos); T.SUBTYPE(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   186
"!>"          => (col:=yypos-(!eolpos); T.DEP_PROD(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   187
"?*"          => (col:=yypos-(!eolpos); T.DEP_SUM(!linep,!col));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   188
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   189
":-"          => (col:=yypos-(!eolpos); T.LET_TERM(!linep,!col));