#include <typecheck.h>

Inheritance diagram for mcrl2::data::data_type_checker:

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.

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.

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.

const data_specification	operator() () const
	Yields a type checked data specification, provided typechecking was successful. If not successful an exception is thrown.

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.

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

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)

const data_specification &	typechecked_data_specification () const

void	print_context () const

Public Member Functions inherited from mcrl2::data::sort_type_checker
	sort_type_checker (const sort_specification &sort_spec, bool must_check_aliases=true)
	constructs a sort expression checker.

const sort_specification &	get_sort_specification () const

void	operator() (const sort_expression &x) const
	Type check a sort expression. Throws an exception if the expression is not well typed.

Protected Member Functions
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.

void	read_sort (const sort_expression &SortExpr)

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

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

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

void	initialise_system_defined_functions (void)

void	add_system_constant (const data::function_symbol &f)

void	add_system_function (const data::function_symbol &f)

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

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

sort_expression	UnwindType (const sort_expression &Type) const

variable	UnwindType (const variable &v) const

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

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	InTypesA (const sort_expression &Type, sort_expression_list Types) const

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

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

bool	EqTypesL (sort_expression_list Type1, sort_expression_list Type2) const

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

sort_expression	ExpandNumTypesUp (sort_expression Type) const

sort_expression_list	ExpandNumTypesUpL (const sort_expression_list &type_list) const

sort_expression	ExpandNumTypesDown (sort_expression Type) const

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

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

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

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

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

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

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

bool	MatchListOpConcat (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	MatchListOpTail (const function_sort &type, sort_expression &result) const

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

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

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

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

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

bool	UnifyElementSort (sort_expression &Arg1, sort_expression &Arg2, sort_expression &result) const

bool	MatchSetBagOpUnionDiffIntersect (const core::identifier_string &data_term_name, const function_sort &type, sort_expression &result) const

bool	MatchSetOpSetCompl (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	MatchFuncUpdate (const function_sort &type, sort_expression &result) const

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

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

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

bool	UnFSet (sort_expression PosType, sort_expression &result) const

bool	UnFBag (sort_expression PosType, sort_expression &result) const

bool	UnList (sort_expression PosType, sort_expression &result) const

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

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

void	TransformVarConsTypeData (data_specification &data_spec)

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

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

std::pair< bool, sort_expression_list >	AdjustNotInferredList (const sort_expression_list &PosTypeList, const atermpp::term_list< sort_expression_list > &TypeListList) 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	IsNotInferredL (sort_expression_list TypeList) const

bool	strict_type_check (const data_expression &d) const

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

Protected Member Functions inherited from mcrl2::data::sort_type_checker
void	check_alias_circularity (const data::basic_sort &lhs, const data::sort_expression &rhs, std::set< basic_sort > sort_already_seen, const std::map< basic_sort, sort_expression > &alias_map)

void	check_sorts ()

void	check_aliases ()

void	check_for_sort_alias_loop_through_function_sort (const basic_sort &end_search, const sort_expression &start_search, std::set< basic_sort > &visited, const bool observed_a_sort_constructor, const std::map< basic_sort, sort_expression > &alias_map)

void	check_basic_sort_is_declared (const basic_sort &x) const

void	check_sort_list_is_declared (const sort_expression_list &SortExprList) const

void	check_sort_is_declared (const sort_expression &x) const

void	check_for_empty_constructor_domains (const function_symbol_vector &constructors)

Protected Attributes
bool	was_warning_upcasting

std::map< core::identifier_string, sort_expression_list >	system_constants

std::map< core::identifier_string, sort_expression_list >	system_functions

std::map< core::identifier_string, sort_expression >	user_constants

std::map< core::identifier_string, sort_expression_list >	user_functions

data_specification	type_checked_data_spec

Protected Attributes inherited from mcrl2::data::sort_type_checker
sort_specification	m_sort_specification

Detailed Description

Definition at line 26 of file typecheck.h.

Constructor & Destructor Documentation

◆ data_type_checker()

mcrl2::data::data_type_checker::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

[in] 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.

Definition at line 4297 of file typecheck.cpp.

Member Function Documentation

◆ add_constant()

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

protected

Definition at line 3615 of file typecheck.cpp.

◆ add_function()

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

protected

Definition at line 4029 of file typecheck.cpp.

◆ add_system_constant()

void mcrl2::data::data_type_checker::add_system_constant ( const data::function_symbol & f )

protected

Definition at line 3858 of file typecheck.cpp.

◆ add_system_constants_and_functions()

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

protected

Definition at line 3895 of file typecheck.cpp.

◆ add_system_function()

void mcrl2::data::data_type_checker::add_system_function ( const data::function_symbol & f )

protected

Definition at line 3876 of file typecheck.cpp.

◆ AdjustNotInferredList()

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

protected

Definition at line 4207 of file typecheck.cpp.

◆ determine_allowed_type()

sort_expression mcrl2::data::data_type_checker::determine_allowed_type	(	const data_expression &	d,
		const sort_expression &	proposed_type
	)		const

protected

Definition at line 2063 of file typecheck.cpp.

◆ EqTypesA()

bool mcrl2::data::data_type_checker::EqTypesA	(	const sort_expression &	Type1,
		const sort_expression &	Type2
	)		const

protected

Definition at line 2019 of file typecheck.cpp.

◆ EqTypesL()

bool mcrl2::data::data_type_checker::EqTypesL	(	sort_expression_list	Type1,
		sort_expression_list	Type2
	)		const

protected

Definition at line 2041 of file typecheck.cpp.

◆ ErrorMsgCannotCast()

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

protected

◆ ExpandNumTypesDown()

sort_expression mcrl2::data::data_type_checker::ExpandNumTypesDown ( sort_expression Type ) const

protected

Definition at line 1933 of file typecheck.cpp.

◆ ExpandNumTypesUp()

sort_expression mcrl2::data::data_type_checker::ExpandNumTypesUp ( sort_expression Type ) const

protected

Definition at line 1846 of file typecheck.cpp.

◆ ExpandNumTypesUpL()

sort_expression_list mcrl2::data::data_type_checker::ExpandNumTypesUpL ( const sort_expression_list & type_list ) const

protected

Definition at line 1836 of file typecheck.cpp.

◆ GetNotInferredList()

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

protected

Definition at line 4255 of file typecheck.cpp.

◆ initialise_system_defined_functions()

void mcrl2::data::data_type_checker::initialise_system_defined_functions ( void )

protected

Definition at line 3910 of file typecheck.cpp.

◆ InsertType()

sort_expression_list mcrl2::data::data_type_checker::InsertType	(	const sort_expression_list &	TypeList,
		const sort_expression &	Type
	)		const

protected

Definition at line 4147 of file typecheck.cpp.

◆ InTypesA()

bool mcrl2::data::data_type_checker::InTypesA	(	const sort_expression &	Type,
		sort_expression_list	Types
	)		const

protected

Definition at line 2007 of file typecheck.cpp.

◆ InTypesL()

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

protected

Definition at line 2029 of file typecheck.cpp.

◆ IsNotInferredL()

bool mcrl2::data::data_type_checker::IsNotInferredL ( sort_expression_list TypeList ) const

protected

Definition at line 4193 of file typecheck.cpp.

◆ IsTypeAllowedA()

bool mcrl2::data::data_type_checker::IsTypeAllowedA	(	const sort_expression &	Type,
		const sort_expression &	PosType
	)		const

protected

Definition at line 4164 of file typecheck.cpp.

◆ IsTypeAllowedL()

bool mcrl2::data::data_type_checker::IsTypeAllowedL	(	const sort_expression_list &	TypeList,
		const sort_expression_list &	PosTypeList
	)		const

protected

Definition at line 4180 of file typecheck.cpp.

◆ match_fbag_cinsert()

bool mcrl2::data::data_type_checker::match_fbag_cinsert	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 1337 of file typecheck.cpp.

◆ match_fset_insert()

bool mcrl2::data::data_type_checker::match_fset_insert	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 1305 of file typecheck.cpp.

◆ MatchBagConstructor()

bool mcrl2::data::data_type_checker::MatchBagConstructor	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 1192 of file typecheck.cpp.

◆ MatchBagOpBag2Set()

bool mcrl2::data::data_type_checker::MatchBagOpBag2Set	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 1595 of file typecheck.cpp.

◆ MatchBagOpBagCount()

bool mcrl2::data::data_type_checker::MatchBagOpBagCount	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 1640 of file typecheck.cpp.

◆ MatchEqNeqComparison()

bool mcrl2::data::data_type_checker::MatchEqNeqComparison	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 744 of file typecheck.cpp.

◆ MatchFalseFunction()

bool mcrl2::data::data_type_checker::MatchFalseFunction	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 1180 of file typecheck.cpp.

◆ MatchFuncUpdate()

bool mcrl2::data::data_type_checker::MatchFuncUpdate	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 1685 of file typecheck.cpp.

◆ MatchIf()

bool mcrl2::data::data_type_checker::MatchIf	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 717 of file typecheck.cpp.

◆ MatchListOpConcat()

bool mcrl2::data::data_type_checker::MatchListOpConcat	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 886 of file typecheck.cpp.

◆ MatchListOpCons()

bool mcrl2::data::data_type_checker::MatchListOpCons	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 789 of file typecheck.cpp.

◆ MatchListOpEltAt()

bool mcrl2::data::data_type_checker::MatchListOpEltAt	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 947 of file typecheck.cpp.

◆ MatchListOpHead()

bool mcrl2::data::data_type_checker::MatchListOpHead	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 981 of file typecheck.cpp.

◆ MatchListOpSnoc()

bool mcrl2::data::data_type_checker::MatchListOpSnoc	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 837 of file typecheck.cpp.

◆ MatchListOpTail()

bool mcrl2::data::data_type_checker::MatchListOpTail	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 1014 of file typecheck.cpp.

◆ MatchListSetBagOpIn()

bool mcrl2::data::data_type_checker::MatchListSetBagOpIn	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 1270 of file typecheck.cpp.

◆ MatchSetBagOpUnionDiffIntersect()

bool mcrl2::data::data_type_checker::MatchSetBagOpUnionDiffIntersect	(	const core::identifier_string &	data_term_name,
		const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 1389 of file typecheck.cpp.

◆ MatchSetConstructor()

bool mcrl2::data::data_type_checker::MatchSetConstructor	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 1104 of file typecheck.cpp.

◆ MatchSetOpSet2Bag()

bool mcrl2::data::data_type_checker::MatchSetOpSet2Bag	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 1058 of file typecheck.cpp.

◆ MatchSetOpSetCompl()

bool mcrl2::data::data_type_checker::MatchSetOpSetCompl	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 1538 of file typecheck.cpp.

◆ MatchSqrt()

bool mcrl2::data::data_type_checker::MatchSqrt	(	const function_sort &	type,
		sort_expression &	result
	)		const

protected

Definition at line 768 of file typecheck.cpp.

◆ MaximumType()

bool mcrl2::data::data_type_checker::MaximumType	(	const sort_expression &	Type1,
		const sort_expression &	Type2,
		sort_expression &	result
	)		const

protected

Definition at line 1737 of file typecheck.cpp.

◆ operator()() [1/5]

const data_specification mcrl2::data::data_type_checker::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.

Definition at line 4585 of file typecheck.cpp.

◆ operator()() [2/5]

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

protected

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

Parameters

[in]	data_expr	A data expression that has not been type checked.
[in]	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.

Definition at line 4330 of file typecheck.cpp.

◆ operator()() [3/5]

void mcrl2::data::data_type_checker::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

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

Definition at line 4354 of file typecheck.cpp.

◆ operator()() [4/5]

void mcrl2::data::data_type_checker::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

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

Definition at line 4405 of file typecheck.cpp.

◆ operator()() [5/5]

void mcrl2::data::data_type_checker::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

[in] eqns The list of equations that is type checked and updated.

Definition at line 4428 of file typecheck.cpp.

◆ print_context()

void mcrl2::data::data_type_checker::print_context ( ) const

inline

Definition at line 125 of file typecheck.h.

◆ read_constructors_and_mappings()

void mcrl2::data::data_type_checker::read_constructors_and_mappings	(	const function_symbol_vector &	constructors,
		const function_symbol_vector &	mappings,
		const function_symbol_vector &	normalized_constructors
	)

protected

Definition at line 3546 of file typecheck.cpp.

◆ read_sort()

void mcrl2::data::data_type_checker::read_sort ( const sort_expression & SortExpr )

protected

Definition at line 4069 of file typecheck.cpp.

◆ strict_type_check()

bool mcrl2::data::data_type_checker::strict_type_check ( const data_expression & d ) const

protected

Definition at line 84 of file typecheck.cpp.

◆ TransformVarConsTypeData()

void mcrl2::data::data_type_checker::TransformVarConsTypeData ( data_specification & data_spec )

protected

Definition at line 4540 of file typecheck.cpp.

◆ TraverseVarConsTypeD()

sort_expression mcrl2::data::data_type_checker::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

protected

Definition at line 2656 of file typecheck.cpp.

◆ TraverseVarConsTypeDN()

sort_expression mcrl2::data::data_type_checker::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

protected

Definition at line 2323 of file typecheck.cpp.

◆ typecheck_assignment()

assignment mcrl2::data::data_type_checker::typecheck_assignment	(	const assignment &	x,
		const detail::variable_context &	variable_context
	)

inline

Definition at line 90 of file typecheck.h.

◆ typecheck_assignment_list()

assignment_list mcrl2::data::data_type_checker::typecheck_assignment_list	(	const assignment_list &	assignments,
		const detail::variable_context &	variable_context
	)

inline

Definition at line 97 of file typecheck.h.

◆ typecheck_data_expression()

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

inline

Definition at line 75 of file typecheck.h.

◆ typechecked_data_specification()

const data_specification & mcrl2::data::data_type_checker::typechecked_data_specification ( ) const

inline

Definition at line 120 of file typecheck.h.

◆ TypeMatchA()

bool mcrl2::data::data_type_checker::TypeMatchA	(	const sort_expression &	Type_in,
		const sort_expression &	PosType_in,
		sort_expression &	result
	)		const

protected

Definition at line 3670 of file typecheck.cpp.

◆ TypeMatchL()

bool mcrl2::data::data_type_checker::TypeMatchL	(	const sort_expression_list &	TypeList,
		const sort_expression_list &	PosTypeList,
		sort_expression_list &	result
	)		const

protected

Definition at line 3634 of file typecheck.cpp.

◆ UnArrowProd()

bool mcrl2::data::data_type_checker::UnArrowProd	(	const sort_expression_list &	ArgTypes,
		sort_expression	PosType,
		sort_expression &	result
	)		const

protected

Definition at line 619 of file typecheck.cpp.

◆ UnFBag()

bool mcrl2::data::data_type_checker::UnFBag	(	sort_expression	PosType,
		sort_expression &	result
	)		const

protected

Definition at line 526 of file typecheck.cpp.

◆ UnFSet()

bool mcrl2::data::data_type_checker::UnFSet	(	sort_expression	PosType,
		sort_expression &	result
	)		const

protected

Definition at line 480 of file typecheck.cpp.

◆ UnifyElementSort()

bool mcrl2::data::data_type_checker::UnifyElementSort	(	sort_expression &	Arg1,
		sort_expression &	Arg2,
		sort_expression &	result
	)		const

inlineprotected

Definition at line 1384 of file typecheck.cpp.

◆ UnifyMinType()

bool mcrl2::data::data_type_checker::UnifyMinType	(	const sort_expression &	Type1,
		const sort_expression &	Type2,
		sort_expression &	result
	)		const

protected

Definition at line 696 of file typecheck.cpp.

◆ UnList()

bool mcrl2::data::data_type_checker::UnList	(	sort_expression	PosType,
		sort_expression &	result
	)		const

protected

Definition at line 572 of file typecheck.cpp.

◆ UnwindType() [1/3]

template<class T >

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

inlineprotected

Definition at line 173 of file typecheck.h.

◆ UnwindType() [2/3]

sort_expression mcrl2::data::data_type_checker::UnwindType ( const sort_expression & Type ) const

protected

Definition at line 3660 of file typecheck.cpp.

◆ UnwindType() [3/3]

variable mcrl2::data::data_type_checker::UnwindType ( const variable & v ) const

protected

Definition at line 3665 of file typecheck.cpp.

◆ upcast_numeric_type()

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

inlineprotected

Definition at line 261 of file typecheck.h.

◆ UpCastNumericType()

sort_expression mcrl2::data::data_type_checker::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

protected

Definition at line 199 of file typecheck.cpp.

Member Data Documentation

◆ system_constants

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

protected

Definition at line 31 of file typecheck.h.

◆ system_functions

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

protected

Definition at line 32 of file typecheck.h.

◆ type_checked_data_spec

data_specification mcrl2::data::data_type_checker::type_checked_data_spec

protected

Definition at line 35 of file typecheck.h.

◆ user_constants

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

protected

Definition at line 33 of file typecheck.h.

◆ user_functions

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

protected

Definition at line 34 of file typecheck.h.

◆ was_warning_upcasting

bool mcrl2::data::data_type_checker::was_warning_upcasting

mutableprotected

Definition at line 29 of file typecheck.h.

The documentation for this class was generated from the following files:

data/include/mcrl2/data/typecheck.h
data/source/typecheck.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ data_type_checker()

Member Function Documentation

◆ add_constant()

◆ add_function()

◆ add_system_constant()

◆ add_system_constants_and_functions()

◆ add_system_function()

◆ AdjustNotInferredList()

◆ determine_allowed_type()

◆ EqTypesA()

◆ EqTypesL()

◆ ErrorMsgCannotCast()

◆ ExpandNumTypesDown()

◆ ExpandNumTypesUp()

◆ ExpandNumTypesUpL()

◆ GetNotInferredList()

◆ initialise_system_defined_functions()

◆ InsertType()

◆ InTypesA()

◆ InTypesL()

◆ IsNotInferredL()

◆ IsTypeAllowedA()

◆ IsTypeAllowedL()

◆ match_fbag_cinsert()

◆ match_fset_insert()

◆ MatchBagConstructor()

◆ MatchBagOpBag2Set()

◆ MatchBagOpBagCount()

◆ MatchEqNeqComparison()

◆ MatchFalseFunction()

◆ MatchFuncUpdate()

◆ MatchIf()

◆ MatchListOpConcat()

◆ MatchListOpCons()

◆ MatchListOpEltAt()

◆ MatchListOpHead()

◆ MatchListOpSnoc()

◆ MatchListOpTail()

◆ MatchListSetBagOpIn()

◆ MatchSetBagOpUnionDiffIntersect()

◆ MatchSetConstructor()

◆ MatchSetOpSet2Bag()

◆ MatchSetOpSetCompl()

◆ MatchSqrt()

◆ MaximumType()

◆ operator()() [1/5]

◆ operator()() [2/5]

◆ operator()() [3/5]

◆ operator()() [4/5]

◆ operator()() [5/5]

◆ print_context()

◆ read_constructors_and_mappings()

◆ read_sort()

◆ strict_type_check()

◆ TransformVarConsTypeData()

◆ TraverseVarConsTypeD()

◆ TraverseVarConsTypeDN()

◆ typecheck_assignment()

◆ typecheck_assignment_list()

◆ typecheck_data_expression()

◆ typechecked_data_specification()

◆ TypeMatchA()

◆ TypeMatchL()

◆ UnArrowProd()

◆ UnFBag()

◆ UnFSet()

◆ UnifyElementSort()

◆ UnifyMinType()

◆ UnList()

◆ UnwindType() [1/3]

◆ UnwindType() [2/3]

◆ UnwindType() [3/3]

◆ upcast_numeric_type()

◆ UpCastNumericType()

Member Data Documentation