c3lang / c3c

Compiler for the C3 language
https://c3-lang.org
GNU Lesser General Public License v3.0
3.01k stars 184 forks source link

New doc comments don't work properly with contracts #1618

Closed vssukharev closed 1 week ago

vssukharev commented 1 week ago

Let we have such macro:

<* 
 * @require types::isNumeric($typeof(a)) && types::isNumeric($typeof(b)) "123123" 
 *>
macro add(a, b) => a + b;

It is expected that when we try to call it as add("1", 2), the compiler will error with message:

25: 
26: fn void! main()
27: {
28:   add("1", 2);
      ^^^^^^^^^^^
(/home/starleks/coding/probe/c3-demo/main.c3:28:3) Error: @require "types::isNumeric($typeof(a)) && types::isNumeric($typeof(b))" violated: '123123'.

Instead it goes into:

21: <* 
22:  * @require types::isNumeric($typeof(a)) && types::isNumeric($typeof(b)) "123123" 
23:  *>
24: macro add(a, b) => a + b;
                       ^^^^^
(/home/starleks/coding/probe/c3-demo/main.c3:24:20) Error: Cannot do the addition 'String' + 'int'.

The funniest thing is that when I change mnemonic of a function to:

<* 
 @require types::isNumeric($typeof(a)) && types::isNumeric($typeof(b)) "123123" 
 *>
macro add(a, b) => a + b;

compiler falls into first message! I have deleted star before @require. It may be funny with macros but devastating with run-time checks in functions. So if I do something like this:

<* 
 * @require a != 0
 *>
fn int add(int a, int b) => a + b;

fn void! main()
{
  add(0, 2);
}

Program will successfully run without any problem, but should I erase a star, it works as expected:

ERROR: '@require "a != 0" violated.'
  in std.core.builtin.default_panic (/nix/store/daky9sv8p5yz1y9l1phl741jf0zam19p-c3c-0.6.5/lib/c3/std/core/builtin.c3:98) [./main]
  in main.add (/home/starleks/coding/probe/c3-demo/main.c3:22) [./main]
  in main.main (/home/starleks/coding/probe/c3-demo/main.c3:28) [./main]
  in @main_to_err_main (/nix/store/daky9sv8p5yz1y9l1phl741jf0zam19p-c3c-0.6.5/lib/c3/std/core/private/main_stub.c3:12) [./main] [inline]
  in main (/home/starleks/coding/probe/c3-demo/main.c3:26) [./main]
  in __libc_start_call_main (source unavailable) [/nix/store/3bvxjkkmwlymr0fssczhgi39c3aj1l7i-glibc-2.40-36/lib/libc.so.6]
  in __libc_start_main_alias_2 (source unavailable) [/nix/store/3bvxjkkmwlymr0fssczhgi39c3aj1l7i-glibc-2.40-36/lib/libc.so.6]
  in _start (source unavailable) [./main]
vssukharev commented 1 week ago

Probably I've found the problem. parse_doc_start function in src/compiler/lexer.c. To be more precise, it's line 1200, when we set may_have_contract to false after seeing a *. I don't know why it's done so try to figure out.

lerno commented 1 week ago

This is not a bug. <* *> is not parsed as comments. It consists of a header section which is terminated by either on a new row by an @identifier or *>. When you write * @require then this is interpreted as a the header.

joshring commented 1 week ago

From: https://c3-lang.org/language-fundamentals/comments/#doc-comments

Doc Comments

Documentation comments start with < and must be terminated using >. Note that any number of may follow < and any number of stars may preceed >. Any space and in the beginning of each line will be ignored.

I think we might need to update this to the following?

Documentation comments start with <* and must be terminated using *>. Note that you may not include * after <* except to write *>. Any space at the beginning of each line will be ignored.

lerno commented 1 week ago

I've updated it a bit now @joshring

vssukharev commented 1 week ago

@lerno, it is quiet confusing to have star it the beginning fed as header - it's so easy to misuse that. I've tested it and it doesn't really conflct with existing code as we merely skip the star before contract

Btw, std library also has several functions with:

<*
  * ...
  *>
lerno commented 1 week ago

(1) we don't want people to use a leading star, because that actually complicates parsing (I was pretty unhappy about that special code in the lexer before)

(2) The idea was that this new style would look more like a code block, so making it retain more comment-like affordances is probably not a great idea. There were some suggestions that maintained a left-hand side * vertical line (or similar), but in those cases the intent was to have that mandatory. So we either have mandatory * in the left hand column or we don't allow them, that's what I prefer.

The only occurrence I could found in the stdlib was a single comment that was accidentally turned into a contract. I've fixed it now (turning it into a comment again). Did you find something else?

vssukharev commented 1 week ago

You can comment one line in lexer.c and see the errors during tests to see other occurrences of such bug in stdlib. It reported me an error in mem_alloc or something like that. You can my commit in pull request which erases this line.

Regarding inclusion of a star, it's not really a problem to handle this what I've tried to do in pull request, but this will add one more stylistical benefit to the language.

Could you please give some examples of when this star might be required to write?

lerno commented 1 week ago

Ah, the interfaces has contracts indented.

An example when we don't want to trim the *:

<*
 This code takes abc and calculates
 *(abc + 3), and then puts it into bcd.

 @return "the result of the computation" 
*>
vssukharev commented 1 week ago

For now it doesn't cause any problems and is simply skipped. You mean it would be complicated to distinguish and generate contracts and comments in future?

lerno commented 1 week ago

I have a tentative plan to make the doc comments be accessible at compile time, so I don't want cleaning of * that aren't intended. A similar problem arises with generating docs. It would have to add a heuristic to know if a * should be stripped or not. Consider:

<*
 *abc + foo will be calculated and returned.
 *>
fn void* foo(void* abc, int foo) { ... }

vs

<*
 * abc + foo will be calculated and returned.
 *>
fn int foo(int abc, int foo) { ... }

When parsing the doc, this is done assuming text, so there is no way for anything to work out whether stripping the * is correct or not. Presumably IDEs would like to be able to show these docs on hover etc.

Also having an optional * prefix is reasonable when everything is comment based, less so when it's not.

As for the parsing, mostly it prevents a later extension like this:

<*
 Foo
 @require a > 0
    "a must be at least 1"
*>

Which would eliminate some state from the lexer.

vssukharev commented 1 week ago

Oh, okay. Then it makes more sense to me, thanks!