Revert "Support for multiple signature files in scope."
[ghc.git] / docs / core-spec / README
1 GHC FORMALISM
2 =============
3
4 This directory contains the source code (and built pdf, for convenience) for a
5 formalism of the core language in GHC, properly called System FC. Though a
6 good handful of papers have been published about the language, these papers
7 paraphrase a slice of the language, useful for exposition. The document here
8 contains the official description of the language, as it is implemented in
9 GHC.
10
11 Building
12 --------
13
14 The built pdf is tracked in the git repository, so you should not need to build
15 unless you are editing the source code. If you do need to build, you will need
16 Ott [1] and LaTeX (with latexmk) in your path. Just run 'make'. 'make clean'
17 gets rid of all generated files, including the pdf.
18
19 Details
20 -------
21
22 The source files here are written in Ott [1], a language and toolset designed
23 to help in writing language formalisms. While the syntax of the language is a
24 little finnicky to write out at first, it is remarkably easy to make
25 incremental edits. Ott can be used to generate both LaTeX code and definitions
26 for proof assistants. Here, we use it only to produce LaTeX. Ott also has a
27 filter mode, where it processes a .mng file, looking for snippets enclosed
28 like [[ ... ]]. Ott will process the contents of these brackets and translate
29 into LaTeX math-mode code. Thus, the file core-spec.mng is the source for
30 core-spec.tex, which gets processed into core-spec.pdf.
31
32 The file CoreSyn.ott contains the grammar of System FC, mostly extracted from
33 compiler/coreSyn/CoreSyn.lhs. Here are a few pointers to help those of you
34 unfamiliar with Ott:
35
36 - The {{ ... }} snippets are called "homs", and they assist ott in translating
37 your notation to LaTeX. Three different homs are used:
38   * tex-preamble contains literal LaTeX code to be pasted into the output
39   * com marks a comment, which is rendered to the right of the structure being
40     defined
41   * tex marks a LaTeX typesetting of the structure being defined. It can use
42     [[ ... ]] to refer to metavariables used the structure definition.
43
44 - The </ ... // ... /> notation is used for lists. Please see the Ott manual
45   [2] for more info.
46
47 - Ott requires that all lexemes are separated by whitespace in their initial
48   definition.
49
50 - The M that appears between the :: on some lines means "meta". It is used for
51   a production that is not a proper constructor of the form being defined. For
52   example, the production ( t ) should be considered to be a type, but it is
53   not a separate constructor. Meta productions are not included when
54   typsetting the form with its productions.
55
56 - There are two special forms:
57   * The 'terminal' form contains productions for all terminal symbols that
58     require special typesetting through their tex homs.
59   * The 'formula' form contains productions for all valid formulae that can be
60     used in the premises of an inductive rule. (The 'judgement' production
61     refers to defined judgements in the rules.)
62
63 - See the Ott manual [2] for the 'parsing' section at the bottom. These rules
64   help disambiguate otherwise-ambiguous parses. Getting these right is hard,
65   so if you have trouble, you're not alone.
66
67 - In a few places, it is necessary to use an @ symbol to disambiguate parses. The
68   @ symbol is not typeset and is used solely for disambiguation. Feel free to use
69   it if necessary to disambiguate other parses.
70
71 The file CoreLint.ott contains inductively defined judgements for many of the
72 functions in compiler/coreSyn/CoreLint.lhs. Each judgement is labeled with an
73 abbreviation to distinguish it from the others. These abbreviations appear in
74 the source code right after a turnstile |-. The declaration for each judgment
75 contains a reference to the function it represents. Each rule is labeled with
76 the constructor in question, if applicable. Note that these labels are
77 mandatory in Ott.
78
79 If you need help with these files or do not know how to edit them, please
80 contact Richard Eisenberg (eir@cis.upenn.edu).
81
82 [1] http://www.cl.cam.ac.uk/~pes20/ott/
83 [2] http://www.cl.cam.ac.uk/~pes20/ott/ott_manual_0.21.2.pdf