This commit is contained in:
Johan B.W. de Vries 2025-07-12 11:31:05 +02:00
parent 1a3bc19dce
commit 1d107d1baa
23 changed files with 1217 additions and 8 deletions

22
TODO.md
View File

@ -22,3 +22,25 @@
- Try to implement the min and max functions using select
- Read https://bytecodealliance.org/articles/multi-value-all-the-wasm
- GRose :: (* -> *) -> * -> *
- skolem => variable that cannot be unified
Limitations (for now):
- no type level nats
- only support first order kinds
Do not support yet:
```
data Record f = Record {
field: f Int
}
Record :: (* -> *) -> *
```
(Nested arrows)
- only support rank 1 types
```
mapRecord :: forall f g. (forall a. f a -> f b) -> Record f -> Record g
```
(Nested forall)

View File

@ -27,6 +27,8 @@ from ..type3.types import (
TypeConstructor_Struct,
TypeConstructor_Tuple,
)
from ..type5 import kindexpr as type5kindexpr
from ..type5 import typeexpr as type5typeexpr
from ..wasm import WasmType, WasmTypeInt32, WasmTypeNone
from . import builtins
@ -55,7 +57,9 @@ class MissingImplementationWarning(Warning):
class BuildBase[G]:
__slots__ = (
'dynamic_array',
'dynamic_array_type5_constructor',
'function',
'function_type5_constructor',
'static_array',
'struct',
'tuple_',
@ -67,6 +71,7 @@ class BuildBase[G]:
'type_info_constructed',
'types',
'type5s',
'type_classes',
'type_class_instances',
'type_class_instance_methods',
@ -84,6 +89,8 @@ class BuildBase[G]:
determined length, and each argument is the same.
"""
dynamic_array_type5_constructor: type5typeexpr.TypeConstructor
function: TypeConstructor_Function
"""
This is a function.
@ -91,6 +98,8 @@ class BuildBase[G]:
It should be applied with one or more arguments. The last argument is the 'return' type.
"""
function_type5_constructor: type5typeexpr.TypeConstructor
static_array: TypeConstructor_StaticArray
"""
This is a fixed length piece of memory.
@ -142,6 +151,11 @@ class BuildBase[G]:
Types that are available without explicit import.
"""
type5s: dict[str, type5typeexpr.TypeExpr]
"""
Types that are available without explicit import.
"""
type_classes: dict[str, Type3Class]
"""
Type classes that are available without explicit import.
@ -179,6 +193,11 @@ class BuildBase[G]:
self.struct = builtins.struct
self.tuple_ = builtins.tuple_
S = type5kindexpr.Star()
self.function_type5_constructor = type5typeexpr.TypeConstructor(kind=S >> (S >> S), name="function")
self.dynamic_array_type5_constructor = type5typeexpr.TypeConstructor(kind=S >> S, name="dynamic_array")
self.bool_ = builtins.bool_
self.none_ = builtins.none_
@ -193,6 +212,7 @@ class BuildBase[G]:
'None': self.none_,
'bool': self.bool_,
}
self.type5s = {}
self.type_classes = {}
self.type_class_instances = set()
self.type_class_instance_methods = {}

View File

@ -14,6 +14,8 @@ from ..type3.types import (
TypeConstructor_Struct,
TypeConstructor_Tuple,
)
from ..type5.kindexpr import Star
from ..type5.typeexpr import TypeConstructor as Type5Constructor
dynamic_array = TypeConstructor_DynamicArray('dynamic_array')
function = TypeConstructor_Function('function')
@ -24,3 +26,6 @@ tuple_ = TypeConstructor_Tuple('tuple')
bool_ = Type3('bool', TypeApplication_Nullary(None, None))
none_ = Type3('None', TypeApplication_Nullary(None, None))
s = Star()
static_array5 = Type5Constructor(name="static_array", kind=s >> s)

View File

@ -11,6 +11,7 @@ from ..type3.types import (
Type3,
TypeApplication_Nullary,
)
from ..type5 import typeexpr as type5typeexpr
from ..wasm import (
WasmTypeFloat32,
WasmTypeFloat64,
@ -82,6 +83,12 @@ class BuildDefault(BuildBase[Generator]):
'bytes': bytes_,
})
u8_5 = type5typeexpr.AtomicType('u8')
self.type5s.update({
'u8': u8_5,
'bytes': type5typeexpr.TypeApplication(self.dynamic_array_type5_constructor, u8_5),
})
tc_list = [
bits,
eq, ord,

View File

@ -7,18 +7,21 @@ from .build.base import BuildBase
from .type3.functions import FunctionSignature, TypeVariableContext
from .type3.typeclasses import Type3ClassMethod
from .type3.types import Type3, TypeApplication_Struct
from .type5 import typeexpr as type5typeexpr
class Expression:
"""
An expression within a statement
"""
__slots__ = ('type3', )
__slots__ = ('type3', 'type5', )
type3: Type3 | None
type5: type5typeexpr.TypeExpr | None
def __init__(self) -> None:
self.type3 = None
self.type5 = None
class Constant(Expression):
"""
@ -277,7 +280,7 @@ class Function:
"""
A function processes input and produces output
"""
__slots__ = ('name', 'lineno', 'exported', 'imported', 'statements', 'signature', 'returns_type3', 'posonlyargs', )
__slots__ = ('name', 'lineno', 'exported', 'imported', 'statements', 'signature', 'returns_type3', 'type5', 'posonlyargs', )
name: str
lineno: int
@ -286,6 +289,7 @@ class Function:
statements: List[Statement]
signature: FunctionSignature
returns_type3: Type3
type5: type5typeexpr.TypeExpr | None
posonlyargs: List[FunctionParam]
def __init__(self, name: str, lineno: int, returns_type3: Type3) -> None:
@ -296,6 +300,7 @@ class Function:
self.statements = []
self.signature = FunctionSignature(TypeVariableContext(), [])
self.returns_type3 = returns_type3
self.type5 = None
self.posonlyargs = []
class StructDefinition:
@ -339,17 +344,19 @@ class ModuleConstantDef:
"""
A constant definition within a module
"""
__slots__ = ('name', 'lineno', 'type3', 'constant', )
__slots__ = ('name', 'lineno', 'type3', 'type5', 'constant', )
name: str
lineno: int
type3: Type3
type5: type5typeexpr.TypeExpr
constant: Constant
def __init__(self, name: str, lineno: int, type3: Type3, constant: Constant) -> None:
def __init__(self, name: str, lineno: int, type3: Type3, type5: type5typeexpr.TypeExpr, constant: Constant) -> None:
self.name = name
self.lineno = lineno
self.type3 = type3
self.type5 = type5
self.constant = constant
class ModuleDataBlock:
@ -383,11 +390,12 @@ class Module[G]:
"""
A module is a file and consists of functions
"""
__slots__ = ('build', 'data', 'types', 'struct_definitions', 'constant_defs', 'functions', 'methods', 'operators', 'functions_table', )
__slots__ = ('build', 'data', 'types', 'type5s', 'struct_definitions', 'constant_defs', 'functions', 'methods', 'operators', 'functions_table', )
build: BuildBase[G]
data: ModuleData
types: dict[str, Type3]
type5s: dict[str, type5typeexpr.TypeExpr]
struct_definitions: Dict[str, StructDefinition]
constant_defs: Dict[str, ModuleConstantDef]
functions: Dict[str, Function]
@ -400,6 +408,7 @@ class Module[G]:
self.data = ModuleData()
self.types = {}
self.type5s = {}
self.struct_definitions = {}
self.constant_defs = {}
self.functions = {}

View File

@ -34,6 +34,7 @@ from .ourlang import (
)
from .type3.typeclasses import Type3ClassMethod
from .type3.types import IntType3, Type3
from .type5 import typeexpr as type5typeexpr
from .wasmgenerator import Generator
@ -101,6 +102,7 @@ class OurVisitor[G]:
module.methods.update(self.build.methods)
module.operators.update(self.build.operators)
module.types.update(self.build.types)
module.type5s.update(self.build.type5s)
_not_implemented(not node.type_ignores, 'Module.type_ignores')
@ -160,11 +162,14 @@ class OurVisitor[G]:
_not_implemented(not node.args.posonlyargs, 'FunctionDef.args.posonlyargs')
arg_type5_list = []
for arg in node.args.args:
if arg.annotation is None:
_raise_static_error(node, 'Must give a argument type')
arg_type = self.visit_type(module, arg.annotation)
arg_type5_list.append(self.visit_type5(module, arg.annotation))
# FIXME: Allow TypeVariable in the function signature
# This would also require FunctionParam to accept a placeholder
@ -216,9 +221,18 @@ class OurVisitor[G]:
if node.returns is None: # Note: `-> None` would be a ast.Constant
_raise_static_error(node, 'Must give a return type')
return_type = self.visit_type(module, node.returns)
arg_type5_list.append(self.visit_type5(module, node.returns))
function.signature.args.append(return_type)
function.returns_type3 = return_type
for arg_type5 in reversed(arg_type5_list):
if function.type5 is None:
function.type5 = arg_type5
continue
raise NotImplementedError('TODO: Applying the function type')
_not_implemented(not node.type_comment, 'FunctionDef.type_comment')
return function
@ -264,6 +278,7 @@ class OurVisitor[G]:
node.target.id,
node.lineno,
self.visit_type(module, node.annotation),
self.visit_type5(module, node.annotation),
value_data,
)
@ -277,6 +292,7 @@ class OurVisitor[G]:
node.target.id,
node.lineno,
self.visit_type(module, node.annotation),
self.visit_type5(module, node.annotation),
value_data,
)
@ -290,6 +306,7 @@ class OurVisitor[G]:
node.target.id,
node.lineno,
self.visit_type(module, node.annotation),
self.visit_type5(module, node.annotation),
value_data,
)
@ -664,6 +681,18 @@ class OurVisitor[G]:
raise NotImplementedError(f'{node} as type')
def visit_type5(self, module: Module[G], node: ast.expr) -> type5typeexpr.TypeExpr:
if isinstance(node, ast.Name):
if not isinstance(node.ctx, ast.Load):
_raise_static_error(node, 'Must be load context')
if node.id in module.type5s:
return module.type5s[node.id]
_raise_static_error(node, f'Unrecognized type {node.id}')
raise NotImplementedError
def _not_implemented(check: Any, msg: str) -> None:
if not check:
raise NotImplementedError(msg)

0
phasm/type4/__init__.py Normal file
View File

131
phasm/type4/classes.py Normal file
View File

@ -0,0 +1,131 @@
from __future__ import annotations
from dataclasses import dataclass
from typing import TypeAlias
## Kind * (part 1)
@dataclass
class Atomic:
"""
Atomic (or base or fundamental) type - it doesn't construct anything and wasn't constructed
"""
name: str
class Struct(Atomic):
"""
Structs are a fundamental type. But we need to store some extra info.
"""
fields: list[tuple[str, Type4]]
@dataclass
class Variable:
"""
Type variable of kind *.
"""
name: str
@dataclass
class Nat:
"""
Some type constructors take a natural number as argument, rather than a type.
"""
value: int
@property
def name(self) -> str:
return str(self.value)
## Kind * -> *
@dataclass
class ConcreteConSS:
"""
An concrete type construtor of kind * -> *, like dynamic array.
"""
name: str
@dataclass
class VariableConSS:
"""
A type variable of kind * -> *.
"""
name: str
@dataclass
class AppliedConSS:
"""
An application of a type constructor of kind * -> *.
The result is a type of kind *.
"""
con: ConcreteConSS | VariableConSS | AppliedConSSS | AppliedConNSS
arg: Type4
@property
def name(self) -> str:
return f'{self.con.name} {self.arg.name}'
## Kind * -> * -> *
@dataclass
class ConcreteConSSS:
"""
An concrete type construtor of kind * -> * -> *, like function, tuple or Either.
"""
name: str
@dataclass
class VariableConSSS:
"""
A type variable of kind * -> * -> *.
"""
name: str
@dataclass
class AppliedConSSS:
"""
An application of a type constructor of kind * -> * -> *.
The result is a type construtor of kind * -> *.
"""
con: ConcreteConSSS | VariableConSSS
arg: Type4
@property
def name(self) -> str:
return f'{self.con.name} {self.arg.name}'
## Kind Nat -> * -> *
@dataclass
class ConcreteConNSS:
"""
An concrete type construtor of kind Nat -> * -> *, like static array.
"""
name: str
@dataclass
class VariableConNSS:
"""
A type variable of kind Nat -> * -> *.
"""
name: str
@dataclass
class AppliedConNSS:
"""
An application of a type constructor of kind Nat -> * -> *.
The result is a type construtor of kind * -> *.
"""
con: ConcreteConNSS | VariableConNSS
arg: Nat
@property
def name(self) -> str:
return f'{self.con.name} {self.arg.name}'
# Kind * (part 2)
Type4: TypeAlias = Atomic | Variable | AppliedConSS

202
phasm/type4/unify.py Normal file
View File

@ -0,0 +1,202 @@
from dataclasses import dataclass
from .classes import (
AppliedConNSS,
AppliedConSS,
AppliedConSSS,
Atomic,
ConcreteConNSS,
ConcreteConSS,
ConcreteConSSS,
Type4,
Variable,
VariableConNSS,
VariableConSS,
VariableConSSS,
)
@dataclass
class Failure:
"""
Both types are already different - cannot be unified.
"""
msg: str
@dataclass
class Action:
pass
UnifyResult = Failure | list[Action]
@dataclass
class SetTypeForVariable(Action):
var: Variable
type: Atomic | AppliedConSS
@dataclass
class SetTypeForConSSVariable(Action):
var: VariableConSS
type: ConcreteConSS | AppliedConSSS | AppliedConNSS
@dataclass
class SetTypeForConSSSVariable(Action):
var: VariableConSSS
type: ConcreteConSSS
@dataclass
class ReplaceVariable(Action):
before: Variable
after: Variable
@dataclass
class ReplaceConSSVariable(Action):
before: VariableConSS
after: VariableConSS
def unify(lft: Type4, rgt: Type4) -> UnifyResult:
"""
Tries to unify the given two types.
"""
if isinstance(lft, Atomic) and isinstance(rgt, Atomic):
if lft == rgt:
return []
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
if isinstance(lft, Atomic) and isinstance(rgt, Variable):
return [SetTypeForVariable(rgt, lft)]
if isinstance(lft, Atomic) and isinstance(rgt, AppliedConSS):
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
if isinstance(lft, Variable) and isinstance(rgt, Atomic):
return [SetTypeForVariable(lft, rgt)]
if isinstance(lft, Variable) and isinstance(rgt, Variable):
return [ReplaceVariable(lft, rgt)]
if isinstance(lft, Variable) and isinstance(rgt, AppliedConSS):
return [SetTypeForVariable(lft, rgt)]
if isinstance(lft, AppliedConSS) and isinstance(rgt, Atomic):
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
if isinstance(lft, AppliedConSS) and isinstance(rgt, Variable):
return [SetTypeForVariable(rgt, lft)]
if isinstance(lft, AppliedConSS) and isinstance(rgt, AppliedConSS):
con_res = unify_con_ss(lft.con, rgt.con)
if isinstance(con_res, Failure):
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
arg_res = unify(lft.arg, rgt.arg)
if isinstance(arg_res, Failure):
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
return con_res + arg_res
raise NotImplementedError
def unify_con_ss(
lft: ConcreteConSS | VariableConSS | AppliedConSSS | AppliedConNSS,
rgt: ConcreteConSS | VariableConSS | AppliedConSSS | AppliedConNSS,
) -> UnifyResult:
"""
Tries to unify the given two constuctors of kind * -> *.
"""
if isinstance(lft, ConcreteConSS) and isinstance(rgt, ConcreteConSS):
if lft == rgt:
return []
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
if isinstance(lft, ConcreteConSS) and isinstance(rgt, VariableConSS):
return [SetTypeForConSSVariable(rgt, lft)]
if isinstance(lft, ConcreteConSS) and isinstance(rgt, AppliedConSSS):
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
if isinstance(lft, ConcreteConSS) and isinstance(rgt, AppliedConNSS):
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
if isinstance(lft, VariableConSS) and isinstance(rgt, ConcreteConSS):
return [SetTypeForConSSVariable(lft, rgt)]
if isinstance(lft, VariableConSS) and isinstance(rgt, VariableConSS):
return [ReplaceConSSVariable(lft, rgt)]
if isinstance(lft, VariableConSS) and isinstance(rgt, AppliedConSSS):
return [SetTypeForConSSVariable(lft, rgt)]
if isinstance(lft, VariableConSS) and isinstance(rgt, AppliedConNSS):
return [SetTypeForConSSVariable(lft, rgt)]
if isinstance(lft, AppliedConSSS) and isinstance(rgt, ConcreteConSS):
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
if isinstance(lft, AppliedConSSS) and isinstance(rgt, VariableConSS):
return [SetTypeForConSSVariable(rgt, lft)]
if isinstance(lft, AppliedConSSS) and isinstance(rgt, AppliedConSSS):
con_res = unify_con_sss(lft.con, rgt.con)
if isinstance(con_res, Failure):
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
arg_res = unify(lft.arg, rgt.arg)
if isinstance(arg_res, Failure):
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
return con_res + arg_res
if isinstance(lft, AppliedConSSS) and isinstance(rgt, AppliedConNSS):
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
if isinstance(lft, AppliedConNSS) and isinstance(rgt, ConcreteConSS):
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
if isinstance(lft, AppliedConNSS) and isinstance(rgt, VariableConSS):
return [SetTypeForConSSVariable(rgt, lft)]
if isinstance(lft, AppliedConNSS) and isinstance(rgt, AppliedConSSS):
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
if isinstance(lft, AppliedConNSS) and isinstance(rgt, AppliedConNSS):
con_res = unify_con_nss(lft.con, rgt.con)
if isinstance(con_res, Failure):
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
if lft.arg.value != rgt.arg.value:
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
return con_res
raise NotImplementedError
def unify_con_sss(
lft: ConcreteConSSS | VariableConSSS,
rgt: ConcreteConSSS | VariableConSSS,
) -> UnifyResult:
"""
Tries to unify the given two constuctors of kind * -> * -> *.
"""
if isinstance(lft, ConcreteConSSS) and isinstance(rgt, ConcreteConSSS):
if lft == rgt:
return []
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
raise NotImplementedError
def unify_con_nss(
lft: ConcreteConNSS | VariableConNSS,
rgt: ConcreteConNSS | VariableConNSS,
) -> UnifyResult:
"""
Tries to unify the given two constuctors of kind * -> * -> *.
"""
if isinstance(lft, ConcreteConNSS) and isinstance(rgt, ConcreteConNSS):
if lft == rgt:
return []
return Failure(f'Cannot unify {lft.name} and {rgt.name}')
raise NotImplementedError

0
phasm/type5/__init__.py Normal file
View File

93
phasm/type5/__main__.py Normal file
View File

@ -0,0 +1,93 @@
from .kindexpr import Star
from .record import Record
from .typeexpr import AtomicType, TypeApplication, TypeConstructor, TypeVariable
from .unify import unify
def main() -> None:
S = Star()
a_var = TypeVariable(name="a", kind=S)
b_var = TypeVariable(name="b", kind=S)
t_var = TypeVariable(name="t", kind=S >> S)
r_var = TypeVariable(name="r", kind=S >> S)
print(a_var)
print(b_var)
print(t_var)
print(r_var)
print()
u32_type = AtomicType(name="u32")
f64_type = AtomicType(name="f64")
print(u32_type)
print(f64_type)
print()
maybe_constructor = TypeConstructor(name="Maybe", kind=S >> S)
maybe_a_type = TypeApplication(constructor=maybe_constructor, argument=a_var)
maybe_u32_type = TypeApplication(constructor=maybe_constructor, argument=u32_type)
print(maybe_constructor)
print(maybe_a_type)
print(maybe_u32_type)
print()
either_constructor = TypeConstructor(name="Either", kind=S >> (S >> S))
either_a_constructor = TypeApplication(constructor=either_constructor, argument=a_var)
either_a_a_type = TypeApplication(constructor=either_a_constructor, argument=a_var)
either_u32_constructor = TypeApplication(constructor=either_constructor, argument=u32_type)
either_u32_f64_type = TypeApplication(constructor=either_u32_constructor, argument=f64_type)
either_u32_a_type = TypeApplication(constructor=either_u32_constructor, argument=a_var)
print(either_constructor)
print(either_a_constructor)
print(either_a_a_type)
print(either_u32_constructor)
print(either_u32_f64_type)
print(either_u32_a_type)
print()
t_a_type = TypeApplication(constructor=t_var, argument=a_var)
t_u32_type = TypeApplication(constructor=t_var, argument=u32_type)
print(t_a_type)
print(t_u32_type)
print()
shape_record = Record("Shape", [
("width", u32_type),
("height", either_u32_f64_type),
])
print('shape_record', shape_record)
print()
values = [
a_var,
b_var,
u32_type,
f64_type,
t_var,
t_a_type,
r_var,
maybe_constructor,
maybe_u32_type,
maybe_a_type,
either_u32_constructor,
either_u32_a_type,
either_u32_f64_type,
]
seen_exprs: set[str] = set()
for lft in values:
for rgt in values:
expr = f"{lft.name} ~ {rgt.name}"
if expr in seen_exprs:
continue
print(expr.ljust(40) + " => " + str(unify(lft, rgt)))
inv_expr = f"{rgt.name} ~ {lft.name}"
seen_exprs.add(inv_expr)
print()
if __name__ == '__main__':
main()

122
phasm/type5/constraints.py Normal file
View File

@ -0,0 +1,122 @@
from typing import Any, Protocol
from ..build.base import BuildBase
from ..wasm import WasmTypeInt32, WasmTypeInt64
from .kindexpr import KindExpr, Star
from .typeexpr import TypeExpr, TypeVariable
from .unify import ActionList, Failure, ReplaceVariable, is_concrete, unify
class ExpressionProtocol(Protocol):
"""
A protocol for classes that should be updated on substitution
"""
type5: TypeExpr | None
"""
The type to update
"""
class Context:
__slots__ = ("build", "placeholder_update", )
build: BuildBase[Any]
placeholder_update: dict[TypeVariable, ExpressionProtocol]
def __init__(self, build: BuildBase[Any]) -> None:
self.build = build
self.placeholder_update = {}
def make_placeholder(self, arg: ExpressionProtocol, kind: KindExpr = Star()) -> TypeVariable:
res = TypeVariable(kind, f"p_{len(self.placeholder_update)}")
self.placeholder_update[res] = arg
return res
class SkipForNow:
pass
CheckResult = None | ActionList | Failure | SkipForNow
class ConstraintBase:
__slots__ = ("ctx", "comment",)
ctx: Context
comment: str | None
def __init__(self, ctx: Context, comment: str | None = None) -> None:
self.ctx = ctx
self.comment = comment
def check(self) -> CheckResult:
raise NotImplementedError(self)
def apply(self, action_list: ActionList) -> None:
for action in action_list:
if isinstance(action, ReplaceVariable):
self.replace_variable(action.var, action.typ)
continue
raise NotImplementedError(action)
def replace_variable(self, var: TypeVariable, typ: TypeExpr) -> None:
pass
class LiteralFitsConstraint(ConstraintBase):
__slots__ = ("type", "literal",)
def __init__(self, ctx: Context, type: TypeExpr, literal: Any, *, comment: str | None = None) -> None:
super().__init__(ctx, comment)
self.type = type
self.literal = literal
def check(self) -> CheckResult:
if not is_concrete(self.type):
return SkipForNow()
type_info = self.ctx.build.type_info_map.get(self.type.name)
if type_info is not None and (type_info.wasm_type is WasmTypeInt32 or type_info.wasm_type is WasmTypeInt64):
assert type_info.signed is not None
if not isinstance(self.literal.value, int):
return Failure('Must be integer')
try:
self.literal.value.to_bytes(type_info.alloc_size, 'big', signed=type_info.signed)
except OverflowError:
return Failure(f'Must fit in {type_info.alloc_size} byte(s)')
return None
raise NotImplementedError(type_info)
def replace_variable(self, var: TypeVariable, typ: TypeExpr) -> None:
if var == self.type:
self.type = typ
def __str__(self) -> str:
return f"{self.type} can contain {self.literal!r}"
class UnifyTypesConstraint(ConstraintBase):
__slots__ = ("lft", "rgt",)
def __init__(self, ctx: Context, lft: TypeExpr, rgt: TypeExpr, *, comment: str | None = None) -> None:
super().__init__(ctx, comment)
self.lft = lft
self.rgt = rgt
def check(self) -> CheckResult:
return unify(self.lft, self.rgt)
def replace_variable(self, var: TypeVariable, typ: TypeExpr) -> None:
if var == self.lft:
self.lft = typ
if var == self.rgt:
self.rgt = typ
def __str__(self) -> str:
return f"{self.lft} ~ {self.rgt}"

85
phasm/type5/fromast.py Normal file
View File

@ -0,0 +1,85 @@
from typing import Any, Generator
from .. import ourlang
from .constraints import (
ConstraintBase,
Context,
LiteralFitsConstraint,
UnifyTypesConstraint,
)
from .typeexpr import TypeApplication, TypeVariable
ConstraintGenerator = Generator[ConstraintBase, None, None]
def phasm_type5_generate_constraints(ctx: Context, inp: ourlang.Module[Any]) -> list[ConstraintBase]:
return [*module(ctx, inp)]
def expression_constant(ctx: Context, inp: ourlang.Constant, phft: TypeVariable) -> ConstraintGenerator:
if isinstance(inp, (ourlang.ConstantPrimitive, ourlang.ConstantBytes, ourlang.ConstantTuple, ourlang.ConstantStruct)):
yield LiteralFitsConstraint(
ctx, phft, inp,
comment='The given literal must fit the expected type'
)
return
raise NotImplementedError(inp)
def expression_variable_reference(ctx: Context, inp: ourlang.VariableReference, phft: TypeVariable) -> ConstraintGenerator:
if isinstance(inp.variable, ourlang.FunctionParam):
raise NotImplementedError
yield UnifyTypesConstraint(ctx, inp.variable.type5, phft)
def expression(ctx: Context, inp: ourlang.Expression, phft: TypeVariable) -> ConstraintGenerator:
if isinstance(inp, ourlang.Constant):
yield from expression_constant(ctx, inp, phft)
return
if isinstance(inp, ourlang.VariableReference):
yield from expression_variable_reference(ctx, inp, phft)
return
raise NotImplementedError(inp)
def statement_return(ctx: Context, fun: ourlang.Function, inp: ourlang.StatementReturn) -> ConstraintGenerator:
phft = ctx.make_placeholder(inp.value)
if fun.type5 is None:
raise NotImplementedError("Deducing function type - you'll have to annotate it.")
type5 = fun.type5
while isinstance(type5, TypeApplication) and type5.constructor == ctx.build.function_type5_constructor:
type5 = type5.argument
yield UnifyTypesConstraint(ctx, type5, phft)
yield from expression(ctx, inp.value, phft)
def statement(ctx: Context, fun: ourlang.Function, inp: ourlang.Statement) -> ConstraintGenerator:
if isinstance(inp, ourlang.StatementReturn):
yield from statement_return(ctx, fun, inp)
return
raise NotImplementedError(inp)
def function(ctx: Context, inp: ourlang.Function) -> ConstraintGenerator:
for stmt in inp.statements:
yield from statement(ctx, inp, stmt)
def module_constant_def(ctx: Context, inp: ourlang.ModuleConstantDef) -> ConstraintGenerator:
phft = ctx.make_placeholder(inp.constant)
yield from expression_constant(ctx, inp.constant, phft)
yield UnifyTypesConstraint(ctx, inp.type5, phft)
def module(ctx: Context, inp: ourlang.Module[Any]) -> ConstraintGenerator:
for cdef in inp.constant_defs.values():
yield from module_constant_def(ctx, cdef)
for func in inp.functions.values():
if func.imported:
continue
yield from function(ctx, func)
# TODO: Generalize?

46
phasm/type5/kindexpr.py Normal file
View File

@ -0,0 +1,46 @@
from __future__ import annotations
from dataclasses import dataclass
from typing import TypeAlias
@dataclass
class Star:
def __rshift__(self, other: KindExpr) -> Arrow:
return Arrow(self, other)
def __str__(self) -> str:
return "*"
def __hash__(self) -> int:
return 0 # All Stars are the same
@dataclass
class Arrow:
"""
Represents an arrow kind `K1 -> K2`.
To create K1 -> K2 -> K3, pass an Arrow for result_kind.
For now, we do not support Arrows as arguments (i.e.,
no higher order kinds).
"""
arg_kind: Star
result_kind: KindExpr
def __str__(self) -> str:
if isinstance(self.arg_kind, Star):
arg_kind = "*"
else:
arg_kind = f"({str(self.arg_kind)})"
if isinstance(self.result_kind, Star):
result_kind = "*"
else:
result_kind = f"({str(self.result_kind)})"
return f"{arg_kind} -> {result_kind}"
def __hash__(self) -> int:
return hash((self.arg_kind, self.result_kind, ))
KindExpr: TypeAlias = Star | Arrow

42
phasm/type5/record.py Normal file
View File

@ -0,0 +1,42 @@
from dataclasses import dataclass
from .kindexpr import Star
from .typeexpr import AtomicType, TypeApplication, TypeExpr
@dataclass
class Record(TypeExpr):
"""
Records are a fundamental type. But we need to store some extra info.
"""
fields: list[tuple[str, AtomicType | TypeApplication]]
def __init__(self, name: str, fields: list[tuple[str, AtomicType | TypeApplication]]) -> None:
for field_name, field_type in fields:
if field_type.kind == Star():
continue
raise TypeError(f"Record fields must be concrete types ({field_name} :: {field_type})")
super().__init__(Star(), name)
self.fields = fields
def __str__(self) -> str:
args = ", ".join(
f"{field_name} :: {field_type}"
for field_name, field_type in self.fields
)
return f"{self.name} {{{args}}} :: {self.kind}"
@dataclass
class RecordConstructor(TypeExpr):
"""
TODO.
i.e.:
```
class Foo[T, R]:
lft: T
rgt: R
"""
name: str

8
phasm/type5/router.py Normal file
View File

@ -0,0 +1,8 @@
from typing import Callable
from .typeexpr import TypeExpr
class TypeRouter[S, R]:
def add(self, typ: TypeExpr, mtd: Callable[[S, TypeExpr], R]) -> None:
raise NotImplementedError

61
phasm/type5/solver.py Normal file
View File

@ -0,0 +1,61 @@
from typing import Any
from .. import ourlang
from .constraints import Context, SkipForNow
from .fromast import phasm_type5_generate_constraints
from .typeexpr import TypeExpr, TypeVariable
from .unify import ActionList, Failure, ReplaceVariable
MAX_RESTACK_COUNT = 100
class Type5SolverException(Exception):
pass
def phasm_type5(inp: ourlang.Module[Any], verbose: bool = False) -> None:
ctx = Context(inp.build)
constraint_list = phasm_type5_generate_constraints(ctx, inp)
assert constraint_list
placeholder_types: dict[TypeVariable, TypeExpr] = {}
error_list: list[Failure] = []
for _ in range(MAX_RESTACK_COUNT):
new_constraint_list = []
for constraint in constraint_list:
print(constraint)
result = constraint.check()
if isinstance(result, SkipForNow):
new_constraint_list.append(constraint)
continue
if isinstance(result, Failure):
error_list.append(result)
continue
if isinstance(result, ActionList):
for action in result:
if isinstance(action, ReplaceVariable):
assert action.var not in placeholder_types
placeholder_types[action.var] = action.typ
continue
for constraint in constraint_list:
constraint.apply(result)
continue
raise NotImplementedError(result)
if error_list:
raise Type5SolverException(error_list)
if not new_constraint_list:
break
constraint_list = new_constraint_list
for placeholder, expression in ctx.placeholder_update.items():
expression.type5 = placeholder_types[placeholder]

55
phasm/type5/typeexpr.py Normal file
View File

@ -0,0 +1,55 @@
from __future__ import annotations
from dataclasses import dataclass
from .kindexpr import Arrow, KindExpr, Star
@dataclass
class TypeExpr:
kind: KindExpr
name: str
def __str__(self) -> str:
return f"{self.name} :: {self.kind}"
@dataclass
class AtomicType(TypeExpr):
def __init__(self, name: str) -> None:
super().__init__(Star(), name)
@dataclass
class TypeVariable(TypeExpr):
"""
A placeholder in a type expression
"""
def __hash__(self) -> int:
return hash((self.kind, self.name))
@dataclass
class TypeConstructor(TypeExpr):
name: str
def __init__(self, kind: Arrow, name: str) -> None:
super().__init__(kind, name)
@dataclass
class TypeApplication(TypeExpr):
constructor: TypeConstructor | TypeApplication | TypeVariable
argument: TypeExpr
def __init__(self, constructor: TypeConstructor | TypeApplication | TypeVariable, argument: TypeExpr) -> None:
if isinstance(constructor.kind, Star):
raise TypeError("A constructor cannot be a concrete type")
if constructor.kind.arg_kind != argument.kind:
raise TypeError("Argument does match construtor's expectations")
super().__init__(
constructor.kind.result_kind,
f"{constructor.name} {argument.name}",
)
self.constructor = constructor
self.argument = argument

157
phasm/type5/unify.py Normal file
View File

@ -0,0 +1,157 @@
from dataclasses import dataclass
from .typeexpr import (
AtomicType,
TypeApplication,
TypeConstructor,
TypeExpr,
TypeVariable,
)
@dataclass
class Failure:
"""
Both types are already different - cannot be unified.
"""
msg: str
@dataclass
class Action:
pass
class ActionList(list[Action]):
def __str__(self) -> str:
return '{' + ', '.join(map(str, self)) + '}'
UnifyResult = Failure | ActionList
@dataclass
class ReplaceVariable(Action):
var: TypeVariable
typ: TypeExpr
def __str__(self) -> str:
return f'{self.var.name} := {self.typ.name}'
def unify(lft: TypeExpr, rgt: TypeExpr) -> UnifyResult:
if lft == rgt:
return ActionList()
if lft.kind != rgt.kind:
return Failure("Kind mismatch")
if isinstance(lft, AtomicType) and isinstance(rgt, AtomicType):
return Failure("Not the same type")
if isinstance(lft, AtomicType) and isinstance(rgt, TypeVariable):
return ActionList([ReplaceVariable(rgt, lft)])
if isinstance(lft, AtomicType) and isinstance(rgt, TypeConstructor):
raise NotImplementedError # Should have been caught by kind check above
if isinstance(lft, AtomicType) and isinstance(rgt, TypeApplication):
if is_concrete(rgt):
return Failure("Not the same type")
return Failure("Type shape mismatch")
if isinstance(lft, TypeVariable) and isinstance(rgt, AtomicType):
return unify(rgt, lft)
if isinstance(lft, TypeVariable) and isinstance(rgt, TypeVariable):
return ActionList([ReplaceVariable(lft, rgt)])
if isinstance(lft, TypeVariable) and isinstance(rgt, TypeConstructor):
return ActionList([ReplaceVariable(lft, rgt)])
if isinstance(lft, TypeVariable) and isinstance(rgt, TypeApplication):
if occurs(lft, rgt):
return Failure("One type occurs in the other")
return ActionList([ReplaceVariable(lft, rgt)])
if isinstance(lft, TypeConstructor) and isinstance(rgt, AtomicType):
return unify(rgt, lft)
if isinstance(lft, TypeConstructor) and isinstance(rgt, TypeVariable):
return unify(rgt, lft)
if isinstance(lft, TypeConstructor) and isinstance(rgt, TypeConstructor):
return Failure("Not the same type constructor")
if isinstance(lft, TypeConstructor) and isinstance(rgt, TypeApplication):
return Failure("Not the same type constructor")
if isinstance(lft, TypeApplication) and isinstance(rgt, AtomicType):
return unify(rgt, lft)
if isinstance(lft, TypeApplication) and isinstance(rgt, TypeVariable):
return unify(rgt, lft)
if isinstance(lft, TypeApplication) and isinstance(rgt, TypeConstructor):
return unify(rgt, lft)
if isinstance(lft, TypeApplication) and isinstance(rgt, TypeApplication):
con_res = unify(lft.constructor, rgt.constructor)
if isinstance(con_res, Failure):
return con_res
arg_res = unify(lft.argument, rgt.argument)
if isinstance(arg_res, Failure):
return arg_res
return ActionList(con_res + arg_res)
return Failure('Not implemented')
def occurs(lft: TypeVariable, rgt: TypeApplication) -> bool:
"""
Checks whether the given variable occurs in the given application.
"""
if lft == rgt.constructor:
return True
if lft == rgt.argument:
return True
if isinstance(rgt.argument, TypeApplication):
return occurs(lft, rgt.argument)
return False
def is_concrete(lft: TypeExpr) -> bool:
"""
A concrete type has no variables in it.
This is also known as a monomorphic type.
"""
if isinstance(lft, AtomicType):
return True
if isinstance(lft, TypeVariable):
return False
if isinstance(lft, TypeConstructor):
return True
if isinstance(lft, TypeApplication):
return is_concrete(lft.constructor) and is_concrete(lft.argument)
raise NotImplementedError
def is_polymorphic(lft: TypeExpr) -> bool:
"""
A polymorphic type has one or more variables in it.
"""
return not is_concrete(lft)

View File

@ -11,6 +11,7 @@ from phasm.compiler import phasm_compile
from phasm.optimise.removeunusedfuncs import removeunusedfuncs
from phasm.parser import phasm_parse
from phasm.type3.entry import phasm_type3
from phasm.type5.solver import phasm_type5
from phasm.wasmgenerator import Generator as WasmGenerator
Imports = Optional[Dict[str, Callable[[Any], Any]]]
@ -39,6 +40,7 @@ class RunnerBase:
Parses the Phasm code into an AST
"""
self.phasm_ast = phasm_parse(self.phasm_code)
phasm_type5(self.phasm_ast, verbose=verbose)
phasm_type3(self.phasm_ast, verbose=verbose)
def compile_ast(self) -> None:

View File

@ -1,6 +1,6 @@
import pytest
from phasm.type3.entry import Type3Exception
from phasm.type5.solver import Type5SolverException
from ..helpers import Suite
@ -15,7 +15,7 @@ def testEntry() -> u8:
return CONSTANT
"""
with pytest.raises(Type3Exception, match=r'Must fit in 1 byte\(s\)'):
with pytest.raises(Type5SolverException, match=r'Must fit in 1 byte\(s\)'):
Suite(code_py).run_code()
@pytest.mark.integration_test
@ -26,5 +26,5 @@ def testEntry() -> u8:
return 1000
"""
with pytest.raises(Type3Exception, match=r'Must fit in 1 byte\(s\)'):
with pytest.raises(Type5SolverException, match=r'Must fit in 1 byte\(s\)'):
Suite(code_py).run_code()

View File

View File

@ -0,0 +1,113 @@
import pytest
from phasm.type4 import classes
from phasm.type4 import unify as sut
class TestNamespace:
## Kind * (part 1)
u32 = classes.Atomic('u32')
f64 = classes.Atomic('f64')
a = classes.Variable('a')
b = classes.Variable('b')
## Kind * -> *
dynamic_array = classes.ConcreteConSS('dynamic_array')
maybe = classes.ConcreteConSS('maybe')
f = classes.VariableConSS('f')
t = classes.VariableConSS('t')
## Kind * -> * -> *
function = classes.ConcreteConSSS('function')
either = classes.ConcreteConSSS('either')
## Kind Nat -> * -> *
static_array = classes.ConcreteConNSS('static_array')
## Kind * -> * (part 2)
function_u32 = classes.AppliedConSSS(function, u32)
function_f64 = classes.AppliedConSSS(function, f64)
either_u32 = classes.AppliedConSSS(either, u32)
either_f64 = classes.AppliedConSSS(either, f64)
static_array_4 = classes.AppliedConNSS(static_array, classes.Nat(4))
static_array_8 = classes.AppliedConNSS(static_array, classes.Nat(8))
## Kind * (part 2)
dynamic_array_u32 = classes.AppliedConSS(dynamic_array, u32)
dynamic_array_f64 = classes.AppliedConSS(dynamic_array, f64)
maybe_u32 = classes.AppliedConSS(maybe, u32)
maybe_f64 = classes.AppliedConSS(maybe, f64)
t_u32 = classes.AppliedConSS(t, u32)
t_f64 = classes.AppliedConSS(t, f64)
f_u32 = classes.AppliedConSS(f, u32)
f_f64 = classes.AppliedConSS(f, f64)
function_f64_u32 = classes.AppliedConSS(function_f64, u32)
either_f64_u32 = classes.AppliedConSS(either_f64, u32)
static_array_4_u32 = classes.AppliedConSS(static_array_4, u32)
static_array_8_u32 = classes.AppliedConSS(static_array_8, u32)
TEST_LIST: list[tuple[classes.Type4, classes.Type4, sut.UnifyResult]] = [
# Atomic / Atomic
(u32, u32, []),
(u32, f64, sut.Failure('Cannot unify u32 and f64')),
# Atomic / Variable
(u32, a, [sut.SetTypeForVariable(a, u32)]),
# Atomic / AppliedConSS
(u32, t_f64, sut.Failure('Cannot unify u32 and t f64')),
# Variable / Atomic
(a, u32, [sut.SetTypeForVariable(a, u32)]),
# Variable / Variable
(a, b, [sut.ReplaceVariable(a, b)]),
# Variable / AppliedConSS
(a, t_f64, [sut.SetTypeForVariable(a, t_f64)]),
# AppliedConSS / Atomic
(t_f64, u32, sut.Failure('Cannot unify t f64 and u32')),
# AppliedConSS / Variable
(t_f64, a, [sut.SetTypeForVariable(a, t_f64)]),
# AppliedConSS ConcreteConSS / AppliedConSS ConcreteConSS
(dynamic_array_u32, dynamic_array_u32, []),
(dynamic_array_u32, maybe_u32, sut.Failure('Cannot unify dynamic_array u32 and maybe u32')),
# AppliedConSS ConcreteConSS / AppliedConSS VariableConSS
(dynamic_array_u32, t_u32, [sut.SetTypeForConSSVariable(t, dynamic_array)]),
# AppliedConSS ConcreteConSS / AppliedConSS AppliedConSSS
(dynamic_array_u32, function_f64_u32, sut.Failure('Cannot unify dynamic_array u32 and function f64 u32')),
# AppliedConSS ConcreteConSS / AppliedConSS AppliedConNSS
(dynamic_array_u32, static_array_4_u32, sut.Failure('Cannot unify dynamic_array u32 and static_array 4 u32')),
# AppliedConSS VariableConSS / AppliedConSS ConcreteConSS
(t_u32, dynamic_array_u32, [sut.SetTypeForConSSVariable(t, dynamic_array)]),
# AppliedConSS VariableConSS / AppliedConSS VariableConSS
(t_u32, f_u32, [sut.ReplaceConSSVariable(t, f)]),
# AppliedConSS VariableConSS / AppliedConSS AppliedConSSS
(t_u32, function_f64_u32, [sut.SetTypeForConSSVariable(t, function_f64)]),
# AppliedConSS VariableConSS / AppliedConSS AppliedConNSS
(t_u32, static_array_4_u32, [sut.SetTypeForConSSVariable(t, static_array_4)]),
# AppliedConSS AppliedConSSS / AppliedConSS ConcreteConSS
(function_f64_u32, dynamic_array_u32, sut.Failure('Cannot unify function f64 u32 and dynamic_array u32')),
# AppliedConSS AppliedConSSS / AppliedConSS VariableConSS
(function_f64_u32, t_u32, [sut.SetTypeForConSSVariable(t, function_f64)]),
# AppliedConSS AppliedConSSS / AppliedConSS AppliedConSSS
# (function_f64_u32, function_f64_u32, []),
(function_f64_u32, either_f64_u32, sut.Failure('Cannot unify function f64 u32 and either f64 u32')),
# AppliedConSS AppliedConSSS / AppliedConSS AppliedConNSS
(function_f64_u32, static_array_4_u32, sut.Failure('Cannot unify function f64 u32 and static_array 4 u32')),
# AppliedConSS AppliedConNSS / AppliedConSS ConcreteConSS
(static_array_4_u32, dynamic_array_u32, sut.Failure('Cannot unify static_array 4 u32 and dynamic_array u32')),
# AppliedConSS AppliedConNSS / AppliedConSS VariableConSS
(static_array_4_u32, t_u32, [sut.SetTypeForConSSVariable(t, static_array_4)]),
# AppliedConSS AppliedConNSS / AppliedConSS AppliedConSSS
(static_array_4_u32, function_f64_u32, sut.Failure('Cannot unify static_array 4 u32 and function f64 u32')),
# AppliedConSS AppliedConNSS / AppliedConSS AppliedConNSS
(static_array_4_u32, static_array_4_u32, []),
(static_array_4_u32, static_array_8_u32, sut.Failure('Cannot unify static_array 4 u32 and static_array 8 u32')),
]
@pytest.mark.parametrize('lft,rgt,exp_out', TestNamespace.TEST_LIST)
def test_unify(lft: classes.Type4, rgt: classes.Type4, exp_out: sut.UnifyResult) -> None:
assert exp_out == sut.unify(lft, rgt)