78118d532c43deb08c6a01a78118826b48f5e57f
[ghc.git] / docs / core-spec / CoreSyn.ott
1 %%
2 %% CoreSyn.ott
3 %%
4 %% defines formal version of core syntax
5 %%
6 %% See accompanying README file
7
8 embed {{ tex-preamble
9   \newcommand{\coderef}[2]{\ghcfile{#1}:\texttt{#2}%
10 }
11   \newcommand{\keyword}[1]{\textbf{#1} }
12   \newcommand{\labeledjudge}[1]{\vdash_{\!\!\mathsf{#1} } }
13   \newcommand{\ctor}[1]{\texttt{#1}%
14 }
15 }}
16
17 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
18 %%  Metavariables  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
19 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
20
21 metavar x, c ::=   {{ com Term-level variable names }}
22 metavar p ::=    {{ com Labels }}
23 metavar alpha {{ tex \alpha }}, beta {{ tex \beta }} ::=
24   {{ com Type-level variable names }}
25 metavar N ::=   {{ com Type-level constructor names }}
26 metavar M ::=   {{ com Axiom rule names }}
27
28 indexvar i, j, kk {{ tex k }}, aa {{ tex a }}, bb {{ tex b }}, cc {{ tex c }} ::= {{ com Indices to be used in lists }}
29
30 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
31 %%  Syntax  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
32 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
33
34 grammar
35
36 lit {{ tex \textsf{lit} }} :: 'Literal_' ::=
37   {{ com Literals, \coderef{basicTypes/Literal.lhs}{Literal} }}
38
39 z :: 'Name_' ::= {{ com Term or type name }}
40   | alpha           ::   :: Type    {{ com Type-level name }}
41   | x               ::   :: Term    {{ com Term-level name }}
42
43 n, m, aname {{ tex \alpha }}, xname {{ tex x }} :: 'Var_' ::= {{ com Variable names, \coderef{basicTypes/Var.lhs}{Var} }}
44   | z _ t           ::   :: IdOrTyVar   {{ com Name, labeled with type/kind }}
45     {{ tex {[[z]]}^{[[t]]} }}
46   | z $             :: M :: NoSupScript {{ com Name without an explicit type/kind }}
47   | K               :: M :: DataCon     {{ com Data constructor }}
48
49 l :: 'Label_' ::= {{ com Labels for join points, also \coderef{basicTypes/Var.lhs}{Var} }}
50   | p / I _ t     ::   :: Label   {{ com Label with join arity and type }}
51     {{ tex  {[[p]]}_{[[I]]}^{[[t]]} }}
52
53 vars :: 'Vars_' ::= {{ com List of variables }}
54   | </ ni // , // i />       ::   :: List
55   | fv ( t )                 :: M :: fv_t
56     {{ tex \textit{fv}([[t]]) }}
57   | fv ( e )                 :: M :: fv_e
58     {{ tex \textit{fv}([[e]]) }}
59   | empty                    :: M :: empty
60   | vars1 \inter vars2       :: M :: intersection
61     {{ tex [[vars1]] \cap [[vars2]] }}
62
63 labels :: 'Labels_' ::= {{ com List of labels }}
64   | </ li // , // i />       ::   :: List
65   | empty                    :: M :: empty
66
67 e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.lhs}{Expr} }}
68   | n                                            ::   :: Var  {{ com \ctor{Var}: Variable }}
69   | lit                                          ::   :: Lit  {{ com \ctor{Lit}: Literal }}
70   | e1 e2                                        ::   :: App  {{ com \ctor{App}: Application }}
71   | jump l </ ui // i />                         ::   :: Jump {{ com \ctor{App}: Jump }}
72   | \ n . e                                      ::   :: Lam  {{ com \ctor{Lam}: Abstraction }}
73   | let binding in e                             ::   :: Let  {{ com \ctor{Let}: Variable binding }}
74   | join jbinding in e                           ::   :: Join {{ com \ctor{Let}: Join binding }}
75   | case e as n return t of </ alti // | // i /> ::   :: Case {{ com \ctor{Case}: Pattern match }}
76   | e |> g                                       ::   :: Cast {{ com \ctor{Cast}: Cast }}
77   | e { tick }                                   ::   :: Tick {{ com \ctor{Tick}: Internal note }}
78     {{ tex {[[e]]}_{\{[[tick]]\} } }}
79   | t                                            ::   :: Type {{ com \ctor{Type}: Type }}
80   | g                                            ::   :: Coercion {{ com \ctor{Coercion}: Coercion }}
81   | e subst                                      :: M :: Subst {{ com Substitution }}
82   | ( e )                                        :: M :: Parens {{ com Parenthesized expression }}
83   | e </ ui // i />                              :: M :: Apps {{ com Nested application }}
84   | S ( n )                                      :: M :: Lookup {{ com Lookup in the runtime store }}
85   | \\ e                                         :: M :: Newline
86     {{ tex \qquad \\ \multicolumn{1}{r}{[[e]]} }}
87
88 binding :: 'Bind_' ::= {{ com Let-bindings, \coderef{coreSyn/CoreSyn.lhs}{Bind} }}
89   | n = e                         ::   :: NonRec  {{ com \ctor{NonRec}: Non-recursive binding }}
90   | rec </ ni = ei // ;; // i /> ::   :: Rec     {{ com \ctor{Rec}: Recursive binding }}
91
92 jbinding :: 'JoinBind_' ::= {{ com Join bindings, also \coderef{coreSyn/CoreSyn.lhs}{Bind} }}
93   | l </ ni // i /> = e     ::   :: NonRec {{ com \ctor{NonRec}: Non-recursive binding }}
94   | rec </ li </ nij // j /> = ei // i /> :: :: Rec {{ com \ctor{Rec}: Recursive binding }}
95
96 alt :: 'Alt_' ::= {{ com Case alternative, \coderef{coreSyn/CoreSyn.lhs}{Alt} }}
97   | Kp </ ni // i /> -> e    ::   :: Alt  {{ com Constructor applied to fresh names }}
98
99 tick :: 'Tickish_' ::= {{ com Internal notes, \coderef{coreSyn/CoreSyn.lhs}{Tickish} }}
100
101 Kp {{ tex \mathbb{K} }} :: 'AltCon_' ::= {{ com Constructors used in patterns, \coderef{coreSyn/CoreSyn.lhs}{AltCon} }}
102   | K        ::   :: DataAlt         {{ com \ctor{DataAlt}: Data constructor }}
103   | lit      ::   :: LitAlt          {{ com \ctor{LitAlt}: Literal (such as an integer or character) }}
104   | _        ::   :: DEFAULT         {{ com \ctor{DEFAULT}: Wildcard }}
105
106 program :: 'CoreProgram_' ::= {{ com A System FC program, \coderef{coreSyn/CoreSyn.lhs}{CoreProgram} }}
107   | </ bindingi // i />  ::   :: CoreProgram  {{ com List of bindings }}
108
109 %% TYPES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
110
111 t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}, phi {{ tex \phi }}
112   :: 'Type_' ::= {{ com Types/kinds, \coderef{types/TyCoRep.lhs}{Type} }}
113   | n                       ::   :: TyVarTy       {{ com \ctor{TyVarTy}: Variable }}
114   | t1 t2                   ::   :: AppTy         {{ com \ctor{AppTy}: Application }}
115   | T </ ti // i />         ::   :: TyConApp      {{ com \ctor{TyConApp}: Application of type constructor }}
116   | t1 -> t2                ::   :: FunTy         {{ com \ctor{ForAllTy (Anon ...) ...}: Function }}
117   | forall n . t            ::   :: ForAllTy      {{ com \ctor{ForAllTy (Named ...) ...}: Type and coercion polymorphism }}
118   | lit                     ::   :: LitTy         {{ com \ctor{LitTy}: Type-level literal }}
119   | t |> g                  ::   :: CastTy        {{ com \ctor{CastTy}: Kind cast }}
120   | g                       ::   :: CoercionTy    {{ com \ctor{CoercionTy}: Coercion used in type }}
121   | tyConKind T             :: M :: tyConKind     {{ com \coderef{types/TyCon.lhs}{tyConKind} }}
122   | t1 k1 ~# k2 t2          :: M :: unliftedEq    {{ com Metanotation for coercion types }}
123     {{ tex [[t1]] \mathop{ {}^{[[k1]]}\!\! \sim_{\#}^{[[k2]]} } [[t2]] }}
124   | t1 k1 ~Rep# k2 t2         :: M :: unliftedREq   {{ com Metanotation for coercion types }}
125     {{ tex [[t1]] \mathop{ {}^{[[k1]]}\!\! \sim_{\mathsf{R}\#}^{[[k2]]} } [[t2]] }}
126   | literalType lit         :: M :: literalType   {{ com \coderef{basicTypes/Literal.lhs}{literalType} }}
127   | ( t )                   :: M :: parens        {{ com Parentheses }}
128   | { t }                   :: M :: IParens       {{ com Invisible parentheses }}
129     {{ tex [[t]] }}
130   | t [ n |-> s ]           :: M :: TySubst       {{ com Type substitution }}
131   | subst ( k )             :: M :: TySubstList   {{ com Type substitution list }}
132   | t subst                 :: M :: TySubstListPost {{ com Type substitution list }}
133   | dataConRepType K        :: M :: dataConRepType {{ com Type of DataCon }}
134   | forall </ ni // , // i /> . t
135                             :: M :: ForAllTys     {{ com Nested polymorphism }}
136   | </ ti // i /> $ -> t'   :: M :: FunTys        {{ com Nested arrows }}
137
138 %% COERCIONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
139
140 g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coderef{types/TyCoRep.lhs}{Coercion} }}
141   | < t > _ R               ::   :: Refl          {{ com \ctor{Refl}: Reflexivity }}
142     {{ tex {\langle [[t]] \rangle}_{[[R]]} }}
143   | T RA </ gi // i />      ::   :: TyConAppCo    {{ com \ctor{TyConAppCo}: Type constructor application }}
144   | g1 g2                   ::   :: AppCo         {{ com \ctor{AppCo}: Application }}
145   | forall z : h . g        ::   :: ForAllCo      {{ com \ctor{ForAllCo}: Polymorphism }}
146     {{ tex [[forall]] [[z]]{:}[[h]].[[g]] }}
147   | n                       ::   :: CoVarCo       {{ com \ctor{CoVarCo}: Variable }}
148   | C ind </ gi // i />     ::   :: AxiomInstCo   {{ com \ctor{AxiomInstCo}: Axiom application }}
149   | prov < t1 , t2 > _ R ^ ( h ) ::  :: UnivCo    {{ com \ctor{UnivCo}: Universal coercion }}
150     {{ tex {}_{[[prov]]}{\langle [[t1]], [[t2]] \rangle}_{[[R]]}^{[[h]]} }}
151   | sym g                   ::   :: SymCo         {{ com \ctor{SymCo}: Symmetry }}
152   | g1 ; g2                 ::   :: TransCo       {{ com \ctor{TransCo}: Transitivity }}
153   | mu </ ti // i /> $ </ gj // j />
154                             ::   :: AxiomRuleCo   {{ com \ctor{AxiomRuleCo}: Axiom-rule application (for type-nats) }}
155   | nth I g                 ::   :: NthCo         {{ com \ctor{NthCo}: Projection (0-indexed) }}
156     {{ tex \textsf{nth}^{[[I]]}\,[[g]] }}
157   | LorR g                  ::   :: LRCo          {{ com \ctor{LRCo}: Left/right projection }}
158   | g @ h                   ::   :: InstCo        {{ com \ctor{InstCo}: Instantiation }}
159   | g |> h                  ::   :: CoherenceCo   {{ com \ctor{CoherenceCo}: Coherence }}
160   | kind g                  ::   :: KindCo        {{ com \ctor{KindCo}: Kind extraction }}
161   | sub g                   ::   :: SubCo         {{ com \ctor{SubCo}: Sub-role --- convert nominal to representational }}
162   | ( g )                   :: M :: Parens        {{ com Parentheses }}
163   | t $ liftingsubst        :: M :: Lifted        {{ com Type lifted to coercion }}
164
165 prov :: 'UnivCoProvenance_' ::= {{ com \ctor{UnivCo} provenance, \coderef{types/TyCoRep.lhs}{UnivCoProvenance} }}
166   | UnsafeCoerceProv   ::   :: UnsafeCoerceProv  {{ com From \texttt{unsafeCoerce\#} }}
167     {{ tex \mathsf{unsafe} }}
168   | PhantomProv        ::   :: PhantomProv       {{ com From the need for a phantom coercion }}
169     {{ tex \mathsf{phant} }}
170   | ProofIrrelProv     ::   :: ProofIrrelProv    {{ com From proof irrelevance }}
171     {{ tex \mathsf{irrel} }}
172
173 LorR :: 'LeftOrRight_' ::= {{ com left or right deconstructor, \coderef{types/TyCoRep.lhs}{LeftOrRight} }}
174   | Left             ::   :: CLeft                {{ com \ctor{CLeft}: Left projection }}
175   | Right            ::   :: CRight               {{ com \ctor{CRight}: Right projection }}
176
177 C :: 'CoAxiom_' ::= {{ com Axioms, \coderef{types/TyCon.lhs}{CoAxiom} }}
178   | T RA </ axBranchi // ; // i />     ::   :: CoAxiom  {{ com \ctor{CoAxiom}: Axiom }}
179   | ( C )                              :: M :: Parens   {{ com Parentheses }}
180
181 R {{ tex \rho }} :: 'Role_' ::= {{ com Roles, \coderef{types/CoAxiom.lhs}{Role} }}
182   | Nom              ::   :: Nominal              {{ com Nominal }}
183     {{ tex \mathsf{N} }}
184   | Rep              ::   :: Representational     {{ com Representational }}
185     {{ tex \mathsf{R} }}
186   | Ph               ::   :: Phantom              {{ com Phantom }}
187     {{ tex \mathsf{P} }}
188   | role_list [ i ]  :: M :: RoleListIndex        {{ com Look up in list }}
189
190 axBranch, b :: 'CoAxBranch_' ::= {{ com Axiom branches, \coderef{types/TyCon.lhs}{CoAxBranch} }}
191   | forall </ ni RAi // i /> . ( </ tj // j /> ~> s )  ::   :: CoAxBranch  {{ com \ctor{CoAxBranch}: Axiom branch }}
192   | ( </ axBranchi // i /> ) [ ind ]               :: M :: lookup      {{ com List lookup }}
193
194 mu {{ tex \mu }} :: 'CoAxiomRule_' ::= {{ com CoAxiomRules, \coderef{types/CoAxiom.lhs}{CoAxiomRule} }}
195   | M ( I , role_list , R' )   ::  :: CoAxiomRule  {{ com Named rule, with parameter info }}
196     {{ tex {[[M]]}_{([[I]], [[ role_list ]], [[R']])} }}
197
198 %% TYCONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
199
200 T :: 'TyCon_' ::= {{ com Type constructors, \coderef{types/TyCon.lhs}{TyCon} }}
201   | ( -> )       ::   :: FunTyCon          {{ com \ctor{FunTyCon}: Arrow }}
202
203   % the following also includes TupleTyCon, SynTyCon
204   | N _ k        ::   :: AlgTyCon          {{ com \ctor{AlgTyCon}, \ctor{TupleTyCon}, \ctor{SynTyCon}: algebraic, tuples, families, and synonyms }}
205     {{ tex {[[N]]}^{[[k]]} }}
206   | H            ::   :: PrimTyCon         {{ com \ctor{PrimTyCon}: Primitive tycon }}
207   | ' K          ::   :: PromotedDataCon   {{ com \ctor{PromotedDataCon}: Promoted data constructor }}
208   | dataConTyCon K :: M :: dataConTyCon    {{ com TyCon extracted from DataCon }}
209
210 H :: 'PrimTyCon_' ::= {{ com Primitive type constructors, \coderef{prelude/TysPrim.lhs}{} }}
211   | Int#         ::   :: intPrimTyCon           {{ com Unboxed Int (\texttt{intPrimTyCon}) }}
212   | ( ~# )       ::   :: eqPrimTyCon            {{ com Unboxed equality (\texttt{eqPrimTyCon}) }}
213   | ( ~Rep# )      ::   :: eqReprPrimTyCon        {{ com Unboxed representational equality (\texttt{eqReprPrimTyCon}) }}
214   | *            ::   :: liftedTypeKindTyCon    {{ com Kind of lifted types (\texttt{liftedTypeKindTyCon}) }}
215   | #            ::   :: unliftedTypeKindTyCon  {{ com Kind of unlifted types (\texttt{unliftedTypeKindTyCon}) }}
216   | OpenKind     ::   :: openTypeKindTyCon      {{ com Either $*$ or $\#$ (\texttt{openTypeKindTyCon}) }}
217   | Constraint   ::   :: constraintTyCon        {{ com Constraint (\texttt{constraintTyCon}) }}
218   | TYPE         ::   :: TYPE                   {{ com TYPE (\texttt{tYPETyCon}) }}
219   | Levity       ::   :: Levity                 {{ com Levity (\texttt{LevityTyCon}) }}
220
221 K :: 'DataCon_' ::= {{ com Data constructors, \coderef{basicTypes/DataCon.lhs}{DataCon} }}
222   | Lifted       ::   :: Lifted       {{ com \ctor{Lifted}, a lifted type }}
223   | Unlifted     ::   :: Unlifted     {{ com \ctor{Unlifted}, an unlifted type }}
224
225 %% CONTEXTS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
226
227 G {{ tex \Gamma }} :: 'LintM_Bindings_' ::= {{ com List of bindings, \coderef{coreSyn/CoreLint.lhs}{LintM} }}
228   | n                        ::   :: Binding   {{ com Single binding }}
229   | </ Gi // , // i />       ::   :: Concat    {{ com Context concatenation }}
230   | vars_of binding          :: M :: VarsOf    {{ com \coderef{coreSyn/CoreSyn.lhs}{bindersOf} }}
231
232 D {{ tex \Delta }} :: 'LintM_JoinBindings_' ::= {{ com List of join bindings, \coderef{coreSyn/CoreLint.lhs}{LintM} }}
233   | l                        ::   :: Binding   {{ com Single binding }}
234   | </ Di // , // i />       ::   :: Concat    {{ com Context concatenation }}
235   | empty                    :: M :: Empty     {{ com Empty context }}
236   | labels_of binding        :: M :: LabelsOf  {{ com \coderef{coreSyn/CoreSyn.lhs}{bindersOf} }}
237
238 O {{ tex \Omega }} :: 'VarEnv_Role_' ::= {{ com Mapping from type variables to roles }}
239   | </ ni : Ri // i />       ::   :: List      {{ com List of bindings }}
240   | O1 , O2                  :: M :: Concat    {{ com Concatenate two lists }}
241
242 S {{ tex \Sigma }} :: 'St_' ::= {{ com Runtime store }}
243   | [ n |-> e ]            ::   :: Binding  {{ com Single binding }}
244   | </ Si // , // i />     ::   :: Concat   {{ com Store concatentation }}
245
246 %% UTILITY %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
247
248 B {{ tex \mathbb{B} }} :: 'Bool_' ::= {{ com Booleans in metatheory }}
249   | false        ::   :: False
250   | true         ::   :: True
251
252 kinded_types {{ tex \overline{(\sigma_i : \kappa_i)}^i }} :: 'Kinded_Types_' ::= {{ com List of types with kinds }}
253   | </ ( si : ki ) // , // i />    ::   :: List
254   | empty                          :: M :: empty
255
256 subst :: 'Subst_' ::= {{ com List of substitutions }}
257   | [ n |-> t ]        ::   :: TyMapping
258   | [ n |-> e ]        ::   :: TmMapping
259   | [ z |-> t ]        ::   :: TyMapping_Raw
260   | </ substi // i />  ::   :: List
261   | empty              :: M :: Empty
262
263 liftingsubst :: 'LiftSubst_' ::= {{ com List of lifting substitutions }}
264   | [ n |-> g ]               ::   :: Mapping
265   | </ liftingsubsti // i />  ::   :: List
266
267 ind, I {{ tex i }} :: 'Ind_' ::= {{ com Indices, numbers }}
268   | i                           ::   :: index
269   | length </ ti // i />        :: M :: length_t
270   | length </ gi // i />        :: M :: length_g
271   | length </ axBranchi // i /> :: M :: length_axBranch
272   | tyConArity T                :: M :: tyConArity
273   | ind - 1                     :: M :: decrement
274   | -1                          :: M :: minusOne
275   | 0                           :: M :: zero
276   | 1                           :: M :: one
277   | 2                           :: M :: two
278
279 terms :: 'Terms_' ::= {{ com List of terms }}
280   | </ ei // i />      ::   :: List
281
282 types :: 'Types_' ::= {{ com List of types }}
283   | </ ti // i />      ::   :: List
284
285 names {{ tex \overline{n_i}^i }} :: 'Names_' ::= {{ com List of names }}
286   | </ ni // , // i />      ::   :: List
287   | empty                   :: M :: Empty
288   | names , n               :: M :: Snoc
289
290 namesroles {{ tex \overline{n_i \!\! {}_{\rho_i} }^i }} :: 'NamesRoles_' ::= {{ com List of names, annotated with roles }}
291   | </ ni RAi // , // i />    ::   :: List
292   | empty                     :: M :: Empty
293   | namesroles , n RA         :: M :: Snoc
294
295 gs {{ tex \overline{\gamma} }} :: 'Cos_' ::= {{ com List of coercions }}
296   | </ gi // , // i />     ::   :: List
297   | empty                  :: M :: Empty
298   | gs , g                 :: M :: Snoc
299
300 RA {{ tex {\!\!{}_{\rho} } }} :: 'RoleAnnot_' ::= {{ com Role annotation }}
301   | _ R                    :: M :: annotation
302   {{ tex {\!\!{}_{[[R]]} } }}
303   | _ ^^ R                 :: M :: spaced_annotation
304   {{ tex {}_{[[R]]} }}
305
306 role_list {{ tex {\overline{\rho_j} }^j }} :: 'RoleList_' ::= {{ com List of roles }}
307   | </ Ri // , // i />       ::   :: List
308   | tyConRolesX R T          :: M :: tyConRolesX
309   | tyConRoles T             :: M :: tyConRoles
310   | ( role_list )            :: M :: Parens
311   | { role_list }            :: M :: Braces
312   | take ( ind , role_list ) :: M :: Take
313
314 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
315 %%  Terminals  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
316 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
317
318 terminals :: 'terminals_' ::=
319   | \            ::   :: lambda           {{ tex \lambda }}
320   | let          ::   :: let              {{ tex \keyword{let} }}
321   | join         ::   :: join             {{ tex \keyword{join} }}
322   | in           ::   :: key_in           {{ tex \keyword{in} }}
323   | rec          ::   :: rec              {{ tex \keyword{rec} }}
324   | and          ::   :: key_and          {{ tex \keyword{and} }}
325   | jump         ::   :: jump             {{ tex \keyword{jump} }}
326   | case         ::   :: case             {{ tex \keyword{case} }}
327   | of           ::   :: of               {{ tex \keyword{of} }}
328   | ->           ::   :: arrow            {{ tex \to }}
329   | |>           ::   :: cast             {{ tex \triangleright }}
330   | forall       ::   :: forall           {{ tex {\forall}\! }}
331   | ==>!         ::   :: unsafe
332     {{ tex \twoheadrightarrow\!\!\!\!\!\! \raisebox{-.3ex}{!} \,\,\,\,\, }}
333   | sym          ::   :: sym              {{ tex \textsf{sym} }}
334   | ;            ::   :: trans            {{ tex \fatsemi }}
335   | ;;           ::   :: semi             {{ tex ; }}
336   | Left         ::   :: Left             {{ tex \textsf{left} }}
337   | Right        ::   :: Right            {{ tex \textsf{right} }}
338   | _            ::   :: wildcard         {{ tex \text{\textvisiblespace} }}
339   | Int#         ::   :: int_hash         {{ tex {\textsf{Int} }_{\#} }}
340   | ~#           ::   :: eq_hash          {{ tex \mathop{ {\sim}_{\#} } }}
341   | ~Rep#        ::   :: eq_repr_hash     {{ tex \mathop{ {\sim}_{\mathsf{R}\#} } }}
342   | OpenKind     ::   :: OpenKind         {{ tex \textsf{OpenKind} }}
343   | ok           ::   :: ok               {{ tex \textsf{ ok} }}
344   | no_duplicates ::  :: no_duplicates    {{ tex \textsf{no\_duplicates } }}
345   | vars_of      ::   :: vars_of          {{ tex \textsf{vars\_of } }}
346   | split        ::   :: split            {{ tex \mathop{\textsf{split} } }}
347   | not          ::   :: not              {{ tex \neg }}
348   | isUnLiftedTyCon :: :: isUnLiftedTyCon {{ tex \textsf{isUnLiftedTyCon} }}
349   | compatibleUnBoxedTys :: :: compatibleUnBoxedTys {{ tex \textsf{compatibleUnBoxedTys} }}
350   | false        ::   :: false            {{ tex \textsf{false} }}
351   | true         ::   :: true             {{ tex \textsf{true} }}
352   | \/           ::   :: or               {{ tex \vee }}
353   | /\           ::   :: and              {{ tex \mathop{\wedge} }}
354   | elt          ::   :: elt              {{ tex \in }}
355   | /=           ::   :: neq              {{ tex \neq }}
356   | literalType  ::   :: literalType      {{ tex \textsf{literalType} }}
357   | |->          ::   :: mapsto           {{ tex \mapsto }}
358   | <-           ::   :: assignment       {{ tex \leftarrow }}
359   | $            ::   :: marker           {{ tex  }}
360   | inits        ::   :: inits            {{ tex \textsf{inits} }}
361   | ~>           ::   :: squigarrow       {{ tex \rightsquigarrow }}
362   | tyConKind    ::   :: tyConKind        {{ tex \mathop{\textsf{tyConKind} } }}
363   | empty        ::   :: empty            {{ tex \cdot }}
364   | length       ::   :: length           {{ tex \mathsf{length} }}
365   | ~            ::   :: eq               {{ tex \sim }}
366   | tyConArity   ::   :: tyConArity       {{ tex \textsf{tyConArity} }}
367   | dataConTyCon ::   :: dataConTyCon     {{ tex \textsf{dataConTyCon} }}
368   | dataConRepType :: :: dataConRepType   {{ tex \textsf{dataConRepType} }}
369   | isNewTyCon   ::   :: isNewTyCon       {{ tex \textsf{isNewTyCon} }}
370   | Constraint   ::   :: Constraint       {{ tex \textsf{Constraint} }}
371   | TYPE         ::   :: TYPE             {{ tex \textsf{TYPE} }}
372   | RuntimeRep   ::   :: RuntimeRep       {{ tex \textsf{RuntimeRep} }}
373   | LiftedRep    ::   :: LiftedRep        {{ tex \textsf{LiftedRep} }}
374   | UnliftedRep  ::   :: UnliftedRep      {{ tex \textsf{UnliftedRep} }}
375   | no_conflict  ::   :: no_conflict      {{ tex \textsf{no\_conflict} }}
376   | apart        ::   :: apart            {{ tex \textsf{apart} }}
377   | kind         ::   :: kind             {{ tex \textsf{kind} }}
378   | kapp         ::   :: kapp             {{ tex \textsf{kapp} }}
379   | sub          ::   :: sub              {{ tex \textsf{sub} }}
380   | #            ::   :: free             {{ tex \mathop{ \# } }}
381   | BOX          ::   :: BOX              {{ tex \square }}
382   | *            ::   :: star             {{ tex \star }}
383   | unify        ::   :: unify            {{ tex \textsf{unify} }}
384   | tyConRolesX  ::   :: tyConRolesX      {{ tex \textsf{tyConRolesX} }}
385   | tyConRoles   ::   :: tyConRoles       {{ tex \textsf{tyConRoles} }}
386   | tyConDataCons ::  :: tyConDataCons    {{ tex \textsf{tyConDataCons} }}
387   | validRoles   ::   :: validRoles       {{ tex \textsf{validRoles} }}
388   | validDcRoles ::   :: validDcRoles     {{ tex \textsf{validDcRoles} }}
389   | -->          ::   :: steps            {{ tex \longrightarrow }}
390   | coercionKind ::   :: coercionKind     {{ tex \textsf{coercionKind} }}
391   | take         ::   :: take             {{ tex \textsf{take}\! }}
392   | coaxrProves  ::   :: coaxrProves      {{ tex \textsf{coaxrProves} }}
393   | Just         ::   :: Just             {{ tex \textsf{Just} }}
394   | \\           ::   :: newline          {{ tex \\ }}
395   | classifiesTypeWithValues :: :: ctwv   {{ tex \textsf{classifiesTypeWithValues} }}
396   | 0            ::   :: zero             {{ tex 0 }}
397   | +1           ::   :: succ             {{ tex +1 }}
398
399 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
400 %%  Formulae  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
401 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
402
403 formula :: 'formula_' ::=
404   | judgement                          ::   :: judgement
405   | formula1 ... formulai              ::   :: dots
406   | G1 = G2                            ::   :: context_rewrite
407   | D1 = D2                            ::   :: join_context_rewrite
408   | t1 = t2                            ::   :: type_rewrite
409   | t1 /= t2                           ::   :: type_inequality
410   | e1 /=e e2                          ::   :: expr_inequality
411     {{ tex [[e1]] \neq [[e2]] }}
412   | 0 <= ind1 < ind2                   ::   :: in_bounds
413     {{ tex 0 \leq [[ind1]] < [[ind2]] }}
414   | g1 = g2                            ::   :: co_rewrite
415   | no_duplicates </ zi // i />        ::   :: no_duplicates_name
416   | no_duplicates </ bindingi // i />  ::   :: no_duplicates_binding
417   | no_duplicates </ li // i />        ::   :: no_duplicates_label
418   | not formula                        ::   :: not
419   | isUnLiftedTyCon T                  ::   :: isUnLiftedTyCon
420   | compatibleUnBoxedTys t1 t2         ::   :: compatibleUnBoxedTys
421   | formula1 /\ formula2               ::   :: and
422   | formula1 \/ formula2               ::   :: or
423   | ( formula1 ) \\/ ( formula2 )      ::   :: newline
424     {{ tex \begin{array}{@{}l@{}%
425 }[[formula1]] \vee \\ \multicolumn{1}{@{}r@{}%
426 }{\quad [[formula2]]} \end{array} }}
427   | ( formula )                        ::   :: parens
428   | n elt G                            ::   :: context_inclusion
429   | l elt D                            ::   :: join_context_inclusion
430   | vars1 = vars2                      ::   :: vars_rewrite
431   | </ Gi $ // i /> = inits ( </ nj // j /> ) :: :: context_folding
432   | </ substi $ // i /> = inits ( </ [ nj |-> tj ] // j /> ) :: :: subst_folding
433   | ind1 = ind2                        ::   :: eq_ind
434   | ind1 < ind2                        ::   :: lt
435   | G |- tylit lit : k                 ::   :: lintTyLit
436     {{ tex [[G]] \labeledjudge{tylit} [[lit]] : [[k]] }}
437   | isNewTyCon T                       ::   :: isNewTyCon
438   | k1 elt { </ ki // , // i /> }      ::   :: kind_elt
439   | e is_a_type                        ::   :: is_a_type
440     {{ tex \exists \tau \text{ s.t.~} [[e]] = \tau }}
441   | t is_a_coercion_type               ::   :: is_a_coercion_type
442     {{ tex \exists \tau_1, \tau_2, \kappa_1, \kappa_2 \text{ s.t.~} [[t]] =
443            \tau_1 \mathop{ {}^{\kappa_1} {\sim}_{\#}^{\kappa_2} } \tau_2 }}
444   | e is_a_coercion                    ::   :: is_a_coercion
445     {{ tex \exists \gamma \text{ s.t.~} [[e]] = \gamma }}
446   | t is_a_prop                        ::   :: is_a_prop
447     {{ tex \exists \tau_1, \tau_2, \kappa \text{ s.t.~} [[t]] =
448            \tau_1 \mathop{ {\sim}_{\#}^{\kappa} } \tau_2 }}
449   | axBranch1 = axBranch2              ::   :: branch_rewrite
450   | C1 = C2                            ::   :: axiom_rewrite
451   | apart ( </ ti // i /> , </ sj // j /> ) :: :: apart
452   | unify ( </ ti // i /> , </ sj // j /> ) = subst :: :: unify
453   | role_list1 = role_list2            ::   :: eq_role_list
454   | R1 /= R2                           ::   :: role_neq
455   | R1 = R2                            ::   :: eq_role
456   | </ Ki // i /> = tyConDataCons T    ::   :: tyConDataCons
457   | O ( n ) = R                        ::   :: role_lookup
458   | R elt role_list                    ::   :: role_elt
459   | formula1 => formula2               ::   :: implication
460     {{ tex [[formula1]] \implies [[formula2]] }}
461   | alt1 = alt2                        ::   :: alt_rewrite
462   | e1 = e2                            ::   :: e_rewrite
463   | no other case matches              ::   :: no_other_case
464     {{ tex \text{no other case matches} }}
465   | t = coercionKind g                 ::   :: coercionKind
466   | Just ( t1 , t2 ) = coaxrProves mu </ si // i /> </ ( s'j , s''j ) // j />
467                                        ::   :: coaxrProves
468   | mu1 = mu2                          ::   :: mu_rewrite
469   | classifiesTypeWithValues k         ::   :: classifies_type_with_values
470   | z elt vars                         ::   :: in_vars
471   | split _ I s = types                ::   :: split_type
472     {{ tex \mathop{\textsf{split} }_{[[I]]} [[s]] = [[types]] }}
473
474 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
475 %%  Subrules and Parsing  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
476 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
477
478 parsing
479
480 TyCon_FunTyCon right Type_AppTy
481 TyCon_PrimTyCon right Type_AppTy
482 TyCon_AlgTyCon right Type_AppTy
483 TyCon_PromotedDataCon right Type_AppTy
484
485 TyCon_FunTyCon right Coercion_AppCo
486 TyCon_PrimTyCon right Coercion_AppCo
487 TyCon_AlgTyCon right Coercion_AppCo
488 TyCon_PromotedDataCon right Coercion_AppCo
489
490 Subst_TyMapping <= Type_TySubstList
491 Subst_TmMapping <= Type_TySubstList
492 Subst_List <= Type_TySubstList
493
494 Subst_TyMapping <= Type_TySubstListPost
495 Subst_TmMapping <= Type_TySubstListPost
496
497 Expr_Type <= formula_e_rewrite
498 Expr_Jump <= Expr_Apps
499
500 Coercion_TyConAppCo <= Coercion_AppCo
501
502 Coercion_TyConAppCo <= Type_CoercionTy
503 Coercion_CoVarCo <= Type_CoercionTy
504
505 Type_unliftedEq left Var_IdOrTyVar
506
507 Expr_Coercion <= Subst_TmMapping
508
509 Type_CastTy <= Var_IdOrTyVar
510