summaryrefslogtreecommitdiff
path: root/docs/core-spec
diff options
context:
space:
mode:
Diffstat (limited to 'docs/core-spec')
-rw-r--r--docs/core-spec/CoreLint.ott147
-rw-r--r--docs/core-spec/CoreSyn.ott64
-rw-r--r--docs/core-spec/OpSem.ott45
-rw-r--r--docs/core-spec/core-spec.mng112
-rw-r--r--docs/core-spec/core-spec.pdfbin346103 -> 356480 bytes
5 files changed, 286 insertions, 82 deletions
diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index 50b11ce7e7..6ace483cb5 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -30,7 +30,7 @@ G |-sbind n <- e
---------------------- :: NonRec
G |-bind n = e
-</ G |-sbind ni <- ei // i />
+</ G, </ ni // i /> |-sbind ni <- ei // i />
---------------------- :: Rec
G |-bind rec </ ni = ei // i />
@@ -38,50 +38,64 @@ defn G |- sbind n <- e :: :: lintSingleBinding :: 'SBinding_' {{ com Single bi
{{ tex [[G]] \labeledjudge{sbind} [[n]] [[<-]] [[e]] }}
by
-G |-tm e : t
+G; empty |-tm e : t
G |-name z_t ok
</ mi // i /> = fv(t)
</ mi elt G // i />
----------------- :: SingleBinding
G |-sbind z_t <- e
-defn G |- tm e : t :: :: lintCoreExpr :: 'Tm_'
+defn G ; D |-sjbind l vars <- e : t :: :: lintSingleBinding_joins :: 'SJBinding_' {{ com Single join binding typing, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding} }}
+ {{ tex [[G]];[[D]] \labeledjudge{sjbind} [[l]] \, [[vars]] [[<-]] [[e]] : [[t]] }}
+by
+
+</ G'j $ // j /> = inits(</ nj // j />)
+G, </ nj // j /> ; D |-tm e : t
+G |-label p/I_s ok
+</ G, G'j |-name nj ok // j />
+</ mj // j /> = fv(s)
+</ mj elt G // j />
+split_I s = </ sj // j /> t
+----------------- :: SingleBinding
+G; D |-sjbind p/I_s </ nj // j /> <- e : t
+
+defn G ; D |- tm e : t :: :: lintCoreExpr :: 'Tm_'
{{ com Expression typing, \coderef{coreSyn/CoreLint.lhs}{lintCoreExpr} }}
- {{ tex [[G]] \labeledjudge{tm} [[e]] : [[t]] }}
+ {{ tex [[G]]; [[D]] \labeledjudge{tm} [[e]] : [[t]] }}
by
x_t elt G
not (t is_a_coercion_type)
------------------ :: Var
-G |-tm x_t : t
+G; D |-tm x_t : t
t = literalType lit
------------------- :: Lit
-G |-tm lit : t
+G; D |-tm lit : t
-G |-tm e : s
+G; empty |-tm e : s
G |-co g : s k1~Rep k2 t
k2 elt { *, # }
------------------- :: Cast
-G |-tm e |> g : t
+G; D |-tm e |> g : t
-G |-tm e : t
+G; empty |-tm e : t
------------------- :: Tick
-G |-tm e {tick} : t
+G; D |-tm e {tick} : t
G' = G, alpha_k
G |-ki k ok
G' |-subst alpha_k |-> s ok
-G' |-tm e[alpha_k |-> s] : t
+G'; D |-tm e[alpha_k |-> s] : t
--------------------------- :: LetTyKi
-G |-tm let alpha_k = s in e : t
+G; D |-tm let alpha_k = s in e : t
G |-sbind x_s <- u
G |-ty s : k
k = * \/ k = #
-G, x_s |-tm e : t
+G, x_s ; D |-tm e : t
------------------------- :: LetNonRec
-G |-tm let x_s = u in e : t
+G; D |-tm let x_s = u in e : t
</ G'i $ // i /> = inits(</ zi_si // i />)
</ G, G'i |-ty si : ki // i />
@@ -89,54 +103,72 @@ G |-tm let x_s = u in e : t
no_duplicates </ zi // i />
G' = G, </ zi_si // i />
</ G' |-sbind zi_si <- ui // i />
-G' |-tm e : t
+G'; D |-tm e : t
------------------------ :: LetRec
-G |-tm let rec </ zi_si = ui // i /> in e : t
+G; D |-tm let rec </ zi_si = ui // i /> in e : t
+
+G; D |-sjbind l </ ni // i /> <- u : t
+G; D, l |-tm e : t
+------------------------------------------- :: JoinNonRec
+G; D |-tm join l </ ni // i /> = u in e : t
+
+no_duplicates </ li // i />
+D' = D, </ li // i />
+</ G; D' |-sjbind l </ nj // j /> <- ui : t // i />
+G; D' |-tm e : t
+------------------------------------------------------------- :: JoinRec
+G; D |-tm join rec </ li </ nj // j /> = ui // i /> in e : t
% lintCoreArg is incorporated in these next two rules
-G |-tm e : forall alpha_k.t
+G; empty |-tm e : forall alpha_k.t
G |-subst alpha_k |-> s ok
---------------- :: AppType
-G |-tm e s : t[alpha_k |-> s]
+G; D |-tm e s : t[alpha_k |-> s]
not (e2 is_a_type)
-G |-tm e1 : t1 -> t2
-G |-tm e2 : t1
+G; empty |-tm e1 : t1 -> t2
+G; empty |-tm e2 : t1
---------------- :: AppExpr
-G |-tm e1 e2 : t2
+G; D |-tm e1 e2 : t2
+
+p/I_s elt D
+split_I s = </ sj // j /> t
+</ G; empty |-tm ej : sj // j />
+--------------------- :: Jump
+G; D |-tm jump p/I_s </ ej // j /> : t
not (k is_a_coercion_type)
G |-ty t : k
-G, x_t |-tm e : s
+G, x_t; |-tm e : s
----------------- :: LamId
-G |-tm \x_t.e : t -> s
+G; D |-tm \x_t.e : t -> s
G |-ki k ok
-G,alpha_k |-tm e : t
+G,alpha_k; |-tm e : t
--------------------------- :: LamTy
-G |-tm \alpha_k.e : forall alpha_k. t
+G; D |-tm \alpha_k.e : forall alpha_k. t
phi = s1 k1~#k2 s2
G |-ki phi ok
-G,c_phi |-tm e : t
+G,c_phi; |-tm e : t
-------------------------------- :: LamCo
-G |-tm \c_phi.e : forall c_phi.t
+G; D |-tm \c_phi.e : forall c_phi.t
-G |-tm e : s
+G; empty |-tm e : s
s = * \/ s = #
G |-ty t : TYPE s2
-</ G, z_s; s |-altern alti : t // i />
+</ G, z_s; D; s |-altern alti : t // i />
---------------------------------------------------- :: Case
-G |-tm case e as z_s return t of </ alti // i /> : t
+G; D |-tm case e as z_s return t of </ alti // i /> : t
G |-co g : t1 k1~Nom k2 t2
-------------------- :: Coercion
-G |-tm g : t1 k1~#k2 t2
+G; D |-tm g : t1 k1~#k2 t2
G |-co g : t1 k1~Rep k2 t2
----------------------- :: CoercionRep
-G |-tm g : (~Rep#) k1 k2 t1 t2
+G; D |-tm g : (~Rep#) k1 k2 t1 t2
defn G |- name n ok :: :: lintSingleBinding_lintBinder :: 'Name_'
{{ com Name consistency check, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding\#lintBinder} }}
@@ -151,6 +183,19 @@ G |-name x_t ok
----------------- :: TyVar
G |-name alpha_k ok
+defn G |- label l ok :: :: lintSingleBinding_lintBinder_join :: 'Label_'
+ {{ com Label consistency check, \coderef{coreSyn/CoreLint.hs}{lintSingleBinding\#lintBinder} }}
+ {{ tex [[G]] \labeledjudge{label} [[l]] [[ok]] }}
+by
+
+G |- ty t : k
+k = * \/ k = #
+split_I t = </ si // i /> t'
+G |- ty t' : k'
+k' = * \/ k' = #
+----------------- :: Label
+G |-label p / I _ t ok
+
defn G |- bnd n ok :: :: lintBinder :: 'Binding_'
{{ com Binding consistency, \coderef{coreSyn/CoreLint.lhs}{lintBinder} }}
{{ tex [[G]] \labeledjudge{bnd} [[n]] [[ok]] }}
@@ -172,7 +217,16 @@ by
G |-ty t : k
---------------------- :: Refl
-G |-co <t>_R : t k~R k t
+G |-co <t> : t k~Nom k t
+
+G |-ty t : k
+---------------------- :: GReflMRefl
+G |-co <t> R MRefl : t k~R k t
+
+G |-ty t : k1
+G |-co g : k1 *~Nom * k2
+---------------------- :: GReflMCo
+G |-co <t> R MCo g : t k1~R k2 (t |> g)
G |-co g1 : s1 k1~R k'1 t1
G |-co g2 : s2 k2~R k'2 t2
@@ -255,11 +309,11 @@ not (si is_a_coercion)
not (ti is_a_coercion)
R' = (tyConRolesX R T)[i]
---------------------- :: NthCoTyCon
-G |-co nth i g : si k2~R' k2' ti
+G |-co nth R' i g : si k2~R' k2' ti
G |-co g : (forall z1_k1.t1) k3~R k4 (forall z2_k2.t2)
--------------------------- :: NthCoForAll
-G |-co nth 0 g : k1 *~Nom * k2
+G |-co nth Nom 0 g : k1 *~Nom * k2
G |-co g : (s1 s2) k~Nom k' (t1 t2)
G |-ty s1 : k1
@@ -294,11 +348,6 @@ G |-ty t2 : k'
G |-co C ind </ gi // i /> : s2 k~R0 k' t2
G |-co g : t1 k1~R k2 t2
-G |-ty t1 |> h : k1'
----------------------------------- :: CoherenceCo
-G |-co g |> h : t1 |> h k1'~R k2 t2
-
-G |-co g : t1 k1~R k2 t2
-------------------------- :: KindCo
G |-co kind g : k1 *~Nom * k2
@@ -316,7 +365,7 @@ G |-ty t'2 : k0'
G |-co mu </ ti // i /> $ </ gj // j /> : t'1 k0 ~R' k0' t'2
defn G |- axk [ namesroles |-> gs ] ~> ( subst1 , subst2 ) :: :: check_ki :: 'AxiomKind_'
- {{ com Axiom argument kinding, \coderef{coreSyn/CoreLint.lhs}{check\_ki} }}
+ {{ com Axiom argument kinding, \coderef{coreSyn/CoreLint.lhs}{lintCoercion\#check\_ki} }}
{{ tex [[G]] \labeledjudge{axk} [ [[namesroles]] [[|->]] [[gs]] ] [[~>]] ([[subst1]], [[subst2]]) }}
by
@@ -477,19 +526,19 @@ G |-ty t : k
---------------------- :: Type
G |-subst z_k |-> t ok
-defn G ; s |- altern alt : t :: :: lintCoreAlt :: 'Alt_'
+defn G ; D ; s |- altern alt : t :: :: lintCoreAlt :: 'Alt_'
{{ com Case alternative consistency, \coderef{coreSyn/CoreLint.lhs}{lintCoreAlt} }}
- {{ tex [[G]];[[s]] \labeledjudge{alt} [[alt]] : [[t]] }}
+ {{ tex [[G]];[[D]];[[s]] \labeledjudge{alt} [[alt]] : [[t]] }}
by
-G |-tm e : t
+G; D |-tm e : t
--------------------- :: DEFAULT
-G; s |-altern _ -> e : t
+G; D; s |-altern _ -> e : t
s = literalType lit
-G |-tm e : t
+G; D |-tm e : t
---------------------------------------- :: LitAlt
-G; s |-altern lit -> e : t
+G; D; s |-altern lit -> e : t
T = dataConTyCon K
not (isNewTyCon T)
@@ -498,9 +547,9 @@ t2 = t1 {</ sj // j />}
</ G |-bnd ni ok // i />
G' = G, </ ni // i />
G' |-altbnd </ ni // i /> : t2 ~> T </ sj // j />
-G' |-tm e : t
+G'; D |-tm e : t
--------------------------------------- :: DataAlt
-G; T </ sj // j /> |-altern K </ ni // i /> -> e : t
+G; D; T </ sj // j /> |-altern K </ ni // i /> -> e : t
defn t' = t { </ si // , // i /> } :: :: applyTys :: 'ApplyTys_'
{{ com Telescope substitution, \coderef{types/Type.lhs}{applyTys} }}
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index 578d200b6b..b11730c276 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -19,6 +19,7 @@ embed {{ tex-preamble
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
metavar x, c ::= {{ com Term-level variable names }}
+metavar p ::= {{ com Labels }}
metavar alpha {{ tex \alpha }}, beta {{ tex \beta }} ::=
{{ com Type-level variable names }}
metavar N ::= {{ com Type-level constructor names }}
@@ -45,6 +46,10 @@ n, m, aname {{ tex \alpha }}, xname {{ tex x }} :: 'Var_' ::= {{ com Variable na
| z $ :: M :: NoSupScript {{ com Name without an explicit type/kind }}
| K :: M :: DataCon {{ com Data constructor }}
+l :: 'Label_' ::= {{ com Labels for join points, also \coderef{basicTypes/Var.lhs}{Var} }}
+ | p / I _ t :: :: Label {{ com Label with join arity and type }}
+ {{ tex {[[p]]}_{[[I]]}^{[[t]]} }}
+
vars :: 'Vars_' ::= {{ com List of variables }}
| </ ni // , // i /> :: :: List
| fv ( t ) :: M :: fv_t
@@ -55,12 +60,18 @@ vars :: 'Vars_' ::= {{ com List of variables }}
| vars1 \inter vars2 :: M :: intersection
{{ tex [[vars1]] \cap [[vars2]] }}
+labels :: 'Labels_' ::= {{ com List of labels }}
+ | </ li // , // i /> :: :: List
+ | empty :: M :: empty
+
e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.lhs}{Expr} }}
| n :: :: Var {{ com \ctor{Var}: Variable }}
| lit :: :: Lit {{ com \ctor{Lit}: Literal }}
| e1 e2 :: :: App {{ com \ctor{App}: Application }}
+ | jump l </ ui // i /> :: :: Jump {{ com \ctor{App}: Jump }}
| \ n . e :: :: Lam {{ com \ctor{Lam}: Abstraction }}
| let binding in e :: :: Let {{ com \ctor{Let}: Variable binding }}
+ | join jbinding in e :: :: Join {{ com \ctor{Let}: Join binding }}
| case e as n return t of </ alti // | // i /> :: :: Case {{ com \ctor{Case}: Pattern match }}
| e |> g :: :: Cast {{ com \ctor{Cast}: Cast }}
| e { tick } :: :: Tick {{ com \ctor{Tick}: Internal note }}
@@ -78,6 +89,10 @@ binding :: 'Bind_' ::= {{ com Let-bindings, \coderef{coreSyn/CoreSyn.lhs}{Bind}
| n = e :: :: NonRec {{ com \ctor{NonRec}: Non-recursive binding }}
| rec </ ni = ei // ;; // i /> :: :: Rec {{ com \ctor{Rec}: Recursive binding }}
+jbinding :: 'JoinBind_' ::= {{ com Join bindings, also \coderef{coreSyn/CoreSyn.lhs}{Bind} }}
+ | l </ ni // i /> = e :: :: NonRec {{ com \ctor{NonRec}: Non-recursive binding }}
+ | rec </ li </ nij // j /> = ei // i /> :: :: Rec {{ com \ctor{Rec}: Recursive binding }}
+
alt :: 'Alt_' ::= {{ com Case alternative, \coderef{coreSyn/CoreSyn.lhs}{Alt} }}
| Kp </ ni // i /> -> e :: :: Alt {{ com Constructor applied to fresh names }}
@@ -98,8 +113,8 @@ t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}, phi {{ tex \phi }}
| n :: :: TyVarTy {{ com \ctor{TyVarTy}: Variable }}
| t1 t2 :: :: AppTy {{ com \ctor{AppTy}: Application }}
| T </ ti // i /> :: :: TyConApp {{ com \ctor{TyConApp}: Application of type constructor }}
- | t1 -> t2 :: :: FunTy {{ com \ctor{ForAllTy (Anon ...) ...}: Function }}
- | forall n . t :: :: ForAllTy {{ com \ctor{ForAllTy (Named ...) ...}: Type and coercion polymorphism }}
+ | t1 -> t2 :: :: FunTy {{ com \ctor{FunTy}: Function }}
+ | forall n . t :: :: ForAllTy {{ com \ctor{ForAllTy}: Type and coercion polymorphism }}
| lit :: :: LitTy {{ com \ctor{LitTy}: Type-level literal }}
| t |> g :: :: CastTy {{ com \ctor{CastTy}: Kind cast }}
| g :: :: CoercionTy {{ com \ctor{CoercionTy}: Coercion used in type }}
@@ -123,8 +138,10 @@ t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}, phi {{ tex \phi }}
%% COERCIONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coderef{types/TyCoRep.lhs}{Coercion} }}
- | < t > _ R :: :: Refl {{ com \ctor{Refl}: Reflexivity }}
- {{ tex {\langle [[t]] \rangle}_{[[R]]} }}
+ | < t > :: :: Refl {{ com \ctor{Refl}: Nominal Reflexivity }}
+ {{ tex {\langle [[t]] \rangle} }}
+ | < t > R mg :: :: GRefl {{ com \ctor{GRefl}: Generalized Reflexivity }}
+ {{ tex {\langle [[t]] \rangle}^{[[mg]]}_{[[R]]} }}
| T RA </ gi // i /> :: :: TyConAppCo {{ com \ctor{TyConAppCo}: Type constructor application }}
| g1 g2 :: :: AppCo {{ com \ctor{AppCo}: Application }}
| forall z : h . g :: :: ForAllCo {{ com \ctor{ForAllCo}: Polymorphism }}
@@ -137,11 +154,10 @@ g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coder
| g1 ; g2 :: :: TransCo {{ com \ctor{TransCo}: Transitivity }}
| mu </ ti // i /> $ </ gj // j />
:: :: AxiomRuleCo {{ com \ctor{AxiomRuleCo}: Axiom-rule application (for type-nats) }}
- | nth I g :: :: NthCo {{ com \ctor{NthCo}: Projection (0-indexed) }}
- {{ tex \textsf{nth}^{[[I]]}\,[[g]] }}
+ | nth R I g :: :: NthCo {{ com \ctor{NthCo}: Projection (0-indexed) }}
+ {{ tex \textsf{nth}^{[[I]]}_{[[R]]}\,[[g]] }}
| LorR g :: :: LRCo {{ com \ctor{LRCo}: Left/right projection }}
| g @ h :: :: InstCo {{ com \ctor{InstCo}: Instantiation }}
- | g |> h :: :: CoherenceCo {{ com \ctor{CoherenceCo}: Coherence }}
| kind g :: :: KindCo {{ com \ctor{KindCo}: Kind extraction }}
| sub g :: :: SubCo {{ com \ctor{SubCo}: Sub-role --- convert nominal to representational }}
| ( g ) :: M :: Parens {{ com Parentheses }}
@@ -155,6 +171,11 @@ prov :: 'UnivCoProvenance_' ::= {{ com \ctor{UnivCo} provenance, \coderef{types/
| ProofIrrelProv :: :: ProofIrrelProv {{ com From proof irrelevance }}
{{ tex \mathsf{irrel} }}
+mg {{ tex m }} :: 'MCoercion_' ::= {{ com A possibly reflexive coercion , \coderef{types/TyCoRep.lhs}{MCoercion} }}
+ | MRefl :: :: MRefl {{ com \ctor{MRefl}: A trivial reflexive coercion }}
+ | MCo g :: :: MCo {{ com \ctor{MCo}: Other coercions }}
+ {{ tex [[g]] }}
+
LorR :: 'LeftOrRight_' ::= {{ com left or right deconstructor, \coderef{types/TyCoRep.lhs}{LeftOrRight} }}
| Left :: :: CLeft {{ com \ctor{CLeft}: Left projection }}
| Right :: :: CRight {{ com \ctor{CRight}: Right projection }}
@@ -214,6 +235,12 @@ G {{ tex \Gamma }} :: 'LintM_Bindings_' ::= {{ com List of bindings, \coderef{co
| </ Gi // , // i /> :: :: Concat {{ com Context concatenation }}
| vars_of binding :: M :: VarsOf {{ com \coderef{coreSyn/CoreSyn.lhs}{bindersOf} }}
+D {{ tex \Delta }} :: 'LintM_JoinBindings_' ::= {{ com List of join bindings, \coderef{coreSyn/CoreLint.lhs}{LintM} }}
+ | l :: :: Binding {{ com Single binding }}
+ | </ Di // , // i /> :: :: Concat {{ com Context concatenation }}
+ | empty :: M :: Empty {{ com Empty context }}
+ | labels_of binding :: M :: LabelsOf {{ com \coderef{coreSyn/CoreSyn.lhs}{bindersOf} }}
+
O {{ tex \Omega }} :: 'VarEnv_Role_' ::= {{ com Mapping from type variables to roles }}
| </ ni : Ri // i /> :: :: List {{ com List of bindings }}
| O1 , O2 :: M :: Concat {{ com Concatenate two lists }}
@@ -254,6 +281,10 @@ ind, I {{ tex i }} :: 'Ind_' ::= {{ com Indices, numbers }}
| 0 :: M :: zero
| 1 :: M :: one
| 2 :: M :: two
+ | 3 :: M :: three
+
+terms :: 'Terms_' ::= {{ com List of terms }}
+ | </ ei // i /> :: :: List
types :: 'Types_' ::= {{ com List of types }}
| </ ti // i /> :: :: List
@@ -294,9 +325,11 @@ role_list {{ tex {\overline{\rho_j} }^j }} :: 'RoleList_' ::= {{ com List of rol
terminals :: 'terminals_' ::=
| \ :: :: lambda {{ tex \lambda }}
| let :: :: let {{ tex \keyword{let} }}
+ | join :: :: join {{ tex \keyword{join} }}
| in :: :: key_in {{ tex \keyword{in} }}
| rec :: :: rec {{ tex \keyword{rec} }}
| and :: :: key_and {{ tex \keyword{and} }}
+ | jump :: :: jump {{ tex \keyword{jump} }}
| case :: :: case {{ tex \keyword{case} }}
| of :: :: of {{ tex \keyword{of} }}
| -> :: :: arrow {{ tex \to }}
@@ -317,8 +350,9 @@ terminals :: 'terminals_' ::=
| ok :: :: ok {{ tex \textsf{ ok} }}
| no_duplicates :: :: no_duplicates {{ tex \textsf{no\_duplicates } }}
| vars_of :: :: vars_of {{ tex \textsf{vars\_of } }}
+ | split :: :: split {{ tex \mathop{\textsf{split} } }}
| not :: :: not {{ tex \neg }}
- | isUnLiftedTyCon :: :: isUnLiftenTyCon {{ tex \textsf{isUnLiftedTyCon} }}
+ | isUnLiftedTyCon :: :: isUnLiftedTyCon {{ tex \textsf{isUnLiftedTyCon} }}
| compatibleUnBoxedTys :: :: compatibleUnBoxedTys {{ tex \textsf{compatibleUnBoxedTys} }}
| false :: :: false {{ tex \textsf{false} }}
| true :: :: true {{ tex \textsf{true} }}
@@ -361,11 +395,16 @@ terminals :: 'terminals_' ::=
| validDcRoles :: :: validDcRoles {{ tex \textsf{validDcRoles} }}
| --> :: :: steps {{ tex \longrightarrow }}
| coercionKind :: :: coercionKind {{ tex \textsf{coercionKind} }}
+ | coercionRole :: :: coercionRole {{ tex \textsf{coercionRole} }}
| take :: :: take {{ tex \textsf{take}\! }}
| coaxrProves :: :: coaxrProves {{ tex \textsf{coaxrProves} }}
| Just :: :: Just {{ tex \textsf{Just} }}
| \\ :: :: newline {{ tex \\ }}
| classifiesTypeWithValues :: :: ctwv {{ tex \textsf{classifiesTypeWithValues} }}
+ | 0 :: :: zero {{ tex 0 }}
+ | +1 :: :: succ {{ tex +1 }}
+ | MRefl :: :: mrefl {{ tex \cdot }}
+ | MCo :: :: mco
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Formulae %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -375,6 +414,7 @@ formula :: 'formula_' ::=
| judgement :: :: judgement
| formula1 ... formulai :: :: dots
| G1 = G2 :: :: context_rewrite
+ | D1 = D2 :: :: join_context_rewrite
| t1 = t2 :: :: type_rewrite
| t1 /= t2 :: :: type_inequality
| e1 /=e e2 :: :: expr_inequality
@@ -384,6 +424,7 @@ formula :: 'formula_' ::=
| g1 = g2 :: :: co_rewrite
| no_duplicates </ zi // i /> :: :: no_duplicates_name
| no_duplicates </ bindingi // i /> :: :: no_duplicates_binding
+ | no_duplicates </ li // i /> :: :: no_duplicates_label
| not formula :: :: not
| isUnLiftedTyCon T :: :: isUnLiftedTyCon
| compatibleUnBoxedTys t1 t2 :: :: compatibleUnBoxedTys
@@ -395,6 +436,7 @@ formula :: 'formula_' ::=
}{\quad [[formula2]]} \end{array} }}
| ( formula ) :: :: parens
| n elt G :: :: context_inclusion
+ | l elt D :: :: join_context_inclusion
| vars1 = vars2 :: :: vars_rewrite
| </ Gi $ // i /> = inits ( </ nj // j /> ) :: :: context_folding
| </ substi $ // i /> = inits ( </ [ nj |-> tj ] // j /> ) :: :: subst_folding
@@ -421,6 +463,8 @@ formula :: 'formula_' ::=
| role_list1 = role_list2 :: :: eq_role_list
| R1 /= R2 :: :: role_neq
| R1 = R2 :: :: eq_role
+ | R1 <= R2 :: :: lte_role
+ {{ tex [[R1]] \leq [[R2]] }}
| </ Ki // i /> = tyConDataCons T :: :: tyConDataCons
| O ( n ) = R :: :: role_lookup
| R elt role_list :: :: role_elt
@@ -431,11 +475,14 @@ formula :: 'formula_' ::=
| no other case matches :: :: no_other_case
{{ tex \text{no other case matches} }}
| t = coercionKind g :: :: coercionKind
+ | R = coercionRole g :: :: coercionRole
| Just ( t1 , t2 ) = coaxrProves mu </ si // i /> </ ( s'j , s''j ) // j />
:: :: coaxrProves
| mu1 = mu2 :: :: mu_rewrite
| classifiesTypeWithValues k :: :: classifies_type_with_values
| z elt vars :: :: in_vars
+ | split _ I s = types :: :: split_type
+ {{ tex \mathop{\textsf{split} }_{[[I]]} [[s]] = [[types]] }}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Subrules and Parsing %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -461,6 +508,7 @@ Subst_TyMapping <= Type_TySubstListPost
Subst_TmMapping <= Type_TySubstListPost
Expr_Type <= formula_e_rewrite
+Expr_Jump <= Expr_Apps
Coercion_TyConAppCo <= Coercion_AppCo
diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott
index 8fb9b0e068..b9dc4ff893 100644
--- a/docs/core-spec/OpSem.ott
+++ b/docs/core-spec/OpSem.ott
@@ -13,6 +13,10 @@
% point for an analysis of FC's operational semantics. If you don't want to
% worry about mutual recursion (and who does?), you can even drop the
% environment S.
+%
+% Join points are ignored here because operationally they work exactly the same
+% as regular bindings. Simply read "join" as "let" and "jump" as application to
+% see how a (well-typed!) program should run.
grammar
@@ -30,19 +34,39 @@ e1 e2 --> e1' e2
----------------------------- :: Beta
(\n.e1) e2 --> e1[n |-> e2]
-g0 = sym (nth 0 g)
-g1 = nth 1 g
+% g : (t1 -> t2) ~Rep# (t3 -> t4)
+% e2 : t3
+% g0 : t3 ~Rep# t1
+% g1 : t2 ~Rep# t4
+g0 = sym (nth Rep 2 g)
+g1 = nth Rep 3 g
not e2 is_a_type
not e2 is_a_coercion
----------------------------------------------- :: Push
((\n.e1) |> g) e2 --> (\n.e1 |> g1) (e2 |> g0)
----------------------------------------- :: TPush
-((\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
+% g : (forall (a : k1). t1) ~Rep# (forall (a : k2). t2)
+% t : k2
+% g' : k2 ~# k1
+% t' : k1
+g' = sym (nth Nom 0 g)
+t' = t |> g'
+-------------------------------------------------------- :: TPush
+((\n.e) |> g) t --> ((\n.e) t') |> (g @ (sym <t> Nom MCo g'))
+
+% g : ((t1 ~rho# t2) -> t3) ~Rep# ((t4 ~rho# t5) -> t6)
+% g2 : t3 ~Rep# t6
+% g' : t4 ~rho# t5
+% g0 : t1 ~rho# t4
+% g1 : t5 ~rho# t2
+% recall that (->) :: forall r1 r2. TYPE r1 -> TYPE r2 -> Type
+% and that (~#) :: forall k1 k2. k1 -> k2 -> TYPE (TupleRep '[])
+% so pulling out the first visible argument for both is argument 2,
+% and the second visible argument for both is argument 3
+R = coercionRole g'
+g0 = nth R 2 (nth Rep 2 g)
+g1 = sym (nth R 3 (nth Rep 2 g))
+g2 = nth Rep 3 g
------------------------------- :: CPush
((\n.e) |> g) g' --> (\n.e |> g2) (g0 ; g' ; g1)
@@ -76,9 +100,10 @@ no other case matches
------------------------------------------------------------ :: MatchDefault
case e as n return t of </ alti // i /> --> u[n |-> e]
-T </ taa // aa /> k'~#k T </ t'aa // aa /> = coercionKind g
+T </ taa // aa /> k'~Rep# k T </ t'aa // aa /> = coercionKind g
+</ Raa // aa /> = tyConRoles T
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 />
+</ e'cc = ecc |> (t1cc $ </ [alphaaa_kaa |-> nth Raa aa g] // aa /> </ [betabb_k'bb |-> <sbb>] // bb />) // cc />
--------------------------- :: CasePush
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 />
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index d1d89055e7..952a172e6f 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 23 October, 2015
+\Large 26 January, 2018
\end{center}
\section{Introduction}
@@ -89,6 +89,10 @@ variables:
\ottn
}
+\gram{
+\ottl
+}
+
We sometimes omit the type/kind annotation to a variable when it is obvious from context.
\subsection{Expressions}
@@ -112,13 +116,39 @@ is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{coreSyn/CoreSy
\item Types and coercions can only appear on the right-hand-side of an application.
\item The $[[t]]$ form of an expression must not then turn out to be a coercion.
In other words, the payload inside of a \texttt{Type} constructor must not turn out
-to be built with \texttt{CoercionTy}.
+to be built with \texttt{CoercionTy}.
+\item Join points (introduced by $[[join]]$ expressions) follow the invariants
+laid out in \verb|Note [Invariants on join points]| in
+\ghcfile{coreSyn/CoreSyn.lhs}:
+\begin{enumerate}
+ \item All occurences must be tail calls. This is enforced in our typing
+ rules using the label environment $[[D]]$.
+ \item Each join point has a \emph{join arity}. In this document, we write
+ each label as $[[p/I_t]]$ for the name $[[p]]$, the type $[[t]]$, and the
+ join arity $[[I]]$. The right-hand side of the binding must begin with at
+ least $[[I]]$ lambdas. This is enforced implicitly in
+ \ottdrulename{Tm\_JoinNonRec} and \ottdrulename{Tm\_JoinRec} by the use of
+ $[[split]]$ meta-function.
+ \item If the binding is recursive, then all other bindings in the recursive
+ group must be join points. We enforce this in our reformulation of the
+ grammar; in the actual AST, a $[[join]]$ is simply a $[[let]]$ where each
+ identifier is flagged as a join id, so this invariant requires that this
+ flag must be consistent across a recursive binding.
+ \item The binding's type must not be polymorphic in its return type. This
+ is expressed in \ottdrulename{Label\_Label}; see
+ Section~\ref{sec:name_consistency}.
+\end{enumerate}
+
\end{itemize}
Bindings for $[[let]]$ statements:
\gram{\ottbinding}
+Bindings for $[[join]]$ statements:
+
+\gram{\ottjbinding}
+
Case alternatives:
\gram{\ottalt}
@@ -139,9 +169,10 @@ A program is just a list of bindings:
\gram{\ottt}
-\ctor{ForAllTy}s are represented in two different ways, depending on whether
-the \ctor{ForAllTy} is anonymous (written $[[t1 -> t2]]$) or
-named (written $[[forall n . t]]$).
+\ctor{FunTy} is the special case for non-dependent function type. The
+\ctor{TyBinder} in \ghcfile{types/TyCoRep.lhs} distinguishes whether a binder is
+anonymous (\ctor{FunTy}) or named (\ctor{ForAllTy}). See
+\verb|Note [TyBinders]| in \ghcfile{types/TyCoRep.lhs}.
There are some invariants on types:
\begin{itemize}
@@ -152,7 +183,7 @@ $[[T]]$. It should be another application or a type variable.
does \emph{not} need to be saturated.
\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{ForAllTy}.
+The constructor for a saturated $[[(->)]]$ is \texttt{FunTy}.
\item A type-level literal is represented in GHC with a different datatype than
a term-level literal, but we are ignoring this distinction here.
\item A coercion used as a type should appear only in the right-hand side of
@@ -164,7 +195,7 @@ are purely representational. The metatheory would remain the same if these forms
were removed in favor of $[[t1 t2]]$. Nevertheless, we keep all three forms in
this documentation to accurately reflect the implementation.
-The \texttt{Named} variant of a \texttt{Binder} (the first argument to a
+The \texttt{ArgFlag} field of a \texttt{TyVarBinder} (the first argument to a
\texttt{ForAllTy}) also tracks visibility of arguments. Visibility affects
only source Haskell, and is omitted from this presentation.
@@ -176,14 +207,14 @@ We use the notation $[[t1 k1~#k2 t2]]$ to stand for $[[(~#) k1 k2 t1 t2]]$.
Invariants on coercions:
\begin{itemize}
-\item $[[<t1 t2>_R]]$ is used; never $[[<t1>_R <t2>_Nom]]$.
-\item If $[[<T>_R]]$ is applied to some coercions, at least one of which is not
-reflexive, use $[[T_R </ gi // i />]]$, never $[[<T>_R g1 g2]] \ldots$.
+\item $[[<t1 t2>]]$ is used; never $[[<t1> <t2> ]]$.
+\item If $[[<T>]]$ is applied to some coercions, at least one of which is not
+reflexive, use $[[T_R </ gi // i />]]$, never $[[<T> g1 g2]] \ldots$.
\item The $[[T]]$ in $[[T_R </gi//i/>]]$ is never a type synonym, though it could
be a type function.
\item Every non-reflexive coercion coerces between two distinct types.
\item The name in a coercion must be a term-level name (\ctor{Id}).
-\item The contents of $[[<t>_R]]$ must not be a coercion. In other words,
+\item The contents of $[[<t>]]$ must not be a coercion. In other words,
the payload in a \texttt{Refl} must not be built with \texttt{CoercionTy}.
\end{itemize}
@@ -201,6 +232,20 @@ for more background.
\gram{\ottR}
+The \texttt{GRefl} constructor taks an $[[mg]]$. It wraps a kind coercion, which
+might be reflexive or any coercion:
+
+\gram{\ottmg}
+
+A nominal reflexive coercion is quite common, so we keep the special form
+\texttt{Refl}. Invariants on reflexive coercions:
+
+\begin{itemize}
+\item Always use $[[<t>]]$; never $[[<t> Nom MRefl]]$.
+\item All invariants on $[[<t>]]$ hold for $[[<t> R MRefl]]$.
+\item Use $[[<t> Rep MRefl]]$; never $[[sub <t>]]$.
+\end{itemize}
+
Is it a left projection or a right projection?
\gram{\ottLorR}
@@ -275,15 +320,21 @@ synonym for $[[TYPE 'Unlifted]]$.
\section{Contexts}
The functions in \ghcfile{coreSyn/CoreLint.lhs} use the \texttt{LintM} monad.
-This monad contains a context with a set of bound variables $[[G]]$. The
-formalism treats $[[G]]$ as an ordered list, but GHC uses a set as its
+This monad contains a context with a set of bound variables $[[G]]$ and a set
+of bound labels $[[D]]$. The formalism treats $[[G]]$ and $[[D]]$ as ordered
+lists, but GHC uses sets as its
representation.
\gram{
\ottG
}
-We assume the Barendregt variable convention that all new variables are
+\gram{
+\ottD
+}
+
+We assume the Barendregt variable convention that all new variables and labels
+are
fresh in the context. In the implementation, of course, some work is done
to guarantee this freshness. In particular, adding a new type variable to
the context sometimes requires creating a new, fresh variable name and then
@@ -313,12 +364,29 @@ Here is the definition of $[[vars_of]]$, taken from \coderef{coreSyn/CoreSyn.lhs
\end{array}
\]
+Here is the definition of $[[split]]$, which has no direct analogue in the
+source but simplifies the presentation here:
+
+\[
+\begin{array}{ll}
+[[split]]_0 [[t]] &= [[t]] \\
+[[split]]_n ([[s -> t]]) &= [[s]] \; ([[split]]_{n-1} [[t]]) \\
+[[split]]_n ([[forall alpha _ k . t]]) &= [[k]] \; ([[split]]_{n-1} [[t]])
+\end{array}
+\]
+
+The idea is simply to peel off the leading $i$ argument types (which may be
+kinds for type arguments) from a given type and return them in a sequence, with
+the return type (given $i$ arguments) as the final element of the sequence.
+
\subsection{Binding consistency}
\ottdefnlintXXbind{}
\ottdefnlintSingleBinding{}
+\ottdefnlintSingleBindingXXjoins{}
+
In the GHC source, this function contains a number of other checks, such
as for strictness and exportability. See the source code for further information.
@@ -376,11 +444,19 @@ See Section~\ref{sec:tyconroles} for more information about $[[tyConRolesX]]$, a
see Section~\ref{sec:axiom_rules} for more information about $[[coaxrProves]]$.
\subsection{Name consistency}
+\label{sec:name_consistency}
-There are two very similar checks for names, one declared as a local function:
+There are three very similar checks for names, two performed as part of
+\coderef{coreSyn/CoreLint.hs}{lintSingleBinding}:
\ottdefnlintSingleBindingXXlintBinder{}
+\ottdefnlintSingleBindingXXlintBinderXXjoin{}
+
+The point of the extra checks on $[[t']]$ is that a join point's type cannot be
+polymorphic in its return type; see \texttt{Note [The polymorphism rule of join
+points]} in \ghcfile{coreSyn/CoreSyn.hs}.
+
\ottdefnlintBinder{}
\subsection{Substitution consistency}
@@ -477,6 +553,12 @@ 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{Join points}
+Dealing with join points properly here would be cumbersome and pointless, since
+by design they work no differently than functions as far as FC is concerned.
+Reading $[[join]]$ as $[[let]]$ and $[[jump]]$ as application should tell you
+all need to know.
+
\subsection{Operational semantics rules}
\ottdefnstep{}
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index dde6c9eeba..a0a73cbaba 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf
Binary files differ
View Lorry Controller Status