# Synthesising Python Code with Generated Domains

### Step 1: Write functions in Python

@log_function_call
def cons(a: int, l: list[int]) -> list[int]:
    return [a, *l]

The decorator generates necessary typing information for the generated domain. Define your functions, tag them with the decorator and write example code that uses these functions.

@log_test
def test_1():
    return cons(0, cons(1, cons(2, cons(3, cons(4, cons(5, []))))))

# Trigger the complex operation to see nested logging
result = test_1()

Generated JSON:

{
    "name": "PyDomain",
    "functions": [
        {
            "name": "cons",
            "inputs": [
                {
                    "name": "arg1",
                    "tp": "int"
                },
                {
                    "name": "arg2",
                    "tp": "list"
                }
            ],
            "output": "list",
            "body": "def cons(a: int, l: list[int]) -> list[int]:\n    return [a, *l]"
        }
    ],
    "tests": [
        [
            {
                "name": "test_1",
                "args": [],
                "expr": "(cons 0 (cons 1 (cons 2 (cons 3 (cons 4 (cons 5))))))",
                "expected": "[0, 1, 2, 3, 4, 5]"
            }
        ]
    ]
}

## Step 2

Make the domain. Create a new module in `lambdas/domains/` and copy the resulting JSON inside the `make_domain` macro. This will generate all the necessary code to define your own domain. This lets you customize the behaviour of your domain. Inside the macro, you just need to specify the functions that you will get called for each of these tasks.

use domaingen::make_domain;

make_domain!({
    "name": "PyDomain",
    "functions": [
        {
            "name": "cons",
            "inputs": [
                {
                    "name": "arg1",
                    "tp": "int"
                },
                {
                    "name": "arg2",
                    "tp": "list"
                }
            ],
            "output": "list",
            "body": "def cons(a: int, l: list[int]) -> list[int]:\n    return [a, *l]"
        }
    ],
    "consts": [
    ],
    "tests": [
        {
            "name": "test_1",
            "args": [],
            "expr": "(eval (cons 0 (cons 1 (cons 2 (cons 3 (cons 4 (cons 5 [])))))))",
            "expected": "[0, 1, 2, 3, 4, 5]"
        }
    ],
    "check_match": "eval_check_match",
    "eval_fn": "eval",
    "val_of_prim": "val_of_prim_fallback"
});

Constant values (or literals if you will) needed for synthesis can be specified inside the `consts` field.

make_domain!({
    ....
    "consts": [
        {
            "name": "1",
            "tp": "int",
            "value": "1"
        },
        {
            "name": "2",
            "tp": "int",
            "value": "2"
        }
    ],
....
});

For flexibility, the functions for parsing values (`val_of_prim`), evaluating expressions (`eval_fn`) and matching results (`check_match`) need to be defined outside the macro. You can now define these functions in the same file.

fn eval_check_match(sym1: &crate::Val<PyDomain>, sym2: &crate::Val<PyDomain>) -> bool {
    if let (Dom(s1), Dom(s2)) = (sym1, sym2) {
        s1.to_string() == s2.to_string()
    } else {
        false
    }
}

fn val_of_prim_fallback(p: &string_cache::DefaultAtom) -> Option<crate::Val<PyDomain>> {
    // ommited for brevity
    todo!()
}

fn eval(mut args: Env, handle: &Evaluator) -> VResult {
    load_args!(args, expr: Val);

    let expr = expr.dom()?.to_string();

    let function_defs = &handle.data.borrow().function_defs;

    let mut code = function_defs.join("\n\n");

    code.push_str("\n\n");

    code.push_str(&format!("result = {}", &expr));

    ok(INTERPRETER
        .eval(&code)
        .map_err(|e| e.to_string())
        .map(|res| Int(res))?)
}

## Step 3: Synthesis!
Now, we have a domain ready for synthesis. Define your test cases in a JSON file. Here, we are synthesising against these test cases:

[
    {
        "name": "cons test 1",
        "tp": "list -> any",
        "ios": [
            [
                [
                    "[]"
                ],
                "[1]"
            ],
            [
                [
                    "[5,6]"
                ],
                "[1, 5, 6]"
            ]
        ]
    },
    {
        "name": "cons test 2",
        "tp": "list -> any",
        "ios": [
            [
                [
                    "[4]"
                ],
                "[1, 2, 4]"
            ],
            [
                [
                    "[5,6]"
                ],
                "[1, 2, 5, 6]"
            ]
        ]
    }
]

Time to test synthesis:

$ cargo run --release --bin cli top ./synth/data/code/code.json  --domain py-code --timeout=100 --min-ll=-60.0 --max-ll=0.0 --threads 8

Output:

cons test 1: [5 solns] [ll=-4.564] @ 0.055s (fix1 #0 (lam (lam (eval (eval (cons 1 $0))))))
cons test 2: [5 solns] [ll=-5.951] @ 0.061s (fix1 #0 (lam (lam (eval (eval (cons 1 (cons 2 $0)))))))

The generated Python code for these will look something like this:

# (fix1 #0 (lam (lam (eval (cons 1 $0)))))

def cons(a: int, l: list[int]) -> list[int]:
    return [a, *l]
    
result = cons(1, [5, 6])

# (fix1 #0 (lam (lam (eval (cons 1 $0)))))

def cons(a: int, l: list[int]) -> list[int]:
    return [a, *l]
    
result = cons(1, cons(2, [5, 6]))