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 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
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
Aymeric Fromherz
a7ad86233e
[skip ci] document Z3encoding context type
2022-01-12 18:23:50 +01:00
Aymeric Fromherz
862af7a3d8
[skip ci] Pretty-print simple Z3 models when a VC is not satisfied
2022-01-12 18:15:09 +01:00
Aymeric Fromherz
45dc3faeed
[skip ci] minor refactor: prepare to parse Z3 model
2022-01-12 17:55:32 +01:00
Aymeric Fromherz
0e59cff1ed
[skip ci] print Z3 model when verification is failing
2022-01-12 17:51:28 +01:00
Aymeric Fromherz
9995837564
[skip ci] Z3encoding: support function calls
2022-01-12 17:38:12 +01:00
Denis Merigoux
78b1fe08f4
[skip ci] Always name of the variable on the left
2022-01-12 16:56:05 +01:00
Denis Merigoux
6d06f9c81c
Prettified error messages
2022-01-12 16:50:10 +01:00
Aymeric Fromherz
2a8f7f7c07
[skip ci] remove all logs before encoding query to z3
2022-01-12 16:30:00 +01:00
Denis Merigoux
0831f462ae
Correct signature
2022-01-12 16:28:03 +01:00
Denis Merigoux
16d8554384
Provide a function that removes all log calls
2022-01-12 16:25:46 +01:00
Aymeric Fromherz
d455e29978
[skip ci] Z3encoding: obtain type of bound variables
2022-01-12 15:58:19 +01:00
Denis Merigoux
c7b225bad5
Add types of free variables in VC [skip ci]
2022-01-12 15:52:44 +01:00
Aymeric Fromherz
7f3e59f7b0
[skip ci] Z3encoding: more debug information when encoding fails
2022-01-12 15:21:13 +01:00
Aymeric Fromherz
8bb8053580
[skip ci] Z3 encoding: Better split output between debug and non-debug information
2022-01-12 14:43:17 +01:00
Aymeric Fromherz
3c6f9d9174
[skip ci] formatting + slight refactor for better error messages during Z3 verification
2022-01-12 14:20:52 +01:00
Aymeric Fromherz
b11c76404f
[skip ci] Spawn one query per VC and correctly encode VC by negating it
2022-01-12 14:08:35 +01:00
Aymeric Fromherz
e10a25876f
[skip ci] Print Z3 encoding information as debug information only
2022-01-12 13:58:38 +01:00
Aymeric Fromherz
1c8f9c31f5
Z3 encoding: Add missing Lte for integers
2022-01-12 12:16:54 +01:00
Denis Merigoux
260959b088
Formatting + correct expected tests output
2022-01-11 18:33:45 +01:00
Aymeric Fromherz
20cc0795f9
Arithmetic binary operators
2022-01-11 17:54:02 +01:00
Aymeric Fromherz
f642bfe4be
Z3 encoding: More binary operators, pass more tests
2022-01-11 17:49:02 +01:00
Denis Merigoux
006f5f6c2a
Fix authorship
2022-01-11 16:36:38 +01:00
Denis Merigoux
83bdd0b632
Test base for verification conditions encoding
2022-01-11 16:13:34 +01:00
Denis Merigoux
d705334d9e
Merge branch 'master' into proof_platform
2022-01-11 15:43:33 +01:00
Denis Merigoux
7fc37f9af8
Added controls for Dcalc and Scopelang
2022-01-11 11:25:41 +01:00
Denis Merigoux
56e4adb3f7
Merge branch 'master' into clerk
2022-01-10 18:36:49 +01:00
Denis Merigoux
f8dc1494f0
Autoformatting
2022-01-10 18:36:14 +01:00
Denis Merigoux
2b6e7c8b98
Working prototype of clerk, the new build system for Catala
2022-01-10 17:57:58 +01:00
Alain
5c5bc77c87
formatting (sorry, problem with the makefile)
2022-01-10 17:53:48 +01:00
Alain
5bc9a36308
vc generation for conflict errors
2022-01-10 17:30:19 +01:00
Alain
e8dbaaec47
add not to z3encoding
2022-01-10 17:30:08 +01:00
Alain
0c2dbdddd1
correct typo in vc generation for conflict error
...
add some debug in comments
2022-01-10 17:29:53 +01:00
Alain
baa435d2c5
optimization for not
2022-01-10 17:28:37 +01:00
Alain
8a0a4c7603
naive verification condition for conflicts
2022-01-10 16:25:20 +01:00
Louis Gesbert
8d059b420e
Fix console formatting with colors
...
closes #174
2022-01-10 15:56:55 +01:00
Aymeric Fromherz
4b47f7fd9a
More binary operators encoding, some boolean examples now passing
2022-01-10 14:53:58 +01:00
Aymeric Fromherz
b9b593a361
Encode some basic types to Z3
2022-01-10 14:51:36 +01:00
Aymeric Fromherz
0455029951
Z3: Start encoding Catala types as Z3 sorts
2022-01-10 14:50:50 +01:00
Aymeric Fromherz
bc4608755a
Z3: Encode EVar node
2022-01-10 14:46:41 +01:00
Aymeric Fromherz
2d036f9925
Add ctx_var to z3encoding context
2022-01-10 14:37:17 +01:00
Aymeric Fromherz
a9ebfaed38
Pass program to z3encoder
2022-01-10 14:36:15 +01:00
Denis Merigoux
ca7b009b02
Should compile
2022-01-10 14:35:51 +01:00
Denis Merigoux
ab194c76fd
Give function for retrieving variable types
2022-01-10 14:32:27 +01:00
Denis Merigoux
1fcd66ba78
Made pretty printing without logs for dcalc
2022-01-10 14:19:04 +01:00
Denis Merigoux
50719911f8
Added TODOs
2022-01-10 13:48:00 +01:00
Denis Merigoux
04cc274d3e
Print term for error message
2022-01-10 11:52:48 +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
ad4218285d
Working partial evaluation for Dcalc using ugly but correct style
2022-01-09 19:16:34 +01:00
Denis Merigoux
743a1b74c9
Renamed and grouped modules cleanly
2022-01-08 18:37:04 +01:00
Aymeric Fromherz
8b6595426e
Add Lt node and int literals
2022-01-07 18:54:15 +01:00
Aymeric Fromherz
ce80d1e9e9
Omit Log node from VC generation
2022-01-07 18:47:53 +01:00
Denis Merigoux
71a2f85d7c
Comments
2022-01-07 18:44:10 +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
cc8e88ec4e
Start supporting unary operators
2022-01-07 18:36:25 +01:00
Aymeric Fromherz
75b42423c6
Start encoding literals to Z3
2022-01-07 18:25:35 +01:00
Aymeric Fromherz
98b5518638
Add support for Z3 encoding of if_then_else
2022-01-07 18:23:46 +01:00
Aymeric Fromherz
f2bd803f0f
Add support for Z3 encoding of binary operators application
2022-01-07 18:14:01 +01:00
Aymeric Fromherz
1105858bea
Setting up the pipeline for encoding VCs to Z3
2022-01-07 17:50:45 +01:00
Aymeric Fromherz
6c67ed03bb
Add z3 dependency to build system
2022-01-07 16:58:24 +01:00
Denis Merigoux
ee92ed2385
Added comments
2022-01-07 16:18:26 +01:00
Denis Merigoux
75ef1ef70f
Added proof of concept of verification condition generation
2022-01-07 12:04:31 +01:00
Denis Merigoux
909e539cdc
Fixed all bugs
2022-01-05 15:57:18 +01:00
Denis Merigoux
82c09ee455
Fixed a bug [skip ci]
2022-01-05 15:37:34 +01:00
Denis Merigoux
3752328671
Code working but needs debugging [skip ci]
2022-01-05 10:42:46 +01:00
Denis Merigoux
9733f39653
Refactoring done except Desugared_to_scope.def_map_to_tree [skip ci]
2022-01-05 09:14:43 +01:00
Denis Merigoux
f6825668dd
Propagate labels in desugaring, not building desugared/ yet [skip-ci]
2022-01-04 18:19:15 +01:00
Denis Merigoux
e9d54e120d
Changed label scoping from scope to scope definition key [skip ci]
2022-01-03 18:39:59 +01:00
Denis Merigoux
cacf605a64
Merge pull request #169 from EmileRolley/fix-odoc-gen
...
Fix(build/doc): remove warnings due to .ml* files
2022-01-02 17:26:24 +01:00
Emile Rolley
397b0e1d7c
fix(build/doc): remove warnings due to .ml* files
2022-01-02 14:53:51 +01:00
Emile Rolley
7a62147283
fix(latex): render properly the '^' and fix the french babel usage
2021-12-31 20:50:03 +01:00
Emile Rolley
5a06d33d2d
fix(latex): escape '#' inside latex outputs + refactor pre_latexify
2021-12-31 19:47:55 +01:00
Alain
2d267471da
tentative beta reduction
2021-12-17 15:32:20 +01:00
Alain
84cd6ddc61
error on empty everywhere
2021-12-17 15:27:34 +01:00
Alain
c3268cc13c
more mistakes removed
2021-12-16 19:48:14 +01:00
Alain
63ff6cfbb3
wip (compiling but can't compile catala program without internal errors)
...
instrumentation of Dcalc.expr to show internals representation
2021-12-16 19:16:57 +01:00
Alain
3a09b39bf5
wip
2021-12-16 16:59:25 +01:00
Alain
0d1363b2f6
wip
2021-12-15 15:43:11 +01:00
Alain
65ad229373
scope_let translation 2/6
2021-12-15 09:23:03 +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
e8a95db9ed
Trying to box everything but optimizations complaining
2021-12-10 16:54:51 +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
3a21bec4b1
Scopelang to dcalc done [skip ci]
2021-12-09 18:42:36 +01:00
Denis Merigoux
fcf7c31279
Progress on Scopelang -> Dcalc [skip ci]
2021-12-09 13:54:10 +01:00
Denis Merigoux
d9f21e9e66
Progress
2021-12-09 11:58:42 +01:00
Denis Merigoux
6099d1e4ad
Beginning to bring more structure to Dcalc
2021-12-08 23:56:03 +01:00
Alain
9c76b34afc
removed assert false
2021-12-08 12:58:21 +01:00
Alain
df545e5761
add translate_binder
...
refactor make_bindopt
refactor make_matchopt
added make_bindmopt
remove _{i}_ printing in to_ocaml
add correct printing of handle_default_opt
add two-step translation
correct context for new variables
2021-12-07 18:57:28 +01:00
Alain
177a2149ac
handle_opt
2021-12-07 16:03:15 +01:00
Denis Merigoux
2732a87ca1
Fix CLI doc
2021-12-02 09:19:35 +01:00
Alain
959203e595
add: error message when unary operator log is left somewhere it shouldn't
2021-12-01 15:48:58 +01:00
Alain
ac7df6cdd7
add: implementation of generic operator without the need of rewriting each one
...
add: error when using an operator not in the right place when using --avoid_empty
2021-12-01 15:48:18 +01:00
Alain
0dfac8210e
fix invariant correction within ErrorOnEmpty
2021-12-01 15:43:19 +01:00
Alain
86fa2ea7fa
correct bindlib utilization (cont)
2021-12-01 15:42:37 +01:00
Alain
3f8bc482f3
add refine iota transformation in lcalc
2021-12-01 15:42:01 +01:00
Alain
5f86837428
correct use of bindlib in the translation
2021-12-01 11:17:16 +01:00
Alain
be166eb479
add lazy implementation of handle_default_opt in runtime
2021-12-01 10:17:05 +01:00
Alain
fd8ff75079
renamed transform -> visitor_map
2021-12-01 10:12:00 +01:00
Alain
76f5e6115c
changing signature -- cont
2021-11-30 18:05:30 +01:00
Denis Merigoux
604fbbf2bf
Stub of changing signature
2021-11-30 16:52:33 +01:00
Denis Merigoux
c3bde49194
Merge branch 'master' into alain_default-option
2021-11-30 16:52:19 +01:00
Denis Merigoux
536dde9834
Formatting + CI + etc
2021-11-30 16:27:47 +01:00
Alain
8d580f1db6
fix: removed ESome and ENone constructions.
2021-11-29 17:53:07 +01:00
Alain
22af2a9335
refactored transformation to remove matchopt construction
2021-11-29 17:40:30 +01:00
