Commit Graph

1130 Commits

Author SHA1 Message Date
adelaett
f3abc23c32 fixings tests (90% atm) 2023-03-28 09:54:44 +02:00
adelaett
c3d9ee299f without exception: removing thunking 2023-03-28 09:54:04 +02:00
Denis Merigoux
44d8c32b9f
C backend for Catala : the closure conversion strikes back (#364) 2023-03-28 09:53:22 +02:00
adelaett
ba1c83f278 correct printing of option type 2023-03-28 09:52:40 +02:00
Denis Merigoux
e4c4339856
Small fixes 2023-03-28 09:38:47 +02:00
Aymeric Fromherz
5f04e0efaf cleanup 2023-03-28 13:08:24 +09:00
Aymeric Fromherz
c711b0b1d7 cleanup 2023-03-28 13:00:07 +09:00
Aymeric Fromherz
082caae498 Add support for let_in in Z3 backend 2023-03-28 12:48:44 +09:00
adelaett
9806eb7e0f format for program 2023-03-23 13:46:17 +01:00
adelaett
72ceafd67c scopes does not return optional terms 2023-03-23 10:45:44 +01:00
Denis Merigoux
8b2f3319b8
Merge remote-tracking branch 'origin/master' into aides_logement_outre_mer 2023-03-21 17:57:38 +01:00
Louis Gesbert
69be2f6ed8 Fix literate output of dates 2023-03-21 16:59:34 +01:00
Denis Merigoux
3122dd7821
Update assets 2023-03-21 16:10:00 +01:00
adelaett
78c0842dc6 optimization tests 2023-03-21 14:31:45 +01:00
adelaett
256adcae4b rename invariant 2023-03-21 14:31:21 +01:00
Denis Merigoux
48ef5b8f21
Fix warning and update assets 2023-03-21 14:00:49 +01:00
Denis Merigoux
578091f196
Restore check 2023-03-21 13:49:16 +01:00
Denis Merigoux
aa8ab3be3d
Merge branch 'master' into c_backend 2023-03-21 12:14:10 +01:00
Denis Merigoux
1a7982d225
Better printing 2023-03-21 11:24:19 +01:00
Denis Merigoux
7f705beb07
Merge branch 'master' into aides_logement_outre_mer 2023-03-17 17:52:10 +01:00
adelaett
d2da1c3e43 advancing 2023-03-17 17:24:51 +01:00
adelaett
7c39ad953b fix iota optmi 2023-03-17 17:23:10 +01:00
adelaett
8c66fabe6a fix mission operators in translate 2023-03-17 17:20:46 +01:00
adelaett
9a34ee95b1 equality program 2023-03-17 17:20:35 +01:00
adelaett
61ad00f277 unit test infrastructure for optimization 2023-03-17 17:19:50 +01:00
adelaett
850a1fdb56 more optimization on fold 2023-03-17 11:34:52 +01:00
Louis Gesbert
db09eb0c42
Add date rounding option in scope (#397) 2023-03-17 10:14:36 +01:00
Denis Merigoux
056e84792d
Printing warning for undefined variables 2023-03-17 09:25:14 +01:00
Denis Merigoux
4fcdd005e0
Merge branch 'master' into aides_logement_outre_mer 2023-03-17 09:18:27 +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
51ea9d8cff Format code 2023-03-16 17:20:14 +01:00
Raphaël Monat
d3c27799de Raise exception when more than one rounding mode option has been specified 2023-03-16 17:20:13 +01:00
Raphaël Monat
1e1e3b538e Simplify format 2023-03-16 17:20:13 +01:00
Raphaël Monat
b013f4257d Update parser error message 2023-03-16 17:20:13 +01:00
Raphaël Monat
887ec00d0e Add explicit match 2023-03-16 17:20:13 +01:00
Raphaël Monat
64fa32392f Update generated files 2023-03-16 17:20:09 +01:00
adelaett
4038ea02be rainbox parenthesis 2023-03-16 17:15:08 +01:00
adelaett
82af9e8305 unfolding more bugs 2023-03-16 17:14:33 +01:00
Raphaël Monat
5fc1e8e5d5 Fix operator printing 2023-03-16 16:55:55 +01:00
Raphaël Monat
7021c41f93 Add date rounding option within scopes 2023-03-16 16:55:55 +01:00
adelaett
26551434f2 correct monadic bind & map implementation 2023-03-14 18:36:05 +01:00
adelaett
91ed8e1f5d special handling of the option constructor as a polymorphic one with custom typing rules 2023-03-14 18:31:32 +01:00
adelaett
366a0d952b introducing new operators for handleing defaults 2023-03-14 18:30:58 +01:00
Louis Gesbert
abc5a00c2f Compile LaTeX code using minted without the Python venv
This is a hack, but not a dirty one: a new command `catala pygmentize` is added,
which is just a wrapper around `pygmentize` that calls it with the proper lexers
defined.

The point is that this needs no installation, just a stock `pygmentize`
installation and the `catala` binary.
2023-03-14 17:35:22 +01:00
Denis Merigoux
74df4ee988
Merge branch 'master' into aides_logement_outre_mer 2023-03-14 14:10:09 +01:00
Louis Gesbert
f1e44619e0 LaTeX literate output: handle pygments coloration from within Catala
This leverages the embedded lexer already used for HTML output, and uses the
LaTeX pygments backend to colorise code directly, without the need for `minted`.
2023-03-13 22:33:48 +01:00
adelaett
4d3b021eef finished the implementation, but a few issues are missing 2023-03-13 16:51:06 +01:00
Louis Gesbert
5282aec400 LaTeX output: start refactor 2023-03-13 14:44:34 +01:00
Louis Gesbert
508992de33 Embed the Pygments Catala lexer
This enables the HTML output to work without a custom Pygments installation (or
the proper venv activated)
2023-03-13 14:41:24 +01:00
adelaett
b891114b72 tentative at a fully monadic encoding 2023-03-10 15:35:03 +01:00
adelaett
a8f0155c6e Revert "toying"
This reverts commit 841b14aa0f.
2023-03-10 15:34:29 +01:00
adelaett
21577ff1ba introducing usefull term in the shared ast 2023-03-10 15:33:58 +01:00
adelaett
1580272d7f more precise invariant 2023-03-10 15:32:42 +01:00
adelaett
ba74bbc52a adding MapLabels and SetLabels to the standard Uid definitions. 2023-03-10 15:32:27 +01:00
Louis Gesbert
e1fe37ad09 Fix coloration in HTML output 2023-03-09 15:46:00 +01:00
Louis Gesbert
deb12d2c4a Bump version to 0.8.0
Changelog:
---

A lot has been going on, with more than 530 patches and 70 PRs merged since
0.7.0 last summer. In summary:

- Quite a lot of syntax improvements and changes. Checkout the latest
  [cheat-sheet](https://catalalang.github.io/catala/syntax.pdf) for an overview

- Allow local `let ... equals ... in ...` definitions

- Better error messages and positions throughout

- Added the ability to directly call a scope and retrieve its outputs, like a
  function

- Added disambiguation, allowing to access structure fields without specifying
  the structure type each time

- Added automated resolution of operators, allowing e.g. to write just `+` in
  place of all the type-specific operators `+.`, `+$`, `+@`, `+^`, etc.

- More consistent priority for operators. It is no longer allowed to write `a
  and b or c` without parenthesis.

- Added and changed some operators (`date + duration` now allowed either way,
  `int / int` now returns a decimal, added `duration / duration`)

- Added the ability to have variables and functions defined at
  top-level (outside of any scope). See annex A of the tutorial for details.

- Added support for functions with multiple arguments

- Some big refactors in the compiler, allowing much better code sharing between
  the different passes, and making it much easier to extend. Also added the
  possibility to run the type-checker earlier, etc.

- Countless bug-fixes

- Improvements to our proof backend with Z3

- A tool to automatically synchronise with the upstream French law from
  Legifrance
2023-03-08 18:07:53 +01:00
Louis Gesbert
6388a4b79f Improved some error messages (cyclic defs, def positions) 2023-03-08 15:27:48 +01:00
Louis Gesbert
188a186735 Parser: make state rule syntax consistent with state definitions
Previously the `state` marker for rules was in a weird position:
```catala
rule foo under condition bar
  consequence state st fulfilled
```

This patch unifies the syntax with definitions, now using instead:
```catala
rule foo state st
  under condition bar
  consequence fulfilled.
```
2023-03-08 15:17:58 +01:00
Louis Gesbert
42b8adb968 Add a duration / duration overload
Interstingly enough, it was already implemented in the Python backend.

Required to implement *pro rata temporis*, which the US tax section 121 does
make use of.

Only allowed for durations expressed in days (as returned by `<date> - <date>`),
of course.
2023-03-08 15:17:58 +01:00
adelaett
841b14aa0f toying 2023-03-06 18:26:46 +01:00
adelaett
6c0e04942f corrected iota optimization 2023-03-06 16:00:41 +01:00
Denis Merigoux
bfc827296c
Merge branch 'master' into aides_logement_outre_mer 2023-03-06 14:09:51 +01:00
Denis Merigoux
1fe3987168
Formatting 2023-03-05 12:10:04 +01:00
Louis Gesbert
5398b1037f Fix ill-funded order function on desugared vars 2023-03-03 19:22:17 +01:00
adelaett
78f121b44a before any issues with mark on code_item 2023-03-03 11:39:55 +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
3766e9db2c Fix function argument naming consistency in the examples 2023-02-28 16:17:19 +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
Denis Merigoux
0667e3d40f
Merge branch 'master' into aides_logement_outre_mer 2023-02-28 15:01:31 +01:00
adelaett
73bd4b4064 finished to detect unpure subexpressions 2023-02-28 14:26:48 +01:00
adelaett
43b6595a09 Revert "not working fix for from_scopelang"
This reverts commit 1c837ec3b5.
2023-02-28 09:32:25 +01:00
adelaett
1c837ec3b5 not working fix for from_scopelang 2023-02-28 09:32:10 +01:00
adelaett
178367efc0 adding invariant about App(EStructAccess) 2023-02-28 09:07:12 +01:00
adelaett
4cd3ec7cc3 Add an optimization pass to remove struct access of struct constructor
ie { e = x}.e -> x
2023-02-28 09:06:33 +01:00
adelaett
001a8205af ? 2023-02-28 08:39:30 +01:00
adelaett
631b6d77ff Revert "Abandoning json conversion :("
This reverts commit 02780f5439.
2023-02-28 08:37:50 +01:00
adelaett
02780f5439 Abandoning json conversion :( 2023-02-28 08:36:45 +01:00
adelaett
5fe09238c5 better error management when building with make_app 2023-02-28 08:36:45 +01:00
adelaett
2ae2ff7d50 adding a non-passing invariant 2023-02-28 08:36:34 +01:00
adelaett
75dc978fa9 remove logs from the no_partial_evaluation invariant
removed error_on_empty when functions
2023-02-27 11:20:59 +01:00
adelaett
b5f3621302 serialization wip 2023-02-27 11:20:59 +01:00
adelaett
9ec2b7785d more work on invariants 2023-02-27 11:20:59 +01:00
adelaett
382150b513 new invariant option when launching the compiler 2023-02-27 11:20:59 +01:00
adelaett
6c3f0af9e0 invariant assertion checking 2023-02-27 11:20:59 +01:00
adelaett
173859d10e invariant checking (untested) 2023-02-27 11:20:59 +01:00
adelaett
9319e94617 fix typo 2023-02-27 11:20:59 +01:00
adelaett
9a68563488 assert_internal & skeleton for the static pass 2023-02-27 11:20:59 +01:00
adelaett
8784ae6175 unpure detection in expressions 2023-02-27 11:20:59 +01:00
adelaett
214bc55aae internal error message 2023-02-27 11:20:59 +01:00
adelaett
0262019d45 make app 2023-02-27 11:20:59 +01:00
adelaett
363ef39704 let case 2023-02-27 11:20:59 +01:00
adelaett
2a222f0aab changed nix dependency from ocamlformat 24.1 to 21.0 2023-02-27 11:20:59 +01:00
adelaett
e765ee8a0c requesting to have a typed tree 2023-02-27 11:20:59 +01:00
adelaett
44ce5a636b fix tentative for functions applications 2023-02-27 11:20:59 +01:00
adelaett
5b33b39636 new helpers functions in lcalc's ast 2023-02-27 11:20:59 +01:00
Louis Gesbert
5bd140ae5f
Arrow List (#404) 2023-02-22 14:06:55 +01:00
adelaett
4f029db47b explicitly don't accept multiple arguments from surface to desugared 2023-02-22 12:21:55 +01:00
adelaett
9f31715a47 style 2023-02-22 12:11:42 +01:00
adelaett
8553b9dd7e Alternative printing of type TArrow
Changed the typing printing in the pretty printer to:
* () -> unit for empty lists
* a -> b for single elements lists
* (a, b, c, d) -> b for multiple elements lists
2023-02-22 11:52:22 +01:00
adelaett
bd0243359e changed the invariant documentation of scopelang -> dcalc
Since functions inside catala can now have multiple arguments (while
not yet being user-definable) the invariant is now about partial
evaluation not being possible.
2023-02-22 11:42:48 +01:00
adelaett
576f21f69c Added documentation for encoding constructors in the typing inference 2023-02-22 11:41:21 +01:00
adelaett
51b5ccb08e change operator definition style to something more readable 2023-02-22 11:40:22 +01:00
adelaett
a4466fecc7 fixed some mixup in Format.fprintf arguments 2023-02-21 16:19:17 +01:00
adelaett
99d82bc33e Fix toplevel type definition (if arg_types is [], then use a different way) 2023-02-21 14:17:24 +01:00
adelaett
b512dc6ec7 Fix List.combine internal error (create multiple TAny instead of only one) 2023-02-21 14:16:50 +01:00
adelaett
7036464df3 fix printing error (use utf8 insteed of ->) 2023-02-21 14:16:23 +01:00
adelaett
839a7ffd83 finished refactoring 2023-02-20 17:58:29 +01:00
adelaett
e519b7f146 until desugared 2023-02-20 17:21:44 +01:00
adelaett
f2bebe613b - [x] shared_ast 2023-02-20 15:57:42 +01:00
adelaett
d79b8463a6 - [ ] shared_ast 2023-02-20 15:57:42 +01:00
adelaett
391bf2527d make the change in the datatype 2023-02-20 15:57:42 +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
03645e6404 Rename Scalc from_lambda to from_lcalc for consistency 2023-02-17 19:49:56 +01:00
Denis Merigoux
fced0fff54
Add top-level definitions (#391) 2023-02-15 16:27:04 +01:00
Louis Gesbert
72cf477dd9 Toplevel definitions: fixes following review
Thanks @denismerigoux!
2023-02-15 12:40:15 +01:00
Rohan Padhye
014e11720e Python backend: Use true division
Fixes a regression after the change in #368, which converted all
integer division to return a decimal. The code generation backend
was still using the integer division operand `//`, which is not
overloaded by class `Integer` in the catala runtime.
2023-02-13 16:31:24 -05: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
Louis Gesbert
9b0c7583ec Add top-level definitions
Only handled until before scalc at the moment.
2023-02-13 11:43:49 +01:00
Louis Gesbert
98ebc36343 Add all missing parser error messages
... that's one less thing to do

Two notes:

- Updated the syntax errors in
  examples/NSW_community_gaming/tests/test_nsw_social_housie.catala_en ; those
  probably aren't expected though, but fixing them is outside my purpose here

- There is consensus on keeping the error messages in English; however, here,
  the error messages include hints on the syntax to use, which are only valid
  for users of the English syntax.
  * A possible solution would be to apply cppo on parser.messages, using the
    macros already defined in lexer_LANG.cppo.ml. However, we would then need to
    tweak (or duplicate!) the parser to use the messages for the correct language.
    Furthermore, updating and merging the file on parser updates would need
    special care.
  * Another, maybe easier solution would be manual processing, using a custom
    escape in the parser messages and rewriting that at runtime when printing
    the message. We would need to extract a runtime version of the macro
    definitions though.
2023-02-13 10:51:42 +01:00
Louis Gesbert
3f487a16ed WIP: handle toplevel definitions at the parser level 2023-02-13 10:51:42 +01:00
Louis Gesbert
0540cd31fe Allow ETuple, ETupleAccess on all ASTs
they used to be only allowed on lcalc
2023-02-13 10:51:42 +01:00
Denis Merigoux
7702949401
Better printing 2023-02-08 16:03:23 +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
36a80b0ed3
Better type propagation 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
e7d1fb84e9
Trying to retype closure conversion but fails [skip-ci] 2023-02-08 16:00:20 +01:00
Denis Merigoux
38d5ef9715
Small improvement 2023-02-08 15:59:51 +01:00
Denis Merigoux
4521d05839
Starting to implement hoisting 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
Louis Gesbert
467a338b6c Install Catala plugins
Fixes #378

- the plugins are compiled as libraries rather than with `executable`, so that
  dune is able to install them
- they get installed to `lib/catala/plugins/<plugin-name>/<plugin-name>.cmxs`
- the lookup for plugins is now recursive to cope with the plugin subdirectories
  in the point above
2023-01-17 14:38:09 +01:00
Louis Gesbert
ca7f14e219 formatting fix 2023-01-16 12:10:33 +01:00
Louis Gesbert
19033669f5 Add support for paths in the parser
Using them will lead to "not supported yet" errors soon after, but it's a start
to get to handling separate modules.

The idea is that `foo` can now also be `Bar.foo`, `Bar.Baz.foo`, `foo.Struc.fld`
can be `foo.Bar.Baz.Struc.fld`, etc.
The next steps are to enable the lookups to handle this paths, and to provide
ways to load the external modules to feed these lookups.
2023-01-16 12:09:23 +01:00
Louis Gesbert
f835225a34 Tiny parser simplification
There is no need to keep separate rules for the different kinds of binops anymore.
2023-01-16 12:09:19 +01:00
Denis Merigoux
f4c92530c6
Update aides_logement and fix bugs to produce an updated working simulator (#377) 2023-01-13 12:05:32 +01:00
Denis Merigoux
5fb9031c8a
Fixing review comments 2023-01-11 10:42:21 +01:00
Louis Gesbert
41eb25e9e0 Fix code in LaTeX literate output
pfffff
2023-01-10 12:06:48 +01:00
Denis Merigoux
c31ebdf3f8
Add tabularx as a latex dependency 2023-01-10 10:49:03 +01:00
Denis Merigoux
2f4a51ce64
Bug fixed! It was tricky 2023-01-07 20:22:36 +01:00
Denis Merigoux
9d619a26ba
Correct cli typecheck behavior 2023-01-05 18:56:19 +01:00
Denis Merigoux
124491410d
Revamp encoding, still doesn't work 2023-01-05 18:56:06 +01:00
Denis Merigoux
a3fffb3c8d
Forgot log 2023-01-05 16:43:53 +01:00
Denis Merigoux
fa84dd4330
Splitting long lines 2023-01-05 16:20:51 +01:00
Denis Merigoux
d2ce111fc2
Better legifrance inclusion 2023-01-04 16:30:14 +01:00
Louis Gesbert
e3b98b4f50 Literate: more explicit dune dependency 2023-01-04 12:18:46 +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
e678d0770f Rename a few tokens
In particular `CONSTRUCTOR` is no longer valid for paths & modules, so let's
switch to the more usual LIDENT / UIDENT for lower- or upper- case idents.

cd compiler/surface
sed -i 's/VERTICAL/BAR/g' *
sed -i 's/BRACKET/BRACE/g' *
sed -i 's/SQUARE/BRACKET/g' *
sed -i 's/IDENT/LIDENT/g' *
sed -i 's/CONSTRUCTOR/UIDENT/g' *
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
29a961f786 Puns 2022-12-19 13:03:19 +01:00
Louis Gesbert
b9cc89ebb5 Switch the parser to "new" menhir syntax 2022-12-19 13:03:19 +01:00
Louis Gesbert
19f6d3d352 Add a notice on overload rules
Overloads are powerful, but let's clearly draw the line right now between
convenience and type safety, for when someone else will want to add new
operators.
2022-12-19 13:03:16 +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
9b939d07a4 New syntax for collection operations 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
4a66848eb3 Clarify some bits of the overload handling code
and address other remarks from the review of #365
2022-12-13 12:00:05 +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
da1350f581
Simplify unboxing 2022-12-07 17:44:14 +01:00
Denis Merigoux
619461dba8
Merge branch 'master' into fix_362 2022-12-07 15:32:08 +01:00
Denis Merigoux
e9fd40dddd
Hotfix for CI 2022-12-06 18:11:40 +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
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
b3ee503b12 Scopelang.From_desugared: some cleanup/reformat 2022-11-28 16:38:09 +01:00
Louis Gesbert
01957c6698 Desugaring: inline the Fold predicate
the intermediate variable made it much harder to type.
2022-11-28 16:38:09 +01:00
Louis Gesbert
3f2aa19e97 Add ambiguous StructAccess for desugared
to be resolved in scopelang
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
9fc4c0c10c Define Catala_utils.String as an overlay to stdlib string 2022-11-28 16:38:09 +01:00
Louis Gesbert
660e5775de Rename utils to catala_utils 2022-11-28 16:38:09 +01:00
Louis Gesbert
b329afbbdb Rename all Map/Set calls accordingly
This is just a bunch of `sed` calls:
```shell
sed -i 's/ScopeSet/ScopeName.Set/g' compiler/**/*.ml*
sed -i 's/ScopeMap/ScopeName.Map/g' compiler/**/*.ml*
sed -i 's/StructMap/StructName.Map/g' compiler/**/*.ml*
sed -i 's/StructSet/StructName.Set/g' compiler/**/*.ml*
sed -i 's/EnumMap/EnumName.Map/g' compiler/**/*.ml*
sed -i 's/EnumSet/EnumName.Set/g' compiler/**/*.ml*
sed -i 's/StructFieldName/StructField/g' compiler/**/*.ml*
sed -i 's/StructFieldMap/StructField.Map/g' compiler/**/*.ml*
sed -i 's/StructFieldSet/StructField.Set/g' compiler/**/*.ml*
sed -i 's/EnumConstructorMap/EnumConstructor.Map/g' compiler/**/*.ml*
sed -i 's/EnumConstructorSet/EnumConstructor.Set/g' compiler/**/*.ml*
sed -i 's/RuleMap/RuleName.Map/g' compiler/**/*.ml*
sed -i 's/RuleSet/RuleName.Set/g' compiler/**/*.ml*
sed -i 's/LabelMap/LabelName.Map/g' compiler/**/*.ml*
sed -i 's/LabelSet/LabelName.Set/g' compiler/**/*.ml*
sed -i 's/ScopeVarMap/ScopeVar.Map/g' compiler/**/*.ml*
sed -i 's/ScopeVarSet/ScopeVar.Set/g' compiler/**/*.ml*
sed -i 's/SubScopeNameMap/SubScopeName.Map/g' compiler/**/*.ml*
sed -i 's/SubScopeNameSet/SubScopeName.Set/g' compiler/**/*.ml*
```

... and reformat
2022-11-28 16:38:09 +01:00
Louis Gesbert
0030fac7c4 Remove previous set/map definitions 2022-11-28 16:38:09 +01:00
Louis Gesbert
206a24a3e1 Factorise definitions of set and maps for uids 2022-11-28 16:38:09 +01:00
Louis Gesbert
8a4462f6cc Name resolution: small reformatting 2022-11-28 16:38:09 +01:00
Denis Merigoux
d7b9396e87
Correct lines 2022-11-24 15:17:00 +01:00
Louis Gesbert
47799ea24f Uniform naming of conversion modules across compilation passes 2022-11-22 12:08:18 +01:00
Louis Gesbert
4dfb4ab44f Add some more doc for Expr.shallow_fold and Expr.map_gather 2022-11-21 17:54:17 +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
Louis Gesbert
8d7f2152a6 Fill in lambda types when doing type inference 2022-11-17 17:47:24 +01:00
Aymeric Fromherz
1d0871e65c format 2022-11-16 22:28:20 +01:00
Aymeric Fromherz
cfba9d456a Merge branch 'afromher_verif' into afromher_334 2022-11-16 22:16:11 +01:00
Aymeric Fromherz
16c9bae810 cleanup unused var/module errors 2022-11-16 22:13:14 +01:00
Aymeric Fromherz
fe9ef4f8cb Remove map of free_vars_typ from VC generation 2022-11-16 22:08:07 +01:00
Aymeric Fromherz
5a5003b22d Do not pass free_vars to make_context 2022-11-16 21:59:48 +01:00
Aymeric Fromherz
0ccf7da89a Remove ctx_var from Z3 backend context 2022-11-16 21:57:26 +01:00
Aymeric Fromherz
1343f9e1f6 Leverage typed information embedded in expressions to remove uses of the ctx_var map 2022-11-16 21:55:31 +01:00
Aymeric Fromherz
5c19bdc0db Store typ in z3_vars map 2022-11-16 21:52:14 +01:00
Aymeric Fromherz
43fa3ba550 Start removing ctx_var 2022-11-16 21:36:21 +01:00
Aymeric Fromherz
4af44fb519 Add debug info about encoded assertions 2022-11-08 22:25:07 +01:00
Aymeric Fromherz
c4756c485c WIP: Encoding assertions to Z3 2022-11-08 22:09:35 +01:00
Aymeric Fromherz
b443174033 Better handling of assertions in conditions.ml 2022-11-08 22:09:21 +01:00
Aymeric Fromherz
fee9533b87 Add local asserts to each generated vc 2022-11-08 21:51:56 +01:00
Aymeric Fromherz
3c478148e1 Basic infrastructure for collecting assertions 2022-11-08 20:55:40 +01:00
Aymeric Fromherz
5f36bee94f Extend verification_condition with field for assertions in scope 2022-11-08 20:48:43 +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
9e69273141 Location printer: avoid trailing whitespace 2022-11-04 11:24:41 +01:00
Louis Gesbert
3e004551fc Callable scopes: fixes following review 2022-11-03 15:18:51 +01:00
Louis Gesbert
47a1258648 Fix error handling of invalid subscope variable assignments 2022-10-27 11:42:55 +02:00
Louis Gesbert
96b623c724 Subscope calls: fix handling of input variables with multiple states 2022-10-27 11:42:27 +02: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
ac77e791b9 Always enable backtrace recording in debug mode
it's easier than remembering to set OCAMLRUNPARAM=b, and can help debug the
tests (that ignore this variable).
2022-10-25 11:31:06 +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
7267543ca1 Rename Expr.Box.inj to Expr.Box.lift
it is more consistent with the naming of functions in Bindlib.
2022-10-21 15:35:49 +02:00
Louis Gesbert
f9f834e30a Add a helper to fold on expressions 2022-10-21 15:35:49 +02:00
Louis Gesbert
f103fb1ea5 Typing: be strict about no TAny remaining
Ideally we could replace `TAny` by an option on the whole type, and have untyped
/ partially typed / fully typed terms.
2022-10-21 15:26:16 +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
f9de650d62 Magic * 2022-10-07 18:01:04 +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
e925ec1795 Swap boxing and annotations in expressions
This was the only reasonable solution I found to the issue raised
[here](https://github.com/CatalaLang/catala/pull/334#discussion_r987175884).

This was a pretty tedious rewrite, but it should now ensure we are doing things
correctly. As a bonus, the "smart" expression constructors are now used
everywhere to build expressions (so another refactoring like this one should be
much easier) and this makes the code overall feel more
straightforward (`Bindlib.box_apply` or `let+` no longer need to be visible!)

---

Basically, we were using values of type `gexpr box = naked_gexpr marked box`
throughout when (re-)building expressions. This was done 99% of the time by
using `Bindlib.box_apply add_mark naked_e` right after building `naked_e`. In
lots of places, we needed to recover the annotation of this expression later on,
typically to build its parent term (to inherit the position, or build the type).

Since it wasn't always possible to wrap these uses within `box_apply` (esp. as
bindlib boxes aren't a monad), here and there we had to call `Bindlib.unbox`,
just to recover the position or type. This had the very unpleasant effect of
forcing the resolution of the whole box (including applying any stored closures)
to reach the top-level annotation which isn't even dependant on specific
variable bindings. Then, generally, throwing away the result.

Therefore, the change proposed here transforms
- `naked_gexpr marked Bindlib.box` into
- `naked_gexpr Bindlib.box marked` (aliased to `boxed_gexpr` or `gexpr boxed` for
convenience)

This means only
1. not fitting the mark into the box right away when building, and
2. accessing the top-level mark directly without unboxing

The functions for building terms from module `Shared_ast.Expr` could be changed
easily. But then they needed to be consistently used throughout, without
manually building terms through `Bindlib.apply_box` -- which covers most of the
changes in this patch.

`Expr.Box.inj` is provided to swap back to a box, before binding for example.

Additionally, this gives a 40% speedup on `make -C examples pass_all_tests`,
which hints at the amount of unnecessary work we were doing --'
2022-10-07 18:00:23 +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
14f1ebfd0a Reformat 2022-10-04 14:50:37 +02:00
Louis Gesbert
ea114bada2 Fix one more typing mismatch 2022-10-04 14:50:37 +02:00
Louis Gesbert
920b3679df Some more fixes for remaining invalid typing 2022-10-04 14:50:37 +02:00
Louis Gesbert
5da55f1605 Fix some remaining invalid type annots 2022-10-04 14:50:37 +02:00
Louis Gesbert
5bb694c7b8 scope_to_dcalc: fix propagating wrong types
fill with TAny when building non-trivial things instead (in particular the
toplevel scope structure)
2022-10-04 14:50:37 +02:00
Louis Gesbert
0fdefacf7c Add marks to scopelang Call 2022-10-04 14:50:37 +02:00
Louis Gesbert
749810625f Activate double typing 2022-10-04 14:50:37 +02:00
Louis Gesbert
41315dc650 Scopelang: add toplevel mark for convenience
it allows to discriminate typed and non-typed ASTs
2022-10-04 14:50:37 +02:00
Louis Gesbert
9349fb918d Scope: fix getting external body mark 2022-10-04 14:50:37 +02:00
Louis Gesbert
742c4acb3e Expr.make_app: fix assertion to allow for TAny values 2022-10-04 14:50:37 +02:00
Louis Gesbert
e17baac840 Printer: add debug version that doesn't require a context
very handy sometimes...
2022-10-04 14:50:37 +02:00
Louis Gesbert
fd3219a34e Catala driver: re-run the typer after dcalc compilation 2022-10-04 14:50:37 +02:00
Louis Gesbert
0dbc4c8c35 Separate type ordering from scopelang->dcalc transformation
it's now done explicitely from the driver, which allows to do it before typing
and is more consistent; the information was already forwarded to the later
compilation stages separately from the program AST anyway.
2022-10-04 14:50:37 +02:00
Louis Gesbert
ff76d0498f Make the typer use (and check) already existing annotations, if any 2022-10-04 14:50:37 +02:00
Louis Gesbert
76d1c1cc93 Dcalc.Optimization should reasonably preserve types
since it only does reductions while preserving marks. The patch is mostly a
renaming from `pos` to `mark`
2022-10-04 14:50:37 +02:00
Louis Gesbert
4d8bc20fcd Test new typing 2022-10-04 14:50:37 +02:00
Louis Gesbert
3b4b070aaa Fix typing 2022-10-04 14:50:37 +02:00
Louis Gesbert
2955ef3235 Implement typing at the scopelang level 2022-10-04 14:50:37 +02:00
Louis Gesbert
9f7a0f6078 Fix naming error in interface
Hmm I used too much `sed` and overlooked this one
(patch looks big because of reformatting, but it's mostly just `naked_expr`→`expr`)
2022-10-04 14:50:37 +02:00
Louis Gesbert
05f4bb3537 Typing: simplify interface, split code in smaller functions 2022-10-04 14:50:37 +02:00