mCRL2
Loading...
Searching...
No Matches
normalize_sorts.h
Go to the documentation of this file.
1// Author(s): Jan Friso Groote. Based on pbes/normalize_sorts by Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
9/// \file mcrl2/pres/normalize_sorts.h
10/// \brief add your file description here.
11
12#ifndef MCRL2_PRES_NORMALIZE_SORTS_H
13#define MCRL2_PRES_NORMALIZE_SORTS_H
14
15#include "mcrl2/data/normalize_sorts.h"
16#include "mcrl2/pres/builder.h"
17
18namespace mcrl2
19{
20
21namespace pres_system
22{
23
24template <typename T>
26 const data::sort_specification& sortspec,
27 typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
28 )
29{
30 core::make_update_apply_builder<pres_system::sort_expression_builder>(data::detail::normalize_sorts_function(sortspec)).update(x);
31}
32
33template <typename T>
34T normalize_sorts(const T& x,
35 const data::sort_specification& sortspec,
36 typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
37 )
38{
39 T result;
40 core::make_update_apply_builder<pres_system::sort_expression_builder>(data::detail::normalize_sorts_function(sortspec)).apply(result, x);
41 return result;
42}
43
44} // namespace pres_system
45
46} // namespace mcrl2
47
48#endif // MCRL2_PRES_NORMALIZE_SORTS_H
The interface for a class that reads aterm from a stream. The default constructed term aterm() indica...
Definition aterm_io.h:59
The interface for a class that writes aterm to a stream. Every written term is retrieved by the corre...
Definition aterm_io.h:48
A helper class to restore the state of the aterm_{i,o}stream objects upon destruction....
Definition aterm_io.h:84
aterm_stream_state(aterm_stream &stream)
Definition aterm_io.h:86
const function_symbol & function() const
Returns the function symbol belonging to an aterm.
Definition aterm.h:144
aterm & operator=(aterm &&other) noexcept=default
binary_aterm_istream(std::istream &is)
Provide the input stream from which terms are read.
binary_aterm_ostream(std::ostream &os)
Provide the output stream to which the terms are written.
bool operator==(const function_symbol &f) const
Equality test.
bool operator!=(const unprotected_aterm_core &t) const
Inequality operator on two unprotected aterms.
Definition aterm_core.h:92
void translate_user_notation()
Translate user notation within the equations of the data specification.
data_specification()
Default constructor. Generate a data specification that contains only booleans and positive numbers.
\brief A function symbol
function_symbol(const core::identifier_string &name, const sort_expression &sort)
Constructor.
const core::identifier_string & name() const
const sort_expression & sort() const
const core::identifier_string & name() const
\brief A data variable
Definition variable.h:28
const core::identifier_string & name() const
Definition variable.h:38
const sort_expression & sort() const
Definition variable.h:43
variable(const core::identifier_string &name, const sort_expression &sort)
Constructor.
Definition variable.h:62
logger(const log_level_t l)
Default constructor.
Definition logger.h:164
\brief A propositional variable declaration
const data::variable_list & parameters() const
const core::identifier_string & name() const
\brief The multiplication with a positive constant with the constant at the right.
const pres_expression & left() const
\brief The multiplication with a positive constant with the constant at the left.
const pres_expression & right() const
data::sort_expression_list propositional_variable_sorts(const core::identifier_string &name) const
bool is_declared(const core::identifier_string &name) const
std::map< core::identifier_string, pbes_system::propositional_variable > m_propositional_variables
void add_propositional_variables(const PropositionalVariableContainer &propositional_variables, const data::sort_type_checker &sort_typechecker)
\brief The infimum over a data type for pres expressions
const pres_expression & body() const
infimum(const data::variable_list &variables, const pres_expression &body)
\brief Constructor Z14.
const data::variable_list & variables() const
const propositional_variable & variable() const
Returns the pres variable of the equation.
pres_equation(const fixpoint_symbol &symbol, const propositional_variable &variable, const pres_expression &expr)
Constructor.
const pres_expression & formula() const
Returns the predicate formula on the right hand side of the equation.
const fixpoint_symbol & symbol() const
Returns the fixpoint symbol of the equation.
pres_expression & operator=(pres_expression &&) noexcept=default
void operator()(pres &presspec)
Typecheck the pres presspec.
Definition typecheck.h:268
pres_type_checker(const data::data_specification &dataspec=data::data_specification())
Default constructor.
Definition typecheck.h:254
pres_expression typecheck(const pres_expression &x, const data::variable_list &parameters)
Definition typecheck.h:324
data::data_type_checker m_data_type_checker
Definition typecheck.h:238
pres_expression operator()(const pres_expression &x)
Type check a process expression. Throws a mcrl2::runtime_error exception if the expression is not wel...
Definition typecheck.h:315
pres_type_checker(const data::data_specification &dataspec, const VariableContainer &global_variables, const PropositionalVariableContainer &propositional_variables)
Constructor.
Definition typecheck.h:260
std::vector< propositional_variable > equation_variables(const std::vector< pres_equation > &equations)
Definition typecheck.h:242
data::detail::variable_context m_variable_context
Definition typecheck.h:239
detail::pres_context m_pres_context
Definition typecheck.h:240
parameterized boolean equation system
Definition pres.h:59
propositional_variable_instantiation & initial_state()
Returns the initial state.
Definition pres.h:205
void set_data(const data::data_specification &d)
Allows to set the data specification of a pres.
Definition pres.h:159
const propositional_variable_instantiation & initial_state() const
Returns the initial state.
Definition pres.h:198
bool is_well_typed() const
Checks if the PRES is well typed.
Definition pres.h:273
\brief A propositional variable instantiation
propositional_variable_instantiation & operator=(const propositional_variable_instantiation &) noexcept=default
propositional_variable_instantiation(const core::identifier_string &name, const data::data_expression_list &parameters)
Constructor.
const data::data_expression_list & parameters() const
\brief The generic sum operator for pres expressions
const data::variable_list & variables() const
const pres_expression & body() const
\brief The supremeum over a data type for pres expressions
supremum(const data::variable_list &variables, const pres_expression &body)
\brief Constructor Z14.
const data::variable_list & variables() const
const pres_expression & body() const
Standard exception class for reporting runtime errors.
Definition exception.h:27
const std::string & shortname() const
bool operator==(const file_format &other) const
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
The main namespace for the aterm++ library.
Definition algorithm.h:21
aterm_istream & operator>>(aterm_istream &stream, aterm &term)
Read the given term from the stream, but for aterm_list we want to use a specific one that performs v...
Definition aterm_io.h:77
term_list< aterm > aterm_list
A term_list with elements of type aterm.
Definition aterm_list.h:497
aterm_istream & operator>>(aterm_istream &stream, aterm_transformer transformer)
Sets the given transformer to be applied to following reads.
Definition aterm_io.h:70
const atermpp::function_symbol & function_symbol_OpIdNoIndex()
std::string file_source(const std::string &filename)
Definition load_aterm.h:25
const atermpp::function_symbol & function_symbol_GlobVarSpec()
const atermpp::function_symbol & function_symbol_DataVarIdNoIndex()
const atermpp::function_symbol & function_symbol_PropVarInstNoIndex()
const atermpp::function_symbol & function_symbol_PRES()
const atermpp::function_symbol & function_symbol_PRInit()
const atermpp::function_symbol & function_symbol_OpId()
std::string pp(const core::identifier_string &x)
Definition core.cpp:26
atermpp::aterm_string identifier_string
String type of the LPS library. Identifier strings are represented internally as ATerms.
void check_duplicate_variable_names(const data::variable_list &x, const std::string &msg)
atermpp::aterm data_specification_to_aterm(const data_specification &s)
Definition data_io.cpp:44
Namespace for all data library functionality.
Definition data.cpp:22
std::string pp(const data::untyped_data_parameter &x)
Definition data.cpp:73
atermpp::term_list< sort_expression > sort_expression_list
\brief list of sort_expressions
atermpp::aterm_istream & operator>>(atermpp::aterm_istream &stream, data_specification &spec)
Reads a data specification from a stream.
Definition data_io.cpp:66
atermpp::term_list< variable > variable_list
\brief list of variables
@ verbose
Definition logger.h:37
The main namespace for the PBES library.
void save_pres(const pres &presspec, const std::string &filename)
Saves an PRES to filename, or to stdout if filename equals "".
Definition io.cpp:298
void complete_pres(pres &x)
Definition pres.cpp:147
untyped_pres parse_pres_new(const std::string &text)
Definition pres.cpp:136
typecheck_builder make_typecheck_builder(data::data_type_checker &data_typechecker, const data::detail::variable_context &variables, const detail::pres_context &propositional_variables)
Definition typecheck.h:224
pres load_pres(const std::string &filename)
Loads a PRES from filename, or from stdin if filename equals "".
Definition io.cpp:283
propositional_variable parse_propositional_variable(const std::string &text)
Definition pres.cpp:154
pres_expression parse_pres_expression_new(const std::string &text)
Definition pres.cpp:125
pres_expression parse_pres_expression(const std::string &text)
Definition pres.cpp:163
The main namespace for the PRES library.
std::string pp(const pres_system::supremum &x)
Definition pres.cpp:37
std::string pp(const pres_system::const_multiply &x)
Definition pres.cpp:43
void load_pres(pres &pres, std::istream &stream, utilities::file_format format, const std::string &)
Load a PRES from file.
Definition io.cpp:73
void typecheck_pres(pres &presspec)
Type check a parsed mCRL2 pres specification. Throws an exception if something went wrong.
Definition typecheck.h:341
const utilities::file_format guess_format(const std::string &filename)
Definition io.h:45
propositional_variable parse_propositional_variable(const std::string &text, const VariableContainer &variables, const data::data_specification &dataspec=data::data_specification())
Definition parse.h:66
std::string pp(const pres_system::pres_expression &x)
Definition pres.cpp:47
atermpp::aterm_istream & operator>>(atermpp::aterm_istream &stream, pres_equation &equation)
Definition io.cpp:205
std::string pp(const pres_system::infimum &x)
Definition pres.cpp:39
static atermpp::aterm remove_index_impl(const atermpp::aterm &x)
Definition io.cpp:165
const utilities::file_format & pres_format_internal()
Definition io.h:40
std::istream & operator>>(std::istream &from, pres &result)
Reads a PRES from an input stream.
Definition parse.h:52
void save_pres(const pres &pres, std::ostream &stream, utilities::file_format format)
Save a PRES in the format specified.
Definition io.cpp:43
pres_expression typecheck_pres_expression(pres_expression &x, const VariableContainer &variables, const PropositionalVariableContainer &propositional_variables, const data::data_specification &dataspec=data::data_specification())
Type check a parsed mCRL2 pres expression. Throws an exception if something went wrong.
Definition typecheck.h:394
const utilities::file_format & pres_format_text()
Definition io.h:42
std::string pp(const pres_system::const_multiply_alt &x)
Definition pres.cpp:44
void load_pres(pres &pres, const std::string &filename, utilities::file_format format)
Load pres from file.
Definition io.cpp:139
atermpp::aterm pres_marker()
Definition io.cpp:220
T normalize_sorts(const T &x, const data::sort_specification &sortspec, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
std::string pp(const pres_system::sum &x)
Definition pres.cpp:40
void save_pres(const pres &pres, const std::string &filename, utilities::file_format format, bool welltypedness_check)
save_pres Saves a PRES to a file.
Definition io.cpp:104
const std::vector< utilities::file_format > & pres_file_formats()
Definition io.cpp:24
pres_expression parse_pres_expression(const std::string &text, const pres &presspec, const VariableContainer &variables, bool type_check=true, bool translate_user_notation=true, bool normalize_sorts=true)
Parse a pres expression. Throws an exception if something went wrong.
Definition parse.h:119
pres_expression parse_pres_expression(const std::string &text, const data::data_specification &dataspec, const VariableContainer &variables, const PropositionalVariableContainer &propositional_variables, bool type_check=true, bool translate_user_notation=true, bool normalize_sorts=true)
Parse a pres expression. Throws an exception if something went wrong.
Definition parse.h:85
void normalize_sorts(T &x, const data::sort_specification &sortspec, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
atermpp::aterm_istream & operator>>(atermpp::aterm_istream &stream, pres &pres)
Reads a pres from a stream.
Definition io.cpp:238
pres_system::pres_expression translate_user_notation(const pres_system::pres_expression &x)
Definition pres.cpp:54
pres parse_pres(std::istream &in)
Definition parse.h:39
atermpp::aterm pres_to_aterm(const pres &p)
Conversion to atermappl.
Definition io.cpp:319
propositional_variable typecheck_propositional_variable(const propositional_variable &x, const VariableContainer &variables, const data::data_specification &dataspec=data::data_specification())
Type check a parsed mCRL2 propositional variable. Throws an exception if something went wrong.
Definition typecheck.h:362
bool is_pres_file_format(const utilities::file_format &format)
Definition io.h:27
std::string pp(const pres_system::pres &x)
Definition pres.cpp:45
std::string pp(const pres_system::propositional_variable_instantiation &x)
Definition pres.cpp:49
static atermpp::aterm add_index_impl(const atermpp::aterm &x)
Definition io.cpp:177
void complete_data_specification(pres &)
Adds all sorts that appear in the PRES p to the data specification of p.
Definition pres.h:320
std::string pp(const pres_system::propositional_variable &x)
Definition pres.cpp:48
pres parse_pres(const std::string &text)
Definition parse.h:59
std::string read_text(std::istream &in)
Read text from a stream.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
normalize_sorts_function(const sort_specification &sort_spec)
void apply(T &result, const infimum &x)
Definition typecheck.h:67
void apply(T &result, const sum &x)
Definition typecheck.h:105
void apply(T &result, const data::untyped_data_parameter &x)
Definition typecheck.h:189
typecheck_builder(data::data_type_checker &data_typechecker, const data::detail::variable_context &variables, const detail::pres_context &pres_context)
Definition typecheck.h:37
pres_expression_builder< typecheck_builder > super
Definition typecheck.h:30
void apply(T &result, const const_multiply &x)
Definition typecheck.h:124
void apply(T &result, const const_multiply_alt &x)
Definition typecheck.h:139
void apply(T &result, const propositional_variable_instantiation &x)
Definition typecheck.h:155
data::detail::variable_context m_variable_context
Definition typecheck.h:34
void apply(T &result, const data::data_expression &x)
Definition typecheck.h:47
const detail::pres_context & m_pres_context
Definition typecheck.h:35
void apply(T &result, const supremum &x)
Definition typecheck.h:86
data::data_type_checker & m_data_type_checker
Definition typecheck.h:33
std::size_t operator()(const atermpp::detail::reference_aterm< T > &t) const