Added the docs/core-spec README

2 files changed, 83 insertions, 2 deletions

diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index 22949eddf3..b142901ede 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -115,8 +115,6 @@ G |-ty t : k2
 ---------------------------------------------------- :: Case
 G |-tm case e as z_s return t of </ alti // i /> : t
 
-% Type case of lintCoreExpr omitted because it is irrelevant
-
 G |-co g : t1 ~#k t2
 -------------------- :: Coercion
 G |-tm g : t1 ~#k t2
diff --git a/docs/core-spec/README b/docs/core-spec/README
new file mode 100644
index 0000000000..e193955490
--- /dev/null
+++ b/docs/core-spec/README
@@ -0,0 +1,83 @@
+GHC FORMALISM
+=============
+
+This directory contains the source code (and built pdf, for convenience) for a
+formalism of the core language in GHC, properly called System FC. Though a
+good handful of papers have been published about the language, these papers
+paraphrase a slice of the language, useful for exposition. The document here
+contains the official description of the language, as it is implemented in
+GHC.
+
+Building
+--------
+
+The built pdf is tracked in the git repository, so you should not need to build
+unless you are editing the source code. If you do need to build, you will need
+Ott [1] and LaTeX (with latexmk) in your path. Just run 'make'. 'make clean'
+gets rid of all generated files, including the pdf.
+
+Details
+-------
+
+The source files here are written in Ott [1], a language and toolset designed
+to help in writing language formalisms. While the syntax of the language is a
+little finnicky to write out at first, it is remarkably easy to make
+incremental edits. Ott can be used to generate both LaTeX code and definitions
+for proof assistants. Here, we use it only to produce LaTeX. Ott also has a
+filter mode, where it processes a .mng file, looking for snippets enclosed
+like [[ ... ]]. Ott will process the contents of these brackets and translate
+into LaTeX math-mode code. Thus, the file core-spec.mng is the source for
+core-spec.tex, which gets processed into core-spec.pdf.
+
+The file CoreSyn.ott contains the grammar of System FC, mostly extracted from
+compiler/coreSyn/CoreSyn.lhs. Here are a few pointers to help those of you
+unfamiliar with Ott:
+
+- The {{ ... }} snippets are called "homs", and they assist ott in translating
+your notation to LaTeX. Three different homs are used:
+  * tex-preamble contains literal LaTeX code to be pasted into the output
+  * com marks a comment, which is rendered to the right of the structure being
+    defined
+  * tex marks a LaTeX typesetting of the structure being defined. It can use
+    [[ ... ]] to refer to metavariables used the structure definition.
+
+- The </ ... // ... /> notation is used for lists. Please see the Ott manual
+  [2] for more info.
+
+- Ott requires that all lexemes are separated by whitespace in their initial
+  definition.
+
+- The M that appears between the :: on some lines means "meta". It is used for
+  a production that is not a proper constructor of the form being defined. For
+  example, the production ( t ) should be considered to be a type, but it is
+  not a separate constructor. Meta productions are not included when
+  typsetting the form with its productions.
+
+- There are two special forms:
+  * The 'terminal' form contains productions for all terminal symbols that
+    require special typesetting through their tex homs.
+  * The 'formula' form contains productions for all valid formulae that can be
+    used in the premises of an inductive rule. (The 'judgement' production
+    refers to defined judgements in the rules.)
+
+- See the Ott manual [2] for the 'parsing' section at the bottom. These rules
+  help disambiguate otherwise-ambiguous parses. Getting these right is hard,
+  so if you have trouble, you're not alone.
+
+- In one place, it was necessary to use an @ symbol to disambiguate parses. The
+  @ symbol is not typeset and is used solely for disambiguation. Feel free to use
+  it if necessary to disambiguate other parses.
+
+The file CoreLint.ott contains inductively defined judgements for many of the
+functions in compiler/coreSyn/CoreLint.lhs. Each judgement is labeled with an
+abbreviation to distinguish it from the others. These abbreviations appear in
+the source code right after a turnstile |-. The declaration for each judgment
+contains a reference to the function it represents. Each rule is labeled with
+the constructor in question, if applicable. Note that these labels are
+mandatory in Ott.
+
+If you need help with these files or do not know how to edit them, please
+contact Richard Eisenberg (eir@cis.upenn.edu).
+
+[1] http://www.cl.cam.ac.uk/~pes20/ott/
+[2] http://www.cl.cam.ac.uk/~pes20/ott/ott_manual_0.21.2.pdf
\ No newline at end of file