diff options
| author | ningning <xnningxie@gmail.com> | 2018-07-26 17:20:42 -0400 |
|---|---|---|
| committer | Ben Gamari <ben@smart-cactus.org> | 2018-07-27 12:29:40 -0400 |
| commit | e5f3de2cf2f52e7079cbee624ae91beecf663f87 (patch) | |
| tree | 8f02e56aecbdad396c73c4a2bd468f4b0ad68d8c /docs/core-spec/CoreSyn.ott | |
| parent | 3581212e3a5ba42114f47ed83a96322e0e8028ab (diff) | |
| download | haskell-e5f3de2cf2f52e7079cbee624ae91beecf663f87.tar.gz | |
update core-spec for GRefl and re-factored Refl
Ticket #15192 introduced the generalized reflexive coercion `GRefl` and
nominal reflexive `Refl`, and removed `CoherenceCo`. Update core-spec
accordingly. Not sure about notations though; suggestions on more
concise notations would be great.
Test Plan: Read core-spec.pdf
Reviewers: goldfire, bgamari
Reviewed By: goldfire
Subscribers: rwbarton, thomie, carter
Differential Revision: https://phabricator.haskell.org/D4984
Diffstat (limited to 'docs/core-spec/CoreSyn.ott')
| -rw-r--r-- | docs/core-spec/CoreSyn.ott | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott index 57ed6e261d..b11730c276 100644 --- a/docs/core-spec/CoreSyn.ott +++ b/docs/core-spec/CoreSyn.ott @@ -138,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 }} @@ -156,7 +158,6 @@ g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coder {{ 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 }} @@ -170,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 }} @@ -397,6 +403,8 @@ terminals :: 'terminals_' ::= | classifiesTypeWithValues :: :: ctwv {{ tex \textsf{classifiesTypeWithValues} }} | 0 :: :: zero {{ tex 0 }} | +1 :: :: succ {{ tex +1 }} + | MRefl :: :: mrefl {{ tex \cdot }} + | MCo :: :: mco %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Formulae %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |