Commit Graph

267 Commits

Author SHA1 Message Date
Denis Merigoux
aa8ab3be3d
Merge branch 'master' into c_backend 2023-03-21 12:14:10 +01:00
adelaett
82af9e8305 unfolding more bugs 2023-03-16 17:14:33 +01:00
Louis Gesbert
abc5a00c2f Compile LaTeX code using minted without the Python venv
This is a hack, but not a dirty one: a new command `catala pygmentize` is added,
which is just a wrapper around `pygmentize` that calls it with the proper lexers
defined.

The point is that this needs no installation, just a stock `pygmentize`
installation and the `catala` binary.
2023-03-14 17:35:22 +01:00
adelaett
4d3b021eef finished the implementation, but a few issues are missing 2023-03-13 16:51:06 +01:00
Louis Gesbert
508992de33 Embed the Pygments Catala lexer
This enables the HTML output to work without a custom Pygments installation (or
the proper venv activated)
2023-03-13 14:41:24 +01:00
adelaett
6c0e04942f corrected iota optimization 2023-03-06 16:00:41 +01:00
adelaett
2ae2ff7d50 adding a non-passing invariant 2023-02-28 08:36:34 +01:00
adelaett
9ec2b7785d more work on invariants 2023-02-27 11:20:59 +01:00
adelaett
382150b513 new invariant option when launching the compiler 2023-02-27 11:20:59 +01:00
Louis Gesbert
03645e6404 Rename Scalc from_lambda to from_lcalc for consistency 2023-02-17 19:49:56 +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
912e1500c4 Handle toplevel defs down to scalc 2023-02-13 11:44:32 +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
7702949401
Better printing 2023-02-08 16:03:23 +01:00
Denis Merigoux
c78a004b53
Leave everything unresolved for now 2023-02-08 16:00:53 +01:00
Denis Merigoux
e7d1fb84e9
Trying to retype closure conversion but fails [skip-ci] 2023-02-08 16:00:20 +01:00
Denis Merigoux
38d5ef9715
Small improvement 2023-02-08 15:59:51 +01:00
Denis Merigoux
83e9e83909
Progressing [skip ci]
Testing with dune exec catala -- Lcalc -s S tests/test_func/good/closure_conversion.catala_en  --avoid_exceptions -O --closure_conversion
2023-02-08 15:59:51 +01:00
Louis Gesbert
467a338b6c Install Catala plugins
Fixes #378

- the plugins are compiled as libraries rather than with `executable`, so that
  dune is able to install them
- they get installed to `lib/catala/plugins/<plugin-name>/<plugin-name>.cmxs`
- the lookup for plugins is now recursive to cope with the plugin subdirectories
  in the point above
2023-01-17 14:38:09 +01:00
Denis Merigoux
2f4a51ce64
Bug fixed! It was tricky 2023-01-07 20:22:36 +01:00
Denis Merigoux
9d619a26ba
Correct cli typecheck behavior 2023-01-05 18:56:19 +01:00
Louis Gesbert
8960e5dbbc Add typing-based disambiguation pass after desugaring
Some typing errors are changed a little, because they get triggered during the
typing of the disambiguation pass, which does not specify the expected return
type (it's an expected invariant that it should not be needed for
disambiguation).

It would be possible to still specify these types during disambiguation just to
get the same errors, but since the newer ones don't appear to be clearly worse
at the moment, it has not been done.
2022-11-28 16:38:09 +01:00
Louis Gesbert
3f2aa19e97 Add ambiguous StructAccess for desugared
to be resolved in scopelang
2022-11-28 16:38:09 +01:00
Louis Gesbert
660e5775de Rename utils to catala_utils 2022-11-28 16:38:09 +01:00
Louis Gesbert
b329afbbdb Rename all Map/Set calls accordingly
This is just a bunch of `sed` calls:
```shell
sed -i 's/ScopeSet/ScopeName.Set/g' compiler/**/*.ml*
sed -i 's/ScopeMap/ScopeName.Map/g' compiler/**/*.ml*
sed -i 's/StructMap/StructName.Map/g' compiler/**/*.ml*
sed -i 's/StructSet/StructName.Set/g' compiler/**/*.ml*
sed -i 's/EnumMap/EnumName.Map/g' compiler/**/*.ml*
sed -i 's/EnumSet/EnumName.Set/g' compiler/**/*.ml*
sed -i 's/StructFieldName/StructField/g' compiler/**/*.ml*
sed -i 's/StructFieldMap/StructField.Map/g' compiler/**/*.ml*
sed -i 's/StructFieldSet/StructField.Set/g' compiler/**/*.ml*
sed -i 's/EnumConstructorMap/EnumConstructor.Map/g' compiler/**/*.ml*
sed -i 's/EnumConstructorSet/EnumConstructor.Set/g' compiler/**/*.ml*
sed -i 's/RuleMap/RuleName.Map/g' compiler/**/*.ml*
sed -i 's/RuleSet/RuleName.Set/g' compiler/**/*.ml*
sed -i 's/LabelMap/LabelName.Map/g' compiler/**/*.ml*
sed -i 's/LabelSet/LabelName.Set/g' compiler/**/*.ml*
sed -i 's/ScopeVarMap/ScopeVar.Map/g' compiler/**/*.ml*
sed -i 's/ScopeVarSet/ScopeVar.Set/g' compiler/**/*.ml*
sed -i 's/SubScopeNameMap/SubScopeName.Map/g' compiler/**/*.ml*
sed -i 's/SubScopeNameSet/SubScopeName.Set/g' compiler/**/*.ml*
```

... and reformat
2022-11-28 16:38:09 +01:00
Louis Gesbert
47799ea24f Uniform naming of conversion modules across compilation passes 2022-11-22 12:08:18 +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
Louis Gesbert
ac77e791b9 Always enable backtrace recording in debug mode
it's easier than remembering to set OCAMLRUNPARAM=b, and can help debug the
tests (that ignore this variable).
2022-10-25 11:31:06 +02:00
Louis Gesbert
41d6d3cbe9 Make scopes directly callable
Quite a few changes are included here, some of which have some extra
implications visible in the language:

- adds the `Scope of { -- input_v: value; ... }` construct in the language

- handle it down the pipeline:
  * `ScopeCall` in the surface AST
  * `EScopeCall` in desugared and scopelang
  * expressions are now traversed to detect dependencies between scopes
  * transformed into a normal function call in dcalc

- defining a scope now implicitely defines a structure with the same name, with
  the output variables of the scope defined as fields. This allows us to type
  the return value from a scope call and access its fields easily.
  * the implications are mostly in surface/name_resolution.ml code-wise
  * the `Scope_out` struct that was defined in scope_to_dcalc is no longer
    needed/used and the fields are no longer renamed (changes some outputs; the
    explicit suffix for variables with multiple states is ignored as well)
  * one benefit is that disambiguation works just like for structures when there
    are conflicts on field names
  * however, it's now a conflict if a scope and a structure have the same
    name (side-note: issues with conflicting enum / struct names or scope
    variables / subscope names were silent and are now properly reported)

- you can consequently use scope names as types for variables as well. Writing
  literals is not allowed though, they can only be obtained by calling the
  scope.

Remaining TODOs:

- context variables are not handled properly at the moment

- error handling on invalid calls

- tests show a small error message regression; lots of examples will need
  tweaking to avoid scope/struct name or struct fields / output variable
  conflicts

- add a `->` syntax to make struct field access distinct from scope output var
  access, enforced with typing. This is expected to reduce confusion of users
  and add a little typing precision.

- document the new syntax & implications (tutorial, cheat-sheet)

- a consequence of the changes is that subscope variables also can now be typed.
  A possible future evolution / simplification would be to rewrite subscopes as
  explicit scope calls early in the pipeline. That could also allow to manipulate
  them as expressions (bind them in let-ins, return them...)
2022-10-21 17:17:26 +02: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
6c8a9f830c Compute the Dcalc stage when running catala Typecheck
it has some important resolution/sanity checks
2022-10-07 17:41:27 +02:00
Louis Gesbert
920b3679df Some more fixes for remaining invalid typing 2022-10-04 14:50:37 +02:00
Louis Gesbert
749810625f Activate double typing 2022-10-04 14:50:37 +02:00
Louis Gesbert
fd3219a34e Catala driver: re-run the typer after dcalc compilation 2022-10-04 14:50:37 +02:00
Louis Gesbert
0dbc4c8c35 Separate type ordering from scopelang->dcalc transformation
it's now done explicitely from the driver, which allows to do it before typing
and is more consistent; the information was already forwarded to the later
compilation stages separately from the program AST anyway.
2022-10-04 14:50:37 +02:00
Louis Gesbert
4d8bc20fcd Test new typing 2022-10-04 14:50:37 +02:00
Louis Gesbert
05f4bb3537 Typing: simplify interface, split code in smaller functions 2022-10-04 14:50:37 +02:00
Louis Gesbert
af9f497ffb Implement typing of desugared/scopelang and lcalc terms
Note that this is incomplete in the case of desugared/scopelang because we only
have typing for expressions yet, and the scope/program structure is different.

The code allows passing an environment of types for scope/subscope variables in
order to resolve `ELocation` terms, but that's unused until we implement
scopelang typing at the scope level.
2022-10-04 14:50:37 +02:00
Louis Gesbert
b37a6c3703 Generalise the typer
This moves dcalc/typing.ml to shared_ast, and generalises the input type, but
without yet implementing the extra cases (these are all `assert false`): it's
just a first step.
2022-10-04 14:50:37 +02:00
Louis Gesbert
01cc957b3b Used shared_ast for scopelang expressions 2022-08-26 11:31:14 +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
8e7f65d204 Split Shared_ast.Expr of scope and program functions 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
Emile Rolley
ba620fca28 ocamlformat: new break-infix rule 2022-08-05 10:55:48 +02:00
Emile Rolley
2da94b88c2 fix(compiler): use Plugin.extension instead of the hardcoded ".ml" one 2022-08-01 10:28:38 +02:00
Emile Rolley
1a6934b538 feat(build): add the generation of json schemas to the build workflow 2022-07-29 18:47:42 +02:00
Emile Rolley
21af0c8c04 refactor(compiler): split web plugin into api_web and json_schema + factorize some util functions 2022-07-29 18:42:47 +02:00
Emile Rolley
6ce6ea8afc refactor(plugins): add scope as argument for the apply function 2022-07-29 18:42:41 +02:00
Denis Merigoux
522deb50c2
Factorizing Dcalc.program 2022-07-22 15:49:57 +02:00
Louis Gesbert
83de1a229b Mark the optimization passes as untyped
It's not expected to stay that way forever, but some additional effort will be required for them to preserve (or restore) types; until then, be safe and don't forward possibly incorrect information.
2022-07-13 12:17:43 +02:00
Louis Gesbert
49efb5ddd7 Improve debugging, add backtraces (when recording is enabled) 2022-07-11 17:42:34 +02:00
Louis Gesbert
67179a793c Add type annotations on all AST nodes (first pass) 2022-07-11 16:51:54 +02:00
Denis Merigoux
66a7d2f7a3 Fix test encoding 2022-07-08 15:37:01 +02:00
Denis Merigoux
ec225994af
Add "print_only_law" option 2022-05-26 19:05:06 +02:00
Louis Gesbert
9a95a3554c Add support for backend plugins using dynlink 2022-05-19 10:40:02 +02:00
Emile Rolley
144704f7fb refactor(compiler): add the Utils.File module
+ Adds wrapper functions for formatter of file/out_channel
	and uses it in both the compiler and the clerk drivers.
2022-05-19 10:04:34 +02:00
Louis Gesbert
f17875f90e Formatting: some other personal preferences 2022-05-11 16:25:49 +02:00
Louis Gesbert
74c5629153 Formatting: reduce extra match-case indentation
2 is plenty enough, esp. for nested matches :)
2022-05-11 16:25:20 +02:00
Louis Gesbert
6837af4e80 Upgrade Cmdliner dep 2022-05-09 11:39:18 +02:00
Denis Merigoux
764edb6ef0
Refactoring finished 2022-04-26 16:06:36 +02:00
Denis Merigoux
e68fe42856
Put closure conversion prototype under a flag 2022-04-04 17:43:30 +02:00
Denis Merigoux
7ca5ef283a
Code builds but bugguy [skip ci] 2022-04-04 08:56:48 +02:00
Denis Merigoux
2652b9c406
Continuing to adapt code to new binded representation [skip ci] 2022-04-02 14:51:11 +02:00
Denis Merigoux
a660987df0
Starting to implement closure conversion [skip ci] 2022-03-21 17:26:23 +01:00
Denis Merigoux
a7bdc0a114
Add condition for focusing the proof mode on a single scope 2022-03-17 17:44:24 +01:00
Denis Merigoux
bba5e3afea
Only print logging in Scopelang if debug 2022-03-16 12:00:36 +01:00
Denis Merigoux
c59451751b
Fix logging operator location for default justifications 2022-03-16 11:44:34 +01:00
Denis Merigoux
41cf1ec0e6
Merge pull request #222 from CatalaLang/refactor-catala_backend_option-functions
Refactor: group common functions related to backend_option in the Cli module
2022-03-09 11:12:01 +01:00
Louis Gesbert
b4b6d5d648 Fix compilation catala_web_interpreter
oops I overlooked that one
2022-03-08 17:35:57 +01:00
Louis Gesbert
729fb7e551 reformat (sync with master) 2022-03-08 16:12:25 +01:00
Louis Gesbert
071ec35234 Command-line: use a record for the options
Should make it much easier and less error-prone to add new options. There is
still a bit of boiler-plate, but at least it's contained in the Cli.options
function and doesn't transpire in the interfaces.
2022-03-08 16:11:39 +01:00
Emile Rolley
7c1f4cc02d refactor: group common functions related to backend_option in the Cli module 2022-03-08 15:52:26 +01:00
Denis Merigoux
5bd66142a6
Big reformatting
ocamlformat 0.19.0 -> 0.20.1
100 -> 80 columns per line
Reestablished @emilerolley's smart fun break
2022-03-08 15:03:14 +01:00
Louis Gesbert
12ec65601d Use format strings directly in debug/error/log functions
This avoids many intermediate calls to e.g. `Format.asprintf`; should result in
some cases in "more correct" use of `Format`¹, avoid the computation of unused
debug strings, and make the code more readable.

¹ for `Format` to work as expected, all intermediate calls need to go through
it. Some cases of formatting to an intermediate string then printing through Format
again are still present, but this makes the situation better.
2022-03-08 13:04:27 +01:00
Denis Merigoux
c65c38a2d5
Correct flag for enabling optimization 2022-02-24 16:46:02 +01:00
Denis Merigoux
756e7cb9b2
Merge branch 'master' into alain_default-option 2022-02-24 16:41:35 +01:00
Alain
73fe2f876c Revert "Merge pull request #196 from CatalaLang/fixup-cmdliner"
fix cmdliner to 1.0.4

This reverts commit 8e1a1ccb63, reversing
changes made to 4812830a25.
2022-02-21 14:53:48 +01:00
Denis Merigoux
cab4e5c17e
Merge branch 'master' into alain_default-option 2022-02-15 10:20:53 +01:00
Denis Merigoux
1cec4b0721
Pretty-printer for scalc 2022-02-14 18:22:26 +01:00
Denis Merigoux
b25f64c3ae
Improve printing 2022-02-14 17:01:34 +01:00
Denis Merigoux
69a7465339
Merge branch 'master' into alain_default-option 2022-02-14 12:09:11 +01:00
Denis Merigoux
e1dc36f1b1
Merge branch 'master' into io-qualifiers-112-part-2 2022-02-10 22:59:37 +01:00
Denis Merigoux
b6d9d7cf5f
Update Cmdliner with breaking changes 2022-02-10 22:57:07 +01:00
Denis Merigoux
30061b8c86
Better encoding of inputs [skip ci] 2022-02-09 11:37:52 +01:00
Denis Merigoux
97f8875a39
Merge branch 'master' into alain_default-option 2022-02-04 15:35:52 +01:00
Denis Merigoux
6cf1b768d2
Fix bug in Python backend producing unreachable code 2022-02-01 15:41:53 +01:00
Denis Merigoux
edeba14692
Just typechecking for compiler 2022-01-31 15:28:19 +01:00
Denis Merigoux
5e253ba321
Disabling exact counterexamples values from CI testing because of randomness 2022-01-26 16:24:09 +01:00
Denis Merigoux
b11e3329b3
Functorize VC solving IO [skip ci] 2022-01-18 18:51:02 +01:00
Denis Merigoux
d705334d9e
Merge branch 'master' into proof_platform 2022-01-11 15:43:33 +01:00
Denis Merigoux
2b6e7c8b98
Working prototype of clerk, the new build system for Catala 2022-01-10 17:57:58 +01:00
Aymeric Fromherz
a9ebfaed38 Pass program to z3encoder 2022-01-10 14:36:15 +01:00
Denis Merigoux
4082e5056e
More prettier things 2022-01-10 10:59:30 +01:00
Denis Merigoux
3a864b6160
Aesthetic improvements 2022-01-10 10:28:14 +01:00
Denis Merigoux
743a1b74c9
Renamed and grouped modules cleanly 2022-01-08 18:37:04 +01:00
Denis Merigoux
546107bfb0
Merge branch 'proof_platform' of github.com:CatalaLang/catala into proof_platform 2022-01-07 18:37:30 +01:00
Denis Merigoux
50224851f5
Port optimizations to Dcalc 2022-01-07 18:36:56 +01:00
Aymeric Fromherz
1105858bea Setting up the pipeline for encoding VCs to Z3 2022-01-07 17:50:45 +01:00
Denis Merigoux
75ef1ef70f
Added proof of concept of verification condition generation 2022-01-07 12:04:31 +01:00
Emile Rolley
397b0e1d7c fix(build/doc): remove warnings due to .ml* files 2022-01-02 14:53:51 +01:00
Alain
16b0dba9d0 Merge branch 'master' into feat/default-option 2021-12-14 10:27:11 +01:00
Denis Merigoux
9f0929b86d
Fix the final bug! 2021-12-10 17:55:24 +01:00
Denis Merigoux
f16ebf8b8b
Removed optimizations, just one weird bug missing [skip ci] 2021-12-10 17:23:14 +01:00
Denis Merigoux
00a998462a
Implementation OK, now on to debugging Bindlib [skip ci] 2021-12-10 16:30:36 +01:00
Denis Merigoux
50400c445d
Few progress 2021-12-09 23:29:49 +01:00
Denis Merigoux
c456a62cb3
Builds but with empty stubs [skip ci] 2021-12-09 22:59:39 +01:00
Denis Merigoux
7d3e381d45
Improvements with Alain during weekly meeting 2021-11-24 15:51:49 +01:00
Alain
f75341c44f making options default compilation target 2021-11-22 15:55:21 +01:00
Denis Merigoux
b56299f3d3
Switch ocamlformat to 0.19.0 2021-08-19 11:35:56 +02:00
Denis Merigoux
817b1785df
Python translation working but still buggy 2021-06-24 17:50:08 +02:00
Denis Merigoux
eb9c75f394
Making progress into translation 2021-06-23 17:47:34 +02:00
Denis Merigoux
1313183353
Defining a new intermediate representation 2021-06-22 16:01:57 +02:00
Denis Merigoux
fffd0ffb63
Working the way into the Python backend 2021-06-22 14:55:43 +02:00
Denis Merigoux
9ab32efcce
Added machinery for Python backend 2021-06-21 18:00:06 +02:00
Denis Merigoux
bbd50747d9
Big renaming and dir reorg 2021-06-21 11:39:06 +02:00