Commit Graph

86 Commits

Author SHA1 Message Date
Louis Gesbert
b9156bb60e Implement safe renaming of idents for backend printing
Previously we had some heuristics in the backends trying to achieve this with a
lot of holes ; this should be much more solid, relying on `Bindlib` to do the
correct renamings.

**Note1**: it's not plugged into the backends other than OCaml at the moment.

**Note2**: the related, obsolete heuristics haven't been cleaned out yet

**Note3**: we conservatively suppose a single namespace at the moment. This is
required for e.g. Python, but it forces vars named like struct fields to be
renamed, which is more verbose in e.g. OCaml. The renaming engine could be
improved to support different namespaces, with a way to select how to route the
different kinds of identifiers into them.

Similarly, customisation for what needs to be uppercase or lowercase is not
available yet.

**Note4**: besides excluding keywords, we should also be careful to exclude (or
namespace):
- the idents used in the runtime (e.g. `o_add_int_int`)
- the dynamically generated idents (e.g. `embed_*`)

**Note5**: module names themselves aren't handled yet. The reason is that they
must be discoverable by the user, and even need to match the filenames, etc. In
other words, imagine that `Mod` is a keyword in the target language. You can't
rename a module called `Mod` to `Mod1` without knowing the whole module context,
because that would destroy the mapping for a module already called `Mod1`.

A reliable solution would be to translate all module names to e.g.
`CatalaModule_*`, which we can assume will never conflict with any built-in, and
forbid idents starting with that prefix. We may also want to restrict their
names to ASCII ? Currently we use a projection, but what if I have two modules
called `Là` and `La` ?
2024-08-28 17:18:26 +02:00
Louis Gesbert
cee8e57d02 More precise positions for operators throughout 2024-04-30 16:35:08 +02:00
Louis Gesbert
9d07015864 Unify runtime error handling
- Clearly distinguish Exceptions from Errors. The only catchable exception
  available in our AST is `EmptyError`, so the corresponding nodes are made less
  generic, and a node `FatalError` is added

- Runtime errors are defined as a specific type in the OCaml runtime, with a
  carrier exception and printing functions. These are used throughout, and
  consistently by the interpreter. They always carry a position, that can be
  converted to be printed with the fancy compiler location printer, or in a
  simpler way from the backends.

- All operators that might be subject to an error take a position as argument,
  in order to print an informative message without relying on backtraces from
  the backend
2024-04-26 18:31:26 +02:00
Louis Gesbert
98fc97a241 Rewriting message calls to use the new intf 2024-04-10 19:26:23 +02:00
Louis Gesbert
afcc435593 CI: fix the check for bad promoted files 2024-02-12 16:44:14 +01:00
Louis Gesbert
721597a70d Small additional simplification 2024-02-12 15:39:29 +01:00
Louis Gesbert
e308ff8d02 Generalise the definition of lists of nested binders 2024-02-09 18:33:41 +01:00
Louis Gesbert
2823795f9f AST change: more specific application
As part of making tuples first-class citizens, expliciting the arity upon
function application was needed (so that a function of two args can
transparently -- in the surface language -- be applied to either two arguments
or a pair).

It was decided to actually explicit the whole type of arguments because the cost
is the same, and this is consistent with lambda definitions.

A related change done here is the replacement of the `EOp` node for operators by
an "operator application" `EAppOp` node, enforcing a pervasive invariant that
operators are always directly applied. This makes matches terser, and highlights
the fact that the treatment of operator application is almost always different
from function application in practice.
2023-12-19 17:27:40 +01:00
Louis Gesbert
9203e4f7bb Verification: support unboxed defaults 2023-11-27 11:06:33 +01:00
Louis Gesbert
4910158aea Reformat 2023-09-01 16:24:27 +02:00
Louis Gesbert
f2fc79f640 Add some helper functions in a wrapper Map module
and use them throughout. No more `List.map fst (Map.bindings m)` !

Also adds some facilities for direct formatting without going through a list.
2023-07-12 11:51:15 +02:00
Louis Gesbert
f9e3964621 Add an explain plugin
Based on the lazy_interp plugin, this new plugin generates a `dot` graph
retracing a given computation from source definitions to the results.
2023-07-11 17:33:56 +02:00
Louis Gesbert
0f9ee2c72e Refacter the main Driver module
- Use separate functions for successive passes in module `Driver.Passes`
- Use other functions for end results printing in module `Driver.Commands`

As a consequence, it is much more flexible to use by plugins or libs and we no
longer need the complex polymorphic variant parameter.

This patch leverages previous changes to use Cmdliner subcommands and
effectively specialises the flags of each Catala subcommand.

Other changes include:

- an attempt to normalise the generic options and reduce the number of global
  references. Some are ok, like `debug` ; some would better be further cleaned up,
  e.g. the ones used by Proof backend were moved to a `Proof.globals` module and
  need discussion. The printer no longer relies on the global languages and prints
  money amounts in an agnostic way.
- the plugin directory is automatically guessed and loaded even in dev setups.
  Plugins are shown by the main `catala` command and listed in `catala --help`
- exception catching at the toplevel has been refactored a bit as well; return
  codes are normalised to follow the manpage and avoid codes >= 128 that are
  generally reserved for shells.

Update tests
2023-07-03 16:42:54 +02:00
Aminata-Dev
10d147a8b1 Messages renamed to Message (lighter syntax) 2023-06-13 11:50:56 +02:00
Denis Merigoux
0faa97b8fc Abstract messages interface 2023-06-02 10:50:29 +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
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
ad02a0959d
Merge branch 'master' into aides_logement_outre_mer 2023-04-03 14:12:10 +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
Denis Merigoux
0667e3d40f
Merge branch 'master' into aides_logement_outre_mer 2023-02-28 15:01:31 +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
21d4360120
Add verification condition special case for scope context arguments 2023-01-20 15:55:28 -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
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
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
660e5775de Rename utils to catala_utils 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
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
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
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
e10771c187
Make all supertypes use ('a, 't) gexpr as parameter instead of naked_gexpr 2022-08-29 10:57:21 +02:00
Louis Gesbert
a9c8bab2b3
Same treatment for typ and marked_typ 2022-08-29 10:57:21 +02:00
Louis Gesbert
0a23dc526d
Rename marked_expr -> expr, expr -> naked_expr throughout
Since the marked kind is used throughout, this should be more clear
2022-08-29 10:57:21 +02:00
Louis Gesbert
4caf828e48 Additional cleanup/fixes on the compiler refactoring
following review ^^
2022-08-23 00:13:02 +02:00
Louis Gesbert
576e0fb3ff Factorise AST printers
Note that there were significant differences between the two printers (see the test diff!). Overall the `dcalc` one seemed newer so that's what I took, with only the required additions from `lcalc` (exceptions, raise and catch)
2022-08-22 19:28:27 +02:00
Louis Gesbert
ae2801be6d Move mode handling code from dcalc to shared_ast
Handling code should now be reasonably well sorted between `Shared_ast.{Var,Expr,Scope,Program}`

The function parameters (e.g. `make_let_in`) could be removed from the
scope handling functions since now the types are compatible, which
makes them much easier to read.
2022-08-22 19:28:27 +02:00
Louis Gesbert
4bb49c14f1 Simplify some type aliases 2022-08-22 19:28:27 +02:00
Louis Gesbert
06dbab74d2 reformat 2022-08-22 19:28:27 +02:00
Louis Gesbert
2b6ee8dd4b Leverage the shared AST: big cleanup (part I) 2022-08-22 19:28:21 +02:00
Louis Gesbert
0b0e774d1c More factorisation, in particular for variables 2022-08-12 17:18:06 +02:00