LCOV - code coverage report
Current view: top level - data/include/mcrl2/data - typecheck.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 54 61 88.5 %
Date: 2024-03-08 02:52:28 Functions: 11 11 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Jan Friso Groote, 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/data/typecheck.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_TYPECHECK_H
      13             : #define MCRL2_DATA_TYPECHECK_H
      14             : 
      15             : #include "mcrl2/atermpp/aterm_io.h"
      16             : #include "mcrl2/data/data_specification.h"
      17             : #include "mcrl2/data/detail/variable_context.h"
      18             : #include "mcrl2/data/sort_type_checker.h"
      19             : 
      20             : namespace mcrl2
      21             : {
      22             : 
      23             : namespace data
      24             : {
      25             : 
      26             : class data_type_checker: public sort_type_checker
      27             : {
      28             :   protected:
      29             :     mutable bool was_warning_upcasting; // This variable is used to limit the number of upcasting warnings.
      30             : 
      31             :     std::map<core::identifier_string,sort_expression_list> system_constants;   //name -> Set(sort expression)
      32             :     std::map<core::identifier_string,sort_expression_list> system_functions;   //name -> Set(sort expression)
      33             :     std::map<core::identifier_string,sort_expression> user_constants;          //name -> sort expression
      34             :     std::map<core::identifier_string,sort_expression_list> user_functions;     //name -> Set(sort expression)
      35             :     data_specification type_checked_data_spec;
      36             : 
      37             :   public:
      38             :     /** \brief     make a data type checker.
      39             :      *             Throws a mcrl2::runtime_error exception if the data_specification is not well typed.
      40             :      *  \param[in] data_spec A data specification that does not need to have been type checked.
      41             :      *  \return    A data expression where all untyped identifiers have been replace by typed ones.
      42             :      **/
      43             :     data_type_checker(const data_specification& data_spec);
      44             : 
      45             :     /** \brief     Type checks a variable.
      46             :      *             Throws an mcrl2::runtime_error exception if the variable is not well typed.
      47             :      *  \details   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
      48             :      *             the variable is used in its context with a different sort.
      49             :      *  \param[in] v A variables that is to be type checked.
      50             :      *  \param[in] context Information about the context of the variable.
      51             :      **/
      52             :     void operator()(const variable& v, const detail::variable_context& context) const;
      53             : 
      54             :     /** \brief     Type checks a variable list.
      55             :      *             Throws an mcrl2::runtime_error exception if the variables are not well typed.
      56             :      *  \details   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
      57             :      *             a variable occurs in the context. Furthermore, variables cannot occur multiple times in a variable list.
      58             :      *  \param[in] l A list of variables that must be type checked.
      59             :      *  \param[in] context Information about the context of the variables in the list.
      60             :      **/
      61             :     void operator()(const variable_list& l, const detail::variable_context& context) const;
      62             : 
      63             :     /** \brief     Yields a type checked data specification, provided typechecking was successful.
      64             :      *             If not successful an exception is thrown.
      65             :      *  \return    a data specification where all untyped identifiers have been replace by typed ones.
      66             :      **/
      67             :     const data_specification operator()() const;
      68             : 
      69             :     /** \brief     Yields a type checked equation list, and sets the types in the equations right.
      70             :      *             If not successful an exception is thrown.
      71             :      *  \param[in] eqns The list of equations that is type checked and updated. 
      72             :      **/
      73             :     void operator()(data_equation_vector& eqns);
      74             : 
      75       12882 :     data_expression typecheck_data_expression(const data_expression& x,
      76             :                                               const sort_expression& expected_sort,
      77             :                                               const detail::variable_context& variable_context
      78             :                                              )
      79             :     {
      80       12882 :       data_expression x1 = x;
      81       12882 :       TraverseVarConsTypeD(variable_context, x1, expected_sort);
      82       12553 :       x1 = data::normalize_sorts(x1, get_sort_specification());
      83       12553 :       if (x1.sort() != expected_sort)
      84             :       {
      85         779 :         x1 = upcast_numeric_type(x1, expected_sort, variable_context);
      86             :       }
      87       12553 :       return x1;
      88         329 :     }
      89             : 
      90          15 :     assignment typecheck_assignment(const assignment& x, const detail::variable_context& variable_context)
      91             :     {
      92          15 :       sort_type_checker::check_sort_is_declared(x.lhs().sort());
      93          15 :       data_expression rhs = typecheck_data_expression(x.rhs(), x.lhs().sort(), variable_context);
      94          30 :       return assignment(x.lhs(), rhs);
      95          15 :     }
      96             : 
      97         168 :     assignment_list typecheck_assignment_list(const assignment_list& assignments, const detail::variable_context& variable_context)
      98             :     {
      99             :       // check for name clashes
     100         168 :       std::set<core::identifier_string> names;
     101         183 :       for (const assignment& a: assignments)
     102             :       {
     103          15 :         const core::identifier_string& name = a.lhs().name();
     104          15 :         if (names.find(name) != names.end())
     105             :         {
     106           0 :           throw mcrl2::runtime_error("duplicate variable names in assignments: " + data::pp(assignments) + ")");
     107             :         }
     108          15 :         names.insert(name);
     109             :       }
     110             : 
     111             :       // typecheck the assignments
     112         168 :       assignment_vector result;
     113         183 :       for (const assignment& a: assignments)
     114             :       {
     115          15 :         result.push_back(typecheck_assignment(a, variable_context));
     116             :       }
     117         336 :       return assignment_list(result.begin(), result.end());
     118         168 :     }
     119             : 
     120        3404 :     const data_specification& typechecked_data_specification() const
     121             :     {
     122        3404 :       return type_checked_data_spec;
     123             :     }
     124             : 
     125             :     void print_context() const
     126             :     {
     127             :       auto const& sortspec = get_sort_specification();
     128             :       std::cout << "--- basic sorts ---" << std::endl;
     129             :       for (auto const& x: sortspec.user_defined_sorts())
     130             :       {
     131             :         std::cout << x << std::endl;
     132             :       }
     133             :       std::cout << "--- aliases ---" << std::endl;
     134             :       for (auto const& x: sortspec.user_defined_aliases())
     135             :       {
     136             :         std::cout << x << std::endl;
     137             :       }
     138             :       std::cout << "--- user constants ---" << std::endl;
     139             :       for (const auto& user_constant: user_constants)
     140             :       {
     141             :         std::cout << user_constant.first << " -> " << user_constant.second << std::endl;
     142             :       }
     143             :       std::cout << "--- user functions ---" << std::endl;
     144             :       for (const auto& user_function: user_functions)
     145             :       {
     146             :         std::cout << user_function.first << " -> " << user_function.second << std::endl;
     147             :       }
     148             :     }
     149             : 
     150             :   protected:
     151             :     /** \brief     Type check a data expression.
     152             :      *  Throws a mcrl2::runtime_error exception if the expression is not well typed.
     153             :      *  \param[in] data_expr A data expression that has not been type checked.
     154             :      *  \param[in] context The variable context in which this term must be typechecked.
     155             :      *  \return    a data expression where all untyped identifiers have been replace by typed ones.
     156             :      **/
     157             :     data_expression operator()(const data_expression& data_expr,
     158             :                                const detail::variable_context& context) const;
     159             : 
     160             :     void read_sort(const sort_expression& SortExpr);
     161             :     void read_constructors_and_mappings(const function_symbol_vector& constructors, const function_symbol_vector& mappings, const function_symbol_vector& normalized_constructors);
     162             :     void add_function(const data::function_symbol& f, const std::string& msg, bool allow_double_decls=false);
     163             :     void add_constant(const data::function_symbol& f, const std::string& msg);
     164             :     void initialise_system_defined_functions(void);
     165             :     void add_system_constant(const data::function_symbol& f);
     166             :     void add_system_function(const data::function_symbol& f);
     167             :     void add_system_constants_and_functions(const std::vector<data::function_symbol>& v);
     168             :     bool TypeMatchA(const sort_expression& Type_in, const sort_expression& PosType_in, sort_expression& result) const;
     169             :     bool TypeMatchL(const sort_expression_list& TypeList, const sort_expression_list& PosTypeList, sort_expression_list& result) const;
     170             :     sort_expression UnwindType(const sort_expression& Type) const;
     171             :     variable UnwindType(const variable& v) const;
     172             :     template <class T>
     173             :     atermpp::term_list<T> UnwindType(const atermpp::term_list<T>& l)
     174             :     {
     175             :       std::vector<T> result;
     176             :       for(typename atermpp::term_list<T>::const_iterator i=l.begin(); i!=l.end(); ++i)
     177             :       {
     178             :         result.push_back(UnwindType(*i));
     179             :       }
     180             :       return atermpp::term_list<T>(result.begin(),result.end());
     181             :     }
     182             : 
     183             :     sort_expression TraverseVarConsTypeD(
     184             :                         const detail::variable_context& DeclaredVars,
     185             :                         data_expression& DataTerm,
     186             :                         const sort_expression& PosType,
     187             :                         const bool strictly_ambiguous=true,
     188             :                         const bool warn_upcasting=false,
     189             :                         const bool print_cast_error=true) const;
     190             : 
     191             :     /* sort_expression TraverseVarConsTypeD(const std::map<core::identifier_string,sort_expression>& DeclaredVars,
     192             :                                          data_expression& t1,
     193             :                                          const sort_expression& t2); */
     194             : 
     195             :     sort_expression TraverseVarConsTypeDN(
     196             :                            const detail::variable_context& DeclaredVars,
     197             :                            data_expression& DataTerm,
     198             :                            sort_expression PosType,
     199             :                            const bool strictly_ambiguous=true,
     200             :                            const std::size_t nFactPars=std::string::npos,
     201             :                            const bool warn_upcasting=false,
     202             :                            const bool print_cast_error=true) const;
     203             : 
     204             :     bool InTypesA(const sort_expression& Type, sort_expression_list Types) const;
     205             :     bool EqTypesA(const sort_expression& Type1, const sort_expression& Type2) const;
     206             :     bool InTypesL(const sort_expression_list& Type, atermpp::term_list<sort_expression_list> Types) const;
     207             :     bool EqTypesL(sort_expression_list Type1, sort_expression_list Type2) const;
     208             :     bool MaximumType(const sort_expression& Type1, const sort_expression& Type2, sort_expression& result) const;
     209             :     sort_expression ExpandNumTypesUp(sort_expression Type) const;
     210             :     sort_expression_list ExpandNumTypesUpL(const sort_expression_list& type_list) const;
     211             :     sort_expression ExpandNumTypesDown(sort_expression Type) const;
     212             :     bool UnifyMinType(const sort_expression& Type1, const sort_expression& Type2, sort_expression& result) const;
     213             :     sort_expression determine_allowed_type(const data_expression& d, const sort_expression& proposed_type) const;
     214             :     bool MatchIf(const function_sort& type, sort_expression& result) const;
     215             :     bool MatchEqNeqComparison(const function_sort& type, sort_expression& result) const;
     216             :     bool MatchSqrt(const function_sort& type, sort_expression& result) const;
     217             :     bool MatchListOpCons(const function_sort& type, sort_expression& result) const;
     218             :     bool MatchListOpSnoc(const function_sort& type, sort_expression& result) const;
     219             :     bool MatchListOpConcat(const function_sort& type, sort_expression& result) const;
     220             :     bool MatchListOpEltAt(const function_sort& type, sort_expression& result) const;
     221             :     bool MatchListOpHead(const function_sort& type, sort_expression& result) const;
     222             :     bool MatchListOpTail(const function_sort& type, sort_expression& result) const;
     223             :     bool MatchSetOpSet2Bag(const function_sort& type, sort_expression& result) const;
     224             :     bool MatchFalseFunction(const function_sort& type, sort_expression& result) const;
     225             :     bool MatchListSetBagOpIn(const function_sort& type, sort_expression& result) const;
     226             :     bool match_fset_insert(const function_sort& type, sort_expression& result) const;
     227             :     bool match_fbag_cinsert(const function_sort& type, sort_expression& result) const;
     228             :     bool MatchSetBagOpUnionDiffIntersect(const function_sort& type, sort_expression& result) const;
     229             :     bool MatchSetOpSetCompl(const function_sort& type, sort_expression& result) const;
     230             :     bool MatchBagOpBag2Set(const function_sort& type, sort_expression& result) const;
     231             :     bool MatchBagOpBagCount(const function_sort& type, sort_expression& result) const;
     232             :     bool MatchFuncUpdate(const function_sort& type, sort_expression& result) const;
     233             :     bool MatchSetConstructor(const function_sort& type, sort_expression& result) const;
     234             :     bool MatchBagConstructor(const function_sort& type, sort_expression& result) const;
     235             :     bool UnArrowProd(const sort_expression_list& ArgTypes, sort_expression PosType, sort_expression& result) const;
     236             :     bool UnFSet(sort_expression PosType, sort_expression& result) const;
     237             :     bool UnFBag(sort_expression PosType, sort_expression& result) const;
     238             :     bool UnList(sort_expression PosType, sort_expression& result) const;
     239             :     void ErrorMsgCannotCast(sort_expression CandidateType, data_expression_list Arguments, sort_expression_list ArgumentTypes,std::string previous_reason) const;
     240             :     sort_expression UpCastNumericType(
     241             :                     sort_expression NeededType,
     242             :                     sort_expression Type,
     243             :                     data_expression& Par,
     244             :                     const detail::variable_context& DeclaredVars,
     245             :                     const bool strictly_ambiguous,
     246             :                     bool warn_upcasting=false,
     247             :                     const bool print_cast_error=false) const;
     248             :     void TransformVarConsTypeData(data_specification& data_spec);
     249             :     sort_expression_list GetNotInferredList(const atermpp::term_list<sort_expression_list>& TypeListList) const;
     250             :     sort_expression_list InsertType(const sort_expression_list& TypeList, const sort_expression& Type) const;
     251             :     std::pair<bool,sort_expression_list> AdjustNotInferredList(
     252             :             const sort_expression_list& PosTypeList,
     253             :             const atermpp::term_list<sort_expression_list>& TypeListList) const;
     254             :     bool IsTypeAllowedA(const sort_expression& Type, const sort_expression& PosType) const;
     255             :     bool IsTypeAllowedL(const sort_expression_list& TypeList, const sort_expression_list& PosTypeList) const;
     256             :     bool IsNotInferredL(sort_expression_list TypeList) const;
     257             :     bool strict_type_check(const data_expression& d) const;
     258             : 
     259             :     // for example Pos -> Nat, or Nat -> Int
     260         779 :     data_expression upcast_numeric_type(const data_expression& x,
     261             :                                         const sort_expression& expected_sort,
     262             :                                         const detail::variable_context& variable_context
     263             :                                        )
     264             :     {
     265             :       try
     266             :       {
     267         779 :         data_expression x1 = x;
     268         779 :         UpCastNumericType(expected_sort, x.sort(), x1, variable_context, false, false, false);
     269        1558 :         return data::normalize_sorts(x1, get_sort_specification());
     270         779 :       }
     271           0 :       catch (mcrl2::runtime_error& e)
     272             :       {
     273           0 :         throw mcrl2::runtime_error(std::string(e.what()) + "\ncannot (up)cast " + data::pp(x) + " to type " + data::pp(expected_sort));
     274           0 :       }
     275             :     }
     276             : 
     277             : };
     278             : 
     279             : /** \brief     Type check a sort expression.
     280             :  *  Throws an exception if something went wrong.
     281             :  *  \param[in] sort_expr A sort expression that has not been type checked.
     282             :  *  \param[in] data_spec The data specification to use as context.
     283             :  *  \post      sort_expr is type checked.
     284             :  **/
     285             : inline
     286          29 : void typecheck_sort_expression(const sort_expression& sort_expr, const data_specification& data_spec)
     287             : {
     288             :   try
     289             :   {
     290             :     // sort_type_checker type_checker(data_spec.user_defined_sorts(), data_spec.user_defined_aliases());
     291          29 :     sort_type_checker type_checker(data_spec);
     292          29 :     type_checker(sort_expr);
     293          29 :   }
     294           0 :   catch (mcrl2::runtime_error& e)
     295             :   {
     296           0 :     throw mcrl2::runtime_error(std::string(e.what()) + "\nCould not type check sort " + pp(sort_expr));
     297           0 :   }
     298          29 : }
     299             : 
     300             : /** \brief     Type check a data expression.
     301             :  *  Throws an exception if something went wrong.
     302             :  *  \param[in] x A data expression that has not been type checked.
     303             :  *  \param[in] variables A container with variables that can occur in the data expression.
     304             :  *  \param[in] dataspec The data specification that is used for type checking.
     305             :  *  \post      data_expr is type checked.
     306             :  **/
     307             : template <typename VariableContainer>
     308         809 : data_expression typecheck_data_expression(const data_expression& x,
     309             :                                           const VariableContainer& variables,
     310             :                                           const data_specification& dataspec = data_specification()
     311             :                                          )
     312             : {
     313             :   try
     314             :   {
     315         809 :     data_type_checker typechecker(dataspec);
     316         809 :     detail::variable_context variable_context;
     317         809 :     variable_context.add_context_variables(variables, typechecker);
     318        2397 :     return typechecker.typecheck_data_expression(x, untyped_sort(), variable_context);
     319         839 :   }
     320          60 :   catch (mcrl2::runtime_error& e)
     321             :   {
     322          30 :     throw mcrl2::runtime_error(std::string(e.what()) + "\nCould not type check data expression " + data::pp(x));
     323             :   }
     324             : }
     325             : 
     326             : /** \brief     Type check a data expression.
     327             :  *  Throws an exception if something went wrong.
     328             :  *  \param[in] x A data expression that has not been type checked.
     329             :  *  \param[in] dataspec Data specification to be used as context.
     330             :  *  \post      data_expr is type checked.
     331             :  **/
     332             : inline
     333          16 : data_expression typecheck_data_expression(const data_expression& x, const data_specification& dataspec = data_specification())
     334             : {
     335          16 :   return typecheck_data_expression(x, variable_list(), dataspec);
     336             : }
     337             : 
     338             : /** \brief     Type check a parsed mCRL2 data specification.
     339             :  *  Throws an exception if something went wrong.
     340             :  *  \param[in] data_spec A data specification that has not been type checked.
     341             :  *  \post      data_spec is type checked.
     342             :  **/
     343             : inline
     344         158 : void typecheck_data_specification(data_specification& data_spec)
     345             : {
     346         158 :   data_type_checker type_checker(data_spec);
     347         146 :   data_spec=type_checker();
     348         146 : }
     349             : 
     350             : inline
     351         165 : data_expression typecheck_untyped_data_parameter(data_type_checker& typechecker,
     352             :                                                  const core::identifier_string& name,
     353             :                                                  const data_expression_list& parameters,
     354             :                                                  const data::sort_expression& expected_sort,
     355             :                                                  const detail::variable_context& variable_context
     356             :                                                 )
     357             : {
     358         165 :   if (parameters.empty())
     359             :   {
     360         190 :     return typechecker.typecheck_data_expression(untyped_identifier(name), expected_sort, variable_context);
     361             :   }
     362             :   else
     363             :   {
     364         140 :     return typechecker.typecheck_data_expression(application(untyped_identifier(name), parameters), expected_sort, variable_context);
     365             :   }
     366             : }
     367             : 
     368             : typedef atermpp::term_list<sort_expression_list> sorts_list;
     369             : 
     370             : } // namespace data
     371             : 
     372             : } // namespace mcrl2
     373             : 
     374             : #endif // MCRL2_DATA_TYPECHECK_H

Generated by: LCOV version 1.14