Commit Graph

324 Commits

Author SHA1 Message Date
Louis Gesbert
2f2614c508 Use the AST mapper for scopelang-> dcalc 2023-06-15 17:55:52 +02:00
Aminata-Dev
10d147a8b1 Messages renamed to Message (lighter syntax) 2023-06-13 11:50:56 +02:00
Denis Merigoux
91ee1122f6 Last typo 2023-06-03 15:32:38 +02:00
Denis Merigoux
79801292e9
Fix most doc errors 2023-06-02 17:17:45 +02:00
Denis Merigoux
d1210cc0e4 The thing compiles 2023-06-02 10:50:33 +02:00
Denis Merigoux
4e6efe08da All renamings done, on with actual refactor 2023-06-02 10:50:33 +02:00
Denis Merigoux
0faa97b8fc Abstract messages interface 2023-06-02 10:50:29 +02:00
Denis Merigoux
8987d358e7
Implement the rest 2023-05-26 16:54:52 +02:00
Denis Merigoux
1f23f701bc
Move types 2023-05-26 16:03:26 +02:00
Louis Gesbert
209be6b758 Improve integration of marks into the main AST
Two interdependent changes here:
1. Enforce all instances of Shared_ast.gexpr to use the generic type for marks.
   This makes the interfaces a tad simpler to manipulate: you now write
   `('a, 'm) gexpr` rather than `('a, 'm mark) gexpr`.
2. Define a polymorphic `Custom` mark case for use by pass-specific annotations.
   And leverage this in the typing module
2023-05-17 17:37:00 +02:00
Louis Gesbert
fc531777c0 Rework and normalise the Marked interface
The module is renamed to `Mark`, and functions renamed to avoid redundancy:

`Marked.mark` is now `Mark.add`
`Marked.unmark` is now `Mark.remove`
`Marked.map_under_mark` is now simply `Mark.map`
etc.

`Marked.same_mark_as` is replaced by `Mark.copy`, but with the arguments
swapped (which seemed more convenient throughout)

Since a type `Mark.t` would indicate a mark, and to avoid confusion, the type
`Marked.t` is renamed to `Mark.ed` as a shorthand for `Mark.marked` ; this part
can easily be removed if that's too much quirkiness.
2023-05-17 17:37:00 +02:00
Louis Gesbert
558fcb6fef Build: remove unnecessary ppx on dcalc, lcalc
we only use `visitors` for positions on the surface AST
2023-05-17 14:08:32 +02:00
Louis Gesbert
5e26c5c83d Yet more printer improvements
- Fix the printer for scopes
- Improve the printer for struct types
- Remove `Print.expr'`. Use `Expr.format` as the function with simplified arguments instead.
2023-05-02 16:33:23 +02:00
Louis Gesbert
83e7a845fe Cleanup expr printer interface
- `Print.expr` no longer needs the context
- This removes the need for `expr ~debug` + `expr_debug` ;
  use `Print.expr` for normal (non-debug) output,
  and `Print.expr' ?debug ()` for possibly debug output.
- This improves consistency of debug expr output in many places
- Prints simplified operators (without type suffix) in non-verbose mode

(this patch also fixes some cases of `Expr.skip_wrappers` and leverages the
binder equality provided by Bindlib)
2023-05-02 13:32:16 +02:00
Denis Merigoux
1bb338526d
Generalized optimizations 2023-04-21 11:56:07 +02:00
Denis Merigoux
f9a6644da3
Cleanliness and aesthetics 2023-04-18 15:45:30 +02:00
adelaett
abc30e1612
handling invariants checking differently in the main driver 2023-04-14 12:01:16 +02:00
adelaett
cfc1d86e96
Revert "incorrect simplification"
This reverts commit 3233ff108f.
2023-04-14 11:51:02 +02:00
adelaett
3233ff108f
incorrect simplification 2023-04-14 11:48:19 +02:00
adelaett
3e35d4b826
Merge branch 'master' into adelaett-withoutexceptionsfix 2023-04-11 11:49:22 +02:00
adelaett
12d85570e8 fix printing boxes & merge issues 2023-04-07 10:51:21 +02:00
alain
ec40de83fc
Merge branch 'master' into adelaett-withoutexceptionsfix 2023-04-06 13:57:22 +02:00
adelaett
68e0f0a0ee changing position of the interpreter 2023-04-05 10:32:52 +02:00
adelaett
8ef3db005f clean deadcode 2023-04-04 15:56:49 +02:00
Denis Merigoux
ad02a0959d
Merge branch 'master' into aides_logement_outre_mer 2023-04-03 14:12:10 +02:00
adelaett
84548769b4 renable optimization since the behavior of ite is now different 2023-04-03 10:56:44 +02:00
adelaett
cc1c018818 trace flag when needed 2023-04-03 10:56:13 +02:00
adelaett
2a50a06b36 invariant mli 2023-04-03 10:38:33 +02:00
adelaett
380a3a0c92 structural invariants 2023-03-31 16:03:51 +02:00
adelaett
e9ead93f3f fix typing errors 2023-03-31 16:01:05 +02:00
adelaett
573df8416f Merge branch 'master' into adelaett-withoutexceptionsfix 2023-03-31 15:52:06 +02:00
Louis Gesbert
1208744c6b EmptyError is no longer a literal
it's much simpler to handle it as an AST node, as that makes the literal
identical across all AST passes.
2023-03-30 18:54:50 +02:00
Louis Gesbert
4973c74410 Remove date rounding mode from Operator.translate 2023-03-30 15:33:00 +02:00
Louis Gesbert
a415355a39 Rework the AST Gadt to allow merging of different ASTs
The phantom polymorphic variant qualifying AST nodes is reversed:
- previously, we were explicitely restricting each AST node to the passes where it belonged using a closed type (e.g. `[< dcalc | lcalc]`)
- now, each node instead declares the "feature" it provides using an open type (e.g. `[> 'Exceptions ]`)
- then the AST for a specific pass limits the features it allows with a closed type

The result is that you can mix and match all features if you wish,
even if the result is not a valid AST for any given pass. More
interestingly, it's now easier to write a function that works on
different ASTs at once (it's the inferred default if you don't write a
type restriction).

The opportunity was also taken to simplify the encoding of the
operators, which don't need a second type parameter anymore.
2023-03-30 15:30:08 +02:00
adelaett
6dee3874cc Merge branch 'master' into adelaett-withoutexceptionsfix 2023-03-30 10:50:32 +02:00
adelaett
256adcae4b rename invariant 2023-03-21 14:31:21 +01:00
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
51ea9d8cff Format code 2023-03-16 17:20:14 +01:00
Raphaël Monat
1e1e3b538e Simplify format 2023-03-16 17:20:13 +01:00
Raphaël Monat
887ec00d0e Add explicit match 2023-03-16 17:20:13 +01:00
adelaett
82af9e8305 unfolding more bugs 2023-03-16 17:14:33 +01:00
Raphaël Monat
7021c41f93 Add date rounding option within scopes 2023-03-16 16:55:55 +01:00
adelaett
366a0d952b introducing new operators for handleing defaults 2023-03-14 18:30:58 +01:00
Denis Merigoux
74df4ee988
Merge branch 'master' into aides_logement_outre_mer 2023-03-14 14:10:09 +01:00
adelaett
1580272d7f more precise invariant 2023-03-10 15:32:42 +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
6c0e04942f corrected iota optimization 2023-03-06 16:00:41 +01:00
adelaett
78f121b44a before any issues with mark on code_item 2023-03-03 11:39:55 +01:00
Denis Merigoux
0667e3d40f
Merge branch 'master' into aides_logement_outre_mer 2023-02-28 15:01:31 +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
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
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
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
b512dc6ec7 Fix List.combine internal error (create multiple TAny instead of only one) 2023-02-21 14:16:50 +01:00
adelaett
839a7ffd83 finished refactoring 2023-02-20 17:58:29 +01:00
Louis Gesbert
72cf477dd9 Toplevel definitions: fixes following review
Thanks @denismerigoux!
2023-02-15 12:40:15 +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
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
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
ec6616c091
Changing encoding of direct scope call to avoid empty error confusing static analysis 2023-01-20 15:23:50 -05:00
Denis Merigoux
5fb9031c8a
Fixing review comments 2023-01-11 10:42:21 +01:00
Denis Merigoux
2f4a51ce64
Bug fixed! It was tricky 2023-01-07 20:22:36 +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
Louis Gesbert
51df581aba Small cleanup/fixes following PR review on Syntax Changes 2022-12-20 16:03:41 +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
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
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
e448a1a1b4
Fix 362 (was harder than expected and unit tests helped catch subsequent encoding bugs!) 2022-12-02 16:42:29 +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
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
47799ea24f Uniform naming of conversion modules across compilation passes 2022-11-22 12:08:18 +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
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
14f1ebfd0a Reformat 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
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
b37a6c3703 Generalise the typer
This moves dcalc/typing.ml to shared_ast, and generalises the input type, but
without yet implementing the extra cases (these are all `assert false`): it's
just a first step.
2022-10-04 14:50:37 +02:00
Louis Gesbert
0bb9cce341 Simplify a few mark operations 2022-10-04 14:50:37 +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
c18de3b980 Tweak the order in which typing is done 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
Denis Merigoux
01e333b833
Use dates_calc library (#306)
This is a WIP. Current version 0.0.2 of `dates_calc` is in the process of being published, so I guess the CI should fail currently.

- [x] Test current implementation
- [x] I commented out the `duration / duration` operator, can we remove it?
- [x] Need to add support for first and last day of month
- [x] Finish porting the Z3 backend to dates_calc
2022-09-05 15:57:08 +02:00