Commit f8b25c30 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu
Browse files

Update to core-spec documentation.

This update includes some wibbles to make Co_TyConAppCo clearer,
as well as the introduction of forms for AxiomRuleCo.
parent 5c904ba0
......@@ -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
......
......@@ -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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......
......@@ -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}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment