Commit Graph

1250 Commits

Author SHA1 Message Date
Denis Merigoux
9007eb4204
Apply suggestions by @altgr 2023-06-19 17:29:51 +02:00
Louis Gesbert
237dca2e75 Some commented code cleanup and clarifications 2023-06-19 16:36:09 +02:00
Denis Merigoux
420348beda Added a last TODO and put big example under CI 2023-06-18 21:38:00 +02:00
Denis Merigoux
b55d8c823b Closure conversion & hoisting working 2023-06-18 21:30:55 +02:00
Denis Merigoux
2ddbe93126 Bug identified 2023-06-18 18:15:29 +02:00
Denis Merigoux
a20adc0055 Closure hoisting (missing a bug on hardest case) 2023-06-18 18:08:18 +02:00
Denis Merigoux
2c45ca1599 More doc 2023-06-18 16:08:16 +02:00
Denis Merigoux
9cf55b0edd Closure env is unit if no extra variable captured 2023-06-18 15:49:02 +02:00
Louis Gesbert
52b1c25d50 Refactor CLI to use sub-commands
The upside of this is that each command can define specific flags ; there is a
small loss of backwards-compatibility in that the command needs to be the first
argument.

`catala --help` will now only show a summary of commands, with more specific
manpages shown on `catala CMD --help`.

Another point is that the plugin interface is extended to allow plugins to be
registered as subcommands and have their own flags (this will be very useful for
adding flags to the lazy/dot/explanation plugin that has many options).

Note that no efforts has yet been made to specialise the options, the previous
type was just made global for all subcommands.
2023-06-15 18:00:10 +02:00
Louis Gesbert
da59076223 Add a command-line option ('--use') for module linking 2023-06-15 17:58:46 +02:00
Louis Gesbert
ec97c386c3 Reformat + regen 2023-06-15 17:57:01 +02:00
Louis Gesbert
26c75af2ae Allow declaration of toplevel values without definition 2023-06-15 17:57:01 +02:00
Louis Gesbert
e224e87f71 Wip support for modules
(first working dynload test with compilation done by manual calls to ocaml)

A few pieces of the puzzle:

* Loading of interfaces only from Catala files
* Registration of toplevel values in modules compiled to OCaml, to allow access
  using dynlink
* Shady conversion from OCaml runtime values to/from Catala expressions, to
  allow interop (ffi) of compiled modules and the interpreter
2023-06-15 17:56:57 +02:00
Denis Merigoux
6962761774
Merge branch 'master' into closure_conversion 2023-06-15 17:56:41 +02:00
Louis Gesbert
2f2614c508 Use the AST mapper for scopelang-> dcalc 2023-06-15 17:55:52 +02:00
Louis Gesbert
2b7beeefb2 Rename 'IdentName' to 'Ident' 2023-06-15 17:55:49 +02:00
Denis Merigoux
3d3e735402
Nicer error message 2023-06-15 17:47:58 +02:00
Denis Merigoux
ed2891c761
Closure conversion should work now 2023-06-15 17:32:00 +02:00
Denis Merigoux
d850ac688a
Added operators for closure environment handling 2023-06-15 16:52:36 +02:00
Denis Merigoux
57abfbf2c7
Other pattern matching 2023-06-15 16:33:14 +02:00
Denis Merigoux
a3087ee163 Adding typing for closure env 2023-06-15 11:11:56 +02:00
Denis Merigoux
385e19b9e1 Formatting 2023-06-15 10:51:31 +02:00
Denis Merigoux
571c7c5d89
Correctly count number of var occurences 2023-06-14 11:39:27 +02:00
Denis Merigoux
42aaa1017d
Created minimal not working example and tame down beta-reduction 2023-06-14 11:18:39 +02:00
Denis Merigoux
2c9b56fb70
More agressive re-typing 2023-06-13 20:37:23 +02:00
Denis Merigoux
27bbe78438
Understanding a limitation 2023-06-13 20:10:42 +02:00
Aminata-Dev
10d147a8b1 Messages renamed to Message (lighter syntax) 2023-06-13 11:50:56 +02:00
Denis Merigoux
7072369b2d
Starting to work 2023-06-13 11:43:13 +02:00
Denis Merigoux
926c9436e3
Fix some bugs 2023-06-13 11:15:32 +02:00
Denis Merigoux
0e99d1598b
Continue closure conversion 2023-06-13 10:49:46 +02:00
Denis Merigoux
30eb3c0bdb
Better printing for types in typing error message 2023-06-13 09:55:48 +02:00
Denis Merigoux
84350b1593
Better typing error message 2023-06-13 09:07:42 +02:00
Denis Merigoux
26d53cc87f
Rainbow parenthesis for types 2023-06-13 08:59:33 +02:00
Aminata-Dev
5f9cb55e34 s 2023-06-12 17:00:10 +02:00
Denis Merigoux
45375dd7b5
Fix a bug in closure conversion 2023-06-12 15:21:06 +02:00
Denis Merigoux
cdae3e43ac
Improve names of temp variable in monadic pass 2023-06-12 15:02:08 +02:00
Louis Gesbert
b975e7c149 Cleanup commented code 2023-06-09 15:28:12 +02:00
Louis Gesbert
e4c1216848 Tweak whitespace in messages 2023-06-08 14:36:28 +02:00
Louis Gesbert
fcadd9808e Update tests with whitespace changes 2023-06-08 14:03:08 +02:00
Louis Gesbert
11730ce271 Repair indentation of log messages 2023-06-08 13:34:54 +02:00
Louis Gesbert
c564e70636 Correctly setup ocolor on all output channels
(and some cleanup of the remaining deps to ANSITerminal)
2023-06-08 12:14:11 +02:00
Louis Gesbert
16c93fbb0c Reformat 2023-06-08 12:14:11 +02:00
Louis Gesbert
deaf40761e Use ocolor instead of ANSITerminal 2023-06-08 12:11:55 +02:00
Louis Gesbert
7aa7bfb8fa
Fix most doc errors (#471) 2023-06-05 10:51:59 +02:00
Denis Merigoux
d1a836c646 Removing less precise message 2023-06-03 18:04:41 +02:00
Denis Merigoux
09bcefbcc1 Update tests 2023-06-03 18:02:57 +02:00
Denis Merigoux
91ee1122f6 Last typo 2023-06-03 15:32:38 +02:00
Denis Merigoux
79801292e9
Fix most doc errors 2023-06-02 17:17:45 +02:00
Denis Merigoux
ddee094783
Fix CI 2023-06-02 15:41:27 +02:00
Denis Merigoux
5d765676b5 Format rather than print 2023-06-02 10:58:03 +02:00
Denis Merigoux
d1210cc0e4 The thing compiles 2023-06-02 10:50:33 +02:00
Denis Merigoux
4e6efe08da All renamings done, on with actual refactor 2023-06-02 10:50:33 +02:00
Denis Merigoux
5f227933f3 Errors are now things to refactor [skip ci] 2023-06-02 10:50:33 +02:00
Denis Merigoux
0faa97b8fc Abstract messages interface 2023-06-02 10:50:29 +02:00
Denis Merigoux
4612920bf4
Merge branch 'master' into more_infos_in_logs 2023-06-01 17:38:41 +02:00
Denis Merigoux
94999dcc25
Correctly generate latex, nowrap option not working anymore? 2023-05-30 12:03:50 +02:00
Denis Merigoux
fa9f432e8b
Python runtime OK now 2023-05-26 17:08:26 +02:00
Denis Merigoux
8987d358e7
Implement the rest 2023-05-26 16:54:52 +02:00
Denis Merigoux
1f23f701bc
Move types 2023-05-26 16:03:26 +02:00
Louis Gesbert
209be6b758 Improve integration of marks into the main AST
Two interdependent changes here:
1. Enforce all instances of Shared_ast.gexpr to use the generic type for marks.
   This makes the interfaces a tad simpler to manipulate: you now write
   `('a, 'm) gexpr` rather than `('a, 'm mark) gexpr`.
2. Define a polymorphic `Custom` mark case for use by pass-specific annotations.
   And leverage this in the typing module
2023-05-17 17:37:00 +02:00
Louis Gesbert
fc531777c0 Rework and normalise the Marked interface
The module is renamed to `Mark`, and functions renamed to avoid redundancy:

`Marked.mark` is now `Mark.add`
`Marked.unmark` is now `Mark.remove`
`Marked.map_under_mark` is now simply `Mark.map`
etc.

`Marked.same_mark_as` is replaced by `Mark.copy`, but with the arguments
swapped (which seemed more convenient throughout)

Since a type `Mark.t` would indicate a mark, and to avoid confusion, the type
`Marked.t` is renamed to `Mark.ed` as a shorthand for `Mark.marked` ; this part
can easily be removed if that's too much quirkiness.
2023-05-17 17:37:00 +02:00
Louis Gesbert
558fcb6fef Build: remove unnecessary ppx on dcalc, lcalc
we only use `visitors` for positions on the surface AST
2023-05-17 14:08:32 +02:00
Louis Gesbert
ba52aae401 Cleanup: definitions.ml is not for values
A module without mli is ok as long as it only contains types

Here we already stretch it a bit with some functor applications, but having
toplevel values defeats the expectation that you can safely `open` this module.
2023-05-17 13:26:47 +02:00
Denis Merigoux
eae61256ef
Adhere to the GNU standard for error messages 2023-05-04 19:19:19 +02:00
Denis Merigoux
a5d4f54115
Push some fixes suggested by @altgr 2023-05-04 18:28:24 +02:00
Denis Merigoux
bcd91f5dea
Merge branch 'master' into aides_logement_outre_mer 2023-05-04 11:04:28 +02:00
Louis Gesbert
b1955bd9d4 Don't use a debug printing function for OCaml output 2023-05-02 16:48:01 +02:00
Louis Gesbert
5e26c5c83d Yet more printer improvements
- Fix the printer for scopes
- Improve the printer for struct types
- Remove `Print.expr'`. Use `Expr.format` as the function with simplified arguments instead.
2023-05-02 16:33:23 +02:00
Louis Gesbert
83e7a845fe Cleanup expr printer interface
- `Print.expr` no longer needs the context
- This removes the need for `expr ~debug` + `expr_debug` ;
  use `Print.expr` for normal (non-debug) output,
  and `Print.expr' ?debug ()` for possibly debug output.
- This improves consistency of debug expr output in many places
- Prints simplified operators (without type suffix) in non-verbose mode

(this patch also fixes some cases of `Expr.skip_wrappers` and leverages the
binder equality provided by Bindlib)
2023-05-02 13:32:16 +02:00
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