From 9a045cadf5141625c4688e36f7e36cb44175769e Mon Sep 17 00:00:00 2001 From: Oli Date: Sun, 15 Jun 2025 08:28:36 +0700 Subject: [PATCH] fix missing dependencies and add type visitor --- godelOS/core_kr/type_system/__init__.py | 25 +- godelOS/core_kr/type_system/types.py | 322 ++++++++++------- godelOS/core_kr/type_system/visitor.py | 458 +++++++++++++++--------- requirements.txt | 4 +- setup.py | 2 + 5 files changed, 489 insertions(+), 322 deletions(-) diff --git a/godelOS/core_kr/type_system/__init__.py b/godelOS/core_kr/type_system/__init__.py index 523251a..f9ce5c3 100644 --- a/godelOS/core_kr/type_system/__init__.py +++ b/godelOS/core_kr/type_system/__init__.py @@ -4,21 +4,15 @@ This module defines and manages the type hierarchy and performs type checking and inference. """ -from godelOS.core_kr.type_system.types import ( - Type, - AtomicType, - FunctionType, - TypeVariable, - ParametricTypeConstructor, - InstantiatedParametricType, -) -from godelOS.core_kr.type_system.manager import TypeSystemManager from godelOS.core_kr.type_system.environment import TypeEnvironment -from godelOS.core_kr.type_system.visitor import ( - Error, - TypeInferenceVisitor, - TypeCheckingVisitor, -) +from godelOS.core_kr.type_system.manager import TypeSystemManager +from godelOS.core_kr.type_system.types import (AtomicType, FunctionType, + InstantiatedParametricType, + ParametricTypeConstructor, Type, + TypeVariable) +from godelOS.core_kr.type_system.visitor import (Error, TypeCheckingVisitor, + TypeInferenceVisitor, + TypeVisitor) __all__ = [ "Type", @@ -32,4 +26,5 @@ "Error", "TypeInferenceVisitor", "TypeCheckingVisitor", -] \ No newline at end of file + "TypeVisitor", +] diff --git a/godelOS/core_kr/type_system/types.py b/godelOS/core_kr/type_system/types.py index aec1eaf..6df7651 100644 --- a/godelOS/core_kr/type_system/types.py +++ b/godelOS/core_kr/type_system/types.py @@ -5,72 +5,86 @@ including atomic types, function types, type variables, and parametric types. """ -from typing import Dict, List, Optional, Set +from __future__ import annotations + from abc import ABC, abstractmethod +from typing import TYPE_CHECKING, Any, Dict, List, Optional, Set + +if TYPE_CHECKING: + from godelOS.core_kr.type_system.visitor import TypeVisitor class Type(ABC): """ Base class for all types in the GödelOS type system. """ - + @abstractmethod - def is_subtype_of(self, other_type: 'Type', type_system: 'TypeSystemManager') -> bool: + def is_subtype_of( + self, other_type: "Type", type_system: "TypeSystemManager" + ) -> bool: """ Check if this type is a subtype of another type. - + Args: other_type: The type to check against type_system: The type system manager to use for the check - + Returns: True if this type is a subtype of other_type, False otherwise """ pass - + @abstractmethod - def substitute_type_vars(self, bindings: Dict['TypeVariable', 'Type']) -> 'Type': + def substitute_type_vars(self, bindings: Dict["TypeVariable", "Type"]) -> "Type": """ Substitute type variables in this type according to the given bindings. - + Args: bindings: A mapping from type variables to types - + Returns: A new type with the substitutions applied """ pass + @abstractmethod + def accept(self, visitor: "TypeVisitor") -> Any: + """Accept a TypeVisitor and return its result.""" + pass + class AtomicType(Type): """ A basic, non-decomposable type. - + Examples: Entity, Agent, Integer, Boolean, String. """ - + def __init__(self, name: str): """ Initialize an atomic type. - + Args: name: The name of the type """ self._name = name - + @property def name(self) -> str: """Get the name of the type.""" return self._name - - def is_subtype_of(self, other_type: 'Type', type_system: 'TypeSystemManager') -> bool: + + def is_subtype_of( + self, other_type: "Type", type_system: "TypeSystemManager" + ) -> bool: """ Check if this atomic type is a subtype of another type. - + Args: other_type: The type to check against type_system: The type system manager to use for the check - + Returns: True if this type is a subtype of other_type, False otherwise """ @@ -78,85 +92,90 @@ def is_subtype_of(self, other_type: 'Type', type_system: 'TypeSystemManager') -> # 1. They are the same type # 2. The other type is also an atomic type and this type is a subtype of it in the hierarchy # 3. The other type is a type variable that can be bound to this type (handled by TypeVariable) - + if self == other_type: return True - + if isinstance(other_type, AtomicType): return type_system.is_subtype(self, other_type) - + return False - - def substitute_type_vars(self, bindings: Dict['TypeVariable', 'Type']) -> 'Type': + + def substitute_type_vars(self, bindings: Dict["TypeVariable", "Type"]) -> "Type": """ Substitute type variables in this type according to the given bindings. - + For atomic types, this is a no-op since they don't contain type variables. - + Args: bindings: A mapping from type variables to types - + Returns: This type unchanged """ return self - + def __eq__(self, other: object) -> bool: if not isinstance(other, AtomicType): return False return self._name == other._name - + def __hash__(self) -> int: return hash(("AtomicType", self._name)) - + def __str__(self) -> str: return self._name - + def __repr__(self) -> str: return f"AtomicType({self._name})" + def accept(self, visitor: "TypeVisitor") -> Any: + return visitor.visit_atomic_type(self) + class FunctionType(Type): """ A type representing a function from argument types to a return type. - + Examples: (Entity, Entity) -> Boolean, () -> Integer. """ - + def __init__(self, arg_types: List[Type], return_type: Type): """ Initialize a function type. - + Args: arg_types: The types of the arguments return_type: The return type """ self._arg_types = tuple(arg_types) # Make immutable self._return_type = return_type - + @property def arg_types(self) -> tuple: """Get the argument types.""" return self._arg_types - + @property def return_type(self) -> Type: """Get the return type.""" return self._return_type - - def is_subtype_of(self, other_type: 'Type', type_system: 'TypeSystemManager') -> bool: + + def is_subtype_of( + self, other_type: "Type", type_system: "TypeSystemManager" + ) -> bool: """ Check if this function type is a subtype of another type. - + For function types, this follows the contravariant/covariant rule: (S1,...,Sn) -> T is a subtype of (R1,...,Rn) -> U if - R1 is a subtype of S1, ..., Rn is a subtype of Sn (contravariant in argument types) - T is a subtype of U (covariant in return type) - + Args: other_type: The type to check against type_system: The type system manager to use for the check - + Returns: True if this type is a subtype of other_type, False otherwise """ @@ -164,157 +183,173 @@ def is_subtype_of(self, other_type: 'Type', type_system: 'TypeSystemManager') -> # 1. They are the same type # 2. The other type is also a function type with the same number of arguments, # and the subtyping relationship holds for arguments (contravariant) and return type (covariant) - + if self == other_type: return True - + if not isinstance(other_type, FunctionType): return False - + if len(self._arg_types) != len(other_type._arg_types): return False - + # Contravariant in argument types for i in range(len(self._arg_types)): - if not other_type._arg_types[i].is_subtype_of(self._arg_types[i], type_system): + if not other_type._arg_types[i].is_subtype_of( + self._arg_types[i], type_system + ): return False - + # Covariant in return type return self._return_type.is_subtype_of(other_type._return_type, type_system) - - def substitute_type_vars(self, bindings: Dict['TypeVariable', 'Type']) -> 'Type': + + def substitute_type_vars(self, bindings: Dict["TypeVariable", "Type"]) -> "Type": """ Substitute type variables in this type according to the given bindings. - + Args: bindings: A mapping from type variables to types - + Returns: A new function type with the substitutions applied """ - new_arg_types = [arg_type.substitute_type_vars(bindings) for arg_type in self._arg_types] + new_arg_types = [ + arg_type.substitute_type_vars(bindings) for arg_type in self._arg_types + ] new_return_type = self._return_type.substitute_type_vars(bindings) return FunctionType(new_arg_types, new_return_type) - + def __eq__(self, other: object) -> bool: if not isinstance(other, FunctionType): return False - return (self._arg_types == other._arg_types and - self._return_type == other._return_type) - + return ( + self._arg_types == other._arg_types + and self._return_type == other._return_type + ) + def __hash__(self) -> int: return hash(("FunctionType", self._arg_types, self._return_type)) - + def __str__(self) -> str: args_str = ", ".join(str(arg_type) for arg_type in self._arg_types) return f"({args_str}) -> {self._return_type}" - + def __repr__(self) -> str: return f"FunctionType({self._arg_types}, {self._return_type})" + def accept(self, visitor: "TypeVisitor") -> Any: + return visitor.visit_function_type(self) + class TypeVariable(Type): """ A type variable, used for parametric polymorphism. - + Examples: ?T, ?U. """ - + def __init__(self, name: str): """ Initialize a type variable. - + Args: name: The name of the type variable """ self._name = name - + @property def name(self) -> str: """Get the name of the type variable.""" return self._name - - def is_subtype_of(self, other_type: 'Type', type_system: 'TypeSystemManager') -> bool: + + def is_subtype_of( + self, other_type: "Type", type_system: "TypeSystemManager" + ) -> bool: """ Check if this type variable is a subtype of another type. - + A type variable is a subtype of another type if it is the same type variable. - + Args: other_type: The type to check against type_system: The type system manager to use for the check - + Returns: True if this type is a subtype of other_type, False otherwise """ return self == other_type - - def substitute_type_vars(self, bindings: Dict['TypeVariable', 'Type']) -> 'Type': + + def substitute_type_vars(self, bindings: Dict["TypeVariable", "Type"]) -> "Type": """ Substitute this type variable according to the given bindings. - + Args: bindings: A mapping from type variables to types - + Returns: The type bound to this type variable, or this type variable if not bound """ return bindings.get(self, self) - + def __eq__(self, other: object) -> bool: if not isinstance(other, TypeVariable): return False return self._name == other._name - + def __hash__(self) -> int: return hash(("TypeVariable", self._name)) - + def __str__(self) -> str: return f"?{self._name}" - + def __repr__(self) -> str: return f"TypeVariable({self._name})" + def accept(self, visitor: "TypeVisitor") -> Any: + return visitor.visit_type_variable(self) + class ParametricType(Type): """ Base class for parametric types. - + This is an abstract base class that serves as a common parent for ParametricTypeConstructor and InstantiatedParametricType. """ - + @abstractmethod - def get_type_params(self) -> List['TypeVariable']: + def get_type_params(self) -> List["TypeVariable"]: """ Get the type parameters of this parametric type. - + Returns: A list of type variables representing the type parameters """ pass - - def is_subtype_of(self, other_type: 'Type', type_system: 'TypeSystemManager') -> bool: + + def is_subtype_of( + self, other_type: "Type", type_system: "TypeSystemManager" + ) -> bool: """ Check if this parametric type is a subtype of another type. - + Args: other_type: The type to check against type_system: The type system manager to use for the check - + Returns: True if this type is a subtype of other_type, False otherwise """ # This is a base implementation that should be overridden by subclasses return self == other_type - - def substitute_type_vars(self, bindings: Dict['TypeVariable', 'Type']) -> 'Type': + + def substitute_type_vars(self, bindings: Dict["TypeVariable", "Type"]) -> "Type": """ Substitute type variables in this type according to the given bindings. - + Args: bindings: A mapping from type variables to types - + Returns: A new type with the substitutions applied """ @@ -325,52 +360,54 @@ def substitute_type_vars(self, bindings: Dict['TypeVariable', 'Type']) -> 'Type' class ParametricTypeConstructor(ParametricType): """ A type constructor for parametric types. - + Examples: List, Map, Option. """ - + def __init__(self, name: str, type_params: List[TypeVariable]): """ Initialize a parametric type constructor. - + Args: name: The name of the type constructor type_params: The type parameters """ self._name = name self._type_params = tuple(type_params) # Make immutable - + @property def name(self) -> str: """Get the name of the type constructor.""" return self._name - + @property def type_params(self) -> tuple: """Get the type parameters.""" """Get the type parameters.""" return self._type_params - + def __eq__(self, other: object) -> bool: if not isinstance(other, ParametricTypeConstructor): return False - return (self._name == other._name and - self._type_params == other._type_params) - + return self._name == other._name and self._type_params == other._type_params + def __hash__(self) -> int: return hash(("ParametricTypeConstructor", self._name, self._type_params)) - + def __str__(self) -> str: params_str = ", ".join(str(param) for param in self._type_params) return f"{self._name}[{params_str}]" - + def __repr__(self) -> str: return f"ParametricTypeConstructor({self._name}, {self._type_params})" - - def get_type_params(self) -> List['TypeVariable']: + + def accept(self, visitor: "TypeVisitor") -> Any: + return visitor.visit_parametric_type(self) + + def get_type_params(self) -> List["TypeVariable"]: """ Get the type parameters of this parametric type constructor. - + Returns: A list of type variables representing the type parameters """ @@ -380,42 +417,48 @@ def get_type_params(self) -> List['TypeVariable']: class InstantiatedParametricType(ParametricType): """ A parametric type with concrete type arguments. - + Examples: List[Integer], Map[String, Entity]. """ - - def __init__(self, constructor: ParametricTypeConstructor, actual_type_args: List[Type]): + + def __init__( + self, constructor: ParametricTypeConstructor, actual_type_args: List[Type] + ): """ Initialize an instantiated parametric type. - + Args: constructor: The parametric type constructor actual_type_args: The actual type arguments """ if len(actual_type_args) != len(constructor.type_params): - raise ValueError(f"Expected {len(constructor.type_params)} type arguments, got {len(actual_type_args)}") - + raise ValueError( + f"Expected {len(constructor.type_params)} type arguments, got {len(actual_type_args)}" + ) + self._constructor = constructor self._actual_type_args = tuple(actual_type_args) # Make immutable - + @property def constructor(self) -> ParametricTypeConstructor: """Get the parametric type constructor.""" return self._constructor - + @property def actual_type_args(self) -> tuple: """Get the actual type arguments.""" return self._actual_type_args - - def is_subtype_of(self, other_type: 'Type', type_system: 'TypeSystemManager') -> bool: + + def is_subtype_of( + self, other_type: "Type", type_system: "TypeSystemManager" + ) -> bool: """ Check if this instantiated parametric type is a subtype of another type. - + Args: other_type: The type to check against type_system: The type system manager to use for the check - + Returns: True if this type is a subtype of other_type, False otherwise """ @@ -424,64 +467,75 @@ def is_subtype_of(self, other_type: 'Type', type_system: 'TypeSystemManager') -> # 2. The other type is also an instantiated parametric type with the same constructor, # and the type arguments are compatible according to their variance # 3. There's an explicit subtyping relationship defined in the type system - + if self == other_type: return True - + if isinstance(other_type, InstantiatedParametricType): if self._constructor != other_type._constructor: return False - + # Check if the type arguments are compatible # This depends on the variance of the type parameters # For simplicity, we assume invariance here (exact match required) if len(self._actual_type_args) != len(other_type._actual_type_args): return False - + for i in range(len(self._actual_type_args)): # For invariant parameters, types must be equal if self._actual_type_args[i] != other_type._actual_type_args[i]: return False - + return True - + # Check if there's an explicit subtyping relationship in the type system return type_system.is_subtype(self, other_type) - - def substitute_type_vars(self, bindings: Dict['TypeVariable', 'Type']) -> 'Type': + + def substitute_type_vars(self, bindings: Dict["TypeVariable", "Type"]) -> "Type": """ Substitute type variables in this type according to the given bindings. - + Args: bindings: A mapping from type variables to types - + Returns: A new instantiated parametric type with the substitutions applied """ - new_type_args = [arg.substitute_type_vars(bindings) for arg in self._actual_type_args] + new_type_args = [ + arg.substitute_type_vars(bindings) for arg in self._actual_type_args + ] return InstantiatedParametricType(self._constructor, new_type_args) - + def __eq__(self, other: object) -> bool: if not isinstance(other, InstantiatedParametricType): return False - return (self._constructor == other._constructor and - self._actual_type_args == other._actual_type_args) - + return ( + self._constructor == other._constructor + and self._actual_type_args == other._actual_type_args + ) + def __hash__(self) -> int: - return hash(("InstantiatedParametricType", self._constructor, self._actual_type_args)) - + return hash( + ("InstantiatedParametricType", self._constructor, self._actual_type_args) + ) + def __str__(self) -> str: args_str = ", ".join(str(arg) for arg in self._actual_type_args) return f"{self._constructor.name}[{args_str}]" - + def __repr__(self) -> str: - return f"InstantiatedParametricType({self._constructor}, {self._actual_type_args})" - - def get_type_params(self) -> List['TypeVariable']: + return ( + f"InstantiatedParametricType({self._constructor}, {self._actual_type_args})" + ) + + def get_type_params(self) -> List["TypeVariable"]: """ Get the type parameters of this instantiated parametric type. - + Returns: A list of type variables representing the type parameters """ - return self._constructor.get_type_params() \ No newline at end of file + return self._constructor.get_type_params() + + def accept(self, visitor: "TypeVisitor") -> Any: + return visitor.visit_instantiated_parametric_type(self) diff --git a/godelOS/core_kr/type_system/visitor.py b/godelOS/core_kr/type_system/visitor.py index ce01fca..3150dda 100644 --- a/godelOS/core_kr/type_system/visitor.py +++ b/godelOS/core_kr/type_system/visitor.py @@ -4,26 +4,53 @@ This module defines a visitor for type checking and inference of AST nodes. """ -from typing import Dict, List, Optional, Tuple, TYPE_CHECKING +from typing import TYPE_CHECKING, Dict, Generic, List, Optional, Tuple, TypeVar -from godelOS.core_kr.ast.nodes import ( - AST_Node, ASTVisitor, ConstantNode, VariableNode, ApplicationNode, - QuantifierNode, ConnectiveNode, ModalOpNode, LambdaNode, DefinitionNode -) -from godelOS.core_kr.type_system.types import Type, FunctionType +from godelOS.core_kr.ast.nodes import (ApplicationNode, AST_Node, ASTVisitor, + ConnectiveNode, ConstantNode, + DefinitionNode, LambdaNode, ModalOpNode, + QuantifierNode, VariableNode) from godelOS.core_kr.type_system.environment import TypeEnvironment +from godelOS.core_kr.type_system.types import FunctionType, Type if TYPE_CHECKING: from godelOS.core_kr.type_system.manager import TypeSystemManager + from godelOS.core_kr.type_system.types import (AtomicType, FunctionType, + InstantiatedParametricType, + ParametricType, + TypeVariable) + +T = TypeVar("T") + + +class TypeVisitor(Generic[T]): + """Base class for visitors over type objects.""" + + def visit_atomic_type(self, type_obj: "AtomicType") -> T: + raise NotImplementedError + + def visit_function_type(self, type_obj: "FunctionType") -> T: + raise NotImplementedError + + def visit_parametric_type(self, type_obj: "ParametricType") -> T: + raise NotImplementedError + + def visit_instantiated_parametric_type( + self, type_obj: "InstantiatedParametricType" + ) -> T: + raise NotImplementedError + + def visit_type_variable(self, type_obj: "TypeVariable") -> T: + raise NotImplementedError class Error: """Simple error class for type checking/inference errors.""" - + def __init__(self, message: str, node: Optional[AST_Node] = None): self.message = message self.node = node - + def __str__(self) -> str: return self.message @@ -31,45 +58,45 @@ def __str__(self) -> str: class TypeInferenceVisitor(ASTVisitor[Tuple[Optional[Type], List[Error]]]): """ Visitor for inferring the types of AST nodes. - + This visitor implements the visitor pattern to traverse the AST and infer the types of nodes based on their structure and the types of their components. """ - - def __init__(self, type_system: 'TypeSystemManager', environment: TypeEnvironment): + + def __init__(self, type_system: "TypeSystemManager", environment: TypeEnvironment): """ Initialize a type inference visitor. - + Args: type_system: The type system manager to use for type checking environment: The type environment to use for variable lookups """ self.type_system = type_system self.environment = environment - + def visit_constant(self, node: ConstantNode) -> Tuple[Optional[Type], List[Error]]: """ Infer the type of a constant node. - + For constants, the type is already stored in the node. - + Args: node: The constant node - + Returns: The type of the constant and an empty list of errors """ return node.type, [] - + def visit_variable(self, node: VariableNode) -> Tuple[Optional[Type], List[Error]]: """ Infer the type of a variable node. - + For variables, look up the type in the environment. - + Args: node: The variable node - + Returns: The type of the variable and a list of errors """ @@ -78,19 +105,23 @@ def visit_variable(self, node: VariableNode) -> Tuple[Optional[Type], List[Error # If not in environment, use the type stored in the node var_type = node.type if var_type is None: - return None, [Error(f"Cannot determine type for variable {node.name}", node)] + return None, [ + Error(f"Cannot determine type for variable {node.name}", node) + ] return var_type, [] - - def visit_application(self, node: ApplicationNode) -> Tuple[Optional[Type], List[Error]]: + + def visit_application( + self, node: ApplicationNode + ) -> Tuple[Optional[Type], List[Error]]: """ Infer the type of an application node. - + For applications, check that the operator has a function type and the arguments match the expected types. - + Args: node: The application node - + Returns: The type of the application and a list of errors """ @@ -98,142 +129,164 @@ def visit_application(self, node: ApplicationNode) -> Tuple[Optional[Type], List op_type, op_errors = node.operator.accept(self) if op_errors: return None, op_errors - + if not isinstance(op_type, FunctionType): - return None, [Error(f"Operator {node.operator} is not a function", node.operator)] - + return None, [ + Error(f"Operator {node.operator} is not a function", node.operator) + ] + # Check that the number of arguments matches if len(node.arguments) != len(op_type.arg_types): - return None, [Error( - f"Function expects {len(op_type.arg_types)} arguments, got {len(node.arguments)}", - node - )] - + return None, [ + Error( + f"Function expects {len(op_type.arg_types)} arguments, got {len(node.arguments)}", + node, + ) + ] + # Check each argument type for i, arg in enumerate(node.arguments): arg_type, arg_errors = arg.accept(self) if arg_errors: return None, arg_errors - + if arg_type is None: return None, [Error(f"Cannot determine type for argument {i+1}", arg)] - + if not self.type_system.is_subtype(arg_type, op_type.arg_types[i]): - return None, [Error( - f"Argument {i+1} has type {arg_type}, expected {op_type.arg_types[i]}", - arg - )] - + return None, [ + Error( + f"Argument {i+1} has type {arg_type}, expected {op_type.arg_types[i]}", + arg, + ) + ] + # The type of the application is the return type of the function return op_type.return_type, [] - - def visit_quantifier(self, node: QuantifierNode) -> Tuple[Optional[Type], List[Error]]: + + def visit_quantifier( + self, node: QuantifierNode + ) -> Tuple[Optional[Type], List[Error]]: """ Infer the type of a quantifier node. - + For quantifiers, check that the scope is a boolean expression and return boolean type. - + Args: node: The quantifier node - + Returns: The type of the quantifier and a list of errors """ boolean_type = self.type_system.get_type("Boolean") if boolean_type is None: return None, [Error("Boolean type not defined in type system", node)] - + # Create a new environment with the bound variables new_env = self.environment.extend() for var in node.bound_variables: new_env.set_type(var, var.type) - + # Create a new visitor with the extended environment new_visitor = TypeInferenceVisitor(self.type_system, new_env) - + # Check that the scope is a boolean expression scope_type, scope_errors = node.scope.accept(new_visitor) if scope_errors: return None, scope_errors - + if scope_type is None: - return None, [Error("Cannot determine type for quantifier scope", node.scope)] - + return None, [ + Error("Cannot determine type for quantifier scope", node.scope) + ] + if not self.type_system.is_subtype(scope_type, boolean_type): - return None, [Error( - f"Quantifier scope has type {scope_type}, expected {boolean_type}", - node.scope - )] - + return None, [ + Error( + f"Quantifier scope has type {scope_type}, expected {boolean_type}", + node.scope, + ) + ] + # Quantifiers always return boolean return boolean_type, [] - - def visit_connective(self, node: ConnectiveNode) -> Tuple[Optional[Type], List[Error]]: + + def visit_connective( + self, node: ConnectiveNode + ) -> Tuple[Optional[Type], List[Error]]: """ Infer the type of a connective node. - + For connectives, check that all operands are boolean expressions and return boolean type. - + Args: node: The connective node - + Returns: The type of the connective and a list of errors """ boolean_type = self.type_system.get_type("Boolean") if boolean_type is None: return None, [Error("Boolean type not defined in type system", node)] - + for operand in node.operands: operand_type, operand_errors = operand.accept(self) if operand_errors: return None, operand_errors - + if operand_type is None: - return None, [Error("Cannot determine type for connective operand", operand)] - + return None, [ + Error("Cannot determine type for connective operand", operand) + ] + if not self.type_system.is_subtype(operand_type, boolean_type): - return None, [Error( - f"Connective operand has type {operand_type}, expected {boolean_type}", - operand - )] - + return None, [ + Error( + f"Connective operand has type {operand_type}, expected {boolean_type}", + operand, + ) + ] + # Connectives always return boolean return boolean_type, [] - + def visit_modal_op(self, node: ModalOpNode) -> Tuple[Optional[Type], List[Error]]: """ Infer the type of a modal operator node. - + For modal operators, check that the proposition is a boolean expression and return boolean type. - + Args: node: The modal operator node - + Returns: The type of the modal operator and a list of errors """ boolean_type = self.type_system.get_type("Boolean") if boolean_type is None: return None, [Error("Boolean type not defined in type system", node)] - + # Check that the proposition is a boolean expression prop_type, prop_errors = node.proposition.accept(self) if prop_errors: return None, prop_errors - + if prop_type is None: - return None, [Error("Cannot determine type for modal proposition", node.proposition)] - + return None, [ + Error("Cannot determine type for modal proposition", node.proposition) + ] + if not self.type_system.is_subtype(prop_type, boolean_type): - return None, [Error( - f"Modal proposition has type {prop_type}, expected {boolean_type}", - node.proposition - )] - + return None, [ + Error( + f"Modal proposition has type {prop_type}, expected {boolean_type}", + node.proposition, + ) + ] + # If there's an agent or world, check its type (typically Entity or Agent) if node.agent_or_world: # The type depends on the modal operator @@ -242,33 +295,40 @@ def visit_modal_op(self, node: ModalOpNode) -> Tuple[Optional[Type], List[Error] agent_type = self.type_system.get_type("Agent") if agent_type is None: return None, [Error("Agent type not defined in type system", node)] - + agent_world_type, agent_world_errors = node.agent_or_world.accept(self) if agent_world_errors: return None, agent_world_errors - + if agent_world_type is None: - return None, [Error("Cannot determine type for modal agent/world", node.agent_or_world)] - + return None, [ + Error( + "Cannot determine type for modal agent/world", + node.agent_or_world, + ) + ] + if not self.type_system.is_subtype(agent_world_type, agent_type): - return None, [Error( - f"Modal agent has type {agent_world_type}, expected {agent_type}", - node.agent_or_world - )] - + return None, [ + Error( + f"Modal agent has type {agent_world_type}, expected {agent_type}", + node.agent_or_world, + ) + ] + # Modal operators always return boolean return boolean_type, [] - + def visit_lambda(self, node: LambdaNode) -> Tuple[Optional[Type], List[Error]]: """ Infer the type of a lambda node. - + For lambda expressions, create a new environment with the bound variables and infer the type of the body. - + Args: node: The lambda node - + Returns: The type of the lambda and a list of errors """ @@ -276,32 +336,34 @@ def visit_lambda(self, node: LambdaNode) -> Tuple[Optional[Type], List[Error]]: new_env = self.environment.extend() for var in node.bound_variables: new_env.set_type(var, var.type) - + # Create a new visitor with the extended environment new_visitor = TypeInferenceVisitor(self.type_system, new_env) - + # Infer the type of the body body_type, body_errors = node.body.accept(new_visitor) if body_errors: return None, body_errors - + if body_type is None: return None, [Error("Cannot determine type for lambda body", node.body)] - + # The type of the lambda is a function from the bound variables' types to the body type arg_types = [var.type for var in node.bound_variables] return FunctionType(arg_types, body_type), [] - - def visit_definition(self, node: DefinitionNode) -> Tuple[Optional[Type], List[Error]]: + + def visit_definition( + self, node: DefinitionNode + ) -> Tuple[Optional[Type], List[Error]]: """ Infer the type of a definition node. - + For definitions, infer the type of the definition body and check that it matches the defined symbol type. - + Args: node: The definition node - + Returns: The type of the definition and a list of errors """ @@ -309,17 +371,24 @@ def visit_definition(self, node: DefinitionNode) -> Tuple[Optional[Type], List[E body_type, body_errors = node.definition_body_ast.accept(self) if body_errors: return None, body_errors - + if body_type is None: - return None, [Error("Cannot determine type for definition body", node.definition_body_ast)] - + return None, [ + Error( + "Cannot determine type for definition body", + node.definition_body_ast, + ) + ] + # Check that the body type matches the defined symbol type if not self.type_system.is_subtype(body_type, node.defined_symbol_type): - return None, [Error( - f"Definition body has type {body_type}, but symbol is defined with type {node.defined_symbol_type}", - node - )] - + return None, [ + Error( + f"Definition body has type {body_type}, but symbol is defined with type {node.defined_symbol_type}", + node, + ) + ] + # The type of the definition is the defined symbol type return node.defined_symbol_type, [] @@ -327,15 +396,20 @@ def visit_definition(self, node: DefinitionNode) -> Tuple[Optional[Type], List[E class TypeCheckingVisitor(ASTVisitor[List[Error]]): """ Visitor for checking that AST nodes have the expected types. - + This visitor implements the visitor pattern to traverse the AST and check that nodes have the expected types. """ - - def __init__(self, type_system: 'TypeSystemManager', environment: TypeEnvironment, expected_type: Type): + + def __init__( + self, + type_system: "TypeSystemManager", + environment: TypeEnvironment, + expected_type: Type, + ): """ Initialize a type checking visitor. - + Args: type_system: The type system manager to use for type checking environment: The type environment to use for variable lookups @@ -345,171 +419,211 @@ def __init__(self, type_system: 'TypeSystemManager', environment: TypeEnvironmen self.environment = environment self.expected_type = expected_type self.inference_visitor = TypeInferenceVisitor(type_system, environment) - + def visit_constant(self, node: ConstantNode) -> List[Error]: """ Check that a constant node has the expected type. - + Args: node: The constant node - + Returns: A list of errors, empty if the node has the expected type """ if not self.type_system.is_subtype(node.type, self.expected_type): - return [Error(f"Constant {node.name} has type {node.type}, expected {self.expected_type}", node)] + return [ + Error( + f"Constant {node.name} has type {node.type}, expected {self.expected_type}", + node, + ) + ] return [] - + def visit_variable(self, node: VariableNode) -> List[Error]: """ Check that a variable node has the expected type. - + Args: node: The variable node - + Returns: A list of errors, empty if the node has the expected type """ var_type, var_errors = self.inference_visitor.visit_variable(node) if var_errors: return var_errors - + if var_type is None: return [Error(f"Cannot determine type for variable {node.name}", node)] - + if not self.type_system.is_subtype(var_type, self.expected_type): - return [Error(f"Variable {node.name} has type {var_type}, expected {self.expected_type}", node)] - + return [ + Error( + f"Variable {node.name} has type {var_type}, expected {self.expected_type}", + node, + ) + ] + return [] - + def visit_application(self, node: ApplicationNode) -> List[Error]: """ Check that an application node has the expected type. - + Args: node: The application node - + Returns: A list of errors, empty if the node has the expected type """ app_type, app_errors = self.inference_visitor.visit_application(node) if app_errors: return app_errors - + if app_type is None: return [Error(f"Cannot determine type for application {node}", node)] - + if not self.type_system.is_subtype(app_type, self.expected_type): - return [Error(f"Application has type {app_type}, expected {self.expected_type}", node)] - + return [ + Error( + f"Application has type {app_type}, expected {self.expected_type}", + node, + ) + ] + return [] - + def visit_quantifier(self, node: QuantifierNode) -> List[Error]: """ Check that a quantifier node has the expected type. - + Args: node: The quantifier node - + Returns: A list of errors, empty if the node has the expected type """ quant_type, quant_errors = self.inference_visitor.visit_quantifier(node) if quant_errors: return quant_errors - + if quant_type is None: return [Error(f"Cannot determine type for quantifier {node}", node)] - + if not self.type_system.is_subtype(quant_type, self.expected_type): - return [Error(f"Quantifier has type {quant_type}, expected {self.expected_type}", node)] - + return [ + Error( + f"Quantifier has type {quant_type}, expected {self.expected_type}", + node, + ) + ] + return [] - + def visit_connective(self, node: ConnectiveNode) -> List[Error]: """ Check that a connective node has the expected type. - + Args: node: The connective node - + Returns: A list of errors, empty if the node has the expected type """ conn_type, conn_errors = self.inference_visitor.visit_connective(node) if conn_errors: return conn_errors - + if conn_type is None: return [Error(f"Cannot determine type for connective {node}", node)] - + if not self.type_system.is_subtype(conn_type, self.expected_type): - return [Error(f"Connective has type {conn_type}, expected {self.expected_type}", node)] - + return [ + Error( + f"Connective has type {conn_type}, expected {self.expected_type}", + node, + ) + ] + return [] - + def visit_modal_op(self, node: ModalOpNode) -> List[Error]: """ Check that a modal operator node has the expected type. - + Args: node: The modal operator node - + Returns: A list of errors, empty if the node has the expected type """ modal_type, modal_errors = self.inference_visitor.visit_modal_op(node) if modal_errors: return modal_errors - + if modal_type is None: return [Error(f"Cannot determine type for modal operator {node}", node)] - + if not self.type_system.is_subtype(modal_type, self.expected_type): - return [Error(f"Modal operator has type {modal_type}, expected {self.expected_type}", node)] - + return [ + Error( + f"Modal operator has type {modal_type}, expected {self.expected_type}", + node, + ) + ] + return [] - + def visit_lambda(self, node: LambdaNode) -> List[Error]: """ Check that a lambda node has the expected type. - + Args: node: The lambda node - + Returns: A list of errors, empty if the node has the expected type """ lambda_type, lambda_errors = self.inference_visitor.visit_lambda(node) if lambda_errors: return lambda_errors - + if lambda_type is None: return [Error(f"Cannot determine type for lambda {node}", node)] - + if not self.type_system.is_subtype(lambda_type, self.expected_type): - return [Error(f"Lambda has type {lambda_type}, expected {self.expected_type}", node)] - + return [ + Error( + f"Lambda has type {lambda_type}, expected {self.expected_type}", + node, + ) + ] + return [] - + def visit_definition(self, node: DefinitionNode) -> List[Error]: """ Check that a definition node has the expected type. - + Args: node: The definition node - + Returns: A list of errors, empty if the node has the expected type """ def_type, def_errors = self.inference_visitor.visit_definition(node) if def_errors: return def_errors - + if def_type is None: return [Error(f"Cannot determine type for definition {node}", node)] - + if not self.type_system.is_subtype(def_type, self.expected_type): - return [Error(f"Definition has type {def_type}, expected {self.expected_type}", node)] - - return [] \ No newline at end of file + return [ + Error( + f"Definition has type {def_type}, expected {self.expected_type}", + node, + ) + ] + + return [] diff --git a/requirements.txt b/requirements.txt index 5f82d3d..84efdbc 100644 --- a/requirements.txt +++ b/requirements.txt @@ -4,10 +4,12 @@ psutil>=5.9.0 spacy>=3.5.0 nltk>=3.8.0 semver>=3.0.0 +networkx>=2.8.0 +requests>=2.31.0 # Development dependencies pytest>=7.0.0 pytest-cov>=4.0.0 black>=23.0.0 isort>=5.0.0 -mypy>=1.0.0 \ No newline at end of file +mypy>=1.0.0 diff --git a/setup.py b/setup.py index 86b62c5..767bafd 100644 --- a/setup.py +++ b/setup.py @@ -11,6 +11,8 @@ install_requires=[ # Core dependencies "typing-extensions>=4.0.0", + "networkx>=2.8.0", + "requests>=2.31.0", ], extras_require={ "dev": [