Commit Graph

281 Commits

Author SHA1 Message Date
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
Alain
6fe75f3486 fv --> free_vars_set
free_vars --> free_vars_list
2022-02-21 11:51:01 +01:00
Alain
d7b9aa9492 fixing if-then-else bug 2022-02-18 16:11:22 +01:00
Alain
d512b27e2c fmt 2022-02-18 15:49:23 +01:00
Alain
19bf2d934f dcalc review 2022-02-18 15:31:52 +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
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
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
Denis Merigoux
9bb858b79b
Added input/output/internal description in tutorial 2022-02-09 18:06:03 +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
Denis Merigoux
30061b8c86
Better encoding of inputs [skip ci] 2022-02-09 11:37:52 +01:00
Denis Merigoux
72274057cd
Better Dcalc printing 2022-02-06 18:25:37 +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
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
Alain
6da5cc518b cleanup dcalc-ast.ml 2022-02-04 12:33:26 +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
Denis Merigoux
0d90dcea00
Better optimizations with values instead of literals 2022-02-02 10:30:39 +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
Alain
1bfb891aa1 printing dcalc and lcalc ast 2022-01-25 13:55:17 +01:00
Denis Merigoux
d2977b48ce
Documentation pass 2022-01-19 10:54:16 +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
Denis Merigoux
d705334d9e
Merge branch 'master' into proof_platform 2022-01-11 15:43:33 +01:00
Denis Merigoux
f8dc1494f0
Autoformatting 2022-01-10 18:36:14 +01:00
Alain
5c5bc77c87 formatting (sorry, problem with the makefile) 2022-01-10 17:53:48 +01:00
Alain
baa435d2c5 optimization for not 2022-01-10 17:28:37 +01:00
Louis Gesbert
8d059b420e Fix console formatting with colors
closes #174
2022-01-10 15:56:55 +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
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
3752328671
Code working but needs debugging [skip ci] 2022-01-05 10:42:46 +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
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
0f5fde2c5a advancing 2021-11-22 15:55:21 +01:00
Alain
41a8961285 tentative, trying something else 2021-11-22 15:55:21 +01:00
Alain
a24a4ab6df starting to work on type inference 2021-11-22 15:55:21 +01:00
Denis Merigoux
2c0e8a7864
x10 performance on Catala compilation & interpretation
Cleaner rewriting of main let-binding chaining procedure from Scopelang to Dcalc
Removed costly unboxing in DCalc.Ast.make_let_in seemed to do the trick
2021-10-28 15:24:39 +02:00
Denis Merigoux
b56299f3d3
Switch ocamlformat to 0.19.0 2021-08-19 11:35:56 +02:00
EmileRolley
923a90b883 syntax(compiler): remove an @EmileRolley's note 2021-07-09 19:44:55 +02:00
EmileRolley
731513a003 refactor(compiler): factorize formatters inside prints modules 2021-07-08 16:36:53 +02:00
EmileRolley
6169d19b1e feat(compiler): add collection concatenation operator 2021-07-08 16:27:46 +02:00
Denis Merigoux
bbd50747d9
Big renaming and dir reorg 2021-06-21 11:39:06 +02:00