[commit: ghc] wip/T13588: core-spec: Simplify the handling of LetRec (2572e82)
git at git.haskell.org
git at git.haskell.org
Tue Apr 18 22:59:27 UTC 2017
Repository : ssh://git@git.haskell.org/ghc
On branch : wip/T13588
Link : http://ghc.haskell.org/trac/ghc/changeset/2572e820b9d1f0d7f4c32b3d8ebace4b12d494ee/ghc
>---------------------------------------------------------------
commit 2572e820b9d1f0d7f4c32b3d8ebace4b12d494ee
Author: Joachim Breitner <mail at joachim-breitner.de>
Date: Tue Apr 18 16:33:38 2017 -0400
core-spec: Simplify the handling of LetRec
We do not need to keep an enrivonment around to implement letrec, as
long as we only do call-by-name. Instead, evaluate letrec by
substituting for all the variables with their RHS wrapped in the letrec
binding.
Since nothing adds to the enrivonment any more, there is no need for a
S_Var rule.
>---------------------------------------------------------------
2572e820b9d1f0d7f4c32b3d8ebace4b12d494ee
docs/core-spec/OpSem.ott | 62 +++++++++++++++----------------------------
docs/core-spec/core-spec.mng | 18 +++----------
docs/core-spec/core-spec.pdf | Bin 349621 -> 346103 bytes
3 files changed, 24 insertions(+), 56 deletions(-)
diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott
index b833b74..8fb9b0e 100644
--- a/docs/core-spec/OpSem.ott
+++ b/docs/core-spec/OpSem.ott
@@ -19,92 +19,72 @@ grammar
defns
OpSem :: '' ::=
-defn S |- e --> e' :: :: step :: 'S_' {{ com Single step semantics }}
-{{ tex \begin{array}{l} [[S]] \labeledjudge{op} [[e]] [[-->]] [[e']] \end{array} }}
+defn e --> e' :: :: step :: 'S_' {{ com Single step semantics }}
+{{ tex \begin{array}{l} [[e]] [[-->]] [[e']] \end{array} }}
by
-S(n) = e
------------------ :: Var
-S |- n --> e
-
-S |- e1 --> e1'
+e1 --> e1'
------------------- :: App
-S |- e1 e2 --> e1' e2
+e1 e2 --> e1' e2
----------------------------- :: Beta
-S |- (\n.e1) e2 --> e1[n |-> e2]
+(\n.e1) e2 --> e1[n |-> e2]
g0 = sym (nth 0 g)
g1 = nth 1 g
not e2 is_a_type
not e2 is_a_coercion
----------------------------------------------- :: Push
-S |- ((\n.e1) |> g) e2 --> (\n.e1 |> g1) (e2 |> g0)
+((\n.e1) |> g) e2 --> (\n.e1 |> g1) (e2 |> g0)
---------------------------------------- :: TPush
-S |- ((\n.e) |> g) t --> (\n.(e |> g n)) t
+((\n.e) |> g) t --> (\n.(e |> g n)) t
g0 = nth 1 (nth 0 g)
g1 = sym (nth 2 (nth 0 g))
g2 = nth 1 g
------------------------------- :: CPush
-S |- ((\n.e) |> g) g' --> (\n.e |> g2) (g0 ; g' ; g1)
+((\n.e) |> g) g' --> (\n.e |> g2) (g0 ; g' ; g1)
--------------------------------------- :: Trans
-S |- (e |> g1) |> g2 --> e |> (g1 ; g2)
+(e |> g1) |> g2 --> e |> (g1 ; g2)
-S |- e --> e'
+e --> e'
------------------------ :: Cast
-S |- e |> g --> e' |> g
+e |> g --> e' |> g
-S |- e --> e'
+e --> e'
------------------------------ :: Tick
-S |- e { tick } --> e' { tick }
+e { tick } --> e' { tick }
-S |- e --> e'
+e --> e'
--------------------------------------- :: Case
-S |- case e as n return t of </ alti // i /> --> case e' as n return t of </ alti // i />
+case e as n return t of </ alti // i /> --> case e' as n return t of </ alti // i />
altj = K </ alphabb_kbb // bb /> </ xcc_tcc // cc /> -> u
e = K </ t'aa // aa /> </ sbb // bb /> </ ecc // cc />
u' = u[n |-> e] </ [alphabb_kbb |-> sbb] // bb /> </ [xcc_tcc |-> ecc] // cc />
-------------------------------------------------------------- :: MatchData
-S |- case e as n return t of </ alti // i /> --> u'
+case e as n return t of </ alti // i /> --> u'
altj = lit -> u
---------------------------------------------------------------- :: MatchLit
-S |- case lit as n return t of </ alti // i /> --> u[n |-> lit]
+case lit as n return t of </ alti // i /> --> u[n |-> lit]
altj = _ -> u
no other case matches
------------------------------------------------------------ :: MatchDefault
-S |- case e as n return t of </ alti // i /> --> u[n |-> e]
+case e as n return t of </ alti // i /> --> u[n |-> e]
T </ taa // aa /> k'~#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 />
+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 />
----------------- :: LetNonRec
-S |- let n = e1 in e2 --> e2[n |-> e1]
+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'
-
---------------- :: 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
+let rec </ ni = ei // i /> in u --> u </ [ni |-> let rec </ ni = ei // i /> in ei ] // i />
-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 0b147f9..d1d8905 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -473,14 +473,9 @@ analogously to \texttt{CoreLint.lhs}.
Nevertheless, these rules are included in this document to help the reader
understand System FC.
-\subsection{The context $[[S]]$}
-We use a context $[[S]]$ to keep track of the values of variables in a (mutually)
-recursive group. Its definition is as follows:
-\[
-[[S]] \quad ::= \quad [[ empty ]] \ |\ [[S]], [[ [n |-> e] ]]
-\]
-The presence of the context $[[S]]$ is solely to deal with recursion. If your
-use of FC does not require modeling recursion, you will not need to track $[[S]]$.
+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{Operational semantics rules}
@@ -489,13 +484,6 @@ use of FC does not require modeling recursion, you will not need to track $[[S]]
\subsection{Notes}
\begin{itemize}
-\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 \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 f45e871..dde6c9e 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