mcrl2::data::data_type_checker

Include file:

#include "mcrl2/data/typecheck.h

class mcrl2::data::data_type_checker

Protected attributes

std::map<core::identifier_string, sort_expression_list> mcrl2::data::data_type_checker::system_constants

std::map<core::identifier_string, sort_expression_list> mcrl2::data::data_type_checker::system_functions

data_specification mcrl2::data::data_type_checker::type_checked_data_spec

std::map<core::identifier_string, sort_expression> mcrl2::data::data_type_checker::user_constants

std::map<core::identifier_string, sort_expression_list> mcrl2::data::data_type_checker::user_functions

bool mcrl2::data::data_type_checker::was_warning_upcasting

Public member functions

data_type_checker(const data_specification &data_spec)

make a data type checker. Throws a mcrl2::runtime_error exception if the data_specification is not well typed.

Parameters:

• data_spec A data specification that does not need to have been type checked.

Returns: A data expression where all untyped identifiers have been replace by typed ones.

const data_specification operator()() const

Yields a type checked data specification, provided typechecking was successful. If not successful an exception is thrown.

Returns: a data specification where all untyped identifiers have been replace by typed ones.

void operator()(const variable &v, const detail::variable_context &context) const

Type checks a variable. Throws an mcrl2::runtime_error exception if the variable is not well typed.

A variable is not well typed if its name clashes with the name of a declared function, when its sort does not exist, or when the variable is used in its context with a different sort.

Parameters:

• v A variables that is to be type checked.
• context Information about the context of the variable.

void operator()(const variable_list &l, const detail::variable_context &context) const

Type checks a variable list. Throws an mcrl2::runtime_error exception if the variables are not well typed.

A variable is not well typed if its name clashes with the name of a declared function, when its sort does not exist, or when a variable occurs in the context. Furthermore, variables cannot occur multiple times in a variable list.

Parameters:

• l A list of variables that must be type checked.
• context Information about the context of the variables in the list.

void operator()(data_equation_vector &eqns)

Yields a type checked equation list, and sets the types in the equations right. If not successful an exception is thrown.

Parameters:

• eqns The list of equations that is type checked and updated.

void print_context() const

assignment typecheck_assignment(const assignment &x, const detail::variable_context &variable_context)

assignment_list typecheck_assignment_list(const assignment_list &assignments, const detail::variable_context &variable_context)

data_expression typecheck_data_expression(const data_expression &x, const sort_expression &expected_sort, const detail::variable_context &variable_context)

const data_specification &typechecked_data_specification() const

Protected member functions

void add_constant(const data::function_symbol &f, const std::string &msg)

void add_function(const data::function_symbol &f, const std::string &msg, bool allow_double_decls = false)

void add_system_constant(const data::function_symbol &f)

void add_system_constants_and_functions(const std::vector<data::function_symbol> &v)

void add_system_function(const data::function_symbol &f)

std::pair<bool, sort_expression_list> AdjustNotInferredList(const sort_expression_list &PosTypeList, const atermpp::term_list<sort_expression_list> &TypeListList) const

sort_expression determine_allowed_type(const data_expression &d, const sort_expression &proposed_type) const

bool EqTypesA(const sort_expression &Type1, const sort_expression &Type2) const

bool EqTypesL(sort_expression_list Type1, sort_expression_list Type2) const

void ErrorMsgCannotCast(sort_expression CandidateType, data_expression_list Arguments, sort_expression_list ArgumentTypes, std::string previous_reason) const

sort_expression ExpandNumTypesDown(sort_expression Type) const

sort_expression ExpandNumTypesUp(sort_expression Type) const

sort_expression_list ExpandNumTypesUpL(const sort_expression_list &type_list) const

sort_expression_list GetNotInferredList(const atermpp::term_list<sort_expression_list> &TypeListList) const

void initialise_system_defined_functions(void)

sort_expression_list InsertType(const sort_expression_list &TypeList, const sort_expression &Type) const

bool InTypesA(const sort_expression &Type, sort_expression_list Types) const

bool InTypesL(const sort_expression_list &Type, atermpp::term_list<sort_expression_list> Types) const

bool IsNotInferredL(sort_expression_list TypeList) const

bool IsTypeAllowedA(const sort_expression &Type, const sort_expression &PosType) const

bool IsTypeAllowedL(const sort_expression_list &TypeList, const sort_expression_list &PosTypeList) const

bool match_fbag_cinsert(const function_sort &type, sort_expression &result) const

bool match_fset_insert(const function_sort &type, sort_expression &result) const

bool MatchBagConstructor(const function_sort &type, sort_expression &result) const

bool MatchBagOpBag2Set(const function_sort &type, sort_expression &result) const

bool MatchBagOpBagCount(const function_sort &type, sort_expression &result) const

bool MatchEqNeqComparison(const function_sort &type, sort_expression &result) const

bool MatchFalseFunction(const function_sort &type, sort_expression &result) const

bool MatchFuncUpdate(const function_sort &type, sort_expression &result) const

bool MatchIf(const function_sort &type, sort_expression &result) const

bool MatchListOpConcat(const function_sort &type, sort_expression &result) const

bool MatchListOpCons(const function_sort &type, sort_expression &result) const

bool MatchListOpEltAt(const function_sort &type, sort_expression &result) const

bool MatchListOpHead(const function_sort &type, sort_expression &result) const

bool MatchListOpSnoc(const function_sort &type, sort_expression &result) const

bool MatchListOpTail(const function_sort &type, sort_expression &result) const

bool MatchListSetBagOpIn(const function_sort &type, sort_expression &result) const

bool MatchSetBagOpUnionDiffIntersect(const function_sort &type, sort_expression &result) const

bool MatchSetConstructor(const function_sort &type, sort_expression &result) const

bool MatchSetOpSet2Bag(const function_sort &type, sort_expression &result) const

bool MatchSetOpSetCompl(const function_sort &type, sort_expression &result) const

bool MatchSqrt(const function_sort &type, sort_expression &result) const

bool MaximumType(const sort_expression &Type1, const sort_expression &Type2, sort_expression &result) const

data_expression operator()(const data_expression &data_expr, const detail::variable_context &context) const

Type check a data expression. Throws a mcrl2::runtime_error exception if the expression is not well typed.

Parameters:

• data_expr A data expression that has not been type checked.
• context The variable context in which this term must be typechecked.

Returns: a data expression where all untyped identifiers have been replace by typed ones.

void read_constructors_and_mappings(const function_symbol_vector &constructors, const function_symbol_vector &mappings, const function_symbol_vector &normalized_constructors)

void read_sort(const sort_expression &SortExpr)

bool strict_type_check(const data_expression &d) const

void TransformVarConsTypeData(data_specification &data_spec)

sort_expression TraverseVarConsTypeD(const detail::variable_context &DeclaredVars, data_expression &DataTerm, const sort_expression &PosType, const bool strictly_ambiguous = true, const bool warn_upcasting = false, const bool print_cast_error = true) const

sort_expression TraverseVarConsTypeDN(const detail::variable_context &DeclaredVars, data_expression &DataTerm, sort_expression PosType, const bool strictly_ambiguous = true, const std::size_t nFactPars = std::string::npos, const bool warn_upcasting = false, const bool print_cast_error = true) const

bool TypeMatchA(const sort_expression &Type_in, const sort_expression &PosType_in, sort_expression &result) const

bool TypeMatchL(const sort_expression_list &TypeList, const sort_expression_list &PosTypeList, sort_expression_list &result) const

bool UnArrowProd(const sort_expression_list &ArgTypes, sort_expression PosType, sort_expression &result) const

bool UnFBag(sort_expression PosType, sort_expression &result) const

bool UnFSet(sort_expression PosType, sort_expression &result) const

bool UnifyMinType(const sort_expression &Type1, const sort_expression &Type2, sort_expression &result) const

bool UnList(sort_expression PosType, sort_expression &result) const

atermpp::term_list<T> UnwindType(const atermpp::term_list<T> &l)

sort_expression UnwindType(const sort_expression &Type) const

variable UnwindType(const variable &v) const

data_expression upcast_numeric_type(const data_expression &x, const sort_expression &expected_sort, const detail::variable_context &variable_context)

sort_expression UpCastNumericType(sort_expression NeededType, sort_expression Type, data_expression &Par, const detail::variable_context &DeclaredVars, const bool strictly_ambiguous, bool warn_upcasting = false, const bool print_cast_error = false) const