Louis Gesbert
e7e89873db
Make Z3 an optional dependency
...
If Catala is compiled without Z3, trying to run it with the backend `Proof` will
yield:
```
[ERROR] This instance of Catala was compiled without Z3 support.
```
and return 124
Note that this doesn't change the `make depends`, opam file or CI to account for it,
it just enables it at the build-system level.
There are also no hooks at this moment to have Catala self-document the options
whith which it was compiled (e.g. in the `--help` screen). But that could be
added in a more general way later, it's probably not really needed yet.
2022-03-08 18:38:42 +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
Denis Merigoux
c07bab1377
FIXME -> TODO
2022-03-08 14:55:48 +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
1a7fb349eb
Merge branch 'master' into variable_state_114
2022-03-07 11:59:49 +01:00
Denis Merigoux
23766e34a9
More negative tests
2022-03-07 11:55:26 +01:00
Denis Merigoux
b9f46afcd7
Revert ocamlformat changes; creates too much conflict in other files
...
Changes in autoformatting should be made in a separate PR in a time where
there isn't too much pending PRs for the OCaml files
2022-03-07 11:09:47 +01:00
Denis Merigoux
8167d7ee00
Simple tests
2022-03-06 17:13:40 +01:00
Emile Rolley
7d12b5f9f1
Merge branch 'master' into refactor-clerk-w-ninja
2022-03-06 15:02:42 +01:00
Denis Merigoux
5ef7e45e11
Desugared to scope complete but untested [skip ci]
2022-03-06 14:15:09 +01:00
Denis Merigoux
cf8c6233d9
Finished translation of expressions [skip ci]
2022-03-01 20:41:01 +01:00
Denis Merigoux
5a0719b25d
Starting to translate expressions [skip ci]
2022-03-01 10:15:44 +01:00
Denis Merigoux
171e8932bc
Desugaring implemented [skip ci]
2022-02-28 18:34:32 +01:00
Denis Merigoux
518ff02696
Added desugared AST, necessary to distinguish Desugared.ScopeVar from Scopelang.ScopeVar [skip ci]
2022-02-28 17:19:39 +01:00
Denis Merigoux
1e11f6c1d5
Name resolution
2022-02-28 15:40:19 +01:00
Denis Merigoux
eb7f00f56d
Syntax: parser and highlighting
2022-02-28 14:33:07 +01:00
Emile Rolley
b0829148c7
format: add break-fun-decl in .ocamlformat
2022-02-26 19:53:56 +01:00
Emile Rolley
3a6450b42f
Merge branch 'master' into refactor-clerk-w-ninja
2022-02-25 12:31:16 +01:00
Denis Merigoux
09dd02c8a0
Python backend works with exceptions avoided
...
Few bugs in Lcalc->Scalc fixed
2022-02-25 12:30:34 +01:00
Denis Merigoux
ddacc94de2
Correct types for make_some and make_none
2022-02-24 16:50:01 +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
Aymeric Fromherz
908be78d32
Merge pull request #205 from CatalaLang/afromher_rationals
...
Add support for rationals in Z3 encoding
2022-02-21 15:44:02 +01:00
Aymeric Fromherz
a463ec7db2
Use Cli.max_prec_digits
2022-02-21 14:54:40 +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
Alain
4ee9b71e00
to_lcalc option type printing
2022-02-21 11:58:26 +01:00
Alain
f7b70b8f19
add typing information to make_none and make_some
2022-02-21 11:55:39 +01:00
Alain
6fe75f3486
fv --> free_vars_set
...
free_vars --> free_vars_list
2022-02-21 11:51:01 +01:00
Aymeric Fromherz
63704324c1
[Z3 Backend] Better error message when function has type TAny
2022-02-19 23:28:04 +01:00
Aymeric Fromherz
31c2adf0f1
Z3 Backend: Extend arithmetic operations to money
2022-02-19 23:18:23 +01:00
Aymeric Fromherz
25ff8c50fb
[Z3 Backend]: Add support for rationals
2022-02-19 01:59:34 +01:00
Alain
d7b9aa9492
fixing if-then-else bug
2022-02-18 16:11:22 +01:00
Alain
5c9996e427
more comment
2022-02-18 15:59:35 +01:00
Alain
4b1f235e6c
util review (bis)
2022-02-18 15:56:36 +01:00
Alain
f54b3b317c
review lcalc
2022-02-18 15:55:37 +01:00
Alain
137fb8c552
util review
2022-02-18 15:54:40 +01:00
Alain
d512b27e2c
fmt
2022-02-18 15:49:23 +01:00
Alain
7e1057c541
review of lcalc
2022-02-18 15:47:54 +01:00
Alain
19bf2d934f
dcalc review
2022-02-18 15:31:52 +01:00
Aymeric Fromherz
dd05e4468b
[Z3backend]: Do not crash when trying to print function model
2022-02-18 00:34:42 +01:00
Aymeric Fromherz
6dec7bfe04
Refactor Z3 print_model: get_const_interp is only usable for non-function expressions
2022-02-18 00:28:36 +01:00
Aymeric Fromherz
d776a10e5f
format
2022-02-17 18:44:40 +01:00
Aymeric Fromherz
378ab4697a
Encode TUnit in Z3
2022-02-17 18:34:30 +01:00
Emile Rolley
351c7346d6
refactor(clerk): factorize functions for building ninja rules
...
+ add "test cases" for Lcalc and Scalc backends.
+ add support for Scalc and Lcalc and sort by alphabetical
order their type declarations.
2022-02-17 16:45:49 +01:00
Denis Merigoux
9fcc79a66f
Fix bug for encoding verification conditions from Dcalc, coming from #189
2022-02-15 17:58:18 +01:00
Denis Merigoux
48f064ccea
Adapt translation to new i/o invariants, bug discovered
2022-02-15 11:38:56 +01:00
Denis Merigoux
cab4e5c17e
Merge branch 'master' into alain_default-option
2022-02-15 10:20:53 +01:00
Denis Merigoux
21c73edfc9
Link to modules in the docs
2022-02-14 18:27:29 +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
