Commit Graph

689 Commits

Author SHA1 Message Date
Denis Merigoux
ec03ad8892 Fixed list semantics to prove first case of big theorem 2021-02-08 13:51:56 +01:00
Denis Merigoux
f3a38eeab6 Beginning to attack last trickiest theorem 2021-02-08 12:24:51 +01:00
Denis Merigoux
e68d86a3cb Fist theorem proven 2021-02-08 10:17:38 +01:00
Denis Merigoux
71f3c29b26 Added silent variables in target lambda calculus 2021-02-08 10:03:57 +01:00
Denis Merigoux
08883e04a9 Beginning to attack first certification theorem 2021-02-07 22:38:04 +01:00
Denis Merigoux
774e31245b Translation defined, proof to come 2021-02-07 19:35:00 +01:00
Denis Merigoux
014056794d Beginning to write the translatio 2021-02-07 16:10:01 +01:00
Denis Merigoux
736c49507c Robust and complete proof of type safety for the lambda calculus 2021-02-07 15:36:30 +01:00
Denis Merigoux
8875408665 Preservation proven 2021-02-06 19:05:11 +01:00
Denis Merigoux
6df17f7039 Missing preservation only for lambda calculus 2021-02-06 18:01:17 +01:00
Denis Merigoux
6a8b0b6c88 Progress proven for lambda calculus 2021-02-05 17:29:45 +01:00
Denis Merigoux
7fb5a4280b Begin formalization of target lambda calculus 2021-02-05 15:28:26 +01:00
Denis Merigoux
02a6cbb966 Added new decret about the SMIC 2021-02-04 18:28:56 +01:00
Denis Merigoux
f2c4303f53 Update website assets make rules 2021-02-04 11:17:45 +01:00
Denis Merigoux
f685c9302f Added test suite for compiled code 2021-02-03 10:53:21 +01:00
Denis Merigoux
2730f76201 Fix assets scripts 2021-02-02 22:54:35 +01:00
Denis Merigoux
423e6aff10 Formalized compilation scheme and proved correctness on paper 2021-02-02 13:16:58 +01:00
Denis Merigoux
3dcba2fede Speed up compilation using batch let bindings 2021-02-01 23:35:15 +01:00
Denis Merigoux
b3c8b49a3b Fixed typo 2021-02-01 22:42:58 +01:00
Denis Merigoux
c212a1e2f8 Fixed makefile 2021-02-01 20:24:50 +01:00
Denis Merigoux
9c98afed6e Allow approximate merlin 2021-02-01 20:20:33 +01:00
Denis Merigoux
81462a3e8a Added version of allocations_familiales 2021-02-01 20:15:58 +01:00
Denis Merigoux
5c5dbc542f Js version of Allocations familiales 2021-02-01 20:09:16 +01:00
Denis Merigoux
d88ccc38f6 Switched scope functions input to struct instead of many arguments 2021-02-01 15:57:19 +01:00
Denis Merigoux
1faa35900b Improvements for the generated OCaml 2021-02-01 09:54:48 +01:00
Denis Merigoux
aed578d6df Dox fix 2021-01-30 18:00:49 +01:00
Denis Merigoux
647320d4aa Benchmark, randomness of inputs, bugs fixed 2021-01-30 17:54:05 +01:00
Denis Merigoux
e85b2bceaf Fix tests 2021-01-29 16:32:04 +01:00
Denis Merigoux
1d7a908646 Return type of Catala scope functions changed to structs 2021-01-29 16:24:20 +01:00
Denis Merigoux
a70868e7a1 Better generated ML code 2021-01-29 11:48:17 +01:00
Denis Merigoux
313ca065f4 Benchmarked the result on allocations familiales, it is fast enough 2021-01-28 23:46:39 +01:00
Denis Merigoux
617d19df24 Improved OCaml backend, made dev loop 2021-01-28 18:30:01 +01:00
Denis Merigoux
50bccd8d13 Generated OCaml has valid syntax 2021-01-28 13:58:59 +01:00
Denis Merigoux
27b6303982 Beginning compilation to OCaml 2021-01-28 00:28:28 +01:00
Denis Merigoux
f3cc01ef3c Merge branch 'master' into compiling_defaults 2021-01-27 22:11:53 +01:00
Denis Merigoux
26c2458df4 Update formalization in F* 2021-01-27 19:59:00 +01:00
Denis Merigoux
a0a37aceca
Merge pull request #75 from R1kM/master
Disambiguation syntax for fields and constructors. Fixes #74
2021-01-27 15:28:39 +01:00
Denis Merigoux
694170bd93 Disabled translation stub 2021-01-27 14:58:26 +01:00
Denis Merigoux
585031305e Added dummy implementation of compilation 2021-01-27 09:58:58 +01:00
Denis Merigoux
430ba0d429 Finished first draft of default compilation formalization 2021-01-27 09:58:58 +01:00
Denis Merigoux
6b1c6fad5d More compilation discussion 2021-01-27 09:58:58 +01:00
Denis Merigoux
a81a50334b Beginning formalization 2021-01-27 09:58:58 +01:00
Aymeric Fromherz
fec4334b49 Allow fully qualified enum names in matches 2021-01-26 11:41:20 -05:00
Aymeric Fromherz
2e71cc503c Fix typo in grammar 2021-01-26 10:47:48 -05:00
Aymeric Fromherz
f154ec15ad Add support for fully qualified enum elements 2021-01-26 10:38:10 -05:00
Aymeric Fromherz
e1ac9564c2 Add a few tests for fully qualified struct accesses 2021-01-25 23:08:30 -05:00
Aymeric Fromherz
f90db72c25 Handle fully qualified struct accesses during desugaring 2021-01-25 23:07:12 -05:00
Aymeric Fromherz
b10e93fc5f Add syntax for enum/struct constructors to AST and parser (doing nothing with them yet) 2021-01-25 22:32:31 -05:00
Aymeric Fromherz
ec1695e41e Add failing test for ambiguous struct fields 2021-01-25 22:31:48 -05:00
Denis Merigoux
5973c677cf
Merge pull request #72 from R1kM/master
Better structure for the testing framework
2021-01-25 09:30:56 +01:00