Uninterpreted function declaration, created via ``Function(...)``.
| 896 | |
| 897 | |
| 898 | class FuncDeclRef: |
| 899 | """Uninterpreted function declaration, created via ``Function(...)``.""" |
| 900 | |
| 901 | __slots__ = ("_name", "_domain", "_range", "_ast_sort") |
| 902 | |
| 903 | def __init__( |
| 904 | self, |
| 905 | name: str, |
| 906 | domain: tuple[SortRef, ...], |
| 907 | range_sort: SortRef, |
| 908 | ) -> None: |
| 909 | self._name = name |
| 910 | self._domain = domain |
| 911 | self._range = range_sort |
| 912 | # Build arrow sort for the function type |
| 913 | sorts = [*domain, range_sort] |
| 914 | ast_sort: ASTSort = sorts[-1]._ast_sort |
| 915 | for s in reversed(sorts[:-1]): |
| 916 | ast_sort = ArrowASTSort(s._ast_sort, ast_sort) |
| 917 | self._ast_sort = ast_sort |
| 918 | |
| 919 | def __call__(self, *args: ExprRef) -> ExprRef: |
| 920 | if len(args) != len(self._domain): |
| 921 | raise TypeError(f"{self._name} expects {len(self._domain)} args, got {len(args)}") |
| 922 | merged: frozenset[tuple[str, ASTSort]] = frozenset().union(*(a._vars for a in args)) |
| 923 | # The function itself is a free variable |
| 924 | merged = merged | frozenset([(self._name, self._ast_sort)]) |
| 925 | # Uninterpreted sorts used by the function are also free |
| 926 | # (unless already declared as axioms in the Lean environment) |
| 927 | for s in (*self._domain, self._range): |
| 928 | if isinstance(s, UninterpretedSortRef) and isinstance(s._ast_sort, UninterpASTSort): |
| 929 | if s._ast_sort.name not in _declared_uninterp_sorts: |
| 930 | merged = merged | frozenset([(s._ast_sort.name, TypeASTSort())]) |
| 931 | func_ast = _AstVar(self._name) |
| 932 | args_ast = tuple(a._ast for a in args) |
| 933 | ast = AppNode(func_ast, args_ast) if args else func_ast |
| 934 | return _wrap_expr(ast, self._range, merged) |
| 935 | |
| 936 | def name(self) -> str: |
| 937 | """Return the function name.""" |
| 938 | return self._name |
| 939 | |
| 940 | def arity(self) -> int: |
| 941 | """Return the number of arguments.""" |
| 942 | return len(self._domain) |
| 943 | |
| 944 | def domain(self, i: int) -> SortRef: |
| 945 | """Return the sort of the i-th argument.""" |
| 946 | return self._domain[i] |
| 947 | |
| 948 | def range(self) -> SortRef: |
| 949 | """Return the range (return) sort.""" |
| 950 | return self._range |
| 951 | |
| 952 | def __repr__(self) -> str: |
| 953 | return f"{self._name} : {_sort_repr(self._ast_sort)}" |
| 954 | |
| 955 |
no outgoing calls
no test coverage detected