[commit: ghc] master: Fix the formal operational semantics (#10121) (414e20b)
git at git.haskell.org
git at git.haskell.org
Fri Apr 24 21:02:14 UTC 2015
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/414e20bc7f5166d020ace3d92cd605e121d5eb3c/ghc
>---------------------------------------------------------------
commit 414e20bc7f5166d020ace3d92cd605e121d5eb3c
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date: Thu Apr 23 16:02:43 2015 -0400
Fix the formal operational semantics (#10121)
This adapts the work of Christiaan Baaij to present a sensible
operational semantics for FC with mutual recursion.
>---------------------------------------------------------------
414e20bc7f5166d020ace3d92cd605e121d5eb3c
docs/core-spec/CoreLint.ott | 2 +-
docs/core-spec/CoreSyn.ott | 6 +++++-
docs/core-spec/OpSem.ott | 48 +++++++++++++++++++++++++++----------------
docs/core-spec/core-spec.mng | 8 +++++---
docs/core-spec/core-spec.pdf | Bin 340768 -> 342464 bytes
5 files changed, 41 insertions(+), 23 deletions(-)
diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index 6015731..7058e8a 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
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index d64667a..247fd05 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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott
index 1c21ada..ed59e95 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 ddbc614..7830e89 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 at 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}
@@ -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 8d2e5cb..93242e9 100644
Binary files a/docs/core-spec/core-spec.pdf and b/docs/core-spec/core-spec.pdf differ
More information about the ghc-commits
mailing list