(self, tokens, command, type_params=None, additional_token=None)
Parses a single type name from the tokens
Parses a single type name from the tokens
Parses a single type name from the tokens
def parse_type(self, tokens, command, type_params=None, additional_token=None):
        """Parses a single type name from the tokens"""
        if additional_token is not None:
            var = additional_token
        else:
            var = tokens.consume("Unexpected end of stream in %s command." %
                                         command)
        res = None
        if type_params and var in type_params:
            return (var,) # This is a type parameter, it is handled recursively
        elif var == "(":
            op = tokens.consume("Unexpected end of stream in %s command." %
                                        command)
            if op == "Array":
                idxtype = self.parse_type(tokens, command)
                elemtype = self.parse_type(tokens, command)
                self.consume_closing(tokens, command)
                res = self.env.type_manager.ArrayType(idxtype, elemtype)

            elif op == "_":
                ts = tokens.consume("Unexpected end of stream in %s command." %
                                            command)
                if ts != "BitVec":
                    raise PysmtSyntaxError("Unexpected token '%s' in %s command." %
                                           (ts, command),
                                           tokens.pos_info)

                size = 0
                dim = tokens.consume()
                try:
                    size = int(dim)
                except ValueError:
                    raise PysmtSyntaxError("Unexpected token '%s' in %s command." %
                                           (dim, command),
                                           tokens.pos_info)

                self.consume_closing(tokens, command)
                res = self.env.type_manager.BVType(size)
            else:
                # It must be a custom-defined type
                base_type = self.cache.get(op)
                if base_type is None or not isinstance(base_type, _TypeDecl):
                    raise PysmtSyntaxError("Unexpected token '%s' in %s command." %
                                           (op, command),
                                           tokens.pos_info)
                pparams = []
                has_free_params = False
                for _ in range(base_type.arity):
                    ty = self.parse_type(tokens, command, type_params=type_params)
                    pparams.append(ty)
                    if isinstance(ty, tuple):
                        has_free_params = True
                if has_free_params:
                    def definition(*args):
                        params = []
                        for x in pparams:
                            if isinstance(x, tuple):
                                params.append(args[type_params.index(x[0])])
                            else:
                                params.append(x)
                        return self.env.type_manager.get_type_instance(base_type, *params)
                    res = PartialType("tmp", definition)
                else:
                    res = self.env.type_manager.get_type_instance(base_type, *pparams)
                self.consume_closing(tokens, command)
        elif var == "Bool":
            res = self.env.type_manager.BOOL()
        elif var == "Int":
            res = self.env.type_manager.INT()
        elif var == "Real":
            res = self.env.type_manager.REAL()
        elif var == "String":
            res = self.env.type_manager.STRING()
        else:
            res = self.cache.get(var)
            if res is None:
                raise PysmtSyntaxError("Unexpected token '%s' in %s command." %
                                       (var, command),
                                       tokens.pos_info)

        if isinstance(res, _TypeDecl):
            return self.env.type_manager.get_type_instance(res)
        else:
            return res
def parse_type ( self , tokens , command , type_params = None , additional_token = None ) : if additional_token is not None : var = additional_token else : var = tokens . consume ( "Unexpected end of stream in %s command." % command ) res = None if type_params and var in type_params : return ( var , ) # This is a type parameter, it is handled recursively elif var == "(" : op = tokens . consume ( "Unexpected end of stream in %s command." % command ) if op == "Array" : idxtype = self . parse_type ( tokens , command ) elemtype = self . parse_type ( tokens , command ) self . consume_closing ( tokens , command ) res = self . env . type_manager . ArrayType ( idxtype , elemtype ) elif op == "_" : ts = tokens . consume ( "Unexpected end of stream in %s command." % command ) if ts != "BitVec" : raise PysmtSyntaxError ( "Unexpected token '%s' in %s command." % ( ts , command ) , tokens . pos_info ) size = 0 dim = tokens . consume ( ) try : size = int ( dim ) except ValueError : raise PysmtSyntaxError ( "Unexpected token '%s' in %s command." % ( dim , command ) , tokens . pos_info ) self . consume_closing ( tokens , command ) res = self . env . type_manager . BVType ( size ) else : # It must be a custom-defined type base_type = self . cache . get ( op ) if base_type is None or not isinstance ( base_type , _TypeDecl ) : raise PysmtSyntaxError ( "Unexpected token '%s' in %s command." % ( op , command ) , tokens . pos_info ) pparams = [ ] has_free_params = False for _ in range ( base_type . arity ) : ty = self . parse_type ( tokens , command , type_params = type_params ) pparams . append ( ty ) if isinstance ( ty , tuple ) : has_free_params = True if has_free_params : def definition ( * args ) : params = [ ] for x in pparams : if isinstance ( x , tuple ) : params . append ( args [ type_params . index ( x [ 0 ] ) ] ) else : params . append ( x ) return self . env . type_manager . get_type_instance ( base_type , * params ) res = PartialType ( "tmp" , definition ) else : res = self . env . type_manager . get_type_instance ( base_type , * pparams ) self . consume_closing ( tokens , command ) elif var == "Bool" : res = self . env . type_manager . BOOL ( ) elif var == "Int" : res = self . env . type_manager . INT ( ) elif var == "Real" : res = self . env . type_manager . REAL ( ) elif var == "String" : res = self . env . type_manager . STRING ( ) else : res = self . cache . get ( var ) if res is None : raise PysmtSyntaxError ( "Unexpected token '%s' in %s command." % ( var , command ) , tokens . pos_info ) if isinstance ( res , _TypeDecl ) : return self . env . type_manager . get_type_instance ( res ) else : return res