Currently, a lot of code effort is required to add new theories to Liquid Fixpoint. It would be nicer if we could leverage most of the system to do this for us. This would remove clutter from having 50 names in the code base for the functions, as well as their accompanying types.
Proposed solution
Have a directive in Liquid Fixpoint syntax to bind a LF function to an underlying SMTLIB2 function. Something like the rust #[...]
Then just prepend a file containing all these definitions when solving a liquid fixpoint file (to avert having to do actual package managing). Of course the syntax of the annotation may be different, but this is also extendible without parser changes for other purposes.
Problem
Currently, a lot of code effort is required to add new theories to Liquid Fixpoint. It would be nicer if we could leverage most of the system to do this for us. This would remove clutter from having 50 names in the code base for the functions, as well as their accompanying types.
Proposed solution
Have a directive in Liquid Fixpoint syntax to bind a LF function to an underlying SMTLIB2 function. Something like the rust #[...]
Then just prepend a file containing all these definitions when solving a liquid fixpoint file (to avert having to do actual package managing). Of course the syntax of the annotation may be different, but this is also extendible without parser changes for other purposes.