thufschmitt/tix-papers
1
1
Fork 0
mirror of https://github.com/thufschmitt/tix-papers.git synced 2024-07-14 16:10:23 +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
8b54b5302e Add (very tiny) readme with a link to the compiled version 2017-05-12 16:39:27 +02:00
regnat
3ca6c5581a Add release.nix 
For hydra build
 2017-05-12 16:32:47 +02:00
regnat
19a9a21e79 Don't automatically show the result 2017-05-12 16:32:35 +02:00
regnat
1114b37de6 Add installphase for hydra builds 
Also takes care of declaring hydra products for download
 2017-05-12 16:29:37 +02:00
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