mcrl2/data/parse.h

Include file:

#include "mcrl2/data/parse.h"

Parser for data specifications.

Functions

data_expression mcrl2::data::parse_data_expression(const std::string &text, const data_specification &data_spec = detail::default_specification(), bool type_check = true, bool translate_user_notation = true, bool normalize_sorts = true)

Parses and type checks a data expression.

See parsing a data expression from a string for details.

Parameters:

  • text The input text containing a data expression.
  • data_spec The data specification that is used for type checking.
  • type_check Indication whether the expression is expected to be type checked.
  • translate_user_notation Indication whether user notation such a numbers must be translated to internal format.
  • normalize_sorts Indication whether the sorts must be rewritten to normal form.
data_expression mcrl2::data::parse_data_expression(const std::string &text, const VariableContainer &variables, const data_specification &data_spec = detail::default_specification(), bool type_check = true, bool translate_user_notation = true, bool normalize_sorts = true)

Parses and type checks a data expression.

See parsing a data expression from a string for details.

Parameters:

  • text The input text containing a data expression.
  • variables A container with variables that can occur in the data expression.
  • data_spec The data specification that is used for type checking.
  • type_check Indication whether the expression is expected to be type checked.
  • translate_user_notation Indication whether user notation such a numbers must be translated to internal format.
  • normalize_sorts Indication whether the sorts must be rewritten to normal form.
data_expression mcrl2::data::parse_data_expression(std::istream &in, const VariableContainer &variables, const data_specification &dataspec = detail::default_specification(), bool type_check = true, bool translate_user_notation = true, bool normalize_sorts = true)

Parses and type checks a data expression.

A data expression is read from the input where it is assumed that it can contain variables from the range from begin to end. The data expression is type checked using the given data specification data_spec. The default data specification contains all standard sorts and functions. If a parse or type check error occurs this is reported using a mcrl2::runtime_error exception. It is assumed that the input contains exactly one expression, and nothing else.

Parameters:

  • in The input stream containing a data expression.
  • variables The variables that can occur in the data expression.
  • dataspec The data specification that is used for type checking.
  • type_check Indication whether the expression is expected to be type checked.
  • translate_user_notation Indication whether user notation such a numbers must be translated to internal format.
  • normalize_sorts Indication whether the sorts must be rewritten to normal form.

Returns: The parsed data expression.

data_expression mcrl2::data::parse_data_expression(std::istream &text, const data_specification &data_spec = detail::default_specification(), bool type_check = true, bool translate_user_notation = true, bool normalize_sorts = true)

Parses and type checks a data expression.

See parsing a data expression from a string for details.

Parameters:

  • text The input text containing a data expression.
  • data_spec The data specification that is used for type checking.
  • type_check Indication whether the expression is expected to be type checked.
  • translate_user_notation Indication whether user notation such a numbers must be translated to internal format.
  • normalize_sorts Indication whether the sorts must be rewritten to normal form.
data_specification mcrl2::data::parse_data_specification(const std::string &text)

Parses a and type checks a data specification.

This function reads a data specification in input string text. See for an example the function parse_data_expression on a string.

Parameters:

  • text A textual description of the data specification.

Returns: the data specification corresponding to the input istream.

data_specification mcrl2::data::parse_data_specification(std::istream &in)

Parses a and type checks a data specification.

This function reads a data specification in input string text. It is assumed that the string contains a single data specification, and nothing else. If a parse or type check error is detected an mcrl2::runtime_error exception is raised with a string that indicates the problem. A typical example of a specification is: sortD=structd1|d2;F=D->Set(D);Natural;conszero:Natural;plus:Natural->Natural;mapplus:Natural#Natural->Natural;varx,y:Natural;eqny==zero->plus(x,y)=x;plus(x,succ(y))=succ(plus(x,y));

Parameters:

  • in A input stream containing the data specification.

Returns: the data specification corresponding to text.

data::function_symbol mcrl2::data::parse_function_symbol(const std::string &text, const std::string &dataspec_text = "")
sort_expression mcrl2::data::parse_sort_expression(const std::string &text, const data_specification &data_spec = detail::default_specification())

Parses and type checks a sort expression.

Parses and type checks the sort expression. An error is signalled using the mcrl2::runtime_error exception. This routine expects exactly one sort expression on the input. The default data specification contains all standard sorts.

Parameters:

  • text The input text containing a sort expression.
  • data_spec The data specification that is used for type checking.
sort_expression mcrl2::data::parse_sort_expression(std::istream &in, const data_specification &data_spec = detail::default_specification())

Parses and type checks a sort expression.

See parsing a sort expression from a string for details.

Parameters:

  • in An input stream containing a sort expression.
  • data_spec The data specification that is used for type checking.
variable mcrl2::data::parse_variable(const std::string &text, const data_specification &data_spec = detail::default_specification())

Parses and type checks a data variable declaration.

See the information for reading a variable declaration from a string.

Parameters:

  • text A textual description of the variable declaration.
  • data_spec The data specification that is used for type checking.

Returns: the variable corresponding to the input istream.

variable mcrl2::data::parse_variable(std::istream &text, const data_specification &data_spec = detail::default_specification())

Parses and type checks a data variable declaration.

A variable declaration has the form x:S where x is a string and S is a sort expression. No trailing information after the declaration of the variable is allowed. The declaration is checked using the data specification that is provided. The default data specification contains all standard data types. If a parse or typecheck error occurs an mcrl2::runtime_error exception is raised.

Parameters:

  • text A textual description of the variable declaration.
  • data_spec The data specification that is used for type checking.

Returns: the variable corresponding to the string text.

variable_list mcrl2::data::parse_variable_declaration_list(const std::string &text, const data_specification &dataspec = detail::default_specification())

Parses a variable declaration list.

Parameters:

  • text The input text.
  • dataspec The data specification used to type normalize the sorts of the variables.

Returns: The parsed variable declaration list.

variable_list mcrl2::data::parse_variables(const std::string &text)
void mcrl2::data::parse_variables(const std::string &text, OutputIterator i, const data_specification &data_spec = detail::default_specification())

Parses and type checks a data variable declaration list.

See parse_variables on a string for more explanation.

Parameters:

  • text A textual description of the variable declarations to be parsed.
  • i An input interator indicating where the parsed variables must be inserted.
  • data_spec The data specification that is used for type checking.
void mcrl2::data::parse_variables(const std::string &text, OutputIterator i, VariableIterator begin, VariableIterator end, const data_specification &data_spec = detail::default_specification())

Parses and type checks a data variable declaration list checking for double occurrences of variables in an existing variable range.

See parse_variables on a string for more explanation.

Parameters:

  • text A textual description of the variable declarations to be parsed.
  • i An input interator indicating where the parsed variables must be inserted.
  • begin The start of a variable range against which the variables are checked for double occurrences.
  • end The end of the variable range against which the parsed variables are checked.
  • data_spec The data specification that is used for type checking.
void mcrl2::data::parse_variables(std::istream &in, OutputIterator o, VariableIterator begin, VariableIterator end, const data_specification &data_spec = detail::default_specification())

Parses and type checks a data variable declaration list checking for double occurrences of variables in an existing variable range.

The shape of the variables are x_11,…,x_1n:S_1; … x_m1,…,x_mk:S_m where x_ij are variable strings and S_i are sort expressions. It is checked that the sort expressions are properly typed regarding the data specification and that the variable names do not clash with the names of mappings and constructors. It is also not allowed to use a variable name twice. If an optional range of variables is given, then it is also checked that there are no conflicts with variable names in this range. An mcrl2::runtime_error exception is raised when an error occurs. In this case no names added using the input iterator. The default data specification contains all standard data types.

The output iterator can be used as follows, on standard variable lists. variable_listl;parse_variables(“x:Nat;y:Pos”,std::front_inserter(l));

Parameters:

  • in An input stream containing the variable declarations to be parsed.
  • o An output interator indicating where the parsed variables must be inserted.
  • begin The start of a variable range against which the variables are checked for double occurrences.
  • end The end of the variable range against which the parsed variables are checked.
  • data_spec The data specification that is used for type checking.
void mcrl2::data::parse_variables(std::istream &text, OutputIterator i, const data_specification &data_spec = detail::default_specification())

Parses and type checks a data variable declaration list.

See parse_variables on a string for more explanation.

Parameters:

  • text A textual description of the variable declarations to be parsed.
  • i An input interator indicating where the parsed variables must be inserted.
  • data_spec The data specification that is used for type checking.

Functions

static data_specification const &mcrl2::data::detail::default_specification()