From 414e20bc7f5166d020ace3d92cd605e121d5eb3c Mon Sep 17 00:00:00 2001 From: Richard Eisenberg Date: Thu, 23 Apr 2015 16:02:43 -0400 Subject: Fix the formal operational semantics (#10121) This adapts the work of Christiaan Baaij to present a sensible operational semantics for FC with mutual recursion. --- docs/core-spec/CoreLint.ott | 8 ++++---- docs/core-spec/CoreSyn.ott | 8 ++++++-- docs/core-spec/OpSem.ott | 48 +++++++++++++++++++++++++++---------------- docs/core-spec/core-spec.mng | 14 +++++++------ docs/core-spec/core-spec.pdf | Bin 340768 -> 342464 bytes 5 files changed, 48 insertions(+), 30 deletions(-) (limited to 'docs/core-spec') diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott index 6015731257..7058e8a113 100644 --- a/docs/core-spec/CoreLint.ott +++ b/docs/core-spec/CoreLint.ott @@ -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 : t'1 ~R' k0 t'2 defn validRoles T :: :: checkValidRoles :: 'Cvr_' {{ com Type constructor role validity, \coderef{typecheck/TcTyClsDecls.lhs}{checkValidRoles} }} -by +by = tyConDataCons T = 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 diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott index d64667af18..247fd05ae3 100644 --- a/docs/core-spec/CoreSyn.ott +++ b/docs/core-spec/CoreSyn.ott @@ -69,10 +69,12 @@ e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.lhs}{Expr} }} | ( e ) :: M :: Parens {{ com Parenthesized expression }} | e :: 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 :: :: Rec {{ com Recursive binding }} + | rec :: :: Rec {{ com Recursive binding }} alt :: 'Alt_' ::= {{ com Case alternative, \coderef{coreSyn/CoreSyn.lhs}{Alt} }} | Kp -> 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 :: :: coaxrProves - + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Subrules and Parsing %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott index 1c21ada0ec..ed59e9538b 100644 --- a/docs/core-spec/OpSem.ott +++ b/docs/core-spec/OpSem.ott @@ -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, ei] // i /> |- u --> u' ------------------------------------- :: LetRec -S |- let rec in u --> let rec in u' +--------------------------------------- :: Trans +S |- (e |> g1) |> g2 --> e |> (g1 ; g2) -fv(u) \inter = empty ------------------------------------------- :: LetRecReturn -S |- let rec 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 ~#k T = coercionKind g forall . forall . @-> T = dataConRepType K (t1cc @ nth aa g] // aa /> _Nom] // bb />) // cc /> --------------------------- :: CasePush -S |- case (K ) |> g as n return t2 of --> case K as n return t2 of +S |- case (K ) |> g as n return t2 of --> \\ case K as n return t2 of -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, ei] // i /> |- u --> u' +------------------------------------ :: LetRec +S |- let rec in u --> let rec in u' + +--------------- :: LetRecApp +S |- (let rec in u) e' --> let rec in (u e') + +---------------- :: LetRecCast +S |- (let rec in u) |> g --> let rec in (u |> g) +--------------- :: LetRecCase +S |- case (let rec in u) as n0 return t of --> \\ let rec in (case u as n0 return t of ) + +--------------- :: LetRecFlat +S |- let rec in (let rec in u) --> let rec ;; in u + +fv(u) \inter = empty +--------------------------------- :: LetRecReturn +S |- let rec in u --> u diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng index ddbc6147d4..7830e890e1 100644 --- a/docs/core-spec/core-spec.mng +++ b/docs/core-spec/core-spec.mng @@ -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 ]]$ (\texttt{TyConApp}) +\item The form $[[T ]]$ (\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 $[[ si] // i /> ]]$. This has the effect of +the first $i$ mappings in $[[ 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 diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf index 8d2e5cbb13..93242e9f72 100644 Binary files a/docs/core-spec/core-spec.pdf and b/docs/core-spec/core-spec.pdf differ -- cgit v1.2.1