Repository : ssh://[email protected]/ghc On branch : type-nats-simple Link : http://ghc.haskell.org/trac/ghc/changeset/e0cd08c100f87fbe34e1f9ed015cf402dff3dd3f/ghc
>--------------------------------------------------------------- commit e0cd08c100f87fbe34e1f9ed015cf402dff3dd3f Author: Iavor S. Diatchki <[email protected]> Date: Sat Sep 7 17:10:47 2013 -0700 Add some simple interactions with inerts for (+), (*), and (^). >--------------------------------------------------------------- e0cd08c100f87fbe34e1f9ed015cf402dff3dd3f compiler/typecheck/TcTypeNats.hs | 39 ++++++++++++++++++++++++++++++++++---- 1 file changed, 35 insertions(+), 4 deletions(-) diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs index 87ed825..998bd81 100644 --- a/compiler/typecheck/TcTypeNats.hs +++ b/compiler/typecheck/TcTypeNats.hs @@ -20,7 +20,7 @@ import PrelNames ( gHC_TYPELITS , typeNatMulTyFamNameKey , typeNatExpTyFamNameKey ) -import FamInst ( TcBuiltInSynFamily(..), trivialBuiltInFamily ) +import FamInst ( TcBuiltInSynFamily(..) ) import FastString ( FastString, fsLit ) import qualified Data.Map as Map @@ -40,7 +40,7 @@ typeNatAddTyCon = mkTypeNatFunTyCon2 name TcBuiltInSynFamily { sfMatchFam = matchFamAdd , sfInteractTop = interactTopAdd - , sfInteractInert = sfInteractInert trivialBuiltInFamily + , sfInteractInert = interactInertAdd } where name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "+") @@ -51,7 +51,7 @@ typeNatMulTyCon = mkTypeNatFunTyCon2 name TcBuiltInSynFamily { sfMatchFam = matchFamMul , sfInteractTop = interactTopMul - , sfInteractInert = sfInteractInert trivialBuiltInFamily + , sfInteractInert = interactInertMul } where name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "*") @@ -62,7 +62,7 @@ typeNatExpTyCon = mkTypeNatFunTyCon2 name TcBuiltInSynFamily { sfMatchFam = matchFamExp , sfInteractTop = interactTopExp - , sfInteractInert = sfInteractInert trivialBuiltInFamily + , sfInteractInert = interactInertExp } where name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "^") @@ -150,6 +150,13 @@ x === y = Pair x y num :: Integer -> Type num = mkNumLitTy +known :: (Integer -> Bool) -> TcType -> Bool +known p x = case isNumLitTy x of + Just a -> p a + Nothing -> False + + + -- For the definitional axioms mkBinAxiom :: String -> TyCon -> @@ -257,8 +264,32 @@ interactTopExp [s,t] r mbZ = isNumLitTy r interactTopExp _ _ = [] +{------------------------------------------------------------------------------- +Interacton with inerts +-------------------------------------------------------------------------------} + +interactInertAdd :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type] +interactInertAdd [x1,y1] z1 [x2,y2] z2 + | sameZ && eqType x1 x2 = [ y1 === y2 ] + | sameZ && eqType y1 y2 = [ x1 === x2 ] + where sameZ = eqType z1 z2 +interactInertAdd _ _ _ _ = [] + +interactInertMul :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type] +interactInertMul [x1,y1] z1 [x2,y2] z2 + | sameZ && known (/= 0) x1 && eqType x1 x2 = [ y1 === y2 ] + | sameZ && known (/= 0) y1 && eqType y1 y2 = [ x1 === x2 ] + where sameZ = eqType z1 z2 + +interactInertMul _ _ _ _ = [] +interactInertExp :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type] +interactInertExp [x1,y1] z1 [x2,y2] z2 + | sameZ && known (> 1) x1 && eqType x1 x2 = [ y1 === y2 ] + | sameZ && known (> 0) y1 && eqType y1 y2 = [ x1 === x2 ] + where sameZ = eqType z1 z2 +interactInertExp _ _ _ _ = [] {- ----------------------------------------------------------------------------- _______________________________________________ ghc-commits mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-commits
