diff --git a/.github/workflows/python-app.yml b/.github/workflows/python-app.yml index 389e5da7..fdf66268 100644 --- a/.github/workflows/python-app.yml +++ b/.github/workflows/python-app.yml @@ -25,12 +25,17 @@ jobs: uses: actions/setup-python@v3 with: python-version: "3.7" - - name: Install development dependencies + - name: Install test dependencies run: | - pip install -e .[dev] + pip install -e .[test] - name: Test run: | - tox run + coverage run -m nose2 --pretty-assert concat.tests + - name: Collect coverage into one file + run: | + coverage combine + coverage xml + coverage lcov - name: Report test coverage to DeepSource uses: deepsourcelabs/test-coverage-action@master with: diff --git a/concat/__main__.py b/concat/__main__.py index ffbb8f5e..85415992 100644 --- a/concat/__main__.py +++ b/concat/__main__.py @@ -3,18 +3,16 @@ import argparse from concat.transpile import parse, transpile_ast, typecheck -import concat.astutils +from concat.error_reporting import get_line_at, create_parsing_failure_message import concat.execute import concat.lex import concat.parser_combinators import concat.stdlib.repl import concat.typecheck -import io import json import os.path import sys -import textwrap -from typing import Callable, IO, AnyStr, Sequence, TextIO +from typing import Callable, IO, AnyStr filename = '' @@ -31,29 +29,6 @@ def func(name: str) -> IO[AnyStr]: return func -def get_line_at(file: TextIO, location: concat.astutils.Location) -> str: - file.seek(0, io.SEEK_SET) - lines = [*file] - return lines[location[0] - 1] - - -def create_parsing_failure_message( - file: TextIO, - stream: Sequence[concat.lex.Token], - failure: concat.parser_combinators.FailureTree, -) -> str: - location = stream[failure.furthest_index].start - line = get_line_at(file, location) - message = f'Expected {failure.expected} at line {location[0]}, column {location[1] + 1}:\n{line.rstrip()}\n{" " * location[1] + "^"}' - if failure.children: - message += '\nbecause:' - for f in failure.children: - message += '\n' + textwrap.indent( - create_parsing_failure_message(file, stream, f), ' ' - ) - return message - - arg_parser = argparse.ArgumentParser(description='Run a Concat program.') arg_parser.add_argument( 'file', @@ -68,6 +43,12 @@ def create_parsing_failure_message( default=False, help='turn stack debugging on', ) +arg_parser.add_argument( + '--verbose', + action='store_true', + default=False, + help='print internal logs and errors', +) arg_parser.add_argument( '--tokenize', action='store_true', @@ -103,11 +84,21 @@ def create_parsing_failure_message( typecheck(concat_ast, source_dir) python_ast = transpile_ast(concat_ast) except concat.typecheck.StaticAnalysisError as e: - print('Static Analysis Error:\n') + if e.path is None: + in_path = '' + else: + in_path = ' in file ' + str(e.path) + print(f'Static Analysis Error{in_path}:\n') print(e, 'in line:') if e.location: - print(get_line_at(args.file, e.location), end='') + if e.path is not None: + with e.path.open() as f: + print(get_line_at(f, e.location), end='') + else: + print(get_line_at(args.file, e.location), end='') print(' ' * e.location[1] + '^') + if args.verbose: + raise except concat.parser_combinators.ParseError as e: print('Parse Error:') print( diff --git a/concat/error_reporting.py b/concat/error_reporting.py new file mode 100644 index 00000000..f44b75fd --- /dev/null +++ b/concat/error_reporting.py @@ -0,0 +1,28 @@ +import concat.astutils +import concat.parser_combinators +import io +import textwrap +from typing import Sequence, TextIO + + +def get_line_at(file: TextIO, location: concat.astutils.Location) -> str: + file.seek(0, io.SEEK_SET) + lines = [*file] + return lines[location[0] - 1] + + +def create_parsing_failure_message( + file: TextIO, + stream: Sequence[concat.lex.Token], + failure: concat.parser_combinators.FailureTree, +) -> str: + location = stream[failure.furthest_index].start + line = get_line_at(file, location) + message = f'Expected {failure.expected} at line {location[0]}, column {location[1] + 1}:\n{line.rstrip()}\n{" " * location[1] + "^"}' + if failure.children: + message += '\nbecause:' + for f in failure.children: + message += '\n' + textwrap.indent( + create_parsing_failure_message(file, stream, f), ' ' + ) + return message diff --git a/concat/examples/continuation.cat b/concat/examples/continuation.cat index 0745daef..0bcd7d59 100644 --- a/concat/examples/continuation.cat +++ b/concat/examples/continuation.cat @@ -6,10 +6,10 @@ from concat.stdlib.continuation import ContinuationMonad from concat.stdlib.continuation import call_with_current_continuation from concat.stdlib.continuation import eval_cont from concat.stdlib.continuation import cont_pure +from concat.stdlib.continuation import map_cont from concat.stdlib.continuation import bind_cont from concat.stdlib.continuation import cont_from_cps from concat.stdlib.pyinterop import to_dict -# from concat.stdlib.execution import loop # FIXME: This line should cause an error when there's no @@types in that module def abort(k:forall *s. (*s x:`a -- *s n:none) -- n:none): @@ -21,10 +21,14 @@ def abort(k:forall *s. (*s x:`a -- *s n:none) -- n:none): # arguments. +def ignore_int(i:int -- n:none): + drop None + + def ten_times(k:forall *s. (*s i:int -- *s c:ContinuationMonad[none, int]) -- c:ContinuationMonad[none, none]): # k 0 $(k:forall *s. (*s i:int -- *s c:ContinuationMonad[none, int]) n:int: - 1 + dup pick call eval_cont drop dup 10 < + 1 + dup pick call $:~ignore_int map_cont eval_cont drop dup 10 < ) loop drop drop $:~abort cont_from_cps diff --git a/concat/examples/strstr.cat b/concat/examples/strstr.cat index 9820723b..84ade233 100644 --- a/concat/examples/strstr.cat +++ b/concat/examples/strstr.cat @@ -17,6 +17,7 @@ def simple_str(obj:object -- string:str): None swap None swap to_str def strstr(haystack:str needle:str -- index:int): - [(), None, None] None to_dict swap pick$.find py_call cast (int) nip + # FIXME: These casts should be unnecessary + [(), None, None] None to_dict swap pick cast (str) $.find py_call cast (int) nip get_input get_input strstr simple_str put_output diff --git a/concat/examples/symmetric_tree.cat b/concat/examples/symmetric_tree.cat index 5adf33e2..6e216cbc 100644 --- a/concat/examples/symmetric_tree.cat +++ b/concat/examples/symmetric_tree.cat @@ -6,7 +6,6 @@ # Tree input format: [, , ] # None is the empty tree -from builtins import eval from concat.stdlib.pyinterop import getitem from concat.stdlib.pyinterop import to_str from concat.stdlib.pyinterop import to_dict diff --git a/concat/kind-poly.md b/concat/kind-poly.md new file mode 100644 index 00000000..f223cfb7 --- /dev/null +++ b/concat/kind-poly.md @@ -0,0 +1,55 @@ +# Kind Polymorphism + +* Will probably want kind variables in the future + * Introduce a kind `Kind` at that point +* And kind aliases, too + +Probably, the easiest migration is to take the individual variable syntax: + +``` +`t +``` + +And use it to mean item-kinded variables instead. + +## Prior art + +* [Adding kind-polymorphism to the Scala programming language](https://codesync.global/media/adding-kind-polymorphism-to-the-scala-programming-language/) + * [`AnyKind`](https://www.scala-lang.org/api/current/scala/AnyKind.html) + +## Kinds + +* (?) Item: the kind of types of stack items + * Just use Individual? + * I use kinds for arity checking too, so I think that would make it harder + * Needed to exclude Sequence from kind-polymorphic type parameters where a + Sequence is invalid, e.g: + * `def drop[t : Item](*s t -- *s)` (possible syntax) +* Individual: the kind of zero-arity types of values +* Generic: type constructors + * they have arities + * they always construct an individual type + * I should change this + * they can be the type of a value, e.g. polymorphic functions +* Sequence: stack types + +### Subkinding + +``` + Item + / \ +Individual Generic + + +Sequence +``` + +## Syntax + +* `def drop[t : Item](*s t -- *s)` + * First thing I thought of + * Looks more natural to me + * Similar to type parameter syntax for classes +* `def drop(forall (t : Item). (*s t -- *s)):` + * Uses existing forall syntax, but extended + * Opens the door to allowing any type syntax as a type annotation diff --git a/concat/lex.py b/concat/lex.py index 11a3e481..09ba5686 100644 --- a/concat/lex.py +++ b/concat/lex.py @@ -127,6 +127,8 @@ def _tokens(self) -> Iterator['Token']: continue elif tok.value == '$': tok.type = 'DOLLARSIGN' + elif tok.value == '!': + tok.type = 'EXCLAMATIONMARK' elif tok.value in {'def', 'import', 'from'}: tok.type = tok.value.upper() tok.is_keyword = True diff --git a/concat/linked_list.py b/concat/linked_list.py new file mode 100644 index 00000000..887ef315 --- /dev/null +++ b/concat/linked_list.py @@ -0,0 +1,116 @@ +from typing import ( + Callable, + Iterable, + Iterator, + List, + Optional, + Sequence, + Tuple, + TypeVar, + Union, + overload, +) +from typing_extensions import Never + +_T_co = TypeVar('_T_co', covariant=True) +_T = TypeVar('_T') + + +class LinkedList(Sequence[_T_co]): + def __init__( + self, _val: Optional[Tuple[_T_co, 'LinkedList[_T_co]']] + ) -> None: + self._val = _val + self._length: Optional[int] = None + + @classmethod + def from_iterable(cls, iterable: Iterable[_T_co]) -> 'LinkedList[_T_co]': + if isinstance(iterable, cls): + return iterable + l: LinkedList[_T_co] = cls(None) + head = l + for el in iterable: + next_node = cls(None) + l._val = (el, next_node) + l = next_node + return head + + @overload + def __getitem__(self, i: int) -> _T_co: + pass + + @overload + def __getitem__(self, i: slice) -> 'LinkedList[_T_co]': + pass + + def __getitem__( + self, i: Union[slice, int] + ) -> Union['LinkedList[_T_co]', _T_co]: + if isinstance(i, slice): + raise NotImplementedError + for _ in range(i): + if self._val is None: + raise IndexError + self = self._val[1] + if self._val is None: + raise IndexError + return self._val[0] + + def __len__(self) -> int: + if self._length is None: + node = self + length = 0 + while node._val is not None: + node = node._val[1] + length += 1 + self._length = length + return self._length + + def __add__(self, other: 'LinkedList[_T_co]') -> 'LinkedList[_T_co]': + if not isinstance(other, LinkedList): + return NotImplemented + for el in reversed(list(self)): + other = LinkedList((el, other)) + return other + + def filter(self, p: Callable[[_T_co], bool]) -> 'LinkedList[_T_co]': + if self._val is None: + return self + # FIXME: Stack safety + # TODO: Reuse as much of tail as possible + if p(self._val[0]): + tail = self._val[1].filter(p) + return LinkedList((self._val[0], tail)) + return self._val[1].filter(p) + + def _tails(self) -> 'List[LinkedList[_T_co]]': + res: List[LinkedList[_T_co]] = [] + while self._val is not None: + res.append(self) + self = self._val[1] + return res + + def __iter__(self) -> Iterator[_T_co]: + while self._val is not None: + yield self._val[0] + self = self._val[1] + + def __str__(self) -> str: + return str(list(self)) + + def __repr__(self) -> str: + return f'LinkedList.from_iterable({list(self)!r})' + + # "supertype defines the argument type as object" + def __eq__(self, other: object) -> bool: + if not isinstance(other, LinkedList): + return NotImplemented + if len(self) != len(other): + return False + for a, b in zip(self, other): + if a != b: + return False + return True + + +empty_list = LinkedList[Never](None) diff --git a/concat/orderedset.py b/concat/orderedset.py index dae23a5a..3ffa2708 100644 --- a/concat/orderedset.py +++ b/concat/orderedset.py @@ -1,6 +1,13 @@ -from itertools import repeat -from typing import AbstractSet, Iterable, Iterator, TypeVar - +from concat.linked_list import LinkedList +from typing import ( + AbstractSet, + Any, + Iterable, + Iterator, + Optional, + Tuple, + TypeVar, +) _T = TypeVar('_T', covariant=True) @@ -8,26 +15,544 @@ class OrderedSet(AbstractSet[_T]): def __init__(self, elements: Iterable[_T]) -> None: super().__init__() - # In Python 3.7+, dicts are guaranteed to use insertion order. - self._dictionary = dict(zip(elements, repeat(None))) + self._data = _Tree23.from_iterable(elements) + + def __sub__(self, other: object) -> 'OrderedSet[Any]': + if not isinstance(other, AbstractSet): + return NotImplemented + data = self._data + for el in other: + data = data.delete(el) + return OrderedSet(data) + + def __or__(self, other: object) -> 'OrderedSet[Any]': + if not isinstance(other, AbstractSet): + return NotImplemented + data = self._data + for el in other: + data = data.insert(el) + return OrderedSet(data) + + def __contains__(self, element: object) -> bool: + return element in self._data + + def __iter__(self) -> Iterator[_T]: + return iter(self._data) + + def __reversed__(self) -> Iterator[_T]: + return reversed(self._data) + + def __len__(self) -> int: + return len(self._data) + + +# Inspired by Java's LinkedHashSet +# https://github.com/anjbur/java-immutable-collections/blob/master/src/main/java/org/javimmutable/collections/inorder/JImmutableInsertOrderSet.java +class InsertionOrderedSet(AbstractSet[_T]): + def __init__( + self, + elements: 'Iterable[_T]', + _order: Optional[LinkedList[_T]] = None, + ) -> None: + super().__init__() + self._order = ( + LinkedList.from_iterable(elements) if _order is None else _order + ) + if isinstance(elements, OrderedSet): + self._data = elements + else: + # elements might be an iterator that gets exhausted + self._data = OrderedSet(self._order) - def __sub__(self, other: object) -> 'OrderedSet[_T]': + def __sub__(self, other: object) -> 'InsertionOrderedSet[_T]': if not isinstance(other, AbstractSet): return NotImplemented - return OrderedSet( - element for element in self._dictionary if element not in other + data = self._data - other + new_set = InsertionOrderedSet[_T]( + data, self._order.filter(lambda x: x not in other) ) + return new_set - def __or__(self, other: object) -> 'OrderedSet[_T]': + def __or__(self, other: object) -> 'InsertionOrderedSet[Any]': if not isinstance(other, AbstractSet): return NotImplemented - return OrderedSet([*self, *other]) + data = self._data | other + if isinstance(other, InsertionOrderedSet): + order = self._order + other._order + else: + order = self._order + LinkedList.from_iterable(list(other)) + order = filter_duplicates(order) + new_set = InsertionOrderedSet(data, order) + return new_set def __contains__(self, element: object) -> bool: - return element in self._dictionary + return element in self._data def __iter__(self) -> Iterator[_T]: - return iter(self._dictionary) + return iter(self._order) + + def __len__(self) -> int: + return len(self._data) + + +def filter_duplicates(xs: LinkedList[_T]) -> LinkedList[_T]: + found = set() + + def predicate(x: _T) -> bool: + nonlocal found + if x in found: + return False + found.add(x) + return True + + return xs.filter(predicate) + + +class _Tree23Hole: + pass + + +class _Tree23: + """Implementation based on https://www.cs.princeton.edu/~dpw/courses/cos326-12/ass/2-3-trees.pdf. + + Kinds of nodes: + Leaf: () + 2-node: (l, X, r) + 3-node: (l, X, m, Y, r) + + Intermediary nodes: + Kicked up node: ('up', a, w, b) + Hole node: (__hole, l)""" + + def __init__(self, data: tuple) -> None: + self._data = data + if self.is_leaf(): + self.height = 0 + elif self.is_2_node(): + # assert not isinstance(data[0], _Tree23Hole) and not isinstance( + # data[2], _Tree23Hole) + self.height = max(data[0].height, data[2].height) + 1 + elif self.is_3_node(): + # assert not isinstance(data[0], _Tree23Hole) and not isinstance( + # data[2], _Tree23Hole) and not isinstance(data[4], _Tree23Hole) + self.height = ( + max(data[0].height, data[2].height, data[4].height) + 1 + ) + elif self._is_kicked_up_node(): + assert not isinstance(data[2], _Tree23Hole) and not isinstance( + data[3], _Tree23Hole + ) + self.height = max(data[1].height, data[3].height) + elif self._is_hole_node(): + self.height = data[1].height + 1 + else: + raise ValueError('Invalid 2-3 tree') + + @classmethod + def from_iterable(cls, i: Iterable) -> '_Tree23': + if isinstance(i, cls): + return i + tree = _leaf_23_tree + for el in i: + tree = tree.insert(el) + return tree + + def search(self, d) -> Tuple[bool, Any]: + t = self + while True: + data = t._data + if t.is_leaf(): + return (False, None) + if t.is_2_node(): + p, a, q = data + if d < a: + t = p + elif d == a: + return (True, a) + else: + t = q + elif t.is_3_node(): + p, a, q, b, r = data + if d < a: + t = p + elif d == a: + return (True, a) + elif d < b: + t = q + elif d == b: + return (True, b) + else: + t = r + + def __iter__(self) -> Iterator: + if self.is_leaf(): + return + yield from self._data[0] + yield self._data[1] + yield from self._data[2] + if self.is_3_node(): + yield self._data[3] + yield from self._data[4] + + def __reversed__(self) -> Iterator: + if self.is_leaf(): + return + if self.is_3_node(): + yield from reversed(self._data[4]) + yield self._data[3] + yield from reversed(self._data[2]) + yield self._data[1] + yield from reversed(self._data[0]) def __len__(self) -> int: - return len(self._dictionary) + if self.is_leaf(): + return 0 + if self.is_2_node(): + return len(self._data[0]) + 1 + len(self._data[2]) + if self.is_3_node(): + return ( + len(self._data[0]) + + 1 + + len(self._data[2]) + + 1 + + len(self._data[4]) + ) + raise ValueError('Invalid 2-3 tree') + + def _insert(self, key) -> '_Tree23': + data = self._data + if self.is_leaf(): + return _Tree23(('up', _leaf_23_tree, key, _leaf_23_tree)) + if self.is_2_node(): + p, a, q = data + # print(key, a) + if key < a: + p_ = p._insert(key) + return _Tree23((p_, a, q))._insert_upwards_phase() + if key == a: + return _Tree23((p, key, q)) + q_ = q._insert(key) + return _Tree23((p, a, q_))._insert_upwards_phase() + if self.is_3_node(): + l, X, m, Y, r = data + if key < X: + return _Tree23( + (l._insert(key), X, m, Y, r) + )._insert_upwards_phase() + if key == X: + return _Tree23((l, key, m, Y, r)) + if key < Y: + return _Tree23( + (l, X, m._insert(key), Y, r) + )._insert_upwards_phase() + if key == Y: + return _Tree23((l, X, m, key, r)) + return _Tree23( + (l, X, m, Y, r._insert(key)) + )._insert_upwards_phase() + raise ValueError('Invalid 2-3 tree') + + def _insert_upwards_phase(self) -> '_Tree23': + if self.is_2_node(): + q, X, r = self._data + if q._is_kicked_up_node(): + # 2-node upstairs, kicked up node on left + _, l, w, m = q._data + return _Tree23((l, w, m, X, r)) + if r._is_kicked_up_node(): + # 2-node upstairs, kicked up node on right + _, m, w, r = r._data + l = q + return _Tree23((l, X, m, w, r)) + return self + if self.is_3_node(): + a, X, c, Y, d = self._data + if a._is_kicked_up_node(): + _, a, w, b = a._data + return _Tree23( + ('up', _Tree23((a, w, b)), X, _Tree23((c, Y, d))) + ) + if c._is_kicked_up_node(): + _, b, w, c = c._data + return _Tree23( + ('up', _Tree23((a, X, b)), w, _Tree23((c, Y, d))) + ) + if d._is_kicked_up_node(): + b = c + _, c, w, d = d._data + return _Tree23( + ('up', _Tree23((a, X, b)), Y, _Tree23((c, w, d))) + ) + return self + + def insert(self, key) -> '_Tree23': + """Insert key into the tree and return a new tree. + + This method should only be called on the root of a tree.""" + + tree = self._insert(key) + if tree._is_kicked_up_node(): + return _Tree23(tree._data[1:]) + return tree + + def _delete(self, key) -> '_Tree23': + data = self._data + if self.is_leaf(): + return _leaf_23_tree + if self.is_2_node(): + p, a, q = data + if key < a: + p_ = p._delete(key) + return _Tree23((p_, a, q))._delete_upwards_phase() + if key == a: + if self._is_2_node_terminal(): + return _Tree23((p, self.__hole, q))._delete_upwards_phase() + pred = p.max() + return _Tree23( + (p._delete(pred), pred, q) + )._delete_upwards_phase() + q_ = q._delete(key) + return _Tree23((p, a, q_))._delete_upwards_phase() + if self.is_3_node(): + l, X, m, Y, r = data + if key < X: + return _Tree23( + (l._delete(key), X, m, Y, r) + )._delete_upwards_phase() + if key == X: + if self._is_3_node_terminal(): + return _Tree23( + (l, self.__hole, m, Y, r) + )._delete_upwards_phase() + pred = l.max() + return _Tree23( + (l._delete(pred), pred, m, Y, r) + )._delete_upwards_phase() + if key < Y: + return _Tree23( + (l, X, m._delete(key), Y, r) + )._delete_upwards_phase() + if key == Y: + if self._is_3_node_terminal(): + return _Tree23( + (l, X, m, self.__hole, r) + )._delete_upwards_phase() + pred = m.max() + return _Tree23( + (l, X, m._delete(pred), pred, r) + )._delete_upwards_phase() + return _Tree23( + (l, X, m, Y, r._delete(key)) + )._delete_upwards_phase() + raise ValueError('Invalid 2-3 tree') + + def _delete_upwards_phase(self) -> '_Tree23': + if self.is_3_node(): + w, x, alpha, y, d = self._data + if self._is_3_node_terminal(): + if x is self.__hole: + return _Tree23((_leaf_23_tree, y, _leaf_23_tree)) + if y is self.__hole: + return _Tree23((_leaf_23_tree, x, _leaf_23_tree)) + if w._is_hole_node(): + a = w._data[1] + if alpha.is_2_node(): + z = y + b, y, c = alpha._data + if all( + map( + lambda h: h == d.height - 1, + (a.height, b.height, c.height), + ) + ): + # 3-node parent, 2-node sibling, hole on left, height condition + return _Tree23((_Tree23((a, x, b, y, c)), z, d)) + if alpha.is_3_node(): + w = x + z = y + e = d + b, x, c, y, d = alpha._data + if all( + map( + lambda h: h == e.height - 1, + (a.height, b.height, c.height, d.height), + ) + ): + # 3-node parent, 3-parent sibling in middle, hole on left, right condition + return _Tree23( + (_Tree23((a, w, b)), x, _Tree23((c, y, d)), z, e) + ) + if alpha._is_hole_node(): + if w.is_2_node(): + z = y + y = x + a, x, b = w._data + c = alpha._data[1] + if all( + map( + lambda h: h == d.height - 1, + (a.height, b.height, c.height), + ) + ): + # 3-node parent, 2-node sibling on left, hole in middle, height condition + return _Tree23((_Tree23((a, x, b, y, c)), z, d)) + if w.is_3_node(): + z = y + y = x + a, w, b, x, c = w._data + e = d + d = alpha._data[1] + if all( + map( + lambda h: h == e.height - 1, + (a.height, b.height, c.height, d.height), + ) + ): + # 3-node parent, 3-node sibling on left, hole in middle, height condition + return _Tree23( + (_Tree23((a, w, b)), x, _Tree23((c, y, d)), z, e) + ) + if d.is_2_node(): + a = w + b = alpha._data[1] + c, z, d = d._data + if all( + map( + lambda h: h == a.height - 1, + (b.height, c.height, d.height), + ) + ): + return _Tree23((a, x, _Tree23((b, y, c, z, d)))) + if d.is_3_node(): + a = w + w = x + b = alpha._data[1] + x = y + c, y, d, z, e = d._data + if all( + map( + lambda h: h == a.height - 1, + (b.height, c.height, d.height, e.height), + ) + ): + # 3-node parent, 3-node sibling on right, hole in middle, height condition + return _Tree23( + (a, w, _Tree23((b, x, c)), y, _Tree23((d, z, e))) + ) + if d._is_hole_node(): + a = w + if alpha.is_2_node(): + z = y + b, y, c = alpha._data + d = d._data[1] + if all( + map( + lambda h: h == a.height - 1, + (b.height, c.height, d.height), + ) + ): + # 3-node parent, 2-node sibling in middle, hole on right, height condition + return _Tree23((a, x, _Tree23((b, y, c, z, d)))) + if alpha.is_3_node(): + w = x + z = y + e = d._data[1] + b, x, c, y, d = alpha._data + if all( + map( + lambda h: h == a.height - 1, + (b.height, c.height, d.height, e.height), + ) + ): + # 3-node parent, 3-node sibling in middle, hole on right, height condition + return _Tree23( + (a, w, _Tree23((b, x, c)), y, _Tree23((d, z, e))) + ) + # 3-node that either has no data or children, or has bad heights + return self + if self.is_2_node(): + left, x, right = self._data + if self._is_2_node_terminal() and x is self.__hole: + return _Tree23((x, _leaf_23_tree)) + if left._is_hole_node(): + if right.is_2_node(): + # 2-node parent, 2-node sibling, hole on left + l = left._data[1] + m, y, r = right._data + return _Tree23((self.__hole, _Tree23((l, x, m, y, r)))) + if right.is_3_node(): + # 2-node parent, 3-node sibling, hole on left + a = left._data[1] + b, y, c, z, d = right._data + return _Tree23((_Tree23((a, x, b)), y, _Tree23((c, z, d)))) + if right._is_hole_node(): + if left.is_2_node(): + # 2-node parent, 2-node sibling, hole on right + r = right._data[1] + y = x + l, x, m = left._data + return _Tree23((self.__hole, _Tree23((l, x, m, y, r)))) + if left.is_3_node(): + # 2-node parent, 3-node sibling, hole on right + z = x + d = right._data[1] + a, x, b, y, c = left._data + return _Tree23((_Tree23((a, x, b)), y, _Tree23((c, z, d)))) + # no hole in key or children + return self + raise RuntimeError(f'Missing case in delete for {self!r}') + + def delete(self, key) -> '_Tree23': + tree = self._delete(key) + if tree._is_hole_node(): + return tree._data[1] + return tree + + def max(self, default: object = None) -> Any: + tree = self + while not tree.is_leaf(): + if tree.is_2_node(): + if tree._is_2_node_terminal(): + return tree._data[1] + tree = tree._data[2] + if tree.is_3_node(): + if tree._is_3_node_terminal(): + return tree._data[3] + tree = tree._data[4] + if default is None: + raise ValueError('Empty 2-3 tree has no max') + return default + + __hole = _Tree23Hole() + + def is_leaf(self) -> bool: + return len(self._data) == 0 + + def is_2_node(self) -> bool: + return len(self._data) == 3 + + def is_3_node(self) -> bool: + return len(self._data) == 5 + + def _is_kicked_up_node(self) -> bool: + return len(self._data) == 4 and self._data[0] == 'up' + + def _is_3_node_terminal(self) -> bool: + return all( + map( + lambda t: t.is_leaf(), + (self._data[0], self._data[2], self._data[4]), + ) + ) + + def _is_2_node_terminal(self) -> bool: + return all(map(lambda t: t.is_leaf(), (self._data[0], self._data[2]))) + + def _is_hole_node(self) -> bool: + return len(self._data) == 2 and self._data[0] is self.__hole + + def __repr__(self) -> str: + return f'{type(self).__qualname__}({self._data!r})' + + +_leaf_23_tree = _Tree23(()) diff --git a/concat/parse.py b/concat/parse.py index a993ea5c..6131c15a 100644 --- a/concat/parse.py +++ b/concat/parse.py @@ -29,19 +29,18 @@ def word_ext(parsers): import abc import operator from typing import ( + Any, + Generator, Iterable, Iterator, + List, Optional, - Type, - TypeVar, - Any, Sequence, - Tuple, - Dict, - Generator, - List, - Callable, TYPE_CHECKING, + Tuple, + Type, + TypeVar, + Union, ) import concat.lex import concat.astutils @@ -56,11 +55,15 @@ def word_ext(parsers): class Node(abc.ABC): - @abc.abstractmethod def __init__(self): self.location = (0, 0) self.children: Iterable[Node] = [] + def assert_no_parse_errors(self) -> None: + failures = list(self.parsing_failures) + if failures: + raise concat.parser_combinators.ParseError(failures) + @property def parsing_failures( self, @@ -212,6 +215,9 @@ def __str__(self) -> str: ) return '(' + input_stack_type + ' '.join(map(str, self.children)) + ')' + def __repr__(self) -> str: + return f'{type(self).__qualname__}(children={self.children!r}, location={self.location!r}, input_stack_type={self.input_stack_type!r})' + class NameWordNode(WordNode): def __init__(self, name: 'concat.lex.Token'): @@ -260,6 +266,9 @@ def parsing_failures( assert self.result.failures is not None yield self.result.failures + def __repr__(self) -> str: + return f'{type(self).__qualname__}(result={self.result!r})' + class BytesWordNode(WordNode): def __init__(self, bytes: 'concat.lex.Token'): @@ -296,6 +305,7 @@ class FuncdefStatementNode(StatementNode): def __init__( self, name: 'Token', + type_parameters: Sequence[Tuple['Token', Node]], decorators: Iterable[WordNode], annotation: Optional[Iterable[WordNode]], body: 'WordsOrStatements', @@ -305,25 +315,21 @@ def __init__( super().__init__() self.location = location self.name = name.value + self.type_parameters = type_parameters self.decorators = decorators self.annotation = annotation self.body = body + self.stack_effect = stack_effect self.children = [ + *self.type_parameters, *self.decorators, *(self.annotation or []), + self.stack_effect, *self.body, ] - self.stack_effect = stack_effect def __repr__(self) -> str: - return 'FuncdefStatementNode(decorators={!r}, name={!r}, annotation={!r}, body={!r}, stack_effect={!r}, location={!r})'.format( - self.decorators, - self.name, - self.annotation, - self.body, - self.stack_effect, - self.location, - ) + return f'FuncdefStatementNode(decorators={self.decorators!r}, name={self.name!r}, type_parameters={self.type_parameters!r}, annotation={self.annotation!r}, body={self.body!r}, stack_effect={self.stack_effect!r}, location={self.location!r})' class FromImportStatementNode(ImportStatementNode): @@ -352,6 +358,8 @@ def __init__( decorators: Optional['Words'] = None, bases: Iterable['Words'] = (), keyword_args: Iterable[Tuple[str, WordNode]] = (), + type_parameters: Iterable[Node] = (), + is_variadic: bool = False, ): super().__init__() self.location = location @@ -360,6 +368,18 @@ def __init__( self.decorators = [] if decorators is None else decorators self.bases = bases self.keyword_args = keyword_args + self.type_parameters = type_parameters + self.is_variadic = is_variadic + + +class PragmaNode(Node): + def __init__( + self, location: 'Location', pragma_name: str, args: Sequence[str] + ) -> None: + super().__init__() + self.location = location + self.pragma = pragma_name + self.args = args def token(typ: str) -> concat.parser_combinators.Parser: @@ -382,9 +402,7 @@ def top_level_parser() -> Generator[ newline = token('NEWLINE') statement = parsers['statement'] word = parsers['word'] - children = yield recover( - (word | statement | newline).many(), skip_until(token('ENDMARKER')) - ).map(lambda w: [ParseError(w[1])] if isinstance(w, tuple) else w) + children = yield (word | statement | newline).commit().many() children = [ child for child in children @@ -406,10 +424,6 @@ def top_level_parser() -> Generator[ # statement = import statement ; parsers['statement'] = parsers.ref_parser('import-statement') - ImportStatementParserGenerator = Generator[ - concat.parser_combinators.Parser, Any, ImportStatementNode - ] - # This parses one of many types of word. # The specific word node is returned. # word = @@ -434,10 +448,10 @@ def top_level_parser() -> Generator[ @concat.parser_combinators.generate def quote_word_contents() -> Generator: - if 'type-sequence' in parsers: - input_stack_type_parser = parsers['type-sequence'] << token( - 'COLON' - ) + if 'stack-effect-type-sequence' in parsers: + input_stack_type_parser = parsers[ + 'stack-effect-type-sequence' + ] << token('COLON') input_stack_type = yield input_stack_type_parser.optional() else: input_stack_type = None @@ -554,26 +568,49 @@ def word_list_parser() -> Generator: ) # This parses a function definition. - # funcdef statement = DEF, NAME, stack effect, decorator*, + # funcdef statement = DEF, NAME, [ type parameters ], stack effect, decorator*, # [ annotation ], COLON, suite ; # decorator = AT, word ; # annotation = RARROW, word* ; # suite = NEWLINE, INDENT, (word | statement, NEWLINE)+, DEDENT | statement # | word+ ; + # type parameters = "[", [ type parameter ], + # (",", type parameter)*, [ "," ], "]" ; + # type parameter = NAME, COLON, type ; # The stack effect syntax is defined within the typecheck module. @concat.parser_combinators.generate def funcdef_statement_parser() -> Generator: location = (yield token('DEF')).start name = yield token('NAME') + type_params = (yield type_parameters.optional()) or [] effect_ast = yield parsers['stack-effect-type'] decorators = yield decorator.many() annotation = yield annotation_parser.optional() yield token('COLON') body = yield suite return FuncdefStatementNode( - name, decorators, annotation, body, location, effect_ast + name, + type_params, + decorators, + annotation, + body, + location, + effect_ast, ) + @concat.parser_combinators.generate + def type_parameter() -> Generator: + name = yield token('NAME') + yield token('COLON') + ty = yield parsers['type'] + return (name, ty) + + type_parameters = bracketed( + token('LSQB'), + type_parameter.sep_by(token('COMMA')) << token('COMMA').optional(), + token('RQSB'), + ).map(handle_recovery) + parsers['funcdef-statement'] = funcdef_statement_parser.desc( 'funcdef statement' ) @@ -592,7 +629,7 @@ def suite(): statement = concat.parser_combinators.seq(parsers['statement']) block_content = ( parsers['word'] << token('NEWLINE').optional() - | parsers['statement'] << token('NEWLINE') + | parsers['statement'] << token('NEWLINE').optional() ).at_least(1) indented_block = token('NEWLINE').optional() >> bracketed( token('INDENT'), block_content, token('DEDENT') @@ -654,15 +691,47 @@ def from_import_star_statement_parser() -> Generator: parsers['import-statement'] |= from_import_star_statement_parser - # This parses a class definition statement. - # classdef statement = CLASS, NAME, decorator*, [ bases ], keyword arg*, - # COLON, suite ; - # bases = tuple word ; - # keyword arg = NAME, EQUAL, word ; @concat.parser_combinators.generate('classdef statement') def classdef_statement_parser(): + """This parses a class definition statement. + + classdef statement = CLASS, NAME, + [ LSQB, ((type variable, (COMMA, type variable)*, [ COMMA ]) | (type variable, NAME=...)), RSQB) ], + decorator*, [ bases ], keyword arg*, + COLON, suite ; + bases = tuple word ; + keyword arg = NAME, EQUAL, word ;""" location = (yield token('CLASS')).start name_token = yield token('NAME') + is_variadic = False + + def ellispis_verify( + tok: concat.lex.Token, + ) -> concat.parser_combinators.Parser[concat.lex.Token, Any]: + nonlocal is_variadic + + if tok.value == '...': + is_variadic = True + return concat.parser_combinators.success(None) + return concat.parser_combinators.fail('a literal ellispis (...)') + + ellispis_parser = token('NAME').bind(ellispis_verify) + type_parameters = ( + yield bracketed( + token('LSQB'), + ( + concat.parser_combinators.seq(parsers['type-variable']) + << ellispis_parser + ) + | ( + parsers['type-variable'].sep_by(token('COMMA')) + << token('COMMA').optional() + ), + token('RSQB'), + ) + .map(handle_recovery) + .optional() + ) decorators = yield decorator.many() bases_list = yield bases.optional() keyword_args = yield keyword_arg.map(tuple).many() @@ -675,6 +744,8 @@ def classdef_statement_parser(): decorators, bases_list, keyword_args, + type_parameters=type_parameters or [], + is_variadic=is_variadic, ) parsers['classdef-statement'] = classdef_statement_parser @@ -688,6 +759,24 @@ def classdef_statement_parser(): parsers.ref_parser('word'), ) + @concat.parser_combinators.generate('internal pragma') + def pragma_parser() -> Generator: + """This parses a pragma for internal use. + + pragma = EXCLAMATIONMARK, @, @, qualified name+ + qualified name = module""" + location = (yield token('EXCLAMATIONMARK')).start + for _ in range(2): + name_token = yield token('NAME') + if name_token.value != '@': + return concat.parser_combinators.fail('a literal at sign (@)') + pragma_name = yield module + args = yield module.many() + return PragmaNode(location, pragma_name, args) + + parsers['pragma'] = pragma_parser + parsers['statement'] |= parsers.ref_parser('pragma') + parsers['word'] |= parsers.ref_parser('cast-word') @concat.parser_combinators.generate @@ -729,3 +818,17 @@ def freeze_word_parser() -> Generator: # parsers['word'] |= parsers['freeze-word'].should_fail( # 'not a freeze word, which has polymorphic type' # ) + + +def handle_recovery( + x: Union[ + Sequence[Node], Tuple[Any, concat.parser_combinators.Result[Any]], + ] +) -> Sequence[Node]: + if ( + isinstance(x, tuple) + and len(x) > 1 + and isinstance(x[1], concat.parser_combinators.Result) + ): + return [ParseError(x[1])] + return x diff --git a/concat/parser_combinators/__init__.py b/concat/parser_combinators/__init__.py index ea257d4b..ef18190f 100644 --- a/concat/parser_combinators/__init__.py +++ b/concat/parser_combinators/__init__.py @@ -92,6 +92,7 @@ def __init__( current_index: int, is_success: bool, failures: Optional[FailureTree] = None, + is_committed: bool = False, ) -> None: self.output = output self.current_index = current_index @@ -101,9 +102,10 @@ def __init__( ) self.is_success = is_success self.failures = failures + self.is_committed = is_committed def __repr__(self) -> str: - return f'{type(self).__qualname__}({self.output!r}, {self.current_index!r}, {self.is_success!r}, {self.failures!r})' + return f'{type(self).__qualname__}({self.output!r}, {self.current_index!r}, {self.is_success!r}, {self.failures!r}, is_committed={self.is_committed!r})' def __eq__(self, other: object) -> bool: if isinstance(other, Result): @@ -112,17 +114,25 @@ def __eq__(self, other: object) -> bool: self.current_index, self.is_success, self.failures, + self.is_committed, ) == ( other.output, other.current_index, other.is_success, other.failures, + other.is_committed, ) return NotImplemented def __hash__(self) -> int: return hash( - (self.output, self.current_index, self.is_success, self.failures) + ( + self.output, + self.current_index, + self.is_success, + self.failures, + self.is_committed, + ) ) @@ -142,29 +152,37 @@ def new_parser( stream: Sequence[_T_contra], index: int ) -> Result[Union[_U_co, _V]]: left_result = self(stream, index) - if left_result.is_success: + if ( + left_result.is_success + or left_result.is_committed + and left_result.current_index > index + ): return left_result right_result = other(stream, index) new_failure: Optional[FailureTree] if right_result.is_success: if left_result.current_index > right_result.current_index: - if ( - left_result.failures is not None - and right_result.failures is not None - ): + if right_result.failures is not None: + assert left_result.failures is not None new_failure = FailureTree( f'{left_result.failures.expected} or {right_result.failures.expected}', left_result.failures.furthest_index, left_result.failures.children + right_result.failures.children, ) - return Result( - right_result.output, - right_result.current_index, - True, - new_failure, - ) - raise Exception('todo') + else: + new_failure = left_result.failures + return Result( + right_result.output, + right_result.current_index, + True, + new_failure, + ) + return right_result + if ( + right_result.is_committed + and right_result.current_index > index + ): return right_result assert left_result.failures is not None assert right_result.failures is not None @@ -321,14 +339,30 @@ def new_parser() -> Generator: return new_parser def optional(self) -> 'Parser[_T_contra, Optional[_U_co]]': + return self | success(None) + + # See + # https://elixirforum.com/t/parser-combinators-how-to-know-when-many-should-return-an-error/46048/12 + # on the problem this solves. + def commit(self) -> 'Parser[_T_contra, _U_co]': + """Do not try alteratives adjacent to this parser if it consumes input before failure. + + This is useful with combinators like many(): parser.many() succeeds + even if `parser` fails in a way that you know is an error and should be + reported for a better error message.""" + @Parser def new_parser( stream: Sequence[_T_contra], index: int - ) -> Result[Optional[_U_co]]: + ) -> Result[_U_co]: result = self(stream, index) - if result.is_success: - return result - return Result(None, index, True, result.failures) + return Result( + result.output, + result.current_index, + result.is_success, + result.failures, + is_committed=True, + ) return new_parser diff --git a/concat/poly-subsumption.md b/concat/poly-subsumption.md new file mode 100644 index 00000000..6894b24f --- /dev/null +++ b/concat/poly-subsumption.md @@ -0,0 +1,55 @@ +Subsumption of a polymorphic type by another type may involve instantiation and +reordering of type variables. Subsumption can be checked using +"regeneralization." + +I think a correct(-ish?) way of doing regeneralization in Concat is the +following (substitution notation might be backwards): + +``` + t[fresh(a+)/a+] <: s with b+ rigid + b+ all not in ftv(forall a+. t) +------------------------------------------------------ [FORALL<:FORALL] + forall a+. t <: forall b+. s +``` + +In the `HMV_InstG` rule of [Visible Type Application (Extended +version)](https://www.seas.upenn.edu/~sweirich/papers/type-app-extended.pdf), in +Fig. 4, there's a condition that the bs are not free in `forall a.... t`. + +`FORALL<:FORALL` means that `forall a. int <: forall a, b. int`. But `forall (a : +Individual). a /<: forall (b : Item). b` because we would have to solve +`fresh(a) <: b`, which requires the substitution `[b/a]` because the kind of +`b` >= the kind of `a`. But we made `b` rigid! + +``` + (s can be generic, but not a forall) + forall a+, b*. t : Generic[k+, l*] + s : Generic[m*] + l* :> m* + forall b*. t[fresh(a+)/a+] <: s +---------------------------------------- [FORALL<:INST] + forall a+, b*. t <: s + + (b is a unification variable) + forall a+. t : Generic[k+] + b : l + Generic[k+] <: l +-------------------------------------- [FORALL<:VAR] +forall a+. t <: b --> [b/forall a+. t] +``` + +The following might not make sense: + +``` +(s can be generic, but not a forall) + forall a+. t : Generic[k+] + s : l + Generic[k+] <: l + b+ = fresh(a+) +t[b+/a+] <: s[b+] (type application) +------------------------------------ [FORALL<:KIND-SUB] + forall a+. t <: s +``` + +Other papers mentioning regeneralization: +- [Guarded impredicative polymorphism](https://www.microsoft.com/en-us/research/uploads/prod/2017/07/impred-pldi18-submission.pdf) diff --git a/concat/stdlib/continuation.cati b/concat/stdlib/continuation.cati new file mode 100644 index 00000000..c2835f9c --- /dev/null +++ b/concat/stdlib/continuation.cati @@ -0,0 +1,20 @@ +class ContinuationMonad[`r, `a]: + () + +def call_with_current_continuation(*s f:forall *t. (*t g:forall *u. (*u x:`a -- *u cont1:ContinuationMonad[`r, `b]) -- *t cont2:ContinuationMonad[`r, `a]) -- *s cont:ContinuationMonad[`r, `a]): + () + +def eval_cont(*s cont:ContinuationMonad[`r, `r] -- *s res:`r): + () + +def cont_pure(*s x:`a -- *s cont:ContinuationMonad[`r, `a]): + () + +def map_cont(*s cont:ContinuationMonad[`r, `a] f:forall *t. (*t x:`a -- *t y:`b) -- *s cont2:ContinuationMonad[`r, `b]): + () + +def bind_cont(*s cont:ContinuationMonad[`r, `a] f:forall *t. (*t x:`a -- *t cont:ContinuationMonad[`r, `b]) -- *s cont2:ContinuationMonad[`r, `b]): + () + +def cont_from_cps(*s cps:forall *t. (*t k:forall *u. (*u x:`a -- *u res:`r) -- *t res:`r) -- *s cont:ContinuationMonad[`r, `a]): + () diff --git a/concat/stdlib/continuation.py b/concat/stdlib/continuation.py index 6eed251f..23933903 100644 --- a/concat/stdlib/continuation.py +++ b/concat/stdlib/continuation.py @@ -1,13 +1,5 @@ from concat.common_types import ConcatFunction -from concat.typecheck.types import ( - ForAll, - IndividualVariable, - SequenceVariable, - StackEffect, - TypeSequence, - continuation_monad_type, -) -from typing import Callable, Generic, List, NoReturn, Type, TypeVar, cast +from typing import Any, Callable, Generic, List, NoReturn, Type, TypeVar, cast _A = TypeVar('_A', covariant=True) @@ -90,116 +82,6 @@ def compose( # Concat API -_s, _t, _u = SequenceVariable(), SequenceVariable(), SequenceVariable() -_a, _b, _r = IndividualVariable(), IndividualVariable(), IndividualVariable() - -globals()['@@types'] = { - 'ContinuationMonad': continuation_monad_type, - 'call_with_current_continuation': ForAll( - [_s, _r, _a, _b], - StackEffect( - TypeSequence( - [ - _s, - ForAll( - [_t], - StackEffect( - TypeSequence( - [ - _t, - ForAll( - [_u], - StackEffect( - TypeSequence([_u, _a]), - TypeSequence( - [ - _u, - continuation_monad_type[ - _r, _b - ], - ] - ), - ), - ), - ] - ), - TypeSequence( - [_t, continuation_monad_type[_r, _a]] - ), - ), - ), - ] - ), - TypeSequence([_s, continuation_monad_type[_r, _a]]), - ), - ), - 'eval_cont': ForAll( - [_s, _r], - StackEffect( - TypeSequence([_s, continuation_monad_type[_r, _r]]), - TypeSequence([_s, _r]), - ), - ), - 'cont_pure': ForAll( - [_s, _a, _r], - StackEffect( - TypeSequence([_s, _a]), - TypeSequence([_s, continuation_monad_type[_r, _a]]), - ), - ), - 'bind_cont': ForAll( - [_s, _r, _a, _b], - StackEffect( - TypeSequence( - [ - _s, - continuation_monad_type[_r, _a], - ForAll( - [_t], - StackEffect( - TypeSequence([_t, _a]), - TypeSequence( - [_t, continuation_monad_type[_r, _b]] - ), - ), - ), - ] - ), - TypeSequence([_s, continuation_monad_type[_r, _b]]), - ), - ), - 'cont_from_cps': ForAll( - [_s, _t, _u, _a, _r], - StackEffect( - TypeSequence( - [ - _s, - ForAll( - [_t], - StackEffect( - TypeSequence( - [ - _t, - ForAll( - [_u], - StackEffect( - TypeSequence([_u, _a]), - TypeSequence([_u, _r]), - ), - ), - ] - ), - TypeSequence([_t, _r]), - ), - ), - ] - ), - TypeSequence([_s, continuation_monad_type[_r, _a]]), - ), - ), -} - - def call_with_current_continuation( stack: List[object], stash: List[object] ) -> None: @@ -235,6 +117,21 @@ def cont_pure(stack: List[object], _: List[object]) -> None: stack.append(result) +def map_cont(stack: List[Any], stash: List[Any]) -> None: + f, cont = ( + cast(ConcatFunction, stack.pop()), + cast(ContinuationMonad, stack.pop()), + ) + + def python_function(b: Any) -> Any: + stack.append(b) + f(stack, stash) + return stack.pop() + + result = cont.map(python_function) + stack.append(result) + + def bind_cont(stack: List[object], stash: List[object]) -> None: f, cont = ( cast(ConcatFunction, stack.pop()), @@ -247,7 +144,7 @@ def python_function(b: _B) -> ContinuationMonad[_R, _C]: f(stack, stash) return cast(ContinuationMonad[_R, _C], stack.pop()) - result = cont.bind(python_function) + result: ContinuationMonad = cont.bind(python_function) stack.append(result) @@ -264,5 +161,5 @@ def concat_k(stack: List[object], _: List[object]) -> None: concat_run(stack, stash) return cast(_R, stack.pop()) - result = ContinuationMonad(python_run) + result: ContinuationMonad = ContinuationMonad(python_run) stack.append(result) diff --git a/concat/stdlib/pyinterop/__init__.cati b/concat/stdlib/pyinterop/__init__.cati new file mode 100644 index 00000000..6f65d92a --- /dev/null +++ b/concat/stdlib/pyinterop/__init__.cati @@ -0,0 +1,17 @@ +def getitem(*stack_type_var obj:subscriptable[`x, `y] index:`x -- *stack_type_var res:`y): + () + +def to_dict(*stack_type_var it:Optional[iterable[tuple[`x, `y]]] -- *stack_type_var d:dict[`x, `y]): + () + +def to_str(*stack_type_var errors:object encoding:object obj:object -- *stack_type_var string:str): + () + +def to_py_function(*rest_var f:(*rest_var_2 -- *rest_var_3) -- *rest_var py_f:py_function[*any_args, `any_ret]): + () + +def to_slice(*stack_type_var step:Optional[`x] stop:Optional[`y] start:Optional[`z] -- *stack_type_var slice_:slice[`z, `y, `x]): + () + +def map(*rest_var f:(*rest_var x:`y -- *rest_var fx:`z) it:iterable[`y] -- *rest_var fit:iterable[`z]): + () diff --git a/concat/stdlib/pyinterop/__init__.py b/concat/stdlib/pyinterop/__init__.py index 71ebc7cc..a742afae 100644 --- a/concat/stdlib/pyinterop/__init__.py +++ b/concat/stdlib/pyinterop/__init__.py @@ -1,21 +1,6 @@ """Concat-Python interoperation helpers.""" +from concat.common_types import ConcatFunction import concat.stdlib.ski -from concat.typecheck.types import ( - ForAll, - IndividualVariable, - SequenceVariable, - StackEffect, - TypeSequence, - dict_type, - iterable_type, - object_type, - optional_type, - py_function_type, - slice_type, - str_type, - subscriptable_type, - tuple_type, -) import builtins import importlib import os @@ -36,63 +21,6 @@ ) -_stack_type_var = SequenceVariable() -_rest_var = SequenceVariable() -_rest_var_2 = SequenceVariable() -_rest_var_3 = SequenceVariable() -_x = IndividualVariable() -_y = IndividualVariable() -_z = IndividualVariable() -globals()['@@types'] = { - 'getitem': ForAll( - [_stack_type_var, _x, _y], - StackEffect( - TypeSequence([_stack_type_var, subscriptable_type[_x, _y], _x,]), - TypeSequence([_stack_type_var, _y]), - ), - ), - 'to_dict': ForAll( - [_stack_type_var, _x, _y], - StackEffect( - TypeSequence( - [ - _stack_type_var, - optional_type[ - iterable_type[tuple_type[TypeSequence([_x, _y]),],], - ], - ] - ), - TypeSequence([_stack_type_var, dict_type[_x, _y]]), - ), - ), - 'to_slice': ForAll( - [_stack_type_var, _x, _y, _z], - StackEffect( - TypeSequence( - [ - _stack_type_var, - optional_type[_x,], - optional_type[_y,], - optional_type[_z,], - ] - ), - TypeSequence([_stack_type_var, slice_type[_z, _y, _x]]), - ), - ), - 'to_str': StackEffect( - TypeSequence([_stack_type_var, object_type, object_type, object_type]), - TypeSequence([_stack_type_var, str_type]), - ), - 'to_py_function': ForAll( - [_rest_var, _rest_var_2, _rest_var_3], - StackEffect( - [_rest_var, StackEffect([_rest_var_2], [_rest_var_3])], - [_rest_var, py_function_type], - ), - ), -} - - def to_py_function(stack: List[object], stash: List[object]) -> None: func = cast(Callable[[List[object], List[object]], None], stack.pop()) @@ -339,6 +267,19 @@ def import_advanced(stack: List[object], stash: List[object]) -> None: ) +def map(stack: List[object], stash: List[object]) -> None: + 'f iterable -- map(f, iterable)' + iterable = cast(Iterable[object], stack.pop()) + f = cast(ConcatFunction, stack.pop()) + + def python_f(x: object) -> object: + stack.append(x) + f(stack, stash) + return stack.pop() + + stack.append(builtins.map(python_f, iterable)) + + def open(stack: List[object], stash: List[object]) -> None: 'kwargs -- open(**kwargs)' # open has a lot of arguments stack.append(builtins.open(**cast(Mapping[str, Any], stack.pop()))) diff --git a/concat/stdlib/repl.py b/concat/stdlib/repl.py index 71b9e383..176c1be2 100644 --- a/concat/stdlib/repl.py +++ b/concat/stdlib/repl.py @@ -77,8 +77,10 @@ def read_form(stack: List[object], stash: List[object]) -> None: string = _read_until_complete_line() try: ast = _parse('$(' + string + ')') + ast.assert_no_parse_errors() except concat.parser_combinators.ParseError: ast = _parse(string) + ast.assert_no_parse_errors() concat.typecheck.check(caller_globals['@@extra_env'], ast.children) # I don't think it makes sense for us to get multiple children if what # we got was a statement, so we assert. @@ -149,7 +151,7 @@ def show_var(stack: List[object], stash: List[object]): 'visible_vars': set(), 'show_var': show_var, 'concat': concat, - '@@extra_env': concat.typecheck.Environment(), + '@@extra_env': concat.typecheck.load_builtins_and_preamble(), **initial_globals, } locals: Dict[str, object] = {} diff --git a/concat/tests/fixtures/imported_module.cati b/concat/tests/fixtures/imported_module.cati new file mode 100644 index 00000000..e69de29b diff --git a/concat/tests/stdlib/test_repl.py b/concat/tests/stdlib/test_repl.py index e30bccec..e5cb5eae 100644 --- a/concat/tests/stdlib/test_repl.py +++ b/concat/tests/stdlib/test_repl.py @@ -2,7 +2,7 @@ import io import sys import contextlib -import concat.parse +import concat.parser_combinators import concat.typecheck from concat.typecheck.types import SequenceVariable, StackEffect, TypeSequence import concat.stdlib.types @@ -62,5 +62,5 @@ def test_catch_parse_errors(self): with replace_stdin(io.StringIO('drg nytu y,i.')): try: concat.stdlib.repl.repl([], []) - except concat.parse.ParseError: + except concat.parser_combinators.ParseError: self.fail('repl must recover from parser failures') diff --git a/concat/tests/strategies.py b/concat/tests/strategies.py index 13399d20..12a6bcdb 100644 --- a/concat/tests/strategies.py +++ b/concat/tests/strategies.py @@ -1,13 +1,18 @@ -from concat.lex import Token from concat.typecheck.types import ( + IndividualKind, IndividualType, - IndividualVariable, + ItemVariable, ObjectType, + PythonFunctionType, SequenceVariable, StackEffect, + StuckTypeApplication, TypeSequence, + no_return_type, + optional_type, + py_function_type, ) -from hypothesis.strategies import ( +from hypothesis.strategies import ( # type: ignore SearchStrategy, builds, dictionaries, @@ -18,21 +23,19 @@ recursive, register_type_strategy, text, + tuples, ) -from typing import ( - Iterable, - Sequence, - Type, -) +from typing import Type def _type_sequence_strategy( individual_type_strategy: SearchStrategy[IndividualType], + no_rest_var: bool = False, ) -> SearchStrategy[TypeSequence]: return builds( lambda maybe_seq_var, rest: TypeSequence(maybe_seq_var + rest), - lists(from_type(SequenceVariable), max_size=1), - lists(individual_type_strategy, max_size=10), + lists(from_type(SequenceVariable), max_size=0 if no_rest_var else 1), + lists(individual_type_strategy, max_size=5), ) @@ -43,28 +46,14 @@ def _object_type_strategy( builds( ObjectType, attributes=dictionaries(text(), individual_type_strategy), - nominal_supertypes=lists(individual_type_strategy), - _type_arguments=lists( - from_type(SequenceVariable) - | individual_type_strategy - | _type_sequence_strategy(individual_type_strategy) - ), _head=none(), - _other_kwargs=just({}), ), lambda children: builds( ObjectType, attributes=dictionaries(text(), individual_type_strategy), - nominal_supertypes=lists(individual_type_strategy), - _type_arguments=lists( - from_type(SequenceVariable) - | individual_type_strategy - | _type_sequence_strategy(individual_type_strategy) - ), _head=children, - _other_kwargs=just({}), ), - max_leaves=50, + max_leaves=10, ) @@ -81,7 +70,10 @@ def _mark_individual_type_strategy( _individual_type_strategy = recursive( _mark_individual_type_strategy( - from_type(IndividualVariable), IndividualVariable + builds(ItemVariable, just(IndividualKind)), ItemVariable + ) + | _mark_individual_type_strategy( + just(no_return_type), type(no_return_type) ), lambda children: _mark_individual_type_strategy( builds( @@ -93,12 +85,26 @@ def _mark_individual_type_strategy( ) | _mark_individual_type_strategy( _object_type_strategy(children), ObjectType + ) + | _mark_individual_type_strategy( + builds( + lambda args: py_function_type[args], + tuples( + _type_sequence_strategy(children, no_rest_var=True), children + ), + ), + PythonFunctionType, + ) + | _mark_individual_type_strategy( + builds(lambda args: optional_type[args], tuples(children),), + type(optional_type[ObjectType({}),]), ), max_leaves=50, ) for subclass in _individual_type_subclasses: - assert subclass in _individual_type_strategies, subclass + if subclass not in [StuckTypeApplication]: + assert subclass in _individual_type_strategies, subclass register_type_strategy(IndividualType, _individual_type_strategy) register_type_strategy( diff --git a/concat/tests/test_linked_list.py b/concat/tests/test_linked_list.py new file mode 100644 index 00000000..6a8c515b --- /dev/null +++ b/concat/tests/test_linked_list.py @@ -0,0 +1,85 @@ +from concat.linked_list import LinkedList, empty_list +from hypothesis import given +import hypothesis.strategies as st +from typing import Callable, List +import unittest + + +linked_lists = st.lists(st.integers()).map(LinkedList.from_iterable) + + +class TestMonoid(unittest.TestCase): + def test_empty(self) -> None: + self.assertEqual(0, len(empty_list)) + self.assertFalse(empty_list) + self.assertListEqual([], list(empty_list)) + + @given(st.lists(st.integers()), st.lists(st.integers())) + def test_add(self, a: List[int], b: List[int]) -> None: + self.assertListEqual( + a + b, + list(LinkedList.from_iterable(a) + LinkedList.from_iterable(b)), + ) + + @given(linked_lists, linked_lists, linked_lists) + def test_assoc( + self, a: LinkedList[int], b: LinkedList[int], c: LinkedList[int] + ) -> None: + self.assertEqual((a + b) + c, a + (b + c)) + + @given(linked_lists) + def test_id(self, a: LinkedList[int]) -> None: + self.assertEqual(a, a + empty_list) + self.assertEqual(a, empty_list + a) + + +predicates = st.functions( + like=lambda _: True, returns=st.booleans(), pure=True +) + + +class TestFilter(unittest.TestCase): + @given(predicates) + def test_empty(self, p: Callable[[int], bool]) -> None: + self.assertEqual(empty_list, empty_list.filter(p)) + + @given(linked_lists) + def test_remove_all(self, l: LinkedList[int]) -> None: + self.assertEqual(empty_list, l.filter(lambda _: False)) + + @given(linked_lists) + def test_keep_all(self, l: LinkedList[int]) -> None: + self.assertEqual(l, l.filter(lambda _: True)) + + @given(linked_lists, predicates) + def test_idempotency( + self, l: LinkedList[int], p: Callable[[int], bool] + ) -> None: + self.assertEqual(l.filter(p), l.filter(p).filter(p)) + + @given(linked_lists, predicates) + def test_excluded_middle( + self, l: LinkedList[int], p: Callable[[int], bool] + ) -> None: + self.assertSetEqual( + set(l), set(l.filter(p) + l.filter(lambda x: not p(x))) + ) + + @given(linked_lists, predicates) + def test_subset( + self, l: LinkedList[int], p: Callable[[int], bool] + ) -> None: + self.assertLessEqual(set(l.filter(p)), set(l)) + + @given(linked_lists, predicates) + def test_forward_observable_order( + self, l: LinkedList[int], p: Callable[[int], bool] + ) -> None: + observed_order = [] + + def pred(x: int) -> bool: + observed_order.append(x) + return p(x) + + l.filter(pred) + self.assertListEqual(list(l), observed_order) diff --git a/concat/tests/test_orderedset.py b/concat/tests/test_orderedset.py new file mode 100644 index 00000000..3e180935 --- /dev/null +++ b/concat/tests/test_orderedset.py @@ -0,0 +1,35 @@ +from concat.orderedset import InsertionOrderedSet +from hypothesis import given # type: ignore +import hypothesis.strategies as st # type: ignore +from typing import List, Set +import unittest + + +class TestInsertionOrderedSet(unittest.TestCase): + @given(st.sets(st.integers()).map(list)) + def test_insertion_from_list_preserves_order(self, l: List[int]) -> None: + self.assertListEqual(l, list(InsertionOrderedSet(l))) + + @given(st.sets(st.integers()), st.sets(st.integers())) + def test_set_difference_preserves_order( + self, original: Set[int], to_remove: Set[int] + ) -> None: + insertion_order_set = InsertionOrderedSet[int](list(original)) + expected_order = [x for x in insertion_order_set if x not in to_remove] + insertion_order_set -= to_remove + actual_order = list(insertion_order_set) + self.assertListEqual(expected_order, actual_order) + + @given(st.sets(st.integers()), st.sets(st.integers())) + def test_union_preserves_order( + self, original: Set[int], to_add: Set[int] + ) -> None: + insertion_order_set = InsertionOrderedSet[int](list(original)) + insertion_order_to_add = InsertionOrderedSet[int](list(to_add)) + expected_order = list(insertion_order_set) + for x in insertion_order_to_add: + if x not in expected_order: + expected_order.append(x) + insertion_order_set = insertion_order_set | insertion_order_to_add + actual_order = list(insertion_order_set) + self.assertListEqual(expected_order, actual_order) diff --git a/concat/tests/test_parse.py b/concat/tests/test_parse.py index 3a287251..cfb5d351 100644 --- a/concat/tests/test_parse.py +++ b/concat/tests/test_parse.py @@ -23,6 +23,9 @@ def test_examples(self) -> None: >> concat.parse.token('NAME').many() >> concat.parse.token('RPAR') ) + parsers['type-variable'] = concat.parser_combinators.fail( + 'not implemented' + ) # for example programs, we only test acceptance diff --git a/concat/tests/test_transpile.py b/concat/tests/test_transpile.py index 79aca29d..d90f0711 100644 --- a/concat/tests/test_transpile.py +++ b/concat/tests/test_transpile.py @@ -1,12 +1,11 @@ import concat.visitors -from concat.astutils import get_explicit_positional_function_parameters from concat.lex import Token import concat.parse import concat.transpile from concat.typecheck import StackEffectTypeNode, TypeSequenceNode import unittest import ast -from typing import Iterable, Iterator, List, Sequence, Type, cast +from typing import Iterable, Iterator, Type import astunparse # type: ignore @@ -56,6 +55,7 @@ def test_funcdef_statement_visitor(self) -> None: [], [], [], + [], (0, 0), StackEffectTypeNode( (0, 0), diff --git a/concat/tests/test_typecheck.py b/concat/tests/test_typecheck.py index 4401dab0..6b7114d5 100644 --- a/concat/tests/test_typecheck.py +++ b/concat/tests/test_typecheck.py @@ -2,27 +2,27 @@ import concat.parse import concat.typecheck import concat.parse -from concat.typecheck import Environment +from concat.typecheck import Environment, Substitutions +from concat.typecheck.errors import TypeError as ConcatTypeError from concat.typecheck.types import ( + BoundVariable, ClassType, + Fix, + IndividualKind, IndividualType, - IndividualVariable, + ItemKind, + ItemVariable, ObjectType, StackEffect, Type as ConcatType, TypeSequence, - int_type, - dict_type, - ellipsis_type, - file_type, float_type, - list_type, - none_type, + get_object_type, + get_int_type, no_return_type, - not_implemented_type, - object_type, + get_none_type, + optional_type, py_function_type, - str_type, ) import concat.typecheck.preamble_types import concat.astutils @@ -35,12 +35,14 @@ from hypothesis.strategies import ( dictionaries, from_type, - integers, sampled_from, text, ) +default_env = concat.typecheck.load_builtins_and_preamble() + + def lex_string(string: str) -> List[concat.lex.Token]: return lex.tokenize(string) @@ -62,46 +64,48 @@ def build_parsers() -> concat.parse.ParserDict: class TestTypeChecker(unittest.TestCase): @given(from_type(concat.parse.AttributeWordNode)) def test_attribute_word(self, attr_word) -> None: - _, type = concat.typecheck.infer( + _, type, _ = concat.typecheck.infer( concat.typecheck.Environment(), [attr_word], initial_stack=TypeSequence( [ ObjectType( - IndividualVariable(), { attr_word.value: StackEffect( - TypeSequence([]), TypeSequence([int_type]) + TypeSequence([]), + TypeSequence([get_int_type()]), ), }, ), ] ), ) - self.assertEqual(list(type.output), [int_type]) + self.assertEqual(list(type.output), [get_int_type()]) - @given(integers(min_value=0), integers(min_value=0)) - def test_add_operator_inference(self, a: int, b: int) -> None: - try_prog = '{!r} {!r} +\n'.format(a, b) + def test_add_operator_inference(self) -> None: + try_prog = '0 0 +\n' tree = parse(try_prog) - _, type = concat.typecheck.infer( - concat.typecheck.Environment( - {'+': concat.typecheck.preamble_types.types['+']} - ), + sub, type, _ = concat.typecheck.infer( + concat.typecheck.Environment({'+': default_env['+']}), tree.children, is_top_level=True, ) - note(str(type)) + print( + 'explain!:', + type + == StackEffect(TypeSequence([]), TypeSequence([get_int_type()])), + ) + self.assertEqual( - type, StackEffect(TypeSequence([]), TypeSequence([int_type])) + type, StackEffect(TypeSequence([]), TypeSequence([get_int_type()])) ) def test_if_then_inference(self) -> None: try_prog = 'True $() if_then\n' tree = parse(try_prog) - _, type = concat.typecheck.infer( + _, type, _ = concat.typecheck.infer( concat.typecheck.Environment( - concat.typecheck.preamble_types.types + {**default_env, **concat.typecheck.preamble_types.types,} ), tree.children, is_top_level=True, @@ -111,30 +115,27 @@ def test_if_then_inference(self) -> None: def test_call_inference(self) -> None: try_prog = '$(42) call\n' tree = parse(try_prog) - _, type = concat.typecheck.infer( - concat.typecheck.Environment( - concat.typecheck.preamble_types.types - ), + _, type, _ = concat.typecheck.infer( + concat.typecheck.load_builtins_and_preamble(), tree.children, is_top_level=True, ) self.assertEqual( - type, StackEffect(TypeSequence([]), TypeSequence([int_type])) + type, StackEffect(TypeSequence([]), TypeSequence([get_int_type()])) ) @given(sampled_from(['None', '...', 'NotImplemented'])) def test_constants(self, constant_name) -> None: - _, effect = concat.typecheck.infer( - concat.typecheck.Environment( - concat.typecheck.preamble_types.types - ), + env = concat.typecheck.load_builtins_and_preamble() + _, effect, _ = concat.typecheck.infer( + env, [concat.parse.NameWordNode(lex.Token(value=constant_name))], initial_stack=TypeSequence([]), ) expected_types = { - 'None': none_type, - 'NotImplemented': not_implemented_type, - '...': ellipsis_type, + 'None': get_none_type(), + 'NotImplemented': env['not_implemented'], + '...': env['ellipsis'], } expected_type = expected_types[constant_name] self.assertEqual(list(effect.output), [expected_type]) @@ -165,7 +166,7 @@ def seek_file(file:file offset:int whence:int --): ) ) env = concat.typecheck.Environment( - concat.typecheck.preamble_types.types + {**default_env, **concat.typecheck.preamble_types.types,} ) concat.typecheck.infer(env, tree.children, None, True) # If we get here, we passed @@ -173,21 +174,23 @@ def seek_file(file:file offset:int whence:int --): def test_cast_word(self) -> None: """Test that the type checker properly checks casts.""" tree = parse('"str" cast (int)') - _, type = concat.typecheck.infer( - Environment(concat.typecheck.preamble_types.types), + _, type, _ = concat.typecheck.infer( + Environment( + {**default_env, **concat.typecheck.preamble_types.types} + ), tree.children, is_top_level=True, ) self.assertEqual( - type, StackEffect(TypeSequence([]), TypeSequence([int_type])) + type, StackEffect(TypeSequence([]), TypeSequence([get_int_type()])) ) class TestStackEffectParser(unittest.TestCase): _a_bar = concat.typecheck.SequenceVariable() _d_bar = concat.typecheck.SequenceVariable() - _b = concat.typecheck.IndividualVariable() - _c = concat.typecheck.IndividualVariable() + _b = concat.typecheck.ItemVariable(ItemKind) + _c = concat.typecheck.ItemVariable(ItemKind) examples: Dict[str, StackEffect] = { 'a b -- b a': StackEffect( TypeSequence([_a_bar, _b, _c]), TypeSequence([_a_bar, _c, _b]) @@ -199,8 +202,8 @@ class TestStackEffectParser(unittest.TestCase): TypeSequence([_a_bar, _b]), TypeSequence([_a_bar]) ), 'a:object b:object -- b a': StackEffect( - TypeSequence([_a_bar, object_type, object_type,]), - TypeSequence([_a_bar, *[object_type] * 2]), + TypeSequence([_a_bar, get_object_type(), get_object_type(),]), + TypeSequence([_a_bar, *[get_object_type()] * 2]), ), 'a:`t -- a a': StackEffect( TypeSequence([_a_bar, _b]), TypeSequence([_a_bar, _b, _b]) @@ -232,9 +235,13 @@ def test_examples(self) -> None: effect = build_parsers()['stack-effect-type'].parse(tokens) except concat.parser_combinators.ParseError as e: self.fail(f'could not parse {effect_string}\n{e}') - env = Environment(concat.typecheck.preamble_types.types) + env = Environment( + {**default_env, **concat.typecheck.preamble_types.types} + ) actual = effect.to_type(env)[0].generalized_wrt(env) expected = self.examples[example].generalized_wrt(env) + print(str(actual)) + print(str(expected)) self.assertEqual( actual, expected, ) @@ -263,12 +270,12 @@ def test_builtin_name_does_not_exist_in_empty_environment(self) -> None: ) @example( named_type_node=concat.typecheck.NamedTypeNode((0, 0), ''), - type=IndividualVariable(), + type=ItemVariable(IndividualKind), ) def test_name_does_exist(self, named_type_node, type) -> None: env = concat.typecheck.Environment({named_type_node.name: type}) expected_type = named_type_node.to_type(env)[0] - note((expected_type, type)) + note(str((expected_type, type))) self.assertEqual(named_type_node.to_type(env)[0], type) @@ -288,9 +295,8 @@ def test_attribute_error_location(self) -> None: class TestTypeEquality(unittest.TestCase): @given(from_type(ConcatType)) - @example(type=int_type.self_type) - @example(type=int_type.get_type_of_attribute('__add__')) - @example(type=int_type) + @example(type=get_int_type().get_type_of_attribute('__add__')) + @example(type=get_int_type()) @settings(suppress_health_check=(HealthCheck.filter_too_much,)) def test_reflexive_equality(self, type): self.assertEqual(type, type) @@ -299,26 +305,35 @@ def test_reflexive_equality(self, type): class TestSubtyping(unittest.TestCase): def test_int_not_subtype_of_float(self) -> None: """Differ from Reticulated Python: !(int <= float).""" - self.assertFalse(int_type <= float_type) + with self.assertRaises(ConcatTypeError): + get_int_type().constrain_and_bind_variables(float_type, set(), []) @given(from_type(IndividualType), from_type(IndividualType)) @settings(suppress_health_check=(HealthCheck.filter_too_much,)) def test_stack_effect_subtyping(self, type1, type2) -> None: fun1 = StackEffect(TypeSequence([type1]), TypeSequence([type2])) fun2 = StackEffect( - TypeSequence([no_return_type]), TypeSequence([object_type]) + TypeSequence([no_return_type]), TypeSequence([get_object_type()]) + ) + self.assertEqual( + fun1.constrain_and_bind_variables(fun2, set(), []), Substitutions() ) - self.assertLessEqual(fun1, fun2) @given(from_type(IndividualType)) @settings(suppress_health_check=(HealthCheck.filter_too_much,)) def test_no_return_is_bottom_type(self, type) -> None: - self.assertLessEqual(no_return_type, type) + self.assertEqual( + no_return_type.constrain_and_bind_variables(type, set(), []), + Substitutions(), + ) @given(from_type(IndividualType)) @settings(suppress_health_check=(HealthCheck.filter_too_much,)) def test_object_is_top_type(self, type) -> None: - self.assertLessEqual(type, object_type) + self.assertEqual( + type.constrain_and_bind_variables(get_object_type(), set(), []), + Substitutions(), + ) __attributes_generator = dictionaries( text(max_size=25), from_type(IndividualType), max_size=5 # type: ignore @@ -334,27 +349,35 @@ def test_object_is_top_type(self, type) -> None: def test_object_structural_subtyping( self, attributes, other_attributes ) -> None: - x1, x2 = IndividualVariable(), IndividualVariable() - object1 = ObjectType(x1, {**other_attributes, **attributes}) - object2 = ObjectType(x2, attributes) - self.assertLessEqual(object1, object2) + object1 = ObjectType({**other_attributes, **attributes}) + object2 = ObjectType(attributes) + self.assertEqual( + object1.constrain_and_bind_variables(object2, set(), []), + Substitutions(), + ) @given(__attributes_generator, __attributes_generator) @settings(suppress_health_check=(HealthCheck.filter_too_much,)) def test_class_structural_subtyping( self, attributes, other_attributes ) -> None: - x1, x2 = IndividualVariable(), IndividualVariable() - object1 = ClassType(x1, {**other_attributes, **attributes}) - object2 = ClassType(x2, attributes) - self.assertLessEqual(object1, object2) + object1 = ClassType({**other_attributes, **attributes}) + object2 = ClassType(attributes) + note(repr(object1)) + note(repr(object2)) + self.assertEqual( + object1.constrain_and_bind_variables(object2, set(), []), + Substitutions(), + ) @given(from_type(StackEffect)) @settings(suppress_health_check=(HealthCheck.filter_too_much,)) def test_object_subtype_of_stack_effect(self, effect) -> None: - x = IndividualVariable() - object = ObjectType(x, {'__call__': effect}) - self.assertLessEqual(object, effect) + object = ObjectType({'__call__': effect}) + self.assertEqual( + object.constrain_and_bind_variables(effect, set(), []), + Substitutions(), + ) @given(from_type(IndividualType), from_type(IndividualType)) @settings( @@ -364,20 +387,25 @@ def test_object_subtype_of_stack_effect(self, effect) -> None: ) ) def test_object_subtype_of_py_function(self, type1, type2) -> None: - x = IndividualVariable() py_function = py_function_type[TypeSequence([type1]), type2] - object = ObjectType(x, {'__call__': py_function}) - self.assertLessEqual(object, py_function) + object = ObjectType({'__call__': py_function}) + self.assertEqual( + object.constrain_and_bind_variables(py_function, set(), []), + Substitutions(), + ) @given(from_type(StackEffect)) def test_class_subtype_of_stack_effect(self, effect) -> None: - x = IndividualVariable() + x = BoundVariable(kind=IndividualKind) # NOTE: self-last convention is modelled after Factor. unbound_effect = StackEffect( TypeSequence([*effect.input, x]), effect.output ) - cls = ClassType(x, {'__init__': unbound_effect}) - self.assertLessEqual(cls, effect) + cls = Fix(x, ClassType({'__init__': unbound_effect})) + self.assertEqual( + cls.constrain_and_bind_variables(effect, set(), []), + Substitutions(), + ) @given(from_type(IndividualType), from_type(IndividualType)) @settings( @@ -387,8 +415,30 @@ def test_class_subtype_of_stack_effect(self, effect) -> None: ) ) def test_class_subtype_of_py_function(self, type1, type2) -> None: - x = IndividualVariable() + x = ItemVariable(IndividualKind) py_function = py_function_type[TypeSequence([type1]), type2] unbound_py_function = py_function_type[TypeSequence([x, type1]), type2] - cls = ClassType(x, {'__init__': unbound_py_function}) - self.assertLessEqual(cls, py_function) + cls = Fix(x, ClassType({'__init__': unbound_py_function})) + self.assertEqual( + cls.constrain_and_bind_variables(py_function, set(), []), + Substitutions(), + ) + + @given(from_type(IndividualType)) + def test_none_subtype_of_optional(self, ty: IndividualType) -> None: + opt_ty = optional_type[ + ty, + ] + self.assertEqual( + get_none_type().constrain_and_bind_variables(opt_ty, set(), []), + Substitutions(), + ) + + @given(from_type(IndividualType)) + def test_type_subtype_of_optional(self, ty: IndividualType) -> None: + opt_ty = optional_type[ + ty, + ] + self.assertEqual( + ty.constrain_and_bind_variables(opt_ty, set(), []), Substitutions() + ) diff --git a/concat/tests/typecheck/__init__.py b/concat/tests/typecheck/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/concat/tests/typecheck/test_imports.py b/concat/tests/typecheck/test_imports.py new file mode 100644 index 00000000..821b9a59 --- /dev/null +++ b/concat/tests/typecheck/test_imports.py @@ -0,0 +1,39 @@ +from concat.parse import ImportStatementNode +from concat.typecheck import Environment, infer +from concat.typecheck.types import ( + BoundVariable, + GenericType, + SequenceKind, + StackEffect, + TypeSequence, + get_module_type, +) +import pathlib +from unittest import TestCase + + +class TestImports(TestCase): + def test_import_generates_module_type(self) -> None: + """Test that imports generate a module type for the right namespace.""" + test_module_path = ( + pathlib.Path(__file__) / '../../fixtures/' + ).resolve() + env = infer( + Environment(), + [ImportStatementNode('imported_module')], + is_top_level=True, + source_dir=test_module_path, + )[2] + ty = env['imported_module'] + seq_var = BoundVariable(kind=SequenceKind) + ty.constrain_and_bind_variables( + GenericType( + [seq_var], + StackEffect( + TypeSequence([seq_var]), + TypeSequence([seq_var, get_module_type()]), + ), + ), + set(), + [], + ) diff --git a/concat/tests/typecheck/test_types.py b/concat/tests/typecheck/test_types.py new file mode 100644 index 00000000..39acbcd5 --- /dev/null +++ b/concat/tests/typecheck/test_types.py @@ -0,0 +1,200 @@ +from concat.typecheck import ( + Environment, + Substitutions, + TypeError as ConcatTypeError, + load_builtins_and_preamble, +) +from concat.typecheck.types import ( + BoundVariable, + Fix, + ForwardTypeReference, + GenericType, + IndividualKind, + ItemKind, + ItemVariable, + ObjectType, + SequenceVariable, + StackEffect, + TypeSequence, + addable_type, + get_int_type, + get_object_type, + optional_type, + py_function_type, + get_tuple_type, +) +import unittest + + +load_builtins_and_preamble() + + +class TestIndividualVariableConstrain(unittest.TestCase): + def test_individual_variable_subtype(self) -> None: + v = ItemVariable(IndividualKind) + ty = get_int_type() + sub = v.constrain_and_bind_variables(ty, set(), []) + self.assertEqual(ty, sub(v)) + + def test_individual_variable_supertype(self) -> None: + v = ItemVariable(IndividualKind) + ty = get_int_type() + sub = ty.constrain_and_bind_variables(v, set(), []) + self.assertEqual(ty, sub(v)) + + def test_attribute_subtype(self) -> None: + v = ItemVariable(IndividualKind) + attr_ty = ObjectType({'__add__': v}) + ty = get_int_type() + with self.assertRaises(ConcatTypeError): + attr_ty.constrain_and_bind_variables(ty, set(), []) + + def test_attribute_supertype(self) -> None: + v = ItemVariable(IndividualKind) + attr_ty = ObjectType({'__add__': v}) + ty = get_int_type() + sub = ty.constrain_and_bind_variables(attr_ty, set(), []) + self.assertEqual(ty.get_type_of_attribute('__add__'), sub(v)) + + def test_py_function_return_subtype(self) -> None: + v = ItemVariable(IndividualKind) + py_fun_ty = py_function_type[TypeSequence([get_int_type()]), v] + ty = get_int_type().get_type_of_attribute('__add__') + sub = py_fun_ty.constrain_and_bind_variables(ty, set(), []) + self.assertEqual(get_int_type(), sub(v)) + + def test_py_function_return_supertype(self) -> None: + v = ItemVariable(IndividualKind) + py_fun_ty = py_function_type[TypeSequence([get_int_type()]), v] + ty = get_int_type().get_type_of_attribute('__add__') + sub = ty.constrain_and_bind_variables(py_fun_ty, set(), []) + self.assertEqual(get_int_type(), sub(v)) + + def test_type_sequence_subtype(self) -> None: + v = ItemVariable(IndividualKind) + seq_ty = TypeSequence([v]) + ty = TypeSequence([get_int_type()]) + sub = seq_ty.constrain_and_bind_variables(ty, set(), []) + self.assertEqual(get_int_type(), sub(v)) + + def test_type_sequence_supertype(self) -> None: + v = ItemVariable(IndividualKind) + seq_ty = TypeSequence([v]) + ty = TypeSequence([get_int_type()]) + sub = ty.constrain_and_bind_variables(seq_ty, set(), []) + self.assertEqual(get_int_type(), sub(v)) + + def test_int_addable(self) -> None: + v = ItemVariable(IndividualKind) + sub = get_int_type().constrain_and_bind_variables( + addable_type[v, v], set(), [] + ) + self.assertEqual(get_int_type(), sub(v)) + + def test_int__add__addable__add__(self) -> None: + v = ItemVariable(IndividualKind) + int_add = get_int_type().get_type_of_attribute('__add__') + addable_add = addable_type[v, v].get_type_of_attribute('__add__') + sub = int_add.constrain_and_bind_variables(addable_add, set(), []) + print(v) + print(int_add) + print(addable_add) + print(sub) + self.assertEqual(get_int_type(), sub(v)) + + +class TestSequenceVariableConstrain(unittest.TestCase): + def test_stack_effect_input_subtype(self) -> None: + v = SequenceVariable() + effect_ty = StackEffect(TypeSequence([v]), TypeSequence([])) + ty = StackEffect(TypeSequence([]), TypeSequence([])) + sub = effect_ty.constrain_and_bind_variables(ty, set(), []) + self.assertEqual(TypeSequence([]), sub(v)) + + def test_stack_effect_input_supertype(self) -> None: + v = SequenceVariable() + effect_ty = StackEffect(TypeSequence([v]), TypeSequence([])) + ty = StackEffect(TypeSequence([]), TypeSequence([])) + sub = ty.constrain_and_bind_variables(effect_ty, set(), []) + self.assertEqual(TypeSequence([]), sub(v)) + + +class TestFix(unittest.TestCase): + fix_var = BoundVariable(IndividualKind) + linked_list = Fix( + fix_var, optional_type[get_tuple_type()[get_object_type(), fix_var],], + ) + + def test_unroll_supertype(self) -> None: + self.assertEqual( + Substitutions(), + self.linked_list.constrain_and_bind_variables( + self.linked_list.unroll(), set(), [] + ), + ) + + def test_unroll_subtype(self) -> None: + self.assertEqual( + Substitutions(), + self.linked_list.unroll().constrain_and_bind_variables( + self.linked_list, set(), [] + ), + ) + + def test_unroll_equal(self) -> None: + self.assertEqual(self.linked_list.unroll(), self.linked_list) + self.assertEqual(self.linked_list, self.linked_list.unroll()) + + +class TestForwardReferences(unittest.TestCase): + env = Environment({'ty': get_object_type()}) + ty = ForwardTypeReference(IndividualKind, 'ty', env) + + def test_resolve_supertype(self) -> None: + self.assertEqual( + Substitutions(), + self.ty.constrain_and_bind_variables( + self.ty.resolve_forward_references(), set(), [] + ), + ) + + def test_resolve_subtype(self) -> None: + self.assertEqual( + Substitutions(), + self.ty.resolve_forward_references().constrain_and_bind_variables( + self.ty, set(), [] + ), + ) + + def test_resolve_equal(self) -> None: + self.assertEqual(self.ty.resolve_forward_references(), self.ty) + self.assertEqual(self.ty, self.ty.resolve_forward_references()) + + +class TestTypeSequence(unittest.TestCase): + def test_constrain_empty(self) -> None: + self.assertEqual( + Substitutions(), + TypeSequence([]).constrain_and_bind_variables( + TypeSequence([]), set(), [] + ), + ) + + def test_empty_equal(self) -> None: + self.assertEqual(TypeSequence([]), TypeSequence([])) + + +class TestGeneric(unittest.TestCase): + def test_generalize(self) -> None: + a, b = BoundVariable(ItemKind), BoundVariable(ItemKind) + subtype = GenericType([a], get_int_type()) + supertype = GenericType([a, b], get_int_type()) + subtype.constrain_and_bind_variables(supertype, set(), []) + + def test_parameter_kinds(self) -> None: + ind = BoundVariable(IndividualKind) + item = BoundVariable(ItemKind) + subtype = GenericType([ind], ind) + supertype = GenericType([item], item) + with self.assertRaises(ConcatTypeError): + subtype.constrain_and_bind_variables(supertype, set(), []) diff --git a/concat/transpile.py b/concat/transpile.py index da761387..e18308b4 100644 --- a/concat/transpile.py +++ b/concat/transpile.py @@ -51,9 +51,8 @@ def parse(tokens: Sequence[Token]) -> concat.parse.TopLevelNode: def typecheck(concat_ast: concat.parse.TopLevelNode, source_dir: str) -> None: # FIXME: Consider the type of everything entered interactively beforehand. - concat.typecheck.check( - concat.typecheck.Environment(), concat_ast.children, source_dir - ) + env = concat.typecheck.load_builtins_and_preamble() + concat.typecheck.check(env, concat_ast.children, source_dir) def transpile(code: str, source_dir: str = '.') -> ast.Module: diff --git a/concat/type-level-lang-precedence.md b/concat/type-level-lang-precedence.md new file mode 100644 index 00000000..67d46f52 --- /dev/null +++ b/concat/type-level-lang-precedence.md @@ -0,0 +1,37 @@ +The type constructor of a type application is restricted to being a name. + +```python +{ + seed: py_function[(int), none], + shuffle: forall `t. py_function[(list[`t]), none] +} +``` + +``` +Object + seed: + type application + name - py_function + args + sequence + item 1: + name - _ + name - int + name - none + shuffle: + forall + args + individual var - t + type + type application + name - py_function + args + sequence + item 1: + name - _ + type application + name - list + args + individual var - t + name - none +``` diff --git a/concat/typecheck/__init__.py b/concat/typecheck/__init__.py index b9db76f1..79bed40c 100644 --- a/concat/typecheck/__init__.py +++ b/concat/typecheck/__init__.py @@ -4,117 +4,126 @@ "Robert Kleffner: A Foundation for Typed Concatenative Languages, April 2017." """ -import abc -import builtins -import collections.abc -from concat.lex import Token -import importlib -import sys + +from concat.typecheck.errors import ( + NameError, + StaticAnalysisError, + TypeError, + UnhandledNodeTypeError, +) from typing import ( + Any, + Callable, + Dict, Generator, Iterable, + Iterator, List, - Set, - Tuple, - Dict, - Union, + Mapping, Optional, - Callable, Sequence, - TypeVar, + Set, TYPE_CHECKING, - overload, + Tuple, + TypeVar, + Union, cast, ) from typing_extensions import Protocol -import concat.parser_combinators -import concat.parse if TYPE_CHECKING: import concat.astutils - from concat.orderedset import OrderedSet - from concat.typecheck.types import _Variable + from concat.orderedset import InsertionOrderedSet + from concat.typecheck.types import Type, Variable -class StaticAnalysisError(Exception): - def __init__(self, message: str) -> None: - self.message = message - self.location: Optional['concat.astutils.Location'] = None +class Environment(Dict[str, 'Type']): + _next_id = -1 - def set_location_if_missing( - self, location: 'concat.astutils.Location' - ) -> None: - if not self.location: - self.location = location - - def __str__(self) -> str: - return '{} at {}'.format(self.message, self.location) + def __init__(self, *args, **kwargs) -> None: + super().__init__(*args, **kwargs) + self.id = Environment._next_id + Environment._next_id -= 1 + def copy(self) -> 'Environment': + return Environment(super().copy()) -class TypeError(StaticAnalysisError, builtins.TypeError): - pass + def apply_substitution(self, sub: 'Substitutions') -> 'Environment': + return Environment({name: sub(t) for name, t in self.items()}) + def free_type_variables(self) -> 'InsertionOrderedSet[Variable]': + return free_type_variables_of_mapping(self) -class NameError(StaticAnalysisError, builtins.NameError): - def __init__( - self, - name: Union[concat.parse.NameWordNode, str], - location: Optional[concat.astutils.Location] = None, - ) -> None: - if isinstance(name, concat.parse.NameWordNode): - location = name.location - name = name.value - super().__init__(f'name {name!r} not previously defined') - self._name = name - self.location = location - def __str__(self) -> str: - location_info = '' - if self.location: - location_info = ' (error at {}:{})'.format(*self.location) - return self.message + location_info +_Result = TypeVar('_Result', covariant=True) -class AttributeError(TypeError, builtins.AttributeError): - def __init__(self, type: 'Type', attribute: str) -> None: - super().__init__( - 'object of type {} does not have attribute {}'.format( - type, attribute - ) - ) - self._type = type - self._attribute = attribute +class _Substitutable(Protocol[_Result]): + def apply_substitution(self, sub: 'Substitutions') -> _Result: + # empty, abstract protocol method + pass -class StackMismatchError(TypeError): +class Substitutions(Mapping['Variable', 'Type']): def __init__( - self, actual: 'TypeSequence', expected: 'TypeSequence' + self, + sub: Union[ + Iterable[Tuple['Variable', 'Type']], + Mapping['Variable', 'Type'], + None, + ] = None, ) -> None: - super().__init__( - 'The stack here is {}, but sequence type {} was expected'.format( - actual, expected - ) - ) - - -class UnhandledNodeTypeError(builtins.NotImplementedError): - pass + self._sub = {} if sub is None else dict(sub) + for variable, ty in self._sub.items(): + if not (variable.kind >= ty.kind): + raise TypeError( + f'{variable} is being substituted by {ty}, which has the wrong kind ({variable.kind} vs {ty.kind})' + ) + self._cache: Dict[int, 'Type'] = {} + # innermost first + self.subtyping_provenance: List[Any] = [] + def add_subtyping_provenance( + self, subtyping_query: Tuple['Type', 'Type'] + ) -> None: + self.subtyping_provenance.append(subtyping_query) -_Result = TypeVar('_Result', covariant=True) + def __getitem__(self, var: 'Variable') -> 'Type': + return self._sub[var] + def __iter__(self) -> Iterator['Variable']: + return iter(self._sub) -class _Substitutable(Protocol[_Result]): - def apply_substitution(self, sub: 'Substitutions') -> _Result: - pass + def __len__(self) -> int: + return len(self._sub) + def __bool__(self) -> bool: + return bool(self._sub) -class Substitutions(Dict['_Variable', 'Type']): def __call__(self, arg: _Substitutable[_Result]) -> _Result: - return arg.apply_substitution(self) - - def _dom(self) -> Set['_Variable']: + from concat.typecheck.types import Type + + result: _Result + # Previously I tried caching results by the id of the argument. But + # since the id is the memory address of the object in CPython, another + # object might have the same id later. I think this was leading to + # nondeterministic Concat type errors from the type checker. + if isinstance(arg, Type): + if arg._type_id not in self._cache: + if not (self._dom() & arg.free_type_variables()): + self._cache[arg._type_id] = arg + else: + self._cache[arg._type_id] = arg.apply_substitution(self) + result = self._cache[arg._type_id] + if isinstance(arg, Environment): + if arg.id not in self._cache: + self._cache[arg.id] = arg.apply_substitution(self) + result = self._cache[arg.id] + result = arg.apply_substitution(self) + return result + + def _dom(self) -> Set['Variable']: return {*self} def __str__(self) -> str: @@ -127,70 +136,96 @@ def __str__(self) -> str: ) def apply_substitution(self, sub: 'Substitutions') -> 'Substitutions': - return Substitutions( + new_sub = Substitutions( { **sub, **{a: sub(i) for a, i in self.items() if a not in sub._dom()}, } ) + new_sub.subtyping_provenance = [ + (self.subtyping_provenance, sub.subtyping_provenance) + ] + return new_sub + + def __hash__(self) -> int: + return hash(tuple(self.items())) from concat.typecheck.types import ( - Type, - IndividualVariable, - StackEffect, - ForAll, + BoundVariable, + Brand, + Fix, + ForwardTypeReference, + GenericType, + GenericTypeKind, + IndividualKind, IndividualType, + ItemKind, + ItemVariable, + Kind, + NominalType, ObjectType, - PythonFunctionType, + QuotationType, + SequenceKind, SequenceVariable, - TypeSequence, + StackEffect, StackItemType, - QuotationType, - bool_type, - context_manager_type, - ellipsis_type, + TypeSequence, free_type_variables_of_mapping, - int_type, - init_primitives, - invertible_type, - iterable_type, - list_type, - module_type, - none_type, - not_implemented_type, - object_type, - py_function_type, - slice_type, - str_type, - subscriptable_type, - subtractable_type, - tuple_type, + get_int_type, + get_list_type, + get_str_type, + get_tuple_type, + get_module_type, + no_return_type, ) +import abc +from concat.error_reporting import create_parsing_failure_message +from concat.lex import Token +import itertools +import pathlib +import sys +import concat.parser_combinators +import concat.parse -class Environment(Dict[str, Type]): - def copy(self) -> 'Environment': - return Environment(super().copy()) +_builtins_stub_path = pathlib.Path(__file__) / '../builtin_stubs/builtins.cati' - def apply_substitution(self, sub: 'Substitutions') -> 'Environment': - return Environment({name: sub(t) for name, t in self.items()}) - def free_type_variables(self) -> 'OrderedSet[_Variable]': - return free_type_variables_of_mapping(self) +def load_builtins_and_preamble() -> Environment: + env = _check_stub(pathlib.Path(__file__).with_name('preamble0.cati'),) + env = _check_stub(_builtins_stub_path, initial_env=env) + env = _check_stub( + pathlib.Path(__file__).with_name('preamble.cati'), initial_env=env, + ) + # pick up ModuleType + _check_stub( + _builtins_stub_path.with_name('types.cati'), initial_env=env.copy(), + ) + return env def check( environment: Environment, - program: concat.astutils.WordsOrStatements, + program: 'concat.astutils.WordsOrStatements', source_dir: str = '.', -) -> None: + _should_check_bodies: bool = True, +) -> Environment: import concat.typecheck.preamble_types environment = Environment( - {**concat.typecheck.preamble_types.types, **environment} + {**concat.typecheck.preamble_types.types, **environment,} + ) + res = infer( + environment, + program, + None, + True, + source_dir, + check_bodies=_should_check_bodies, ) - infer(environment, program, None, True, source_dir) + + return res[2] # FIXME: I'm really passing around a bunch of state here. I could create an @@ -202,7 +237,8 @@ def infer( is_top_level=False, source_dir='.', initial_stack: Optional[TypeSequence] = None, -) -> Tuple[Substitutions, StackEffect]: + check_bodies: bool = True, +) -> Tuple[Substitutions, StackEffect, Environment]: """The infer function described by Kleffner.""" e = list(e) current_subs = Substitutions() @@ -212,11 +248,63 @@ def infer( ) current_effect = StackEffect(initial_stack, initial_stack) + # Prepare for forward references. + # TODO: Do this in a more principled way with scope graphs. + gamma = gamma.copy() + for node in e: + if isinstance(node, concat.parse.ClassdefStatementNode): + type_name = node.class_name + kind: Kind = IndividualKind + type_parameters = [] + parameter_kinds: Sequence[Kind] + if node.is_variadic: + parameter_kinds = [SequenceKind] + else: + for param in node.type_parameters: + if isinstance(param, TypeNode): + type_parameters.append(param.to_type(gamma)[0]) + continue + raise UnhandledNodeTypeError(param) + if type_parameters: + parameter_kinds = [ + variable.kind for variable in type_parameters + ] + kind = GenericTypeKind(parameter_kinds, IndividualKind) + gamma[type_name] = ForwardTypeReference(kind, type_name, gamma) + for node in e: try: S, (i, o) = current_subs, current_effect - if isinstance(node, concat.parse.PushWordNode): + if isinstance(node, concat.parse.PragmaNode): + namespace = 'concat.typecheck.' + if node.pragma.startswith(namespace): + pragma = node.pragma[len(namespace) :] + if pragma == 'builtin_object': + name = node.args[0] + concat.typecheck.types.set_object_type(gamma[name]) + if pragma == 'builtin_list': + name = node.args[0] + concat.typecheck.types.set_list_type(gamma[name]) + if pragma == 'builtin_str': + name = node.args[0] + concat.typecheck.types.set_str_type(gamma[name]) + if pragma == 'builtin_int': + name = node.args[0] + concat.typecheck.types.set_int_type(gamma[name]) + if pragma == 'builtin_bool': + name = node.args[0] + concat.typecheck.types.set_bool_type(gamma[name]) + if pragma == 'builtin_tuple': + name = node.args[0] + concat.typecheck.types.set_tuple_type(gamma[name]) + if pragma == 'builtin_none': + name = node.args[0] + concat.typecheck.types.set_none_type(gamma[name]) + if pragma == 'builtin_module': + name = node.args[0] + concat.typecheck.types.set_module_type(gamma[name]) + elif isinstance(node, concat.parse.PushWordNode): S1, (i1, o1) = S, (i, o) child = node.children[0] if isinstance(child, concat.parse.FreezeWordNode): @@ -242,6 +330,8 @@ def infer( if child.value not in gamma: raise NameError(child) name_type = gamma[child.value] + if isinstance(name_type, ForwardTypeReference): + raise NameError(child) if should_instantiate: name_type = name_type.instantiate() current_effect = StackEffect( @@ -257,12 +347,13 @@ def infer( # The majority of quotations I've written don't comsume # anything on the stack, so make that the default. input_stack = TypeSequence([SequenceVariable()]) - S2, fun_type = infer( + S2, fun_type, _ = infer( S1(gamma), child.children, extensions=extensions, source_dir=source_dir, initial_stack=input_stack, + check_bodies=check_bodies, ) current_subs, current_effect = ( S2(S1), @@ -280,20 +371,21 @@ def infer( elif isinstance(node, concat.parse.ListWordNode): phi = S collected_type = o - element_type: IndividualType = object_type + element_type: 'Type' = no_return_type for item in node.list_children: - phi1, fun_type = infer( + phi1, fun_type, _ = infer( phi(gamma), item, extensions=extensions, source_dir=source_dir, initial_stack=collected_type, + check_bodies=check_bodies, ) collected_type = fun_type.output # FIXME: Infer the type of elements in the list based on # ALL the elements. - if element_type == object_type: - assert isinstance(collected_type[-1], IndividualType) + if element_type == no_return_type: + assert collected_type[-1] != SequenceKind element_type = collected_type[-1] # drop the top of the stack to use as the item collected_type = collected_type[:-1] @@ -304,7 +396,10 @@ def infer( StackEffect( i, TypeSequence( - [*collected_type, list_type[element_type,]] + [ + *collected_type, + get_list_type()[element_type,], + ] ), ) ), @@ -314,12 +409,13 @@ def infer( collected_type = current_effect.output element_types: List[IndividualType] = [] for item in node.tuple_children: - phi1, fun_type = infer( + phi1, fun_type, _ = infer( phi(gamma), item, extensions=extensions, source_dir=source_dir, initial_stack=collected_type, + check_bodies=check_bodies, ) collected_type = fun_type.output assert isinstance(collected_type[-1], IndividualType) @@ -335,7 +431,7 @@ def infer( TypeSequence( [ *collected_type, - tuple_type[TypeSequence(element_types),], + get_tuple_type()[element_types], ] ), ) @@ -343,38 +439,47 @@ def infer( ) elif isinstance(node, concat.parse.FromImportStatementNode): imported_name = node.asname or node.imported_name - # mutate type environment - gamma[imported_name] = object_type - # We will try to find a more specific type. - sys.path, old_path = [source_dir, *sys.path], sys.path - module = importlib.import_module(node.value) - sys.path = old_path - # For now, assume the module's written in Python. - try: - # TODO: Support star imports - gamma[imported_name] = current_subs( - getattr(module, '@@types')[node.imported_name] - ) - except (KeyError, builtins.AttributeError): - # attempt introspection to get a more specific type - if callable(getattr(module, node.imported_name)): - args_var = SequenceVariable() - gamma[imported_name] = ObjectType( - IndividualVariable(), - { - '__call__': py_function_type[ - TypeSequence([args_var]), object_type - ], - }, - type_parameters=[args_var], - nominal=True, + module_parts = node.value.split('.') + module_spec = None + path = None + if module_parts[0] in sys.builtin_module_names: + stub_path = pathlib.Path(__file__) / '../builtin_stubs' + for part in module_parts: + stub_path = stub_path / part + else: + for module_prefix in itertools.accumulate( + module_parts, lambda a, b: f'{a}.{b}' + ): + for finder in sys.meta_path: + module_spec = finder.find_spec(module_prefix, path) + if module_spec is not None: + path = module_spec.submodule_search_locations + break + assert module_spec is not None + module_path = module_spec.origin + if module_path is None: + raise TypeError( + f'Cannot find path of module {node.value}' ) + # For now, assume the module's written in Python. + stub_path = pathlib.Path(module_path) + stub_path = stub_path.with_suffix('.cati') + stub_env = _check_stub( + stub_path, initial_env=load_builtins_and_preamble() + ) + imported_type = stub_env.get(node.imported_name) + if imported_type is None: + raise TypeError( + f'Cannot find {node.imported_name} in module {node.value}' + ) + # TODO: Support star imports + gamma[imported_name] = current_subs(imported_type) elif isinstance(node, concat.parse.ImportStatementNode): # TODO: Support all types of import correctly. if node.asname is not None: gamma[node.asname] = current_subs( _generate_type_of_innermost_module( - node.value, source_dir + node.value, source_dir=pathlib.Path(source_dir) ).generalized_wrt(current_subs(gamma)) ) else: @@ -385,53 +490,79 @@ def infer( # should implement namespaces properly. gamma[components[0]] = current_subs( _generate_module_type( - components, source_dir=source_dir + components, source_dir=pathlib.Path(source_dir) ) ) elif isinstance(node, concat.parse.FuncdefStatementNode): S = current_subs - f = current_effect name = node.name - # NOTE: To continue the "bidirectional" bent, we will require a + # NOTE: To continue the "bidirectional" bent, we will require a ghg # type annotation. # TODO: Make the return types optional? declared_type, _ = node.stack_effect.to_type(S(gamma)) declared_type = S(declared_type) recursion_env = gamma.copy() + if not isinstance(declared_type, StackEffect): + raise TypeError( + f'declared type of {name} must be a stack effect, got {declared_type}' + ) recursion_env[name] = declared_type.generalized_wrt(S(gamma)) - phi1, inferred_type = infer( - S(recursion_env), - node.body, + if check_bodies: + phi1, inferred_type, _ = infer( + S(recursion_env), + node.body, + is_top_level=False, + extensions=extensions, + initial_stack=declared_type.input, + check_bodies=check_bodies, + ) + # We want to check that the inferred outputs are subtypes of + # the declared outputs. Thus, inferred_type.output should be a subtype + # declared_type.output. + try: + S = inferred_type.output.constrain_and_bind_variables( + declared_type.output, + S(recursion_env).free_type_variables(), + [], + )(S) + except TypeError as e: + message = ( + 'declared function type {} is not compatible with ' + 'inferred type {}' + ) + raise TypeError( + message.format(declared_type, inferred_type) + ) from e + effect = declared_type + # type check decorators + _, final_type_stack, _ = infer( + gamma, + list(node.decorators), is_top_level=False, extensions=extensions, - initial_stack=declared_type.input, + initial_stack=TypeSequence([effect]), + check_bodies=check_bodies, ) - # We want to check that the inferred outputs are subtypes of - # the declared outputs. Thus, inferred_type.output should be a subtype - # declared_type.output. - try: - S = inferred_type.output.constrain_and_bind_subtype_variables( - declared_type.output, - S(recursion_env).free_type_variables(), - [], - )( - S - ) - except TypeError: - message = ( - 'declared function type {} is not compatible with ' - 'inferred type {}' + final_type_stack_output = final_type_stack.output.as_sequence() + if len(final_type_stack_output) != 1: + raise TypeError( + f'Decorators produce too many stack items: only 1 should be left. Stack: {final_type_stack.output}' ) + final_type = final_type_stack_output[0] + if not isinstance(final_type, IndividualType): raise TypeError( - message.format(declared_type, inferred_type) + f'Decorators should produce something of individual type, got {final_type}' ) - effect = declared_type # we *mutate* the type environment - gamma[name] = effect.generalized_wrt(S(gamma)) + gamma[name] = ( + final_type.generalized_wrt(S(gamma)) + if isinstance(final_type, StackEffect) + else final_type + ) elif isinstance(node, concat.parse.NumberWordNode): if isinstance(node.value, int): current_effect = StackEffect( - i, TypeSequence([*o, int_type]) + i, TypeSequence([*o, get_int_type()]) ) else: raise UnhandledNodeTypeError @@ -439,7 +570,10 @@ def infer( (i1, o1) = current_effect if node.value not in current_subs(gamma): raise NameError(node) - type_of_name = current_subs(gamma)[node.value].instantiate() + type_of_name = current_subs(gamma)[node.value] + if isinstance(type_of_name, ForwardTypeReference): + raise NameError(node) + type_of_name = type_of_name.instantiate() type_of_name = type_of_name.get_type_of_attribute( '__call__' ).instantiate() @@ -449,7 +583,7 @@ def infer( node.value, type_of_name, type_of_name ) ) - constraint_subs = o1.constrain_and_bind_supertype_variables( + constraint_subs = o1.constrain_and_bind_variables( type_of_name.input, set(), [] ) current_subs = constraint_subs(current_subs) @@ -461,17 +595,18 @@ def infer( # make sure any annotation matches the current stack if quotation.input_stack_type is not None: input_stack, _ = quotation.input_stack_type.to_type(gamma) - S = o.constrain_and_bind_supertype_variables( - input_stack, set(), [] - )(S) + S = o.constrain_and_bind_variables(input_stack, set(), [])( + S + ) else: input_stack = o - S1, (i1, o1) = infer( + S1, (i1, o1), _ = infer( gamma, [*quotation.children], extensions=extensions, source_dir=source_dir, initial_stack=input_stack, + check_bodies=check_bodies, ) current_subs, current_effect = ( S1(S), @@ -482,7 +617,7 @@ def infer( S, StackEffect( current_effect.input, - TypeSequence([*current_effect.output, str_type]), + TypeSequence([*current_effect.output, get_str_type()]), ), ) elif isinstance(node, concat.parse.AttributeWordNode): @@ -497,7 +632,7 @@ def infer( node.value, attr_function_type, attr_function_type ) ) - R = out_types.constrain_and_bind_supertype_variables( + R = out_types.constrain_and_bind_variables( attr_function_type.input, set(), [] ) current_subs, current_effect = ( @@ -514,17 +649,157 @@ def infer( ) elif isinstance(node, concat.parse.ParseError): current_effect = StackEffect( - current_effect.input, - TypeSequence([SequenceVariable()]), + current_effect.input, TypeSequence([SequenceVariable()]), ) + elif not check_bodies and isinstance( + node, concat.parse.ClassdefStatementNode + ): + type_parameters: List[Variable] = [] + temp_gamma = gamma.copy() + if node.is_variadic: + type_parameters.append(SequenceVariable()) + else: + for param_node in node.type_parameters: + if not isinstance(param_node, TypeNode): + raise UnhandledNodeTypeError(param_node) + param, temp_gamma = param_node.to_type(temp_gamma) + type_parameters.append(param) + + kind: Kind = IndividualKind + if type_parameters: + kind = GenericTypeKind( + [v.kind for v in type_parameters], IndividualKind + ) + self_type = BoundVariable(kind) + temp_gamma[node.class_name] = self_type + _, _, body_attrs = infer( + temp_gamma, + node.children, + extensions=extensions, + source_dir=source_dir, + initial_stack=TypeSequence([]), + check_bodies=check_bodies, + ) + # TODO: Introduce scopes into the environment object + body_attrs = Environment( + { + name: ty + for name, ty in body_attrs.items() + if name not in temp_gamma + } + ) + ty: Type = NominalType( + Brand(node.class_name, IndividualKind, []), + ObjectType(attributes=body_attrs,), + ) + if type_parameters: + ty = GenericType( + type_parameters, ty, is_variadic=node.is_variadic + ) + ty = Fix(self_type, ty) + gamma[node.class_name] = ty + # TODO: Type aliases else: raise UnhandledNodeTypeError( "don't know how to handle '{}'".format(node) ) - except TypeError as e: - e.set_location_if_missing(node.location) + except TypeError as error: + error.set_location_if_missing(node.location) raise - return current_subs, current_effect + return current_subs, current_effect, gamma + + +def _find_stub_path( + module_parts: Sequence[str], source_dir: pathlib.Path +) -> pathlib.Path: + if module_parts[0] in sys.builtin_module_names: + stub_path = pathlib.Path(__file__) / '../builtin_stubs' + for part in module_parts: + stub_path = stub_path / part + else: + module_spec = None + path: Optional[List[str]] + if source_dir is not None: + path = [str(source_dir)] + sys.path + else: + path = sys.path + for module_prefix in itertools.accumulate( + module_parts, lambda a, b: f'{a}.{b}' + ): + for finder in sys.meta_path: + module_spec = finder.find_spec(module_prefix, path) + if module_spec is not None: + path = module_spec.submodule_search_locations + break + if module_spec is None: + raise TypeError( + f'Cannot find module {".".join(module_parts)} from source dir {source_dir}' + ) + module_path = module_spec.origin + if module_path is None: + raise TypeError( + f'Cannot find path of module {".".join(module_parts)}' + ) + # For now, assume the module's written in Python. + stub_path = pathlib.Path(module_path) + stub_path = stub_path.with_suffix('.cati') + return stub_path + + +_module_namespaces: Dict[pathlib.Path, 'Environment'] = {} + + +def _check_stub_resolved_path( + path: pathlib.Path, initial_env: Optional['Environment'] = None, +) -> 'Environment': + if path in _module_namespaces: + return _module_namespaces[path] + try: + source = path.read_text() + except FileNotFoundError as e: + raise TypeError(f'Type stubs at {path} do not exist') from e + except IOError as e: + raise TypeError(f'Failed to read type stubs at {path}') from e + tokens = concat.lex.tokenize(source) + env = initial_env or Environment() + from concat.transpile import parse + + try: + concat_ast = parse(tokens) + except concat.parser_combinators.ParseError as e: + print('Parse Error:') + with path.open() as file: + print( + create_parsing_failure_message( + file, tokens, e.args[0].failures + ) + ) + _module_namespaces[path] = env + return env + recovered_parsing_failures = concat_ast.parsing_failures + with path.open() as file: + for failure in recovered_parsing_failures: + print('Parse Error:') + print(create_parsing_failure_message(file, tokens, failure)) + try: + env = check( + env, + concat_ast.children, + str(path.parent), + _should_check_bodies=False, + ) + except StaticAnalysisError as e: + e.set_path_if_missing(path) + raise + _module_namespaces[path] = env + return env + + +def _check_stub( + path: pathlib.Path, initial_env: Optional['Environment'] = None, +) -> 'Environment': + path = path.resolve() + return _check_stub_resolved_path(path, initial_env) # Parsing type annotations @@ -532,10 +807,12 @@ def infer( class TypeNode(concat.parse.Node, abc.ABC): def __init__(self, location: concat.astutils.Location) -> None: + super().__init__() self.location = location + self.children: Sequence[concat.parse.Node] @abc.abstractmethod - def to_type(self, env: Environment) -> Tuple[Type, Environment]: + def to_type(self, env: Environment) -> Tuple['Type', Environment]: pass @@ -545,23 +822,24 @@ def __init__(self, location: concat.astutils.Location) -> None: super().__init__(location) @abc.abstractmethod - def to_type(self, env: Environment) -> Tuple[IndividualType, Environment]: + def to_type(self, env: Environment) -> Tuple['Type', Environment]: pass # A dataclass is not used here because making this a subclass of an abstract # class does not work without overriding __init__ even when it's a dataclass. class NamedTypeNode(TypeNode): - def __init__(self, location: tuple, name: str) -> None: + def __init__(self, location: concat.astutils.Location, name: str) -> None: super().__init__(location) self.name = name + self.children = [] def __repr__(self) -> str: return '{}({!r}, {!r})'.format( type(self).__qualname__, self.location, self.name ) - def to_type(self, env: Environment) -> Tuple[Type, Environment]: + def to_type(self, env: Environment) -> Tuple['Type', Environment]: type = env.get(self.name, None) if type is None: raise NameError(self.name, self.location) @@ -587,12 +865,15 @@ class _GenericTypeNode(IndividualTypeNode): def __init__( self, location: concat.astutils.Location, + end_location: concat.astutils.Location, generic_type: IndividualTypeNode, type_arguments: Sequence[IndividualTypeNode], ) -> None: super().__init__(location) self._generic_type = generic_type self._type_arguments = type_arguments + self.end_location = end_location + self.children = [generic_type] + list(type_arguments) def to_type(self, env: Environment) -> Tuple[IndividualType, Environment]: args = [] @@ -600,7 +881,7 @@ def to_type(self, env: Environment) -> Tuple[IndividualType, Environment]: arg_as_type, env = arg.to_type(env) args.append(arg_as_type) generic_type, env = self._generic_type.to_type(env) - if isinstance(generic_type, ObjectType): + if isinstance(generic_type.kind, GenericTypeKind): return generic_type[args], env raise TypeError('{} is not a generic type'.format(generic_type)) @@ -616,13 +897,20 @@ def __init__( super().__init__(location) self._name = None if args[0] is None else args[0].value self._type = args[1] + self.children = [n for n in args if isinstance(n, TypeNode)] - # QUESTION: Should I have a separate space for the temporary associated names? + # QUESTION: Should I have a separate space for the temporary associated + # names? def to_type(self, env: Environment) -> Tuple[IndividualType, Environment]: if self._name is None: return self._type.to_type(env) elif self._type is None: - return env[self._name].to_type(env) + ty = env[self._name] + if not isinstance(ty, IndividualType): + raise TypeError( + f'an individual type was expected in this part of a type sequence, got {ty}' + ) + return ty, env elif self._name in env: raise TypeError( '{} is associated with a type more than once in this sequence of types'.format( @@ -654,19 +942,23 @@ def __init__( super().__init__(location or (-1, -1)) self._sequence_variable = seq_var self._individual_type_items = tuple(individual_type_items) + self.children = [] if seq_var is None else [seq_var] + self.children.extend(self._individual_type_items) def to_type(self, env: Environment) -> Tuple[TypeSequence, Environment]: sequence: List[StackItemType] = [] + temp_env = env.copy() if self._sequence_variable is None: # implicit stack polymorphism + # FIXME: This should be handled in stack effect construction sequence.append(SequenceVariable()) - elif self._sequence_variable.name not in env: - env = env.copy() + elif self._sequence_variable.name not in temp_env: + temp_env = temp_env.copy() var = SequenceVariable() - env[self._sequence_variable.name] = var + temp_env[self._sequence_variable.name] = var sequence.append(var) for type_node in self._individual_type_items: - type, env = type_node.to_type(env) + type, temp_env = type_node.to_type(temp_env) sequence.append(type) return TypeSequence(sequence), env @@ -693,6 +985,7 @@ def __init__( self.input = [(i.name, i.type) for i in input.individual_type_items] self.output_sequence_variable = output.sequence_variable self.output = [(o.name, o.type) for o in output.individual_type_items] + self.children = [input, output] def __repr__(self) -> str: return '{}({!r}, {!r}, {!r}, {!r}, location={!r})'.format( @@ -708,6 +1001,7 @@ def to_type(self, env: Environment) -> Tuple[StackEffect, Environment]: a_bar = SequenceVariable() b_bar = a_bar new_env = env.copy() + known_stack_item_names = Environment() if self.input_sequence_variable is not None: if self.input_sequence_variable.name in new_env: a_bar = cast( @@ -727,11 +1021,15 @@ def to_type(self, env: Environment) -> Tuple[StackEffect, Environment]: in_types = [] for item in self.input: - type, new_env = _ensure_type(item[1], new_env, item[0]) + type, new_env = _ensure_type( + item[1], new_env, item[0], known_stack_item_names, + ) in_types.append(type) out_types = [] for item in self.output: - type, new_env = _ensure_type(item[1], new_env, item[0]) + type, new_env = _ensure_type( + item[1], new_env, item[0], known_stack_item_names, + ) out_types.append(type) return ( @@ -739,34 +1037,33 @@ def to_type(self, env: Environment) -> Tuple[StackEffect, Environment]: TypeSequence([a_bar, *in_types]), TypeSequence([b_bar, *out_types]), ), - new_env, + env, ) -class _IndividualVariableNode(IndividualTypeNode): - """The AST type for individual type variables.""" +class _ItemVariableNode(TypeNode): + """The AST type for item type variables.""" def __init__(self, name: Token) -> None: super().__init__(name.start) self._name = name.value + self.children = [] - def to_type( - self, env: Environment - ) -> Tuple[IndividualVariable, Environment]: + def to_type(self, env: Environment) -> Tuple['Variable', Environment]: # QUESTION: Should callers be expected to have already introduced the # name into the context? if self._name in env: ty = env[self._name] - if not isinstance(ty, IndividualVariable): + if not (ty.kind <= ItemKind): error = TypeError( - f'{self._name} is not an individual type variable' + f'{self._name} is not an item type variable (has kind {ty.kind})' ) error.location = self.location raise error return ty, env env = env.copy() - var = IndividualVariable() + var = BoundVariable(ItemKind) env[self._name] = var return var, env @@ -781,6 +1078,7 @@ class _SequenceVariableNode(TypeNode): def __init__(self, name: Token) -> None: super().__init__(name.start) self._name = name.value + self.children = [] def to_type( self, env: Environment @@ -814,22 +1112,23 @@ def __init__( self, location: 'concat.astutils.Location', type_variables: Sequence[ - Union[_IndividualVariableNode, _SequenceVariableNode] + Union[_ItemVariableNode, _SequenceVariableNode] ], ty: TypeNode, ) -> None: super().__init__(location) self._type_variables = type_variables self._type = ty + self.children = list(type_variables) + [ty] - def to_type(self, env: Environment) -> Tuple[Type, Environment]: + def to_type(self, env: Environment) -> Tuple['Type', Environment]: temp_env = env.copy() variables = [] for var in self._type_variables: parameter, temp_env = var.to_type(temp_env) variables.append(parameter) ty, _ = self._type.to_type(temp_env) - forall_type = ForAll(variables, ty) + forall_type = GenericType(variables, ty) return forall_type, env @@ -842,7 +1141,8 @@ def __init__( location: concat.astutils.Location, end_location: concat.astutils.Location, ) -> None: - super().__init__(location, end_location) + super().__init__(location) + self.end_location = end_location self._attribute_type_pairs = attribute_type_pairs def to_type(self, env: Environment) -> Tuple[ObjectType, Environment]: @@ -851,11 +1151,9 @@ def to_type(self, env: Environment) -> Tuple[ObjectType, Environment]: for attribute, type_node in self._attribute_type_pairs: ty, temp_env = type_node.to_type(temp_env) attribute_type_mapping[attribute.value] = ty + # FIXME: Support recursive types in syntax return ( - ObjectType( - self_type=IndividualVariable(), # FIXME: Support recursive types in syntax - attributes=attribute_type_mapping, - ), + ObjectType(attributes=attribute_type_mapping,), env, ) @@ -870,7 +1168,7 @@ def non_star_name_parser() -> Generator: @concat.parser_combinators.generate def named_type_parser() -> Generator: - name_token = yield concat.parse.token('NAME') + name_token = yield non_star_name_parser return NamedTypeNode(name_token.start, name_token.value) @concat.parser_combinators.generate @@ -884,7 +1182,7 @@ def possibly_nullary_generic_type_parser() -> Generator: end_location = (yield concat.parse.token('RSQB')).end return _GenericTypeNode( type_constructor_name.location, - # end_location, + end_location, type_constructor_name, type_arguments, ) @@ -895,7 +1193,7 @@ def individual_type_variable_parser() -> Generator: yield concat.parse.token('BACKTICK') name = yield non_star_name_parser - return _IndividualVariableNode(name) + return _ItemVariableNode(name) @concat.parser_combinators.generate def sequence_type_variable_parser() -> Generator: @@ -907,8 +1205,8 @@ def sequence_type_variable_parser() -> Generator: return _SequenceVariableNode(name) @concat.parser_combinators.generate - def type_sequence_parser() -> Generator: - type = parsers['type'] | individual_type_variable_parser + def stack_effect_type_sequence_parser() -> Generator: + type = parsers['type'] # TODO: Allow type-only items item = concat.parser_combinators.seq( @@ -931,14 +1229,37 @@ def type_sequence_parser() -> Generator: return TypeSequenceNode(location, seq_var_parsed, i) + parsers['stack-effect-type-sequence'] = stack_effect_type_sequence_parser + + @concat.parser_combinators.generate + def type_sequence_parser() -> Generator: + type = parsers['type'] + + item = type.map(lambda t: _TypeSequenceIndividualTypeNode((None, t))) + items = item.many() + + seq_var = sequence_type_variable_parser + seq_var_parsed: Optional[_SequenceVariableNode] + seq_var_parsed = yield seq_var.optional() + i = yield items + + if seq_var_parsed is None and i: + location = i[0].location + elif seq_var_parsed is not None: + location = seq_var_parsed.location + else: + location = None + + return TypeSequenceNode(location, seq_var_parsed, i) + @concat.parser_combinators.generate def stack_effect_type_parser() -> Generator: separator = concat.parse.token('MINUSMINUS') location = (yield concat.parse.token('LPAR')).start - i = yield parsers['type-sequence'] << separator - o = yield parsers['type-sequence'] + i = yield stack_effect_type_sequence_parser << separator + o = yield stack_effect_type_sequence_parser yield concat.parse.token('RPAR') @@ -955,8 +1276,11 @@ def generic_type_parser() -> Generator: type_arguments = yield parsers['type'].sep_by( concat.parse.token('COMMA'), min=1 ) - yield concat.parse.token('RSQB') - return _GenericTypeNode(type.location, type, type_arguments) + end_location = (yield concat.parse.token('RSQB')).end + # TODO: Add end_location to all type nodes + return _GenericTypeNode( + type.location, end_location, type, type_arguments + ) @concat.parser_combinators.generate def forall_type_parser() -> Generator: @@ -974,7 +1298,10 @@ def forall_type_parser() -> Generator: return _ForallTypeNode(forall.start, type_variables, ty) - # TODO: Parse type variables + parsers['type-variable'] = concat.parser_combinators.alt( + sequence_type_variable_parser, individual_type_variable_parser, + ) + parsers['nonparameterized-type'] = concat.parser_combinators.alt( named_type_parser.desc('named type'), parsers.ref_parser('stack-effect-type'), @@ -1000,8 +1327,6 @@ def object_type_parser() -> Generator: individual_type_variable_parser, ).desc('individual type') - # TODO: Parse sequence type variables - parsers['type'] = concat.parser_combinators.alt( # NOTE: There's a parsing ambiguity that might come back to bite me... forall_type_parser.desc('forall type'), @@ -1009,6 +1334,7 @@ def object_type_parser() -> Generator: concat.parse.token('LPAR') >> parsers.ref_parser('type-sequence') << concat.parse.token('RPAR'), + sequence_type_variable_parser, ) parsers['type-sequence'] = type_sequence_parser.desc('type sequence') @@ -1018,88 +1344,69 @@ def object_type_parser() -> Generator: def _generate_type_of_innermost_module( - qualified_name: str, source_dir + qualified_name: str, source_dir: pathlib.Path ) -> StackEffect: - # We resolve imports as if we are the source file. - sys.path, old_path = [source_dir, *sys.path], sys.path - try: - module = importlib.import_module(qualified_name) - except ModuleNotFoundError: - raise TypeError( - 'module {} not found during type checking'.format(qualified_name) - ) - finally: - sys.path = old_path - module_attributes = {} - for name in dir(module): - attribute_type = object_type - if isinstance(getattr(module, name), int): - attribute_type = int_type - elif callable(getattr(module, name)): - attribute_type = py_function_type - module_attributes[name] = attribute_type - module_t = ObjectType( - IndividualVariable(), - module_attributes, - nominal_supertypes=[module_type], + stub_path = _find_stub_path(qualified_name.split('.'), source_dir) + init_env = load_builtins_and_preamble() + module_attributes = _check_stub(stub_path, init_env) + module_type_brand = get_module_type().unroll().brand # type: ignore + brand = Brand( + f'type({qualified_name})', IndividualKind, [module_type_brand] ) + module_t = NominalType(brand, ObjectType(module_attributes)) return StackEffect( - TypeSequence([_seq_var]), TypeSequence([_seq_var, module_type]) + TypeSequence([_seq_var]), TypeSequence([_seq_var, module_t]) ) def _generate_module_type( components: Sequence[str], _full_name: Optional[str] = None, source_dir='.' -) -> ObjectType: +) -> 'Type': if _full_name is None: _full_name = '.'.join(components) if len(components) > 1: - module_t = ObjectType( - IndividualVariable(), - { - components[1]: _generate_module_type( - components[1:], _full_name, source_dir - )[_seq_var,], - }, - nominal_supertypes=[module_type], + module_type_brand = get_module_type().unroll().brand # type: ignore + brand = Brand( + f'type({_full_name})', IndividualKind, [module_type_brand] ) - effect = StackEffect( - TypeSequence([_seq_var]), TypeSequence([_seq_var, module_type]) + module_t = NominalType( + brand, + ObjectType( + { + components[1]: _generate_module_type( + components[1:], _full_name, source_dir + )[_seq_var,], + } + ), ) - return ObjectType( - IndividualVariable(), {'__call__': effect,}, [_seq_var] + effect = StackEffect( + TypeSequence([_seq_var]), TypeSequence([_seq_var, module_t]) ) + return GenericType([_seq_var], effect) else: innermost_type = _generate_type_of_innermost_module( - _full_name, source_dir - ) - return ObjectType( - IndividualVariable(), {'__call__': innermost_type,}, [_seq_var] + _full_name, source_dir=pathlib.Path(source_dir) ) + return GenericType([_seq_var], innermost_type) def _ensure_type( - typename: Optional[TypeNode], env: Environment, obj_name: Optional[str], -) -> Tuple[StackItemType, Environment]: - type: StackItemType - if obj_name and obj_name in env: - type = cast(StackItemType, env[obj_name]) + typename: Optional[TypeNode], + env: Environment, + obj_name: Optional[str], + known_stack_item_names: Environment, +) -> Tuple['Type', Environment]: + type: Type + if obj_name and obj_name in known_stack_item_names: + type = known_stack_item_names[obj_name] elif typename is None: - # NOTE: This could lead type varibles in the output of a function that - # are unconstrained. In other words, it would basically become an Any - # type. - type = IndividualVariable() + type = ItemVariable(ItemKind) elif isinstance(typename, TypeNode): - type, env = cast( - Tuple[StackItemType, Environment], typename.to_type(env) - ) + type, env = typename.to_type(env) else: raise NotImplementedError( 'Cannot turn {!r} into a type'.format(typename) ) if obj_name: - env[obj_name] = type + known_stack_item_names[obj_name] = type return type, env - - -init_primitives() diff --git a/concat/typecheck/builtin_stubs/builtins.cati b/concat/typecheck/builtin_stubs/builtins.cati new file mode 100644 index 00000000..70dea0ac --- /dev/null +++ b/concat/typecheck/builtin_stubs/builtins.cati @@ -0,0 +1,108 @@ +class object: + () + +!@@concat.typecheck.builtin_object object + +class bool: + () + +!@@concat.typecheck.builtin_bool bool + +class int: + def __add__(--) @cast (py_function[(int), int]): + () + + def __invert__(--) @cast (py_function[(), int]): + () + + def __sub__(--) @cast (py_function[(int), str]): + () + + def __le__(--) @cast (py_function[(int), bool]): + () + + def __lt__(--) @cast (py_function[(int), bool]): + () + + def __ge__(--) @cast (py_function[(int), bool]): + () + +!@@concat.typecheck.builtin_int int + +class float: + () + +class slice[`start, `stop, `step]: + () + +class str: + def __getitem__(--) @cast (py_overloaded[ + py_function[(int), str], + py_function[ + (slice[Optional[int], Optional[int], Optional[int]]), + str + ] + ]): + () + + def __add__(--) @cast (py_function[(object), str]): + () + + def find(--) @cast (py_function[(str Optional[int] Optional[int]), int]): + () + + def join(--) @cast (py_function[(str iterable[str]), str]): + () + + def __iter__(--) @cast (py_function[(), iterator[str]]): + () + + def index(--) @cast (py_function[(str Optional[int] Optional[int]), int]): + () + +!@@concat.typecheck.builtin_str str + +def eval(--) @cast (py_function[(str), object]): + () + +def print(--) @cast (py_function[(), none]): + () + +class BaseException: + () + +class Exception($BaseException,): + () + +def input(--) @cast (py_function[(str), str]): + () + +class tuple[`t...]: + # NOTE: Will need a new feature to get the type of __getitem__ right. + def __getitem__(--) @cast (py_function[(int), object]): + () + +!@@concat.typecheck.builtin_tuple tuple + +class dict[`key, `value]: + def __iter__(--) @cast (py_function[(), iterator[`key]]): + () + +class list[`element]: + def __getitem__(--) @cast (py_overloaded[ + py_function[(int), `element], + py_function[ + (slice[Optional[int], Optional[int], Optional[int]]), + list[`element] + ] + ]): + () + + def __iter__(--) @cast (py_function[(), iterator[`element]]): + () + +!@@concat.typecheck.builtin_list list + +# SupportAbs is the name of the protocol in Python +def abs(--) @cast (py_function[(SupportsAbs[`t]), `t]): + () diff --git a/concat/typecheck/builtin_stubs/itertools.cati b/concat/typecheck/builtin_stubs/itertools.cati new file mode 100644 index 00000000..24fea257 --- /dev/null +++ b/concat/typecheck/builtin_stubs/itertools.cati @@ -0,0 +1,6 @@ +def islice(--) @cast (py_overloaded[ + py_function[(iterable[`t] Optional[int]), iterator[`t]], + py_function[(iterable[`t] Optional[int] Optional[int]), iterator[`t]], + py_function[(iterable[`t] Optional[int] Optional[int] Optional[int]), iterator[`t]] # TODO: allow trailing commas +]): + () diff --git a/concat/typecheck/builtin_stubs/types.cati b/concat/typecheck/builtin_stubs/types.cati new file mode 100644 index 00000000..eb89cac9 --- /dev/null +++ b/concat/typecheck/builtin_stubs/types.cati @@ -0,0 +1,4 @@ +class ModuleType: + () + +!@@concat.typecheck.builtin_module ModuleType diff --git a/concat/typecheck/errors.py b/concat/typecheck/errors.py new file mode 100644 index 00000000..93fca271 --- /dev/null +++ b/concat/typecheck/errors.py @@ -0,0 +1,79 @@ +import builtins +import concat.parse +import pathlib +from typing import Optional, Union, TYPE_CHECKING + + +if TYPE_CHECKING: + import concat.astutils + from concat.typecheck.types import Type, TypeSequence + + +class StaticAnalysisError(Exception): + def __init__(self, message: str) -> None: + self.message = message + self.location: Optional['concat.astutils.Location'] = None + self.path: Optional[pathlib.Path] = None + + def set_location_if_missing( + self, location: 'concat.astutils.Location' + ) -> None: + if not self.location: + self.location = location + + def set_path_if_missing(self, path: pathlib.Path) -> None: + if self.path is None: + self.path = path + + def __str__(self) -> str: + return '{} at {}'.format(self.message, self.location) + + +class TypeError(StaticAnalysisError, builtins.TypeError): + pass + + +class NameError(StaticAnalysisError, builtins.NameError): + def __init__( + self, + name: Union['concat.parse.NameWordNode', str], + location: Optional['concat.astutils.Location'] = None, + ) -> None: + if isinstance(name, concat.parse.NameWordNode): + location = name.location + name = name.value + super().__init__(f'name {name!r} not previously defined') + self._name = name + self.location = location + + def __str__(self) -> str: + location_info = '' + if self.location: + location_info = ' (error at {}:{})'.format(*self.location) + return self.message + location_info + + +class AttributeError(TypeError, builtins.AttributeError): + def __init__(self, type: 'Type', attribute: str) -> None: + super().__init__( + 'object of type {} does not have attribute {}'.format( + type, attribute + ) + ) + self._type = type + self._attribute = attribute + + +class StackMismatchError(TypeError): + def __init__( + self, actual: 'TypeSequence', expected: 'TypeSequence' + ) -> None: + super().__init__( + 'The stack here is {}, but sequence type {} was expected'.format( + actual, expected + ) + ) + + +class UnhandledNodeTypeError(builtins.NotImplementedError): + pass diff --git a/concat/typecheck/preamble.cati b/concat/typecheck/preamble.cati new file mode 100644 index 00000000..4c141113 --- /dev/null +++ b/concat/typecheck/preamble.cati @@ -0,0 +1,139 @@ +# FIXME: Exists only at compile time. Should probably be io.FileIO or something +# in typing +class file: + def seek(--) @cast (py_function[(int), int]): + () + + def read(--) @cast (py_function[*any, `any2]): + () + + def __enter__(--) @cast (py_function[*any, `any2]): + () + + def __exit__(--) @cast (py_function[*any, `any2]): + () + +class ellipsis: + () + +class not_implemented: + () + +def to_list(*rest_var i:iterable[`a_var] -- *rest_var l:list[`a_var]): + () + +def py_call(*rest_var kwargs:iterable[object] args:iterable[object] f:py_function[*seq_var, `a_var] -- *rest_var res:`a_var): + () + +def nip(*rest_var a:`_ b:`a_var -- *rest_var b:`a_var): + () + +def nip_2(*rest_var a:`_1 b:`_2 c:`a_var -- *rest_var c:`a_var): + () + +def drop(*rest_var a:`_ -- *rest_var): + () + +def open(*rest_var kwargs:dict[str, object] path:str -- *rest_var f:file): + () + +def to_int(*stack_type_var base:Optional[int] x:object -- *stack_type_var i:int): + () + +# Addition type rules: +# Mypy allows specifying a restrictive operand type and leaves the whole +# NotImplemented thing up to the programmer. See linked_list.py for an example. +# FIXME: Make the rules safer... somehow +# ... a b => (... {__add__(t) -> s} t) +# --- +# a b + => (... s) +# ... a b => (... t {__radd__(t) -> s}) +# --- +# a b + => (... s) +# FIXME: Implement the second type rule +def +(*stack_type_var x:addable[`other, `c_var] y:`other -- *stack_type_var res:`c_var): + () + +# FIXME: We should check if the other operand supports __rsub__ if the +# first operand doesn't support __sub__. +def -(*stack_type_var x:subtractable[`b_var, `c_var] y:`b_var -- *stack_type_var res:`c_var): + () + +def is(*stack_type_var a:object b:object -- *stack_type_var res:bool): + () + +def and(*stack_type_var a:object b:object -- *stack_type_var res:bool): + () + +def or(*stack_type_var a:object b:object -- *stack_type_var res:bool): + () + +# TODO: I should be more careful here, since at least __eq__ can be +# deleted, if I remember correctly. +def ==(*stack_type_var a:object b:object -- *stack_type_var res:bool): + () + +def False(*rest_var -- *rest_var false:bool): + () + +def True(*rest_var -- *rest_var true:bool): + () + +def loop(*rest_var body:(*rest_var -- *rest_var flag:bool) -- *rest_var): + () + +# Rule 1: first operand has __ge__(type(second operand)) +# Rule 2: second operand has __le__(type(first operand)) +# FIXME: Implement the second type rule +def >=(*stack_type_var a:geq_comparable[`b_var, `ret] b:`b_var -- *stack_type_var res:`ret): + () + +# Rule 1: first operand has __lt__(type(second operand)) +# Rule 2: second operand has __gt__(type(first operand)) +# FIXME: Implement the second type rule +# Also look at Python's note about when reflected method get's priority. +def <(*stack_type_var a:lt_comparable[`b_var, `ret] b:`b_var -- *stack_type_var res:`ret): + () + +# FIXME: Implement the second type rule +def <=(*stack_type_var a:leq_comparable[`b_var, `ret] b:`b_var -- *stack_type_var res:`ret): + () + +def choose(*rest_var b:bool t:(*rest_var -- *seq_var) f:(*rest_var -- *seq_var) -- *seq_var): + () + +def if_not(*rest_var b:bool body:(*rest_var -- *rest_var) -- *rest_var): + () + +def if_then(*rest_var b:bool body:(*rest_var -- *rest_var) -- *rest_var): + () + +def swap(*rest_var x:`a_var y:`b_var -- *rest_var y x): + () + +def pick(*rest_var x:`a_var y:`b_var z:`c_var -- *rest_var x y z x): + () + +def dup(*rest_var x:`a_var -- x x): + () + +def over(*rest_var x:`a_var y:`b_var -- *rest_var x y x): + () + +def curry(*rest_var x:`a_var f:(*seq_var x:`a_var -- *stack_var) -- *rest_var g:(*seq_var -- *stack_var)): + () + +def call(*rest_var f:(*rest_var -- *seq_var) -- *seq_var): + () + +def None(*stack_type_var -- *stack_type_var none:none): + () + +def ...(*stack_type_var -- *stack_type_var ...:ellipsis): + () + +def Ellipsis(*stack_type_var -- *stack_type_var ...:ellipsis): + () + +def NotImplemented(*stack_type_var -- *stack_type_var not_impl:not_implemented): + () diff --git a/concat/typecheck/preamble0.cati b/concat/typecheck/preamble0.cati new file mode 100644 index 00000000..71f4baf8 --- /dev/null +++ b/concat/typecheck/preamble0.cati @@ -0,0 +1,4 @@ +class none: + () + +!@@concat.typecheck.builtin_none none diff --git a/concat/typecheck/preamble_types.py b/concat/typecheck/preamble_types.py index 8ca8923c..51fa448b 100644 --- a/concat/typecheck/preamble_types.py +++ b/concat/typecheck/preamble_types.py @@ -1,404 +1,44 @@ from concat.typecheck.types import ( - IndividualVariable, - SequenceVariable, - ForAll, + BoundVariable, + GenericType, + ItemKind, ObjectType, - StackEffect, TypeSequence, addable_type, - base_exception_type, - bool_type, context_manager_type, - dict_type, - ellipsis_type, - file_type, - float_type, geq_comparable_type, - init_primitives, - int_type, iterable_type, + iterator_type, leq_comparable_type, lt_comparable_type, - list_type, - module_type, - none_type, no_return_type, - not_implemented_type, - object_type, optional_type, py_function_type, - str_type, + py_overloaded_type, subscriptable_type, subtractable_type, - tuple_type, ) -init_primitives() -_rest_var = SequenceVariable() -_seq_var = SequenceVariable() -_stack_var = SequenceVariable() -_stack_type_var = SequenceVariable() -_a_var = IndividualVariable() -_b_var = IndividualVariable() -_c_var = IndividualVariable() -_x = IndividualVariable() +_a_var = BoundVariable(ItemKind) types = { - 'py_call': ForAll( - [_rest_var, _seq_var, _a_var], - StackEffect( - TypeSequence( - [ - _rest_var, - iterable_type[object_type,], - iterable_type[object_type,], - py_function_type[TypeSequence([_seq_var]), _a_var], - ] - ), - TypeSequence([_rest_var, _a_var]), - ), - ), - 'swap': ForAll( - [_rest_var, _a_var, _b_var], - StackEffect( - TypeSequence([_rest_var, _a_var, _b_var]), - TypeSequence([_rest_var, _b_var, _a_var]), - ), - ), - 'pick': ForAll( - [_rest_var, _a_var, _b_var, _c_var], - StackEffect( - TypeSequence([_rest_var, _a_var, _b_var, _c_var]), - TypeSequence([_rest_var, _a_var, _b_var, _c_var, _a_var]), - ), - ), - 'nip': ForAll( - [_rest_var, _a_var], - StackEffect( - TypeSequence([_rest_var, object_type, _a_var]), - TypeSequence([_rest_var, _a_var]), - ), - ), - 'nip_2': ObjectType( - _a_var, - { - '__call__': StackEffect( - TypeSequence([_rest_var, object_type, object_type, _b_var]), - TypeSequence([_rest_var, _b_var]), - ) - }, - [_rest_var, _b_var], - ), - 'drop': ForAll( - [_rest_var], - StackEffect( - TypeSequence([_rest_var, object_type]), TypeSequence([_rest_var]) - ), - ), - 'dup': ForAll( - [_rest_var, _a_var], - StackEffect( - TypeSequence([_rest_var, _a_var]), - TypeSequence([_rest_var, _a_var, _a_var]), - ), - ), - 'open': ForAll( - [_rest_var], - StackEffect( - TypeSequence( - [_rest_var, dict_type[str_type, object_type], str_type] - ), - TypeSequence([_rest_var, file_type]), - ), - ), - 'over': ForAll( - [_rest_var, _a_var, _b_var], - StackEffect( - TypeSequence([_rest_var, _a_var, _b_var]), - TypeSequence([_rest_var, _a_var, _b_var, _a_var]), - ), - ), - 'to_list': ForAll( - [_rest_var], - StackEffect( - TypeSequence([_rest_var, iterable_type[_a_var,]]), - TypeSequence([_rest_var, list_type[_a_var,]]), - ), - ), - 'False': ForAll( - [_rest_var], - StackEffect( - TypeSequence([_rest_var]), TypeSequence([_rest_var, bool_type]) - ), - ), - 'curry': ForAll( - [_rest_var, _seq_var, _stack_var, _a_var], - StackEffect( - TypeSequence( - [ - _rest_var, - _a_var, - StackEffect( - TypeSequence([_seq_var, _a_var]), - TypeSequence([_stack_var]), - ), - ] - ), - TypeSequence( - [ - _rest_var, - StackEffect( - TypeSequence([_seq_var]), TypeSequence([_stack_var]) - ), - ] - ), - ), - ), - 'choose': ForAll( - [_rest_var, _seq_var], - StackEffect( - TypeSequence( - [ - _rest_var, - bool_type, - StackEffect( - TypeSequence([_rest_var]), TypeSequence([_seq_var]) - ), - StackEffect( - TypeSequence([_rest_var]), TypeSequence([_seq_var]) - ), - ] - ), - TypeSequence([_seq_var]), - ), - ), - 'if_not': ForAll( - [_rest_var], - StackEffect( - TypeSequence( - [ - _rest_var, - bool_type, - StackEffect( - TypeSequence([_rest_var]), TypeSequence([_rest_var]) - ), - ] - ), - TypeSequence([_rest_var]), - ), - ), - # Python builtins - 'print': py_function_type, - 'Exception': py_function_type, - 'input': py_function_type, - 'if_then': ObjectType( - _x, - { - '__call__': StackEffect( - TypeSequence( - [ - _rest_var, - bool_type, - StackEffect( - TypeSequence([_rest_var]), - TypeSequence([_rest_var]), - ), - ] - ), - TypeSequence([_rest_var]), - ) - }, - [_rest_var], - ), - 'call': ObjectType( - _x, - { - '__call__': StackEffect( - TypeSequence( - [ - _rest_var, - StackEffect( - TypeSequence([_rest_var]), TypeSequence([_seq_var]) - ), - ] - ), - TypeSequence([_seq_var]), - ) - }, - [_rest_var, _seq_var], - ), - 'loop': ForAll( - [_rest_var], - StackEffect( - TypeSequence( - [ - _rest_var, - StackEffect( - TypeSequence([_rest_var]), - TypeSequence([_rest_var, bool_type]), - ), - ] - ), - TypeSequence([_rest_var]), - ), - ), - 'True': ObjectType( - _a_var, - { - '__call__': StackEffect( - TypeSequence([_rest_var]), TypeSequence([_rest_var, bool_type]) - ) - }, - [_rest_var], - ), + 'addable': addable_type, + 'leq_comparable': leq_comparable_type, + 'lt_comparable': lt_comparable_type, + 'geq_comparable': geq_comparable_type, # TODO: Separate type-check-time environment from runtime environment. - # XXX: generalize to_int over the stack - 'to_int': StackEffect( - TypeSequence([_stack_type_var, optional_type[int_type,], object_type]), - TypeSequence([_stack_type_var, int_type]), - ), 'iterable': iterable_type, - 'tuple': tuple_type, - 'BaseException': base_exception_type, 'NoReturn': no_return_type, 'subscriptable': subscriptable_type, 'subtractable': subtractable_type, - 'bool': bool_type, - 'object': object_type, 'context_manager': context_manager_type, - 'dict': dict_type, - 'module': module_type, - 'list': list_type, - 'str': str_type, + 'iterator': iterator_type, 'py_function': py_function_type, + 'py_overloaded': py_overloaded_type, 'Optional': optional_type, - 'int': int_type, - 'float': float_type, - 'file': file_type, - 'none': none_type, - 'None': ForAll( - [_stack_type_var], - StackEffect( - TypeSequence([_stack_type_var]), - TypeSequence([_stack_type_var, none_type]), - ), - ), - '...': ForAll( - [_stack_type_var], - StackEffect( - TypeSequence([_stack_type_var]), - TypeSequence([_stack_type_var, ellipsis_type]), - ), - ), - 'Ellipsis': ForAll( - [_stack_type_var], - StackEffect( - TypeSequence([_stack_type_var]), - TypeSequence([_stack_type_var, ellipsis_type]), - ), - ), - 'NotImplemented': ForAll( - [_stack_type_var], - StackEffect( - TypeSequence([_stack_type_var]), - TypeSequence([_stack_type_var, not_implemented_type]), - ), - ), - # Addition type rules: - # require object_type because the methods should return - # NotImplemented for most types - # FIXME: Make the rules safer... somehow - # ... a b => (... {__add__(object) -> s} t) - # --- - # a b + => (... s) - # ... a b => (... t {__radd__(object) -> s}) - # --- - # a b + => (... s) - # FIXME: Implement the second type rule - '+': ForAll( - [_stack_type_var, _c_var], - StackEffect( - TypeSequence( - [_stack_type_var, addable_type[_c_var,], object_type] - ), - TypeSequence([_stack_type_var, _c_var]), - ), - ), - # FIXME: We should check if the other operand supports __rsub__ if the - # first operand doesn't support __sub__. - '-': ForAll( - [_stack_type_var, _b_var, _c_var], - StackEffect( - TypeSequence( - [_stack_type_var, subtractable_type[_b_var, _c_var], _b_var] - ), - TypeSequence([_stack_type_var, _c_var]), - ), - ), - # Rule 1: first operand has __ge__(type(second operand)) - # Rule 2: second operand has __le__(type(first operand)) - # FIXME: Implement the second type rule - '>=': ForAll( - [_stack_type_var, _b_var], - StackEffect( - TypeSequence( - [_stack_type_var, geq_comparable_type[_b_var,], _b_var] - ), - TypeSequence([_stack_type_var, bool_type]), - ), - ), - # Rule 1: first operand has __lt__(type(second operand)) - # Rule 2: second operand has __gt__(type(first operand)) - # FIXME: Implement the second type rule - # Also look at Python's note about when reflected method get's priority. - '<': ForAll( - [_stack_type_var, _b_var], - StackEffect( - TypeSequence( - [_stack_type_var, lt_comparable_type[_b_var,], _b_var] - ), - TypeSequence([_stack_type_var, bool_type]), - ), - ), - # FIXME: Implement the second type rule - '<=': ForAll( - [_stack_type_var, _b_var], - StackEffect( - TypeSequence( - [_stack_type_var, leq_comparable_type[_b_var,], _b_var] - ), - TypeSequence([_stack_type_var, bool_type]), - ), - ), - 'is': ForAll( - [_stack_type_var], - StackEffect( - TypeSequence([_stack_type_var, object_type, object_type]), - TypeSequence([_stack_type_var, bool_type]), - ), - ), - 'and': ForAll( - [_stack_type_var], - StackEffect( - TypeSequence([_stack_type_var, object_type, object_type]), - TypeSequence([_stack_type_var, bool_type]), - ), - ), - 'or': ForAll( - [_stack_type_var], - StackEffect( - TypeSequence([_stack_type_var, object_type, object_type]), - TypeSequence([_stack_type_var, bool_type]), - ), - ), - # TODO: I should be more careful here, since at least __eq__ can be - # deleted, if I remember correctly. - '==': ForAll( - [_stack_type_var], - StackEffect( - TypeSequence([_stack_type_var, object_type, object_type]), - TypeSequence([_stack_type_var, bool_type]), - ), + 'SupportsAbs': GenericType( + [_a_var], + ObjectType({'__abs__': py_function_type[TypeSequence([]), _a_var],},), ), } diff --git a/concat/typecheck/types.py b/concat/typecheck/types.py index 4a949003..d2886718 100644 --- a/concat/typecheck/types.py +++ b/concat/typecheck/types.py @@ -1,33 +1,31 @@ -from concat.orderedset import OrderedSet -from concat.typecheck import ( - AttributeError, +import abc +from concat.orderedset import InsertionOrderedSet +import concat.typecheck +from concat.typecheck.errors import ( + AttributeError as ConcatAttributeError, StackMismatchError, - TypeError, + StaticAnalysisError, + TypeError as ConcatTypeError, ) -import concat.typecheck +import functools from typing import ( AbstractSet, - Optional, + Any, Dict, Iterable, Iterator, + List, + Mapping, + NoReturn, + Optional, Sequence, + TYPE_CHECKING, Tuple, TypeVar, Union, - List, - Iterator, - Set, - Mapping, - NoReturn, cast, overload, - TYPE_CHECKING, ) -from typing_extensions import Literal -import abc -import collections.abc -from collections import defaultdict if TYPE_CHECKING: @@ -35,44 +33,76 @@ class Type(abc.ABC): - # TODO: Fully replace with <=. - def is_subtype_of(self, supertype: 'Type') -> bool: - return ( - supertype is self - or isinstance(self, IndividualType) - and supertype is object_type - ) + _next_type_id = 0 - def __le__(self, other: object) -> bool: - if not isinstance(other, Type): - return NotImplemented - return self.is_subtype_of(other) + def __init__(self) -> None: + self._free_type_variables_cached: Optional[ + InsertionOrderedSet[Variable] + ] = None + self._internal_name: Optional[str] = None + self._type_id = Type._next_type_id + Type._next_type_id += 1 + + # No <= implementation using subtyping, because variables overload that for + # sort by identity. def __eq__(self, other: object) -> bool: + from concat.typecheck import Substitutions + if self is other: return True if not isinstance(other, Type): return NotImplemented - return self <= other and other <= self + # QUESTION: Define == separately from subtyping code? + ftv = self.free_type_variables() | other.free_type_variables() + try: + subtype_sub = self.constrain_and_bind_variables(other, set(), []) + supertype_sub = other.constrain_and_bind_variables(self, set(), []) + except StaticAnalysisError: + return False + subtype_sub = Substitutions( + {v: t for v, t in subtype_sub.items() if v in ftv} + ) + supertype_sub = Substitutions( + {v: t for v, t in supertype_sub.items() if v in ftv} + ) + return not subtype_sub and not supertype_sub - def get_type_of_attribute(self, name: str) -> 'IndividualType': - raise AttributeError(self, name) + # NOTE: Avoid hashing types. I might I'm having correctness issues related + # to hashing that I'd rather avoid entirely. Maybe one day I'll introduce + # hash consing, but that would only reflect syntactic eequality, and I've + # been using hashing for type equality. + + def get_type_of_attribute(self, name: str) -> 'Type': + attributes = self.attributes + if name not in attributes: + raise ConcatAttributeError(self, name) + return attributes[name] def has_attribute(self, name: str) -> bool: try: self.get_type_of_attribute(name) return True - except AttributeError: + except ConcatAttributeError: return False @abc.abstractproperty def attributes(self) -> Mapping[str, 'Type']: - pass + return {} @abc.abstractmethod - def free_type_variables(self) -> OrderedSet['_Variable']: + def _free_type_variables(self) -> InsertionOrderedSet['Variable']: pass + def free_type_variables(self) -> InsertionOrderedSet['Variable']: + if self._free_type_variables_cached is None: + # Break circular references. Recusring into the same type won't add + # new FTVs, so we can pretend there are none we finish finding the + # others. + self._free_type_variables_cached = InsertionOrderedSet([]) + self._free_type_variables_cached = self._free_type_variables() + return self._free_type_variables_cached + @abc.abstractmethod def apply_substitution( self, _: 'concat.typecheck.Substitutions' @@ -80,55 +110,89 @@ def apply_substitution( pass @abc.abstractmethod - def constrain_and_bind_supertype_variables( + def constrain_and_bind_variables( self, supertype: 'Type', - rigid_variables: AbstractSet['_Variable'], - subtyping_assumptions: List[Tuple['IndividualType', 'IndividualType']], + rigid_variables: AbstractSet['Variable'], + subtyping_assumptions: List[Tuple['Type', 'Type']], ) -> 'Substitutions': + raise NotImplementedError + + def instantiate(self) -> 'Type': + return self + + @abc.abstractproperty + def kind(self) -> 'Kind': pass - @abc.abstractmethod - def constrain_and_bind_subtype_variables( - self, - supertype: 'Type', - rigid_variables: AbstractSet['_Variable'], - subtyping_assumptions: List[Tuple['IndividualType', 'IndividualType']], + def set_internal_name(self, name: str) -> None: + self._internal_name = name + + def __str__(self) -> str: + if self._internal_name is not None: + return self._internal_name + return super().__str__() + + def __getitem__(self, _: Any) -> Any: + raise ConcatTypeError( + f'{self} is neither a generic type nor a sequence type' + ) + + +class IndividualType(Type): + def instantiate(self) -> 'IndividualType': + return cast(IndividualType, super().instantiate()) + + @property + def kind(self) -> 'Kind': + return IndividualKind + + @property + def attributes(self) -> Mapping[str, Type]: + return {} + + +class StuckTypeApplication(IndividualType): + def __init__(self, head: Type, args: 'TypeArguments') -> None: + super().__init__() + self._head = head + self._args = args + + def apply_substitution(self, sub: 'Substitutions') -> Type: + return sub(self._head)[[sub(t) for t in self._args]] + + def constrain_and_bind_variables( + self, supertype, rigid_variables, subtyping_assumptions ) -> 'Substitutions': - pass + from concat.typecheck import Substitutions - # QUESTION: Should I remove this? Should I not distinguish between subtype - # and supertype variables in the other two constraint methods? I should - # look bidirectional typing with polymorphism/generics. Maybe 'Complete and - # Easy'? - def constrain(self, supertype: 'Type') -> None: - if not self.is_subtype_of(supertype): - raise TypeError( - '{} is not a subtype of {}'.format(self, supertype) + if self is supertype or supertype is get_object_type(): + return Substitutions() + if isinstance(supertype, StuckTypeApplication): + # TODO: Variance + return self._head.constrain_and_bind_variables( + supertype._head, rigid_variables, subtyping_assumptions ) + raise ConcatTypeError( + f'Cannot deduce that {self} is a subtype of {supertype} here' + ) - def instantiate(self) -> 'Type': - return self - + def __str__(self) -> str: + if self._internal_name is not None: + return self._internal_name + return f'{self._head}{_iterable_to_str(self._args)}' -class IndividualType(Type, abc.ABC): - def to_for_all(self) -> Type: - return ForAll([], self) + def __repr__(self) -> str: + return f'StuckTypeApplication({self._head!r}, {self._args!r})' - def is_subtype_of(self, supertype: Type) -> bool: - if isinstance(supertype, _OptionalType): - if ( - self == none_type - or not supertype.type_arguments - or isinstance(supertype.type_arguments[0], IndividualType) - and self.is_subtype_of(supertype.type_arguments[0]) - ): - return True - return False - return super().is_subtype_of(supertype) + def _free_type_variables(self) -> InsertionOrderedSet['Variable']: + ftv = self._head.free_type_variables() + for arg in self._args: + ftv |= arg.free_type_variables() + return ftv -class _Variable(Type, abc.ABC): +class Variable(Type, abc.ABC): """Objects that represent type variables. Every type variable object is assumed to be unique. Thus, fresh type @@ -137,452 +201,559 @@ class _Variable(Type, abc.ABC): def apply_substitution( self, sub: 'concat.typecheck.Substitutions' - ) -> Union[IndividualType, '_Variable', 'TypeSequence']: + ) -> Type: if self in sub: - return sub[self] # type: ignore + result = sub[self] + return result # type: ignore return self - def free_type_variables(self) -> OrderedSet['_Variable']: - return OrderedSet({self}) + def _free_type_variables(self) -> InsertionOrderedSet['Variable']: + return InsertionOrderedSet([self]) + def __lt__(self, other) -> bool: + """Comparator for storing variables in OrderedSets.""" + return id(self) < id(other) -class IndividualVariable(_Variable, IndividualType): - def __init__(self) -> None: + def __gt__(self, other) -> bool: + """Comparator for storing variables in OrderedSets.""" + return id(self) > id(other) + + def __eq__(self, other) -> bool: + return self is other + + # NOTE: This hash impl is kept because sets of variables are fine and + # variables are simple. + def __hash__(self) -> int: + """Hash a variable by its identity. + + __hash__ by object identity is used since that's the only way for two + type variables to be ==.""" + + return hash(id(self)) + + @abc.abstractmethod + def freshen(self) -> 'Variable': + pass + + +class BoundVariable(Variable): + def __init__(self, kind: 'Kind') -> None: super().__init__() + self._kind = kind - def constrain_and_bind_supertype_variables( - self, - supertype: Type, - rigid_variables: AbstractSet['_Variable'], - subtyping_assumptions: List[Tuple[IndividualType, IndividualType]], + @property + def kind(self) -> 'Kind': + return self._kind + + def constrain_and_bind_variables( + self, supertype, rigid_variables, subtyping_assumptions ) -> 'Substitutions': from concat.typecheck import Substitutions - if self is supertype or supertype == object_type: + if ( + self._type_id == supertype._type_id + or supertype._type_id == get_object_type()._type_id + or (self, supertype) in subtyping_assumptions + ): return Substitutions() - if not isinstance(supertype, IndividualType): - raise TypeError( - '{} must be an individual type: expected {}'.format( - supertype, self - ) - ) - if self in rigid_variables: - raise TypeError( - '{} is considered fixed here and cannot become a subtype of {}'.format( - self, supertype - ) - ) if ( - isinstance(supertype, IndividualVariable) + isinstance(supertype, Variable) + and self.kind <= supertype.kind and supertype not in rigid_variables ): - return Substitutions({supertype: self}) - # Let's not support bounded quantification or inferring the types of - # named functions. Thus, the subtype constraint should fail here. - raise TypeError( - '{} is an individual type variable and cannot be a subtype of {}'.format( - self, supertype - ) + return Substitutions([(supertype, self)]) + raise ConcatTypeError( + f'Cannot constrain bound variable {self} to {supertype}' ) - def constrain_and_bind_subtype_variables( + def __getitem__(self, args: 'TypeArguments') -> Type: + if not isinstance(self.kind, GenericTypeKind): + raise ConcatTypeError(f'{self} is not a generic type') + if len(self.kind.parameter_kinds) != len(args): + raise ConcatTypeError( + f'{self} was given {len(args)} arguments but expected {len(self.kind.parameter_kinds)}' + ) + for a, p in zip(args, self.kind.parameter_kinds): + if not (a.kind <= p): + raise ConcatTypeError( + f'{a} has kind {a.kind} but expected kind {p}' + ) + return StuckTypeApplication(self, args) + + def __repr__(self) -> str: + return f'' + + def __str__(self) -> str: + return f't_{id(self)}' + + @property + def attributes(self) -> Mapping[str, Type]: + raise TypeError('Cannot get attributes of bound variables') + + def freshen(self) -> 'Variable': + if self._kind <= ItemKind: + return ItemVariable(self._kind) + return SequenceVariable() + + +class ItemVariable(Variable): + def __init__(self, kind: 'Kind') -> None: + super().__init__() + self._kind = kind + + def constrain_and_bind_variables( self, supertype: Type, - rigid_variables: AbstractSet['_Variable'], - subtyping_assumptions: List[Tuple[IndividualType, IndividualType]], + rigid_variables: AbstractSet['Variable'], + subtyping_assumptions: List[Tuple['Type', 'Type']], ) -> 'Substitutions': from concat.typecheck import Substitutions - if self is supertype: + if ( + self is supertype + # QUESTION: subsumption of polytypes? + or self.kind is IndividualKind + and supertype._type_id is get_object_type()._type_id + ): return Substitutions() - if supertype == object_type: - return Substitutions({self: object_type}) - if not isinstance(supertype, IndividualType): - raise TypeError( - '{} must be an individual type: expected {}'.format( - supertype, self + if ( + isinstance(supertype, Variable) + and self.kind <= supertype.kind + and supertype not in rigid_variables + ): + return Substitutions([(supertype, self)]) + mapping: Mapping[Variable, Type] + if self.kind is IndividualKind and isinstance( + supertype, _OptionalType + ): + try: + return self.constrain_and_bind_variables( + supertype.type_arguments[0], + rigid_variables, + subtyping_assumptions, ) - ) - if self in rigid_variables: - raise TypeError( - '{} is considered fixed here and cannot become a subtype of {}'.format( - self, supertype + except ConcatTypeError: + return self.constrain_and_bind_variables( + get_none_type(), rigid_variables, subtyping_assumptions ) + if self in rigid_variables: + raise ConcatTypeError( + f'{self} is considered fixed here and cannot become a subtype of {supertype}' ) - return Substitutions({self: supertype}) - - # __hash__ by object identity is used since that's the only way for two - # type variables to be ==. - def __hash__(self) -> int: - return hash(id(self)) + if self.kind >= supertype.kind: + mapping = {self: supertype} + return Substitutions(mapping) + raise ConcatTypeError( + f'{self} has kind {self.kind}, but {supertype} has kind {supertype.kind}' + ) def __str__(self) -> str: - return '`t_{}'.format(id(self)) + return 't_{}'.format(id(self)) def __repr__(self) -> str: - return ''.format(id(self)) - - def apply_substitution( - self, sub: 'concat.typecheck.Substitutions' - ) -> IndividualType: - return cast(IndividualType, super().apply_substitution(sub)) + return ''.format(id(self)) @property def attributes(self) -> NoReturn: - raise TypeError( - '{} is an individual type variable, so its attributes are unknown'.format( - self - ) + raise ConcatTypeError( + f'{self} is an item type variable, so its attributes are unknown' ) + @property + def kind(self) -> 'Kind': + return self._kind + + def freshen(self) -> 'ItemVariable': + return ItemVariable(self._kind) + -class SequenceVariable(_Variable): +class SequenceVariable(Variable): def __init__(self) -> None: super().__init__() def __str__(self) -> str: return '*t_{}'.format(id(self)) - def __hash__(self) -> int: - return hash(id(self)) + def __repr__(self) -> str: + return f'' - def constrain_and_bind_supertype_variables( + def constrain_and_bind_variables( self, supertype: Type, - rigid_variables: AbstractSet['_Variable'], - subtyping_assumptions: List[Tuple['IndividualType', 'IndividualType']], + rigid_variables: AbstractSet['Variable'], + subtyping_assumptions: List[Tuple['Type', 'Type']], ) -> 'Substitutions': from concat.typecheck import Substitutions if not isinstance(supertype, (SequenceVariable, TypeSequence)): - raise TypeError( + raise ConcatTypeError( '{} must be a sequence type, not {}'.format(self, supertype) ) + if ( + isinstance(supertype, SequenceVariable) + and supertype not in rigid_variables + ): + sub = Substitutions([(supertype, self)]) + sub.add_subtyping_provenance((self, supertype)) + return sub if self in rigid_variables: - raise Exception('todo') + raise ConcatTypeError( + '{} is fixed here and cannot become a subtype of another type'.format( + self + ) + ) # occurs check if self is not supertype and self in supertype.free_type_variables(): - raise TypeError( + raise ConcatTypeError( '{} cannot be a subtype of {} because it appears in {}'.format( self, supertype, supertype ) ) - if isinstance(supertype, SequenceVariable): - return Substitutions({supertype: self}) - return Substitutions() + sub = Substitutions([(self, supertype)]) + sub.add_subtyping_provenance((self, supertype)) + return sub + + @property + def attributes(self) -> NoReturn: + raise ConcatTypeError( + 'the sequence type {} does not hold attributes'.format(self) + ) + + @property + def kind(self) -> 'Kind': + return SequenceKind + + def freshen(self) -> 'SequenceVariable': + return SequenceVariable() - def constrain_and_bind_subtype_variables( + +class GenericType(Type): + def __init__( self, - supertype: Type, - rigid_variables: AbstractSet['_Variable'], - subtyping_assumptions: List[Tuple['IndividualType', 'IndividualType']], - ) -> 'Substitutions': + type_parameters: Sequence['Variable'], + body: Type, + is_variadic: bool = False, + ) -> None: + super().__init__() + assert type_parameters + self._type_parameters = type_parameters + self._body = body + self._instantiations: Dict[Tuple[int, ...], Type] = {} + self.is_variadic = is_variadic + + def __str__(self) -> str: + if self._internal_name is not None: + return self._internal_name + if self.is_variadic: + params = str(self._type_parameters[0]) + '...' + else: + params = ' '.join(map(str, self._type_parameters)) + + return f'forall {params}. {self._body}' + + def __repr__(self) -> str: + return f'{type(self).__qualname__}({self._type_parameters!r}, {self._body!r}, is_variadic={self.is_variadic!r})' + + def __getitem__(self, type_arguments: 'TypeArguments') -> 'Type': from concat.typecheck import Substitutions - if not isinstance(supertype, (SequenceVariable, TypeSequence)): - raise TypeError( - '{} must be a sequence type, not {}'.format(self, supertype) + type_argument_ids = tuple(t._type_id for t in type_arguments) + if type_argument_ids in self._instantiations: + return self._instantiations[type_argument_ids] + expected_kinds = [var.kind for var in self._type_parameters] + if self.is_variadic: + type_arguments = [TypeSequence(type_arguments)] + actual_kinds = [ty.kind for ty in type_arguments] + if len(expected_kinds) != len(actual_kinds) or not ( + expected_kinds >= actual_kinds + ): + raise ConcatTypeError( + f'A type argument to {self} has the wrong kind, type arguments: {type_arguments}, expected kinds: {expected_kinds}' ) - if self in rigid_variables: - raise TypeError( - '{} is fixed here and cannot become a subtype of another type'.format( - self + sub = Substitutions(zip(self._type_parameters, type_arguments)) + instance = sub(self._body) + self._instantiations[type_argument_ids] = instance + if self._internal_name is not None: + instance_internal_name = self._internal_name + instance_internal_name += ( + '[' + ', '.join(map(str, type_arguments)) + ']' + ) + instance.set_internal_name(instance_internal_name) + return instance + + @property + def kind(self) -> 'GenericTypeKind': + kinds = [var.kind for var in self._type_parameters] + return GenericTypeKind(kinds, self._body.kind) + + def instantiate(self) -> Type: + fresh_vars: Sequence[Variable] = [ + var.freshen() for var in self._type_parameters + ] + return self[fresh_vars] + + def constrain_and_bind_variables( + self, + supertype: 'Type', + rigid_variables: AbstractSet['Variable'], + subtyping_assumptions: List[Tuple['Type', 'Type']], + ) -> 'Substitutions': + from concat.typecheck import Substitutions + + if self is supertype or _contains_assumption( + subtyping_assumptions, self, supertype + ): + return Substitutions() + # NOTE: Here, we implement subsumption of polytypes, so the kinds don't + # need to be the same. See concat/poly-subsumption.md for more + # information. + if ( + isinstance(supertype, Variable) + and supertype not in rigid_variables + and self.kind <= supertype.kind + ): + return Substitutions([(supertype, self)]) + if not isinstance(supertype, GenericType): + supertype_parameter_kinds: Sequence[Kind] + if isinstance(supertype.kind, GenericTypeKind): + supertype_parameter_kinds = supertype.kind.parameter_kinds + elif self.kind.result_kind <= supertype.kind: + supertype_parameter_kinds = [] + else: + raise ConcatTypeError( + f'{self} has kind {self.kind} but {supertype} has kind {supertype.kind}' ) + params_to_inst = len(self.kind.parameter_kinds) - len( + supertype_parameter_kinds ) - # occurs check - if self is not supertype and self in supertype.free_type_variables(): - raise TypeError( - '{} cannot be a subtype of {} because it appears in {}'.format( - self, supertype, supertype + param_kinds_left = self.kind.parameter_kinds[ + -len(supertype_parameter_kinds) : + ] + if params_to_inst < 0 or not ( + param_kinds_left >= supertype_parameter_kinds + ): + raise ConcatTypeError( + f'{self} has kind {self.kind} but {supertype} has kind {supertype.kind}' ) + sub = Substitutions( + [ + (t, t.freshen()) + for t in self._type_parameters[:params_to_inst] + ] ) - return Substitutions({self: supertype}) + parameters_left = self._type_parameters[params_to_inst:] + inst: Type + if parameters_left: + inst = GenericType(parameters_left, sub(self._body)) + else: + inst = sub(self._body) + return inst.constrain_and_bind_variables( + supertype, rigid_variables, subtyping_assumptions + ) + # supertype is a GenericType + # QUESTION: Should I care about is_variadic? + if any( + map( + lambda t: t in self.free_type_variables(), + supertype._type_parameters, + ) + ): + raise ConcatTypeError( + f'Type parameters {supertype._type_parameters} cannot appear free in {self}' + ) + return self.instantiate().constrain_and_bind_variables( + supertype._body, + rigid_variables | set(supertype._type_parameters), + subtyping_assumptions, + ) - def get_type_of_attribute(self, name: str) -> NoReturn: - raise TypeError( - 'the sequence type {} does not hold attributes'.format(self) + def apply_substitution(self, sub: 'Substitutions') -> 'GenericType': + from concat.typecheck import Substitutions + + sub = Substitutions( + { + var: ty + for var, ty in sub.items() + if var not in self._type_parameters + } ) + ty = GenericType( + self._type_parameters, + sub(self._body), + is_variadic=self.is_variadic, + ) + return ty @property def attributes(self) -> NoReturn: - raise TypeError( - 'the sequence type {} does not hold attributes'.format(self) + raise ConcatTypeError( + 'Generic types do not have attributes; maybe you forgot type arguments?' ) + def _free_type_variables(self) -> InsertionOrderedSet['Variable']: + return self._body.free_type_variables() - set(self._type_parameters) + -class TypeSequence(Type, Iterable['StackItemType']): - def __init__(self, sequence: Sequence['StackItemType']) -> None: - self._rest: Optional[SequenceVariable] - if sequence and isinstance(sequence[0], SequenceVariable): +class TypeSequence(Type, Iterable[Type]): + def __init__(self, sequence: Sequence[Type]) -> None: + super().__init__() + self._rest: Optional[Variable] + if ( + sequence + and sequence[0].kind is SequenceKind + and isinstance(sequence[0], Variable) + ): self._rest = sequence[0] self._individual_types = sequence[1:] else: self._rest = None self._individual_types = sequence + for ty in self._individual_types: + if ty.kind is SequenceKind: + raise ConcatTypeError(f'{ty} cannot be a sequence type') - def as_sequence(self) -> Sequence['StackItemType']: + def as_sequence(self) -> Sequence[Type]: if self._rest is not None: return [self._rest, *self._individual_types] return self._individual_types def apply_substitution(self, sub) -> 'TypeSequence': + if all(v not in self.free_type_variables() for v in sub): + return self + subbed_types: List[StackItemType] = [] for type in self: - subbed_type: Union[StackItemType, Sequence[StackItemType]] = sub( - type - ) + subbed_type: Union[StackItemType, TypeSequence] = sub(type) if isinstance(subbed_type, TypeSequence): subbed_types += [*subbed_type] else: subbed_types.append(subbed_type) return TypeSequence(subbed_types) - def is_subtype_of(self, supertype: Type) -> bool: - if ( - isinstance(supertype, SequenceVariable) - and not self._individual_types - and self._rest is supertype - ): - return True - elif isinstance(supertype, TypeSequence): - if self._is_empty() and supertype._is_empty(): - return True - elif not self._individual_types: - if ( - self._rest - and supertype._rest - and not supertype._individual_types - ): - return self._rest is supertype._rest - else: - return False - elif self._individual_types and supertype._individual_types: - if ( - not self._individual_types[-1] - <= supertype._individual_types[-1] - ): - return False - return self[:-1] <= supertype[:-1] - else: - return False - else: - raise TypeError( - '{} must be a sequence type, not {}'.format(self, supertype) - ) - - def constrain_and_bind_supertype_variables( + def constrain_and_bind_variables( self, supertype: Type, - rigid_variables: AbstractSet['_Variable'], - subtyping_assumptions: List[Tuple['IndividualType', 'IndividualType']], + rigid_variables: AbstractSet['Variable'], + subtyping_assumptions: List[Tuple['Type', 'Type']], ) -> 'Substitutions': """Check that self is a subtype of supertype. - Free type variables that appear in the supertype type sequence are set - to be equal to their counterparts in the subtype sequence so that type + Free type variables that appear in either type sequence are set to be + equal to their counterparts in the other sequence so that type information can be propagated into calls of named functions. """ from concat.typecheck import Substitutions + if self is supertype or _contains_assumption( + subtyping_assumptions, self, supertype + ): + sub = Substitutions() + sub.add_subtyping_provenance((self, supertype)) + return sub + if isinstance(supertype, SequenceVariable): supertype = TypeSequence([supertype]) if isinstance(supertype, TypeSequence): - if self._is_empty() and supertype._is_empty(): - return Substitutions() - elif ( - self._is_empty() - and supertype._rest - and not supertype._individual_types - and supertype._rest not in rigid_variables - ): - return Substitutions({supertype._rest: self}) - elif ( - supertype._is_empty() - and self._rest - and not self._individual_types - ): - raise StackMismatchError(self, supertype) - elif not self._individual_types: - if ( - self._is_empty() - and supertype._is_empty() - or self._rest is supertype._rest - ): - return Substitutions() - if ( - self._rest - and supertype._rest - and not supertype._individual_types - and supertype._rest not in rigid_variables - ): - return Substitutions({supertype._rest: self._rest}) + if self._is_empty(): + # [] <: [] + if supertype._is_empty(): + sub = Substitutions() + sub.add_subtyping_provenance((self, supertype)) + return sub + # [] <: *a, *a is not rigid + # --> *a = [] elif ( self._is_empty() and supertype._rest and not supertype._individual_types and supertype._rest not in rigid_variables ): - return Substitutions({supertype._rest: self}) + sub = Substitutions([(supertype._rest, self)]) + sub.add_subtyping_provenance((self, supertype)) + return sub + # [] <: *a? `t0 `t... + # error else: raise StackMismatchError(self, supertype) - elif ( - not supertype._individual_types - and supertype._rest - and supertype._rest not in self.free_type_variables() - and supertype._rest not in rigid_variables - ): - return Substitutions({supertype._rest: self}) - elif self._individual_types and supertype._individual_types: - sub = self._individual_types[ - -1 - ].constrain_and_bind_supertype_variables( - supertype._individual_types[-1], - rigid_variables, - subtyping_assumptions, - ) - # constrain individual variables in the second sequence type to - # be *equal* to the corresponding type in the first sequence - # type. - is_variable = isinstance( - supertype._individual_types[-1], IndividualVariable - ) - if ( - is_variable - and supertype._individual_types[-1] not in rigid_variables - ): - sub = Substitutions( - { - supertype._individual_types[ - -1 - ]: self._individual_types[-1] - } - )(sub) - try: - sub = sub( - self[:-1] - ).constrain_and_bind_supertype_variables( - sub(supertype[:-1]), - rigid_variables, - subtyping_assumptions, - )( - sub - ) + if not self._individual_types: + # *a <: [], *a is not rigid + # --> *a = [] + if supertype._is_empty() and self._rest not in rigid_variables: + assert self._rest is not None + sub = Substitutions([(self._rest, supertype)]) + sub.add_subtyping_provenance((self, supertype)) return sub - except StackMismatchError: - raise StackMismatchError(self, supertype) - else: - # TODO: Add info about occurs check and rigid variables. - raise StackMismatchError(self, supertype) - else: - raise TypeError( - '{} must be a sequence type, not {}'.format(self, supertype) - ) - - def constrain_and_bind_subtype_variables( - self, - supertype: Type, - rigid_variables: AbstractSet['_Variable'], - subtyping_assumptions: List[Tuple['IndividualType', 'IndividualType']], - ) -> 'Substitutions': - from concat.typecheck import Substitutions - - if isinstance(supertype, SequenceVariable): - supertype = TypeSequence([supertype]) - - if isinstance(supertype, TypeSequence): - if self._is_empty() and supertype._is_empty(): - return Substitutions() - elif ( - self._is_empty() - and supertype._rest - and not supertype._individual_types - and supertype._rest not in rigid_variables - ): - raise StackMismatchError(self, supertype) - elif ( - supertype._is_empty() - and self._rest - and not self._individual_types - and self._rest not in rigid_variables - ): - return Substitutions({self._rest: supertype}) - elif not self._individual_types: + # *a <: *a if ( - self._is_empty() - and supertype._is_empty() - or self._rest is supertype._rest + self._rest is supertype._rest + and not supertype._individual_types ): - return Substitutions() + sub = Substitutions() + sub.add_subtyping_provenance((self, supertype)) + return sub + # *a <: *b? `t..., *a is not rigid, *a is not free in RHS + # --> *a = RHS if ( self._rest and self._rest not in rigid_variables and self._rest not in supertype.free_type_variables() ): - return Substitutions({self._rest: supertype}) - elif ( - self._is_empty() - and supertype._rest - and not supertype._individual_types - ): - # QUESTION: Should this be allowed? I'm being defensive here. - raise StackMismatchError(self, supertype) - else: - raise StackMismatchError(self, supertype) + sub = Substitutions([(self._rest, supertype)]) + sub.add_subtyping_provenance((self, supertype)) + return sub + # *a? `t... `t_n <: [] + # error + if supertype._is_empty(): + raise StackMismatchError(self, supertype) + # *a? `t... `t_n <: *b, *b is not rigid, *b is not free in LHS + # --> *b = LHS elif ( not supertype._individual_types and supertype._rest and supertype._rest not in self.free_type_variables() and supertype._rest not in rigid_variables ): - raise StackMismatchError(self, supertype) - elif self._individual_types and supertype._individual_types: - sub = self._individual_types[ - -1 - ].constrain_and_bind_subtype_variables( + sub = Substitutions([(supertype._rest, self)]) + sub.add_subtyping_provenance((self, supertype)) + return sub + # `t_n <: `s_m *a? `t... <: *b? `s... + # --- + # *a? `t... `t_n <: *b? `s... `s_m + elif supertype._individual_types: + sub = self._individual_types[-1].constrain_and_bind_variables( supertype._individual_types[-1], rigid_variables, subtyping_assumptions, ) - is_variable = isinstance( - self._individual_types[-1], IndividualVariable - ) - if ( - is_variable - and self._individual_types[-1] not in rigid_variables - ): - sub = Substitutions( - { - self._individual_types[ - -1 - ]: supertype._individual_types[-1] - } - )(sub) try: - sub = sub(self[:-1]).constrain_and_bind_subtype_variables( + sub = sub(self[:-1]).constrain_and_bind_variables( sub(supertype[:-1]), rigid_variables, subtyping_assumptions, )(sub) return sub except StackMismatchError: + # TODO: Add info about occurs check and rigid + # variables. raise StackMismatchError(self, supertype) else: raise StackMismatchError(self, supertype) + raise StackMismatchError(self, supertype) else: - raise TypeError( - '{} must be a sequence type, not {}'.format(self, supertype) + raise ConcatTypeError( + f'{self} is a sequence type, not {supertype}' ) - def free_type_variables(self) -> OrderedSet['_Variable']: - ftv: OrderedSet[_Variable] = OrderedSet([]) + def _free_type_variables(self) -> InsertionOrderedSet['Variable']: + ftv: InsertionOrderedSet[Variable] = InsertionOrderedSet([]) for t in self: ftv |= t.free_type_variables() return ftv @property def attributes(self) -> NoReturn: - raise TypeError( + raise ConcatTypeError( 'the sequence type {} does not hold attributes'.format(self) ) @@ -600,9 +771,7 @@ def __getitem__(self, key: int) -> 'StackItemType': def __getitem__(self, key: slice) -> 'TypeSequence': ... - def __getitem__( - self, key: Union[int, slice] - ) -> Union['StackItemType', 'TypeSequence']: + def __getitem__(self, key: Union[int, slice]) -> Type: if isinstance(key, int): return self.as_sequence()[key] return TypeSequence(self.as_sequence()[key]) @@ -613,17 +782,12 @@ def __str__(self) -> str: def __repr__(self) -> str: return 'TypeSequence([' + ', '.join(repr(t) for t in self) + '])' - def __iter__(self) -> Iterator['StackItemType']: + def __iter__(self) -> Iterator[Type]: return iter(self.as_sequence()) - def __hash__(self) -> int: - return hash(tuple(self.as_sequence())) - - -# TODO: Actually get rid of ForAll uses. This is a temporary measure since I -# don't want to do that work right now. -def ForAll(type_parameters: Sequence['_Variable'], type: Type) -> Type: - return ObjectType(IndividualVariable(), type.attributes, type_parameters,) + @property + def kind(self) -> 'Kind': + return SequenceKind # TODO: Rename to StackEffect at all use sites. @@ -639,122 +803,52 @@ def __iter__(self) -> Iterator['TypeSequence']: return iter((self.input, self.output)) def generalized_wrt(self, gamma: 'Environment') -> Type: - return ObjectType( - IndividualVariable(), - {'__call__': self,}, - list(self.free_type_variables() - gamma.free_type_variables()), + parameters = list( + self.free_type_variables() - gamma.free_type_variables() ) + return GenericType(parameters, self) - def __hash__(self) -> int: - # FIXME: Alpha equivalence - return hash((self.input, self.output)) - - def is_subtype_of( - self, - supertype: Type, - _sub: Optional['concat.typecheck.Substitutions'] = None, - ) -> bool: - if super().is_subtype_of(supertype): - return True - if isinstance(supertype, _Function): - if len(tuple(self.input)) != len(tuple(supertype.input)) or len( - tuple(self.output) - ) != len(tuple(supertype.output)): - return False - # Sequence variables are handled through renaming. - if _sub is None: - _sub = concat.typecheck.Substitutions() - input_rename_result = self._rename_sequence_variable( - tuple(self.input), tuple(supertype.input), _sub - ) - output_rename_result = self._rename_sequence_variable( - tuple(supertype.output), tuple(self.output), _sub - ) - if not (input_rename_result and output_rename_result): - return False - # TODO: What about individual type variables. We should be careful - # with renaming those, too. - # input types are contravariant - for type_from_self, type_from_supertype in zip( - self.input, supertype.input - ): - type_from_self, type_from_supertype = ( - cast(StackItemType, _sub(type_from_self)), - cast(StackItemType, _sub(type_from_supertype)), - ) - if isinstance(type_from_supertype, _Function): - if not type_from_supertype.is_subtype_of( - type_from_self, _sub - ): - return False - elif not type_from_supertype.is_subtype_of(type_from_self): - return False - # output types are covariant - for type_from_self, type_from_supertype in zip( - self.output, supertype.output - ): - type_from_self, type_from_supertype = ( - cast(StackItemType, _sub(type_from_self)), - cast(StackItemType, _sub(type_from_supertype)), - ) - if isinstance(type_from_self, _Function): - if not type_from_self.is_subtype_of( - type_from_supertype, _sub - ): - return False - elif not type_from_self.is_subtype_of(type_from_supertype): - return False - return True - return False - - def constrain_and_bind_supertype_variables( + def constrain_and_bind_variables( self, supertype: Type, - rigid_variables: AbstractSet['_Variable'], - subtyping_assumptions: List[Tuple[IndividualType, IndividualType]], + rigid_variables: AbstractSet['Variable'], + subtyping_assumptions: List[Tuple['Type', 'Type']], ) -> 'Substitutions': from concat.typecheck import Substitutions if ( - isinstance(supertype, IndividualVariable) + self is supertype + or _contains_assumption(subtyping_assumptions, self, supertype) + or supertype._type_id == get_object_type()._type_id + ): + return Substitutions() + + if ( + isinstance(supertype, ItemVariable) + and supertype.kind <= ItemKind and supertype not in rigid_variables ): - return Substitutions({supertype: self}) - if not isinstance(supertype, StackEffect): - raise TypeError( - '{} is not a subtype of {}'.format(self, supertype) + return Substitutions([(supertype, self)]) + if isinstance(supertype, _OptionalType): + return self.constrain_and_bind_variables( + supertype.type_arguments[0], + rigid_variables, + subtyping_assumptions, ) - # Remember that the input should be contravariant! - # QUESTION: Constrain the supertype variables here during contravariance check? - sub = supertype.input.constrain_and_bind_subtype_variables( - self.input, rigid_variables, subtyping_assumptions - ) - sub = sub(self.output).constrain_and_bind_supertype_variables( - sub(supertype.output), rigid_variables, subtyping_assumptions - )(sub) - return sub - - def constrain_and_bind_subtype_variables( - self, - supertype: Type, - rigid_variables: AbstractSet['_Variable'], - subtyping_assumptions: List[Tuple[IndividualType, IndividualType]], - ) -> 'Substitutions': if not isinstance(supertype, StackEffect): - raise TypeError( + raise ConcatTypeError( '{} is not a subtype of {}'.format(self, supertype) ) # Remember that the input should be contravariant! - # QUESTION: Constrain the supertype variables here during contravariance check? - sub = supertype.input.constrain_and_bind_supertype_variables( + sub = supertype.input.constrain_and_bind_variables( self.input, rigid_variables, subtyping_assumptions ) - sub = sub(self.output).constrain_and_bind_subtype_variables( + sub = sub(self.output).constrain_and_bind_variables( sub(supertype.output), rigid_variables, subtyping_assumptions )(sub) return sub - def free_type_variables(self) -> OrderedSet['_Variable']: + def _free_type_variables(self) -> InsertionOrderedSet['Variable']: return ( self.input.free_type_variables() | self.output.free_type_variables() @@ -773,7 +867,9 @@ def _rename_sequence_variable( and isinstance(subtype_list[0], SequenceVariable) ): if supertype_list[0] not in sub: - sub[supertype_list[0]] = subtype_list[0] + # FIXME: Treat sub immutably, or better yet, don't use + # substitutions here if possible + sub._sub[supertype_list[0]] = subtype_list[0] else: if sub(supertype_list[0]) is not subtype_list[0]: return False @@ -789,11 +885,6 @@ def __str__(self) -> str: out_types = ' '.join(map(str, self.output)) return '({} -- {})'.format(in_types, out_types) - def get_type_of_attribute(self, name: str) -> '_Function': - if name == '__call__': - return self - raise AttributeError(self, name) - @property def attributes(self) -> Mapping[str, 'StackEffect']: return {'__call__': self} @@ -811,46 +902,11 @@ class QuotationType(_Function): def __init__(self, fun_type: _Function) -> None: super().__init__(fun_type.input, fun_type.output) - def is_subtype_of( - self, - supertype: Type, - _sub: Optional['concat.typecheck.Substitutions'] = None, - ) -> bool: - if super().is_subtype_of(supertype, _sub): - return True - if supertype == iterable_type: - return True - return False - - def constrain_and_bind_supertype_variables( - self, - supertype: Type, - rigid_variables: AbstractSet['_Variable'], - subtyping_assumptions: List[Tuple[IndividualType, IndividualType]], - ) -> 'Substitutions': - if ( - isinstance(supertype, ObjectType) - and supertype.head == iterable_type - ): - # FIXME: Don't present new variables every time. - # FIXME: Account for the types of the elements of the quotation. - in_var = IndividualVariable() - out_var = IndividualVariable() - quotation_iterable_type = iterable_type[ - StackEffect(TypeSequence([in_var]), TypeSequence([out_var])), - ] - return quotation_iterable_type.constrain_and_bind_supertype_variables( - supertype, rigid_variables, subtyping_assumptions - ) - return super().constrain_and_bind_supertype_variables( - supertype, rigid_variables, subtyping_assumptions - ) - - def constrain_and_bind_subtype_variables( + def constrain_and_bind_variables( self, supertype: Type, - rigid_variables: AbstractSet['_Variable'], - subtyping_assumptions: List[Tuple[IndividualType, IndividualType]], + rigid_variables: AbstractSet['Variable'], + subtyping_assumptions: List[Tuple['Type', 'Type']], ) -> 'Substitutions': if ( isinstance(supertype, ObjectType) @@ -858,15 +914,15 @@ def constrain_and_bind_subtype_variables( ): # FIXME: Don't present new variables every time. # FIXME: Account for the types of the elements of the quotation. - in_var = IndividualVariable() - out_var = IndividualVariable() + in_var = ItemVariable(IndividualKind) + out_var = ItemVariable(IndividualKind) quotation_iterable_type = iterable_type[ StackEffect(TypeSequence([in_var]), TypeSequence([out_var])), ] - return quotation_iterable_type.constrain_and_bind_subtype_variables( + return quotation_iterable_type.constrain_and_bind_variables( supertype, rigid_variables, subtyping_assumptions ) - return super().constrain_and_bind_subtype_variables( + return super().constrain_and_bind_variables( supertype, rigid_variables, subtyping_assumptions ) @@ -881,610 +937,480 @@ def apply_substitution( def free_type_variables_of_mapping( attributes: Mapping[str, Type] -) -> OrderedSet[_Variable]: - ftv: OrderedSet[_Variable] = OrderedSet([]) +) -> InsertionOrderedSet[Variable]: + ftv: InsertionOrderedSet[Variable] = InsertionOrderedSet([]) for sigma in attributes.values(): ftv |= sigma.free_type_variables() return ftv -def init_primitives(): - pass +TypeArguments = Sequence[Type] +_T = TypeVar('_T') -TypeArguments = Sequence[Union[StackItemType, TypeSequence]] -_T = TypeVar('_T') +def _contains_assumption( + assumptions: Sequence[Tuple[Type, Type]], subtype: Type, supertype: Type +) -> bool: + return any( + sub._type_id == subtype._type_id and sup._type_id == supertype._type_id + for sub, sup in assumptions + ) -class ObjectType(IndividualType): - """The representation of types of objects, based on a gradual typing paper. +# The representation of types of objects. + +# Originally, it was based on a gradual typing paper. That paper is "Design and +# Evaluation of Gradual Typing for Python" (Vitousek et al. 2014). But now +# nominal and structural subtyping will be separated internally by using +# brands, like in "Integrating Nominal and Structural Subtyping" (Malayeri & +# Aldrich 2008). + +# http://reports-archive.adm.cs.cmu.edu/anon/anon/home/ftp/usr0/ftp/2008/CMU-CS-08-120.pdf + +# not using functools.total_ordering because == should be only identity. +class Brand: + def __init__( + self, user_name: str, kind: 'Kind', superbrands: Sequence['Brand'] + ) -> None: + self._user_name = user_name + self.kind = kind + self._superbrands = superbrands + + def __str__(self) -> str: + return self._user_name + + def __repr__(self) -> str: + return f'Brand({self._user_name!r}, {self.kind}, {self._superbrands!r})@{id(self)}' + + def __lt__(self, other: 'Brand') -> bool: + object_brand = get_object_type().unroll().brand # type: ignore + return ( + (self is not other and other is object_brand) + or other in self._superbrands + or any(brand <= other for brand in self._superbrands) + ) + + def __le__(self, other: 'Brand') -> bool: + return self is other or self < other + + +class NominalType(Type): + def __init__(self, brand: Brand, ty: Type) -> None: + super().__init__() + + self._brand = brand + self._ty = ty + # TODO: Make sure brands interact with generics properly + + def _free_type_variables(self) -> InsertionOrderedSet[Variable]: + return self._ty.free_type_variables() + + def apply_substitution(self, sub: 'Substitutions') -> 'NominalType': + return NominalType(self._brand, sub(self._ty)) + + @property + def attributes(self) -> Mapping[str, Type]: + return self._ty.attributes + + def constrain_and_bind_variables( + self, supertype, rigid_variables, subtyping_assumptions + ) -> 'Substitutions': + if ( + supertype._type_id == get_object_type()._type_id + or self._type_id == supertype._type_id + or _contains_assumption(subtyping_assumptions, self, supertype) + ): + return concat.typecheck.Substitutions() + if isinstance(supertype, NominalType): + if self._brand <= supertype._brand: + return concat.typecheck.Substitutions() + raise ConcatTypeError(f'{self} is not a subtype of {supertype}') + # TODO: Find a way to force myself to handle these different cases. + # Visitor pattern? singledispatch? + if isinstance(supertype, _OptionalType): + try: + return self.constrain_and_bind_variables( + get_none_type(), rigid_variables, subtyping_assumptions + ) + except ConcatTypeError: + return self.constrain_and_bind_variables( + supertype.type_arguments[0], + rigid_variables, + subtyping_assumptions, + ) + if isinstance(supertype, Fix): + return self.constrain_and_bind_variables( + supertype.unroll(), + rigid_variables, + subtyping_assumptions + [(self, supertype)], + ) + if isinstance(supertype, ForwardTypeReference): + return self.constrain_and_bind_variables( + supertype.resolve_forward_references(), + rigid_variables, + subtyping_assumptions + [(self, supertype)], + ) + if isinstance(supertype, Variable): + if supertype in rigid_variables: + raise ConcatTypeError( + f'{self} is not a subtype of rigid variable {supertype}' + ) + if not (self.kind <= supertype.kind): + raise ConcatTypeError( + f'{self} has kind {self.kind}, but {supertype} has kind {supertype.kind}' + ) + return concat.typecheck.Substitutions([(supertype, self)]) + return self._ty.constrain_and_bind_variables( + supertype, rigid_variables, subtyping_assumptions + ) + + @property + def kind(self) -> 'Kind': + return self._ty.kind + + @property + def brand(self) -> Brand: + return self._brand + + def __str__(self) -> str: + return str(self._brand) + + def __repr__(self) -> str: + return f'NominalType({self._brand!r}, {self._ty!r})' + - That paper is "Design and Evaluation of Gradual Typing for Python" - (Vitousek et al. 2014).""" +class ObjectType(IndividualType): + """Structural record types.""" def __init__( self, - self_type: IndividualVariable, - # Attributes can be universally quantified since ObjectType allows it. - attributes: Dict[str, IndividualType], - type_parameters: Sequence[_Variable] = (), - nominal_supertypes: Sequence[IndividualType] = (), - nominal: bool = False, - _type_arguments: TypeArguments = (), + attributes: Mapping[str, Type], _head: Optional['ObjectType'] = None, - **_other_kwargs, ) -> None: - # There should be no need to make the self_type variable unique because - # it is treated as a bound variable in apply_substitution. In other - # words, it is removed from any substitution received. - self._self_type = self_type + super().__init__() self._attributes = attributes - self._type_parameters = type_parameters - self._nominal_supertypes = nominal_supertypes - self._nominal = nominal - - self._type_arguments: TypeArguments = _type_arguments - self._head = _head or self self._internal_name: Optional[str] = None self._internal_name = self._head._internal_name - self._other_kwargs = _other_kwargs.copy() - if '_type_arguments' in self._other_kwargs: - del self._other_kwargs['_type_arguments'] - if 'nominal' in self._other_kwargs: - del self._other_kwargs['nominal'] - - self._instantiations: Dict[TypeArguments, ObjectType] = {} + @property + def kind(self) -> 'Kind': + return IndividualKind def apply_substitution( - self, - sub: 'concat.typecheck.Substitutions', - _should_quantify_over_type_parameters=True, + self, sub: 'concat.typecheck.Substitutions', ) -> 'ObjectType': - from concat.typecheck import Substitutions + # if no free type vars will be substituted, just return self + if not any(free_var in sub for free_var in self.free_type_variables()): + return self - if _should_quantify_over_type_parameters: - sub = Substitutions( - { - a: i - for a, i in sub.items() - # Don't include self_type in substitution, it is bound. - if a not in self._type_parameters - and a is not self._self_type - } - ) - # if no free type vars will be substituted, just return self - if not any( - free_var in sub for free_var in self.free_type_variables() - ): - return self - else: - sub = Substitutions( - {a: i for a, i in sub.items() if a is not self._self_type} - ) - # if no free type vars will be substituted, just return self - if not any( - free_var in sub - for free_var in { - *self.free_type_variables(), - *self._type_parameters, - } - ): - return self attributes = cast( Dict[str, IndividualType], {attr: sub(t) for attr, t in self._attributes.items()}, ) - nominal_supertypes = [ - sub(supertype) for supertype in self._nominal_supertypes - ] - type_arguments = [ - cast(Union[StackItemType, TypeSequence], sub(type_argument)) - for type_argument in self._type_arguments - ] subbed_type = type(self)( - self._self_type, attributes, - type_parameters=self._type_parameters, - nominal_supertypes=nominal_supertypes, - nominal=self._nominal, - _type_arguments=type_arguments, # head is only used to keep track of where a type came from, so # there's no need to substitute it _head=self._head, - **self._other_kwargs, ) if self._internal_name is not None: subbed_type.set_internal_name(self._internal_name) return subbed_type - def is_subtype_of(self, supertype: 'Type') -> bool: - from concat.typecheck import Substitutions - - if supertype in self._nominal_supertypes or self is supertype: - return True - if isinstance(supertype, (_Function, PythonFunctionType)): - if '__call__' not in self._attributes: - return False - return self._attributes['__call__'] <= supertype - if not isinstance(supertype, ObjectType): - return super().is_subtype_of(supertype) - if self._arity != supertype._arity: - return False - if self._arity == 0 and supertype is object_type: - return True - if supertype._nominal and self._head is not supertype._head: - return False - # instantiate these types in a way such that alpha equivalence is not - # an issue - # NOTE: I assume the parameters are in the same order, which is - # fragile. - parameter_pairs = zip(self.type_parameters, supertype.type_parameters) - if not all(type(a) == type(b) for a, b in parameter_pairs): - return False - self = self.instantiate() - supertype = supertype.instantiate() - parameter_sub = Substitutions( - { - **dict(zip(self.type_arguments, supertype.type_arguments)), - self.self_type: supertype.self_type, - } - ) - self = parameter_sub(self) - - for attr, attr_type in supertype._attributes.items(): - if attr not in self._attributes: - return False - sub = concat.typecheck.Substitutions( - {self._self_type: supertype._self_type} - ) - if not ( - cast(IndividualType, sub(self._attributes[attr])) <= attr_type - ): - return False - return True - - def constrain_and_bind_supertype_variables( + def constrain_and_bind_variables( self, supertype: Type, - rigid_variables: AbstractSet['_Variable'], - subtyping_assumptions: List[Tuple[IndividualType, IndividualType]], + rigid_variables: AbstractSet['Variable'], + subtyping_assumptions: List[Tuple['Type', 'Type']], ) -> 'Substitutions': from concat.typecheck import Substitutions - if (self, supertype) in subtyping_assumptions: - return Substitutions() - + # every object type is a subtype of object_type + if ( + self is supertype + or supertype._type_id == get_object_type()._type_id + or _contains_assumption(subtyping_assumptions, self, supertype) + ): + sub = Substitutions() + sub.add_subtyping_provenance((self, supertype)) + return sub + # obj <: `t, `t is not rigid + # --> `t = obj if ( - isinstance(supertype, IndividualVariable) + isinstance(supertype, Variable) + and supertype.kind >= IndividualKind and supertype not in rigid_variables ): - return Substitutions({supertype: self}) + sub = Substitutions([(supertype, self)]) + sub.add_subtyping_provenance((self, supertype)) + return sub + # obj <: *s? `t... + # error elif isinstance(supertype, (SequenceVariable, TypeSequence)): - raise TypeError( + raise ConcatTypeError( '{} is an individual type, but {} is a sequence type'.format( self, supertype ) ) - # To support higher-rank polymorphism, polymorphic types are subtypes - # of their instances. - - if isinstance(supertype, StackEffect): - subtyping_assumptions.append((self, supertype)) + if not (self.kind <= supertype.kind): + raise ConcatTypeError( + f'{self} has kind {self.kind}, but {supertype} has kind {supertype.kind}' + ) - instantiated_self = self.instantiate() - # We know instantiated_self is not a type constructor here, so - # there's no need to worry about variable binding - return instantiated_self.get_type_of_attribute( + if isinstance(supertype, (StackEffect, PythonFunctionType)): + sub = self.get_type_of_attribute( '__call__' - ).constrain_and_bind_supertype_variables( - supertype, rigid_variables, subtyping_assumptions - ) - if not isinstance(supertype, ObjectType): - raise NotImplementedError(supertype) - if self._arity < supertype._arity: - raise TypeError( - '{} is not as polymorphic as {}'.format(self, supertype) + ).constrain_and_bind_variables( + supertype, + rigid_variables, + subtyping_assumptions + [(self, supertype)], ) - # every object type is a subtype of object_type - if supertype == object_type: - return Substitutions() - # Don't forget that there's nominal subtyping too. - if supertype._nominal: - if ( - supertype not in self._nominal_supertypes - and supertype != self - and self._head != supertype._head - ): - raise TypeError( - '{} is not a subtype of {}'.format(self, supertype) - ) - - subtyping_assumptions.append((self, supertype)) - - # constraining to an optional type - if ( - supertype._head == optional_type - and supertype._arity == 0 - and self._arity == 0 - ): + sub.add_subtyping_provenance((self, supertype)) + return sub + if isinstance(supertype, _OptionalType): try: - return self.constrain_and_bind_supertype_variables( - none_type, rigid_variables, subtyping_assumptions + sub = self.constrain_and_bind_variables( + get_none_type(), + rigid_variables, + subtyping_assumptions + [(self, supertype)], ) - except TypeError: - return self.constrain_and_bind_supertype_variables( - supertype._type_arguments[0], + sub.add_subtyping_provenance((self, supertype)) + return sub + except ConcatTypeError: + sub = self.constrain_and_bind_variables( + supertype.type_arguments[0], rigid_variables, - subtyping_assumptions, + subtyping_assumptions + [(self, supertype)], ) - - # don't constrain the type arguments, constrain those based on - # the attributes - sub = Substitutions() - # We must not bind any type parameters in self or supertype! To support - # higher-rank polymorphism, let's instantiate both types. At this - # point, self should be at least as polymorphic as supertype. - assert self._arity >= supertype._arity - instantiated_self = self.instantiate() - supertype = supertype.instantiate() - for name in supertype._attributes: - type = instantiated_self.get_type_of_attribute(name) - sub = sub(type).constrain_and_bind_supertype_variables( - sub(supertype.get_type_of_attribute(name)), + sub.add_subtyping_provenance((self, supertype)) + return sub + if isinstance(supertype, _NoReturnType): + raise ConcatTypeError( + f'No other type, in this case, {self}, is a subtype of {supertype}' + ) + if isinstance(supertype, Fix): + unrolled = supertype.unroll() + sub = self.constrain_and_bind_variables( + unrolled, rigid_variables, - subtyping_assumptions, - )(sub) - return sub - - def constrain_and_bind_subtype_variables( - self, - supertype: Type, - rigid_variables: AbstractSet['_Variable'], - subtyping_assumptions: List[Tuple[IndividualType, IndividualType]], - ) -> 'Substitutions': - from concat.typecheck import Substitutions - - if (self, supertype) in subtyping_assumptions: - return Substitutions() - - if isinstance(supertype, IndividualVariable): - raise TypeError( - '{} is unknown here and cannot be a supertype of {}'.format( - supertype, self - ) + subtyping_assumptions + [(self, supertype)], ) - elif isinstance(supertype, (SequenceVariable, TypeSequence)): - raise TypeError( - '{} is an individual type, but {} is a sequence type'.format( - self, supertype - ) + sub.add_subtyping_provenance((self, supertype)) + return sub + if isinstance(supertype, ForwardTypeReference): + resolved = supertype.resolve_forward_references() + sub = self.constrain_and_bind_variables( + resolved, + rigid_variables, + subtyping_assumptions + [(self, supertype)], ) - - # To support higher-rank polymorphism, polymorphic types are subtypes - # of their instances. - - if isinstance(supertype, StackEffect): - subtyping_assumptions.append((self, supertype)) - - instantiated_self = self.instantiate() - # We know self is not a type constructor here, so there's no need - # to worry about variable binding - return instantiated_self.get_type_of_attribute( - '__call__' - ).constrain_and_bind_subtype_variables( - supertype, rigid_variables, subtyping_assumptions + sub.add_subtyping_provenance((self, supertype)) + return sub + # Don't forget that there's nominal subtyping too. + if isinstance(supertype, NominalType): + raise concat.typecheck.errors.TypeError( + f'structural type {self} cannot be a subtype of nominal type {supertype}' ) if not isinstance(supertype, ObjectType): - raise NotImplementedError(supertype) - if self._arity < supertype._arity: - raise TypeError( - '{} is not as polymorphic as {}'.format(self, supertype) - ) - # every object type is a subtype of object_type - if supertype == object_type: - return Substitutions() - # Don't forget that there's nominal subtyping too. - if supertype._nominal: - if ( - supertype not in self._nominal_supertypes - and supertype != self - and self._head != supertype._head - ): - raise TypeError( - '{} is not a subtype of {}'.format(self, supertype) - ) - - subtyping_assumptions.append((self, supertype)) - - # constraining to an optional type - if ( - supertype._head == optional_type - and supertype._arity == 0 - and self._arity == 0 - ): - try: - return self.constrain_and_bind_subtype_variables( - none_type, rigid_variables, subtyping_assumptions - ) - except TypeError: - return self.constrain_and_bind_subtype_variables( - supertype._type_arguments[0], - rigid_variables, - subtyping_assumptions, - ) + raise NotImplementedError(repr(supertype)) # don't constrain the type arguments, constrain those based on # the attributes sub = Substitutions() - # We must not bind any type parameters in self or supertype! To support - # higher-rank polymorphism, let's instantiate both types. At this - # point, self should be at least as polymorphic as supertype. - assert self._arity >= supertype._arity - instantiated_self = self.instantiate() - supertype = supertype.instantiate() for name in supertype._attributes: - type = instantiated_self.get_type_of_attribute(name) - sub = type.constrain_and_bind_subtype_variables( - supertype.get_type_of_attribute(name), + type = self.get_type_of_attribute(name) + sub = sub(type).constrain_and_bind_variables( + sub(supertype.get_type_of_attribute(name)), rigid_variables, subtyping_assumptions, )(sub) + sub.add_subtyping_provenance((self, supertype)) return sub - def get_type_of_attribute(self, attribute: str) -> IndividualType: - if attribute not in self._attributes: - raise AttributeError(self, attribute) - - self_sub = concat.typecheck.Substitutions({self._self_type: self}) - - return self_sub(self._attributes[attribute]) - def __repr__(self) -> str: - return '{}({!r}, {!r}, {!r}, {!r}, {!r}, {!r}, {!r})'.format( - type(self).__qualname__, - self._self_type, - self._attributes, - self._type_parameters, - self._nominal_supertypes, - self._nominal, - self._type_arguments, - None if self._head is self else self._head, - ) + head = None if self._head is self else self._head + return f'{type(self).__qualname__}(attributes={self._attributes!r}, _head={head!r})' - def free_type_variables(self) -> OrderedSet[_Variable]: + def _free_type_variables(self) -> InsertionOrderedSet[Variable]: ftv = free_type_variables_of_mapping(self.attributes) - for arg in self.type_arguments: - ftv |= arg.free_type_variables() # QUESTION: Include supertypes? - ftv -= {self.self_type, *self.type_parameters} return ftv def __str__(self) -> str: if self._internal_name is not None: - if len(self._type_arguments) > 0: - return ( - self._internal_name - + '[' - + ', '.join(map(str, self._type_arguments)) - + ']' - ) return self._internal_name - assert self._internal_name is None - return '{}({}, {}, {}, {}, {}, {}, {})'.format( - type(self).__qualname__, - self._self_type, - _mapping_to_str(self._attributes), - _iterable_to_str(self._type_parameters), - _iterable_to_str(self._nominal_supertypes), - self._nominal, - _iterable_to_str(self._type_arguments), - None if self._head is self else self._head, - ) - - def set_internal_name(self, name: str) -> None: - self._internal_name = name - - _hash_variable = None - - def __hash__(self) -> int: - from concat.typecheck import Substitutions - - if ObjectType._hash_variable is None: - ObjectType._hash_variable = IndividualVariable() - sub = Substitutions({self._self_type: ObjectType._hash_variable}) - type_to_hash = sub(self) - return hash( - ( - tuple(type_to_hash._attributes.items()), - tuple(type_to_hash._type_parameters), - tuple(type_to_hash._nominal_supertypes), - type_to_hash._nominal, - # FIXME: I get 'not hashable' errors about this. - # tuple(type_to_hash._type_arguments), - None if type_to_hash._head == self else type_to_hash._head, - ) - ) - - def __getitem__( - self, type_arguments: Sequence[StackItemType] - ) -> 'ObjectType': - from concat.typecheck import Substitutions - - if self._arity != len(type_arguments): - raise TypeError( - 'type constructor {} given {} arguments, expected {} arguments'.format( - self, len(type_arguments), self._arity - ) - ) - - type_arguments = tuple(type_arguments) - if type_arguments in self._instantiations: - return self._instantiations[type_arguments] - - sub = Substitutions(zip(self._type_parameters, type_arguments)) - result = self.apply_substitution( - sub, _should_quantify_over_type_parameters=False - ) - # HACK: We remove the parameters and add arguments through mutation. - result._type_parameters = () - result._type_arguments = type_arguments - - self._instantiations[type_arguments] = result - - return result - - def instantiate(self: _T) -> _T: - # Avoid overwriting the type arguments if type is already instantiated. - if self._arity == 0: - return self - fresh_variables = [type(a)() for a in self._type_parameters] - return self[fresh_variables] + return f'ObjectType({_mapping_to_str(self._attributes)}, {None if self._head is self else self._head})' @property - def attributes(self) -> Dict[str, IndividualType]: + def attributes(self) -> Mapping[str, Type]: return self._attributes - @property - def self_type(self) -> IndividualVariable: - return self._self_type - - @property - def type_arguments(self) -> TypeArguments: - return self._type_arguments - @property def head(self) -> 'ObjectType': return self._head - @property - def type_parameters(self) -> Sequence[_Variable]: - return self._type_parameters - - @property - def nominal_supertypes(self) -> Sequence[IndividualType]: - return self._nominal_supertypes - - @property - def _arity(self) -> int: - return len(self._type_parameters) - +# QUESTION: Should this exist, or should I use ObjectType? class ClassType(ObjectType): """The representation of types of classes, like in "Design and Evaluation of Gradual Typing for Python" (Vitousek et al. 2014).""" - def is_subtype_of(self, supertype: Type) -> bool: + def constrain_and_bind_variables( + self, supertype, rigid_variables, subtyping_assumptions + ) -> 'Substitutions': if ( not supertype.has_attribute('__call__') or '__init__' not in self._attributes ): - return super().is_subtype_of(supertype) - bound_init = self._attributes['__init__'].bind() - return bound_init <= supertype + sub = super().constrain_and_bind_variables( + supertype, rigid_variables, subtyping_assumptions + ) + sub.add_subtyping_provenance((self, supertype)) + return sub + init = self.get_type_of_attribute('__init__') + while not isinstance(init, (StackEffect, PythonFunctionType)): + init = init.get_type_of_attribute('__call__') + bound_init = init.bind() + sub = bound_init.constrain_and_bind_variables( + supertype.get_type_of_attribute('__call__'), + rigid_variables, + subtyping_assumptions + [(self, supertype)], + ) + sub.add_subtyping_provenance((self, supertype)) + return sub -class PythonFunctionType(ObjectType): +class PythonFunctionType(IndividualType): def __init__( self, - self_type: IndividualVariable, - *args, - _overloads: Sequence[ - Tuple[Sequence[StackItemType], IndividualType] - ] = (), - type_parameters=(), - **kwargs, + _overloads: Sequence[Tuple[Type, Type]] = (), + type_parameters: Sequence[Variable] = (), + _type_arguments: Sequence[Type] = (), ) -> None: - self._kwargs = kwargs.copy() - # HACK: I shouldn't have to manipulate arguments like this - if 'type_parameters' in self._kwargs: - del self._kwargs['type_parameters'] - super().__init__( - self_type, - *args, - **self._kwargs, - _overloads=_overloads, - type_parameters=type_parameters, - ) - assert ( + super().__init__() + self._arity = len(type_parameters) + self._type_parameters = type_parameters + self._type_arguments: Sequence[Type] = [] + self._overloads: Sequence[Tuple[Type, Type]] = [] + if not ( self._arity == 0 - and len(self._type_arguments) == 2 + and len(_type_arguments) == 2 or self._arity == 2 - and len(self._type_arguments) == 0 - ) + and len(_type_arguments) == 0 + ): + raise ConcatTypeError( + f'Ill-formed Python function type with arguments {_type_arguments}' + ) if self._arity == 0: - assert isinstance(self.input, collections.abc.Sequence) - self._args = list(args) - self._overloads = _overloads - if '_head' in self._kwargs: - del self._kwargs['_head'] - self._head: PythonFunctionType + i, o = _type_arguments + if i.kind != SequenceKind: + raise ConcatTypeError( + f'{i} must be a sequence type, but has kind {i.kind}' + ) + # HACK: Sequence variables are introduced by the type sequence AST nodes + if isinstance(i, TypeSequence) and i and i[0].kind == SequenceKind: + i = TypeSequence(i.as_sequence()[1:]) + _type_arguments = i, o + if not (o.kind <= ItemKind): + raise ConcatTypeError( + f'{o} must be an item type, but has kind {o.kind}' + ) + _fixed_overloads: List[Tuple[Type, Type]] = [] + for i, o in _overloads: + if i.kind != SequenceKind: + raise ConcatTypeError( + f'{i} must be a sequence type, but has kind {i.kind}' + ) + if ( + isinstance(i, TypeSequence) + and i + and i[0].kind == SequenceKind + ): + i = TypeSequence(i.as_sequence()[1:]) + if not (o.kind <= ItemKind): + raise ConcatTypeError( + f'{o} must be an item type, but has kind {o.kind}' + ) + _fixed_overloads.append((i, o)) + self._overloads = _fixed_overloads + self._type_arguments = _type_arguments + + def _free_type_variables(self) -> InsertionOrderedSet[Variable]: + if self._arity == 0: + ftv = self.input.free_type_variables() + ftv |= self.output.free_type_variables() + return ftv + else: + return InsertionOrderedSet([]) + + @property + def kind(self) -> 'Kind': + if self._arity == 0: + return IndividualKind + return GenericTypeKind([SequenceKind, IndividualKind], IndividualKind) + + def __repr__(self) -> str: + # QUESTION: Is it worth using type(self)? + return f'{type(self).__qualname__}(_overloads={self._overloads!r}, type_parameters={self._type_parameters!r}, _type_arguments={self._type_arguments})' def __str__(self) -> str: if not self._type_arguments: return 'py_function_type' - return 'py_function_type[{}, {}]'.format( - _iterable_to_str(self.input), self.output - ) - - def get_type_of_attribute(self, attribute: str) -> IndividualType: - from concat.typecheck import Substitutions + return f'py_function_type[{self.input}, {self.output}]' - sub = Substitutions({self._self_type: self}) - if attribute == '__call__': - return self - else: - return super().get_type_of_attribute(attribute) + @property + def attributes(self) -> Mapping[str, Type]: + return {**super().attributes, '__call__': self} def __getitem__( - self, arguments: Tuple[TypeSequence, IndividualType] + self, arguments: Tuple[Type, Type] ) -> 'PythonFunctionType': - assert self._arity == 2 + if self._arity != 2: + raise ConcatTypeError(f'{self} is not a generic type') + if len(arguments) != 2: + raise ConcatTypeError( + f'{self} takes two arguments, got {len(arguments)}' + ) input = arguments[0] output = arguments[1] + if input.kind != SequenceKind: + raise ConcatTypeError( + f'First argument to {self} must be a sequence type of function arguments' + ) + if not (output.kind <= ItemKind): + raise ConcatTypeError( + f'Second argument to {self} (the return type) must be an item type' + ) return PythonFunctionType( - self._self_type, - *self._args, - **{ - **self._kwargs, - '_type_arguments': (input, output), - 'type_parameters': (), - }, - _overloads=[], - _head=self, + _type_arguments=(input, output), type_parameters=(), _overloads=[], ) def apply_substitution( self, sub: 'concat.typecheck.Substitutions' ) -> 'PythonFunctionType': if self._arity == 0: - type = py_function_type[ - sub(TypeSequence(self.input)), sub(self.output) + inp = sub(self.input) + out = sub(self.output) + overloads: Sequence[Tuple[Type, Type]] = [ + (sub(i), sub(o)) for i, o in self._overloads ] - for overload in self._overloads: - # This is one of the few places where a type should be mutated. - type._add_overload( - [sub(i) for i in overload[0]], sub(overload[1]) - ) - return type + return PythonFunctionType( + _type_arguments=(inp, out), _overloads=overloads + ) return self @property - def input(self) -> Sequence[StackItemType]: + def input(self) -> Type: assert self._arity == 0 - if isinstance(self._type_arguments[0], SequenceVariable): - return (self._type_arguments[0],) - assert not isinstance(self._type_arguments[0], IndividualType) - return tuple(self._type_arguments[0]) + return self._type_arguments[0] @property - def output(self) -> IndividualType: + def output(self) -> Type: assert self._arity == 0 - assert isinstance(self._type_arguments[1], IndividualType) return self._type_arguments[1] def select_overload( @@ -1492,186 +1418,199 @@ def select_overload( ) -> Tuple['PythonFunctionType', 'Substitutions']: for overload in [(self.input, self.output), *self._overloads]: try: - sub = TypeSequence( - input_types - ).constrain_and_bind_supertype_variables( - TypeSequence(overload[0]), set(), [] + sub = TypeSequence(input_types).constrain_and_bind_variables( + overload[0], set(), [] ) except TypeError: continue return ( - sub(py_function_type[TypeSequence(overload[0]), overload[1]]), + sub(py_function_type[overload]), sub, ) - raise TypeError( + raise ConcatTypeError( 'no overload of {} matches types {}'.format(self, input_types) ) - def with_overload( - self, input: Sequence[StackItemType], output: IndividualType - ) -> 'PythonFunctionType': + def with_overload(self, input: Type, output: Type) -> 'PythonFunctionType': return PythonFunctionType( - self._self_type, - *self._args, - **self._kwargs, + _type_arguments=self._type_arguments, _overloads=[*self._overloads, (input, output)], - _head=py_function_type, ) - def _add_overload( - self, input: Sequence[StackItemType], output: IndividualType - ) -> None: - self._overloads.append((input, output)) - def bind(self) -> 'PythonFunctionType': assert self._arity == 0 inputs = self.input[1:] output = self.output - return self._head[TypeSequence(inputs), output] - - def is_subtype_of(self, supertype: Type) -> bool: - if isinstance(supertype, PythonFunctionType): - # NOTE: make sure types are of same kind (arity) - if len(self._type_parameters) != len(supertype._type_parameters): - return False - if len(self._type_parameters) == 2: - # both are py_function_type - return True - assert isinstance(supertype._type_arguments[0], TypeSequence) - assert isinstance(self._type_arguments[1], IndividualType) - return ( - supertype._type_arguments[0] <= self._type_arguments[0] - and self._type_arguments[1] <= supertype._type_arguments[1] - ) - else: - return super().is_subtype_of(supertype) + overloads = [(i[1:], o) for i, o in self._overloads] + return PythonFunctionType( + _type_arguments=[TypeSequence(inputs), output], + _overloads=overloads, + ) - def constrain_and_bind_supertype_variables( + def constrain_and_bind_variables( self, supertype: Type, - rigid_variables: AbstractSet['_Variable'], - subtyping_assumptions: List[Tuple[IndividualType, IndividualType]], + rigid_variables: AbstractSet['Variable'], + subtyping_assumptions: List[Tuple['Type', 'Type']], ) -> 'Substitutions': from concat.typecheck import Substitutions - sub = super().constrain_and_bind_supertype_variables( - supertype, rigid_variables, subtyping_assumptions - ) - - if ( - isinstance(supertype, PythonFunctionType) - and supertype._arity <= self._arity + if self is supertype or _contains_assumption( + subtyping_assumptions, self, supertype ): - instantiated_self = self.instantiate() - supertype = supertype.instantiate() - - # ObjectType constrains the attributes, not the type arguments - # directly, so we'll doo that here. This isn't problematic because - # we know the variance of the arguments here. - - # No need to extend the rigid variables, we know both types have no - # parameters at this point. - - # Support overloading the subtype. - for overload in [ - (instantiated_self.input, instantiated_self.output), - *instantiated_self._overloads, - ]: - try: - subtyping_assumptions_copy = subtyping_assumptions[:] - self_input_types = TypeSequence(overload[0]) - supertype_input_types = TypeSequence(supertype.input) - sub = supertype_input_types.constrain_and_bind_subtype_variables( - self_input_types, - rigid_variables, - subtyping_assumptions_copy, - )( - sub + sub = Substitutions() + sub.add_subtyping_provenance((self, supertype)) + return sub + if not (self.kind <= supertype.kind): + raise ConcatTypeError( + f'{self} has kind {self.kind} but {supertype} has kind {supertype.kind}' + ) + if self.kind is IndividualKind: + if supertype is get_object_type(): + sub = Substitutions() + sub.add_subtyping_provenance((self, supertype)) + return sub + if ( + isinstance(supertype, ItemVariable) + and supertype.kind is IndividualKind + and supertype not in rigid_variables + ): + sub = Substitutions([(supertype, self)]) + sub.add_subtyping_provenance((self, supertype)) + return sub + if isinstance(supertype, _OptionalType): + sub = self.constrain_and_bind_variables( + supertype.type_arguments[0], + rigid_variables, + subtyping_assumptions, + ) + sub.add_subtyping_provenance((self, supertype)) + return sub + if isinstance(supertype, ObjectType): + sub = Substitutions() + for attr in supertype.attributes: + self_attr_type = sub(self.get_type_of_attribute(attr)) + supertype_attr_type = sub( + supertype.get_type_of_attribute(attr) ) - sub = sub( - instantiated_self.output - ).constrain_and_bind_supertype_variables( - sub(supertype.output), + sub = self_attr_type.constrain_and_bind_variables( + supertype_attr_type, rigid_variables, - subtyping_assumptions_copy, - )( - sub + subtyping_assumptions, ) - except TypeError: - continue - finally: - subtyping_assumptions[:] = subtyping_assumptions_copy - return sub + sub.add_subtyping_provenance((self, supertype)) + return sub + if isinstance(supertype, PythonFunctionType): + # No need to extend the rigid variables, we know both types have no + # parameters at this point. + + # Support overloading the subtype. + exceptions = [] + for overload in [ + (self.input, self.output), + *self._overloads, + ]: + try: + subtyping_assumptions_copy = subtyping_assumptions[:] + self_input_types = overload[0] + supertype_input_types = supertype.input + sub = supertype_input_types.constrain_and_bind_variables( + self_input_types, + rigid_variables, + subtyping_assumptions_copy, + ) + sub = sub(self.output).constrain_and_bind_variables( + sub(supertype.output), + rigid_variables, + subtyping_assumptions_copy, + )(sub) + sub.add_subtyping_provenance((self, supertype)) + return sub + except ConcatTypeError as e: + exceptions.append(e) + finally: + subtyping_assumptions[:] = subtyping_assumptions_copy + raise ConcatTypeError( + 'no overload of {} is a subtype of {}'.format( + self, supertype + ) + ) from exceptions[0] + raise ConcatTypeError(f'{self} is not a subtype of {supertype}') + # TODO: Remove generic type responsibility from this class + if isinstance(supertype, PythonFunctionType) and isinstance( + supertype.kind, GenericTypeKind + ): + sub = Substitutions() + sub.add_subtyping_provenance((self, supertype)) + return sub + raise ConcatTypeError(f'{self} is not a subtype of {supertype}') - raise TypeError( - 'no overload of {} is a subtype of {}'.format(self, supertype) - ) - def constrain_and_bind_subtype_variables( +class _PythonOverloadedType(Type): + def __init__(self) -> None: + super().__init__() + + def __getitem__(self, args: Sequence[Type]) -> 'PythonFunctionType': + if len(args) == 0: + raise ConcatTypeError( + 'py_overloaded must be applied to at least one argument' + ) + fun_type = args[0] + if not isinstance(fun_type, PythonFunctionType): + raise ConcatTypeError( + 'Arguments to py_overloaded must be Python function types' + ) + for arg in args[1:]: + if not isinstance(arg, PythonFunctionType): + raise ConcatTypeError( + 'Arguments to py_overloaded must be Python function types' + ) + fun_type = fun_type.with_overload(arg.input, arg.output) + return fun_type + + @property + def attributes(self) -> Mapping[str, 'Type']: + raise ConcatTypeError('py_overloaded does not have attributes') + + def _free_type_variables(self) -> InsertionOrderedSet['Variable']: + return InsertionOrderedSet([]) + + def apply_substitution( + self, _: 'concat.typecheck.Substitutions' + ) -> '_PythonOverloadedType': + return self + + def instantiate(self) -> PythonFunctionType: + return self[ + py_function_type.instantiate(), + ] + + def constrain_and_bind_variables( self, - supertype: Type, - rigid_variables: AbstractSet['_Variable'], - subtyping_assumptions: List[Tuple[IndividualType, IndividualType]], + supertype: 'Type', + rigid_variables: AbstractSet['Variable'], + subtyping_assumptions: List[Tuple['Type', 'Type']], ) -> 'Substitutions': - from concat.typecheck import Substitutions + raise ConcatTypeError('py_overloaded is a generic type') - sub = super().constrain_and_bind_subtype_variables( - supertype, rigid_variables, subtyping_assumptions - ) + @property + def kind(self) -> 'Kind': + return GenericTypeKind([SequenceKind], IndividualKind) - if ( - isinstance(supertype, PythonFunctionType) - and supertype._arity <= self._arity - ): - instantiated_self = self.instantiate() - supertype = supertype.instantiate() + def __eq__(self, other: object) -> bool: + return isinstance(other, type(self)) - # ObjectType constrains the attributes, not the type arguments - # directly, so we'll doo that here. This isn't problematic because - # we know the variance of the arguments here. - for overload in [ - (instantiated_self.input, instantiated_self.output), - *instantiated_self._overloads, - ]: - try: - subtyping_assumptions_copy = subtyping_assumptions[:] - self_input_types = TypeSequence(overload[0]) - supertype_input_types = TypeSequence(supertype.input) - sub = supertype_input_types.constrain_and_bind_supertype_variables( - self_input_types, - rigid_variables, - subtyping_assumptions_copy, - )( - sub - ) - sub = sub( - instantiated_self.output - ).constrain_and_bind_subtype_variables( - sub(supertype.output), - rigid_variables, - subtyping_assumptions_copy, - )( - sub - ) - except TypeError: - continue - finally: - subtyping_assumptions[:] = subtyping_assumptions_copy - return sub - - raise TypeError( - 'no overload of {} is a subtype of {}'.format(self, supertype) - ) +py_overloaded_type = _PythonOverloadedType() -class _NoReturnType(ObjectType): - def __init__(self) -> None: - x = IndividualVariable() - super().__init__(x, {}) +class _NoReturnType(IndividualType): + def constrain_and_bind_variables( + self, supertype, rigid_variables, subtyping_assumptions + ) -> 'Substitutions': + from concat.typecheck import Substitutions - def is_subtype_of(self, _: Type) -> Literal[True]: - return True + return Substitutions() def apply_substitution( self, sub: 'concat.typecheck.Substitutions' @@ -1681,27 +1620,386 @@ def apply_substitution( def __repr__(self) -> str: return '{}()'.format(type(self).__qualname__) + def _free_type_variables(self) -> InsertionOrderedSet['Variable']: + return InsertionOrderedSet([]) -class _OptionalType(ObjectType): - def __init__(self, _type_arguments=[]) -> None: - x = IndividualVariable() - type_var = IndividualVariable() - if len(_type_arguments) > 0: - super().__init__(x, {}, [], _type_arguments=_type_arguments) - else: - super().__init__(x, {}, [type_var]) - def __getitem__( - self, type_arguments: Sequence[StackItemType] - ) -> '_OptionalType': - assert len(type_arguments) == 1 - return _OptionalType(type_arguments) +class _OptionalType(IndividualType): + def __init__(self, type_argument: Type) -> None: + super().__init__() + if not (type_argument.kind <= ItemKind): + raise ConcatTypeError( + f'{type_argument} must be an item type, but has kind {type_argument.kind}' + ) + while isinstance(type_argument, _OptionalType): + type_argument = type_argument._type_argument + self._type_argument: Type = type_argument + + def __repr__(self) -> str: + return f'{type(self).__qualname__}({self._type_argument!r})' + + def __str__(self) -> str: + return f'optional_type[{self._type_argument}]' + + def _free_type_variables(self) -> InsertionOrderedSet[Variable]: + return self._type_argument.free_type_variables() + + def __eq__(self, other: object) -> bool: + if isinstance(other, _OptionalType): + return self._type_argument == other._type_argument + return super().__eq__(other) + + def constrain_and_bind_variables( + self, supertype, rigid_variables, subtyping_assumptions + ) -> 'Substitutions': + from concat.typecheck import Substitutions + + if ( + self is supertype + or _contains_assumption(subtyping_assumptions, self, supertype) + or supertype is get_object_type() + ): + return Substitutions() + # A special case for better resuls (I think) + if isinstance(supertype, _OptionalType): + return self._type_argument.constrain_and_bind_variables( + supertype._type_argument, + rigid_variables, + subtyping_assumptions, + ) + if self.kind != supertype.kind: + raise ConcatTypeError( + f'{self} is an individual type, but {supertype} has kind {supertype.kind}' + ) + # FIXME: optional[none] should simplify to none + if ( + self._type_argument is get_none_type() + and supertype is get_none_type() + ): + return Substitutions() + + sub = get_none_type().constrain_and_bind_variables( + supertype, rigid_variables, subtyping_assumptions + ) + sub = sub(self._type_argument).constrain_and_bind_variables( + sub(supertype), rigid_variables, subtyping_assumptions + ) + return sub def apply_substitution( self, sub: 'concat.typecheck.Substitutions' ) -> '_OptionalType': - # FIXME: self._type_arguments might not be a valid stack type. - return _OptionalType(tuple(sub(TypeSequence(self._type_arguments)))) + return _OptionalType(sub(self._type_argument)) + + @property + def type_arguments(self) -> Sequence[Type]: + return [self._type_argument] + + +# FIXME: Not a total order, using total_ordering might be very unsound. +@functools.total_ordering +class Kind(abc.ABC): + @abc.abstractmethod + def __eq__(self, other: object) -> bool: + pass + + @abc.abstractmethod + def __lt__(self, other: 'Kind') -> bool: + pass + + @abc.abstractmethod + def __str__(self) -> str: + pass + + +class _ItemKind(Kind): + __instance: Optional['_ItemKind'] = None + + def __new__(cls) -> '_ItemKind': + if cls.__instance is None: + cls.__instance = super().__new__(cls) + return cls.__instance + + def __eq__(self, other: object) -> bool: + return self is other + + def __lt__(self, other: Kind) -> bool: + return False + + def __str__(self) -> str: + return 'Item' + + +ItemKind = _ItemKind() + + +class _IndividualKind(Kind): + __instance: Optional['_IndividualKind'] = None + + def __new__(cls) -> '_IndividualKind': + if cls.__instance is None: + cls.__instance = super().__new__(cls) + return cls.__instance + + def __eq__(self, other: object) -> bool: + return self is other + + def __lt__(self, other: Kind) -> bool: + return other is ItemKind + + def __str__(self) -> str: + return 'Individual' + + +IndividualKind = _IndividualKind() + + +class _SequenceKind(Kind): + __instance: Optional['_SequenceKind'] = None + + def __new__(cls) -> '_SequenceKind': + if cls.__instance is None: + cls.__instance = super().__new__(cls) + return cls.__instance + + def __eq__(self, other: object) -> bool: + return self is other + + def __lt__(self, other: Kind) -> bool: + return other is ItemKind + + def __str__(self) -> str: + return 'Sequence' + + +SequenceKind = _SequenceKind() + + +class GenericTypeKind(Kind): + def __init__( + self, parameter_kinds: Sequence[Kind], result_kind: Kind + ) -> None: + if not parameter_kinds: + raise ConcatTypeError( + 'Generic type kinds cannot have empty parameters' + ) + self.parameter_kinds = parameter_kinds + self.result_kind = result_kind + + def __eq__(self, other: object) -> bool: + return ( + isinstance(other, GenericTypeKind) + and list(self.parameter_kinds) == list(other.parameter_kinds) + and self.result_kind == other.result_kind + ) + + def __lt__(self, other: Kind) -> bool: + if not isinstance(other, Kind): + return NotImplemented + if other is ItemKind: + return True + if not isinstance(other, GenericTypeKind): + return False + if len(self.parameter_kinds) != len(other.parameter_kinds): + return False + return ( + list(self.parameter_kinds) > list(other.parameter_kinds) + and self.result_kind < other.result_kind + ) + + def __str__(self) -> str: + return f'Generic[{", ".join(map(str, self.parameter_kinds))}, {self.result_kind}]' + + +class Fix(Type): + def __init__(self, var: Variable, body: Type) -> None: + super().__init__() + assert var.kind == body.kind + self._var = var + self._body = body + self._unrolled_ty: Optional[Type] = None + self._cache: Dict[int, Type] = {} + + def __repr__(self) -> str: + return f'Fix({self._var!r}, {self._body!r})' + + def __str__(self) -> str: + if self._internal_name is not None: + return self._internal_name + return f'Fix({self._var}, {self._body})' + + def _apply(self, t: Type) -> Type: + from concat.typecheck import Substitutions + + if t._type_id not in self._cache: + sub = Substitutions([(self._var, t)]) + self._cache[t._type_id] = sub(self._body) + assert ( + self._var not in self._cache[t._type_id].free_type_variables() + ) + return self._cache[t._type_id] + + def unroll(self) -> Type: + if self._unrolled_ty is None: + self._unrolled_ty = self._apply(self) + if self._internal_name is not None: + self._unrolled_ty.set_internal_name(self._internal_name) + # Do not make the type ids equal so that subtyping assumptions are + # useful + return self._unrolled_ty + + def _free_type_variables(self) -> InsertionOrderedSet[Variable]: + return self._body.free_type_variables() - {self._var} + + def apply_substitution(self, sub: 'Substitutions') -> Type: + from concat.typecheck import Substitutions + + if all(v not in self.free_type_variables() for v in sub): + return self + sub = Substitutions( + {v: t for v, t in sub.items() if v is not self._var} + ) + + return Fix(self._var, sub(self._body)) + + @property + def attributes(self) -> Mapping[str, Type]: + return self.unroll().attributes + + def constrain_and_bind_variables( + self, supertype, rigid_variables, subtyping_assumptions + ) -> 'Substitutions': + from concat.typecheck import Substitutions + + if supertype._type_id == get_object_type()._type_id or _contains_assumption( + subtyping_assumptions, self, supertype + ): + sub = Substitutions() + sub.add_subtyping_provenance((self, supertype)) + return sub + + if isinstance(supertype, Fix): + unrolled = supertype.unroll() + sub = self.unroll().constrain_and_bind_variables( + unrolled, + rigid_variables, + subtyping_assumptions + [(self, supertype)], + ) + sub.add_subtyping_provenance((self, supertype)) + return sub + + sub = self.unroll().constrain_and_bind_variables( + supertype, + rigid_variables, + subtyping_assumptions + [(self, supertype)], + ) + sub.add_subtyping_provenance((self, supertype)) + return sub + + @property + def kind(self) -> Kind: + return self._var.kind + + def __getitem__(self, args: Any) -> Any: + return self.unroll()[args] + + +class ForwardTypeReference(Type): + def __init__( + self, + kind: Kind, + name_to_resolve: str, + resolution_env: 'Environment', + _type_arguments: TypeArguments = (), + ) -> None: + super().__init__() + self._kind = kind + self._name_to_resolve = name_to_resolve + self._resolution_env = resolution_env + self._resolved_type: Optional[Type] = None + self._type_arguments = _type_arguments + + def _resolve(self) -> Type: + ty = self._resolution_env[self._name_to_resolve] + if self._type_arguments: + ty = ty[self._type_arguments] + return ty + + def _as_hashable_tuple(self) -> tuple: + return ( + self._kind, + id(self._resolution_env), + self._name_to_resolve, + tuple(self._type_arguments), + ) + + def __getitem__(self, args: TypeArguments) -> Type: + if self._resolved_type is not None: + return self._resolved_type[args] + + if isinstance(self.kind, GenericTypeKind): + if len(self.kind.parameter_kinds) != len(args): + raise ConcatTypeError( + 'Wrong number of arguments to generic type' + ) + for kind, arg in zip(self.kind.parameter_kinds, args): + if kind != arg.kind: + raise ConcatTypeError( + f'Type argument has kind {arg.kind}, expected kind {kind}' + ) + return ForwardTypeReference( + IndividualKind, + self._name_to_resolve, + self._resolution_env, + _type_arguments=args, + ) + raise ConcatTypeError(f'{self} is not a generic type') + + def resolve_forward_references(self) -> Type: + if self._resolved_type is None: + self._resolved_type = self._resolve() + return self._resolved_type + + def apply_substitution( + self, sub: 'concat.typecheck.Substitutions' + ) -> Type: + if self._resolved_type is not None: + return sub(self._resolved_type) + + return self + + @property + def attributes(self) -> Mapping[str, Type]: + if self._resolved_type is not None: + return self._resolved_type.attributes + + raise ConcatTypeError( + 'Cannot access attributes of type before they are defined' + ) + + def constrain_and_bind_variables( + self, + supertype: Type, + rigid_variables: AbstractSet['Variable'], + subtyping_assumptions: List[Tuple['Type', 'Type']], + ) -> 'Substitutions': + if self is supertype or _contains_assumption( + subtyping_assumptions, self, supertype + ): + return concat.typecheck.Substitutions() + + return self.resolve_forward_references().constrain_and_bind_variables( + supertype, + rigid_variables, + subtyping_assumptions + [(self, supertype)], + ) + + def _free_type_variables(self) -> InsertionOrderedSet[Variable]: + return InsertionOrderedSet([]) + + @property + def kind(self) -> Kind: + return self._kind def _iterable_to_str(iterable: Iterable) -> str: @@ -1721,125 +2019,235 @@ def _mapping_to_str(mapping: Mapping) -> str: # expose _Function as StackEffect StackEffect = _Function -_x = IndividualVariable() +_x = BoundVariable(kind=IndividualKind) -float_type = ObjectType(_x, {}, nominal=True) +float_type = NominalType(Brand('float', IndividualKind, []), ObjectType({})) no_return_type = _NoReturnType() -object_type = ObjectType(_x, {}, nominal=True) -object_type.set_internal_name('object_type') + + +_object_type: Optional[Type] = None + + +def get_object_type() -> Type: + assert _object_type is not None + return _object_type + + +def set_object_type(ty: Type) -> None: + global _object_type + assert _object_type is None + _object_type = ty + + +_list_type: Optional[Type] = None + + +def get_list_type() -> Type: + assert _list_type is not None + return _list_type + + +def set_list_type(ty: Type) -> None: + global _list_type + _list_type = ty + + +_str_type: Optional[Type] = None + + +def get_str_type() -> Type: + assert _str_type is not None + return _str_type + + +def set_str_type(ty: Type) -> None: + global _str_type + _str_type = ty + + +_tuple_type: Optional[Type] = None + + +def get_tuple_type() -> Type: + assert _tuple_type is not None + return _tuple_type + + +def set_tuple_type(ty: Type) -> None: + global _tuple_type + _tuple_type = ty + + +_int_type: Optional[Type] = None + + +def get_int_type() -> Type: + assert _int_type is not None + return _int_type + + +def set_int_type(ty: Type) -> None: + global _int_type + _int_type = ty + + +_bool_type: Optional[Type] = None + + +def get_bool_type() -> Type: + assert _bool_type is not None + return _bool_type + + +def set_bool_type(ty: Type) -> None: + global _bool_type + _bool_type = ty + + +_none_type: Optional[Type] = None + + +def get_none_type() -> Type: + assert _none_type is not None + return _none_type + + +def set_none_type(ty: Type) -> None: + global _none_type + _none_type = ty + + +_module_type: Optional[Type] = None + + +def get_module_type() -> Type: + assert _module_type is not None + return _module_type + + +def set_module_type(ty: Type) -> None: + global _module_type + _module_type = ty + _arg_type_var = SequenceVariable() -_return_type_var = IndividualVariable() +_return_type_var = ItemVariable(IndividualKind) py_function_type = PythonFunctionType( - _x, {}, type_parameters=[_arg_type_var, _return_type_var] + type_parameters=[_arg_type_var, _return_type_var] ) py_function_type.set_internal_name('py_function_type') -_invert_result_var = IndividualVariable() -invertible_type = ObjectType( - _x, - {'__invert__': py_function_type[TypeSequence([]), _invert_result_var]}, +_invert_result_var = ItemVariable(IndividualKind) +invertible_type = GenericType( [_invert_result_var], + ObjectType( + {'__invert__': py_function_type[TypeSequence([]), _invert_result_var]}, + ), ) -_sub_operand_type = IndividualVariable() -_sub_result_type = IndividualVariable() +_sub_operand_type = BoundVariable(ItemKind) +_sub_result_type = BoundVariable(ItemKind) # FIXME: Add reverse_substractable_type for __rsub__ -subtractable_type = ObjectType( - _x, - { - '__sub__': py_function_type[ - TypeSequence([_sub_operand_type]), _sub_result_type - ] - }, +subtractable_type = GenericType( [_sub_operand_type, _sub_result_type], + ObjectType( + { + '__sub__': py_function_type[ + TypeSequence([_sub_operand_type]), _sub_result_type + ] + }, + ), ) - -_add_result_type = IndividualVariable() - -addable_type = ObjectType( - _x, - { - '__add__': py_function_type[ - TypeSequence([object_type]), _add_result_type - ] - }, - [_add_result_type], +subtractable_type.set_internal_name('subtractable_type') + +_add_other_operand_type = BoundVariable(ItemKind) +_add_result_type = BoundVariable(ItemKind) + +addable_type = GenericType( + [_add_other_operand_type, _add_result_type], + ObjectType( + { + '__add__': py_function_type[ + # QUESTION: Should methods include self? + TypeSequence([_add_other_operand_type]), + _add_result_type, + ] + }, + ), ) addable_type.set_internal_name('addable_type') -bool_type = ObjectType(_x, {}, nominal=True) -bool_type.set_internal_name('bool_type') - -# QUESTION: Allow comparison methods to return any object? - -_other_type = IndividualVariable() -geq_comparable_type = ObjectType( - _x, - {'__ge__': py_function_type[TypeSequence([_other_type]), bool_type]}, - [_other_type], +# NOTE: Allow comparison methods to return any object. I don't think Python +# stops it. Plus, these definitions don't have to depend on bool, which is +# defined in builtins.cati. + +_other_type = BoundVariable(ItemKind) +_return_type = BoundVariable(ItemKind) +geq_comparable_type = GenericType( + [_other_type, _return_type], + ObjectType( + { + '__ge__': py_function_type[ + TypeSequence([_other_type]), _return_type + ] + }, + ), ) geq_comparable_type.set_internal_name('geq_comparable_type') -leq_comparable_type = ObjectType( - _x, - {'__le__': py_function_type[TypeSequence([_other_type]), bool_type]}, - [_other_type], +leq_comparable_type = GenericType( + [_other_type, _return_type], + ObjectType( + { + '__le__': py_function_type[ + TypeSequence([_other_type]), _return_type + ] + }, + ), ) leq_comparable_type.set_internal_name('leq_comparable_type') -lt_comparable_type = ObjectType( - _x, - {'__lt__': py_function_type[TypeSequence([_other_type]), bool_type]}, - [_other_type], +lt_comparable_type = GenericType( + [_other_type, _return_type], + ObjectType( + { + '__lt__': py_function_type[ + TypeSequence([_other_type]), _return_type + ] + }, + ), ) lt_comparable_type.set_internal_name('lt_comparable_type') -_int_add_type = py_function_type[TypeSequence([object_type]), _x] +_result_type = BoundVariable(ItemKind) -int_type = ObjectType( - _x, - { - '__add__': _int_add_type, - '__invert__': py_function_type[TypeSequence([]), _x], - '__sub__': _int_add_type, - '__invert__': py_function_type[TypeSequence([]), _x], - '__le__': py_function_type[TypeSequence([_x]), bool_type], - '__lt__': py_function_type[TypeSequence([_x]), bool_type], - '__ge__': py_function_type[TypeSequence([_x]), bool_type], - }, - nominal=True, -) -int_type.set_internal_name('int_type') - -none_type = ObjectType(_x, {}) -none_type.set_internal_name('none_type') - -_result_type = IndividualVariable() - -iterator_type = ObjectType( - _x, - { - '__iter__': py_function_type[TypeSequence([]), _x], - '__next__': py_function_type[TypeSequence([none_type,]), _result_type], - }, +iterator_type = GenericType( [_result_type], + Fix( + _x, + ObjectType( + { + '__iter__': py_function_type[TypeSequence([]), _x], + '__next__': py_function_type[TypeSequence([]), _result_type], + }, + ), + ), ) iterator_type.set_internal_name('iterator_type') -iterable_type = ObjectType( - _x, - { - '__iter__': py_function_type[ - TypeSequence([]), iterator_type[_result_type,] - ] - }, +iterable_type = GenericType( [_result_type], + ObjectType( + { + '__iter__': py_function_type[ + TypeSequence([]), iterator_type[_result_type,] + ] + }, + ), ) iterable_type.set_internal_name('iterable_type') context_manager_type = ObjectType( - _x, { # TODO: Add argument and return types. I think I'll need a special # py_function representation for that. @@ -1849,127 +2257,21 @@ def _mapping_to_str(mapping: Mapping) -> str: ) context_manager_type.set_internal_name('context_manager_type') -optional_type = _OptionalType() -optional_type.set_internal_name('optional_type') - -_key_type_var = IndividualVariable() -_value_type_var = IndividualVariable() -dict_type = ObjectType( - _x, - { - '__iter__': py_function_type[ - TypeSequence([]), iterator_type[_key_type_var,] - ] - }, - [_key_type_var, _value_type_var], - nominal=True, +_optional_type_var = BoundVariable(ItemKind) +optional_type = GenericType( + [_optional_type_var], _OptionalType(_optional_type_var) ) -dict_type.set_internal_name('dict_type') - -file_type = ObjectType( - _x, - { - 'seek': py_function_type[TypeSequence([int_type]), int_type], - 'read': py_function_type, - '__enter__': py_function_type, - '__exit__': py_function_type, - }, - [], - # context_manager_type is a structural supertype - [iterable_type], - nominal=True, -) -file_type.set_internal_name('file_type') - -_start_type_var, _stop_type_var, _step_type_var = ( - IndividualVariable(), - IndividualVariable(), - IndividualVariable(), -) -slice_type = ObjectType( - _x, {}, [_start_type_var, _stop_type_var, _step_type_var], nominal=True -) -slice_type.set_internal_name('slice_type') - -_element_type_var = IndividualVariable() -_list_getitem_type = py_function_type[ - TypeSequence([int_type]), _element_type_var -].with_overload((slice_type[(optional_type[int_type,],) * 3],), _x) -list_type = ObjectType( - _x, - { - '__getitem__': _list_getitem_type, - '__iter__': py_function_type[ - TypeSequence([]), iterator_type[_element_type_var,] - ], - }, - [_element_type_var], - nominal=True, -) -list_type.set_internal_name('list_type') - -_str_getitem_type = py_function_type[ - TypeSequence([int_type]), _x -].with_overload( - [ - slice_type[ - optional_type[int_type,], - optional_type[int_type,], - optional_type[int_type,], - ] - ], - _x, -) -str_type = ObjectType( - _x, - { - '__getitem__': _str_getitem_type, - '__add__': py_function_type[TypeSequence([object_type]), _x], - # FIXME: str doesn't have an __radd__. I added it only to help with - # type checking. - '__radd__': py_function_type[TypeSequence([object_type]), _x], - 'find': py_function_type[ - TypeSequence( - [_x, optional_type[int_type,], optional_type[int_type,]] - ), - int_type, - ], - 'join': py_function_type[TypeSequence([_x, iterable_type[_x,]]), _x], - }, - nominal=True, -) -str_type.set_internal_name('str_type') - -ellipsis_type = ObjectType(_x, {}) -not_implemented_type = ObjectType(_x, {}) - -_element_types_var = SequenceVariable() -tuple_type = ObjectType( - _x, - {'__getitem__': py_function_type}, - [_element_types_var], - nominal=True - # iterable_type is a structural supertype -) -tuple_type.set_internal_name('tuple_type') - -base_exception_type = ObjectType(_x, {}) -module_type = ObjectType(_x, {}) +optional_type.set_internal_name('optional_type') -_index_type_var = IndividualVariable() -_result_type_var = IndividualVariable() -subscriptable_type = ObjectType( - IndividualVariable(), - { - '__getitem__': py_function_type[ - TypeSequence([_index_type_var]), _result_type_var - ], - }, +_index_type_var = BoundVariable(ItemKind) +_result_type_var = BoundVariable(ItemKind) +subscriptable_type = GenericType( [_index_type_var, _result_type_var], + ObjectType( + { + '__getitem__': py_function_type[ + TypeSequence([_index_type_var]), _result_type_var + ], + }, + ), ) - -_answer_type_var = IndividualVariable() -continuation_monad_type = ObjectType( - _x, {}, [_result_type_var, _answer_type_var], nominal=True -) -continuation_monad_type.set_internal_name('continuation_monad_type') diff --git a/language-concat/lib/main.ts b/language-concat/lib/main.ts index 903afb4e..5842e8dc 100644 --- a/language-concat/lib/main.ts +++ b/language-concat/lib/main.ts @@ -32,4 +32,8 @@ module.exports = { consumeLinterV2: concatLanguageClient.consumeLinterV2.bind( concatLanguageClient ), + + consumeDatatip: concatLanguageClient.consumeDatatip.bind( + concatLanguageClient + ), }; diff --git a/language-concat/package.json b/language-concat/package.json index 5c1c4325..4f170177 100644 --- a/language-concat/package.json +++ b/language-concat/package.json @@ -36,6 +36,11 @@ "versions": { "2.0.0": "consumeLinterV2" } + }, + "datatip": { + "versions": { + "0.1.0": "consumeDatatip" + } } } } diff --git a/mypy.ini b/mypy.ini index 5a93ed2c..4af77846 100644 --- a/mypy.ini +++ b/mypy.ini @@ -2,3 +2,4 @@ check_untyped_defs = True disallow_any_unimported = True mypy_path = stubs/ +python_version = 3.7 diff --git a/pyproject.toml b/pyproject.toml index 991ce2e6..649551e6 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -27,12 +27,21 @@ readme = "README.md" [project.optional-dependencies] dev = [ "axblack==20220330", + "importlib-metadata<5", "mypy>=1.1.1", "pre-commit>=2.6.0,<3", - "tox>=4.5.1,<5", - "hypothesis>=6.75.1,<7" + "pylsp-mypy", + "python-lsp-server[all]==1.7.2", + "snakeviz", + "virtualenv<=20.17.1", +] +test = [ + "coverage>=6.4.4,<7", + "hypothesis>=6.75.1,<7", + "nose2==0.13.0", + "pywinpty>=2.0.7,<3; platform_system==\"Windows\"", + "scripttest", ] - [project.urls] "Source code" = "https://github.com/jmanuel1/concat" @@ -43,6 +52,10 @@ pattern = "version = '(?P.*)'" [tool.hatch.envs.default] features = [ - "dev" + "dev", + "test", ] python = "3.7" + +[tool.hatch.metadata] +allow-direct-references = true diff --git a/tox.ini b/tox.ini deleted file mode 100644 index aad4e97d..00000000 --- a/tox.ini +++ /dev/null @@ -1,23 +0,0 @@ -[tox] -requires = - tox>=4 -env_list = py37 - -[testenv] -description = run tests with coverage -deps = - coverage>=6.4.4,<7 - hypothesis>=6.75.1,<7 - nose2==0.13.0 - pywinpty>=2.0.7,<3; platform_system=="Windows" - scripttest -commands = - coverage erase - coverage run -m nose2 -v --pretty-assert {posargs:concat.tests} - coverage combine - coverage xml - coverage lcov -passenv = - CARGO_BUILD_TARGET -setenv = - PYTHONWARNINGS = default