Commit Graph

107 Commits

Author SHA1 Message Date
Micah Kendall d39dbd6697 fmt 2024-04-12 21:40:27 -04:00
Micah Kendall d25b8f91c7 feat: Emit keyword 2024-04-12 21:40:27 -04:00
rvcas b27fcf38e5
fix(check): collapse_links on tuple_index access closes #905 2024-04-02 19:45:16 -04:00
rvcas 4f8e900aac
fix: Discard not taken into account in backpassing
closes #890

Co-authored-by: Kasey White <kwhitemsg@gmail.com>
2024-03-20 17:53:17 -04:00
rvcas 898ef74457
fix: spans for backpassing args
closes #882

Co-authored-by: Kasey White <kwhitemsg@gmail.com>
2024-03-20 17:27:17 -04:00
KtorZ 3055c5ef52
Do not allow casting when rhs or lhs contain an opaque type.
Also slightly extended the check test 'framework' to allow registering side-dependency and using them from another module. This allows to check the interplay between opaque type from within and outside of their host module.
2024-03-14 11:00:17 +01:00
rvcas e71470747f
feat: fix some tests and add a failing one 2024-03-13 20:18:56 -04:00
KtorZ 9127dcdd6e
Add note on the type-casting check. 2024-03-13 20:18:56 -04:00
KtorZ 8f31b45e36
Fix allow_casting condition in unification
We should allow casting from any type to any type. Or at the very least, allow it for well-known types like List.
2024-03-13 20:18:56 -04:00
KtorZ f10cf73905
Rework 'is_opaque' to also check for inner types.
Also removed the duplication in infer_assignment and moved the check down.
2024-03-13 20:18:56 -04:00
KtorZ 3820d2af14
Remove potentially problematic use of ".." in pattern-match
Discard pattern are _dangerous_ is used recklessly. The problem comes
  from maintenance and when adding new fields. We usually don't get any
  compiler warnings which may lead to missing spots and confusing
  behaviors.

  So I have, in some cases, inline discard to explicitly list all
  fields. That's a bit more cumbersome to write but hopefully will catch
  a few things for us in the future.
2024-03-13 20:18:51 -04:00
rvcas 7af4ef53ab
feat: block expects on opaque types 2024-03-13 20:17:54 -04:00
microproofs b16880a170 feat(annotation): not passing annotation into lambda when backpassing
Co-authored-by: Lucas Rosa <x@rvcas.dev>
2024-03-13 19:08:53 -04:00
rvcas 7b32d4ae30 chore: add a test for formatting assignment patterns 2024-03-12 08:10:33 -04:00
rvcas 97247ce949 chore: assignment patterns refactor tuple into struct 2024-03-12 08:10:33 -04:00
rvcas b6b52ba508 feat(backpassing): implements multi patterns
The main trick here was transforming Assignment
to contain `Vec<UntypedPattern, Option<Annotation>>`
in a field called patterns. This then meant that I
could remove the `pattern` and `annotation` field
from `Assignment`. The parser handles `=` and `<-`
just fine because in the future `=` with multi
patterns will mean some kind of optimization on tuples.
But, since we don't have that optimization yet, when
someone uses multi patterns with an `=` there will be an
error returned from the type checker right where `infer_seq`
looks for `backpassing`. From there the rest of the work
was in `Project::backpassing` where I only needed to rework
some things to work with a list of patterns instead of just one.
2024-03-12 08:10:33 -04:00
KtorZ 7e8e959251
Fix spans and error reporting for backpassing. 2024-03-11 00:20:29 +01:00
KtorZ a57dcf3307
Allow backpassing with expect. 2024-03-11 00:20:29 +01:00
KtorZ 435dd0d213
Refactor AssignmentKind to allow backpassing on both let and expect.
The 3rd kind of assignment kind (Bind) is gone and now reflected through a boolean parameter. Note that this parameter is completely erased by the type-checker so that the rest of the pipeline (i.e. code-generation) doesn't have to make any assumption. They simply can't see a backpassing let or expect.
2024-03-11 00:16:23 +01:00
KtorZ df898bf239
Rework monadic-bind into function backpassing.
This is more holistic and less awkward than having monadic bind working only with some pre-defined type. Backpassing work with _any_ function, and can be implemented relatively easily by rewriting the AST on-the-fly.

  Also, it is far easier to explain than trying to explain what a monadic bind is, how its behavior differs from type to type and why it isn't generally available for any monadic type.
2024-03-11 00:16:22 +01:00
KtorZ 1f530f3b24
Experiment with monadic bind. 2024-03-11 00:16:22 +01:00
KtorZ c169596c76
preserve type-aliases from annotations on calls. 2024-03-10 00:38:03 +01:00
KtorZ ee54266d1f
Forbid non-serializable inhabitants in compound data-types. 2024-03-09 22:25:51 +01:00
KtorZ d6cc9bdfbe
Allow implicit discard when right-hand side is Void.
This is the most intuitive/expected behavior. Otherwise, it forces a pointless let-binding to 'Void' or into a discard.
2024-03-09 01:28:29 +01:00
rvcas 836e853827 fix: bring back vec1 2024-03-08 19:19:07 -05:00
rvcas fe6710935d feat: impl serde on errythang 2024-03-08 19:19:07 -05:00
KtorZ 23a22a65cb
Handle (recursive) generic types during reification.
Also moved a bunch of functions from code-gen back into _tipo_, as
  they're better suited and generic enough to be reused elsewhere.
2024-03-07 18:07:52 +01:00
KtorZ aadf3cfb48
Allow test definition to carry one parameter
The parameter is special as it takes no annotation but a 'via' keyword followed by an expression that should unify to a Fuzzer<a>, where Fuzzer<a> = fn(Seed) -> (Seed, a). The current commit only allow name identifiers for now. Ultimately, this may allow full expressions.
2024-03-03 19:33:24 +01:00
rvcas 3582c5569d
fix: no single when clause warning sometimes
While looking at some code, I noticed that this
warning would show up even if an error for a
non-exhaustive when/is shows up for the same when/is
expression. This isn't a useful situation to show this
warning because things are not exhaustive yet so we should
let the user finish and only provide the errors. If things
are exhaustive then the code proceeds and if a warning was set
when there's only one clause pattern then this warning message
can be pushed because that's when it's actually useful.
2024-02-13 20:12:40 -05:00
rvcas 4c5a449d83
chore: improve a comment/doc 2024-02-13 19:46:34 -05:00
rvcas 25a837ab3f
feat: parser and check fixes
- do not erase sequences if the sole expression is an assignment
- emit parse error if an assignment is assigned to an assignment
- do not allow assignments in logical op chains
2024-01-19 14:32:21 -05:00
KtorZ 59c784778e
Convert span's start to line number + col
This requires to make line numbers a first-class citizen in the module
  hierarchy but it is fortunately not _too involved_.
2024-01-19 14:30:15 +01:00
KtorZ e67d5863a1
Introduce 'compact' trace level verbosity
For now, it only shows the span start. We'll change that in the next commit to show a line number and a column.
2024-01-19 14:30:15 +01:00
KtorZ d27ea98a8f
Rework tracing arguments to --keep-traces & --trace-level
This allows for a more fine-grained control over how the traces are showed. Now users can instrument the compiler to preserve only their user-defined traces, or the only the compiler, or all, or none. We also want to add another trace level on top of that: 'compact' to only show line numbers; which will work for both user-defined and/or compiler-generated traces.
2024-01-19 14:30:15 +01:00
rvcas 832ca81a8c
fix(lsp): when desugaring and/or chains we should use the whole span of the chain for the generated BinOp locations 2023-11-28 19:19:56 -05:00
rvcas 2980e8e21d
fix: use a distinct warning for discarded let assignments to avoid confusion closes #763 2023-11-27 21:23:10 -05:00
rvcas 6869f73033 fix: sequence formatting when not top level 2023-11-20 11:44:16 -05:00
microproofs 8b89ba3b93 feat: implement bls primitives in code gen 2023-11-15 15:55:56 -05:00
rvcas 3675762c3e feat(bls): aiken level g1 and g2 literals 2023-11-15 15:55:56 -05:00
rvcas e5801f9c19
feat: support doc comments for functions args and validator params
- Add support to the formatter for these doc comments
- Add a new field to `Arg` `doc: Option<String>`
- Don't attach docs immediately after typechecking a module
  - instead we should do it on demand in docs, build, and lsp
  - the check command doesn't need to have any docs attached
  - doing it more lazily defers the computation until later making
    typechecking feedback a bit faster
- Add support for function arg and validator param docs in
  `attach_module_docs` methods
- Update some snapshots
- Add put_doc to Arg

closes #685
2023-10-16 13:38:23 -04:00
rvcas e8bcbecf31
chore: avoid cloning name 2023-10-12 17:50:44 -04:00
rvcas 55f89a7ff4
fix: incorrect 'unused::constructor'
`ExprTyper` was not incrementing the usage of a constructor
when infering `RecordAccess`.

closes #554
2023-10-12 17:44:57 -04:00
rvcas 52dfc13f8f
chore: explain a weird if condition 2023-10-12 17:24:11 -04:00
rvcas 135dbd8335 feat: handle pipe fn infer TODOs
This improves error messages for `a |> b(x)`.

We need to do a special check when looping over the args
and unifying. This information is within a function that does not belong
to pipe typer so I used a closure to forward along a way to add
metadata to the error when the first argument in the loop has a
unification error. Simply adding the metadata at the pipe typer
level is not good enough because then we may annotate regular
unification errors from the args.
2023-10-03 01:17:15 -04:00
rvcas d808197507
chore: clippy fix 2023-09-13 18:17:59 -04:00
rvcas e4ef386c44 feat(tipo): inference for and/or chains 2023-08-15 09:58:35 -04:00
rvcas f1100e901d feat(exhaustiveness): pretty print missing patterns 2023-08-01 21:13:50 -04:00
rvcas de2791fe82 feat(tipo): add new error for redundant clauses 2023-08-01 21:13:50 -04:00
rvcas e8a71cd63b chore: rename usefulness module 2023-08-01 21:13:50 -04:00
rvcas 03efb46e6f feat(exhaustiveness): algorithm U borrowed from elm 2023-08-01 21:13:50 -04:00