Commit 414e20bc authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Fix the formal operational semantics (#10121)

This adapts the work of Christiaan Baaij to present a sensible
operational semantics for FC with mutual recursion.
parent a8d39a72
......@@ -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
......@@ -276,7 +276,7 @@ G |-co mu </ ti // i /> </ gj // j /> : t'1 ~R' k0 t'2
defn validRoles T :: :: checkValidRoles :: 'Cvr_'
{{ com Type constructor role validity, \coderef{typecheck/TcTyClsDecls.lhs}{checkValidRoles} }}
by
by
</ Ki // i /> = tyConDataCons T
</ Rj // j /> = tyConRoles T
......@@ -341,7 +341,7 @@ Nom <= R
R <= Ph
------- :: Refl
R <= R
R <= R
defn G |- ki k ok :: :: lintKind :: 'K_'
{{ com Kind validity, \coderef{coreSyn/CoreLint.lhs}{lintKind} }}
......@@ -352,7 +352,7 @@ G |-ty k : BOX
-------------- :: Box
G |-ki k ok
defn G |- ty t : k :: :: lintType :: 'Ty_'
defn G |- ty t : k :: :: lintType :: 'Ty_'
{{ com Kinding, \coderef{coreSyn/CoreLint.lhs}{lintType} }}
{{ tex [[G]] \labeledjudge{ty} [[t]] : [[k]] }}
by
......
......@@ -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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -374,7 +378,7 @@ formula :: 'formula_' ::=
| t = coercionKind g :: :: coercionKind
| Just ( t1 , t2 ) = coaxrProves mu </ si // i /> </ ( s'j , s''j ) // j />
:: :: coaxrProves
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Subrules and Parsing %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......
......@@ -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
......@@ -30,7 +30,7 @@ System FC, as implemented in GHC\footnote{This
document was originally prepared by Richard Eisenberg (\texttt{eir@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}
......@@ -136,9 +136,9 @@ There are some invariants on types:
\begin{itemize}
\item The type $[[t1]]$ in the form $[[t1 t2]]$ must not be a type constructor
$[[T]]$. It should be another application or a type variable.
\item The form $[[T </ ti // i /> ]]$ (\texttt{TyConApp})
\item The form $[[T </ ti // i /> ]]$ (\texttt{TyConApp})
does \emph{not} need to be saturated.
\item A saturated application of $[[(->) t1 t2]]$ should be represented as
\item A saturated application of $[[(->) t1 t2]]$ should be represented as
$[[t1 -> t2]]$. This is a different point in the grammar, not just pretty-printing.
The constructor for a saturated $[[(->)]]$ is \texttt{FunTy}.
\item A type-level literal is represented in GHC with a different datatype than
......@@ -326,7 +326,7 @@ and \ottdrulename{Co\_CoVarCoRepr}.
\ottdefnlintCoercion{}
In \ottdrulename{Co\_AxiomInstCo}, the use of $[[inits]]$ creates substitutions from
the first $i$ mappings in $[[ </ [ni |-> si] // i /> ]]$. This has the effect of
the first $i$ mappings in $[[ </ [ni |-> si] // i /> ]]$. This has the effect of
folding the substitution over the kinds for kind-checking.
See Section~\ref{sec:tyconroles} for more information about $[[tyConRolesX]]$, and
......@@ -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
......
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