core-spec: Simplify the handling of LetRec
authorJoachim Breitner <mail@joachim-breitner.de>
Tue, 18 Apr 2017 20:33:38 +0000 (16:33 -0400)
committerJoachim Breitner <mail@joachim-breitner.de>
Mon, 24 Apr 2017 20:34:26 +0000 (16:34 -0400)
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

docs/core-spec/OpSem.ott
docs/core-spec/core-spec.mng
docs/core-spec/core-spec.pdf

index b833b74..8fb9b0e 100644 (file)
@@ -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
index 0b147f9..d1d8905 100644 (file)
@@ -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
index f45e871..dde6c9e 100644 (file)
Binary files a/docs/core-spec/core-spec.pdf and b/docs/core-spec/core-spec.pdf differ