Commit 969a9ba8 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Implement a parser to extract PVS subtype expressions from variable types.

In order to support PVS style subtype expressions, the system has to be able
to parser such expressions.  To simplify the variable list parse, it simply
extracts the PVS expressions as a single token, unprocessed.  While requiring
more parsing work for the subtype expression, it avoids the necessity of
changing the parser in the future should a new subtype language be used.

As part of this change, the variable list parser's lexer became to complicated
to be expressed in Antlr's combined grammar format.  Thus split it out.
Everything works the same as before from an API point of view.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10852 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 98223593
Loading
Loading
Loading
Loading
+0 −21
Original line number Diff line number Diff line
grammar VariableParser;

varlist: var (',' var)*; //Build list of variables
var:    ID vartype;
vartype: ':' type_info
       | defaulttype;
defaulttype: ;
type_info: bool_type
         | real_type
         | fixed_type ;

bool_type: 'bool';

real_type: 'real';

fixed_type: 'fixedt(' NAT ',' NAT ')'
          | 'fixedt(' NAT ',' NAT ',' NAT ')';

ID: [a-zA-Z][a-zA-Z0-9]*; //Variable identifier.  Start with letter, then alpha numerical allowed.
NAT: [0-9]+;
WS : [ \t\r\n]+ -> skip ; // skip spaces, tabs, newlines
+1 −1
Original line number Diff line number Diff line
@@ -59,7 +59,7 @@ final public class VariableParser {
        return listener.m_variables;
    }
    
    private static class VariablesParserToVariables extends VariableParserBaseListener {
    private static class VariablesParserToVariables extends VariableParserParserBaseListener {
        private String currentName;
        private VariableType currentType;

+42 −0
Original line number Diff line number Diff line
lexer grammar VariableParserLexer;

tokens { ID }

fragment IDRule: [a-zA-Z][a-zA-Z0-9]*; //Variable identifier.  Start with letter, then alpha numerical allowed.

REGULAR_ID: IDRule -> type(ID), pushMode(VARIABLE_TYPE);

fragment WS : [ \t\r\n]+; // skip spaces, tabs, newlines
WS1: WS -> skip ;


mode PVS_EXPR_MODE;
PVS_EXPR: ~[\{\}]+ -> popMode;


mode VARIABLE_TYPE;
VAR_SEPARATOR: ',' -> popMode;
COLON: ':';
BOOL_TYPE: 'bool';
REAL_TYPE: 'real';
FIXEDT: 'fixedt' -> pushMode(FIXED_TYPE);

OPEN_SUBTYPE: '{' -> pushMode(ID_FETCH);
PVS_EXPR_BEGIN: '|' -> pushMode(PVS_EXPR_MODE);
CLOSE_SUBTYPE: '}';

WS2: WS -> skip;

mode FIXED_TYPE;
NAT_SEPARATOR: ',';
OPEN_BRACKET: '(';
CLOSE_BRACKET: ')' -> popMode;
NAT: [0-9]+;

WS3: WS -> skip;


mode ID_FETCH;
SUBTYPE_ID: IDRule -> type(ID), popMode;

WS4: WS -> skip;
+29 −0
Original line number Diff line number Diff line
parser grammar VariableParserParser;
options { tokenVocab=VariableParserLexer; }

varlist: var (VAR_SEPARATOR var)*; //Build list of variables
var:    ID vartype;
vartype: ':' type_info
       | defaulttype;

defaulttype: ;

type_info: simple_type_info
         | '{' subtype '}';

subtype: subtype_var '|' pvs_expr;
subtype_var:    ID subtype_vartype;
subtype_vartype: ':' simple_type_info
       | defaulttype;
pvs_expr: PVS_EXPR;

simple_type_info: bool_type
         | real_type
         | fixed_type ;

bool_type: BOOL_TYPE;

real_type: 'real';

fixed_type: 'fixedt' '(' NAT NAT_SEPARATOR NAT ')'
          | 'fixedt' '(' NAT NAT_SEPARATOR NAT NAT_SEPARATOR NAT ')';