Parametric refinements

aeon/__main__.py

@@ -47,7 +47,7 @@ def _parse_common_arguments(parser: ArgumentParser):
         "--log",
         nargs="+",
         default="",
-        help="""set log level: \nTRACE \nDEBUG \nINFO \nWARNINGS \nCONSTRAINT \nTYPECHECKER \nSYNTH_TYPE \nCONSTRAINT \nSYNTHESIZER
+        help="""set log level: \nTRACE \nDEBUG \nINFO \nWARNINGS \nCONSTRAINT \nTYPECHECKER \nSYNTH_TYPE \nCONSTRAINT \nSYNTHESIZER \nAST_INFO
                         \nERROR \nCRITICAL\n TIME""",
     )
     parser.add_argument(

aeon/core/bind.py

@@ -19,6 +19,7 @@
     Term,
     TypeAbstraction,
     TypeApplication,
+    RefinementApplication,
     Var,
     Literal,
 )
@@ -30,6 +31,7 @@
     Type,
     TypeConstructor,
     TypePolymorphism,
+    RefinimentPolymorphism,
     TypeVar,
 )
 from aeon.typechecking.context import (
@@ -132,6 +134,9 @@ def bind_type(ty: Type, subs: RenamingSubstitions) -> Type:
         case TypePolymorphism(name, kind, body):
             name, subs = check_name(name, subs)
             return TypePolymorphism(name, kind, bind_type(body, subs))
+        case RefinimentPolymorphism(name, kind, body):
+            name, subs = check_name(name, subs)
+            return RefinimentPolymorphism(name, kind, bind_type(body, subs))
         case _:
             assert False, f"Unique not supported for {ty} ({type(ty)})"
 
@@ -155,6 +160,8 @@ def bind_term(t: Term, subs: RenamingSubstitions) -> Term:
             return Abstraction(name, nbody)
         case TypeApplication(body, ty):
             return TypeApplication(bind_term(body, subs), bind_type(ty, subs))
+        case RefinementApplication(body, refinement):
+            return RefinementApplication(bind_term(body, subs), bind_type(refinement, subs))
         case TypeAbstraction(name, kind, body):
             name, subs = check_name(name, subs)
             return TypeAbstraction(name, kind, bind_term(body, subs))

aeon/core/substitutions.py

@@ -1,14 +1,14 @@
 from __future__ import annotations
 
 from aeon.core.liquid import LiquidApp
-from aeon.core.types import LiquidHornApplication, TypeConstructor, TypePolymorphism
+from aeon.core.types import LiquidHornApplication, TypeConstructor, TypePolymorphism, RefinimentPolymorphism
 from aeon.core.liquid import LiquidLiteralBool
 from aeon.core.liquid import LiquidLiteralFloat
 from aeon.core.liquid import LiquidLiteralInt
 from aeon.core.liquid import LiquidLiteralString
 from aeon.core.liquid import LiquidTerm
 from aeon.core.liquid import LiquidVar
-from aeon.core.terms import Abstraction, TypeAbstraction, TypeApplication
+from aeon.core.terms import Abstraction, TypeAbstraction, TypeApplication, RefinementApplication
 from aeon.core.terms import Annotation
 from aeon.core.terms import Application
 from aeon.core.terms import Hole
@@ -48,6 +48,11 @@ def rec(k: Type):
                 return t
             else:
                 return TypePolymorphism(pname, kind, rec(body))
+        case RefinimentPolymorphism(pname, kind, body):
+            if name == pname:
+                return t
+            else:
+                return RefinimentPolymorphism(pname, kind, rec(body))
         case TypeConstructor(cname, args):
             return TypeConstructor(cname, [rec(arg) for arg in args])
         case _:
@@ -144,6 +149,8 @@ def rec(t: Type) -> Type:
                 )
         case TypePolymorphism(name, kind, body):
             return TypePolymorphism(name, kind, rec(body))
+        case RefinimentPolymorphism(name, kind, body):
+            return RefinimentPolymorphism(name, kind, rec(body))
         case TypeConstructor(name, args):
             return TypeConstructor(name, [rec(arg) for arg in args])
         case _:
@@ -178,6 +185,8 @@ def rec(t: Type) -> Type:
                 )
         case TypePolymorphism(name, kind, body):
             return TypePolymorphism(name, kind, rec(body))
+        case RefinimentPolymorphism(name, kind, body):
+            return RefinimentPolymorphism(name, kind, rec(body))
         case TypeConstructor(name, args):
             return TypeConstructor(name, [rec(arg) for arg in args])
         case _:
@@ -227,6 +236,8 @@ def rec(x: Term):
             return If(rec(cond), rec(then), rec(otherwise))
         case TypeApplication(expr, ty):
             return TypeApplication(rec(expr), ty)
+        case RefinementApplication(body, refinement):
+            return RefinementApplication(rec(body), refinement)
         case TypeAbstraction(pname, kind, body):
             return TypeAbstraction(pname, kind, rec(body))
         case _:
@@ -254,6 +265,8 @@ def inline_lets(t: Term) -> Term:
             return inline_lets(substitute_vartype_in_term(body, ty, name))
         case TypeApplication(expr, ty):
             return TypeApplication(inline_lets(expr), ty)
+        case RefinementApplication(body, refinement):
+            return RefinementApplication(inline_lets(body), refinement)
         case _:
             return t
 
@@ -263,6 +276,8 @@ def uncurry(t: Term, args: list[LiquidTerm]) -> LiquidTerm | None:
     match t:
         case TypeApplication(body, _):
             return uncurry(body, args)
+        case RefinementApplication(body, _):
+            return uncurry(body, args)
         case Application(fun, arg):
             liquid_arg = liquefy(arg)
             if liquid_arg is None:

aeon/core/terms.py

@@ -192,7 +192,7 @@ class TypeAbstraction(Term):
     loc: Location = field(default_factory=lambda: SynthesizedLocation("default"))
 
     def __str__(self):
-        return f"ƛ{self.name}:{self.kind}.({self.body.pretty()})"
+        return f"ƛ{self.name}:{self.kind}.({self.body})"
 
 
 @dataclass(frozen=True)
@@ -203,3 +203,13 @@ class TypeApplication(Term):
 
     def __str__(self):
         return f"({self.body})[{self.type}]"
+
+
+@dataclass(frozen=True)
+class RefinementApplication(Term):
+    body: Term
+    refinement: Type
+    loc: Location = field(default_factory=lambda: SynthesizedLocation("default"))
+
+    def __str__(self):
+        return f"{{ {self.body} }}[{self.refinement}]"

aeon/core/types.py

@@ -134,6 +134,20 @@ def __hash__(self) -> int:
         return hash(self.name) + hash(self.kind) + hash(self.body)
 
 
+@dataclass
+class RefinimentPolymorphism(Type):
+    name: Name  # ro
+    type: Type
+    body: Type
+    loc: Location = field(default_factory=lambda: SynthesizedLocation("default"))
+
+    def __str__(self):
+        return f"forallR {self.name}:{self.type}, {self.body}"
+
+    def __hash__(self) -> int:
+        return hash(self.name) + hash(self.type) + hash(self.body)
+
+
 @dataclass
 class TypeConstructor(Type):
     name: Name