Commit 583fa9e3 authored by Joachim Breitner's avatar Joachim Breitner

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.

Differential Revision: https://phabricator.haskell.org/D3466
parent cd10a232
......@@ -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
......@@ -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
......
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