Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Register builtins during scoping and report proper errors instead of crashing #2943

Merged
merged 19 commits into from
Aug 20, 2024

Conversation

janmasrovira
Copy link
Collaborator

@janmasrovira janmasrovira commented Aug 7, 2024

This pr has two relevant changes:

Errors instead of crases

When registering a builtin, we perform some sanity checks. When unsuccessful, the compiler crashes. This seldom happens because builtins are defined in libraries that we write ourselves. However, any compiler crash is a bug, so this pr refactors these crashes into proper errors.

Registering builtins during scoping

Before this pr, builtins are registered and sanity checked during the translation from Concrete to Internal. This imposes that the order in which we translate stuff is relevant, as we must register a builtin before we use it. For the most part this is fine when the dependency is explicit in the code, but sometimes there are explicit dependencies. E.g. do notation and the builtin monad-bind. In order to avoid adding special rules, it is easier to just register builtins during scoping, so I've refactored the code to do this.

I've also removed the Builtins effect and moved its methods to the InfoTableBuilder since the builtins table is now part of the Scoped InfoTable. Consequently, I've removed the the field _artifactBuiltins.

Future work

@janmasrovira janmasrovira self-assigned this Aug 7, 2024
@janmasrovira janmasrovira changed the title Register builtins during scoping Register builtins during scoping and report proper errors instead of crashing Aug 7, 2024
@janmasrovira janmasrovira force-pushed the register-builtins-scoping branch 3 times, most recently from 375269c to 9ae71b6 Compare August 9, 2024 15:13
@janmasrovira janmasrovira mentioned this pull request Aug 14, 2024
@janmasrovira janmasrovira marked this pull request as ready for review August 14, 2024 21:30
@paulcadman paulcadman added this to the 0.6.6 milestone Aug 20, 2024
@paulcadman paulcadman merged commit 41450a8 into main Aug 20, 2024
4 checks passed
@paulcadman paulcadman deleted the register-builtins-scoping branch August 20, 2024 12:23
janmasrovira added a commit that referenced this pull request Aug 21, 2024
- Closes #2355
- Depends on #2943 

Example:
```
minusOne : Nat -> Maybe Nat
  | zero := nothing
  | (suc n) := just n;


minusThree (n : Nat) : Maybe Nat :=
  do {
    x1 <- minusOne n;
    x2 <- minusOne x1;
    let
      x2' : Nat := x2;
    in
    x3 <- minusOne x2';
    pure x3;
  };
```
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

It is possible to define the same builtin twice without an error
2 participants