Commit 9c0e3e44 authored by Takenobu Tani's avatar Takenobu Tani

core-spec: Modify `.lhs` to `.hs` (source files)

Modify old filename `.lhs` to `.hs` in following files:

  * docs/core-spec/README
  * docs/core-spec/CoreLint.ott
  * docs/core-spec/CoreSyn.ott
  * docs/core-spec/core-spec.mng

[ci skip]
parent 7fcc07c8
......@@ -12,7 +12,7 @@
defns
CoreLint :: '' ::=
defn |- prog program :: :: lintCoreBindings :: 'Prog_' {{ com Program typing, \coderef{coreSyn/CoreLint.lhs}{lintCoreBindings} }}
defn |- prog program :: :: lintCoreBindings :: 'Prog_' {{ com Program typing, \coderef{coreSyn/CoreLint.hs}{lintCoreBindings} }}
{{ tex \labeledjudge{prog} [[program]] }}
by
......@@ -22,7 +22,7 @@ no_duplicates </ bindingi // i />
--------------------- :: CoreBindings
|-prog </ bindingi // i />
defn G |- bind binding :: :: lint_bind :: 'Binding_' {{ com Binding typing, \coderef{coreSyn/CoreLint.lhs}{lint\_bind} }}
defn G |- bind binding :: :: lint_bind :: 'Binding_' {{ com Binding typing, \coderef{coreSyn/CoreLint.hs}{lint\_bind} }}
{{ tex [[G]] \labeledjudge{bind} [[binding]] }}
by
......@@ -34,7 +34,7 @@ G |-bind n = e
---------------------- :: Rec
G |-bind rec </ ni = ei // i />
defn G |- sbind n <- e :: :: lintSingleBinding :: 'SBinding_' {{ com Single binding typing, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding} }}
defn G |- sbind n <- e :: :: lintSingleBinding :: 'SBinding_' {{ com Single binding typing, \coderef{coreSyn/CoreLint.hs}{lintSingleBinding} }}
{{ tex [[G]] \labeledjudge{sbind} [[n]] [[<-]] [[e]] }}
by
......@@ -45,7 +45,7 @@ G |-name z_t ok
----------------- :: SingleBinding
G |-sbind z_t <- e
defn G ; D |-sjbind l vars <- e : t :: :: lintSingleBinding_joins :: 'SJBinding_' {{ com Single join binding typing, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding} }}
defn G ; D |-sjbind l vars <- e : t :: :: lintSingleBinding_joins :: 'SJBinding_' {{ com Single join binding typing, \coderef{coreSyn/CoreLint.hs}{lintSingleBinding} }}
{{ tex [[G]];[[D]] \labeledjudge{sjbind} [[l]] \, [[vars]] [[<-]] [[e]] : [[t]] }}
by
......@@ -60,7 +60,7 @@ split_I s = </ sj // j /> t
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} }}
{{ com Expression typing, \coderef{coreSyn/CoreLint.hs}{lintCoreExpr} }}
{{ tex [[G]]; [[D]] \labeledjudge{tm} [[e]] : [[t]] }}
by
......@@ -171,7 +171,7 @@ G |-co g : t1 k1~Rep k2 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} }}
{{ com Name consistency check, \coderef{coreSyn/CoreLint.hs}{lintSingleBinding\#lintBinder} }}
{{ tex [[G]] \labeledjudge{n} [[n]] [[ok]] }}
by
......@@ -197,7 +197,7 @@ k' = * \/ k' = #
G |-label p / I _ t ok
defn G |- bnd n ok :: :: lintBinder :: 'Binding_'
{{ com Binding consistency, \coderef{coreSyn/CoreLint.lhs}{lintBinder} }}
{{ com Binding consistency, \coderef{coreSyn/CoreLint.hs}{lintBinder} }}
{{ tex [[G]] \labeledjudge{bnd} [[n]] [[ok]] }}
by
......@@ -211,7 +211,7 @@ G |-ki k ok
G |-bnd alpha_k ok
defn G |- co g : t1 k1 ~ R k2 t2 :: :: lintCoercion :: 'Co_'
{{ com Coercion typing, \coderef{coreSyn/CoreLint.lhs}{lintCoercion} }}
{{ com Coercion typing, \coderef{coreSyn/CoreLint.hs}{lintCoercion} }}
{{ tex [[G]] \labeledjudge{co} [[g]] : [[t1]] \mathop{ {}^{[[k1]]} {\sim}_{[[R]]}^{[[k2]]} } [[t2]] }}
by
......@@ -365,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}{lintCoercion\#check\_ki} }}
{{ com Axiom argument kinding, \coderef{coreSyn/CoreLint.hs}{lintCoercion\#check\_ki} }}
{{ tex [[G]] \labeledjudge{axk} [ [[namesroles]] [[|->]] [[gs]] ] [[~>]] ([[subst1]], [[subst2]]) }}
by
......@@ -379,7 +379,7 @@ G |-co g0 : t1 {subst1(k)}~R subst2(k) t2
G |-axk [ namesroles, n_R |-> gs, g0 ] ~> (subst1 [n |-> t1], subst2 [n |-> t2])
defn validRoles T :: :: checkValidRoles :: 'Cvr_'
{{ com Type constructor role validity, \coderef{typecheck/TcTyClsDecls.lhs}{checkValidRoles} }}
{{ com Type constructor role validity, \coderef{typecheck/TcTyClsDecls.hs}{checkValidRoles} }}
by
</ Ki // i /> = tyConDataCons T
......@@ -389,7 +389,7 @@ by
validRoles T
defn validDcRoles </ Raa // aa /> K :: :: check_dc_roles :: 'Cdr_'
{{ com Data constructor role validity, \coderef{typecheck/TcTyClsDecls.lhs}{check\_dc\_roles} }}
{{ com Data constructor role validity, \coderef{typecheck/TcTyClsDecls.hs}{check\_dc\_roles} }}
by
forall </ naa // aa />. forall </ mbb // bb />. </ tcc // cc /> $ -> T </ naa // aa /> = dataConRepType K
......@@ -398,7 +398,7 @@ forall </ naa // aa />. forall </ mbb // bb />. </ tcc // cc /> $ -> T </ naa //
validDcRoles </ Raa // aa /> K
defn O |- t : R :: :: check_ty_roles :: 'Ctr_'
{{ com Type role validity, \coderef{typecheck/TcTyClsDecls.lhs}{check\_ty\_roles} }}
{{ com Type role validity, \coderef{typecheck/TcTyClsDecls.hs}{check\_ty\_roles} }}
{{ tex [[O]] \labeledjudge{ctr} [[t]] : [[R]] }}
by
......@@ -441,7 +441,7 @@ O |- t |> g : R
O |- g : Ph
defn R1 <= R2 :: :: ltRole :: 'Rlt_'
{{ com Sub-role relation, \coderef{types/Coercion.lhs}{ltRole} }}
{{ com Sub-role relation, \coderef{types/Coercion.hs}{ltRole} }}
{{ tex [[R1]] \leq [[R2]] }}
by
......@@ -455,7 +455,7 @@ R <= Ph
R <= R
defn G |- ki k ok :: :: lintKind :: 'K_'
{{ com Kind validity, \coderef{coreSyn/CoreLint.lhs}{lintKind} }}
{{ com Kind validity, \coderef{coreSyn/CoreLint.hs}{lintKind} }}
{{ tex [[G]] \labeledjudge{k} [[k]] [[ok]] }}
by
......@@ -468,7 +468,7 @@ G |-ty k : #
G |-ki k ok
defn G |- ty t : k :: :: lintType :: 'Ty_'
{{ com Kinding, \coderef{coreSyn/CoreLint.lhs}{lintType} }}
{{ com Kinding, \coderef{coreSyn/CoreLint.hs}{lintType} }}
{{ tex [[G]] \labeledjudge{ty} [[t]] : [[k]] }}
by
......@@ -518,7 +518,7 @@ G |-co g : t1 k1 ~Rep k2 t2
G |-ty g : (~Rep#) k1 k2 t1 t2
defn G |- subst n |-> t ok :: :: lintTyKind :: 'Subst_'
{{ com Substitution consistency, \coderef{coreSyn/CoreLint.lhs}{lintTyKind} }}
{{ com Substitution consistency, \coderef{coreSyn/CoreLint.hs}{lintTyKind} }}
{{ tex [[G]] \labeledjudge{subst} [[n]] [[|->]] [[t]] [[ok]] }}
by
......@@ -527,7 +527,7 @@ G |-ty t : k
G |-subst z_k |-> t ok
defn G ; D ; s |- altern alt : t :: :: lintCoreAlt :: 'Alt_'
{{ com Case alternative consistency, \coderef{coreSyn/CoreLint.lhs}{lintCoreAlt} }}
{{ com Case alternative consistency, \coderef{coreSyn/CoreLint.hs}{lintCoreAlt} }}
{{ tex [[G]];[[D]];[[s]] \labeledjudge{alt} [[alt]] : [[t]] }}
by
......@@ -552,7 +552,7 @@ G'; D |-tm 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} }}
{{ com Telescope substitution, \coderef{types/Type.hs}{applyTys} }}
by
--------------------- :: Empty
......@@ -564,7 +564,7 @@ t'' = t'[n |-> s]
t'' = (forall n. t) { s, </ si // i /> }
defn G |- altbnd vars : t1 ~> t2 :: :: lintAltBinders :: 'AltBinders_'
{{ com Case alternative binding consistency, \coderef{coreSyn/CoreLint.lhs}{lintAltBinders} }}
{{ com Case alternative binding consistency, \coderef{coreSyn/CoreLint.hs}{lintAltBinders} }}
{{ tex [[G]] \labeledjudge{altbnd} [[vars]] : [[t1]] [[~>]] [[t2]] }}
by
......@@ -585,7 +585,7 @@ G |-altbnd </ ni // i /> : t2 ~> s
G |-altbnd x_t1, </ ni // i /> : (t1 -> t2) ~> s
defn G |- arrow k1 -> k2 : k :: :: lintArrow :: 'Arrow_'
{{ com Arrow kinding, \coderef{coreSyn/CoreLint.lhs}{lintArrow} }}
{{ com Arrow kinding, \coderef{coreSyn/CoreLint.hs}{lintArrow} }}
{{ tex [[G]] \labeledjudge{\rightarrow} [[k1]] [[->]] [[k2]] : [[k]] }}
by
......@@ -595,7 +595,7 @@ k2 = TYPE s
G |-arrow k1 -> k2 : *
defn G |- app kinded_types : k1 ~> k2 :: :: lint_app :: 'App_'
{{ com Type application kinding, \coderef{coreSyn/CoreLint.lhs}{lint\_app} }}
{{ com Type application kinding, \coderef{coreSyn/CoreLint.hs}{lint\_app} }}
{{ tex [[G]] \labeledjudge{app} [[kinded_types]] : [[k1]] [[~>]] [[k2]] }}
by
......@@ -611,7 +611,7 @@ G |-app </ (ti : ki) // i /> : k2[z_k1 |-> t] ~> k'
G |-app (t : k1), </ (ti : ki) // i /> : (forall z_k1. k2) ~> k'
defn no_conflict ( C , </ sj // j /> , ind1 , ind2 ) :: :: check_no_conflict :: 'NoConflict_'
{{ com \parbox{5in}{Branched axiom conflict checking, \coderef{types/OptCoercion.lhs}{checkAxInstCo} \\ and \coderef{types/FamInstEnv.lhs}{compatibleBranches} } }}
{{ com \parbox{5in}{Branched axiom conflict checking, \coderef{types/OptCoercion.hs}{checkAxInstCo} \\ and \coderef{types/FamInstEnv.hs}{compatibleBranches} } }}
by
------------------------------------------------ :: NoBranch
......
......@@ -34,19 +34,19 @@ indexvar i, j, kk {{ tex k }}, aa {{ tex a }}, bb {{ tex b }}, cc {{ tex c }} ::
grammar
lit {{ tex \textsf{lit} }} :: 'Literal_' ::=
{{ com Literals, \coderef{basicTypes/Literal.lhs}{Literal} }}
{{ com Literals, \coderef{basicTypes/Literal.hs}{Literal} }}
z :: 'Name_' ::= {{ com Term or type name }}
| alpha :: :: Type {{ com Type-level name }}
| x :: :: Term {{ com Term-level name }}
n, m, aname {{ tex \alpha }}, xname {{ tex x }} :: 'Var_' ::= {{ com Variable names, \coderef{basicTypes/Var.lhs}{Var} }}
n, m, aname {{ tex \alpha }}, xname {{ tex x }} :: 'Var_' ::= {{ com Variable names, \coderef{basicTypes/Var.hs}{Var} }}
| z _ t :: :: IdOrTyVar {{ com Name, labeled with type/kind }}
{{ tex {[[z]]}^{[[t]]} }}
| 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} }}
l :: 'Label_' ::= {{ com Labels for join points, also \coderef{basicTypes/Var.hs}{Var} }}
| p / I _ t :: :: Label {{ com Label with join arity and type }}
{{ tex {[[p]]}_{[[I]]}^{[[t]]} }}
......@@ -64,7 +64,7 @@ labels :: 'Labels_' ::= {{ com List of labels }}
| </ li // , // i /> :: :: List
| empty :: M :: empty
e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.lhs}{Expr} }}
e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.hs}{Expr} }}
| n :: :: Var {{ com \ctor{Var}: Variable }}
| lit :: :: Lit {{ com \ctor{Lit}: Literal }}
| e1 e2 :: :: App {{ com \ctor{App}: Application }}
......@@ -85,31 +85,31 @@ e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.lhs}{Expr} }}
| \\ e :: M :: Newline
{{ tex \qquad \\ \multicolumn{1}{r}{[[e]]} }}
binding :: 'Bind_' ::= {{ com Let-bindings, \coderef{coreSyn/CoreSyn.lhs}{Bind} }}
binding :: 'Bind_' ::= {{ com Let-bindings, \coderef{coreSyn/CoreSyn.hs}{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} }}
jbinding :: 'JoinBind_' ::= {{ com Join bindings, also \coderef{coreSyn/CoreSyn.hs}{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} }}
alt :: 'Alt_' ::= {{ com Case alternative, \coderef{coreSyn/CoreSyn.hs}{Alt} }}
| Kp </ ni // i /> -> e :: :: Alt {{ com Constructor applied to fresh names }}
tick :: 'Tickish_' ::= {{ com Internal notes, \coderef{coreSyn/CoreSyn.lhs}{Tickish} }}
tick :: 'Tickish_' ::= {{ com Internal notes, \coderef{coreSyn/CoreSyn.hs}{Tickish} }}
Kp {{ tex \mathbb{K} }} :: 'AltCon_' ::= {{ com Constructors used in patterns, \coderef{coreSyn/CoreSyn.lhs}{AltCon} }}
Kp {{ tex \mathbb{K} }} :: 'AltCon_' ::= {{ com Constructors used in patterns, \coderef{coreSyn/CoreSyn.hs}{AltCon} }}
| K :: :: DataAlt {{ com \ctor{DataAlt}: Data constructor }}
| lit :: :: LitAlt {{ com \ctor{LitAlt}: Literal (such as an integer or character) }}
| _ :: :: DEFAULT {{ com \ctor{DEFAULT}: Wildcard }}
program :: 'CoreProgram_' ::= {{ com A System FC program, \coderef{coreSyn/CoreSyn.lhs}{CoreProgram} }}
program :: 'CoreProgram_' ::= {{ com A System FC program, \coderef{coreSyn/CoreSyn.hs}{CoreProgram} }}
| </ bindingi // i /> :: :: CoreProgram {{ com List of bindings }}
%% TYPES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}, phi {{ tex \phi }}
:: 'Type_' ::= {{ com Types/kinds, \coderef{types/TyCoRep.lhs}{Type} }}
:: 'Type_' ::= {{ com Types/kinds, \coderef{types/TyCoRep.hs}{Type} }}
| n :: :: TyVarTy {{ com \ctor{TyVarTy}: Variable }}
| t1 t2 :: :: AppTy {{ com \ctor{AppTy}: Application }}
| T </ ti // i /> :: :: TyConApp {{ com \ctor{TyConApp}: Application of type constructor }}
......@@ -118,12 +118,12 @@ t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}, phi {{ tex \phi }}
| 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 }}
| tyConKind T :: M :: tyConKind {{ com \coderef{types/TyCon.lhs}{tyConKind} }}
| tyConKind T :: M :: tyConKind {{ com \coderef{types/TyCon.hs}{tyConKind} }}
| t1 k1 ~# k2 t2 :: M :: unliftedEq {{ com Metanotation for coercion types }}
{{ tex [[t1]] \mathop{ {}^{[[k1]]}\!\! \sim_{\#}^{[[k2]]} } [[t2]] }}
| t1 k1 ~Rep# k2 t2 :: M :: unliftedREq {{ com Metanotation for coercion types }}
{{ tex [[t1]] \mathop{ {}^{[[k1]]}\!\! \sim_{\mathsf{R}\#}^{[[k2]]} } [[t2]] }}
| literalType lit :: M :: literalType {{ com \coderef{basicTypes/Literal.lhs}{literalType} }}
| literalType lit :: M :: literalType {{ com \coderef{basicTypes/Literal.hs}{literalType} }}
| ( t ) :: M :: parens {{ com Parentheses }}
| { t } :: M :: IParens {{ com Invisible parentheses }}
{{ tex [[t]] }}
......@@ -137,7 +137,7 @@ 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} }}
g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coderef{types/TyCoRep.hs}{Coercion} }}
| < t > :: :: Refl {{ com \ctor{Refl}: Nominal Reflexivity }}
{{ tex {\langle [[t]] \rangle} }}
| < t > R mg :: :: GRefl {{ com \ctor{GRefl}: Generalized Reflexivity }}
......@@ -163,7 +163,7 @@ g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coder
| ( g ) :: M :: Parens {{ com Parentheses }}
| t $ liftingsubst :: M :: Lifted {{ com Type lifted to coercion }}
prov :: 'UnivCoProvenance_' ::= {{ com \ctor{UnivCo} provenance, \coderef{types/TyCoRep.lhs}{UnivCoProvenance} }}
prov :: 'UnivCoProvenance_' ::= {{ com \ctor{UnivCo} provenance, \coderef{types/TyCoRep.hs}{UnivCoProvenance} }}
| UnsafeCoerceProv :: :: UnsafeCoerceProv {{ com From \texttt{unsafeCoerce\#} }}
{{ tex \mathsf{unsafe} }}
| PhantomProv :: :: PhantomProv {{ com From the need for a phantom coercion }}
......@@ -171,20 +171,20 @@ 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} }}
mg {{ tex m }} :: 'MCoercion_' ::= {{ com A possibly reflexive coercion , \coderef{types/TyCoRep.hs}{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} }}
LorR :: 'LeftOrRight_' ::= {{ com left or right deconstructor, \coderef{types/TyCoRep.hs}{LeftOrRight} }}
| Left :: :: CLeft {{ com \ctor{CLeft}: Left projection }}
| Right :: :: CRight {{ com \ctor{CRight}: Right projection }}
C :: 'CoAxiom_' ::= {{ com Axioms, \coderef{types/TyCon.lhs}{CoAxiom} }}
C :: 'CoAxiom_' ::= {{ com Axioms, \coderef{types/TyCon.hs}{CoAxiom} }}
| T RA </ axBranchi // ; // i /> :: :: CoAxiom {{ com \ctor{CoAxiom}: Axiom }}
| ( C ) :: M :: Parens {{ com Parentheses }}
R {{ tex \rho }} :: 'Role_' ::= {{ com Roles, \coderef{types/CoAxiom.lhs}{Role} }}
R {{ tex \rho }} :: 'Role_' ::= {{ com Roles, \coderef{types/CoAxiom.hs}{Role} }}
| Nom :: :: Nominal {{ com Nominal }}
{{ tex \mathsf{N} }}
| Rep :: :: Representational {{ com Representational }}
......@@ -193,17 +193,17 @@ R {{ tex \rho }} :: 'Role_' ::= {{ com Roles, \coderef{types/CoAxiom.lhs}{Role}
{{ tex \mathsf{P} }}
| role_list [ i ] :: M :: RoleListIndex {{ com Look up in list }}
axBranch, b :: 'CoAxBranch_' ::= {{ com Axiom branches, \coderef{types/TyCon.lhs}{CoAxBranch} }}
axBranch, b :: 'CoAxBranch_' ::= {{ com Axiom branches, \coderef{types/TyCon.hs}{CoAxBranch} }}
| forall </ ni RAi // i /> . ( </ tj // j /> ~> s ) :: :: CoAxBranch {{ com \ctor{CoAxBranch}: Axiom branch }}
| ( </ axBranchi // i /> ) [ ind ] :: M :: lookup {{ com List lookup }}
mu {{ tex \mu }} :: 'CoAxiomRule_' ::= {{ com CoAxiomRules, \coderef{types/CoAxiom.lhs}{CoAxiomRule} }}
mu {{ tex \mu }} :: 'CoAxiomRule_' ::= {{ com CoAxiomRules, \coderef{types/CoAxiom.hs}{CoAxiomRule} }}
| M ( I , role_list , R' ) :: :: CoAxiomRule {{ com Named rule, with parameter info }}
{{ tex {[[M]]}_{([[I]], [[ role_list ]], [[R']])} }}
%% TYCONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
T :: 'TyCon_' ::= {{ com Type constructors, \coderef{types/TyCon.lhs}{TyCon} }}
T :: 'TyCon_' ::= {{ com Type constructors, \coderef{types/TyCon.hs}{TyCon} }}
| ( -> ) :: :: FunTyCon {{ com \ctor{FunTyCon}: Arrow }}
% the following also includes TupleTyCon, SynTyCon
......@@ -213,7 +213,7 @@ T :: 'TyCon_' ::= {{ com Type constructors, \coderef{types/TyCon.lhs}{TyCon} }}
| ' K :: :: PromotedDataCon {{ com \ctor{PromotedDataCon}: Promoted data constructor }}
| dataConTyCon K :: M :: dataConTyCon {{ com TyCon extracted from DataCon }}
H :: 'PrimTyCon_' ::= {{ com Primitive type constructors, \coderef{prelude/TysPrim.lhs}{} }}
H :: 'PrimTyCon_' ::= {{ com Primitive type constructors, \coderef{prelude/TysPrim.hs}{} }}
| Int# :: :: intPrimTyCon {{ com Unboxed Int (\texttt{intPrimTyCon}) }}
| ( ~# ) :: :: eqPrimTyCon {{ com Unboxed equality (\texttt{eqPrimTyCon}) }}
| ( ~Rep# ) :: :: eqReprPrimTyCon {{ com Unboxed representational equality (\texttt{eqReprPrimTyCon}) }}
......@@ -224,22 +224,22 @@ H :: 'PrimTyCon_' ::= {{ com Primitive type constructors, \coderef{prelude/TysPr
| TYPE :: :: TYPE {{ com TYPE (\texttt{tYPETyCon}) }}
| Levity :: :: Levity {{ com Levity (\texttt{LevityTyCon}) }}
K :: 'DataCon_' ::= {{ com Data constructors, \coderef{basicTypes/DataCon.lhs}{DataCon} }}
K :: 'DataCon_' ::= {{ com Data constructors, \coderef{basicTypes/DataCon.hs}{DataCon} }}
| Lifted :: :: Lifted {{ com \ctor{Lifted}, a lifted type }}
| Unlifted :: :: Unlifted {{ com \ctor{Unlifted}, an unlifted type }}
%% CONTEXTS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
G {{ tex \Gamma }} :: 'LintM_Bindings_' ::= {{ com List of bindings, \coderef{coreSyn/CoreLint.lhs}{LintM} }}
G {{ tex \Gamma }} :: 'LintM_Bindings_' ::= {{ com List of bindings, \coderef{coreSyn/CoreLint.hs}{LintM} }}
| n :: :: Binding {{ com Single binding }}
| </ Gi // , // i /> :: :: Concat {{ com Context concatenation }}
| vars_of binding :: M :: VarsOf {{ com \coderef{coreSyn/CoreSyn.lhs}{bindersOf} }}
| vars_of binding :: M :: VarsOf {{ com \coderef{coreSyn/CoreSyn.hs}{bindersOf} }}
D {{ tex \Delta }} :: 'LintM_JoinBindings_' ::= {{ com List of join bindings, \coderef{coreSyn/CoreLint.lhs}{LintM} }}
D {{ tex \Delta }} :: 'LintM_JoinBindings_' ::= {{ com List of join bindings, \coderef{coreSyn/CoreLint.hs}{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} }}
| labels_of binding :: M :: LabelsOf {{ com \coderef{coreSyn/CoreSyn.hs}{bindersOf} }}
O {{ tex \Omega }} :: 'VarEnv_Role_' ::= {{ com Mapping from type variables to roles }}
| </ ni : Ri // i /> :: :: List {{ com List of bindings }}
......
......@@ -30,7 +30,7 @@ into LaTeX math-mode code. Thus, the file core-spec.mng is the source for
core-spec.tex, which gets processed into core-spec.pdf.
The file CoreSyn.ott contains the grammar of System FC, mostly extracted from
compiler/coreSyn/CoreSyn.lhs. Here are a few pointers to help those of you
compiler/coreSyn/CoreSyn.hs. Here are a few pointers to help those of you
unfamiliar with Ott:
- The {{ ... }} snippets are called "homs", and they assist ott in translating
......@@ -69,7 +69,7 @@ your notation to LaTeX. Three different homs are used:
it if necessary to disambiguate other parses.
The file CoreLint.ott contains inductively defined judgements for many of the
functions in compiler/coreSyn/CoreLint.lhs. Each judgement is labeled with an
functions in compiler/coreSyn/CoreLint.hs. Each judgement is labeled with an
abbreviation to distinguish it from the others. These abbreviations appear in
the source code right after a turnstile |-. The declaration for each judgment
contains a reference to the function it represents. Each rule is labeled with
......@@ -80,4 +80,4 @@ If you need help with these files or do not know how to edit them, please
contact Richard Eisenberg (eir@cis.upenn.edu).
[1] http://www.cl.cam.ac.uk/~pes20/ott/
[2] http://www.cl.cam.ac.uk/~pes20/ott/ott_manual_0.21.2.pdf
\ No newline at end of file
[2] http://www.cl.cam.ac.uk/~pes20/ott/ott_manual_0.21.2.pdf
......@@ -71,8 +71,8 @@ Literals do not play a major role, so we leave them abstract:
\gram{\ottlit}
We also leave abstract the function \coderef{basicTypes/Literal.lhs}{literalType}
and the judgment \coderef{coreSyn/CoreLint.lhs}{lintTyLit} (written $[[G |-tylit lit : k]]$).
We also leave abstract the function \coderef{basicTypes/Literal.hs}{literalType}
and the judgment \coderef{coreSyn/CoreLint.hs}{lintTyLit} (written $[[G |-tylit lit : k]]$).
\subsection{Variables}
\enlargethispage{10pt} % without this first line of "z" definition is placed on
......@@ -109,7 +109,7 @@ $[[let]]$ may be of type \texttt{Addr\#} if it's a primitive string literal.
See \verb|#top_level_invariant#| in \ghcfile{coreSyn/CoreSyn.hs}.
\item The right-hand side of a non-recursive $[[let]]$ and the argument
of an application may be of unlifted type, but only if the expression
is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{coreSyn/CoreSyn.lhs}.
is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{coreSyn/CoreSyn.hs}.
\item We allow a non-recursive $[[let]]$ for bind a type variable.
\item The $[[_]]$ case for a $[[case]]$ must come first.
\item The list of case alternatives must be exhaustive.
......@@ -119,7 +119,7 @@ In other words, the payload inside of a \texttt{Type} constructor must not turn
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}:
\ghcfile{coreSyn/CoreSyn.hs}:
\begin{enumerate}
\item All occurences must be tail calls. This is enforced in our typing
rules using the label environment $[[D]]$.
......@@ -170,9 +170,9 @@ A program is just a list of bindings:
\gram{\ottt}
\ctor{FunTy} is the special case for non-dependent function type. The
\ctor{TyBinder} in \ghcfile{types/TyCoRep.lhs} distinguishes whether a binder is
\ctor{TyBinder} in \ghcfile{types/TyCoRep.hs} distinguishes whether a binder is
anonymous (\ctor{FunTy}) or named (\ctor{ForAllTy}). See
\verb|Note [TyBinders]| in \ghcfile{types/TyCoRep.lhs}.
\verb|Note [TyBinders]| in \ghcfile{types/TyCoRep.hs}.
There are some invariants on types:
\begin{itemize}
......@@ -284,8 +284,8 @@ type arity $[[I]]$, a list of roles $[[role_list]]$ for its coercion parameters,
and an output role $[[R']]$. The definition within GHC also includes a field named
$[[coaxrProves]]$ which computes the output coercion from a list of types and
a list of coercions. This is elided in this presentation, as we simply identify
axiom rules by their names $[[M]]$. See also \coderef{typecheck/TcTypeNats.lhs}{mkBinAxiom}
and \coderef{typecheck/TcTypeNats.lhs}{mkAxiom1}.
axiom rules by their names $[[M]]$. See also \coderef{typecheck/TcTypeNats.hs}{mkBinAxiom}
and \coderef{typecheck/TcTypeNats.hs}{mkAxiom1}.
In \ottdrulename{Co\_UnivCo}, function $ \textsf{compatibleUnBoxedTys} $ stands for following checks:
\begin{itemize}
......@@ -296,7 +296,7 @@ In \ottdrulename{Co\_UnivCo}, function $ \textsf{compatibleUnBoxedTys} $ stands
\item unboxed tuples should have same length and each element should be coercible to
appropriate element of the target tuple;
\end{itemize}
For function implementation see \coderef{coreSyn/CoreLint.lhs}{checkTypes}.
For function implementation see \coderef{coreSyn/CoreLint.hs}{checkTypes}.
For further discussion see \url{https://ghc.haskell.org/trac/ghc/wiki/BadUnsafeCoercions}.
\subsection{Type constructors}
......@@ -306,7 +306,7 @@ for this formalism:
\gram{\ottT}
We include some representative primitive type constructors. There are many more in \ghcfile{prelude/TysPrim.lhs}.
We include some representative primitive type constructors. There are many more in \ghcfile{prelude/TysPrim.hs}.
\gram{\ottH}
......@@ -327,7 +327,7 @@ synonym for $[[TYPE 'Unlifted]]$.
\section{Contexts}
The functions in \ghcfile{coreSyn/CoreLint.lhs} use the \texttt{LintM} monad.
The functions in \ghcfile{coreSyn/CoreLint.hs} use the \texttt{LintM} monad.
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
......@@ -347,13 +347,13 @@ 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
applying a substitution. We elide these details in this formalism, but
see \coderef{types/Type.lhs}{substTyVarBndr} for details.
see \coderef{types/Type.hs}{substTyVarBndr} for details.
\section{Typing judgments}
The following functions are used from GHC. Their names are descriptive, and they
are not formalized here: \coderef{types/TyCon.lhs}{tyConKind},
\coderef{types/TyCon.lhs}{tyConArity}, \coderef{basicTypes/DataCon.lhs}{dataConTyCon}, \coderef{types/TyCon.lhs}{isNewTyCon}, \coderef{basicTypes/DataCon.lhs}{dataConRepType}.
are not formalized here: \coderef{types/TyCon.hs}{tyConKind},
\coderef{types/TyCon.hs}{tyConArity}, \coderef{basicTypes/DataCon.hs}{dataConTyCon}, \coderef{types/TyCon.hs}{isNewTyCon}, \coderef{basicTypes/DataCon.hs}{dataConRepType}.
\subsection{Program consistency}
......@@ -363,7 +363,7 @@ and then check each binding.
\ottdefnlintCoreBindings{}
Here is the definition of $[[vars_of]]$, taken from \coderef{coreSyn/CoreSyn.lhs}{bindersOf}:
Here is the definition of $[[vars_of]]$, taken from \coderef{coreSyn/CoreSyn.hs}{bindersOf}:
\[
\begin{array}{ll}
......@@ -409,11 +409,11 @@ to check each substituted type $[[s'i]]$ in a context containing all the types
that come before it in the list of bindings. The $[[G'i]]$ are contexts
containing the names and kinds of all type variables (and term variables,
for that matter) up to the $i$th binding. This logic is extracted from
\coderef{coreSyn/CoreLint.lhs}{lintAndScopeIds}.
\coderef{coreSyn/CoreLint.hs}{lintAndScopeIds}.
\item The GHC source code checks all arguments in an application expression
all at once using \coderef{coreSyn/CoreSyn.lhs}{collectArgs}
and \coderef{coreSyn/CoreLint.lhs}{lintCoreArgs}. The operation
all at once using \coderef{coreSyn/CoreSyn.hs}{collectArgs}
and \coderef{coreSyn/CoreLint.hs}{lintCoreArgs}. The operation
has been unfolded for presentation here.
\item If a $[[tick]]$ contains breakpoints, the GHC source performs additional
......@@ -505,7 +505,7 @@ $[[tyConRoles]]$, but with an arbitrary number of $[[Nom]]$ at the end, to accou
for potential oversaturation.
The checks encoded in the following
judgments are run from \coderef{typecheck/TcTyClsDecls.lhs}{checkValidTyCon}
judgments are run from \coderef{typecheck/TcTyClsDecls.hs}{checkValidTyCon}
when \texttt{-dcore-lint} is set.
\ottdefncheckValidRoles{}
......@@ -539,12 +539,12 @@ The judgment $[[apart]]$ checks to see whether two lists of types are surely
apart. $[[apart( </ ti // i />, </ si // i /> )]]$, where $[[ </ ti // i />
]]$ is a list of types and $[[ </ si // i /> ]]$ is a list of type
\emph{patterns} (as in a type family equation), first flattens the $[[ </ ti
// i /> ]]$ using \coderef{types/FamInstEnv.lhs}{flattenTys} and then checks to
see if \coderef{types/Unify.lhs}{tcUnifyTysFG} returns \texttt{SurelyApart}.
// i /> ]]$ using \coderef{types/FamInstEnv.hs}{flattenTys} and then checks to
see if \coderef{types/Unify.hs}{tcUnifyTysFG} returns \texttt{SurelyApart}.
Flattening takes all type family applications and replaces them with fresh variables,
taking care to map identical type family applications to the same fresh variable.
The algorithm $[[unify]]$ is implemented in \coderef{types/Unify.lhs}{tcUnifyTys}.
The algorithm $[[unify]]$ is implemented in \coderef{types/Unify.hs}{tcUnifyTys}.
It performs a standard unification, returning a substitution upon success.
\section{Operational semantics}
......@@ -553,7 +553,7 @@ It performs a standard unification, returning a substitution upon success.
GHC does not implement an operational semantics in any concrete form. Most
of the rules below are implied by algorithms in, for example, the simplifier
and optimizer. Yet, there is no one place in GHC that states these rules,
analogously to \texttt{CoreLint.lhs}.
analogously to \texttt{CoreLint.hs}.
Nevertheless, these rules are included in this document to help the reader
understand System FC.
......@@ -581,17 +581,17 @@ to the constructor. The terms are the regular term arguments stored in an
algebraic datatype. Coercions (say, in a GADT) are considered term arguments.
\item The rule \ottdrulename{S\_CasePush} is the most complex rule.
\begin{itemize}
\item The logic in this rule is implemented in \coderef{coreSyn/CoreSubst.lhs}{exprIsConApp\_maybe}.
\item The $[[coercionKind]]$ function (\coderef{types/Coercion.lhs}{coercionKind})
\item The logic in this rule is implemented in \coderef{coreSyn/CoreSubst.hs}{exprIsConApp\_maybe}.
\item The $[[coercionKind]]$ function (\coderef{types/Coercion.hs}{coercionKind})
extracts the two types (and their kinds) from
a coercion. It does not require a typing context, as it does not \emph{check} the
coercion, just extracts its types.
\item The $[[dataConRepType]]$ function (\coderef{basicTypes/DataCon.lhs}{dataConRepType}) extracts the full type of a data constructor. Following the notation for
\item The $[[dataConRepType]]$ function (\coderef{basicTypes/DataCon.hs}{dataConRepType}) extracts the full type of a data constructor. Following the notation for
constructor expressions, the parameters to the constructor are broken into three
groups: universally quantified types, existentially quantified types, and terms.
\item The substitutions in the last premise to the rule are unusual: they replace
\emph{type} variables with \emph{coercions}. This substitution is called lifting
and is implemented in \coderef{types/Coercion.lhs}{liftCoSubst}. The notation is
and is implemented in \coderef{types/Coercion.hs}{liftCoSubst}. The notation is
essentially a pun on the fact that types and coercions have such similar structure.
This operation is quite non-trivial. Please see \emph{System FC with Explicit
Kind Equality} for details.
......
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