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
bb5db91be9
semantics: Rewrite recursive lets using records
...
A let-binding which binds several variables now binds only one to a
record containing all the stuff.
This is probably not a good idea to use for the typing, but makes the
presentation more compact
(BTW, the old rule was incorrect)
2017-04-06 15:42:56 +02:00
regnat
e27fa80d59
grammar: distinguish ({meta-,}sytactic "..."
2017-04-06 15:42:56 +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
regnat
1bdbeb3bda
Add Makefile
...
The added makefile builds each pdf in its own folder with `latexmk`.
To add a new pdf, just add its path to the main rule.
2017-04-01 11:07:14 +02:00
regnat
9f6f9b90b0
grammar: add values definition
2017-03-30 14:28:11 +02:00
regnat
77148b18bf
semantics: add reduction contexts
2017-03-30 14:28:11 +02:00
regnat
de05377107
semantics: split beta-rule on pattern/not pattern
2017-03-30 14:28:11 +02:00
regnat
95fca72e53
semantics: change operators
...
According to beppe recommandation
2017-03-30 14:28:10 +02:00
regnat
60adb32726
semantics: expand ambiguous "fs" and "pfs"
2017-03-30 14:28:03 +02:00
regnat
472e5c3af4
grammar: add lists and constants as patterns
2017-03-29 17:06:09 +02:00
regnat
56aff4a304
some more cosmetic changes
2017-03-29 17:05:53 +02:00
regnat
c084e0b9a5
grammar: use "Cons" instead of "::" for lists
2017-03-29 16:57:58 +02:00
regnat
9fb063fefb
grammar: remove list syntax sugar
2017-03-29 16:50:59 +02:00
regnat
67d275fe83
add "seq" operator
2017-03-29 16:50:14 +02:00
regnat
c34072570a
explicitly uncurrify operators
2017-03-29 16:50:02 +02:00
regnat
a04c176a35
separate operators from expressions
...
(and clean the latex syntax)
2017-03-29 16:48:34 +02:00
regnat
5d85837489
grammar: visually separate syntax and meta-syntax
2017-03-29 16:34:46 +02:00
regnat
8085fb5d79
Merge branch 'master' of github.com:regnat/tix-papers
2017-03-29 16:02:45 +02:00
Beppe
409924a04f
quelques modifs
2017-03-29 12:31:58 +02:00
regnat
0caadfa2fd
grammar: add typeOf as a constant
2017-03-29 11:58:03 +02:00
regnat
fdee9f24ab
grammar : add some builtins as syntax constructs
2017-03-29 11:52:03 +02:00
regnat
7912d99a41
grammar: remove the "assert" construct
...
`assert e1; e2` is morally equivalent to `if e1 then ⊥ else e2`
2017-03-29 11:33:11 +02:00
regnat
e89129ee3d
semantics: replace "s_n" by x_n for readability
2017-03-29 10:38:01 +02:00