Pragma design

[ice1000]

How do we design pragmas? This is needed for the design of prelude.

[ice1000]

Quoted from internal discussion

一种是 Arend 那样的，写一坨能 parse 能 resolve 的代码，然后编译器读进去，把 concrete syntax、reference 啥的 build 好，然后把编译器里面写好的 reduction rule 放进去或者在 normalize 的算法里面特殊处理这些函数的 application

一种是 Agda/Rust 那样的，提供一种 pragma 一样的机制，在代码里面通过一些额外的注解（注解本身是编译器特殊处理的）来告诉编译器『please treat this code this way』，然后编译器来 treat them as you wish

因为如果我们设计了 prelude 那么 sigma 的那个三选一就可以选不要 builtin sigma 了，而是在 prelude 里面扔一个 record binary sigma

[ice1000]

The second question is how should it look like. I hate the Agda and GHC approach because pragma has their semantics, why are we reusing comment syntax!

I'm suggesting three ways (react with emoji to vote) -- 🚀 for Idrisy %pragma as definitions (or we can use alternatively \pragma), ❤️ for Rusty #[definition(modifiers)], 🎉 for Java style @pragma as modifiers

[ice1000]

Well, I think the vote is not good enough. Let me change it. Pragmas should be:

/	Definitions	Modifiers
Prefixed by a token	:rocket:	:tada:
Surrounded by pairs of tokens	:heart:	:smile:

[re-xyr]

I do not think pragmas always have semantics. For example, making some type N builtin Nat has no extra semantics because we get the same results in computations anyway. Am I wrong?

[ice1000]

You are. There are natural number literals, which corresponds to builtin natural types. I think we could automagically recognize the natural-like structures and turn them into primitive numbers at runtime.

[re-xyr]

But what about NATPLUS etc? It does not add any syntactic constructs.

[imkiva]

I am quite unsure if a pragma should be a modifier or a definition. I think it depends:

For something like {-# BUILTIN NATPLUS _+_ #-}, I think it should be a definition as it is a complete term. (independent of other definitions but related, just like other non-pragma definitions) For something like #[cfg(test)], I think it should be a modifier as it describes the thing that followed.

[ice1000]

I think it should be a definition as it is a complete term.

I think a better practice would be adding a modifier to _+_.

[ice1000]

No idea why Agda didn't do that 🤷🏼

[ice1000]

• :tada: @pragma(parameters)
• :eyes: #[inline(parameters)]
• :rocket: %inline parameters
• :smile: special comments

[re-xyr]

\inline(parameters)

[lunalunaa]

• :tada: @pragma(parameters)

• :eyes: #[inline(parameters)]

• :rocket: %inline parameters

• :smile: special comments

Breaking the tie

[ice1000]

• :tada: @pragma(parameters)

• :eyes: #[inline(parameters)]

• :rocket: %inline parameters

• :smile: special comments

Breaking the tie

Lmfao 🤣🤣🤣🤣