Commit Graph

444 Commits

Author SHA1 Message Date
Denis Merigoux
7f705beb07
Merge branch 'master' into aides_logement_outre_mer 2023-03-17 17:52:10 +01:00
Raphaël Monat
d5cd5b206a Show conflicting date rounding mode declarations when they happen 2023-03-16 18:51:01 +01:00
Raphaël Monat
8981b21edb Add test for date rounding option conflict 2023-03-16 17:20:14 +01:00
Raphaël Monat
5cf6bdffb8 Add tests for date rounding option 2023-03-16 17:20:13 +01:00
Denis Merigoux
74df4ee988
Merge branch 'master' into aides_logement_outre_mer 2023-03-14 14:10:09 +01:00
Louis Gesbert
6388a4b79f Improved some error messages (cyclic defs, def positions) 2023-03-08 15:27:48 +01:00
Denis Merigoux
bfc827296c
Merge branch 'master' into aides_logement_outre_mer 2023-03-06 14:09:51 +01:00
Louis Gesbert
97e0cfca6f Improvements on function arguments refactoring
- simplify naming in the french law examples
- make messages yet more precise on function arguments mismatch
2023-03-02 19:11:21 +01:00
Louis Gesbert
fc5910e093 Fix multi-argument scopedefs, improve error message positions
This adds a few positions to the parser, and tweaks some others, vastly
improving the reporting of some errors (inconsistent functions definitions, but
also exceptions cycles, etc.)
2023-02-28 15:53:50 +01:00
Louis Gesbert
2c97d5de14 Enforce consistency of function arguments naming 2023-02-28 15:53:50 +01:00
Louis Gesbert
8200457e43 Syntax change: require declaration of function argument names 2023-02-28 15:53:50 +01:00
Louis Gesbert
6b44d19919 Tests: add function parameter inconsistency checks 2023-02-28 15:53:50 +01:00
Denis Merigoux
0667e3d40f
Merge branch 'master' into aides_logement_outre_mer 2023-02-28 15:01:31 +01:00
adelaett
621b4bd974 add of an example with partial code duplication (non-exponential) 2023-02-28 08:36:45 +01:00
Louis Gesbert
5bd140ae5f
Arrow List (#404) 2023-02-22 14:06:55 +01:00
adelaett
9f31715a47 style 2023-02-22 12:11:42 +01:00
adelaett
9a3a318ee0 updated the output of functions, since we now generate functions with multiple parameters 2023-02-21 14:18:35 +01:00
adelaett
e9f8843e4f adding one simple test about toplevel definitions 2023-02-21 14:17:58 +01:00
adelaett
a59a2f77fc typos in readme 2023-02-21 14:17:30 +01:00
Louis Gesbert
8c40b1ddd0 Fix python output of toplevel defs
there is room for name clashes there though, maybe we should find a more
consistent renaming mechanism
2023-02-17 19:59:22 +01:00
Louis Gesbert
c3af0b4097 Toplevel definitions: branch cleanup
- fix remaining warnings (mostly unused arguments)
- renamings throughout for consistency and clarity
2023-02-13 18:02:09 +01:00
Louis Gesbert
912e1500c4 Handle toplevel defs down to scalc 2023-02-13 11:44:32 +01:00
Louis Gesbert
6f1ac5837d Add syntax for calling multi-argument functions
* temporary and undocumented while waiting for discussion an approval
* previous patches already allowed definition (at toplevel) but there was no
syntax for calls
* no syntax for multi-args _local_ functions yet
2023-02-13 11:44:32 +01:00
Louis Gesbert
d66cd1e29c Toplevel defs: tests & fixes 2023-02-13 11:44:32 +01:00
Denis Merigoux
d7df6b3e80
Typing now takes into account [TAny] in structs/enums 2023-02-08 16:00:53 +01:00
Denis Merigoux
c78a004b53
Leave everything unresolved for now 2023-02-08 16:00:53 +01:00
Denis Merigoux
7d6abf36b2
Taking into account that closures can be input and output of scopes 2023-02-08 16:00:21 +01:00
Denis Merigoux
6906fa48d1
Fix test for CI 2023-02-08 16:00:21 +01:00
Denis Merigoux
3577507ee9
Switch from closure-passing to environment-passing closure conversion 2023-02-08 16:00:21 +01:00
Denis Merigoux
4521d05839
Starting to implement hoisting 2023-02-08 15:59:51 +01:00
Denis Merigoux
47c6746982
One test passing 2023-02-08 15:59:51 +01:00
Denis Merigoux
83e9e83909
Progressing [skip ci]
Testing with dune exec catala -- Lcalc -s S tests/test_func/good/closure_conversion.catala_en  --avoid_exceptions -O --closure_conversion
2023-02-08 15:59:51 +01:00
Denis Merigoux
21d4360120
Add verification condition special case for scope context arguments 2023-01-20 15:55:28 -05:00
Denis Merigoux
ec6616c091
Changing encoding of direct scope call to avoid empty error confusing static analysis 2023-01-20 15:23:50 -05:00
Denis Merigoux
8405d243be
Fix compiler and tests 2023-01-20 14:10:18 -05:00
Denis Merigoux
7cffc53169
Merge branch 'master' into afromher_334 2023-01-20 14:05:38 -05:00
Denis Merigoux
cd4f7db547
Removed useless file 2023-01-13 11:57:56 +01:00
Denis Merigoux
2f4a51ce64
Bug fixed! It was tricky 2023-01-07 20:22:36 +01:00
Denis Merigoux
9c6a126af3
Update formatting 2023-01-07 18:38:02 +01:00
Denis Merigoux
c723249337
Managed to find a MWE of the bug 2023-01-06 17:07:43 +01:00
Louis Gesbert
2003566867 Force parens in compound logic formulas
Closes #373

This forbids expressions such as `a and b or c`, avoiding the need to set an
implicit priority between `and`, `or` and `xor`, which I find error-prone.

Instead, when that appears, a message asking for explicit parentheses will be
shown to the user.

Implementation note: since that would be extremely tedious to do in the parser
directly, the parser is set to allow right-associativity without discrimination
for the logical operators, and the check is done during desugaring. This
required to explicit parentheses in the surface AST to discriminate the case
where the priority was explicit.
2023-01-04 10:46:14 +01:00
Louis Gesbert
51df581aba Small cleanup/fixes following PR review on Syntax Changes 2022-12-20 16:03:41 +01:00
Louis Gesbert
9e514755b7 Collection syntax: re-add combined filter+map 2022-12-19 15:17:17 +01:00
Louis Gesbert
47502335aa Refactor the parser to use priorities
Define a single expression rule with disambiguation using token priorities
instead of the many layers of intermediate rules with explicit sub-terms.

Also replaces `in` for collection operations (`x+1 for foo in [1;2]`) with
`among` which helps a lot.
2022-12-19 15:12:53 +01:00
Louis Gesbert
f236e2cfb2 Replace the type conversion and rounding operators with overloads
Ref. #366

Also updates `CONTRIBUTING.md`.

This was pretty straight-forward :)
2022-12-13 15:32:49 +01:00
Louis Gesbert
c94509e0bb Remove integer division from the language
it's unlikely to be used in any law, and likely to be cause for confusion.

best of all, the new operator has a different return type, which
ensures no inconsistency with the change can get overlooked.
2022-12-13 12:35:02 +01:00
Louis Gesbert
dcb422302d Tests/examples update 2022-12-13 12:30:40 +01:00
Louis Gesbert
bb58d11ca8 Improve syntax for scope calls
implements #357
2022-12-13 12:30:38 +01:00
Louis Gesbert
09d49ab1cc French syntax: replace 'sortie' with 'résultat'
as per comment in #357
2022-12-13 12:27:33 +01:00
Louis Gesbert
71bb67163c Remove explicitely typed operators in tests and examples
Command used: `sed -i 's/\([-+*/><=]=\?\)[.$@^€$]/\1/g' **/*/*.catala_*`

The overload test, of course, is kept unchanged and ensures that explicit
operators still work.
2022-12-13 12:00:04 +01:00
Louis Gesbert
fea01cfe4c Add overloaded operators for the common operations
This uses the same disambiguation mechanism put in place for
structures, calling the typer on individual rules on the desugared AST
to propagate types, in order to resolve ambiguous operators like `+`
to their strongly typed counterparts (`+!`, `+.`, `+$`, `+@`, `+$`) in
the translation to scopelang.

The patch includes some normalisation of the definition of all the
operators, and classifies them based on their typing policy instead of
their arity. It also adds a little more flexibility:
- a couple new operators, like `-` on date and duration
- optional type annotation on some aggregation constructions

The `Shared_ast` lib is also lightly restructured, with the `Expr`
module split into `Type`, `Operator` and `Expr`.
2022-12-13 11:55:24 +01:00
Louis Gesbert
5bcc0a65eb Improve some messages on structure disambiguation 2022-12-13 11:47:21 +01:00
Denis Merigoux
619461dba8
Merge branch 'master' into fix_362 2022-12-07 15:32:08 +01:00
Denis Merigoux
e448a1a1b4
Fix 362 (was harder than expected and unit tests helped catch subsequent encoding bugs!) 2022-12-02 16:42:29 +01:00
Denis Merigoux
eee9946847
Fix extra error on empty 2022-12-02 12:07:26 +01:00
Denis Merigoux
6523181ec7
Wrote unit tests before fix 2022-12-01 18:14:03 +01:00
Louis Gesbert
4ee4a96ac7 Remove *all* struct field access qualifiers in catala code
They are no longer needed \o/
2022-11-28 16:42:02 +01:00
Louis Gesbert
8960e5dbbc Add typing-based disambiguation pass after desugaring
Some typing errors are changed a little, because they get triggered during the
typing of the disambiguation pass, which does not specify the expected return
type (it's an expected invariant that it should not be needed for
disambiguation).

It would be possible to still specify these types during disambiguation just to
get the same errors, but since the newer ones don't appear to be clearly worse
at the moment, it has not been done.
2022-11-28 16:38:09 +01:00
Louis Gesbert
c92fe5e72d Fix underline of code errors when code contains utf8 2022-11-28 16:38:09 +01:00
Louis Gesbert
af2f5dbe19 Tweak error message location printing 2022-11-28 16:38:09 +01:00
Louis Gesbert
a5ea9451bc Fix extra spacing in struct printer 2022-11-21 17:11:53 +01:00
Louis Gesbert
4ae392c900 AST refactoring
Many changes got bundled in here and would be too tedious to separate.

Closes #330

See changes in `shared_ast/definitions.ml` to check the main point.

- the biggest change is a modification of the struct and enum types in
  expressions: they are now stored as `Map`s throughout passes, and no longer
  converted to indexed lists after scopelang. Their accessors are also changed,
  and tuples only exist in Lcalc (they're used for closure conversion).

  This implied adding some more information in the contexts, to keep the mapping
  between struct fields and scope output variables. It should also be much more
  robust (no longer relying on assumptions upon different orderings).

- another very pervasive change is more cosmetic: the rewrite of the main AST to
  use inline records, labelling individual subfields.

- moved the checks for correct definitions and accesses of structures from
  `Scope_to_dcalc` to `Typing`

- defining some new shallow iterators in module `Shared_ast.Expr`, and
  factorising a few same-pass rewriting functions accordingly (closure
  conversion, optimisations, etc.)

- some smaller style improvements (ensuring we use the proper compare/equal
  functions instead of `=` in a few `when` closes, for example)
2022-11-17 18:16:09 +01:00
Aymeric Fromherz
e37ad1de44 Reset tests 2022-11-08 22:28:02 +01:00
Aymeric Fromherz
63572b6963 Add bad test for assertions 2022-11-08 22:27:17 +01:00
Aymeric Fromherz
4af44fb519 Add debug info about encoded assertions 2022-11-08 22:25:07 +01:00
Aymeric Fromherz
9ad7362381 Add testcase from issue 2022-11-08 20:38:09 +01:00
Louis Gesbert
f8f1ae283f Scopelang printer: use 'struct'/'enum' rather than 'type' 2022-11-07 14:13:03 +01:00
Louis Gesbert
4d4dac6727 Some fancy unicode for error outlines
Normally I would make sure this is not by default, or at leat disableable; but
here the code we print may contain utf8 anyway, so the terminal really needs to
support it. Anyway, it's just a little fancier, doesn't add much.
2022-11-07 14:13:01 +01:00
Louis Gesbert
429911024c Add parseable line-column info to error messages
a quick fix for now, ideally we want an option for editor-friendly output.
But for now this is a very cheap way to at least have clickable error messages
which are a big time-saver.
2022-11-07 14:03:38 +01:00
Louis Gesbert
3e004551fc Callable scopes: fixes following review 2022-11-03 15:18:51 +01:00
Louis Gesbert
6e2c3eee4d Fix the regression on badly tagged scope variable error message
it actually simplifies the typer a little to not care about this specific error,
which is better handled in desugared_to_scope already.
2022-10-25 14:50:49 +02:00
Louis Gesbert
ddd7ce9a4e Error handling for invalid scope calls 2022-10-25 11:38:22 +02:00
Louis Gesbert
73173285e4 Scope calls: proper handling of context vars
Also proper error messages on bad scope input specifications.

* Still needs more tests
2022-10-25 11:30:45 +02:00
Louis Gesbert
41d6d3cbe9 Make scopes directly callable
Quite a few changes are included here, some of which have some extra
implications visible in the language:

- adds the `Scope of { -- input_v: value; ... }` construct in the language

- handle it down the pipeline:
  * `ScopeCall` in the surface AST
  * `EScopeCall` in desugared and scopelang
  * expressions are now traversed to detect dependencies between scopes
  * transformed into a normal function call in dcalc

- defining a scope now implicitely defines a structure with the same name, with
  the output variables of the scope defined as fields. This allows us to type
  the return value from a scope call and access its fields easily.
  * the implications are mostly in surface/name_resolution.ml code-wise
  * the `Scope_out` struct that was defined in scope_to_dcalc is no longer
    needed/used and the fields are no longer renamed (changes some outputs; the
    explicit suffix for variables with multiple states is ignored as well)
  * one benefit is that disambiguation works just like for structures when there
    are conflicts on field names
  * however, it's now a conflict if a scope and a structure have the same
    name (side-note: issues with conflicting enum / struct names or scope
    variables / subscope names were silent and are now properly reported)

- you can consequently use scope names as types for variables as well. Writing
  literals is not allowed though, they can only be obtained by calling the
  scope.

Remaining TODOs:

- context variables are not handled properly at the moment

- error handling on invalid calls

- tests show a small error message regression; lots of examples will need
  tweaking to avoid scope/struct name or struct fields / output variable
  conflicts

- add a `->` syntax to make struct field access distinct from scope output var
  access, enforced with typing. This is expected to reduce confusion of users
  and add a little typing precision.

- document the new syntax & implications (tutorial, cheat-sheet)

- a consequence of the changes is that subscope variables also can now be typed.
  A possible future evolution / simplification would be to rewrite subscopes as
  explicit scope calls early in the pipeline. That could also allow to manipulate
  them as expressions (bind them in let-ins, return them...)
2022-10-21 17:17:26 +02:00
Louis Gesbert
19d0c35961 Printer: less verbose variables printing
Pass along a bindlib context to allow the variable names to be altered only when
disambiguation is needed. Partial fix to #240 (doesn't affect the backends, only
the printer for the intermediate ASTs).

This also has the benefit of making the output of the tests much more stable.
2022-10-19 14:40:58 +02:00
Louis Gesbert
7bcafa4ead Fix bug in bindlib use
This is a workaround (but corresponds to what was executed before) and means
that we re-explore all exprs to look for free variables.

The proper fix will be to store boxed_exprs inside scopes instead.
2022-10-07 18:00:59 +02:00
Louis Gesbert
6c8a9f830c Compute the Dcalc stage when running catala Typecheck
it has some important resolution/sanity checks
2022-10-07 17:41:27 +02:00
Louis Gesbert
6c0c2f073d Update test on i/o variable check
This is no longer detected by pure type-checking, as the check is done during
compilation to scope-lang, which now takes place afterwards.
2022-10-04 14:50:37 +02:00
Louis Gesbert
1b3a1f7219 Update test results
These are just variable renumberings, and type error message changes but still
pointing to the same information; the latter are slightly better in general,
pointing to actual expressions rather than scope declarations.
2022-10-04 14:50:37 +02:00
Louis Gesbert
609cc5cc9a Tests: add info on manually running a single test 2022-10-04 14:50:37 +02:00
Louis Gesbert
12d2833306 Fix cyclic type test
Make it type so that it's actually the cycle error that is raised
(now that expression typing is done earlier)
2022-10-04 14:50:37 +02:00
Louis Gesbert
d93b699a4c Forward types in the Expr.make_* constructors
Also add some safeguards against bad propagation of types (e.g. checking the
arrow type of functions upon application); partly disabled at the moment since
they don't pass yet but that'll be further work.
2022-10-04 14:50:37 +02:00
Louis Gesbert
3d73071012 Typing tests: reword test doc for clarity 2022-09-26 15:27:36 +02:00
Louis Gesbert
a41de29293 Improve typing error message on <any> array
- don't print variable id on type variables, there should be no ambiguity
- print "array" as "collection" to match the language
- print just "collection" for "'a collection", which makes sense english-wise
2022-09-26 14:29:15 +02:00
Louis Gesbert
abd5a4de96 Tests: cleanup remaining whitespace 2022-09-26 14:27:47 +02:00
Louis Gesbert
c18de3b980 Tweak the order in which typing is done 2022-09-26 14:11:25 +02:00
Louis Gesbert
76569bb1af Fix position on type error concerning sub-scope variable 2022-09-26 14:11:25 +02:00
Louis Gesbert
498429e4b7 Fix type-checking error getting delayed
The issue was coming from Bindlib: it stores variable bindings as closures, so
`Bindlib.box_apply f bx` actually delays the application of `f` until the term
is substituted or unboxed (likely long after we are out of the `try..with`
block).

The proposed fix is to make sure we run the wrapper outside of bindlib
applications, on explicitely unboxed terms.
2022-09-26 14:11:25 +02:00
Louis Gesbert
8bf6b5b821 Type arrow return types first 2022-09-26 14:11:25 +02:00
Louis Gesbert
2c3be946ec Keep type positions on the right-hand side upon unification of types
This should result in more predictable error messages. Right-hand is arbitrary,
but has been found empirically to give better results.
2022-09-26 14:11:25 +02:00
Louis Gesbert
43e4efeeb8 Some typing error tests improvements 2022-09-26 14:11:25 +02:00
Louis Gesbert
8c1696d0ff Inline tests: cleanup trailing whitespace 2022-09-23 16:56:21 +02:00
Louis Gesbert
fe6fabb1b0 Clerk tests: update README 2022-09-23 16:41:22 +02:00
Louis Gesbert
0c0ef1ae1a Add test return codes
Simply re-generated with 'make tests CLERK_OPTS=--reset'
2022-09-23 14:50:02 +02:00
Louis Gesbert
0ab7a0f9ce Turn all existing tests to inline tests
Done using
```bash
process() { FILE=$1; awk 'match($0, /^```catala-test *{ *id *= *"(.*)" *}/, a) {print "```catala-test-inline"; f="'"$(dirname $FILE)/output/$(basename $FILE)"'." a[1]; getline; print "$ " $0; while ((getline<f) > 0) print; next} {print}' $FILE >$FILE.new; mv $FILE.new $FILE; }
for f in tests/test_*/*/*.catala_* examples/**/*.catala_*; do process $f; git add $f; done
for d in $(find -name output -type d); do git rm -r $d; done
```
2022-09-23 14:45:10 +02:00
Louis Gesbert
1b97f55c00 Add a few tests on typing errors
the `err6` test also highlights that Typecheck errors get overly delayed
2022-09-15 17:28:05 +02:00
Aymeric Fromherz
2c5b3dd25e Add unit tests for extension of Z3 backend to non-bool EMatch nodes 2022-09-13 16:05:33 +02:00
Denis Merigoux
d7e219b0dd
Correct test output for proof mode 2022-09-06 14:10:32 +02:00
Denis Merigoux
a1e6d992a9
Fix test output 2022-09-05 10:48:05 +02:00
Raphaël Monat
d9cc2dbb43 Fix format in excepted test 2022-09-05 09:31:39 +02:00