regnat
|
418a125a23
|
remove unneeded dependencies
|
2017-05-12 16:28:57 +02:00 |
|
regnat
|
914328e8ca
|
Remove \x/ syntax for meta-variables
Those are typeset in math mode anyway, so they can as well be written
$x$
|
2017-05-11 18:21:19 +02:00 |
|
regnat
|
56365fba22
|
slightly clean the header
|
2017-05-11 18:11:41 +02:00 |
|
regnat
|
b4a4e6f2aa
|
Fix make clean
|
2017-05-11 08:32:05 +02:00 |
|
regnat
|
1aaf025299
|
fix chktex-reported errors
|
2017-05-11 08:21:06 +02:00 |
|
regnat
|
5dc76e20f3
|
Add chktex config and makefile rule
|
2017-05-11 08:21:06 +02:00 |
|
regnat
|
cfa357647c
|
Remove definiton of the obsolete matchType symbol
|
2017-05-11 07:37:27 +02:00 |
|
regnat
|
2bd9a4ac58
|
typing: introduce typing judgements for patterns
|
2017-05-11 07:35:39 +02:00 |
|
regnat
|
51468d4d15
|
grammar: add typing annotations to patterns
And remove them from lambdas
|
2017-05-11 07:30:24 +02:00 |
|
regnat
|
864957720a
|
Add paragraph about the typing of the typecase
|
2017-04-27 12:24:23 +02:00 |
|
regnat
|
e8070bbb13
|
Add some explaination about pattern operators
Fixes #10
|
2017-04-27 10:41:10 +02:00 |
|
regnat
|
9e18af9de4
|
Rewrite the Semantics of pattern-matching
Using multi-fields records
This is basically a copy-paste of the semantic of pattern-matching of a
type.
Fixes #8
|
2017-04-27 08:56:52 +02:00 |
|
regnat
|
ee998adb40
|
Rewrite pattern typing operators with \eqdefa
|
2017-04-27 08:29:04 +02:00 |
|
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 |
|