thufschmitt/tix-papers
1
1
Fork 0
mirror of https://github.com/thufschmitt/tix-papers.git synced 2024-08-16 16:20:47 +03:00
Code Issues Projects Releases Wiki Activity
105 Commits 8 Branches 0 Tags 1.2 MiB
master
Commit Graph

105 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
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