Commit 5cf36697 authored by Iavor S. Diatchki's avatar Iavor S. Diatchki
Browse files

Add a type-function for subtraction.

This is used in the definition of `ToNat1` in the `base` library
(module GHC.TypeLits).
parent e2da02d4
......@@ -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
......
......@@ -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)
axMulDef = mkBinAxiom "MulDef" typeNatMulTyCon $
\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 ]
......
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