Commit Graph

326 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
vbot
2b8d6676d5
Scopelang: add list of definitions's positions to scope var def 2024-07-17 18:03:23 +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
Denis Merigoux
1e76366f51
Fix extra_pos/pos 2024-04-12 17:06:44 +02:00
Louis Gesbert
def10e7f98 Message: further simplification 2024-04-10 19:26:23 +02:00
Louis Gesbert
98fc97a241 Rewriting message calls to use the new intf 2024-04-10 19:26:23 +02:00
Louis Gesbert
75bf768264 Reformat 2024-04-04 10:56:56 +02:00
Louis Gesbert
0ec04c4925 Branch cleanup and test outputs update
Lots of tests have a new warning because they were calling subscopes without
using their outputs. A better solution could be to mark these subscopes as
`output`, now that it's possible !
2024-04-04 10:55:21 +02:00
Louis Gesbert
f151a9a794 Wip: handling subscope calls as normal definitions
- for the moment we still have specific vars for subscope inputs (in scopelang)
- this causes trouble with default-embedding of scope calls
2024-04-04 10:24:18 +02:00
Louis Gesbert
4eeb8221f4 Fix var bindings in desugared->scopelang 2024-04-04 10:24:18 +02:00
Louis Gesbert
7951661981 Turn subscope-vars into scope vars
They are to become citizens of the same class if we want to allow
output-subscopes (without unnecessary complications like deconstructing and
reconstructing the same structure). And it's reasonable to assume that they
share the same namespace.

With this we should shortly collapse the (internal) ambiguity between

- `subscope.subvar`: access to a variable within a subscope
- `subscope.subfield`: access to a field of the output structure contained in a
  subscope variable

With the subscope a variable, these should now become strictly equivalent, so
the plan is that the first could be removed.
2024-04-04 10:24:18 +02:00
Louis Gesbert
4cec981f62 Move global options of Cli to their own module
This resolves a dependency cycle that would forbid `Cli` from using the modue
`File`, which was annoying.
2024-03-19 15:18:35 +01:00
Louis Gesbert
e308ff8d02 Generalise the definition of lists of nested binders 2024-02-09 18:33:41 +01:00
Louis Gesbert
870716a3f8 Factorise a bit more with more arguments to Expr.map
allowing a safer way to translate types both in expressions and annotations, and
clarifying the code of the dcalc->lcalc translation
2024-02-05 16:28:56 +01:00
Louis Gesbert
e47a1fc220 Improve translation of typing upon dcalc -> lcalc
A little bit of effort enables us to propagate valid typing annotations, making
subsequent typing re-inference easier (and avoiding a traversal just to remove
type annotations)
2024-01-31 19:15:27 +01:00
Louis Gesbert
a9f8fa36b8 Reduce default verbosity of invariant checks
they break the tests too often for no good reason
2024-01-25 18:18:43 +01:00
Louis Gesbert
12f208b3fc Adding tuples: fixes following review 2024-01-08 12:16:07 +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
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
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
Louis Gesbert
1ae955b504 Reformat 2023-11-30 23:53:38 +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
cc4e5339dd Typed defaults: small simplification and fixes 2023-11-27 11:09:08 +01:00
Louis Gesbert
1efda5ca22 Typing defaults: support nested priorities
The way nested priorities are encoded use `< < excs | true :- nested > :- x >`,
which imply that `nested` can actually be ∅ ; to cope with this, the typing of
default terms is made more generic (the return type is now the same as the
`cons` type `'a`, rather than `<'a>`). For the general case, we add an explicit
`EPureDefault` node which just encapsulates its argument (a `return`, in monad
terminology).
2023-11-27 11:09:08 +01:00
Louis Gesbert
c4715ea86e Reformat 2023-11-27 11:09:08 +01:00
Louis Gesbert
dc3ffa0dcd Fix some error handling on scope calls
(and add suggestions)
2023-11-27 11:06:33 +01:00
Louis Gesbert
958aaebac3 Typing defaults fixes: keep in and out type in scope sigs 2023-11-27 11:06:16 +01:00
Louis Gesbert
0be2636e65 Typing defaults: making the compiler adhere to the new type discipline 2023-11-27 11:06:01 +01:00
Louis Gesbert
2d062a4ad0 Fix bug in dependency analysis around scope call arguments 2023-10-13 16:12:15 +02:00
Louis Gesbert
d09113163d Fix bug in dependency analysis around scope call arguments 2023-10-13 15:09:36 +02:00
Louis Gesbert
61ec34e3d9 Fix handling of context vars with all call cases 2023-10-12 14:47:43 +02:00
Louis Gesbert
af8ff472a5 Fix handing of context variables in modules
The call convention imposes a translation of their types within the scope input
structs definitions in dcalc.
2023-10-12 14:42:57 +02:00
Louis Gesbert
f162f6e9bd Improve handling of module name definitions
and add some sanity-checks for consistency of used modules w.r.t. actually
loaded modules.
2023-09-27 13:14:03 +02:00
Denis Merigoux
9cecf5587a
Register surface syntax languge in program troughout the compilation chain 2023-09-22 18:05:26 +02:00
zapashcanon
97e5b15531
replace let _ by let () or add type annotation 2023-09-09 22:02:39 +02:00
Louis Gesbert
e75ea3da07 Cleanup tmp debug code 2023-08-31 18:31:48 +02:00
Louis Gesbert
8e33355ead Reformat 2023-08-31 18:31:48 +02:00
Louis Gesbert
7db63e5f78 Simplification: store paths in Uids
rather than scattered in structures

The context is still hierarchical for defs though, so one needs to retrieve the
path to lookup in the correct context for info. Exceptions are enums and struct
defs, which are re-exposed at toplevel.
2023-08-31 18:31:48 +02:00
Louis Gesbert
17172cf47d Some fixes & cleanup after early review 2023-08-31 17:55:36 +02:00
Louis Gesbert
72882f82df Reformat 2023-08-31 17:55:36 +02:00
Louis Gesbert
bcde10242f Specialise the Map.Not_found exception raised by Map.find
... and add a custom printer

Since this is a very common bug, this patch should gain us a lot of time when
debugging uncaught Not_found errors, because the element not found can now be
printed straight away without the need for further debugging.

The small cost is that one should remember to catch the correct specialised
`Foo.Map.Not_found _` exception rather than the standard `Not_found` (which
would type-check but not catch the exception). Using `find_opt` should be
preferred anyway.

Note that the other functions from the module `Map` that raise `Not_found` are
not affected ; these functions are `choose`, `min/max_binding`,
`find_first/last` which either take a predicate or fail on the empty map, so it
wouldn't make sense for them (and we probably don't use them much).
2023-08-31 17:55:36 +02:00
Louis Gesbert
9bac045d03 Implement module lookups for scopes, structs, and enums 2023-08-31 17:54:39 +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
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
Louis Gesbert
ec97c386c3 Reformat + regen 2023-06-15 17:57:01 +02:00