Merge pull request #20 from alcides/grammar_filter

Filter the relevant functions to use in Synthesis.

.git-blame-ignore-revs

@@ -0,0 +1 @@
+3afc4a6373239c357df30b3b91c23bf0c8362107

.github/workflows/python-app.yml

@@ -30,9 +30,9 @@ jobs:
           python -m pip install --upgrade uv
           uv pip install flake8 pytest mypy pre-commit
           if [ -f requirements.pip ]; then uv pip install -r requirements.pip; fi
-      #- name: Lint with pre-commit
-      #  run: |
-      #    pre-commit run --all-files
+      - name: Lint with pre-commit
+        run: |
+          pre-commit run --all-files
       - name: Lint with mypy
         run: |
           mypy aeon --no-strict-optional --ignore-missing-imports

aeon/__main__.py

@@ -3,10 +3,9 @@
 import argparse
 import sys
 
-from aeon.backend.evaluator import eval
 from aeon.backend.evaluator import EvaluationContext
+from aeon.backend.evaluator import eval
 from aeon.core.types import top
-from aeon.decorators import apply_decorators
 from aeon.frontend.anf_converter import ensure_anf
 from aeon.frontend.parser import parse_term
 from aeon.logger.logger import export_log
@@ -17,25 +16,30 @@
 from aeon.sugar.parser import parse_program
 from aeon.sugar.program import Program
 from aeon.synthesis_grammar.identification import incomplete_functions_and_holes
-from aeon.synthesis_grammar.synthesizer import synthesize
+from aeon.synthesis_grammar.synthesizer import synthesize, parse_config
 from aeon.typechecking.typeinfer import check_type_errors
 from aeon.utils.ctx_helpers import build_context
 
 
 def parse_arguments():
     parser = argparse.ArgumentParser()
-    parser.add_argument("filename",
-                        help="name of the aeon files to be synthesized")
-    parser.add_argument("--core",
-                        action="store_true",
-                        help="synthesize a aeon core file")
+    parser.add_argument(
+        "filename",
+        help="name of the aeon files to be synthesized",
+    )
+    parser.add_argument(
+        "--core",
+        action="store_true",
+        help="synthesize a aeon core file",
+    )
     parser.add_argument(
         "-l",
         "--log",
         nargs="+",
         default="",
-        help="set log level: \nTRACE \nDEBUG \nINFO \nTYPECHECKER \nCONSTRAINT "
-        "\nWARNINGS \nERROR \nCRITICAL",
+        help=
+        """set log level: \nTRACE \nDEBUG \nINFO \nWARNINGS \nTYPECHECKER \nSYNTH_TYPE \nCONSTRAINT \nSYNTHESIZER
+                \nERROR \nCRITICAL""",
     )
     parser.add_argument("-f",
                         "--logfile",
@@ -47,6 +51,14 @@ def parse_arguments():
                         action="store_true",
                         help="export synthesis csv 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(
         "-d",
         "--debug",
@@ -61,16 +73,6 @@ def read_file(filename: str) -> str:
         return file.read()
 
 
-def apply_decorators_in_program(p: Program) -> Program:
-    """We apply the decorators meta-programming code to each definition in the program."""
-    new_definitions = []
-    for definition in p.definitions:
-        new_def, other_defs = apply_decorators(definition)
-        new_definitions.append(new_def)
-        new_definitions.extend(other_defs)
-    return Program(p.imports, p.type_decls, new_definitions)
-
-
 def log_type_errors(errors: list[Exception | str]):
     logger.log("TYPECHECKER", "-------------------------------")
     logger.log("TYPECHECKER", "+     Type Checking Error     +")
@@ -95,7 +97,6 @@ def log_type_errors(errors: list[Exception | str]):
         core_ast = parse_term(aeon_code)
     else:
         prog: Program = parse_program(aeon_code)
-        prog = apply_decorators_in_program(prog)
         (
             core_ast,
             typing_ctx,
@@ -114,12 +115,21 @@ def log_type_errors(errors: list[Exception | str]):
         list[str]]] = incomplete_functions_and_holes(typing_ctx, core_ast_anf)
 
     if incomplete_functions:
-        file_name = args.filename if args.csv_synth else None
+        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)
 
-        synthesis_result = synthesize(typing_ctx, evaluation_ctx, core_ast_anf,
-                                      incomplete_functions)
-
-        print(f"Best solution: {synthesis_result}")
+        synthesis_result = synthesize(
+            typing_ctx,
+            evaluation_ctx,
+            core_ast_anf,
+            incomplete_functions,
+            filename,
+            synth_config,
+        )
+        print(f"Best solution:{synthesis_result}")
+        # print()
+        # pretty_print_term(ensure_anf(synthesis_result, 200))
         sys.exit(1)
 
     eval(core_ast, evaluation_ctx)

aeon/bindings/binding_utils.py

@@ -1,7 +1,6 @@
 from __future__ import annotations
 
 
-
 def curried(x, argc=None):
     if argc is None:
         argc = x.__code__.co_argcount

aeon/core/pprint.py

@@ -1,12 +1,46 @@
 from __future__ import annotations
 
 from aeon.core.liquid import LiquidLiteralBool
+from aeon.core.terms import (
+    Abstraction,
+    Annotation,
+    Application,
+    Hole,
+    If,
+    Let,
+    Literal,
+    Rec,
+    Term,
+    TypeAbstraction,
+    TypeApplication,
+    Var,
+)
 from aeon.core.types import AbstractionType
 from aeon.core.types import BaseType
 from aeon.core.types import RefinedType
 from aeon.core.types import Type
-from aeon.core.types import type_free_term_vars
 from aeon.core.types import TypeVar
+from aeon.core.types import type_free_term_vars
+from aeon.synthesis_grammar.grammar import aeon_prelude_ops_to_text
+
+ops_to_abstraction: dict[str, str] = {
+    "%": "Int) -> Int",
+    "/": "Int) -> Int",
+    "*": "Int) -> Int",
+    "-": "Int) -> Int",
+    "+": "Int) -> Int",
+    "%.": "Float) -> Float",
+    "/.": "Float) -> Float",
+    "*.": "Float) -> Float",
+    "-.": "Float) -> Float",
+    "+.": "Float) -> Float",
+    ">=": "Int) -> Bool",
+    ">": "Int) -> Bool",
+    "<=": "Int) -> Bool",
+    "<": "Int) -> Bool",
+    "!=": "Int) -> Bool",
+    "==": "Int) -> Bool",
+}
 
 
 def pretty_print(t: Type) -> str:
@@ -18,13 +52,79 @@ def pretty_print(t: Type) -> str:
         at = pretty_print(t.var_type)
         rt = pretty_print(t.type)
         if t.var_name in type_free_term_vars(t.var_type):
-            return f"({t.var_name}:{at}) -> {rt}"
+            return f"""(
+                {t.var_name}:{at}) -> {rt}"""
         else:
-            return f"{at} -> {rt}"
+            return f"""{at} -> {rt}"""
     elif isinstance(t, RefinedType):
         it = pretty_print(t.type)
         if t.refinement == LiquidLiteralBool(True):
             return it
         else:
             return f"{{{t.name}:{it} | {t.refinement}}}"
-    assert False
+    raise ValueError(f"Unknown type {t}")
+
+
+def pretty_print_term(term: Term):
+    term_str: str = custom_preludes_ops_representation(term)[0]
+    print(term_str)
+
+
+def custom_preludes_ops_representation(term: Term, counter: int = 0) -> tuple[str, int]:
+    prelude_operations: dict[str, str] = aeon_prelude_ops_to_text
+    match term:
+        case Application(fun=Var(name=var_name), arg=arg) if var_name in prelude_operations.keys():
+            op = var_name
+            arg_str, counter = custom_preludes_ops_representation(arg, counter)
+            counter += 1
+            new_var_name = f"__{prelude_operations[op]}_{counter}__"
+            abstraction_type_str = f"({new_var_name}:{ops_to_abstraction[op]}"
+            personalized_op = f": {abstraction_type_str} = (\\{new_var_name} -> {arg_str} {op} {new_var_name})"
+            return personalized_op, counter
+
+        case Application(fun=fun, arg=arg):
+            fun_str, counter = custom_preludes_ops_representation(fun, counter)
+            arg_str, counter = custom_preludes_ops_representation(arg, counter)
+            return (
+                f"""= ({fun_str} {arg_str}
+            )""",
+                counter,
+            )
+
+        case Annotation(expr=expr, type=type):
+            expr_str, counter = custom_preludes_ops_representation(expr, counter)
+            return f"""({expr_str} : {type})""", counter
+
+        case Abstraction(var_name=var_name, body=body):
+            body_str, counter = custom_preludes_ops_representation(body, counter)
+            return f"""(\\{var_name} -> {body_str})""", counter
+
+        case Let(var_name=var_name, var_value=var_value, body=body):
+            var_value_prefix = "= " if not isinstance(var_value, Application) else ""
+            var_value_str, counter = custom_preludes_ops_representation(var_value, counter)
+            body_str, counter = custom_preludes_ops_representation(body, counter)
+            return f"""(let {var_name} {var_value_prefix}{var_value_str} in\n {body_str})""", counter
+
+        case Rec(var_name=var_name, var_type=var_type, var_value=var_value, body=body):
+            var_value_str, counter = custom_preludes_ops_representation(var_value, counter)
+            body_str, counter = custom_preludes_ops_representation(body, counter)
+            return f"""(let {var_name} : {var_type} = {var_value_str} in\n {body_str})""", counter
+
+        case If(cond=cond, then=then, otherwise=otherwise):
+            cond_str, counter = custom_preludes_ops_representation(cond, counter)
+            then_str, counter = custom_preludes_ops_representation(then, counter)
+            otherwise_str, counter = custom_preludes_ops_representation(otherwise, counter)
+            return f"""(if {cond_str} then {then_str} else {otherwise_str})""", counter
+
+        case TypeAbstraction(name=name, kind=kind, body=body):
+            body_str, counter = custom_preludes_ops_representation(body, counter)
+            return f"""ƛ{name}:{kind}.({body_str})""", counter
+
+        case TypeApplication(body=body, type=type):
+            body_str, counter = custom_preludes_ops_representation(body, counter)
+            return f"""({body_str})[{type}]""", counter
+
+        case Literal(_, _) | Var(_) | Hole(_):
+            return str(term), counter
+
+    return str(term), counter

aeon/core/substitutions.py

@@ -32,6 +32,7 @@
 
 
 def substitute_vartype(t: Type, rep: Type, name: str):
+
     def rec(k: Type):
         return substitute_vartype(k, rep, name)
 
@@ -54,6 +55,7 @@ def rec(k: Type):
 
 
 def substitute_vartype_in_term(t: Term, rep: Type, name: str):
+
     def rec(x: Term):
         return substitute_vartype_in_term(x, rep, name)
 
@@ -87,25 +89,29 @@ 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))
@@ -164,6 +170,7 @@ def rec(t: Type) -> Type:
 
 
 def substitution(t: Term, rep: Term, name: str) -> Term:
+
     def rec(x: Term):
         return substitution(x, rep, name)
 
@@ -216,15 +223,16 @@ 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