Louis Gesbert
c249cef3cc
Printer: flatten nested let-ins too
2023-05-02 11:53:30 +02:00
Louis Gesbert
3e7a2a34ab
More printer improvements
2023-05-02 11:49:09 +02:00
Louis Gesbert
cec52d47de
Printer: flatten "else if"
2023-05-02 11:49:09 +02:00
Louis Gesbert
8a2b50289e
Printer: add some missing boxes
2023-05-02 11:49:09 +02:00
Denis Merigoux
8d7666ee92
Interleave assertions with rules from desugared to scopelang
2023-04-28 14:15:43 +02:00
Emile Rolley
def003af8d
fix(plugins/json_schema): don't translate the TUnit type into "null" anymore
2023-04-28 13:41:25 +02:00
Denis Merigoux
e6bccd716d
Fix a Catala program bug thanks to Proof mode!
2023-04-27 18:03:27 +02:00
Denis Merigoux
a954942fd9
Bug in the law found with proof mode?
2023-04-27 16:58:40 +02:00
Denis Merigoux
7788bf9e73
Error message when two same states
2023-04-27 15:37:11 +02:00
Denis Merigoux
41d74bc673
Correctly hide function body on the trace
2023-04-27 15:07:04 +02:00
Denis Merigoux
9b056f3ca1
Update assets and fix errors after rebase
2023-04-27 12:18:50 +02:00
Denis Merigoux
e7f56b4310
Removed useless variable
2023-04-27 12:13:19 +02:00
Denis Merigoux
40af4d3a46
Disable optimization that was messing with the Proof backend
2023-04-27 12:13:18 +02:00
Denis Merigoux
4f7564b079
Improve editor parsable errors
2023-04-27 12:09:22 +02:00
Denis Merigoux
fcb5561b24
Coded message format adapted to editors
2023-04-27 12:09:22 +02:00
Denis Merigoux
19b33eaa96
Add lint and fix bugs related
2023-04-27 12:09:22 +02:00
Denis Merigoux
0338418a6f
Allow use of if_then_else beyond booleans in proof backend ( #460 )
2023-04-24 17:33:15 +02:00
Louis Gesbert
49bd5b1915
Cleanup type of Expr.make_app
2023-04-24 15:14:54 +02:00
Louis Gesbert
d7d8bab9b8
Printer: rainbow parens (rewritten)
2023-04-24 14:56:19 +02:00
adelaett
ba6fb5d405
fix documentation
2023-04-24 14:00:12 +02:00
Aymeric Fromherz
c6e478c9dd
[Proof Backend] Use Z3's native encoding for ite
2023-04-24 12:11:55 +02:00
Denis Merigoux
32ee2a0c72
Various small fixes to resolve conversations
2023-04-21 14:54:07 +02:00
Denis Merigoux
d384db4e71
Reestablish some default constructor optimizations
2023-04-21 14:35:10 +02:00
Denis Merigoux
22b24a8634
Fusion of all optimizations done correctly
2023-04-21 12:32:09 +02:00
Denis Merigoux
1bb338526d
Generalized optimizations
2023-04-21 11:56:07 +02:00
Denis Merigoux
2b0e18f5a8
Restore important flushing?!
2023-04-21 11:29:07 +02:00
Denis Merigoux
067c7b9155
Merge branch 'master' into adelaett-withoutexceptionsfix
2023-04-21 10:55:36 +02:00
Denis Merigoux
107ff95dc4
Remove dependency on ppx_expect and use alcotest instead
2023-04-21 10:37:31 +02:00
Louis Gesbert
fc70d18ea8
Correctly typed dcalc/lcalc interpreter
2023-04-20 14:04:29 +02:00
Louis Gesbert
55d343d81c
Version that uses object types instead of polymorphic variants
...
in order to get the row polymorphism controlling the GADT that encodes our AST
2023-04-20 13:51:20 +02:00
Denis Merigoux
f877544368
Remove optimizations for big tests
2023-04-18 15:56:04 +02:00
Denis Merigoux
f9a6644da3
Cleanliness and aesthetics
2023-04-18 15:45:30 +02:00
Denis Merigoux
0ec75ad589
Merge branch 'master' into adelaett-withoutexceptionsfix
2023-04-18 14:37:02 +02:00
Denis Merigoux
0b0451862e
Correct temp variable names
2023-04-18 14:29:22 +02:00
Louis Gesbert
bd870b0c28
Add experimental lazy interpreter as a plugin ( #453 )
2023-04-18 14:08:03 +02:00
Denis Merigoux
732e058712
Fix typos
2023-04-18 11:42:33 +02:00
Denis Merigoux
0266252854
Refactoring for cleaner exception graph building
2023-04-18 11:06:58 +02:00
Denis Merigoux
57da622567
Refactoring changes after @altgr's suggestions
2023-04-18 10:31:44 +02:00
Denis Merigoux
c5ba3e72fe
Restore CI
2023-04-18 09:59:24 +02:00
Denis Merigoux
39f1704d76
Last fixes
2023-04-18 09:59:24 +02:00
Denis Merigoux
ecccb5fb91
Last changes
2023-04-18 09:59:24 +02:00
Denis Merigoux
6479c3c10b
Print exception tree
2023-04-18 09:59:24 +02:00
Denis Merigoux
2afb6fc20c
I/O plumbing necessary for this feature, missing main implem
2023-04-18 09:59:24 +02:00
adelaett
5e46253140
removed one remaning debuging print, and updating all the tests
2023-04-14 17:59:08 +02:00
adelaett
e712c39efb
fix python printing of handle_default
2023-04-14 17:32:09 +02:00
adelaett
b642bdbc54
update optimizations
2023-04-14 17:16:01 +02:00
Louis Gesbert
b4a68fa392
Add experimental lazy interpreter as a plugin
...
To try it (without installing Catala):
```shell-session
$ make plugins
$ export CATALA_PLUGINS=_build/default/compiler/plugins
$ dune exec -- catala lazy examples/aides_logement/tests/tests_calcul_apl_locatif.catala_fr -s Exemple2
```
Keep in mind that this is a work-in-progress prototype :)
2023-04-14 16:56:57 +02:00
adelaett
adf14056fd
backtrace is now determined by the option.debug flag.
2023-04-14 16:38:39 +02:00
adelaett
e14267b0d7
fixing printing
2023-04-14 15:03:26 +02:00
adelaett
cffcdd7cf9
move monad_* to lcalc/Ast.ml
2023-04-14 14:36:28 +02:00
adelaett
02eeb4ad11
Include Bindlib_ext to Expr.Box
2023-04-14 14:18:28 +02:00
adelaett
ebf72213a7
deadcode
2023-04-14 14:12:36 +02:00
adelaett
ddeaa67ff7
Expr.eid -> Expr.fun_id
2023-04-14 14:07:51 +02:00
adelaett
484ae44298
disable detailled printing of enum and struct
2023-04-14 13:59:29 +02:00
adelaett
920bd29835
documentation and deadcode elim
2023-04-14 13:59:06 +02:00
adelaett
f21cb1ff69
adding comment
2023-04-14 12:18:28 +02:00
adelaett
6b6272b0f2
adding an nicer error message
2023-04-14 12:16:09 +02:00
adelaett
123ae9e4c1
rename functions to make the code more readable
2023-04-14 12:15:16 +02:00
adelaett
0c357d2972
adding typing information for monad_* functions
2023-04-14 12:13:33 +02:00
adelaett
167ec9189f
adding a todo related to handle_default and handle_default_opt for
...
the closure conversion.
2023-04-14 12:02:03 +02:00
adelaett
abc30e1612
handling invariants checking differently in the main driver
2023-04-14 12:01:16 +02:00
adelaett
cfc1d86e96
Revert "incorrect simplification"
...
This reverts commit 3233ff108f
.
2023-04-14 11:51:02 +02:00
adelaett
3233ff108f
incorrect simplification
2023-04-14 11:48:19 +02:00
adelaett
622feec9a5
change Invariants choice to --check_invariants flag
2023-04-14 11:32:49 +02:00
adelaett
2ea67de397
typo
2023-04-14 11:21:52 +02:00
adelaett
a9809b69a9
Merge branch 'master' into adelaett-withoutexceptionsfix
2023-04-14 11:19:58 +02:00
adelaett
5833608179
deadcode elim
2023-04-14 10:56:15 +02:00
adelaett
a45ae1869a
Fix #449 by removing premature optimizations on a smart constructor.
2023-04-14 10:50:21 +02:00
adelaett
a53bc27d23
documentation
2023-04-14 10:48:31 +02:00
Louis Gesbert
feeee4016e
Add support for dcalc plugins
...
previously only lcalc and scalc where available
2023-04-14 10:42:26 +02:00
adelaett
f8f6e56cca
fixing the issue of not merging inputs.
2023-04-14 09:22:36 +02:00
Louis Gesbert
e19e4af12d
Vastly improve the printer
...
* fix lots of Format boxes
* add parens based on precedence in the printer
* fix interaction of Format and the colored line debug tags
2023-04-13 18:15:22 +02:00
adelaett
cc66023e51
Thunking justifications and conclusion in avoid_translation pass
2023-04-12 10:58:21 +02:00
adelaett
83553d5950
indicate what interpreter is launched in debug mode.
2023-04-11 16:15:24 +02:00
adelaett
1a46cd8914
initialize inputs argument with default ENone value
2023-04-11 16:14:52 +02:00
adelaett
49e9846386
fix a bug in the translation
2023-04-11 16:14:25 +02:00
adelaett
0cfc446455
implementing the behavior of handle_exceptions_opt for the lcalc interpretor
2023-04-11 14:09:57 +02:00
adelaett
3e35d4b826
Merge branch 'master' into adelaett-withoutexceptionsfix
2023-04-11 11:49:22 +02:00
adelaett
6af7456b98
typo
2023-04-07 16:32:43 +02:00
adelaett
37b2cdf1aa
printing bindm as let*
2023-04-07 16:21:42 +02:00
adelaett
0e8eed7ee1
program equality function
2023-04-07 12:10:08 +02:00
adelaett
300d3b561d
fix too-many-spaces
2023-04-07 12:09:38 +02:00
adelaett
6c7ac061d4
fix identation and use new formatting functions as default
2023-04-07 11:57:14 +02:00
adelaett
618ff0518d
move printing of program & scope to the Print module
2023-04-07 11:26:10 +02:00
adelaett
12d85570e8
fix printing boxes & merge issues
2023-04-07 10:51:21 +02:00
adelaett
9b63743c2f
documentation
2023-04-07 10:49:48 +02:00
Denis Merigoux
77d6a97ddc
Formatting
2023-04-06 16:35:28 +02:00
alain
ec40de83fc
Merge branch 'master' into adelaett-withoutexceptionsfix
2023-04-06 13:57:22 +02:00
adelaett
73423a3cb6
typo
2023-04-06 13:50:58 +02:00
adelaett
65d9ac759a
review printer
2023-04-06 13:50:48 +02:00
adelaett
0906ba025b
reviewed operator.ml
2023-04-06 13:50:34 +02:00
adelaett
5a3a6a9dc1
remove unused json ppx
2023-04-06 13:50:22 +02:00
adelaett
7ebfb2e66a
typo
2023-04-06 13:42:40 +02:00
alain
f16842b71a
add a todo
2023-04-06 13:18:33 +02:00
adelaett
7b0f1b238c
add documentation for interpret_lcalc
2023-04-06 13:09:49 +02:00
adelaett
75e496c62d
correct types
2023-04-05 16:35:12 +02:00
adelaett
72f6ac9f58
append lcalc to driver
2023-04-05 15:42:26 +02:00
adelaett
256c0625ff
forward -> propagate
2023-04-05 14:57:02 +02:00
Louis Gesbert
0098f00512
Yet some more small improvements to the AST encoding
2023-04-05 10:32:58 +02:00
Louis Gesbert
0c1cd481e1
Interpreter on dcalc + lcalc (the simple way)
...
I made some changes in the meantime, and had to factorise e.g. the handling of
the `EEmptyError` case, but this is the simple approach type-wise of making the
function type for `∀ 'a. 'a —> 'a` (with `assert false` match cases), then
restricting its type do `dcalc` or `lcalc` in the `.mli`.
2023-04-05 10:32:58 +02:00
Louis Gesbert
79ff776d2e
Multi-pass interperter: typing (but useless) version
2023-04-05 10:32:58 +02:00
adelaett
503cd6b1e5
implementation of the behavior
2023-04-05 10:32:52 +02:00
adelaett
06147ac5b6
typing working in the file, but does not accept
...
Lcalc for some reason
2023-04-05 10:32:52 +02:00
adelaett
68e0f0a0ee
changing position of the interpreter
2023-04-05 10:32:52 +02:00
adelaett
82992e9858
documentation
2023-04-04 17:02:26 +02:00
adelaett
066388ddfd
fix of_lcalc special handling of handle_opt variables
2023-04-04 15:58:05 +02:00
adelaett
60f8c229d5
fix to_ocaml new handledefault and handledefault opt operator
2023-04-04 15:57:33 +02:00
adelaett
06f2e56c74
fix closure conversion non-existent variable
2023-04-04 15:57:11 +02:00
adelaett
8ef3db005f
clean deadcode
2023-04-04 15:56:49 +02:00
adelaett
61bdd751e4
corrected program equality
2023-04-04 15:18:08 +02:00
adelaett
b6cf552913
lcalc optimization documentation
2023-04-04 15:17:59 +02:00
adelaett
948af85abd
simplification of the driver
2023-04-04 15:17:43 +02:00
Denis Merigoux
ad02a0959d
Merge branch 'master' into aides_logement_outre_mer
2023-04-03 14:12:10 +02:00
Denis Merigoux
38b0041bb8
Add common linting passes to Catala ( #438 )
2023-04-03 14:01:02 +02:00
Denis Merigoux
d147238088
Apply suggestions by @altgr
2023-04-03 13:42:14 +02:00
adelaett
685785eaa3
adding assert_closed function
2023-04-03 11:20:19 +02:00
adelaett
f897226ffb
bindlib extension documentation
2023-04-03 10:57:52 +02:00
adelaett
84548769b4
renable optimization since the behavior of ite is now different
2023-04-03 10:56:44 +02:00
adelaett
cc1c018818
trace flag when needed
2023-04-03 10:56:13 +02:00
adelaett
2a50a06b36
invariant mli
2023-04-03 10:38:33 +02:00
Denis Merigoux
e80143b3ca
Last linting pass and update tests
2023-03-31 17:56:45 +02:00
Denis Merigoux
b3949ae15c
Update assets
2023-03-31 16:55:51 +02:00
Denis Merigoux
6d71d52a2e
Update tests and create disable_warnings option
2023-03-31 16:43:03 +02:00
adelaett
380a3a0c92
structural invariants
2023-03-31 16:03:51 +02:00
adelaett
e9ead93f3f
fix typing errors
2023-03-31 16:01:05 +02:00
adelaett
573df8416f
Merge branch 'master' into adelaett-withoutexceptionsfix
2023-03-31 15:52:06 +02:00
adelaett
272dc9e8b3
optimization reorg
2023-03-31 15:37:18 +02:00
Denis Merigoux
0057afc623
Fixing things after @JusBanuls' review pass on the code!
2023-03-31 15:34:50 +02:00
adelaett
beeecce091
correcting filter definition
2023-03-31 15:31:43 +02:00
Denis Merigoux
3d86a12261
Update error messages
2023-03-31 14:01:04 +02:00
Denis Merigoux
a7ee7074f9
Improve linting
2023-03-31 13:50:02 +02:00
Denis Merigoux
565aa23b8f
Implemented some lints
2023-03-31 11:47:44 +02:00
adelaett
69ac8ca929
implementation of fold, reduce, map & filter in without exceptions
...
Work in progress: not working for filter & map
2023-03-31 11:24:43 +02:00
Louis Gesbert
038861a52c
Generic mapping function across different ASTs
...
Used in lcalc/compile_with_exceptions only at the moment
2023-03-30 18:57:51 +02:00
Louis Gesbert
1208744c6b
EmptyError is no longer a literal
...
it's much simpler to handle it as an AST node, as that makes the literal
identical across all AST passes.
2023-03-30 18:54:50 +02:00
Denis Merigoux
3c364aa1fa
Progress on linting, bugguy unused field detection
2023-03-30 18:52:29 +02:00
Denis Merigoux
9d64150a47
Add linting
2023-03-30 16:09:03 +02:00
Denis Merigoux
fff2b78e31
Deleting linting which will have its own pass
2023-03-30 15:56:39 +02:00
Louis Gesbert
817dcb09fc
Simplify variable translation functions
2023-03-30 15:41:03 +02:00
Louis Gesbert
4973c74410
Remove date rounding mode from Operator.translate
2023-03-30 15:33:00 +02:00
Louis Gesbert
a415355a39
Rework the AST Gadt to allow merging of different ASTs
...
The phantom polymorphic variant qualifying AST nodes is reversed:
- previously, we were explicitely restricting each AST node to the passes where it belonged using a closed type (e.g. `[< dcalc | lcalc]`)
- now, each node instead declares the "feature" it provides using an open type (e.g. `[> 'Exceptions ]`)
- then the AST for a specific pass limits the features it allows with a closed type
The result is that you can mix and match all features if you wish,
even if the result is not a valid AST for any given pass. More
interestingly, it's now easier to write a function that works on
different ASTs at once (it's the inferred default if you don't write a
type restriction).
The opportunity was also taken to simplify the encoding of the
operators, which don't need a second type parameter anymore.
2023-03-30 15:30:08 +02:00
Denis Merigoux
04629f58cd
Merge branch 'master' into aides_logement_outre_mer
2023-03-30 15:14:06 +02:00
adelaett
61830bc348
fixing runtime merge errors
2023-03-30 11:02:35 +02:00
adelaett
6dee3874cc
Merge branch 'master' into adelaett-withoutexceptionsfix
2023-03-30 10:50:32 +02:00
adelaett
7174480153
start of the translation of fold
2023-03-30 10:39:23 +02:00
adelaett
3e8aae99fe
typo in the traslation of lets
2023-03-30 10:39:07 +02:00
adelaett
729d634744
fixing translation of arrays
2023-03-30 10:38:54 +02:00
Aymeric Fromherz
b85a199daa
Add support for let .. in constructions in Z3 backend ( #434 )
2023-03-29 06:41:40 +09:00
adelaett
df740eed05
fixing with-exceptions
2023-03-28 10:07:01 +02:00
adelaett
37dcd96e41
correct scope debug formatting
2023-03-28 09:55:25 +02:00
adelaett
4fe23c894d
driver debugging code
2023-03-28 09:55:01 +02:00
adelaett
f3abc23c32
fixings tests (90% atm)
2023-03-28 09:54:44 +02:00
adelaett
c3d9ee299f
without exception: removing thunking
2023-03-28 09:54:04 +02:00
Denis Merigoux
44d8c32b9f
C backend for Catala : the closure conversion strikes back ( #364 )
2023-03-28 09:53:22 +02:00
adelaett
ba1c83f278
correct printing of option type
2023-03-28 09:52:40 +02:00
Denis Merigoux
e4c4339856
Small fixes
2023-03-28 09:38:47 +02:00
Aymeric Fromherz
5f04e0efaf
cleanup
2023-03-28 13:08:24 +09:00
Aymeric Fromherz
c711b0b1d7
cleanup
2023-03-28 13:00:07 +09:00
Aymeric Fromherz
082caae498
Add support for let_in in Z3 backend
2023-03-28 12:48:44 +09:00
adelaett
9806eb7e0f
format for program
2023-03-23 13:46:17 +01:00
adelaett
72ceafd67c
scopes does not return optional terms
2023-03-23 10:45:44 +01:00
Denis Merigoux
8b2f3319b8
Merge remote-tracking branch 'origin/master' into aides_logement_outre_mer
2023-03-21 17:57:38 +01:00
Louis Gesbert
69be2f6ed8
Fix literate output of dates
2023-03-21 16:59:34 +01:00
Denis Merigoux
3122dd7821
Update assets
2023-03-21 16:10:00 +01:00
adelaett
78c0842dc6
optimization tests
2023-03-21 14:31:45 +01:00
adelaett
256adcae4b
rename invariant
2023-03-21 14:31:21 +01:00
Denis Merigoux
48ef5b8f21
Fix warning and update assets
2023-03-21 14:00:49 +01:00
Denis Merigoux
578091f196
Restore check
2023-03-21 13:49:16 +01:00
Denis Merigoux
aa8ab3be3d
Merge branch 'master' into c_backend
2023-03-21 12:14:10 +01:00
Denis Merigoux
1a7982d225
Better printing
2023-03-21 11:24:19 +01:00
Denis Merigoux
7f705beb07
Merge branch 'master' into aides_logement_outre_mer
2023-03-17 17:52:10 +01:00
adelaett
d2da1c3e43
advancing
2023-03-17 17:24:51 +01:00
adelaett
7c39ad953b
fix iota optmi
2023-03-17 17:23:10 +01:00
adelaett
8c66fabe6a
fix mission operators in translate
2023-03-17 17:20:46 +01:00
adelaett
9a34ee95b1
equality program
2023-03-17 17:20:35 +01:00
adelaett
61ad00f277
unit test infrastructure for optimization
2023-03-17 17:19:50 +01:00
adelaett
850a1fdb56
more optimization on fold
2023-03-17 11:34:52 +01:00
Louis Gesbert
db09eb0c42
Add date rounding option in scope ( #397 )
2023-03-17 10:14:36 +01:00
Denis Merigoux
056e84792d
Printing warning for undefined variables
2023-03-17 09:25:14 +01:00
Denis Merigoux
4fcdd005e0
Merge branch 'master' into aides_logement_outre_mer
2023-03-17 09:18:27 +01:00
Raphaël Monat
d5cd5b206a
Show conflicting date rounding mode declarations when they happen
2023-03-16 18:51:01 +01:00
Raphaël Monat
8981b21edb
Add test for date rounding option conflict
2023-03-16 17:20:14 +01:00
Raphaël Monat
51ea9d8cff
Format code
2023-03-16 17:20:14 +01:00
Raphaël Monat
d3c27799de
Raise exception when more than one rounding mode option has been specified
2023-03-16 17:20:13 +01:00
Raphaël Monat
1e1e3b538e
Simplify format
2023-03-16 17:20:13 +01:00
Raphaël Monat
b013f4257d
Update parser error message
2023-03-16 17:20:13 +01:00
Raphaël Monat
887ec00d0e
Add explicit match
2023-03-16 17:20:13 +01:00
Raphaël Monat
64fa32392f
Update generated files
2023-03-16 17:20:09 +01:00
adelaett
4038ea02be
rainbox parenthesis
2023-03-16 17:15:08 +01:00
adelaett
82af9e8305
unfolding more bugs
2023-03-16 17:14:33 +01:00
Raphaël Monat
5fc1e8e5d5
Fix operator printing
2023-03-16 16:55:55 +01:00
Raphaël Monat
7021c41f93
Add date rounding option within scopes
2023-03-16 16:55:55 +01:00
adelaett
26551434f2
correct monadic bind & map implementation
2023-03-14 18:36:05 +01:00
adelaett
91ed8e1f5d
special handling of the option constructor as a polymorphic one with custom typing rules
2023-03-14 18:31:32 +01:00
adelaett
366a0d952b
introducing new operators for handleing defaults
2023-03-14 18:30:58 +01:00
Louis Gesbert
abc5a00c2f
Compile LaTeX code using minted without the Python venv
...
This is a hack, but not a dirty one: a new command `catala pygmentize` is added,
which is just a wrapper around `pygmentize` that calls it with the proper lexers
defined.
The point is that this needs no installation, just a stock `pygmentize`
installation and the `catala` binary.
2023-03-14 17:35:22 +01:00
Denis Merigoux
74df4ee988
Merge branch 'master' into aides_logement_outre_mer
2023-03-14 14:10:09 +01:00
Louis Gesbert
f1e44619e0
LaTeX literate output: handle pygments coloration from within Catala
...
This leverages the embedded lexer already used for HTML output, and uses the
LaTeX pygments backend to colorise code directly, without the need for `minted`.
2023-03-13 22:33:48 +01:00
adelaett
4d3b021eef
finished the implementation, but a few issues are missing
2023-03-13 16:51:06 +01:00
Louis Gesbert
5282aec400
LaTeX output: start refactor
2023-03-13 14:44:34 +01:00