Commit Graph

235 Commits

Author SHA1 Message Date
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
Louis Gesbert
0540cd31fe Allow ETuple, ETupleAccess on all ASTs
they used to be only allowed on lcalc
2023-02-13 10:51:42 +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
f236e2cfb2 Replace the type conversion and rounding operators with overloads
Ref. #366

Also updates `CONTRIBUTING.md`.

This was pretty straight-forward :)
2022-12-13 15:32:49 +01:00