diff options
-rw-r--r-- | docs/core-spec/OpSem.ott | 62 | ||||
-rw-r--r-- | docs/core-spec/core-spec.mng | 18 | ||||
-rw-r--r-- | 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 b833b7487b..8fb9b0e068 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 0b147f9c23..d1d89055e7 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 Binary files differindex f45e8711b1..dde6c9eeba 100644 --- a/docs/core-spec/core-spec.pdf +++ b/docs/core-spec/core-spec.pdf |