Update to core-spec documentation.

This update includes some wibbles to make Co_TyConAppCo clearer,
as well as the introduction of forms for AxiomRuleCo.

4 files changed, 53 insertions, 16 deletions

diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index f2799841dc..4c51a0559a 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -170,7 +170,7 @@ G |-arrow k1 -> k2 : k
 G |-co (->)_R g1 g2 : (s1 -> s2) ~R k (t1 -> t2)
 
 T /= (->)
-</ Ri // i /> = tyConRolesX R T
+</ Ri // i /> = take(length </ gi // i />, tyConRolesX R T)
 </ G |-co gi : si ~Ri ki ti // i />
 G |-app </ (si : ki) // i /> : tyConKind T ~> k
 --------------------------------- :: TyConAppCo
@@ -259,6 +259,19 @@ G |-ty t2 : k
 ------------------------------------------------------ :: AxiomInstCo
 G |-co C ind </ gi // i /> : T </ s2j // j /> ~R0 k t2
 
+G |-co g : s ~Nom k t
+------------------------- :: SubCo
+G |-co sub g : s ~Rep k t
+
+mu = M(i, </ Rj // j />, R')
+</ G |-ty ti : ki // i />
+</ G |-co gj : sj ~Rj k'j s'j // j />
+Just (t'1, t'2) = coaxrProves mu </ ti // i /> </ (sj, s'j) // j />
+G |-ty t'1 : k0
+G |-ty t'2 : k0
+--------------------------------------------------------------------- :: AxiomRuleCo
+G |-co mu </ ti // i /> </ gj // j /> : t'1 ~R' k0 t'2
+
 defn validRoles T ::  :: checkValidRoles :: 'Cvr_'
   {{ com Type constructor role validity, \coderef{typecheck/TcTyClsDecls.lhs}{checkValidRoles} }}
 by  
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index ca060f2f72..56594eca26 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -21,6 +21,7 @@ metavar alpha {{ tex \alpha }}, beta {{ tex \beta }} ::=
   {{ com Type-level variable names }}
 metavar N ::=   {{ com Type-level constructor names }}
 metavar K ::=   {{ com Term-level data constructor names }}
+metavar M ::=   {{ com Axiom rule names }}
 
 indexvar i, j, kk {{ tex k }}, aa {{ tex a }}, bb {{ tex b }}, cc {{ tex c }} ::= {{ com Indices to be used in lists }}
 
@@ -124,10 +125,13 @@ g {{ tex \gamma }} :: 'Coercion_' ::= {{ com Coercions, \coderef{types/Coercion.
   | t1 ==>! RA t2           ::   :: UnivCo        {{ com Universal coercion }}
   | sym g                   ::   :: SymCo         {{ com Symmetry }}
   | g1 ; g2                 ::   :: TransCo       {{ com Transitivity }}
+  | mu </ ti // i /> </ gj // j />
+                            ::   :: AxiomRuleCo   {{ com Axiom-rule application (for type-nats) }}
   | nth I g                 ::   :: NthCo         {{ com Projection (0-indexed) }}
     {{ tex \textsf{nth}_{[[I]]}\,[[g]] }}
   | LorR g                  ::   :: LRCo          {{ com Left/right projection }}
   | g t                     ::   :: InstCo        {{ com Type application }}
+  | sub g                   ::   :: SubCo         {{ com Sub-role --- convert nominal to representational }}
   | ( g )                   :: M :: Parens        {{ com Parentheses }}
   | t @ liftingsubst        :: M :: Lifted        {{ com Type lifted to coercion }}
 
@@ -152,6 +156,10 @@ axBranch, b :: 'CoAxBranch_' ::= {{ com Axiom branches, \coderef{types/TyCon.lhs
   | forall </ ni RAi // i /> . ( </ tj // j /> ~> s )  ::   :: CoAxBranch  {{ com Axiom branch }}
   | ( </ axBranchi // i /> ) [ ind ]                   :: M :: lookup      {{ com List lookup }}
 
+mu {{ tex \mu }} :: 'CoAxiomRule_' ::= {{ com CoAxiomRules, \coderef{types/CoAxiom.lhs}{CoAxiomRule} }}
+  | M ( I , role_list , R' )   ::  :: CoAxiomRule  {{ com Named rule, with parameter info }}
+    {{ tex {[[M]]}_{([[I]], [[ role_list ]], [[R']])} }}
+
 %% TYCONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 T :: 'TyCon_' ::= {{ com Type constructors, \coderef{types/TyCon.lhs}{TyCon} }}
@@ -212,6 +220,7 @@ liftingsubst :: 'LiftSubst_' ::= {{ com List of lifting substitutions }}
 ind, I {{ tex i }} :: 'Ind_' ::= {{ com Indices, numbers }}
   | i                           ::   :: index
   | length </ ti // i />        :: M :: length_t
+  | length </ gi // i />        :: M :: length_g
   | length </ axBranchi // i /> :: M :: length_axBranch
   | tyConArity T                :: M :: tyConArity
   | ind - 1                     :: M :: decrement
@@ -225,14 +234,15 @@ type_list :: 'TypeList_' ::= {{ com List of types }}
 
 RA {{ tex {\!\!\!{}_{\rho} } }} :: 'RoleAnnot_' ::= {{ com Role annotation }}
   | _ R                    :: M :: annotation
-  {{ tex {}_{[[R]]} }}
+  {{ tex {\!\!\!{}_{[[R]]} } }}
 
-role_list :: 'RoleList_' ::= {{ com List of roles }}
-  | </ Ri // , // i />     ::   :: List
-  | tyConRolesX R T        :: M :: tyConRolesX
-  | tyConRoles T           :: M :: tyConRoles
-  | ( role_list )          :: M :: Parens
-  | { role_list }          :: M :: Braces
+role_list {{ tex {\overline{\rho_j} }^j }} :: 'RoleList_' ::= {{ com List of roles }}
+  | </ Ri // , // i />       ::   :: List
+  | tyConRolesX R T          :: M :: tyConRolesX
+  | tyConRoles T             :: M :: tyConRoles
+  | ( role_list )            :: M :: Parens
+  | { role_list }            :: M :: Braces
+  | take ( ind , role_list ) :: M :: Take
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Terminals  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -298,6 +308,9 @@ terminals :: 'terminals_' ::=
   | validDcRoles ::   :: validDcRoles     {{ tex \textsf{validDcRoles} }}
   | -->          ::   :: steps            {{ tex \longrightarrow }}
   | coercionKind ::   :: coercionKind     {{ tex \textsf{coercionKind} }}
+  | take         ::   :: take             {{ tex \textsf{take}\! }}
+  | coaxrProves  ::   :: coaxrProves      {{ tex \textsf{coaxrProves} }}
+  | Just         ::   :: Just             {{ tex \textsf{Just} }}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Formulae  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -355,6 +368,9 @@ formula :: 'formula_' ::=
   | no other case matches              ::   :: no_other_case
     {{ tex \text{no other case matches} }}
   | t = coercionKind g                 ::   :: coercionKind
+  | Just ( t1 , t2 ) = coaxrProves mu </ si // i /> </ ( s'j , s''j ) // j />
+                                       ::   :: coaxrProves
+                          
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Subrules and Parsing  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index 5f2d806702..e726602397 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -30,7 +30,7 @@ System FC, as implemented in GHC\footnote{This
 document was originally prepared by Richard Eisenberg (\texttt{eir@cis.upenn.edu}),
 but it should be maintained by anyone who edits the functions or data structures
 mentioned in this file. Please feel free to contact Richard for more information.}\\
-\Large 9 September, 2013
+\Large 21 November, 2013
 \end{center}
 
 \section{Introduction}
@@ -181,6 +181,19 @@ as that would unduly clutter this presentation. Instead, as the list
 of incompatible branches can be computed at any time, it is checked for
 in the judgment $[[no_conflict]]$. See Section~\ref{sec:no_conflict}.
 
+Axiom rules, produced by the type-nats solver:
+
+\gram{\ottmu}
+
+\label{sec:axiom_rule}
+An axiom rule $[[mu]] = [[M(I, role_list, R')]]$ is an axiom name $[[M]]$, with a
+type arity $[[I]]$, a list of roles $[[role_list]]$ for its coercion parameters,
+and an output role $[[R']]$. The definition within GHC also includes a field named
+$[[coaxrProves]]$ which computes the output coercion from a list of types and
+a list of coercions. This is elided in this presentation, as we simply identify
+axiom rules by their names $[[M]]$. See also \coderef{typecheck/TcTypeNats.lhs}{mkBinAxiom}
+and \coderef{typecheck/TcTypeNats.lhs}{mkAxiom1}.
+
 \subsection{Type constructors}
 
 Type constructors in GHC contain \emph{lots} of information. We leave most of it out
@@ -246,12 +259,6 @@ as for strictness and exportability. See the source code for further information
 
 \ottdefnlintCoreExpr{}
 
-%\arraylabel{\coderef{coreSyn/CoreLint.lhs}{checkCaseAlts}} \\
-%\multicolumn{2}{l}{[[checkCaseAlts]] \text{ checks ordering and exhaustivity constr%aints}} \\
-
-%\end{array}
-%\]
-
 \begin{itemize}
 \item Some explication of \ottdrulename{Tm\_LetRec} is helpful: The idea behind the
 second premise ($[[</ G, G'i |-ty s'i : ki // i />]]$) is that we wish
@@ -308,7 +315,8 @@ In \ottdrulename{Co\_AxiomInstCo}, the use of $[[inits]]$ creates substitutions
 the first $i$ mappings in $[[ </ [ni |-> si] // i /> ]]$. This has the effect of 
 folding the substitution over the kinds for kind-checking.
 
-See Section~\ref{sec:tyconroles} for more information about $[[tyConRolesX]]$.
+See Section~\ref{sec:tyconroles} for more information about $[[tyConRolesX]]$, and
+see Section~\ref{sec:axiom_rules} for more information about $[[coaxrProves]]$.
 
 \subsection{Name consistency}
 
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index 71533e96f7..2b9c13d195 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf