433 Commits

This Branch

This Branch

All Branches

Author	SHA1	Message	Date
Denis Merigoux	1030e4bc8d	Better type printing	2020-11-27 12:18:49 +01:00
Denis Merigoux	4709680557	Better cyclic dependencies error messages	2020-11-27 12:15:54 +01:00
Denis Merigoux	64cf1fd7cd	Test without func now pass!	2020-11-27 11:54:22 +01:00
Denis Merigoux	341ee710d8	Fixed translation bug	2020-11-27 11:37:21 +01:00
Denis Merigoux	3869f60669	WIP	2020-11-26 17:06:32 +01:00
Denis Merigoux	453c3afc91	Another example passing	2020-11-26 16:32:52 +01:00
Denis Merigoux	4a181ab4b7	First test passing	2020-11-26 16:22:08 +01:00
Denis Merigoux	69f0751037	Translate and typechecking simple exemple	2020-11-26 15:48:26 +01:00
Denis Merigoux	d3fe18aa18	Pretty-printing, fixing bugs in scope_to_dcalc	2020-11-26 13:38:42 +01:00
Denis Merigoux	e0f7baaa2b	Pretty printer	2020-11-26 10:38:13 +01:00
Denis Merigoux	b5e1e48fc8	Chain completed, onto debugging	2020-11-25 18:00:34 +01:00
Denis Merigoux	90de3c7c71	Completed translation from desugared to scope	2020-11-25 16:51:19 +01:00
Denis Merigoux	91f39a1b40	Progress: ... * used generative functors for Uids * priority tree now in Desugared.Ast	2020-11-25 14:35:31 +01:00
Denis Merigoux	89ef30b8da	Reestablished scope dependency computation	2020-11-25 11:53:56 +01:00
Denis Merigoux	b21737194f	Slowly connecting dots, missing a translation	2020-11-25 10:49:53 +01:00
Denis Merigoux	444d0bdf32	Reestablished desugaring	2020-11-25 10:10:27 +01:00
Denis Merigoux	bfdffb7b78	Progress on desugarin	2020-11-24 15:48:57 +01:00
Denis Merigoux	e1dfb52095	Added ints and operators to default calculus	2020-11-24 11:27:23 +01:00
Denis Merigoux	18eb757232	Changed bindings to take list of parameters	2020-11-24 10:28:39 +01:00
Denis Merigoux	bda8215023	Restored build	2020-11-23 22:26:53 +01:00
Denis Merigoux	b386549cf2	Enriched default calculus	2020-11-23 22:26:26 +01:00
Denis Merigoux	6232dd9f02	Git added translation (missing subs-scope-related rules)	2020-11-23 18:51:06 +01:00
Denis Merigoux	35dcd57b2b	Added tuples to default calculus	2020-11-23 16:12:45 +01:00
Denis Merigoux	e5078b1c98	Restored build	2020-11-23 12:20:38 +01:00
Denis Merigoux	39b1b4af08	Split UId	2020-11-23 11:42:29 +01:00
Denis Merigoux	aafd6045e2	Scope -> desugared	2020-11-23 10:52:32 +01:00
Denis Merigoux	8917383a92	Implemented interpreter	2020-11-23 10:44:06 +01:00
Denis Merigoux	0e7943b8f7	Fix makefile	2020-11-23 09:33:07 +01:00
Denis Merigoux	df2c0f1b01	Fixed github workflow	2020-11-23 09:27:55 +01:00
Denis Merigoux	0888422ead	Big code reorg with better dune config	2020-11-23 09:22:47 +01:00
Denis Merigoux	4c66a09895	Added bindlib as a dependency	2020-11-22 21:04:29 +01:00
Denis Merigoux	32800d3011	Added unionfind as a dependencu	2020-11-22 21:00:14 +01:00
Denis Merigoux	1c1f5beb4c	Implemented type inference for default calculus	2020-11-22 20:56:27 +01:00
Denis Merigoux	2575b56f20	Merge pull request #30 from CatalaLang/formalization ... Include catala formalisation	2020-11-20 10:58:17 +01:00
Denis Merigoux	8005f14ad4	Autoformat	2020-11-20 10:19:21 +01:00
Denis Merigoux	e498e6813b	Cleaned formal semantics	2020-11-20 10:17:11 +01:00
Denis Merigoux	f7421d3920	Fixed formalization	2020-11-20 10:12:09 +01:00
Denis Merigoux	7be9abd80a	Proved progress and preservation without default functions	2020-11-19 17:54:11 +01:00
Denis Merigoux	f09dc2ab5b	Still stuck at substitution preservation	2020-11-18 18:44:14 +01:00
Denis Merigoux	2f1011a7bd	Progress	2020-11-18 18:15:36 +01:00
Denis Merigoux	1dfb33f937	Tooling for substitution proof	2020-11-18 17:59:55 +01:00
Denis Merigoux	001ecddde4	More preservation lemmas	2020-11-18 16:26:12 +01:00
Denis Merigoux	a8ff671579	Fixed beta reduction rules for defaults	2020-11-18 15:38:33 +01:00
Denis Merigoux	42a46f417d	Progress proven	2020-11-17 21:08:38 +01:00
Denis Merigoux	75562acb1b	Checkpoint in proof	2020-11-17 15:54:56 +01:00
Denis Merigoux	88b45c7168	Progress in progress	2020-11-17 14:32:44 +01:00
Denis Merigoux	532365a707	Missing only the default case for progress	2020-11-17 12:15:44 +01:00
Denis Merigoux	891dccb6f8	Trying to prove progress	2020-11-17 11:01:09 +01:00
Denis Merigoux	076e2dce22	Finished writing stepper	2020-11-16 22:51:07 +01:00
Denis Merigoux	6bf935b8e9	Added beginning of F* formalization and fixed paper	2020-11-16 19:34:10 +01:00