creusot icon indicating copy to clipboard operation
creusot copied to clipboard

Published 20 hours ago • verified publisher icon creusot-rs

Support macro invocations in pearlite terms.

Open xldenis opened this issue 3 years ago • 1 comments

We should allow calls to macros in pearlite terms. Currently this is an error in pearlite_syn.

xldenis avatar Oct 08 '21 08:10 xldenis

I tried adding this as part of #274, but unfortunately it requires using apis which are not public in syn, much to my chagrin.

xldenis avatar Feb 08 '22 22:02 xldenis

We've settled on only allowing whitelisted macros for now (proof_assert).

xldenis avatar Sep 28 '23 09:09 xldenis

The problem being that arbitrary macros could allow writing non-pearlite code in pearlite context.

jhjourdan avatar Sep 28 '23 09:09 jhjourdan

The problem being that arbitrary macros could allow writing non-pearlite code in pearlite context.

I don't really consider this a problem we need to defend against. They wouldn't be able to do anything unsound, as the "real" parser happens later on in the compilation anyways.

xldenis avatar Sep 28 '23 09:09 xldenis