CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-20 08:47:14 +03:00
Code Issues Projects Releases Wiki Activity
2,602 Commits 41 Branches 8 Tags 60 MiB
429911024c
Commit Graph

718 Commits

Author SHA1 Message Date
Louis Gesbert
fa3693d813 Formatting: disable deprecated "smart" fun-decl option 2022-05-11 16:22:56 +02:00
Louis Gesbert
ac85d8dbb4 Upgrade ocamlformat version 2022-05-11 16:21:58 +02:00
Louis Gesbert
6cb0d581a6 Workaround some ocamlformat crashes 
These files were not reformatted!
 2022-05-11 16:21:07 +02:00
Louis Gesbert
6837af4e80 Upgrade Cmdliner dep 2022-05-09 11:39:18 +02:00
Denis Merigoux
96f1845afd
Merge branch 'master' into allocations_logement 2022-05-08 15:20:04 +02:00
Denis Merigoux
07198e326d
Fixed rounding bug in interpreter for negative values 2022-05-06 15:28:09 +02:00
Denis Merigoux
a52cc0d881
Move fix to lexer as suggested by @altgr 2022-05-06 10:29:39 +02:00
Denis Merigoux
080e60c25d
Fixes money cents parsing 2022-05-05 16:50:33 +02:00
Denis Merigoux
823c223ea8
Restore debug info 2022-05-05 16:28:17 +02:00
Denis Merigoux
025382a85d
Restore debug info 2022-05-05 14:34:29 +02:00
Denis Merigoux
a72944a3ec
Merge branch 'master' into allocations_logement 2022-05-05 14:27:48 +02:00
Denis Merigoux
c7b84ca2d0
Merge pull request #244 from CatalaLang/c_backend 
Bringing structure to the Lcalc AST
 2022-05-05 14:22:26 +02:00
Denis Merigoux
8a0d5d7916
Factoring, nitpicks and updates 2022-05-05 14:01:30 +02:00
Denis Merigoux
dd8956ea01
Use pandoc for HTML 2022-05-05 14:01:09 +02:00
Romain PRIMET
8b53445f8c
update generated catala import instruction 2022-05-05 14:01:09 +02:00
Denis Merigoux
d9da198740
Prettify family benefits 2022-05-05 14:00:44 +02:00
Denis Merigoux
e3e2e6c4e2
Better PDF 2022-05-04 14:01:24 +02:00
Denis Merigoux
1b439a09bd
Better LaTeX beginning [skip ci] 2022-05-02 16:20:39 +02:00
Denis Merigoux
5670546cc8
Fix lines too long 2022-05-02 16:20:39 +02:00
Romain PRIMET
75c67525d3 Merge remote-tracking branch 'upstream/master' into extract_py_runtime 2022-05-02 11:31:43 +02:00
Emile Rolley
ce2c7081b0 refactor(latex): print warning for too long lines + add instruction to compilation 2022-05-01 21:02:36 +02:00
Denis Merigoux
ad7fe6a21a
Use pandoc to prettify a lot the LaTeX document with tables 2022-04-29 23:47:02 +02:00
Denis Merigoux
2254527598
Corrige problème lexing arrondi en français 2022-04-29 21:41:52 +02:00
Denis Merigoux
d08dfb17d2
Corrige problème lexing arrondi en français 2022-04-29 21:41:20 +02:00
Denis Merigoux
aaa6a5d3a6
Merge branch 'master' into allocations_logement 2022-04-29 21:29:07 +02:00
Denis Merigoux
78e8275d5e
Adds a decimal rounding operator 2022-04-29 21:18:15 +02:00
Denis Merigoux
1bf4404bb3
Big refactoring of the APL code 2022-04-29 20:18:01 +02:00
Denis Merigoux
91cfcd9b56
Better PDFs 2022-04-29 12:55:09 +02:00
Denis Merigoux
741d151128
Correct indentation and sectionning + BMAF 2022-2023 [skip ci] 2022-04-29 10:50:46 +02:00
Denis Merigoux
6ec2938581
Subsubsubsections in LaTeX output 2022-04-29 10:25:46 +02:00
Denis Merigoux
3f3563cfeb
Print TOC in PDF 2022-04-28 13:32:35 +02:00
Denis Merigoux
d79e6c974d
Fix last bugs 2022-04-26 16:22:47 +02:00
Denis Merigoux
764edb6ef0
Refactoring finished 2022-04-26 16:06:36 +02:00
Denis Merigoux
6ea73a4291
Progress on refactoring [skip ci] 2022-04-26 12:07:39 +02:00
Denis Merigoux
40480fc4b0
Fix compile_with_exceptions [skip ci] 2022-04-25 18:00:08 +02:00
Denis Merigoux
3ded0c7399
Better error messages 2022-04-25 15:28:16 +02:00
Denis Merigoux
c1c2953131
Fixing more errors [skip ci] 2022-04-25 10:19:04 +02:00
Denis Merigoux
dca6a6c3d4
Merge branch 'master' into allocations_logement 2022-04-22 15:20:48 +02:00
Denis Merigoux
1c86c8298b
Fix decimal parsing 2022-04-22 14:26:28 +02:00
Denis Merigoux
d889397425
Write first computation test with @Lilyaslm! 2022-04-21 17:20:40 +02:00
Romain PRIMET
5397de576c update generated catala import instruction 2022-04-21 09:57:18 +02:00
Denis Merigoux
8ce81fedaa
Start to refactor Lcalc AST (WIP) [skip ci] 2022-04-15 12:16:44 +02:00
Denis Merigoux
88a522d120
Changed maps and folds for Dcalc 2022-04-15 12:16:22 +02:00
Denis Merigoux
4cd6d5519d
Fix doc generation 2022-04-14 11:18:26 +02:00
Denis Merigoux
6e03b512d9
Merge branch 'master' into allocations_logement 2022-04-13 15:28:54 +02:00
Denis Merigoux
8be3d1cfc9
Made more functions generic in Dcalc.Ast 2022-04-12 17:54:00 +02:00
Denis Merigoux
e7440e043c
Remove duplicated function 2022-04-12 17:07:00 +02:00
Denis Merigoux
33ff03a356
Map visitor for Dcalc 2022-04-12 11:51:33 +02:00
Denis Merigoux
b24dbc8360
Remove logging calls for vc generation 2022-04-12 11:14:39 +02:00
Denis Merigoux
48dda14dcd
Merge branch 'master' into c_backend 2022-04-12 10:53:46 +02:00
Denis Merigoux
a43f89a0f4
Parametrize Dcalc.scope_expr 2022-04-12 10:53:07 +02:00
Denis Merigoux
6f223d2519
Restore web build 2022-04-11 10:59:40 +02:00
Romain PRIMET
eafab30809 fix typo 2022-04-07 22:43:05 +02:00
Denis Merigoux
f2d1fab263
Refactoring to clean some Dcalc passes 2022-04-06 09:48:34 +02:00
Denis Merigoux
f6047a43ea
Added boxed constructors for Dcalc 2022-04-06 09:35:07 +02:00
Denis Merigoux
48b324c165
More comments 2022-04-04 18:12:19 +02:00
Denis Merigoux
cbd975d53a
Remove unused stub 2022-04-04 18:07:47 +02:00
Denis Merigoux
f6c8e7fbd9
Crediting author of moved code 2022-04-04 18:06:40 +02:00
Denis Merigoux
3f49824150
Merge branch 'master' into c_backend 2022-04-04 18:02:33 +02:00
Denis Merigoux
31e8f37a43
Sort VCs by alphabetical order 2022-04-04 17:51:41 +02:00
Denis Merigoux
e68fe42856
Put closure conversion prototype under a flag 2022-04-04 17:43:30 +02:00
Denis Merigoux
9d05dad3fb
Passing all tests! 2022-04-04 15:56:45 +02:00
Denis Merigoux
84144c0a56
Tests now passing except for a few position and printing issues [skip ci] 2022-04-04 12:25:00 +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
8f39b65bb6
Started replacement of Ast by Binded_representation in Dcalc [skip-ci] 2022-04-02 12:29:43 +02:00
Denis Merigoux
be26fa2474
Implement app but lots of rtefactoring to do [skip ci] 2022-03-31 14:21:13 +02:00
Denis Merigoux
c7c774a1a1
Closure conversion: case of EAbs implemented 2022-03-31 12:19:31 +02:00
Denis Merigoux
6fb924b7d4
Merge pull request #236 from CatalaLang/afromher_z3 
[Z3 encoding] Add support for durations
 2022-03-28 19:08:11 +02:00
Denis Merigoux
158d49fe86
Removed unnecessary extra runtime function 2022-03-28 18:59:53 +02:00
Aymeric Fromherz
2b0206a5a8 Restrict duration z3 encoding to days only 2022-03-28 18:47:13 +02:00
Denis Merigoux
5d36af01e3
Restore the trace parameter functionality in the web interpreter 2022-03-28 15:16:03 +02:00
Denis Merigoux
ce7e756af1
Nice error messages for empty structs and enums 2022-03-28 14:43:38 +02:00
Aymeric Fromherz
2c247128d1 [Z3encoding] Add support for duration literals 2022-03-24 17:22:31 +01:00
Aymeric Fromherz
e2963bd7f3 Add a duration_to_nb_days function to runtime 2022-03-24 17:22:16 +01:00
Aymeric Fromherz
8d2348d1d9 [Z3 encoding] Add support for Duration type and operators 2022-03-24 17:15:22 +01:00
Denis Merigoux
be191de566
Some closures closed but buggy overall [skip ci] 2022-03-23 17:50:53 +01:00
Denis Merigoux
a660987df0
Starting to implement closure conversion [skip ci] 2022-03-21 17:26:23 +01:00
Denis Merigoux
25977de151
Prettify Scalc 2022-03-21 14:58:54 +01:00
Denis Merigoux
01bbf1230e
Merge branch 'master' into allocations_logement 2022-03-17 17:55:47 +01:00
Denis Merigoux
6722cf9647
Fix bug 2022-03-17 17:52:26 +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
7872e8dac3
Typo in lexer 2022-03-17 13:23:07 +01:00
Denis Merigoux
bb33d05c4a
Typo in lexer 2022-03-17 13:22:07 +01:00
Denis Merigoux
8f68e2b262
Merge branch 'master' into allocations_logement 2022-03-17 13:15:24 +01:00
Denis Merigoux
a3e9dfa534
Fix wrong round definitions in runtime 2022-03-17 13:09:57 +01:00
Denis Merigoux
cdac6de9fe
Implement the round money builtin 2022-03-17 12:30:14 +01:00
Denis Merigoux
66244946c5
Merge branch 'master' into allocations_logement 2022-03-17 11:43:20 +01:00
Denis Merigoux
9b35cfcf7d
Merge branch 'master' into afromher_z3_2 2022-03-16 12:18:01 +01:00
Denis Merigoux
c47ce263b5
Merge pull request #228 from CatalaLang/afromher_z3 
[Z3encoding] Basic support for arrays
 2022-03-16 12:17:31 +01:00
Aymeric Fromherz
97c0211bdc [Z3encoding] Support for unit literal 2022-03-16 12:01:21 +01:00
Denis Merigoux
bba5e3afea
Only print logging in Scopelang if debug 2022-03-16 12:00:36 +01:00
Aymeric Fromherz
b00d270df7 [Z3backend] Add support for EInj nodes 2022-03-16 12:00:19 +01:00
Denis Merigoux
c59451751b
Fix logging operator location for default justifications 2022-03-16 11:44:34 +01:00
Aymeric Fromherz
e3f3704be9 comment typo 2022-03-16 11:35:13 +01:00
Aymeric Fromherz
148afda523 Counterexamples generation for arrays 2022-03-16 11:28:03 +01:00
Aymeric Fromherz
fb6c18763f Fix encoding of hypotheses into Z3 2022-03-16 11:20:20 +01:00
Denis Merigoux
c936e7b6ed
Reshuffle code, make it work, correct a few yes/no inversion bugs 2022-03-15 19:47:41 +01:00
Aymeric Fromherz
f6ad6bbd2f Encode that an array length is always positive 2022-03-15 18:52:02 +01:00
Denis Merigoux
3780af59f5
Merge branch 'master' into allocations_logement 2022-03-15 18:44:49 +01:00
Aymeric Fromherz
fb924c50e5 Encode the length of arrays into Z3 2022-03-15 18:43:11 +01:00
Aymeric Fromherz
4b1ace2739 [Z3Backend] Support GetYear equality comparison 2022-03-15 18:09:56 +01:00
Aymeric Fromherz
d760d883a6 [Z3encoding] Print variable name when encoding is not supported 2022-03-15 18:09:33 +01:00
Denis Merigoux
169432c9f2
Pair programming @Lilyaslm 2022-03-14 11:55:32 +01:00
Denis Merigoux
88bf577db6
Merge branch 'master' into allocations_logement 2022-03-14 10:46:57 +01:00
Denis Merigoux
6227097de4
Merge pull request #223 from AltGr/optional-z3 
Make Z3 an optional dependency
 2022-03-09 17:22:06 +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
Denis Merigoux
97ede2cde1
Merge branch 'master' into allocations_logement 2022-03-09 10:47:29 +01:00
Denis Merigoux
2dfb15d888
reformat (sync with master) 2022-03-09 10:43:17 +01:00
Denis Merigoux
296760f09c
Merge pull request #224 from CatalaLang/afromher_dcalc 
DCalc optimization pass: Remove if_then_else when both branches are identical
 2022-03-09 10:29:51 +01:00
Aymeric Fromherz
9eec6a474c format 2022-03-08 20:43:55 +01:00
Aymeric Fromherz
9cbfc13288 Merge branch 'master' into afromher_dcalc 2022-03-08 20:41:35 +01:00
Aymeric Fromherz
3fb14264c2 Implement equal_ops in dcalc 2022-03-08 20:39:45 +01:00
Aymeric Fromherz
ac42bf65a7 Refactor to extract common equal_exprs_list and equal_typs_list 2022-03-08 20:31:22 +01:00
Aymeric Fromherz
5b345b4782 format 2022-03-08 20:23:45 +01:00
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
Aymeric Fromherz
2fa2f36c1d Optimize if_then_else when both branches are identical 2022-03-08 17:38:14 +01:00
Louis Gesbert
b4b6d5d648 Fix compilation catala_web_interpreter 
oops I overlooked that one
 2022-03-08 17:35:57 +01:00
Aymeric Fromherz
89d69c2316 Implement equality function on dcalc expressions 2022-03-08 17:35:08 +01:00
Emile Rolley
709d4e5ae5 fix(lcalc): disable ocamlformat for let+ expressions 2022-03-08 16:13:47 +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
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
Denis Merigoux
cfbca7b2be
Merge branch 'master' into allocations_logement 2022-02-25 17:10:23 +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
Denis Merigoux
d4a1a43fcc
Merge branch 'master' into allocations_logement 2022-02-23 17:11:45 +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 8e1a1ccb63, reversing
changes made to 4812830a25.
 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
Denis Merigoux
cb8a295945
Allocations logement typechecks now 2022-02-18 11:31:13 +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
Denis Merigoux
69a7465339
Merge branch 'master' into alain_default-option 2022-02-14 12:09:11 +01:00
Denis Merigoux
9a718c6ced
Format comments 2022-02-14 12:07:35 +01:00
Denis Merigoux
a9f5495cf1
More comments for I/O 2022-02-14 10:29:17 +01:00
Alain
80fa3110eb
documentation + finished translating cut to hoist + copyright inside the compile_without_exceptions 2022-02-12 08:08:13 +01:00
Alain
77051cadba
fmt 2022-02-11 11:40:24 +01:00
Alain
cf28a58342
cut --> hoist 
binded representation

few doc
 2022-02-11 11:38:18 +01:00
Alain
8834034094
disable beta-reduction 2022-02-11 09:39:01 +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
5004929a51
Fix #193 -- authored with @R1kM 
Moved no model generation flag
Fixed bug for VC generation in the IfThenElse case
 2022-02-10 16:49:01 +01:00
Denis Merigoux
a140614069
Bring IO down in Scopelang AST 2022-02-10 10:09:58 +01:00
Denis Merigoux
d401b3424c
Fixed verification conditions generation 2022-02-10 10:05:14 +01:00
Denis Merigoux
9bb858b79b
Added input/output/internal description in tutorial 2022-02-09 18:06:03 +01:00
Denis Merigoux
e4be116ded
Add negative tests 2022-02-09 17:22:04 +01:00
Denis Merigoux
a8733e6a61
Fix tests [skip ci] 2022-02-09 15:56:57 +01:00
Denis Merigoux
cb04ef3f9d
OnlyInput variables nore more thunked 2022-02-09 15:34:13 +01:00
Denis Merigoux
f3928dee9d
Better printing [skip ci] 2022-02-09 15:06:21 +01:00
Alain
72da935392 chaging pretty printer for type to Dcalc.Print.format_typ 2022-02-09 11:50:04 +01:00
Alain
bd0fe18cc3 handling with special care SubScopeVarDefinition using the invariant that is it thunked 2022-02-09 11:44:00 +01:00
Denis Merigoux
30061b8c86
Better encoding of inputs [skip ci] 2022-02-09 11:37:52 +01:00
Alain
29b734be46 reorganisation of the file compile_without exceptions 
working binding of whole program

working translation
 2022-02-09 11:30:35 +01:00
Denis Merigoux
5c6a43da57
Fixed compilation to examples 
Had to rename fields of allocations familiales because of a stupid record field confusion in OCaml
 2022-02-07 18:38:31 +01:00
Denis Merigoux
1c4a0bdd5d
Updated all examples with input/output decorations [skip ci] 2022-02-07 18:18:23 +01:00
Denis Merigoux
2263dd7dab
Update syntax highlighting and test suite [skip ci] 2022-02-07 12:04:48 +01:00
Alain
3a1ab17796 fix uncorrect scope definition 
select only part of type transformation to do
 2022-02-07 11:00:36 +01:00
Alain
ed2c192470 Add monomorphisation of eoptions types 
Compilation as TAny is not enough clear to define structures in ocaml.
 2022-02-07 10:58:41 +01:00
Denis Merigoux
e3b5d2d0b6
Finer control over input IO (distinction only_input/reentrant) [skip ci] 2022-02-07 10:30:36 +01:00
Alain
16e09a1e36 type translation 2022-02-07 09:17:23 +01:00
Alain
016056728e forcing the invariant of the previous commit 2022-02-07 09:17:13 +01:00
Denis Merigoux
f4200bb638
Dcalc encoding good, missing error messages for bad cases 2022-02-06 18:52:18 +01:00
Denis Merigoux
72274057cd
Better Dcalc printing 2022-02-06 18:25:37 +01:00
Denis Merigoux
6601585b77
First test passing, awaiting rest of features 
(subscopes, etc.)
 2022-02-05 00:04:19 +01:00
Alain
730bd71cd3 new invariant about assert in dcalc 
it is now a pure function, and is always in the form EAssert (ErrorOnEmpty _).
 2022-02-04 16:58:58 +01:00
Alain
c97ab86c1c removed un-used code 2022-02-04 16:50:40 +01:00
Alain
424b68a6a5 formatting 2022-02-04 16:43:59 +01:00
Alain
b44e8e4f08 changed optimization so it actually work 2022-02-04 16:25:57 +01:00
Denis Merigoux
5962b23f93
Restore CI 2022-02-04 15:45:27 +01:00
Denis Merigoux
97f8875a39
Merge branch 'master' into alain_default-option 2022-02-04 15:35:52 +01:00
Denis Merigoux
a06dfbfaa5
Assets and formatting 2022-02-04 15:29:31 +01:00
Alain
6ad948ed76 more cleanup in lcalc-ast 2022-02-04 15:13:28 +01:00
Denis Merigoux
11d4a34783
Better printing, tests, fix parser ommission 2022-02-04 15:10:47 +01:00
Alain
02187b4bc7 removed useless file 2022-02-04 14:53:47 +01:00
Denis Merigoux
d8c120bf97
Propagate visibility down, missing handling in scope_to_dcalc 2022-02-04 14:41:22 +01:00
Alain
d9fbe4b499 use external pp in compile_without_exceptions 
better error messages

fixed make_matchopt_with_abs_arms

fixed license

few documentation
 2022-02-04 14:32:12 +01:00
Alain
541d5656ac print uid too in Lcalc.Print 2022-02-04 14:31:06 +01:00
Alain
08651d33af better error message in to_ocaml conversion 2022-02-04 14:30:42 +01:00
Alain
154baefd5c runtime fix 2022-02-04 14:30:17 +01:00
Alain
6da5cc518b cleanup dcalc-ast.ml 2022-02-04 12:33:26 +01:00
Alain
f8343d1d0c cleanup lcalc-ast.ml 2022-02-04 12:28:03 +01:00
Alain
88eedbc000 ocamlformat 2022-02-04 09:27:10 +01:00
Alain
b777d3215b computing of free vars+ more debuging 
finally found an error (List.fold_left instead of List.fold_right
 2022-02-04 09:24:51 +01:00
Alain
9e301331e6 more printing 2022-02-03 18:56:37 +01:00
Alain
005646d2b2 implementation of scoping let function 2022-02-03 18:48:17 +01:00
Alain
ebc2adc53e removed comments 2022-02-03 18:30:58 +01:00
Alain
156dd71375 intermediate step 2022-02-03 18:27:55 +01:00
Alain
3e96db43ce more printing to debug 2022-02-03 17:16:45 +01:00
Alain
85fc1be4fb printing ctx at each steps but no error found so far. 2022-02-03 11:50:18 +01:00
Alain
ef7f25b70d runtime correct type 2022-02-03 11:47:27 +01:00
Alain
4290059ab8 newline 2022-02-02 18:10:27 +01:00
Alain
6158a2e150 nicer error messages when Not_Found error is raised inside the compilation without exceptions. 
added explicit match when finding [v ()] where v is a variable.

Correct position of ErrorOnEmpty.

added argument on translate_expr when adding an esome is not required

renamed "unit" to "_" (silent_var) for consistency
 2022-02-02 17:33:36 +01:00
Alain
1db649db3e nicer internal error when Not_Found is raised inside the code generation of ocaml code. 2022-02-02 17:24:32 +01:00
Alain
d7c422d33c clarify make_matchopt + lcalc's ast ocamlformat 2022-02-02 12:23:52 +01:00
Alain
67ccfb0122 renamed the new file 2022-02-02 12:14:07 +01:00
Alain
2c4f9bfc7a removed the old file 2022-02-02 12:13:47 +01:00
Alain
3c5bc4f67e before removing the old file 2022-02-02 12:12:15 +01:00
Alain
717915bc86 more documentation 2022-02-02 12:10:47 +01:00
Alain
0a612bfe7d translate_scope_let 2022-02-02 12:01:05 +01:00
Denis Merigoux
0d90dcea00
Better optimizations with values instead of literals 2022-02-02 10:30:39 +01:00
Alain
90a63ebead finished implementation of translation_expr + some documentation 2022-02-01 17:49:00 +01:00
Denis Merigoux
6cf1b768d2
Fix bug in Python backend producing unreachable code 2022-02-01 15:41:53 +01:00
Denis Merigoux
8ad752eba5
Type refactoring in scope_to_dcalc 2022-01-31 18:09:14 +01:00
Denis Merigoux
edeba14692
Just typechecking for compiler 2022-01-31 15:28:19 +01:00
Denis Merigoux
effc2b24e4
Optimizations for defaults in Dcalc 2022-01-31 15:27:58 +01:00
Denis Merigoux
73ce2f142f
Fixed last bug around rule refactoring 2022-01-31 13:55:25 +01:00
Denis Merigoux
13b476d0a1
[skip ci] reorganized desugared to scope encoding, broke some invariants 
WIP: fixed some bugs and provided documentations but one thing missing
 2022-01-28 17:31:31 +01:00
Denis Merigoux
0a9e6db5f4
Fix UTF8 lexing. 
By what magic did it work until now?
 2022-01-28 11:09:44 +01:00
Alain
fcf6fecf71 implementation of a few cases in the translation without exceptions 2022-01-28 11:07:29 +01:00
Alain
33d9d03dea advancing 2022-01-28 09:28:02 +01:00
Denis Merigoux
05a0bfc9b7
Added parsing support for #112, missing all later compilation steps 2022-01-27 18:03:47 +01:00
Denis Merigoux
228330d0cf
Fix 2022-01-26 17:15:06 +01:00
Denis Merigoux
5e253ba321
Disabling exact counterexamples values from CI testing because of randomness 2022-01-26 16:24:09 +01:00
Alain
1bfb891aa1 printing dcalc and lcalc ast 2022-01-25 13:55:17 +01:00
Denis Merigoux
f7f010a902
Update asset and fix missing link in doc 2022-01-21 20:16:07 +01:00
Denis Merigoux
42d79e5169
Merge branch 'master' into proof_platform 2022-01-21 09:55:34 +01:00
Denis Merigoux
757c3eddb6
Remove mathematical symbols replacement 2022-01-19 14:43:42 +01:00
Denis Merigoux
54c090289b
Revamped CLI doc 2022-01-19 11:20:25 +01:00
Denis Merigoux
d2977b48ce
Documentation pass 2022-01-19 10:54:16 +01:00
Denis Merigoux
a4002fefaf
Finished functorization 2022-01-19 10:17:19 +01:00
Denis Merigoux
bc2742961f
More functors, but still not finished 2022-01-19 10:12:20 +01:00
Denis Merigoux
2f7059c1ac
More functorization 2022-01-19 09:47:08 +01:00
Denis Merigoux
4852891e6c
Added interfaces 2022-01-18 18:59:05 +01:00
Denis Merigoux
b11e3329b3
Functorize VC solving IO [skip ci] 2022-01-18 18:51:02 +01:00
Denis Merigoux
2e1dc4740a
Restore build [skip ci] 2022-01-18 17:59:15 +01:00
Denis Merigoux
777f194178
.mlis and ocamldoc [skip-ci] 2022-01-18 15:13:16 +01:00
Aymeric Fromherz
400a777891 Support common case for getYear: Comparison against a literal [skip ci] 2022-01-17 15:02:56 +01:00
Aymeric Fromherz
cf63e4f3d3 Restore pretty-printing of enum model [skip ci] 2022-01-14 21:10:34 +01:00
Aymeric Fromherz
2548b4ad5e Pretty-print structs, temporarily disable pretty-printing of enum model during refactoring [skip ci] 2022-01-14 21:02:34 +01:00
Aymeric Fromherz
0b011a5e3a Support TTuple type [skip ci] 2022-01-14 20:37:45 +01:00
Aymeric Fromherz
7fa271b9f4 Construct Z3 sort corresponding to a struct [skip ci] 2022-01-14 20:35:22 +01:00
Aymeric Fromherz
89e41b3a33 Encode ETupleAccess node [skip ci] 2022-01-14 20:17:27 +01:00
Aymeric Fromherz
850718be17 Add support for structs in the Z3 encoding context [skip ci] 2022-01-14 20:08:42 +01:00
Aymeric Fromherz
6c749fdbfe Pretty-print enums in Z3 model [skip ci] 2022-01-14 19:23:26 +01:00
Aymeric Fromherz
06b845316d Allow match bodies in VCs to refer to the value corresponding to the destructed enum [skip ci] 2022-01-14 19:01:54 +01:00
Aymeric Fromherz
3c21182dea Finish encoding arms of EMatch in VCs [skip ci] 2022-01-14 18:33:56 +01:00
Aymeric Fromherz
a7abe630e7 More progress towards encoding arms of EMatch in VCs [skip ci] 2022-01-14 18:24:32 +01:00
Aymeric Fromherz
ffee0d815d Wrap up the find_or_create_enum function [skip ci] 2022-01-14 17:42:12 +01:00
Aymeric Fromherz
7c1e808880 Translate the type TEnum to Z3 2022-01-14 17:42:12 +01:00
Aymeric Fromherz
a1e12a22b1 Create or retrieve Z3 enum types [skip ci] 2022-01-14 17:42:12 +01:00
Aymeric Fromherz
ae0935f035 Z3 encoding: Add a map from enumnames to Z3 sorts to the context [skip ci] 2022-01-14 17:42:12 +01:00
Aymeric Fromherz
1932277c80 Fix printing of negative money amounts [skip ci] 2022-01-14 11:45:47 +01:00
Aymeric Fromherz
951e50637f Actually plug date pretty printing into Z3 encoding [skip ci] 2022-01-14 02:08:04 +01:00
Aymeric Fromherz
50ad5e3044 Print dates generated by Z3 model [skip ci] 2022-01-14 02:04:55 +01:00
Aymeric Fromherz
977e985e4c Encode dates to Z3 [skip ci] 2022-01-14 01:54:33 +01:00
Aymeric Fromherz
d89eea0481 Encode comparison operators on money [skip ci] 2022-01-13 20:11:28 +01:00
Aymeric Fromherz
827f5cb916 encode money to Z3 [skip ci] 2022-01-13 20:02:14 +01:00
Aymeric Fromherz
50d0ee0909 Start printing z3 model results according to their type [skip ci] 2022-01-13 19:52:58 +01:00
Denis Merigoux
428ae95c62
[skip ci] Added a walkthrough example for ProLaLa + tweaked tests output order of vcs 2022-01-13 16:58:43 +01:00
Denis Merigoux
5a6f4485e7
Matching subscope variables also [skip ci] 2022-01-13 16:00:09 +01:00
Denis Merigoux
a9454a0aac
Correctly match ignored part of expressions in VC generation [skip ci] 2022-01-13 12:15:37 +01:00
Denis Merigoux
bf444f548f
Error message pretty-printing and sat solving example [skip ci] 2022-01-13 10:46:23 +01:00
Aymeric Fromherz
f342c89482 [skip ci] Z3encoding: proper error message for ill-formed unary operators 2022-01-12 19:15:51 +01:00
Aymeric Fromherz
29ed4ff696 [skip ci] Z3encoding: refer to Catala source code variable names when printing a model 2022-01-12 19:09:20 +01:00
Aymeric Fromherz
297b7ec604 [skip ci] Z3encoding: documenting the function style for the context 2022-01-12 19:02:56 +01:00
Aymeric Fromherz
83e83507ed [skip ci] Z3encoding: Passing the context around to preserve dynamic updates throughout the VC encoding 2022-01-12 18:59:01 +01:00
Aymeric Fromherz
e66730bdd5 [skip ci] Start improving model prettyprinting 2022-01-12 18:35:36 +01:00