Commit Graph

92 Commits

Author SHA1 Message Date
Denis Merigoux
aa8ab3be3d
Merge branch 'master' into c_backend 2023-03-21 12:14:10 +01:00
adelaett
850a1fdb56 more optimization on fold 2023-03-17 11:34:52 +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
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
576f21f69c Added documentation for encoding constructors in the typing inference 2023-02-22 11:41:21 +01:00
adelaett
d79b8463a6 - [ ] shared_ast 2023-02-20 15:57:42 +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
9b0c7583ec Add top-level definitions
Only handled until before scalc at the moment.
2023-02-13 11:43:49 +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
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
Louis Gesbert
ca7f14e219 formatting fix 2023-01-16 12:10:33 +01:00
Louis Gesbert
9b939d07a4 New syntax for collection operations 2022-12-13 12:30:40 +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
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
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
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
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
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
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
f9de650d62 Magic * 2022-10-07 18:01:04 +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
920b3679df Some more fixes for remaining invalid typing 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
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
Louis Gesbert
0ad51b7aec Unify outermost types first in Typing.top_down
It doesn't actually change the error output much, but is more sound, and allowed
to fix a few quirks in the code.
2022-10-04 14:50:37 +02:00
Louis Gesbert
af9f497ffb Implement typing of desugared/scopelang and lcalc terms
Note that this is incomplete in the case of desugared/scopelang because we only
have typing for expressions yet, and the scope/program structure is different.

The code allows passing an environment of types for scope/subscope variables in
order to resolve `ELocation` terms, but that's unused until we implement
scopelang typing at the scope level.
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