WIP

aeon/__main__.py

@@ -6,7 +6,6 @@
 from aeon.backend.evaluator import EvaluationContext
 from aeon.backend.evaluator import eval
 from aeon.core.types import top
-from aeon.frontend.anf_converter import ensure_anf
 from aeon.frontend.parser import parse_term
 from aeon.logger.logger import export_log
 from aeon.logger.logger import setup_logger
@@ -37,27 +36,16 @@ def parse_arguments():
         "--log",
         nargs="+",
         default="",
-        help=
-        """set log level: \nTRACE \nDEBUG \nINFO \nWARNINGS \nTYPECHECKER \nSYNTH_TYPE \nCONSTRAINT \nSYNTHESIZER
+        help="""set log level: \nTRACE \nDEBUG \nINFO \nWARNINGS \nTYPECHECKER \nSYNTH_TYPE \nCONSTRAINT \nSYNTHESIZER
                 \nERROR \nCRITICAL""",
     )
-    parser.add_argument("-f",
-                        "--logfile",
-                        action="store_true",
-                        help="export log file")
+    parser.add_argument("-f", "--logfile", action="store_true", help="export log file")
 
-    parser.add_argument("-csv",
-                        "--csv-synth",
-                        action="store_true",
-                        help="export synthesis csv file")
+    parser.add_argument("-csv", "--csv-synth", action="store_true", help="export synthesis csv file")
 
-    parser.add_argument("-gp",
-                        "--gp-config",
-                        help="path to the GP configuration file")
+    parser.add_argument("-gp", "--gp-config", help="path to the GP configuration file")
 
-    parser.add_argument("-csec",
-                        "--config-section",
-                        help="section name in the GP configuration file")
+    parser.add_argument("-csec", "--config-section", help="section name in the GP configuration file")
 
     parser.add_argument(
         "-d",
@@ -73,7 +61,7 @@ def read_file(filename: str) -> str:
         return file.read()
 
 
-def log_type_errors(errors: list[Exception | str]):
+def log_type_errors(errors: list[Exception]):
     logger.log("TYPECHECKER", "-------------------------------")
     logger.log("TYPECHECKER", "+     Type Checking Error     +")
     for error in errors:
@@ -104,32 +92,30 @@ def log_type_errors(errors: list[Exception | str]):
         ) = desugar(prog)
     logger.info(core_ast)
 
-    core_ast_anf = ensure_anf(core_ast)
-    type_errors = check_type_errors(typing_ctx, core_ast_anf, top)
+    type_errors = check_type_errors(typing_ctx, core_ast, top)
     if type_errors:
         log_type_errors(type_errors)
         sys.exit(1)
 
-    incomplete_functions: list[tuple[
-        str,
-        list[str]]] = incomplete_functions_and_holes(typing_ctx, core_ast_anf)
+    incomplete_functions: list[tuple[str, list[str]]] = incomplete_functions_and_holes(typing_ctx, core_ast)
 
     if incomplete_functions:
         filename = args.filename if args.csv_synth else None
-        synth_config = (parse_config(args.gp_config, args.config_section)
-                        if args.gp_config and args.config_section else None)
+        synth_config = (
+            parse_config(args.gp_config, args.config_section) if args.gp_config and args.config_section else None
+        )
 
         synthesis_result = synthesize(
             typing_ctx,
             evaluation_ctx,
-            core_ast_anf,
+            core_ast,
             incomplete_functions,
             filename,
             synth_config,
         )
         print(f"Best solution:{synthesis_result}")
         # print()
-        # pretty_print_term(ensure_anf(synthesis_result, 200))
+        # pretty_print_term(synthesis_result, 200)
         sys.exit(1)
 
     eval(core_ast, evaluation_ctx)

aeon/core/instantiation.py

@@ -3,7 +3,7 @@
 from aeon.core.liquid import LiquidVar
 from aeon.core.liquid_ops import mk_liquid_and
 from aeon.core.substitutions import substitution_in_liquid
-from aeon.core.types import AbstractionType
+from aeon.core.types import AbstractionType, ExistentialType
 from aeon.core.types import BaseType
 from aeon.core.types import RefinedType
 from aeon.core.types import Type
@@ -42,6 +42,15 @@ def rec(x):
             target.kind,
             type_substitution(target.body, alpha, beta),
         )
+    elif isinstance(t, ExistentialType):
+        new_name = t.var_name
+        new_type = t.type
+        while new_name == alpha:
+            old_name = new_name
+            new_name = new_name + "_fresh"
+            new_type = type_substitution(new_type, old_name, TypeVar(new_name))
+
+        return ExistentialType(new_name, t.var_type, new_type)
     else:
         assert False
 

aeon/core/substitutions.py

@@ -18,7 +18,7 @@
 from aeon.core.terms import Rec
 from aeon.core.terms import Term
 from aeon.core.terms import Var
-from aeon.core.types import AbstractionType
+from aeon.core.types import AbstractionType, ExistentialType
 from aeon.core.types import BaseType
 from aeon.core.types import Bottom
 from aeon.core.types import RefinedType
@@ -89,29 +89,25 @@ 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, LiquidHole):
         if t.name == name:
             return rep
         else:
             return LiquidHole(
                 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:
         print(t, type(t))
@@ -166,6 +162,14 @@ def rec(t: Type) -> Type:
                 t.type,
                 substitution_in_liquid(t.refinement, replacement, name),
             )
+    elif isinstance(t, ExistentialType):
+        if name == t.var_name:
+            new_name = t.var_name + "_"  # TODO: Fresh name
+            nt = ExistentialType(new_name, t.var_type, substitution_in_type(t.type, Var(new_name), t.var_name))
+        else:
+            nt = t
+        return ExistentialType(nt.var_name, nt.var_type, substitution_in_type(nt.type, rep, name))
+
     assert False
 
 
@@ -223,16 +227,15 @@ def liquefy_app(app: Application) -> LiquidApp | None:
     elif isinstance(app.fun, Application):
         liquid_pseudo_fun = liquefy_app(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):
         return liquefy_app(
             Application(
-                substitution(app.fun.body, app.fun.var_value,
-                             app.fun.var_name),
+                substitution(app.fun.body, app.fun.var_value, app.fun.var_name),
                 app.arg,
-            ), )
+            ),
+        )
     assert False
 
 

aeon/core/types.py

@@ -129,16 +129,12 @@ 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
+    type: BaseType | TypeVar | Bottom | Top
     refinement: LiquidTerm
 
-    def __init__(self, name: str, ty: BaseType | TypeVar, refinement: LiquidTerm):
-        self.name = name
-        self.type = ty
-        self.refinement = refinement
-
     def __repr__(self):
         return f"{{ {self.name}:{self.type} | {self.refinement} }}"
 
@@ -154,6 +150,16 @@ def __hash__(self) -> int:
         return hash(self.name) + hash(self.type) + hash(self.refinement)
 
 
+@dataclass
+class ExistentialType(Type):
+    var_name: str
+    var_type: Type
+    type: Type
+
+    def __str__(self) -> str:
+        return f"∃{self.var_name}:{self.var_type}, {self.type}"
+
+
 @dataclass
 class TypePolymorphism(Type):
     name: str  # alpha
@@ -163,7 +169,7 @@ class TypePolymorphism(Type):
 
 def extract_parts(
     t: Type,
-) -> tuple[str, BaseType | TypeVar, LiquidTerm]:
+) -> tuple[str, BaseType | TypeVar | Top | Bottom, LiquidTerm]:
     assert isinstance(t, BaseType) or isinstance(t, RefinedType) or isinstance(t, TypeVar)
     if isinstance(t, RefinedType):
         return (t.name, t.type, t.refinement)

aeon/synthesis_grammar/synthesizer.py

@@ -15,7 +15,7 @@
 from aeon.core.types import BaseType, Top
 from aeon.core.types import Type
 from aeon.core.types import top
-from aeon.frontend.anf_converter import ensure_anf
+
 from aeon.synthesis_grammar.grammar import (
     gen_grammar_nodes,
     get_grammar_node,
@@ -158,7 +158,6 @@ def evaluate_individual(individual: classType, result_queue: mp.Queue) -> Any:
         try:
             first_hole_name = holes[0]
             individual_term = individual.get_core()  # type: ignore
-            individual_term = ensure_anf(individual_term, 10000000)
             new_program = substitution(program_template, individual_term, first_hole_name)
             check_type_errors(ctx, new_program, Top())
             result = eval(new_program, ectx)