Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : type-nats
http://hackage.haskell.org/trac/ghc/changeset/f77108e71ea0087caa9f3eb43796b9d1a77d4dc3 >--------------------------------------------------------------- commit f77108e71ea0087caa9f3eb43796b9d1a77d4dc3 Author: Iavor S. Diatchki <[email protected]> Date: Mon Jul 9 12:23:45 2012 -0700 Some simple support for <=. >--------------------------------------------------------------- compiler/prelude/TysWiredIn.lhs | 28 +++++++++++++++++++++-- compiler/typecheck/TcTypeNats.hs | 39 ++++++++++++++++++++------------ compiler/typecheck/TcTypeNatsRules.hs | 15 ++++++++++++ 3 files changed, 64 insertions(+), 18 deletions(-) diff --git a/compiler/prelude/TysWiredIn.lhs b/compiler/prelude/TysWiredIn.lhs index 515e311..193d8cf 100644 --- a/compiler/prelude/TysWiredIn.lhs +++ b/compiler/prelude/TysWiredIn.lhs @@ -73,7 +73,12 @@ module TysWiredIn ( eqTyCon_RDR, eqTyCon, eqTyConName, eqBoxDataCon, -- * Type families used to compute at the type level. - typeNatLeqTyCon, typeNatAddTyCon, typeNatMulTyCon, typeNatExpTyCon + typeNatLeqTyCon, typeNatAddTyCon, typeNatMulTyCon, typeNatExpTyCon, + + -- * Lifted booleans + boolKindCon, boolKind, + trueTyCon, trueTy, + falseTyCon, falseTy ) where @@ -767,10 +772,9 @@ Type functions related to type-nats. \begin{code} --- XXX: THIS IS WRONG. IT SHOULD RETURN A PROMOTED BOOL. typeNatLeqTyCon :: TyCon typeNatLeqTyCon = mkSynTyCon typeNatLeqTyFamName - (mkArrowKinds [ typeNatKind, typeNatKind ] typeNatKind) + (mkArrowKinds [ typeNatKind, typeNatKind ] boolKind) (take 2 $ tyVarList typeNatKind) SynFamilyTyCon NoParentTyCon @@ -793,6 +797,24 @@ typeNatExpTyCon = mkTypeNatFunTyCon typeNatExpTyFamName \end{code} +Promoted Booleans + +\begin{code} + +boolKindCon, trueTyCon, falseTyCon :: TyCon +boolKindCon = buildPromotedTyCon boolTyCon +trueTyCon = buildPromotedDataCon trueDataCon +falseTyCon = buildPromotedDataCon falseDataCon + + +boolKind :: Kind +boolKind = mkTyConApp boolKindCon [] + +trueTy, falseTy :: Type +trueTy = mkTyConApp trueTyCon [] +falseTy = mkTyConApp falseTyCon [] + +\end{code} diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs index 7d8f3b7..73f61b6 100644 --- a/compiler/typecheck/TcTypeNats.hs +++ b/compiler/typecheck/TcTypeNats.hs @@ -3,6 +3,7 @@ module TcTypeNats where import PrelNames( typeNatAddTyFamName , typeNatMulTyFamName , typeNatExpTyFamName + , typeNatLeqTyFamName ) import Outputable ( ppr, pprWithCommas @@ -22,12 +23,15 @@ import Type ( Type, isNumLitTy, getTyVar_maybe, mkNumLitTy import TysWiredIn ( typeNatAddTyCon , typeNatMulTyCon , typeNatExpTyCon + , trueTy, falseTy ) import Bag ( bagToList ) import DynFlags ( DynFlags ) -- From type checker -import TcTypeNatsRules( bRules, theRules, axAddDef, axMulDef, axExpDef, natVars) +import TcTypeNatsRules( bRules, theRules + , axAddDef, axMulDef, axExpDef, axLeqDef + , natVars) import TcTypeNatsEval ( minus, divide, logExact, rootExact ) import TcCanonical( StopOrContinue(..) ) import TcRnTypes ( Ct(..), isGiven, isWanted, ctEvidence, ctEvId @@ -266,13 +270,17 @@ byAxiom (TPOther ty, TPVar r) | Just (tc,[tp1,tp2]) <- splitTyConApp_maybe ty , Just a <- isNumLitTy tp1, Just b <- isNumLitTy tp2 - = do (ax,op) <- case tyConName tc of - name | name == typeNatAddTyFamName -> Just (axAddDef, (+)) - | name == typeNatMulTyFamName -> Just (axMulDef, (*)) - | name == typeNatExpTyFamName -> Just (axExpDef, (^)) - _ -> Nothing + = do (ax,val) <- + let num op = mkNumLitTy (op a b) + bool op = if op a b then trueTy else falseTy + in case tyConName tc of + name | name == typeNatAddTyFamName -> Just (axAddDef, num (+)) + | name == typeNatMulTyFamName -> Just (axMulDef, num (*)) + | name == typeNatExpTyFamName -> Just (axExpDef, num (^)) + | name == typeNatLeqTyFamName -> Just (axLeqDef, bool (<=)) + _ -> Nothing - return ( [ (r, mkNumLitTy (op a b)) ], useAxiom (ax a b) [] [] ) + return ( [ (r, val) ], useAxiom (ax a b) [] [] ) byAxiom (TPCon tc [TPVar r,TPOther tp1], TPOther tp2) @@ -303,14 +311,15 @@ byAxiom (TPOther ty, TPOther tp3) | Just (tc,[tp1,tp2]) <- splitTyConApp_maybe ty , Just a <- isNumLitTy tp1 , Just b <- isNumLitTy tp2 - , Just c <- isNumLitTy tp3 - = do (ax,op) <- case tyConName tc of - n | n == typeNatAddTyFamName -> Just (axAddDef, (+)) - | n == typeNatMulTyFamName -> Just (axMulDef, (*)) - | n == typeNatExpTyFamName -> Just (axExpDef, (^)) - _ -> Nothing - guard (op a b == c) - return ([], useAxiom (ax a b) [] []) + = do ax <- case tyConName tc of + n | n == typeNatAddTyFamName -> Just axAddDef + | n == typeNatMulTyFamName -> Just axMulDef + | n == typeNatExpTyFamName -> Just axExpDef + | n == typeNatLeqTyFamName -> Just axLeqDef + _ -> Nothing + let r = ax a b + guard (eqType (co_axr_rhs r) tp3) + return ([], useAxiom r [] []) byAxiom _ = Nothing diff --git a/compiler/typecheck/TcTypeNatsRules.hs b/compiler/typecheck/TcTypeNatsRules.hs index 935a152..d9b44d0 100644 --- a/compiler/typecheck/TcTypeNatsRules.hs +++ b/compiler/typecheck/TcTypeNatsRules.hs @@ -11,6 +11,8 @@ import TysPrim ( tyVarList import TysWiredIn ( typeNatAddTyCon , typeNatMulTyCon , typeNatExpTyCon + , typeNatLeqTyCon + , trueTy, falseTy ) import Name ( mkSystemName ) @@ -38,6 +40,9 @@ mkMul a b = mkTyConApp typeNatMulTyCon [a,b] mkExp :: Type -> Type -> Type mkExp a b = mkTyConApp typeNatExpTyCon [a,b] +mkLeq :: Type -> Type -> Type +mkLeq a b = mkTyConApp typeNatLeqTyCon [a,b] + natVars :: [TyVar] natVars = tyVarList typeNatKind @@ -59,6 +64,13 @@ axExpDef :: Integer -> Integer -> CoAxiomRule axExpDef a b = mkAx (axName "ExpDef" a b) [] [] (mkExp (mkNumLitTy a) (mkNumLitTy b)) (mkNumLitTy (a ^ b)) +axLeqDef :: Integer -> Integer -> CoAxiomRule +axLeqDef a b + | a <= b = mkAx (axName "LeqDef" a b) [] [] prop trueTy + | otherwise = mkAx (axName "NotLeqDef" a b) [] [] prop falseTy + where prop = mkLeq (mkNumLitTy a) (mkNumLitTy b) + + -- XXX: We should be able to cope with some assumptions in backward -- reasoning too. @@ -76,6 +88,9 @@ bRules = , bRule "TnExp0R" (mkExp a n0) n1 , bRule "TnExp1L" (mkExp n1 a) n1 , bRule "TnExp1R" (mkExp a n1) a + + , bRule "Leq0" (mkLeq n0 a) trueTy + , bRule "LeqRefl" (mkLeq a a) trueTy ] where bRule y = mkAx y (take 1 natVars) [] _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
