regnat
11b4947f07
Define operators used in the typing of patterns
...
Namely the type accepted by a pattern and the matching of a type against
a pattern
Fixes #9
2017-04-26 17:09:56 +02:00
regnat
7cb7a030d7
Trim margins
...
Latex default margins are sooo big
2017-04-26 17:08:16 +02:00
regnat
dea53df473
Add bibliography
...
Don't really kmow why it wasn't included
2017-04-26 17:07:43 +02:00
regnat
686e289832
Only allow constants as default values in patterns
...
This doesn't change the expressivity of the language, but makes the
typing easier.
2017-04-26 17:06:48 +02:00
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
75d164c873
Add type annotations for lambdas and let-recs
...
Those were already present in the typing rules, they are now added in
the syntax and the semantics
Fixes #5
2017-04-25 08:53:28 +02:00
regnat
b4d0e36856
semantics: fix missing rec in let semantics
2017-04-25 08:22:53 +02:00
regnat
4ecb8f3711
Replace p:e by λp.e
...
Fixes #7
2017-04-24 17:24:57 +02:00
regnat
eb5abd20f1
Fix typesetting in reduction contexts
2017-04-24 17:23:42 +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
8c933d3cb0
Remove typing judgements from semantics
...
Fixes #3
2017-04-24 16:49:34 +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
33e0bd61d0
str -> string
2017-04-24 16:29:20 +02:00
regnat
1b5d5748fe
Unify the typesetting of grammar
...
Fixes #1
2017-04-24 16:20:34 +02:00
regnat
923e4e1995
grammar: simplify access-path
...
Only expressions, no litteral field names
2017-04-24 15:12:04 +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
Beppe
ee2a7ac4f2
added style
2017-04-19 10:45:40 +02:00
regnat
f299ce6d76
fix makefile main target
2017-04-19 09:25:48 +02:00
regnat
8f08d41fce
Change the \orthplus symbol to a diamond
...
The old one was ugly ond too big
2017-04-11 14:56:20 +02:00
regnat
4b8bddc46e
Some explanations on the grammar
2017-04-11 14:01:42 +02:00
regnat
d25edab8f9
[WIP] Refactor everything into one big document
2017-04-11 12:01:24 +02:00
regnat
241bdd5e17
.latexmkrc: quote the evince name
...
This avoids a warning from latexmk
2017-04-11 11:17:45 +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
3547c7f43d
semantics: rewrite rules with \orthplus
2017-04-11 09:09:53 +02:00
regnat
375ac623f7
grammar: typo
2017-04-11 09:09:53 +02:00
regnat
fe2a116939
grammar: use orthplus for record values
2017-04-11 09:09:53 +02:00
regnat
4505512191
grammar: visual fix
2017-04-11 09:09:53 +02:00
regnat
e46d719895
grammar: update to match typing rules
2017-04-11 09:09:53 +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
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
