[commit: ghc] master: Add a type-function for subtraction. (5cf3669)
git at git.haskell.org
git at git.haskell.org
Tue Sep 24 15:24:28 CEST 2013
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/5cf366975f6917c98e82506c674ca6bb4f11336f/ghc
>---------------------------------------------------------------
commit 5cf366975f6917c98e82506c674ca6bb4f11336f
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date: Tue Sep 24 06:14:15 2013 -0700
Add a type-function for subtraction.
This is used in the definition of `ToNat1` in the `base` library
(module GHC.TypeLits).
>---------------------------------------------------------------
5cf366975f6917c98e82506c674ca6bb4f11336f
compiler/prelude/PrelNames.lhs | 3 +-
compiler/typecheck/TcTypeNats.hs | 62 ++++++++++++++++++++++++++++++++++----
2 files changed, 58 insertions(+), 7 deletions(-)
diff --git a/compiler/prelude/PrelNames.lhs b/compiler/prelude/PrelNames.lhs
index 07730e6..453f554 100644
--- a/compiler/prelude/PrelNames.lhs
+++ b/compiler/prelude/PrelNames.lhs
@@ -1465,7 +1465,7 @@ rep1TyConKey = mkPreludeTyConUnique 156
-- Type-level naturals
typeNatKindConNameKey, typeSymbolKindConNameKey,
typeNatAddTyFamNameKey, typeNatMulTyFamNameKey, typeNatExpTyFamNameKey,
- typeNatLeqTyFamNameKey
+ typeNatLeqTyFamNameKey, typeNatSubTyFamNameKey
:: Unique
typeNatKindConNameKey = mkPreludeTyConUnique 160
typeSymbolKindConNameKey = mkPreludeTyConUnique 161
@@ -1473,6 +1473,7 @@ typeNatAddTyFamNameKey = mkPreludeTyConUnique 162
typeNatMulTyFamNameKey = mkPreludeTyConUnique 163
typeNatExpTyFamNameKey = mkPreludeTyConUnique 164
typeNatLeqTyFamNameKey = mkPreludeTyConUnique 165
+typeNatSubTyFamNameKey = mkPreludeTyConUnique 166
ntTyConKey:: Unique
ntTyConKey = mkPreludeTyConUnique 174
diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index 2ff083c..7961df4 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -23,6 +23,7 @@ import PrelNames ( gHC_TYPELITS
, typeNatMulTyFamNameKey
, typeNatExpTyFamNameKey
, typeNatLeqTyFamNameKey
+ , typeNatSubTyFamNameKey
)
import FamInst ( TcBuiltInSynFamily(..) )
import FastString ( FastString, fsLit )
@@ -39,6 +40,7 @@ typeNatTyCons =
, typeNatMulTyCon
, typeNatExpTyCon
, typeNatLeqTyCon
+ , typeNatSubTyCon
]
typeNatAddTyCon :: TyCon
@@ -52,6 +54,17 @@ typeNatAddTyCon = mkTypeNatFunTyCon2 name
name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "+")
typeNatAddTyFamNameKey typeNatAddTyCon
+typeNatSubTyCon :: TyCon
+typeNatSubTyCon = mkTypeNatFunTyCon2 name
+ TcBuiltInSynFamily
+ { sfMatchFam = matchFamSub
+ , sfInteractTop = interactTopSub
+ , sfInteractInert = interactInertSub
+ }
+ where
+ name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "-")
+ typeNatSubTyFamNameKey typeNatSubTyCon
+
typeNatMulTyCon :: TyCon
typeNatMulTyCon = mkTypeNatFunTyCon2 name
TcBuiltInSynFamily
@@ -127,22 +140,28 @@ axAddDef
, axExp1R
, axLeqRefl
, axLeq0L
+ , axSubDef
+ , axSub0R
:: CoAxiomRule
axAddDef = mkBinAxiom "AddDef" typeNatAddTyCon $
- \x y -> num (x + y)
+ \x y -> Just $ num (x + y)
axMulDef = mkBinAxiom "MulDef" typeNatMulTyCon $
- \x y -> num (x * y)
+ \x y -> Just $ num (x * y)
axExpDef = mkBinAxiom "ExpDef" typeNatExpTyCon $
- \x y -> num (x ^ y)
+ \x y -> Just $ num (x ^ y)
axLeqDef = mkBinAxiom "LeqDef" typeNatLeqTyCon $
- \x y -> bool (x <= y)
+ \x y -> Just $ bool (x <= y)
+
+axSubDef = mkBinAxiom "SubDef" typeNatSubTyCon $
+ \x y -> fmap num (minus x y)
axAdd0L = mkAxiom1 "Add0L" $ \t -> (num 0 .+. t) === t
axAdd0R = mkAxiom1 "Add0R" $ \t -> (t .+. num 0) === t
+axSub0R = mkAxiom1 "Sub0R" $ \t -> (t .-. num 0) === t
axMul0L = mkAxiom1 "Mul0L" $ \t -> (num 0 .*. t) === num 0
axMul0R = mkAxiom1 "Mul0R" $ \t -> (t .*. num 0) === num 0
axMul1L = mkAxiom1 "Mul1L" $ \t -> (num 1 .*. t) === t
@@ -170,6 +189,7 @@ typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
, axExp1R
, axLeqRefl
, axLeq0L
+ , axSubDef
]
@@ -181,6 +201,9 @@ Various utilities for making axioms and types
(.+.) :: Type -> Type -> Type
s .+. t = mkTyConApp typeNatAddTyCon [s,t]
+(.-.) :: Type -> Type -> Type
+s .-. t = mkTyConApp typeNatSubTyCon [s,t]
+
(.*.) :: Type -> Type -> Type
s .*. t = mkTyConApp typeNatMulTyCon [s,t]
@@ -221,7 +244,7 @@ known p x = case isNumLitTy x of
-- For the definitional axioms
mkBinAxiom :: String -> TyCon ->
- (Integer -> Integer -> Type) -> CoAxiomRule
+ (Integer -> Integer -> Maybe Type) -> CoAxiomRule
mkBinAxiom str tc f =
CoAxiomRule
{ coaxrName = fsLit str
@@ -232,7 +255,8 @@ mkBinAxiom str tc f =
case (ts,cs) of
([s,t],[]) -> do x <- isNumLitTy s
y <- isNumLitTy t
- return (mkTyConApp tc [s,t] === f x y)
+ z <- f x y
+ return (mkTyConApp tc [s,t] === z)
_ -> Nothing
}
@@ -264,6 +288,15 @@ matchFamAdd [s,t]
mbY = isNumLitTy t
matchFamAdd _ = Nothing
+matchFamSub :: [Type] -> Maybe (TcCoercion, TcType)
+matchFamSub [s,t]
+ | Just 0 <- mbY = Just (mkTcAxiomRuleCo axSub0R [s] [], s)
+ | Just x <- mbX, Just y <- mbY, Just z <- minus x y =
+ Just (mkTcAxiomRuleCo axSubDef [s,t] [], num z)
+ where mbX = isNumLitTy s
+ mbY = isNumLitTy t
+matchFamSub _ = Nothing
+
matchFamMul :: [Xi] -> Maybe (TcCoercion, Xi)
matchFamMul [s,t]
| Just 0 <- mbX = Just (mkTcAxiomRuleCo axMul0L [t] [], num 0)
@@ -312,6 +345,16 @@ interactTopAdd [s,t] r
mbZ = isNumLitTy r
interactTopAdd _ _ = []
+interactTopSub :: [Xi] -> Xi -> [Pair Type]
+interactTopSub [s,t] r
+ | Just 0 <- mbZ = [ s === t ]
+ | otherwise = [ t .+. r === s ]
+ where
+ mbZ = isNumLitTy r
+interactTopSub _ _ = []
+
+
+
interactTopMul :: [Xi] -> Xi -> [Pair Type]
interactTopMul [s,t] r
| Just 1 <- mbZ = [ s === num 1, t === num 1 ]
@@ -355,6 +398,13 @@ interactInertAdd [x1,y1] z1 [x2,y2] z2
where sameZ = eqType z1 z2
interactInertAdd _ _ _ _ = []
+{- XXX: Should we add some rules here?
+When `interactTopSub` sees `x - y ~ z`, it generates `z + y ~ x`.
+Hopefully, this should interact further and generate all additional
+needed facts that we might need. -}
+interactInertSub :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
+interactInertSub _ _ _ _ = []
+
interactInertMul :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
interactInertMul [x1,y1] z1 [x2,y2] z2
| sameZ && known (/= 0) x1 && eqType x1 x2 = [ y1 === y2 ]
More information about the ghc-commits
mailing list