CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-20 08:47:14 +03:00
Code Issues Projects Releases Wiki Activity
1,039 Commits 41 Branches 8 Tags 60 MiB
ed51544a10
Commit Graph

1039 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Denis Merigoux
38f7b72604 Restored proof again 2021-02-21 14:27:10 +01:00
Denis Merigoux
dbc8133821 Found correct version of exception stepping theorem 2021-02-21 13:24:27 +01:00
Denis Merigoux
68c36b26a1 Making slow progress 2021-02-21 00:36:06 +01:00
Denis Merigoux
e926adf6f0 Added thunk to ease proof of substitution correctness 2021-02-20 22:38:10 +01:00
Denis Merigoux
2efdd71866 Restored the proof somewhat 2021-02-20 20:31:51 +01:00
Denis Merigoux
b3fd1c030a proof of typing_empty_can_be_extended 2021-02-20 11:41:48 +01:00
Denis Merigoux
5b92165867 Restored type safety of lambda calculus 2021-02-19 22:06:09 +01:00
Denis Merigoux
9b4466b836 Type safety of default calculus restoed 2021-02-19 19:01:23 +01:00
Denis Merigoux
6662a07bfd Making progress on default calculus 2021-02-19 15:09:39 +01:00
Denis Merigoux
21cf048a19 Starting transition to De Bruijn 2021-02-19 14:01:27 +01:00
Denis Merigoux
fb63c8afc8 Restore tests 2021-02-19 09:09:13 +01:00
Denis Merigoux
e9b134ab79 Progress on section121 after pair programming session 2021-02-18 18:18:34 +01:00
Denis Merigoux
cfd2a4bcc3 WIP 2021-02-18 16:12:23 +01:00
Denis Merigoux
c2dc8db6ac Fix list stepping semantics in both default and lambda calculus 2021-02-17 16:24:19 +01:00
Denis Merigoux
f5caa5d5fb Merge branch 'master' into certfication_proof 2021-02-17 15:32:38 +01:00
Denis Merigoux
daeb50212b
Merge pull request #77 from AltGr/gen-parser-msgs 
Generate parser.messages from dune
 2021-02-17 11:04:19 +01:00
Denis Merigoux
ea451bc46f Add rule to recreate the error message file from scratch 2021-02-17 10:57:48 +01:00
Denis Merigoux
716700c8be Merge branch 'master' into gen-parser-msgs 2021-02-17 10:45:43 +01:00
Denis Merigoux
da828a5304
Merge pull request #76 from AltGr/mlis 
Add .mlis for all of Catala
 2021-02-17 10:41:31 +01:00
Denis Merigoux
44a937630d Removed duplicate comments 2021-02-17 10:34:47 +01:00
Denis Merigoux
f70a4af7b4 More general theorem, second difficult case OK 2021-02-16 16:20:42 +01:00
Denis Merigoux
ddfc67af55 Prove small precedes lemma 2021-02-15 22:01:37 +01:00
Denis Merigoux
252748968a Fix name 2021-02-15 21:45:11 +01:00
Denis Merigoux
494ba820b0 Continue Section121 2021-02-15 21:41:31 +01:00
Denis Merigoux
35ae5ff39a Flesh out other case; more general theorem needed 2021-02-15 20:06:33 +01:00
Denis Merigoux
7711cad2f4 First case fully proven 2021-02-15 16:18:20 +01:00
Denis Merigoux
d7cfbb2eba First case of difficult translation proven 2021-02-15 14:18:55 +01:00
Denis Merigoux
9ffb0c134e Proved one complicated lift 2021-02-15 11:35:51 +01:00
Denis Merigoux
adf16489bf Back to simpler version of step commute 2021-02-14 23:25:29 +01:00
Denis Merigoux
e3e3896d0a Some progress 2021-02-14 22:47:40 +01:00
Denis Merigoux
3776362c67 More interface cleaning 2021-02-14 12:01:32 +01:00
Denis Merigoux
220169aea1 Clean surface mlis 2021-02-14 11:50:05 +01:00
Denis Merigoux
2b1c28302a Update makefile rule 2021-02-12 18:56:36 +01:00
Denis Merigoux
cbd2dc29d9 Merge branch 'master' into mlis 2021-02-12 18:50:10 +01:00
Denis Merigoux
af8a7b1104
Merge pull request #73 from CatalaLang/compiling_defaults 
Compilation of defaults into a pure lambda calculus
 2021-02-12 18:45:57 +01:00
Denis Merigoux
fe5c5d8165 Ready for push on exceptions stepping 2021-02-12 18:29:10 +01:00
Louis Gesbert
c628b31d12 Generate parser.messages from dune 
(and remove generated `parser_errors.ml` from git)
 2021-02-12 18:28:22 +01:00
Louis Gesbert
ece3525433 Reformat mlis 2021-02-12 18:16:06 +01:00
Louis Gesbert
5422107d6c Cleanup generated .mlis 2021-02-12 17:26:39 +01:00
Louis Gesbert
596e98b497 Cleanup surface/ast.mli 2021-02-12 17:26:39 +01:00
Louis Gesbert
70f4e46dcc Add some .mli files 
Generated: these would need cleanup, formatting, insertion of the doc
comments, and removal of non-shared values.
 2021-02-12 17:26:39 +01:00
Louis Gesbert
edd94dcc0e Rename directories to match the names of the libraries they contain 2021-02-12 17:26:39 +01:00
Denis Merigoux
f29bdeb4ac Missing default proof but now with typing and correct lift 2021-02-12 17:06:38 +01:00
Denis Merigoux
e8ed143663 Restored sanity to proof 2021-02-12 16:01:31 +01:00
Denis Merigoux
9773c11fb2 Fixed error propagation in lists 2021-02-12 15:02:40 +01:00
Denis Merigoux
eb0b702b4d Some progress 2021-02-12 11:02:47 +01:00
Denis Merigoux
dff14e67ca More proof progress 2021-02-11 18:49:40 +01:00
Denis Merigoux
cf88f12cdb Some work on the theorem 2021-02-10 19:29:43 +01:00
Denis Merigoux
d0e5e32854 Last case very difficult 2021-02-09 12:49:52 +01:00
Denis Merigoux
7ed0477303 Missing only last little case 2021-02-08 20:11:46 +01:00