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> system_constants
std::map<core::identifier_string, sort_expression_list> system_functions
data_specification type_checked_data_spec
std::map<core::identifier_string, sort_expression> user_constants
std::map<core::identifier_string, sort_expression_list> user_functions
bool 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.

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.
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 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_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
sort_expression UnwindType(const sort_expression &Type) const
variable UnwindType(const variable &v) const
atermpp::term_list<T> UnwindType(const atermpp::term_list<T> &l)
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