39 Commits

Author	SHA1	Message	Date
regnat	91f34b029a	typing: put typing rules in figures	2017-04-25 09:45:54 +02:00
regnat	2c83cb0d5c	typing: replace interfaces by argument annotations ... The return type annotation isn't really useful, so maybe we can drop it	2017-04-25 09:05:35 +02:00
regnat	ef5b2c837d	Add variable substitution in typecases ... This allows to explicit how to do occurence typing Fixes #6	2017-04-24 17:08:51 +02:00
regnat	b2c8475bde	Distinguish between let and let rec ... Fixes #4	2017-04-24 17:01:12 +02:00
regnat	e9d61da64c	Use only $e$, $v$ or $s$ for record fields ... - Remove the occurences of $l$ - Select the right one in a more consistent manner Fixes #2	2017-04-24 16:39:23 +02:00
regnat	06b84e27d7	typing: simplify the let rule ... For some reason, it was written in a really complicated way that had no reason to be	2017-04-21 15:25:13 +02:00
regnat	25c754ccea	Include typing rules into the global document	2017-04-21 15:09:16 +02:00
regnat	d25edab8f9	[WIP] Refactor everything into one big document	2017-04-11 12:01:24 +02:00
regnat	2f899731c1	latexmk: don't cd into directories ... but use a special output one instead	2017-04-11 11:17:01 +02:00
regnat	dcb5c94602	Make chktex happy on the header	2017-04-11 09:20:07 +02:00
regnat	8ca99c4f03	typing: explicit syntactic sugar for record types	2017-04-07 11:24:24 +02:00
regnat	50400c43e4	typing: split typing rules	2017-04-07 11:14:14 +02:00
regnat	2c2e885ad0	typing: add record rules to the type-system	2017-04-07 10:11:19 +02:00
regnat	99f594dd69	typing: add a grammar for types	2017-04-06 16:51:06 +02:00
regnat	8f9f7080b0	factorize header	2017-04-06 16:15:46 +02:00
regnat	54fd631f81	type-system: Change display of the B operator ... (The operator which assigns to each constant its type)	2017-04-06 15:42:57 +02:00
regnat	b67dfbbf9e	type-system: Fix display of pattern types	2017-04-06 15:42:57 +02:00
regnat	db5f5786d1	First draft of a type system for nix ... Currently no records nor builtins operators	2017-04-06 15:42:57 +02:00
regnat	38138ff7eb	typing: add rules for record access	2017-04-06 15:42:56 +02:00
regnat	1edf4be253	typing: Add labels to record typing rules	2017-04-06 15:42:56 +02:00
regnat	bcf70bac37	typing: add typing rule for merge	2017-04-06 15:42:56 +02:00
regnat	ff04f8828f	typing: fix orthplus typing rule ... Add constraint tha both expressions must be records	2017-04-06 15:42:56 +02:00
regnat	18fd26fc33	typing: remove typing rules for static labels ... They are included in the one for dynamic labels anyway	2017-04-06 15:42:56 +02:00
regnat	6c0a079eb4	typing: use \orthplus where possible	2017-04-06 15:42:56 +02:00
regnat	d73e484a2e	typing: Reformulate the motivation for \orthsum	2017-04-06 15:42:56 +02:00
regnat	42fbb241e5	typing: remove useless notation	2017-04-06 15:42:56 +02:00
regnat	ca303edd21	typing: define the grammar of records	2017-04-06 15:42:56 +02:00
regnat	77b4ae21ca	typing: change the undef constant ... Because the emptyset-like one wasn't a really good choice	2017-04-06 15:42:56 +02:00
regnat	80d36493c8	typing: rewrite some inference rules for records	2017-04-06 15:42:56 +02:00
regnat	2c37632b2e	typing: simplify the definition of \orthsum	2017-04-06 15:42:55 +02:00
regnat	f18467a881	typing: small nits	2017-04-06 15:42:55 +02:00
regnat	c1c445f169	Add some typing rules for dynamic records	2017-04-04 11:48:57 +02:00
regnat	3f91810f06	typing: reorganize records document	2017-04-04 10:58:21 +02:00
regnat	e85a9b3cd7	typing: define record subtyping	2017-04-04 10:55:33 +02:00
regnat	2dc5eb8277	typing: annotate the quasiconst arrow ... With the element the function is quasi-constant to	2017-04-04 10:47:21 +02:00
regnat	dd2b96102f	typing: fix inference rule for orthogonal merge	2017-04-04 09:42:16 +02:00
regnat	70dd7ff090	typing: add inference rules for static records	2017-04-04 09:37:29 +02:00
regnat	185a8a5736	typing: add part about records semantics	2017-04-04 09:37:11 +02:00
regnat	674bd88e0d	Add draft about the typing of records in nix	2017-04-01 12:28:19 +02:00