summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--docs/core-spec/CoreLint.ott127
-rw-r--r--docs/core-spec/CoreSyn.ott35
-rw-r--r--docs/core-spec/OpSem.ott4
-rw-r--r--docs/core-spec/core-spec.mng77
-rw-r--r--docs/core-spec/core-spec.pdfbin346103 -> 354307 bytes
5 files changed, 197 insertions, 46 deletions
diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index 50b11ce7e7..3a3468d53b 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -30,7 +30,7 @@ G |-sbind n <- e
---------------------- :: NonRec
G |-bind n = e
-</ G |-sbind ni <- ei // i />
+</ G, </ ni // i /> |-sbind ni <- ei // i />
---------------------- :: Rec
G |-bind rec </ ni = ei // i />
@@ -38,50 +38,64 @@ defn G |- sbind n <- e :: :: lintSingleBinding :: 'SBinding_' {{ com Single bi
{{ tex [[G]] \labeledjudge{sbind} [[n]] [[<-]] [[e]] }}
by
-G |-tm e : t
+G; empty |-tm e : t
G |-name z_t ok
</ mi // i /> = fv(t)
</ mi elt G // i />
----------------- :: SingleBinding
G |-sbind z_t <- e
-defn G |- tm e : t :: :: lintCoreExpr :: 'Tm_'
+defn G ; D |-sjbind l vars <- e : t :: :: lintSingleBinding_joins :: 'SJBinding_' {{ com Single join binding typing, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding} }}
+ {{ tex [[G]];[[D]] \labeledjudge{sjbind} [[l]] \, [[vars]] [[<-]] [[e]] : [[t]] }}
+by
+
+</ G'j $ // j /> = inits(</ nj // j />)
+G, </ nj // j /> ; D |-tm e : t
+G |-label p/I_s ok
+</ G, G'j |-name nj ok // j />
+</ mj // j /> = fv(s)
+</ mj elt G // j />
+split_I s = </ sj // j /> t
+----------------- :: SingleBinding
+G; D |-sjbind p/I_s </ nj // j /> <- e : t
+
+defn G ; D |- tm e : t :: :: lintCoreExpr :: 'Tm_'
{{ com Expression typing, \coderef{coreSyn/CoreLint.lhs}{lintCoreExpr} }}
- {{ tex [[G]] \labeledjudge{tm} [[e]] : [[t]] }}
+ {{ tex [[G]]; [[D]] \labeledjudge{tm} [[e]] : [[t]] }}
by
x_t elt G
not (t is_a_coercion_type)
------------------ :: Var
-G |-tm x_t : t
+G; D |-tm x_t : t
t = literalType lit
------------------- :: Lit
-G |-tm lit : t
+G; D |-tm lit : t
-G |-tm e : s
+G; empty |-tm e : s
G |-co g : s k1~Rep k2 t
k2 elt { *, # }
------------------- :: Cast
-G |-tm e |> g : t
+G; D |-tm e |> g : t
-G |-tm e : t
+G; empty |-tm e : t
------------------- :: Tick
-G |-tm e {tick} : t
+G; D |-tm e {tick} : t
G' = G, alpha_k
G |-ki k ok
G' |-subst alpha_k |-> s ok
-G' |-tm e[alpha_k |-> s] : t
+G'; D |-tm e[alpha_k |-> s] : t
--------------------------- :: LetTyKi
-G |-tm let alpha_k = s in e : t
+G; D |-tm let alpha_k = s in e : t
G |-sbind x_s <- u
G |-ty s : k
k = * \/ k = #
-G, x_s |-tm e : t
+G, x_s ; D |-tm e : t
------------------------- :: LetNonRec
-G |-tm let x_s = u in e : t
+G; D |-tm let x_s = u in e : t
</ G'i $ // i /> = inits(</ zi_si // i />)
</ G, G'i |-ty si : ki // i />
@@ -89,54 +103,72 @@ G |-tm let x_s = u in e : t
no_duplicates </ zi // i />
G' = G, </ zi_si // i />
</ G' |-sbind zi_si <- ui // i />
-G' |-tm e : t
+G'; D |-tm e : t
------------------------ :: LetRec
-G |-tm let rec </ zi_si = ui // i /> in e : t
+G; D |-tm let rec </ zi_si = ui // i /> in e : t
+
+G; D |-sjbind l </ ni // i /> <- u : t
+G; D, l |-tm e : t
+------------------------------------------- :: JoinNonRec
+G; D |-tm join l </ ni // i /> = u in e : t
+
+no_duplicates </ li // i />
+D' = D, </ li // i />
+</ G; D' |-sjbind l </ nj // j /> <- ui : t // i />
+G; D' |-tm e : t
+------------------------------------------------------------- :: JoinRec
+G; D |-tm join rec </ li </ nj // j /> = ui // i /> in e : t
% lintCoreArg is incorporated in these next two rules
-G |-tm e : forall alpha_k.t
+G; empty |-tm e : forall alpha_k.t
G |-subst alpha_k |-> s ok
---------------- :: AppType
-G |-tm e s : t[alpha_k |-> s]
+G; D |-tm e s : t[alpha_k |-> s]
not (e2 is_a_type)
-G |-tm e1 : t1 -> t2
-G |-tm e2 : t1
+G; empty |-tm e1 : t1 -> t2
+G; empty |-tm e2 : t1
---------------- :: AppExpr
-G |-tm e1 e2 : t2
+G; D |-tm e1 e2 : t2
+
+p/I_s elt D
+split_I s = </ sj // j /> t
+</ G; empty |-tm ej : sj // j />
+--------------------- :: Jump
+G; D |-tm jump p/I_s </ ej // j /> : t
not (k is_a_coercion_type)
G |-ty t : k
-G, x_t |-tm e : s
+G, x_t; |-tm e : s
----------------- :: LamId
-G |-tm \x_t.e : t -> s
+G; D |-tm \x_t.e : t -> s
G |-ki k ok
-G,alpha_k |-tm e : t
+G,alpha_k; |-tm e : t
--------------------------- :: LamTy
-G |-tm \alpha_k.e : forall alpha_k. t
+G; D |-tm \alpha_k.e : forall alpha_k. t
phi = s1 k1~#k2 s2
G |-ki phi ok
-G,c_phi |-tm e : t
+G,c_phi; |-tm e : t
-------------------------------- :: LamCo
-G |-tm \c_phi.e : forall c_phi.t
+G; D |-tm \c_phi.e : forall c_phi.t
-G |-tm e : s
+G; empty |-tm e : s
s = * \/ s = #
G |-ty t : TYPE s2
-</ G, z_s; s |-altern alti : t // i />
+</ G, z_s; D; s |-altern alti : t // i />
---------------------------------------------------- :: Case
-G |-tm case e as z_s return t of </ alti // i /> : t
+G; D |-tm case e as z_s return t of </ alti // i /> : t
G |-co g : t1 k1~Nom k2 t2
-------------------- :: Coercion
-G |-tm g : t1 k1~#k2 t2
+G; D |-tm g : t1 k1~#k2 t2
G |-co g : t1 k1~Rep k2 t2
----------------------- :: CoercionRep
-G |-tm g : (~Rep#) k1 k2 t1 t2
+G; D |-tm g : (~Rep#) k1 k2 t1 t2
defn G |- name n ok :: :: lintSingleBinding_lintBinder :: 'Name_'
{{ com Name consistency check, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding\#lintBinder} }}
@@ -151,6 +183,19 @@ G |-name x_t ok
----------------- :: TyVar
G |-name alpha_k ok
+defn G |- label l ok :: :: lintSingleBinding_lintBinder_join :: 'Label_'
+ {{ com Label consistency check, \coderef{coreSyn/CoreLint.hs}{lintSingleBinding\#lintBinder} }}
+ {{ tex [[G]] \labeledjudge{label} [[l]] [[ok]] }}
+by
+
+G |- ty t : k
+k = * \/ k = #
+split_I t = </ si // i /> t'
+G |- ty t' : k'
+k' = * \/ k' = #
+----------------- :: Label
+G |-label p / I _ t ok
+
defn G |- bnd n ok :: :: lintBinder :: 'Binding_'
{{ com Binding consistency, \coderef{coreSyn/CoreLint.lhs}{lintBinder} }}
{{ tex [[G]] \labeledjudge{bnd} [[n]] [[ok]] }}
@@ -316,7 +361,7 @@ G |-ty t'2 : k0'
G |-co mu </ ti // i /> $ </ gj // j /> : t'1 k0 ~R' k0' t'2
defn G |- axk [ namesroles |-> gs ] ~> ( subst1 , subst2 ) :: :: check_ki :: 'AxiomKind_'
- {{ com Axiom argument kinding, \coderef{coreSyn/CoreLint.lhs}{check\_ki} }}
+ {{ com Axiom argument kinding, \coderef{coreSyn/CoreLint.lhs}{lintCoercion\#check\_ki} }}
{{ tex [[G]] \labeledjudge{axk} [ [[namesroles]] [[|->]] [[gs]] ] [[~>]] ([[subst1]], [[subst2]]) }}
by
@@ -477,19 +522,19 @@ G |-ty t : k
---------------------- :: Type
G |-subst z_k |-> t ok
-defn G ; s |- altern alt : t :: :: lintCoreAlt :: 'Alt_'
+defn G ; D ; s |- altern alt : t :: :: lintCoreAlt :: 'Alt_'
{{ com Case alternative consistency, \coderef{coreSyn/CoreLint.lhs}{lintCoreAlt} }}
- {{ tex [[G]];[[s]] \labeledjudge{alt} [[alt]] : [[t]] }}
+ {{ tex [[G]];[[D]];[[s]] \labeledjudge{alt} [[alt]] : [[t]] }}
by
-G |-tm e : t
+G; D |-tm e : t
--------------------- :: DEFAULT
-G; s |-altern _ -> e : t
+G; D; s |-altern _ -> e : t
s = literalType lit
-G |-tm e : t
+G; D |-tm e : t
---------------------------------------- :: LitAlt
-G; s |-altern lit -> e : t
+G; D; s |-altern lit -> e : t
T = dataConTyCon K
not (isNewTyCon T)
@@ -498,9 +543,9 @@ t2 = t1 {</ sj // j />}
</ G |-bnd ni ok // i />
G' = G, </ ni // i />
G' |-altbnd </ ni // i /> : t2 ~> T </ sj // j />
-G' |-tm e : t
+G'; D |-tm e : t
--------------------------------------- :: DataAlt
-G; T </ sj // j /> |-altern K </ ni // i /> -> e : t
+G; D; T </ sj // j /> |-altern K </ ni // i /> -> e : t
defn t' = t { </ si // , // i /> } :: :: applyTys :: 'ApplyTys_'
{{ com Telescope substitution, \coderef{types/Type.lhs}{applyTys} }}
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index c42e38a980..78118d532c 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -19,6 +19,7 @@ embed {{ tex-preamble
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
metavar x, c ::= {{ com Term-level variable names }}
+metavar p ::= {{ com Labels }}
metavar alpha {{ tex \alpha }}, beta {{ tex \beta }} ::=
{{ com Type-level variable names }}
metavar N ::= {{ com Type-level constructor names }}
@@ -45,6 +46,10 @@ n, m, aname {{ tex \alpha }}, xname {{ tex x }} :: 'Var_' ::= {{ com Variable na
| z $ :: M :: NoSupScript {{ com Name without an explicit type/kind }}
| K :: M :: DataCon {{ com Data constructor }}
+l :: 'Label_' ::= {{ com Labels for join points, also \coderef{basicTypes/Var.lhs}{Var} }}
+ | p / I _ t :: :: Label {{ com Label with join arity and type }}
+ {{ tex {[[p]]}_{[[I]]}^{[[t]]} }}
+
vars :: 'Vars_' ::= {{ com List of variables }}
| </ ni // , // i /> :: :: List
| fv ( t ) :: M :: fv_t
@@ -55,12 +60,18 @@ vars :: 'Vars_' ::= {{ com List of variables }}
| vars1 \inter vars2 :: M :: intersection
{{ tex [[vars1]] \cap [[vars2]] }}
+labels :: 'Labels_' ::= {{ com List of labels }}
+ | </ li // , // i /> :: :: List
+ | empty :: M :: empty
+
e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.lhs}{Expr} }}
| n :: :: Var {{ com \ctor{Var}: Variable }}
| lit :: :: Lit {{ com \ctor{Lit}: Literal }}
| e1 e2 :: :: App {{ com \ctor{App}: Application }}
+ | jump l </ ui // i /> :: :: Jump {{ com \ctor{App}: Jump }}
| \ n . e :: :: Lam {{ com \ctor{Lam}: Abstraction }}
| let binding in e :: :: Let {{ com \ctor{Let}: Variable binding }}
+ | join jbinding in e :: :: Join {{ com \ctor{Let}: Join binding }}
| case e as n return t of </ alti // | // i /> :: :: Case {{ com \ctor{Case}: Pattern match }}
| e |> g :: :: Cast {{ com \ctor{Cast}: Cast }}
| e { tick } :: :: Tick {{ com \ctor{Tick}: Internal note }}
@@ -78,6 +89,10 @@ binding :: 'Bind_' ::= {{ com Let-bindings, \coderef{coreSyn/CoreSyn.lhs}{Bind}
| n = e :: :: NonRec {{ com \ctor{NonRec}: Non-recursive binding }}
| rec </ ni = ei // ;; // i /> :: :: Rec {{ com \ctor{Rec}: Recursive binding }}
+jbinding :: 'JoinBind_' ::= {{ com Join bindings, also \coderef{coreSyn/CoreSyn.lhs}{Bind} }}
+ | l </ ni // i /> = e :: :: NonRec {{ com \ctor{NonRec}: Non-recursive binding }}
+ | rec </ li </ nij // j /> = ei // i /> :: :: Rec {{ com \ctor{Rec}: Recursive binding }}
+
alt :: 'Alt_' ::= {{ com Case alternative, \coderef{coreSyn/CoreSyn.lhs}{Alt} }}
| Kp </ ni // i /> -> e :: :: Alt {{ com Constructor applied to fresh names }}
@@ -214,6 +229,12 @@ G {{ tex \Gamma }} :: 'LintM_Bindings_' ::= {{ com List of bindings, \coderef{co
| </ Gi // , // i /> :: :: Concat {{ com Context concatenation }}
| vars_of binding :: M :: VarsOf {{ com \coderef{coreSyn/CoreSyn.lhs}{bindersOf} }}
+D {{ tex \Delta }} :: 'LintM_JoinBindings_' ::= {{ com List of join bindings, \coderef{coreSyn/CoreLint.lhs}{LintM} }}
+ | l :: :: Binding {{ com Single binding }}
+ | </ Di // , // i /> :: :: Concat {{ com Context concatenation }}
+ | empty :: M :: Empty {{ com Empty context }}
+ | labels_of binding :: M :: LabelsOf {{ com \coderef{coreSyn/CoreSyn.lhs}{bindersOf} }}
+
O {{ tex \Omega }} :: 'VarEnv_Role_' ::= {{ com Mapping from type variables to roles }}
| </ ni : Ri // i /> :: :: List {{ com List of bindings }}
| O1 , O2 :: M :: Concat {{ com Concatenate two lists }}
@@ -255,6 +276,9 @@ ind, I {{ tex i }} :: 'Ind_' ::= {{ com Indices, numbers }}
| 1 :: M :: one
| 2 :: M :: two
+terms :: 'Terms_' ::= {{ com List of terms }}
+ | </ ei // i /> :: :: List
+
types :: 'Types_' ::= {{ com List of types }}
| </ ti // i /> :: :: List
@@ -294,9 +318,11 @@ role_list {{ tex {\overline{\rho_j} }^j }} :: 'RoleList_' ::= {{ com List of rol
terminals :: 'terminals_' ::=
| \ :: :: lambda {{ tex \lambda }}
| let :: :: let {{ tex \keyword{let} }}
+ | join :: :: join {{ tex \keyword{join} }}
| in :: :: key_in {{ tex \keyword{in} }}
| rec :: :: rec {{ tex \keyword{rec} }}
| and :: :: key_and {{ tex \keyword{and} }}
+ | jump :: :: jump {{ tex \keyword{jump} }}
| case :: :: case {{ tex \keyword{case} }}
| of :: :: of {{ tex \keyword{of} }}
| -> :: :: arrow {{ tex \to }}
@@ -317,6 +343,7 @@ terminals :: 'terminals_' ::=
| ok :: :: ok {{ tex \textsf{ ok} }}
| no_duplicates :: :: no_duplicates {{ tex \textsf{no\_duplicates } }}
| vars_of :: :: vars_of {{ tex \textsf{vars\_of } }}
+ | split :: :: split {{ tex \mathop{\textsf{split} } }}
| not :: :: not {{ tex \neg }}
| isUnLiftedTyCon :: :: isUnLiftedTyCon {{ tex \textsf{isUnLiftedTyCon} }}
| compatibleUnBoxedTys :: :: compatibleUnBoxedTys {{ tex \textsf{compatibleUnBoxedTys} }}
@@ -366,6 +393,8 @@ terminals :: 'terminals_' ::=
| Just :: :: Just {{ tex \textsf{Just} }}
| \\ :: :: newline {{ tex \\ }}
| classifiesTypeWithValues :: :: ctwv {{ tex \textsf{classifiesTypeWithValues} }}
+ | 0 :: :: zero {{ tex 0 }}
+ | +1 :: :: succ {{ tex +1 }}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Formulae %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -375,6 +404,7 @@ formula :: 'formula_' ::=
| judgement :: :: judgement
| formula1 ... formulai :: :: dots
| G1 = G2 :: :: context_rewrite
+ | D1 = D2 :: :: join_context_rewrite
| t1 = t2 :: :: type_rewrite
| t1 /= t2 :: :: type_inequality
| e1 /=e e2 :: :: expr_inequality
@@ -384,6 +414,7 @@ formula :: 'formula_' ::=
| g1 = g2 :: :: co_rewrite
| no_duplicates </ zi // i /> :: :: no_duplicates_name
| no_duplicates </ bindingi // i /> :: :: no_duplicates_binding
+ | no_duplicates </ li // i /> :: :: no_duplicates_label
| not formula :: :: not
| isUnLiftedTyCon T :: :: isUnLiftedTyCon
| compatibleUnBoxedTys t1 t2 :: :: compatibleUnBoxedTys
@@ -395,6 +426,7 @@ formula :: 'formula_' ::=
}{\quad [[formula2]]} \end{array} }}
| ( formula ) :: :: parens
| n elt G :: :: context_inclusion
+ | l elt D :: :: join_context_inclusion
| vars1 = vars2 :: :: vars_rewrite
| </ Gi $ // i /> = inits ( </ nj // j /> ) :: :: context_folding
| </ substi $ // i /> = inits ( </ [ nj |-> tj ] // j /> ) :: :: subst_folding
@@ -436,6 +468,8 @@ formula :: 'formula_' ::=
| mu1 = mu2 :: :: mu_rewrite
| classifiesTypeWithValues k :: :: classifies_type_with_values
| z elt vars :: :: in_vars
+ | split _ I s = types :: :: split_type
+ {{ tex \mathop{\textsf{split} }_{[[I]]} [[s]] = [[types]] }}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Subrules and Parsing %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -461,6 +495,7 @@ Subst_TyMapping <= Type_TySubstListPost
Subst_TmMapping <= Type_TySubstListPost
Expr_Type <= formula_e_rewrite
+Expr_Jump <= Expr_Apps
Coercion_TyConAppCo <= Coercion_AppCo
diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott
index 8fb9b0e068..03be476bbb 100644
--- a/docs/core-spec/OpSem.ott
+++ b/docs/core-spec/OpSem.ott
@@ -13,6 +13,10 @@
% point for an analysis of FC's operational semantics. If you don't want to
% worry about mutual recursion (and who does?), you can even drop the
% environment S.
+%
+% Join points are ignored here because operationally they work exactly the same
+% as regular bindings. Simply read "join" as "let" and "jump" as application to
+% see how a (well-typed!) program should run.
grammar
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index d1d89055e7..580032129d 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -89,6 +89,10 @@ variables:
\ottn
}
+\gram{
+\ottl
+}
+
We sometimes omit the type/kind annotation to a variable when it is obvious from context.
\subsection{Expressions}
@@ -112,13 +116,39 @@ is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{coreSyn/CoreSy
\item Types and coercions can only appear on the right-hand-side of an application.
\item The $[[t]]$ form of an expression must not then turn out to be a coercion.
In other words, the payload inside of a \texttt{Type} constructor must not turn out
-to be built with \texttt{CoercionTy}.
+to be built with \texttt{CoercionTy}.
+\item Join points (introduced by $[[join]]$ expressions) follow the invariants
+laid out in \verb|Note [Invariants on join points]| in
+\ghcfile{coreSyn/CoreSyn.lhs}:
+\begin{enumerate}
+ \item All occurences must be tail calls. This is enforced in our typing
+ rules using the label environment $[[D]]$.
+ \item Each join point has a \emph{join arity}. In this document, we write
+ each label as $[[p/I_t]]$ for the name $[[p]]$, the type $[[t]]$, and the
+ join arity $[[I]]$. The right-hand side of the binding must begin with at
+ least $[[I]]$ lambdas. This is enforced implicitly in
+ \ottdrulename{Tm\_JoinNonRec} and \ottdrulename{Tm\_JoinRec} by the use of
+ $[[split]]$ meta-function.
+ \item If the binding is recursive, then all other bindings in the recursive
+ group must be join points. We enforce this in our reformulation of the
+ grammar; in the actual AST, a $[[join]]$ is simply a $[[let]]$ where each
+ identifier is flagged as a join id, so this invariant requires that this
+ flag must be consistent across a recursive binding.
+ \item The binding's type must not be polymorphic in its return type. This
+ is expressed in \ottdrulename{Label\_Label}; see
+ Section~\ref{sec:name_consistency}.
+\end{enumerate}
+
\end{itemize}
Bindings for $[[let]]$ statements:
\gram{\ottbinding}
+Bindings for $[[join]]$ statements:
+
+\gram{\ottjbinding}
+
Case alternatives:
\gram{\ottalt}
@@ -275,15 +305,21 @@ synonym for $[[TYPE 'Unlifted]]$.
\section{Contexts}
The functions in \ghcfile{coreSyn/CoreLint.lhs} use the \texttt{LintM} monad.
-This monad contains a context with a set of bound variables $[[G]]$. The
-formalism treats $[[G]]$ as an ordered list, but GHC uses a set as its
+This monad contains a context with a set of bound variables $[[G]]$ and a set
+of bound labels $[[D]]$. The formalism treats $[[G]]$ and $[[D]]$ as ordered
+lists, but GHC uses sets as its
representation.
\gram{
\ottG
}
-We assume the Barendregt variable convention that all new variables are
+\gram{
+\ottD
+}
+
+We assume the Barendregt variable convention that all new variables and labels
+are
fresh in the context. In the implementation, of course, some work is done
to guarantee this freshness. In particular, adding a new type variable to
the context sometimes requires creating a new, fresh variable name and then
@@ -313,12 +349,29 @@ Here is the definition of $[[vars_of]]$, taken from \coderef{coreSyn/CoreSyn.lhs
\end{array}
\]
+Here is the definition of $[[split]]$, which has no direct analogue in the
+source but simplifies the presentation here:
+
+\[
+\begin{array}{ll}
+[[split]]_0 [[t]] &= [[t]] \\
+[[split]]_n ([[s -> t]]) &= [[s]] \; ([[split]]_{n-1} [[t]]) \\
+[[split]]_n ([[forall alpha _ k . t]]) &= [[k]] \; ([[split]]_{n-1} [[t]])
+\end{array}
+\]
+
+The idea is simply to peel off the leading $i$ argument types (which may be
+kinds for type arguments) from a given type and return them in a sequence, with
+the return type (given $i$ arguments) as the final element of the sequence.
+
\subsection{Binding consistency}
\ottdefnlintXXbind{}
\ottdefnlintSingleBinding{}
+\ottdefnlintSingleBindingXXjoins{}
+
In the GHC source, this function contains a number of other checks, such
as for strictness and exportability. See the source code for further information.
@@ -376,11 +429,19 @@ See Section~\ref{sec:tyconroles} for more information about $[[tyConRolesX]]$, a
see Section~\ref{sec:axiom_rules} for more information about $[[coaxrProves]]$.
\subsection{Name consistency}
+\label{sec:name_consistency}
-There are two very similar checks for names, one declared as a local function:
+There are three very similar checks for names, two performed as part of
+\coderef{coreSyn/CoreLint.hs}{lintSingleBinding}:
\ottdefnlintSingleBindingXXlintBinder{}
+\ottdefnlintSingleBindingXXlintBinderXXjoin{}
+
+The point of the extra checks on $[[t']]$ is that a join point's type cannot be
+polymorphic in its return type; see \texttt{Note [The polymorphism rule of join
+points]} in \ghcfile{coreSyn/CoreSyn.hs}.
+
\ottdefnlintBinder{}
\subsection{Substitution consistency}
@@ -477,6 +538,12 @@ Also note that this semantics implements call-by-name, not call-by-need. So
while it describes the operational meaning of a term, it does not describe what
subexpressions are shared, and when.
+\subsection{Join points}
+Dealing with join points properly here would be cumbersome and pointless, since
+by design they work no differently than functions as far as FC is concerned.
+Reading $[[join]]$ as $[[let]]$ and $[[jump]]$ as application should tell you
+all need to know.
+
\subsection{Operational semantics rules}
\ottdefnstep{}
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index dde6c9eeba..1e139115cd 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf
Binary files differ
View Lorry Controller Status