Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Polytypes #16

Draft
wants to merge 81 commits into
base: master
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
81 commits
Select commit Hold shift + click to select a range
8dd988b
Liquid variable lookup is reversed
alcides May 31, 2023
8ee8df8
WIP
alcides Jun 29, 2023
b15b801
Added first polymorphic test
alcides Jul 13, 2023
b803536
Get Type Vars
alcides Jul 15, 2023
d234cae
Fixed the problem with native and whitespace
alcides Jul 17, 2023
3702385
Progress on polymorphism
alcides Jul 17, 2023
f9fd8fa
Added recursion scheme
alcides Jul 17, 2023
791d6e8
Added polymorphism-related elaboration
alcides Aug 7, 2023
78bebde
Removed old unification
alcides Aug 7, 2023
cbdbbc8
HM type inference working
alcides Aug 8, 2023
bdd2167
Moved wrapping
alcides Aug 8, 2023
261f697
Added toml package to dependencies because of yapf
alcides Aug 8, 2023
3956306
More polymorphism work
alcides Aug 8, 2023
06ef1a5
Working on debugging
alcides Aug 9, 2023
dd1054a
Merge branch 'master' of github.com:alcides/aeon into dependent_tuples
alcides Aug 10, 2023
4318c84
Merge branch 'master' of github.com:alcides/aeon into dependent_tuples
alcides Aug 10, 2023
105a9cb
Renaming repeated variables in constraint
alcides Aug 10, 2023
42004b8
Merged dependent tuples with polymorphism
alcides Aug 10, 2023
a0e5fd4
Tests failing
alcides Aug 10, 2023
f618a31
Brought forall backs for inhabitted
alcides Aug 10, 2023
2a8f212
Adapted tests to handle elaboration
alcides Aug 10, 2023
7ff87f2
Fixed prim_op with refined
alcides Aug 14, 2023
0f7fa5b
Allowed literals in horn applications
alcides Aug 15, 2023
761395d
Working on passing tests
alcides Aug 16, 2023
81ddfe4
work in progress
alcides Sep 5, 2023
d5fd0f6
Progress in identifying bug
alcides Sep 13, 2023
5fc7974
test_max passing
alcides Sep 13, 2023
49a9916
Bare Types and Kind checking in TApp
alcides Sep 15, 2023
74390fe
WIP
alcides Sep 20, 2023
c8e8691
Type Elaboration without errors
alcides Sep 21, 2023
f89c067
Merge branch 'master' into polymorphism
alcides Sep 21, 2023
a7815b7
Removed prints
alcides Sep 22, 2023
7c3ca64
Added TypeConstructor
alcides Sep 26, 2023
16194c2
Removed extra comment
alcides Sep 26, 2023
8062cd9
Bumped requirement to 3.10
alcides Sep 26, 2023
ff6617f
Made the AST of dataclasses
alcides Sep 26, 2023
3c4c244
TypeVar modeled as int
alcides Sep 26, 2023
e6b37ad
WIP
alcides Oct 12, 2023
96eaa43
All type arguments have positive polarities
alcides Oct 16, 2023
094f4ed
Refactored substitions
alcides Oct 16, 2023
61fba21
Compiling list
alcides Oct 16, 2023
7803e72
Fixed elaborate in main
alcides Oct 16, 2023
fb9a9f0
Improved List
alcides Oct 16, 2023
7ab9379
Fixed naming error
alcides Oct 17, 2023
d0196a3
Merge branch 'master' into polytypes
alcides Oct 17, 2023
5e5803a
WIP: type constructor syntax
alcides Oct 17, 2023
ba7d0a4
Added polarity handling
alcides Oct 17, 2023
ddb1a69
Merge branch 'master' into polytypes
alcides Oct 17, 2023
1b8e346
Fixed evaluator with polymorphic constructs
alcides Oct 31, 2023
8d34ac5
Different fresh strategy
alcides Nov 15, 2023
7cb0531
WIP
alcides Jun 29, 2023
8483c92
Renaming repeated variables in constraint
alcides Aug 10, 2023
5439bce
Added first polymorphic test
alcides Jul 13, 2023
070cade
Get Type Vars
alcides Jul 15, 2023
0b400c1
Added polymorphism-related elaboration
alcides Aug 7, 2023
cd09ec8
Allowed literals in horn applications
alcides Aug 15, 2023
92a4ec2
Bare Types and Kind checking in TApp
alcides Sep 15, 2023
f2d5d08
Type Elaboration without errors
alcides Sep 21, 2023
54b4e0e
logger message for constraints
eduardo-imadeira Sep 1, 2023
7a5ee2e
pre-commit run --all-files
eduardo-imadeira Sep 1, 2023
6eb6948
Removed prints
alcides Sep 22, 2023
c06d386
Updated pre-commit
alcides Nov 19, 2024
8ab9953
Fixed project config
alcides Nov 19, 2024
a2fe607
Merge branch 'master' into polymorphism
alcides Nov 20, 2024
41a175d
Working on merging polymorphism
alcides Nov 20, 2024
36da2a3
Added elaboration to all checks
alcides Nov 26, 2024
82f6e13
Updated pre-commit
alcides Nov 26, 2024
f5d2b24
Fixed elaboration with holes
alcides Nov 26, 2024
e72c42f
Fixed polymorphic context
alcides Nov 27, 2024
a071516
Integrated new synthesis with polymorphism
alcides Nov 27, 2024
b233a56
Reverted GeneticEngine
alcides Nov 27, 2024
3609dfc
Only First-order functions go to Constraint
alcides Nov 29, 2024
f32259e
Fixed missing spec in vector
alcides Nov 29, 2024
b2dc15d
Inserted typed let
alcides Nov 29, 2024
61c26aa
Fixed elaboration before synthesis
alcides Nov 29, 2024
c25e901
Removed float operators
alcides Nov 29, 2024
e0a66de
Only First-order functions are passed to SMT context
alcides Nov 30, 2024
07b3b3e
Added pre-commit
alcides Nov 30, 2024
5798705
Fixed core elaboration
alcides Nov 30, 2024
af5af3f
Added failing test
alcides Dec 1, 2024
ef89fe2
Merge branch 'polymorphism' into polytypes
alcides Dec 1, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Working on merging polymorphism
alcides committed Nov 20, 2024

Verified

This commit was signed with the committer’s verified signature.
anoek Akita Noek
commit 41a175db5b94e3964e978e38436f497b28e09978
1 change: 0 additions & 1 deletion aeon/backend/evaluator.py
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
from __future__ import annotations

from typing import Any
from loguru import logger

from aeon.core.terms import Abstraction, TypeAbstraction, TypeApplication
from aeon.core.terms import Annotation
66 changes: 50 additions & 16 deletions aeon/core/substitutions.py
Original file line number Diff line number Diff line change
@@ -8,7 +8,7 @@
from aeon.core.liquid import LiquidLiteralString
from aeon.core.liquid import LiquidTerm
from aeon.core.liquid import LiquidVar
from aeon.core.terms import Abstraction
from aeon.core.terms import Abstraction, TypeApplication
from aeon.core.terms import Annotation
from aeon.core.terms import Application
from aeon.core.terms import Hole
@@ -50,7 +50,11 @@ def rec(k: Type):
elif isinstance(t, RefinedType):
it = RefinedType(t.name, rec(t.type), t.refinement)
while isinstance(it.type, RefinedType):
nr = substitution_in_liquid(it.type.refinement, LiquidVar(t.name), it.type.name)
nr = substitution_in_liquid(
it.type.refinement,
LiquidVar(t.name),
it.type.name,
)
ncond = LiquidApp("&&", [t.refinement, nr])
it = RefinedType(t.name, it.type.type, ncond)
return it
@@ -94,25 +98,43 @@ def rec(x: Term):
assert False


def substitution_in_liquid(t: LiquidTerm, rep: LiquidTerm, name: str) -> LiquidTerm:
def substitution_in_liquid(
t: LiquidTerm,
rep: LiquidTerm,
name: str,
) -> LiquidTerm:
"""Substitutes name in the term t with the new replacement term rep."""
assert isinstance(rep, LiquidTerm)
if isinstance(t, (LiquidLiteralInt, LiquidLiteralBool, LiquidLiteralString, LiquidLiteralFloat)):
if isinstance(
t,
(
LiquidLiteralInt,
LiquidLiteralBool,
LiquidLiteralString,
LiquidLiteralFloat,
),
):
return t
elif isinstance(t, LiquidVar):
if t.name == name:
return rep
else:
return t
elif isinstance(t, LiquidApp):
return LiquidApp(t.fun, [substitution_in_liquid(a, rep, name) for a in t.args])
return LiquidApp(
t.fun,
[substitution_in_liquid(a, rep, name) for a in t.args],
)
elif isinstance(t, LiquidHornApplication):
if t.name == name:
return rep
else:
return LiquidHornApplication(
t.name,
[(substitution_in_liquid(a, rep, name), t) for (a, t) in t.argtypes],
[
(substitution_in_liquid(a, rep, name), t)
for (a, t) in t.argtypes
],
)
else:
assert False
@@ -218,23 +240,33 @@ def rec(x: Term):

def liquefy_app(app: Application) -> LiquidApp | None:
arg = liquefy(app.arg)
fun = app.fun
while isinstance(fun, TypeApplication):
fun = fun.body
if not arg:
return None
if isinstance(app.fun, Var):
return LiquidApp(app.fun.name, [arg])
elif isinstance(app.fun, Application):
liquid_pseudo_fun = liquefy_app(app.fun)
if isinstance(fun, Var):
return LiquidApp(fun.name, [arg])
elif isinstance(fun, Application):
liquid_pseudo_fun = liquefy_app(fun)
if liquid_pseudo_fun:
return LiquidApp(liquid_pseudo_fun.fun, liquid_pseudo_fun.args + [arg])
return LiquidApp(
liquid_pseudo_fun.fun,
liquid_pseudo_fun.args + [arg],
)
return None
elif isinstance(app.fun, Let):
elif isinstance(fun, Let):
return liquefy_app(
Application(
substitution(app.fun.body, app.fun.var_value, app.fun.var_name),
substitution(
fun.body,
fun.var_value,
fun.var_name,
),
app.arg,
),
)
assert False
), )
else:
raise Exception(f"{app} is not a valid predicate.")


def liquefy_rec(t: Rec) -> LiquidTerm | None:
@@ -282,6 +314,8 @@ def liquefy(rep: Term) -> LiquidTerm | None:
return LiquidLiteralString(rep.value)
elif isinstance(rep, Application):
return liquefy_app(rep)
elif isinstance(rep, TypeApplication):
return liquefy(rep.body)
elif isinstance(rep, Var):
return LiquidVar(rep.name)
elif isinstance(rep, Hole):
46 changes: 19 additions & 27 deletions aeon/core/types.py
Original file line number Diff line number Diff line change
@@ -7,7 +7,6 @@
from aeon.core.liquid import LiquidHole
from aeon.core.liquid import LiquidLiteralBool
from aeon.core.liquid import LiquidTerm
from aeon.core.liquid import liquid_free_vars


class Kind(ABC):
@@ -38,12 +37,10 @@ class Type(ABC):
pass


@dataclass
class BaseType(Type):
name: str

def __init__(self, name):
self.name = name

def __repr__(self):
return f"{self.name}"

@@ -54,12 +51,10 @@ def __hash__(self) -> int:
return hash(self.name)


@dataclass
class TypeVar(Type):
name: str

def __init__(self, name):
self.name = name

def __repr__(self):
return f"{self.name}"

@@ -110,16 +105,12 @@ def __hash__(self) -> int:
bottom = Bottom()


@dataclass
class AbstractionType(Type):
var_name: str
var_type: Type
type: Type

def __init__(self, var_name: str, var_type: Type, type: Type):
self.var_name = var_name
self.var_type = var_type
self.type = type

def __repr__(self):
return f"({self.var_name}:{self.var_type}) -> {self.type}"

@@ -135,25 +126,18 @@ def __hash__(self) -> int:
return hash(self.var_name) + hash(self.var_type) + hash(self.type)


@dataclass
class RefinedType(Type):
name: str
type: BaseType | TypeVar
refinement: LiquidTerm

def __init__(self, name: str, ty: BaseType | TypeVar, refinement: LiquidTerm):
self.name = name
self.type = ty
self.refinement = refinement
# Disabled because of unification var
# assert isinstance(ty, BaseType) or isinstance(ty, TypeVar) or isinstance(ty, UnificationVar)

def __repr__(self):
return f"{{ {self.name}:{self.type} | {self.refinement} }}"

def __eq__(self, other):
return (
isinstance(other, RefinedType)
and self.name == other.name
isinstance(other, RefinedType) and self.name == other.name
and self.type == other.type
and self.refinement == other.refinement
)
@@ -172,10 +156,11 @@ def __str__(self):
return f"forall {self.name}:{self.kind}, {self.body}"


def extract_parts(
t: Type,
) -> tuple[str, BaseType | TypeVar, LiquidTerm]:
assert isinstance(t, BaseType) or isinstance(t, RefinedType) or isinstance(t, TypeVar)
def extract_parts(t: Type) -> tuple[str, BaseType | TypeVar, LiquidTerm]:
assert isinstance(t, BaseType) or isinstance(t, RefinedType) or isinstance(
t,
TypeVar,
)
if isinstance(t, TypeVar):
return ("_", t_int, LiquidLiteralBool(True))
elif isinstance(t, RefinedType):
@@ -197,7 +182,10 @@ def is_bare(t: Type) -> bool:
elif isinstance(t, Bottom):
return True
elif isinstance(t, RefinedType):
return t.refinement == LiquidHole() or isinstance(t.refinement, LiquidHornApplication)
return t.refinement == LiquidHole() or isinstance(
t.refinement,
LiquidHornApplication,
)
elif isinstance(t, AbstractionType):
return is_bare(t.var_type) and is_bare(t.type)
elif isinstance(t, TypePolymorphism):
@@ -267,7 +255,11 @@ def refined_to_unrefined_type(ty: Type) -> Type:
if isinstance(ty, RefinedType):
return ty.type
if isinstance(ty, AbstractionType):
return AbstractionType(ty.var_name, refined_to_unrefined_type(ty.var_type), refined_to_unrefined_type(ty.type))
return AbstractionType(
ty.var_name,
refined_to_unrefined_type(ty.var_type),
refined_to_unrefined_type(ty.type),
)
return ty


3 changes: 3 additions & 0 deletions aeon/typechecking/context.py
Original file line number Diff line number Diff line change
@@ -111,6 +111,7 @@ def __hash__(self) -> int:
return hash(self.prev) + hash(self.name) + hash(self.type)


@dataclass(init=False)
class VariableBinder(TypingContext):
prev: TypingContext
name: str
@@ -147,7 +148,9 @@ def __hash__(self) -> int:
return hash(self.prev) + hash(self.name) + hash(self.type)


@dataclass(init=False)
class TypeBinder(TypingContext):
prev: TypingContext
type_name: str
type_kind: Kind

Loading