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 8e1a1ccb634812830a25
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
