Gbury / dolmen

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction
BSD 2-Clause "Simplified" License
80 stars 17 forks source link

feat: Add support for user-defined builtins with Dune plugins #214

Open bclement-ocp opened 6 months ago

bclement-ocp commented 6 months ago

This patch adds support for model extensions in Dolmen_loop using a similar mechanism to typing extensions.

Model extensions and typing extensions are now loaded by the binary through Dune's plugin mechanism, and the existing bvconv extension is moved to use the plugin mechanism.

Fixes #203

bclement-ocp commented 6 months ago

the existing bvconv extension is moved to use the plugin mechanism

In retrospect, I am not 100% sure this is a good idea. I did this initially to have an example of usage of the plugin mechanism, but ended up writing two example plugins (abs_real, abs_real_split) which I think is better for that purpose since. I am open to reverting this part of the change.

bclement-ocp commented 6 months ago

the existing bvconv extension is moved to use the plugin mechanism

This was causing build failures on the CI so no longer part of the PR. Instead there is support for builtin extensions when loading them at the CLI level.

bclement-ocp commented 6 months ago

I did some late cleanup but this should be ready to review @Gbury

bclement-ocp commented 4 months ago

Made the requested changes + some others following (old) offline discussions:

bclement-ocp commented 4 months ago

@Gbury ping