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
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.
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?
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
If I use
Elpi.API.RawData.Constants.declare_global_symbol, the result is a constant to be used with
App, not with
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").
const are global symbols, while
"nat_eqType" are OpauqeData (strings are opaque data).
Last updated: Feb 05 2023 at 14:02 UTC