Commit Graph

1333 Commits

Author SHA1 Message Date
Louis Gesbert
c336a7bb62
[WIP] Rehaul CI to run examples and generate artifacts again (#562) 2024-01-19 18:34:24 +01:00
Louis Gesbert
1c2c41b2ff Allow literal scope output structures 2024-01-19 15:43:35 +01:00
Louis Gesbert
c006c3343e Rehaul CI to run examples and generate artifacts again
this requires to fetch catala-examples and french-law from their own repos

Restrict static builds and publication to master
2024-01-18 16:14:27 +01:00
Louis Gesbert
d9a17db4c0 Fix running inline tests
Warning: one of them is broken and was disabled
2024-01-18 16:14:27 +01:00
Louis Gesbert
8ed45c2762
Fixes missing minus sign printing for small negative amounts of money (#560) 2024-01-16 12:21:29 +01:00
Denis Merigoux
15c7691c09
Fixes #555 2024-01-16 11:40:10 +01:00
Denis Merigoux
b616e60c79
Fixes #558 2024-01-16 11:29:45 +01:00
Louis Gesbert
12f208b3fc Adding tuples: fixes following review 2024-01-08 12:16:07 +01:00
Louis Gesbert
d3e7c565a9 Closure conversion: use multiple let-in 2023-12-19 17:30:32 +01:00
Louis Gesbert
5384394a72 Fix typing upon detuplification 2023-12-19 17:30:32 +01:00
Louis Gesbert
a2efc94fd2 Register the option type in ctx when used in lcalc 2023-12-19 17:30:28 +01:00
Louis Gesbert
a1c1a7756f Update invariant tests outputs 2023-12-19 17:27:44 +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
94ebc1b65e Allow deconstruction of tuples using let in 2023-12-19 17:25:44 +01:00
Louis Gesbert
df3ab64fe9 Add tuples to the surface language
No helpers to destruct them at the moment
2023-12-19 17:25:44 +01:00
Louis Gesbert
fb51f58261 Optimise away trivially-true errors-on-empty 2023-12-19 16:10:11 +01:00
Louis Gesbert
ea4e191f27 Add optimisation to skip variable aliasings
This particularly of effect to the code introduced by closure conversion.
2023-12-19 16:07:22 +01:00
Louis Gesbert
7233ec403a Printer: add parens after constructors 2023-12-19 16:07:22 +01:00
Louis Gesbert
ad0afa2f64 Small interpreter optimisation
This is unholy, but we're manually bringing a typing proof so it may be
acceptable...
2023-12-19 16:07:22 +01:00
Louis Gesbert
e123d7eb95 Change type syntax of collection into list of 2023-12-19 15:26:44 +01:00
Louis Gesbert
3779a249db Unify all CLI arguments to use - rather than _
it's more common on UNIXes and the mix was unpleasant.
2023-12-19 15:25:37 +01:00
Denis Merigoux
e6a35f31b6
Fixes #551 2023-12-19 13:39:24 +01:00
Louis Gesbert
5b1462d529 Clerk: allow to include non-yet-existing directories
Useful when you have wide `-I` options that not all targets may depend on.
2023-12-08 13:56:31 +01:00
Louis Gesbert
a988ad473b Fix handling of embedded context through modules
Exceptions raised by the interpreter from within the native modules were not
handled correctly.
2023-12-08 13:56:18 +01:00
Louis Gesbert
509ce9788a
Document and first test for externals (#538) 2023-12-07 16:06:25 +01:00
adelaett
b5e7b297aa
typo fixing 2023-12-07 13:48:46 +01:00
adelaett
9f4a238a4a
Fix error messages for unexpected types.
do not retype the terms in the cases where checking invariant is not mandatory.
2023-12-07 13:45:50 +01:00
adelaett
934ab328ec
invariant checking is now available without printing the ast using the typecheck subprogram 2023-12-07 11:27:14 +01:00
adelaett
e1bda33e07
fmt 2023-12-07 11:27:14 +01:00
adelaett
030705eacd
Make the typing invariant more precise. 2023-12-07 11:27:14 +01:00
adelaett
67e36dcf42
Adding Typing Invariant for TDefault
Added a new type safety invariant to ensure that the type `TDefault` can only appear in certain positions,

* On the left-hand side of an arrow with arity 1, as the type of a scope (for scope calls).
* At the root of the type tree (outside a default).
* On the right-hand side of the arrow at the root of the type (occurs for rentrant variables).

This is crucial to maintain the safety of the type system, as demonstrated in the formal development.

The invariant was checked on all tests cases and on family and housing benefits.

Adjusted inversion invariant about app to handle external objects as well.
2023-12-07 11:27:14 +01:00
Denis Merigoux
2486fbcfb5
Fix LaTeX weaving failing with code blocks (#544) 2023-12-07 11:08:04 +01:00
Denis Merigoux
628cbc4fec
Fix #543 2023-12-06 16:58:38 +01:00
Louis Gesbert
7160093682 Allow scope execution in compiled ocaml executables 2023-12-06 11:06:54 +01:00
Louis Gesbert
54d956823b Some module fixes 2023-12-06 11:06:54 +01:00
Louis Gesbert
9a255522be Document and first test for externals
Also some fixes for Clerk to properly support them
2023-12-06 11:06:54 +01:00
Louis Gesbert
0d5759d99c Allow pre-declarations without an expression for topdefs
it allows for better splitting between metadata and code (even if the type has
to be repeated at the moment)
2023-12-05 16:21:04 +01:00
Louis Gesbert
e689f0c47b Small cleanup and doc on the module handling refactor 2023-12-05 16:01:56 +01:00
Louis Gesbert
1ae955b504 Reformat 2023-11-30 23:53:38 +01:00
Louis Gesbert
8df49dcea2 More tests and some fixes 2023-11-30 23:49:19 +01:00
Louis Gesbert
3649f92975 Rework resolution of module elements
This changes the `decl_ctx` to be toplevel only, with flattened references to
uids for most elements. The module hierarchy, which is still useful in a few
places, is kept separately.

Module names are also changed to UIDs early on, and support for module aliases
has been added (needs testing).

This resolves some issues with lookup, and should be much more robust, as well
as more convenient for most lookups.

The `decl_ctx` was also extended for string ident lookups, which avoids having
to keep the desugared resolution structure available throughout the compilation
chain.
2023-11-30 21:14:12 +01:00
Louis Gesbert
86b7f80e90 Clerk improvements
- Add a `-I` option that allows defined modules to be available from other
  directories

- Add reporting of the number of successful / failed tests

- Locate the project root, and always run the commands from there
2023-11-30 21:14:12 +01:00
Louis Gesbert
c019d1568f Clerk: fix handling of dependency on the catala exec 2023-11-30 17:46:38 +01:00
Louis Gesbert
326ee07f5d Interpreter: handle lcalc with exceptions 2023-11-28 15:02:11 +01:00
Louis Gesbert
4e465d2b48 Printer: some small improvements 2023-11-28 13:37:46 +01:00
Louis Gesbert
447f6d41f1 Interpreter: fix execution with closure_conversion
and context variables
2023-11-28 13:37:46 +01:00
Louis Gesbert
645c263ccc Fix closure-conversion
Joint debugging with @denismerigoux :)
2023-11-28 11:18:41 +01:00
Louis Gesbert
80475ad5ef Printer: show toplevel uids in debug mode
otherwise we had an inconsistency between what's defined at toplevel and what
appears in expressions.
2023-11-28 11:15:01 +01:00
Louis Gesbert
f0d930688e Support closure conversion with disabled typing or optims
This is very useful for debugging
2023-11-28 11:14:48 +01:00
Louis Gesbert
cf89204a4b Reformat 2023-11-27 11:17:38 +01:00