Changeset View
Changeset View
Standalone View
Standalone View
compiler/typecheck/TcTypeNats.hs
| Show All 23 Lines | 23 | import TysWiredIn ( typeNatKind, typeSymbolKind | |||
|---|---|---|---|---|---|
| 24 | , mkWiredInTyConName | 24 | , mkWiredInTyConName | ||
| 25 | , promotedBoolTyCon | 25 | , promotedBoolTyCon | ||
| 26 | , promotedFalseDataCon, promotedTrueDataCon | 26 | , promotedFalseDataCon, promotedTrueDataCon | ||
| 27 | , promotedOrderingTyCon | 27 | , promotedOrderingTyCon | ||
| 28 | , promotedLTDataCon | 28 | , promotedLTDataCon | ||
| 29 | , promotedEQDataCon | 29 | , promotedEQDataCon | ||
| 30 | , promotedGTDataCon | 30 | , promotedGTDataCon | ||
| 31 | ) | 31 | ) | ||
| 32 | import TysPrim ( tyVarList, mkArrowKinds ) | 32 | import TysPrim ( mkArrowKinds, mkTemplateTyVars ) | ||
| 33 | import PrelNames ( gHC_TYPELITS | 33 | import PrelNames ( gHC_TYPELITS | ||
| 34 | , typeNatAddTyFamNameKey | 34 | , typeNatAddTyFamNameKey | ||
| 35 | , typeNatMulTyFamNameKey | 35 | , typeNatMulTyFamNameKey | ||
| 36 | , typeNatExpTyFamNameKey | 36 | , typeNatExpTyFamNameKey | ||
| 37 | , typeNatLeqTyFamNameKey | 37 | , typeNatLeqTyFamNameKey | ||
| 38 | , typeNatSubTyFamNameKey | 38 | , typeNatSubTyFamNameKey | ||
| 39 | , typeNatCmpTyFamNameKey | 39 | , typeNatCmpTyFamNameKey | ||
| 40 | , typeSymbolCmpTyFamNameKey | 40 | , typeSymbolCmpTyFamNameKey | ||
| ▲ Show 20 Lines • Show All 60 Lines • ▼ Show 20 Line(s) | 95 | typeNatExpTyCon = mkTypeNatFunTyCon2 name | |||
| 101 | where | 101 | where | ||
| 102 | name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "^") | 102 | name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "^") | ||
| 103 | typeNatExpTyFamNameKey typeNatExpTyCon | 103 | typeNatExpTyFamNameKey typeNatExpTyCon | ||
| 104 | 104 | | |||
| 105 | typeNatLeqTyCon :: TyCon | 105 | typeNatLeqTyCon :: TyCon | ||
| 106 | typeNatLeqTyCon = | 106 | typeNatLeqTyCon = | ||
| 107 | mkFamilyTyCon name | 107 | mkFamilyTyCon name | ||
| 108 | (mkArrowKinds [ typeNatKind, typeNatKind ] boolKind) | 108 | (mkArrowKinds [ typeNatKind, typeNatKind ] boolKind) | ||
| 109 | (take 2 $ tyVarList typeNatKind) | 109 | (mkTemplateTyVars [ typeNatKind, typeNatKind ]) | ||
| 110 | (BuiltInSynFamTyCon ops) | 110 | (BuiltInSynFamTyCon ops) | ||
| 111 | NoParentTyCon | 111 | NoParentTyCon | ||
| 112 | 112 | | |||
| 113 | where | 113 | where | ||
| 114 | name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "<=?") | 114 | name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "<=?") | ||
| 115 | typeNatLeqTyFamNameKey typeNatLeqTyCon | 115 | typeNatLeqTyFamNameKey typeNatLeqTyCon | ||
| 116 | ops = BuiltInSynFamily | 116 | ops = BuiltInSynFamily | ||
| 117 | { sfMatchFam = matchFamLeq | 117 | { sfMatchFam = matchFamLeq | ||
| 118 | , sfInteractTop = interactTopLeq | 118 | , sfInteractTop = interactTopLeq | ||
| 119 | , sfInteractInert = interactInertLeq | 119 | , sfInteractInert = interactInertLeq | ||
| 120 | } | 120 | } | ||
| 121 | 121 | | |||
| 122 | typeNatCmpTyCon :: TyCon | 122 | typeNatCmpTyCon :: TyCon | ||
| 123 | typeNatCmpTyCon = | 123 | typeNatCmpTyCon = | ||
| 124 | mkFamilyTyCon name | 124 | mkFamilyTyCon name | ||
| 125 | (mkArrowKinds [ typeNatKind, typeNatKind ] orderingKind) | 125 | (mkArrowKinds [ typeNatKind, typeNatKind ] orderingKind) | ||
| 126 | (take 2 $ tyVarList typeNatKind) | 126 | (mkTemplateTyVars [ typeNatKind, typeNatKind ]) | ||
| 127 | (BuiltInSynFamTyCon ops) | 127 | (BuiltInSynFamTyCon ops) | ||
| 128 | NoParentTyCon | 128 | NoParentTyCon | ||
| 129 | 129 | | |||
| 130 | where | 130 | where | ||
| 131 | name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "CmpNat") | 131 | name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "CmpNat") | ||
| 132 | typeNatCmpTyFamNameKey typeNatCmpTyCon | 132 | typeNatCmpTyFamNameKey typeNatCmpTyCon | ||
| 133 | ops = BuiltInSynFamily | 133 | ops = BuiltInSynFamily | ||
| 134 | { sfMatchFam = matchFamCmpNat | 134 | { sfMatchFam = matchFamCmpNat | ||
| 135 | , sfInteractTop = interactTopCmpNat | 135 | , sfInteractTop = interactTopCmpNat | ||
| 136 | , sfInteractInert = \_ _ _ _ -> [] | 136 | , sfInteractInert = \_ _ _ _ -> [] | ||
| 137 | } | 137 | } | ||
| 138 | 138 | | |||
| 139 | typeSymbolCmpTyCon :: TyCon | 139 | typeSymbolCmpTyCon :: TyCon | ||
| 140 | typeSymbolCmpTyCon = | 140 | typeSymbolCmpTyCon = | ||
| 141 | mkFamilyTyCon name | 141 | mkFamilyTyCon name | ||
| 142 | (mkArrowKinds [ typeSymbolKind, typeSymbolKind ] orderingKind) | 142 | (mkArrowKinds [ typeSymbolKind, typeSymbolKind ] orderingKind) | ||
| 143 | (take 2 $ tyVarList typeSymbolKind) | 143 | (mkTemplateTyVars [ typeSymbolKind, typeSymbolKind ]) | ||
| 144 | (BuiltInSynFamTyCon ops) | 144 | (BuiltInSynFamTyCon ops) | ||
| 145 | NoParentTyCon | 145 | NoParentTyCon | ||
| 146 | 146 | | |||
| 147 | where | 147 | where | ||
| 148 | name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "CmpSymbol") | 148 | name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "CmpSymbol") | ||
| 149 | typeSymbolCmpTyFamNameKey typeSymbolCmpTyCon | 149 | typeSymbolCmpTyFamNameKey typeSymbolCmpTyCon | ||
| 150 | ops = BuiltInSynFamily | 150 | ops = BuiltInSynFamily | ||
| 151 | { sfMatchFam = matchFamCmpSymbol | 151 | { sfMatchFam = matchFamCmpSymbol | ||
| 152 | , sfInteractTop = interactTopCmpSymbol | 152 | , sfInteractTop = interactTopCmpSymbol | ||
| 153 | , sfInteractInert = \_ _ _ _ -> [] | 153 | , sfInteractInert = \_ _ _ _ -> [] | ||
| 154 | } | 154 | } | ||
| 155 | 155 | | |||
| 156 | 156 | | |||
| 157 | 157 | | |||
| 158 | 158 | | |||
| 159 | 159 | | |||
| 160 | -- Make a binary built-in constructor of kind: Nat -> Nat -> Nat | 160 | -- Make a binary built-in constructor of kind: Nat -> Nat -> Nat | ||
| 161 | mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon | 161 | mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon | ||
| 162 | mkTypeNatFunTyCon2 op tcb = | 162 | mkTypeNatFunTyCon2 op tcb = | ||
| 163 | mkFamilyTyCon op | 163 | mkFamilyTyCon op | ||
| 164 | (mkArrowKinds [ typeNatKind, typeNatKind ] typeNatKind) | 164 | (mkArrowKinds [ typeNatKind, typeNatKind ] typeNatKind) | ||
| 165 | (take 2 $ tyVarList typeNatKind) | 165 | (mkTemplateTyVars [ typeNatKind, typeNatKind ]) | ||
| 166 | (BuiltInSynFamTyCon tcb) | 166 | (BuiltInSynFamTyCon tcb) | ||
| 167 | NoParentTyCon | 167 | NoParentTyCon | ||
| 168 | 168 | | |||
| 169 | 169 | | |||
| 170 | 170 | | |||
| 171 | 171 | | |||
| 172 | {------------------------------------------------------------------------------- | 172 | {------------------------------------------------------------------------------- | ||
| 173 | Built-in rules axioms | 173 | Built-in rules axioms | ||
| ▲ Show 20 Lines • Show All 518 Lines • Show Last 20 Lines | |||||