Function checkFunApply

analysis/validation.go:1383–1407

(z ast.ApplyFn, fnTpe ast.BaseTerm, varRanges map[ast.Variable]ast.BaseTerm, nameTrie symbols.NameTrie)

}

func checkFunApply(z ast.ApplyFn, fnTpe ast.BaseTerm, varRanges map[ast.Variable]ast.BaseTerm, nameTrie symbols.NameTrie) (ast.BaseTerm, error) {
	if fnTpe.Equals(symbols.EmptyType) {
		return nil, fmt.Errorf("type checking for %v not implemented", z)
	}
	argTypes, err := symbols.FunTypeArgs(fnTpe)
	if err != nil {
		return nil, fmt.Errorf("not a function type: %v", fnTpe)
	}
	if len(argTypes) != len(z.Args) {
		return nil, fmt.Errorf("wrong number of arguments: expected %d got %d", len(argTypes), len(z.Args))
	}
	actualTpes := make([]ast.BaseTerm, len(argTypes))
	for i, arg := range z.Args {
		actualTpes[i] = boundOfArg(arg, varRanges, nameTrie)
	}
	subst, err := unionfind.UnifyTypeExpr(actualTpes, argTypes)
	if err != nil {
		return nil, fmt.Errorf("could not unify %v and %v: %v", actualTpes, argTypes, err)
	}
	res, err := symbols.FunTypeResult(fnTpe)
	if err != nil {
		return nil, fmt.Errorf("not a function type: %v", fnTpe)
	}
	return res.ApplySubstBase(ast.SubstMap(subst)), nil
}

func boundOfArg(x ast.BaseTerm, varRanges map[ast.Variable]ast.BaseTerm, nameTrie symbols.NameTrie) ast.BaseTerm {
	switch z := x.(type) {