Fix the formal operational semantics (#10121)

This adapts the work of Christiaan Baaij to present a sensible
operational semantics for FC with mutual recursion.

5 files changed, 48 insertions, 30 deletions

diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index 6015731257..7058e8a113 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -209,7 +209,7 @@ G |-co z_(s ~R#k t) : s ~Rep k t
 
 G |-ty t1 : k1
 G |-ty t2 : k2
-R <= Phant \/ not (k1 <: OpenKind) \/ not (k2 <: OpenKind) \/ compatibleUnBoxedTys t1 t2
+R <= Ph \/ not (k1 <: OpenKind) \/ not (k2 <: OpenKind) \/ compatibleUnBoxedTys t1 t2
 ------------------------------------------------------------------------ :: UnivCo
 G |-co t1 ==>!_R t2 : t1 ~R k2 t2
 
@@ -276,7 +276,7 @@ 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  
+by
 
 </ Ki // i /> = tyConDataCons T
 </ Rj // j /> = tyConRoles T
@@ -341,7 +341,7 @@ Nom <= R
 R <= Ph
 
 ------- :: Refl
-R <= R 
+R <= R
 
 defn G |- ki k ok ::  :: lintKind :: 'K_'
   {{ com Kind validity, \coderef{coreSyn/CoreLint.lhs}{lintKind} }}
@@ -352,7 +352,7 @@ G |-ty k : BOX
 -------------- :: Box
 G |-ki k ok
 
-defn G |- ty t : k ::  :: lintType :: 'Ty_'  
+defn G |- ty t : k ::  :: lintType :: 'Ty_'
   {{ com Kinding, \coderef{coreSyn/CoreLint.lhs}{lintType} }}
   {{ tex [[G]] \labeledjudge{ty} [[t]] : [[k]] }}
 by
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index d64667af18..247fd05ae3 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -69,10 +69,12 @@ e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.lhs}{Expr} }}
   | ( e )                                        :: M :: Parens {{ com Parenthesized expression }}
   | e </ ui // i />                              :: M :: Apps {{ com Nested application }}
   | S ( n )                                      :: M :: Lookup {{ com Lookup in the runtime store }}
+  | \\ e                                         :: M :: Newline
+    {{ tex \qquad \\ \multicolumn{1}{r}{[[e]]} }}
 
 binding :: 'Bind_' ::= {{ com Let-bindings, \coderef{coreSyn/CoreSyn.lhs}{Bind} }}
   | n = e                         ::   :: NonRec  {{ com Non-recursive binding }}
-  | rec </ ni = ei // and // i /> ::   :: Rec     {{ com Recursive binding }}
+  | rec </ ni = ei // ;; // i />  ::   :: Rec     {{ com Recursive binding }}
 
 alt :: 'Alt_' ::= {{ com Case alternative, \coderef{coreSyn/CoreSyn.lhs}{Alt} }}
   | Kp </ ni // i /> -> e    ::   :: Alt  {{ com Constructor applied to fresh names }}
@@ -265,6 +267,7 @@ terminals :: 'terminals_' ::=
     {{ tex \twoheadrightarrow\!\!\!\!\!\! \raisebox{-.3ex}{!} \,\,\,\,\, }}
   | sym          ::   :: sym              {{ tex \textsf{sym} }}
   | ;            ::   :: trans            {{ tex \fatsemi }}
+  | ;;           ::   :: semi             {{ tex ; }}
   | Left         ::   :: Left             {{ tex \textsf{left} }}
   | Right        ::   :: Right            {{ tex \textsf{right} }}
   | _            ::   :: wildcard         {{ tex \text{\textvisiblespace} }}
@@ -314,6 +317,7 @@ terminals :: 'terminals_' ::=
   | take         ::   :: take             {{ tex \textsf{take}\! }}
   | coaxrProves  ::   :: coaxrProves      {{ tex \textsf{coaxrProves} }}
   | Just         ::   :: Just             {{ tex \textsf{Just} }}
+  | \\           ::   :: newline          {{ tex \\ }}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Formulae  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -374,7 +378,7 @@ formula :: 'formula_' ::=
   | 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/OpSem.ott b/docs/core-spec/OpSem.ott
index 1c21ada0ec..ed59e9538b 100644
--- a/docs/core-spec/OpSem.ott
+++ b/docs/core-spec/OpSem.ott
@@ -20,7 +20,7 @@ defns
 OpSem :: '' ::=
 
 defn S |- e --> e'  ::  :: step :: 'S_' {{ com Single step semantics }}
-{{ tex [[S]] \labeledjudge{op} [[e]] [[-->]] [[e']] }}
+{{ tex \begin{array}{l} [[S]] \labeledjudge{op} [[e]] [[-->]] [[e']] \end{array} }}
 by
 
 S(n) = e
@@ -50,18 +50,16 @@ g2 = nth 1 g
 ------------------------------- :: CPush
 S |- ((\n.e) |> g) g' --> (\n.e |> g2) (g0 ; g' ; g1)
 
------------------ :: LetNonRec
-S |- let n = e1 in e2 --> e2[n |-> e1]
-
-
-S, </ [ni |-> ei] // i /> |- u --> u'
------------------------------------- :: LetRec
-S |- let rec </ ni = ei // i /> in u --> let rec </ ni = ei // i /> in u'
+--------------------------------------- :: Trans
+S |- (e |> g1) |> g2 --> e |> (g1 ; g2)
 
-fv(u) \inter </ ni // i /> = empty
------------------------------------------- :: LetRecReturn
-S |- let rec </ ni = ei // i /> in u --> u
+S |- e --> e'
+------------------------ :: Cast
+S |- e |> g --> e' |> g
 
+S |- e --> e'
+------------------------------ :: Tick
+S |- e { tick } --> e' { tick }
 
 S |- e --> e'
 --------------------------------------- :: Case
@@ -85,13 +83,27 @@ T </ taa // aa /> ~#k T </ t'aa // aa /> = coercionKind g
 forall </ alphaaa_kaa // aa />. forall </ betabb_k'bb // bb />. </ t1cc // cc /> @-> T </ alphaaa_kaa // aa /> = dataConRepType K
 </ e'cc = ecc |> (t1cc @ </ [alphaaa_kaa |-> nth aa g] // aa /> </ [betabb_k'bb |-> <sbb>_Nom] // bb />) // cc />
 --------------------------- :: CasePush
-S |- case (K </ taa // aa /> </ sbb // bb /> </ ecc // cc />) |> g as n return t2 of </ alti // i /> --> case K </ t'aa // aa /> </ sbb // bb /> </ e'cc // cc /> as n return t2 of </ alti // i />
+S |- case (K </ taa // aa /> </ sbb // bb /> </ ecc // cc />) |> g as n return t2 of </ alti // i /> --> \\ case K </ t'aa // aa /> </ sbb // bb /> </ e'cc // cc /> as n return t2 of </ alti // i />
 
-S |- e --> e'
------------------------- :: Cast
-S |- e |> g --> e' |> g
+----------------- :: LetNonRec
+S |- let n = e1 in e2 --> e2[n |-> e1]
 
-S |- e --> e'
------------------------------- :: Tick
-S |- e { tick } --> e' { tick }
+S, </ [ni |-> ei] // i /> |- u --> u'
+------------------------------------ :: LetRec
+S |- let rec </ ni = ei // i /> in u --> let rec </ ni = ei // i /> in u'
+
+--------------- :: LetRecApp
+S |- (let rec </ ni = ei // i /> in u) e' --> let rec </ ni = ei // i /> in (u e')
+
+---------------- :: LetRecCast
+S |- (let rec </ ni = ei // i /> in u) |> g --> let rec </ ni = ei // i /> in (u |> g)
 
+--------------- :: LetRecCase
+S |- case (let rec </ ni = ei // i /> in u) as n0 return t of </ altj // j /> --> \\ let rec </ ni = ei // i /> in (case u as n0 return t of </ altj // j />)
+
+--------------- :: LetRecFlat
+S |- let rec </ ni = ei // i /> in (let rec </ nj' = ej' // j /> in u) --> let rec </ ni = ei // i />;; </ nj' = ej' // j /> in u
+
+fv(u) \inter </ ni // i /> = empty
+--------------------------------- :: LetRecReturn
+S |- let rec </ ni = ei // i /> in u --> u
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index ddbc6147d4..7830e890e1 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 21 November, 2013
+\Large 23 April 2015
 \end{center}
 
 \section{Introduction}
@@ -136,9 +136,9 @@ There are some invariants on types:
 \begin{itemize}
 \item The type $[[t1]]$ in the form $[[t1 t2]]$ must not be a type constructor
 $[[T]]$. It should be another application or a type variable.
-\item The form $[[T </ ti // i /> ]]$ (\texttt{TyConApp}) 
+\item The form $[[T </ ti // i /> ]]$ (\texttt{TyConApp})
 does \emph{not} need to be saturated.
-\item A saturated application of $[[(->) t1 t2]]$ should be represented as 
+\item A saturated application of $[[(->) t1 t2]]$ should be represented as
 $[[t1 -> t2]]$. This is a different point in the grammar, not just pretty-printing.
 The constructor for a saturated $[[(->)]]$ is \texttt{FunTy}.
 \item A type-level literal is represented in GHC with a different datatype than
@@ -326,7 +326,7 @@ and \ottdrulename{Co\_CoVarCoRepr}.
 \ottdefnlintCoercion{}
 
 In \ottdrulename{Co\_AxiomInstCo}, the use of $[[inits]]$ creates substitutions from
-the first $i$ mappings in $[[ </ [ni |-> si] // i /> ]]$. This has the effect of 
+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]]$, and
@@ -446,11 +446,13 @@ use of FC does not require modeling recursion, you will not need to track $[[S]]
 \subsection{Notes}
 
 \begin{itemize}
-\item The \ottdrulename{S\_LetRec} and \ottdrulename{S\_LetRecReturn} rules
+\item The \ottdrulename{S\_LetRec} rules
 implement recursion. \ottdrulename{S\_LetRec} adds to the context $[[S]]$ bindings
 for all of the mutually recursive equations. Then, after perhaps many steps,
 when the body of the $[[let]]\ [[rec]]$ contains no variables that are bound
-in the $[[let]]\ [[rec]]$, the context is popped.
+in the $[[let]]\ [[rec]]$, the context is popped in \ottdrulename{S\_LetRecReturn}.
+The other \ottdrulename{S\_LetRecXXX}
+rules are there to prevent reduction from getting stuck.
 \item In the $[[case]]$ rules, a constructor $[[K]]$ is written taking three
 lists of arguments: two lists of types and a list of terms. The types passed
 in are the universally and, respectively, existentially quantified type variables
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index 8d2e5cbb13..93242e9f72 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf