9a30ca7475
type5 is much more first principles based, so we get a lot of weird quirks removed: - FromLiteral no longer needs to understand AST - Type unifications works more like Haskell - Function types are just ordinary types, saving a lot of manual busywork and more.
121 lines
3.4 KiB
Python
121 lines
3.4 KiB
Python
from dataclasses import dataclass
|
|
from typing import Callable
|
|
|
|
from .typeexpr import (
|
|
AtomicType,
|
|
TypeApplication,
|
|
TypeConstructor,
|
|
TypeExpr,
|
|
TypeVariable,
|
|
is_concrete,
|
|
occurs,
|
|
)
|
|
|
|
|
|
@dataclass
|
|
class Failure:
|
|
"""
|
|
Both types are already different - cannot be unified.
|
|
"""
|
|
msg: str
|
|
|
|
@dataclass
|
|
class Action:
|
|
def to_str(self, type_namer: Callable[[TypeExpr], str]) -> str:
|
|
raise NotImplementedError
|
|
|
|
class ActionList(list[Action]):
|
|
def to_str(self, type_namer: Callable[[TypeExpr], str]) -> str:
|
|
return '{' + ', '.join((x.to_str(type_namer) for x in self)) + '}'
|
|
|
|
UnifyResult = Failure | ActionList
|
|
|
|
@dataclass
|
|
class ReplaceVariable(Action):
|
|
var: TypeVariable
|
|
typ: TypeExpr
|
|
|
|
def to_str(self, type_namer: Callable[[TypeExpr], str]) -> str:
|
|
return f'{self.var.name} := {type_namer(self.typ)}'
|
|
|
|
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')
|