Janno (Feb 22 2022 at 16:07): Janno (Feb 22 2022 at 16:07):I am trying to understand RawData and I have two questions:
1) Why does RawData.App take 3 arguments?
2) What is the difference between constant and builtin?
Enrico Tassi (Feb 22 2022 at 16:41):Well, an application has a head symbol, at least one argument, an maybe some more (a list of them).
Internally constants and builtins are just integers for globally allocated names. But to avoid mistakes Builtin takes an integer flagged as builtin, while, say, App takes a constant as a head symbol.
Enrico Tassi (Feb 22 2022 at 16:46):Builtin used to take a regular constant, but the interpreter relies on the fact that regular constants and (constants) for builtin predicate are not mixed. So I did make the type different in the API in the very last release IIRC. Maybe the API lacks stuff you need because of that?
Janno (Feb 23 2022 at 09:24):Thanks for the explanations. I don't think the API is lacking. I was just confused by the two different notions of application and also the fact that you separate the first argument into its own argument of App.
If I use Elpi.API.RawData.Constants.declare_global_symbol, the result is a constant to be used with App, not with Builtin, right?
Enrico Tassi (Feb 23 2022 at 10:47):Yes. But note that these can only be allocated "before elpi runs", they are OK for your syntax tree and your (non built in) predicate. If you need a notion of name (like the coq-elpi data type gref) look into OpaqueData. I mean, in a rule like
is-eq-type (indt "nat") (const "nat_eqType").
is-eq-type and indt and const are global symbols, while "nat" and "nat_eqType" are OpauqeData (strings are opaque data).
Last updated: Oct 08 2024 at 14:01 UTC