Commit Graph

240 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
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
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
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
9203e4f7bb Verification: support unboxed defaults 2023-11-27 11:06:33 +01:00
Louis Gesbert
ab6bec390d Adjust plugins and warnings 2023-11-27 11:06:16 +01:00
Louis Gesbert
4910158aea Reformat 2023-09-01 16:24:27 +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
72882f82df Reformat 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
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
Denis Merigoux
5f48e5dac1
Merge branch 'master' into closure_conversion 2023-06-20 11:02:13 +02:00
Louis Gesbert
e224e87f71 Wip support for modules
(first working dynload test with compilation done by manual calls to ocaml)

A few pieces of the puzzle:

* Loading of interfaces only from Catala files
* Registration of toplevel values in modules compiled to OCaml, to allow access
  using dynlink
* Shady conversion from OCaml runtime values to/from Catala expressions, to
  allow interop (ffi) of compiled modules and the interpreter
2023-06-15 17:56:57 +02:00
Denis Merigoux
6962761774
Merge branch 'master' into closure_conversion 2023-06-15 17:56:41 +02:00
Denis Merigoux
57abfbf2c7
Other pattern matching 2023-06-15 16:33:14 +02:00
Aminata-Dev
10d147a8b1 Messages renamed to Message (lighter syntax) 2023-06-13 11:50:56 +02:00
Louis Gesbert
16c93fbb0c Reformat 2023-06-08 12:14:11 +02:00
Louis Gesbert
deaf40761e Use ocolor instead of ANSITerminal 2023-06-08 12:11:55 +02:00
Denis Merigoux
ddee094783
Fix CI 2023-06-02 15:41:27 +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
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
0338418a6f
Allow use of if_then_else beyond booleans in proof backend (#460) 2023-04-24 17:33:15 +02:00
Aymeric Fromherz
c6e478c9dd [Proof Backend] Use Z3's native encoding for ite 2023-04-24 12:11:55 +02:00
Denis Merigoux
1bb338526d
Generalized optimizations 2023-04-21 11:56:07 +02:00
Louis Gesbert
0098f00512 Yet some more small improvements to the AST encoding 2023-04-05 10:32:58 +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
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
Denis Merigoux
04629f58cd
Merge branch 'master' into aides_logement_outre_mer 2023-03-30 15:14:06 +02:00
Aymeric Fromherz
5f04e0efaf cleanup 2023-03-28 13:08:24 +09:00
Aymeric Fromherz
c711b0b1d7 cleanup 2023-03-28 13:00:07 +09:00
Aymeric Fromherz
082caae498 Add support for let_in in Z3 backend 2023-03-28 12:48:44 +09:00
Denis Merigoux
7f705beb07
Merge branch 'master' into aides_logement_outre_mer 2023-03-17 17:52:10 +01:00
Raphaël Monat
7021c41f93 Add date rounding option within scopes 2023-03-16 16:55:55 +01:00
Denis Merigoux
0667e3d40f
Merge branch 'master' into aides_logement_outre_mer 2023-02-28 15:01:31 +01:00
adelaett
839a7ffd83 finished refactoring 2023-02-20 17:58:29 +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