G3Kappa / Ergo

Other
4 stars 0 forks source link

Load-time Expansions #36

Closed G3Kappa closed 1 year ago

G3Kappa commented 1 year ago

At the time of writing, expansions work fine but they do unnecessary work because they are called during the solving step. Expansions should only happen when the solver is initialized and when a query is parsed.

Right now the head of predicates is expanded correctly at initialization time, but the body isn't. This is because some macros, such as :=/1, replace themselves with the result of their computation.

Either the macro semantics are limited such that predicate expansion is no longer a problem, or some corner cases need to be addressed:

G3Kappa commented 1 year ago

See #37, closed now. This issue depended on it.

G3Kappa commented 1 year ago

Also, the head of predicates could be expanded better. Consider the following:

add(A, B, :=(A+B)).

Right now, this expansion would crash and burn because A and B are not known at solver initialization time. But it seems reasonable to apply the same kind of transformation that needs to happen inside the body of the expanded predicate to the head as well, if the head is a complex term.

The resulting predicate would look like this:

add(A, B, _Exp1) :- _Exp1 is A + B.