diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,26 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.6 *April 23rd 2018* +* Solving constraints with `a-b` will emit `b <= a` constraints. e.g. solving + `n-1+1 ~ n` will emit a `1 <= n` constraint. + * If you need subtraction to be treated as addition with a negated operarand + run with `-fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers`, and + the `b <= a` constraint won't be emitted. Note that doing so can lead to + unsound behaviour. +* Try to solve equalities using smallest solution of inequalities: + * Solve `x + 1 ~ y` using `1 <= y` => `x + 1 ~ 1` => `x ~ 0` +* Solve inequalities using simple transitivity rules: + * `2 <= x` implies `1 <= x` + * `x <= 9` implies `x <= 10` +* Solve inequalities using _simple_ monotonicity of addition rules: + * `2 <= x` implies `2 + 2*x <= 3*x` +* Solve inequalities using _simple_ monotonicity of multiplication rules: + * `1 <= x` implies `1 <= 3*x` +* Solve inequalities using _simple_ monotonicity of exponentiation rules: + * `1 <= x` implies `2 <= 2^x` +* Solve inequalities using powers of 2 and monotonicity of exponentiation: + * `2 <= x` implies `2^(2 + 2*x) <= 2^(3*x)` + ## 0.5.10 *April 15th 2018* * Add support for GHC 8.5.20180306 diff --git a/ghc-typelits-natnormalise.cabal b/ghc-typelits-natnormalise.cabal --- a/ghc-typelits-natnormalise.cabal +++ b/ghc-typelits-natnormalise.cabal @@ -1,5 +1,5 @@ name: ghc-typelits-natnormalise -version: 0.5.10 +version: 0.6 synopsis: GHC typechecker plugin for types of kind GHC.TypeLits.Nat description: A type checker plugin for GHC that can solve /equalities/ of types of kind @@ -68,7 +68,8 @@ build-depends: base >=4.9 && <5, ghc >=8.0.1 && <8.6, ghc-tcplugins-extra >=0.2.5, - integer-gmp >=1.0 && <1.1 + integer-gmp >=1.0 && <1.1, + transformers >=0.5.2.0 && < 0.6 hs-source-dirs: src default-language: Haskell2010 other-extensions: CPP diff --git a/src/GHC/TypeLits/Normalise.hs b/src/GHC/TypeLits/Normalise.hs --- a/src/GHC/TypeLits/Normalise.hs +++ b/src/GHC/TypeLits/Normalise.hs @@ -37,6 +37,110 @@ @ To the header of your file. + +== Treating subtraction as addition with a negated number + +If you are absolutely sure that your subtractions can /never/ lead to (a locally) +negative number, you can ask the plugin to treat subtraction as addition with +a negated operand by additionally adding: + +@ +{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\} +@ + +to the header of your file, thereby allowing to use associativity and +commutativity rules when proving constraints involving subtractions. Note that +this option can lead to unsound behaviour and should be handled with extreme +care. + +=== When it leads to unsound behaviour + +For example, enabling the /allow-negated-numbers/ feature would allow +you to prove: + +@ +(n - 1) + 1 ~ n +@ + +/without/ a @(1 <= n)@ constraint, even though when /n/ is set to /0/ the +subtraction @n-1@ would be locally negative and hence not be a natural number. + +This would allow the following erroneous definition: + +@ +data Fin (n :: Nat) where + FZ :: Fin (n + 1) + FS :: Fin n -> Fin (n + 1) + +f :: forall n . Natural -> Fin n +f n = case of + 0 -> FZ + x -> FS (f \@(n-1) (x - 1)) + +fs :: [Fin 0] +fs = f \<$\> [0..] +@ + +=== When it might be Okay + +This example is taken from the +library. + +When you have: + +@ +-- | Singleton type for the number of repetitions of an element. +data Times (n :: Nat) where + T :: Times n + +-- | An element of a "run-length encoded" vector, containing the value and +-- the number of repetitions +data Elem :: Type -> Nat -> Type where + (:*) :: t -> Times n -> Elem t n + +-- | A length-indexed vector, optimised for repetitions. +data OptVector :: Type -> Nat -> Type where + End :: OptVector t 0 + (:-) :: Elem t l -> OptVector t (n - l) -> OptVector t n +@ + +And you want to define: + +@ +-- | Append two optimised vectors. +type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where + ys ++ End = ys + End ++ ys = ys + (x :- xs) ++ ys = x :- (xs ++ ys) +@ + +then the last line will give rise to the constraint: + +@ +(n-l)+m ~ (n+m)-l +@ + +because: + +@ +x :: Elem t l +xs :: OptVector t (n-l) +ys :: OptVector t m +@ + +In this case it's okay to add + +@ +{\-\# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers \#-\} +@ + +if you can convince yourself you will never be able to construct a: + +@ +xs :: OptVector t (n-l) +@ + +where /n-l/ is a negative number. -} {-# LANGUAGE CPP #-} @@ -53,6 +157,7 @@ -- external import Control.Arrow (second) import Control.Monad (replicateM) +import Control.Monad.Trans.Writer.Strict import Data.Either (rights) import Data.List (intersect) import Data.Maybe (mapMaybe) @@ -93,7 +198,6 @@ typeNatSubTyCon) import TcTypeNats (typeNatLeqTyCon) -import Type (mkNumLitTy,mkTyConApp) import TysWiredIn (promotedFalseDataCon, promotedTrueDataCon) -- internal @@ -107,19 +211,26 @@ -- -- To the header of your file. plugin :: Plugin -plugin = defaultPlugin { tcPlugin = const $ Just normalisePlugin } +plugin = defaultPlugin { tcPlugin = go } + where + go ["allow-negated-numbers"] = Just (normalisePlugin True) + go _ = Just (normalisePlugin False) -normalisePlugin :: TcPlugin -normalisePlugin = tracePlugin "ghc-typelits-natnormalise" +normalisePlugin :: Bool -> TcPlugin +normalisePlugin negNumbers = tracePlugin "ghc-typelits-natnormalise" TcPlugin { tcPluginInit = return () - , tcPluginSolve = const decideEqualSOP + , tcPluginSolve = const (decideEqualSOP negNumbers) , tcPluginStop = const (return ()) } -decideEqualSOP :: [Ct] -> [Ct] -> [Ct] - -> TcPluginM TcPluginResult -decideEqualSOP _givens _deriveds [] = return (TcPluginOk [] []) -decideEqualSOP givens _deriveds wanteds = do +decideEqualSOP + :: Bool + -> [Ct] + -> [Ct] + -> [Ct] + -> TcPluginM TcPluginResult +decideEqualSOP _negNumbers _givens _deriveds [] = return (TcPluginOk [] []) +decideEqualSOP negNumbers givens _deriveds wanteds = do -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out let wanteds' = filter (isWanted . ctEvidence) wanteds let unit_wanteds = mapMaybe toNatEquality wanteds' @@ -131,7 +242,7 @@ #else unit_givens <- mapMaybe toNatEquality <$> mapM zonkCt givens #endif - sr <- simplifyNats unit_givens unit_wanteds + sr <- simplifyNats negNumbers unit_givens unit_wanteds tcPluginTrace "normalised" (ppr sr) case sr of Simplified evs -> do @@ -141,7 +252,7 @@ Impossible eq -> return (TcPluginContradiction [fromNatEquality eq]) type NatEquality = (Ct,CoreSOP,CoreSOP) -type NatInEquality = (Ct,CoreSOP) +type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool)) fromNatEquality :: Either NatEquality NatInEquality -> Ct fromNatEquality (Left (ct, _, _)) = ct @@ -155,58 +266,90 @@ ppr (Simplified evs) = text "Simplified" $$ ppr evs ppr (Impossible eq) = text "Impossible" <+> ppr eq +mergeSimplifyResult + :: SimplifyResult + -> SimplifyResult + -> SimplifyResult +mergeSimplifyResult a@(Impossible _) _ = a +mergeSimplifyResult _ b@(Impossible _) = b +mergeSimplifyResult (Simplified a) (Simplified b) = Simplified (a ++ b) + simplifyNats - :: [Either NatEquality NatInEquality] + :: Bool + -- ^ Allow negated numbers (potentially unsound!) + -> [(Either NatEquality NatInEquality,[(Type,Type)])] -- ^ Given constraints - -> [Either NatEquality NatInEquality] + -> [(Either NatEquality NatInEquality,[(Type,Type)])] -- ^ Wanted constraints -> TcPluginM SimplifyResult -simplifyNats eqsG eqsW = - let eqs = eqsG ++ eqsW +simplifyNats negNumbers eqsG eqsW = + let eqs = map (second (const [])) eqsG ++ eqsW in tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs where + -- If we allow negated numbers we simply do not emit the inequalities + -- derived from the subtractions that are converted to additions with a + -- negated operand + subToPred | negNumbers = const [] + | otherwise = map subtractionToPred + simples :: [CoreUnify] -> [((EvTerm, Ct), [Ct])] - -> [Either NatEquality NatInEquality] - -> [Either NatEquality NatInEquality] + -> [(Either NatEquality NatInEquality,[(Type,Type)])] + -> [(Either NatEquality NatInEquality,[(Type,Type)])] -> TcPluginM SimplifyResult simples _subst evs _xs [] = return (Simplified evs) - simples subst evs xs (eq@(Left (ct,u,v)):eqs') = do + simples subst evs xs (eq@(Left (ct,u,v),k):eqs') = do ur <- unifyNats ct (substsSOP subst u) (substsSOP subst v) tcPluginTrace "unifyNats result" (ppr ur) case ur of Win -> do - evs' <- maybe evs (:evs) <$> evMagic ct [] + evs' <- maybe evs (:evs) <$> evMagic ct (subToPred k) simples subst evs' [] (xs ++ eqs') - Lose -> return (Impossible eq) + Lose -> return (Impossible (fst eq)) Draw [] -> simples subst evs (eq:xs) eqs' Draw subst' -> do - evM <- evMagic ct (map unifyItemToPredType subst') + evM <- evMagic ct (map unifyItemToPredType subst' ++ + subToPred k) case evM of Nothing -> simples subst evs xs eqs' Just ev -> simples (substsSubst subst' subst ++ subst') (ev:evs) [] (xs ++ eqs') - simples subst evs xs (eq@(Right (ct,u)):eqs') = do - let u' = substsSOP subst u - tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u')) + simples subst evs xs (eq@(Right (ct,u),k):eqs') = do + let u' = substsSOP subst (subtractIneq u) + ineqs = map snd (rights (map fst eqsG)) + tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u')) case isNatural u' of Just True -> do - evs' <- maybe evs (:evs) <$> evMagic ct [] - simples subst evs' xs eqs' - Just False -> return (Impossible eq) - Nothing -> + evs' <- maybe evs (:evs) <$> evMagic ct (subToPred k) + case ineqToSubst u of + Just s + | u `elem` ineqs + -> mergeSimplifyResult + <$> simples (substsSubst [s] subst ++ [s]) evs' [] (xs ++ eqs') + <*> simples subst evs' xs eqs' + _ -> simples subst evs' xs eqs' + + Just False -> return (Impossible (fst eq)) + Nothing -- This inequality is either a given constraint, or it is a wanted -- constraint, which in normal form is equal to another given -- constraint, hence it can be solved. - if u `elem` (map snd (rights eqsG)) - then do - evs' <- maybe evs (:evs) <$> evMagic ct [] - simples subst evs' xs eqs' - else simples subst evs (eq:xs) eqs' + | or (mapMaybe (solveIneq 5 u) ineqs) + -> do + evs' <- maybe evs (:evs) <$> evMagic ct (subToPred k) + case ineqToSubst u of + Just s + | u `elem` ineqs + -> mergeSimplifyResult + <$> simples (substsSubst [s] subst ++ [s]) evs' [] (xs ++ eqs') + <*> simples subst evs' xs eqs' + _ -> simples subst evs' xs eqs' + | otherwise + -> simples subst evs (eq:xs) eqs' -- Extract the Nat equality constraints -toNatEquality :: Ct -> Maybe (Either NatEquality NatInEquality) +toNatEquality :: Ct -> Maybe (Either NatEquality NatInEquality,[(Type,Type)]) toNatEquality ct = case classifyPredType $ ctEvPred $ ctEvidence ct of EqPred NomEq t1 t2 -> go t1 t2 @@ -217,20 +360,31 @@ , null ([tc,tc'] `intersect` [typeNatAddTyCon,typeNatSubTyCon ,typeNatMulTyCon,typeNatExpTyCon]) = case filter (not . uncurry eqType) (zip xs ys) of - [(x,y)] | isNatKind (typeKind x) && isNatKind (typeKind y) - -> Just (Left (ct, normaliseNat x, normaliseNat y)) + [(x,y)] + | isNatKind (typeKind x) + , isNatKind (typeKind y) + , let (x',k1) = runWriter (normaliseNat x) + , let (y',k2) = runWriter (normaliseNat y) + -> Just (Left (ct, x', y'),k1 ++ k2) _ -> Nothing | tc == typeNatLeqTyCon , [x,y] <- xs - = if tc' == promotedTrueDataCon - then Just (Right (ct,normaliseNat (mkTyConApp typeNatSubTyCon [y,x]))) - else if tc' == promotedFalseDataCon - then Just (Right (ct,normaliseNat (mkTyConApp typeNatSubTyCon [x,mkTyConApp typeNatAddTyCon [y,mkNumLitTy 1]]))) - else Nothing + , let (x',k1) = runWriter (normaliseNat x) + , let (y',k2) = runWriter (normaliseNat y) + , let ks = k1 ++ k2 + = case tc' of + _ | tc' == promotedTrueDataCon + -> Just (Right (ct, (x', y', True)), ks) + _ | tc' == promotedFalseDataCon + -> Just (Right (ct, (x', y', False)), ks) + _ -> Nothing go x y - | isNatKind (typeKind x) && isNatKind (typeKind y) - = Just (Left (ct,normaliseNat x,normaliseNat y)) + | isNatKind (typeKind x) + , isNatKind (typeKind y) + , let (x',k1) = runWriter (normaliseNat x) + , let (y',k2) = runWriter (normaliseNat y) + = Just (Left (ct,x',y'),k1 ++ k2) | otherwise = Nothing diff --git a/src/GHC/TypeLits/Normalise/Unify.hs b/src/GHC/TypeLits/Normalise/Unify.hs --- a/src/GHC/TypeLits/Normalise/Unify.hs +++ b/src/GHC/TypeLits/Normalise/Unify.hs @@ -32,14 +32,21 @@ , unifiers -- * Free variables in 'SOP' terms , fvSOP + -- * Inequalities + , subtractIneq + , solveIneq + , ineqToSubst + , subtractionToPred -- * Properties , isNatural ) where -- External +import Control.Monad.Trans.Writer.Strict import Data.Function (on) import Data.List ((\\), intersect, mapAccumL, nub) +import Data.Maybe (fromMaybe, mapMaybe) import GHC.Base (isTrue#,(==#)) import GHC.Integer (smallInteger) @@ -51,11 +58,12 @@ import TcRnMonad (Ct, ctEvidence, isGiven) import TcRnTypes (ctEvPred) import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, - typeNatSubTyCon) + typeNatSubTyCon, typeNatLeqTyCon) import Type (EqRel (NomEq), PredTree (EqPred), TyVar, classifyPredType, coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy, - nonDetCmpType) + nonDetCmpType, PredType, mkPrimEqPred) import TyCoRep (Type (..), TyLit (..)) +import TysWiredIn (promotedTrueDataCon) import UniqSet (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets, unitUniqSet) @@ -85,18 +93,19 @@ -- * literals -- * type variables -- * Applications of the arithmetic operators @(+,-,*,^)@ -normaliseNat :: Type -> CoreSOP +normaliseNat :: Type -> Writer [(Type,Type)] CoreSOP normaliseNat ty | Just ty1 <- coreView ty = normaliseNat ty1 -normaliseNat (TyVarTy v) = S [P [V v]] -normaliseNat (LitTy (NumTyLit i)) = S [P [I i]] +normaliseNat (TyVarTy v) = return (S [P [V v]]) +normaliseNat (LitTy (NumTyLit i)) = return (S [P [I i]]) normaliseNat (TyConApp tc [x,y]) - | tc == typeNatAddTyCon = mergeSOPAdd (normaliseNat x) (normaliseNat y) - | tc == typeNatSubTyCon = mergeSOPAdd (normaliseNat x) - (mergeSOPMul (S [P [I (-1)]]) - (normaliseNat y)) - | tc == typeNatMulTyCon = mergeSOPMul (normaliseNat x) (normaliseNat y) - | tc == typeNatExpTyCon = normaliseExp (normaliseNat x) (normaliseNat y) -normaliseNat t = S [P [C (CType t)]] + | tc == typeNatAddTyCon = mergeSOPAdd <$> normaliseNat x <*> normaliseNat y + | tc == typeNatSubTyCon = do + tell [(x,y)] + mergeSOPAdd <$> normaliseNat x + <*> (mergeSOPMul (S [P [I (-1)]]) <$> normaliseNat y) + | tc == typeNatMulTyCon = mergeSOPMul <$> normaliseNat x <*> normaliseNat y + | tc == typeNatExpTyCon = normaliseExp <$> normaliseNat x <*> normaliseNat y +normaliseNat t = return (S [P [C (CType t)]]) -- | Convert a 'SOP' term back to a type of /kind/ 'GHC.TypeLits.Nat' reifySOP :: CoreSOP -> Type @@ -165,6 +174,59 @@ ,reifySOP (S s2) ] +-- | Subtract an inequality, in order to either: +-- +-- * See if the smallest solution is a natural number +-- * Cancel sums, i.e. monotonicity of addition +-- +-- @ +-- subtractIneq (2*y <=? 3*x ~ True) = (-2*y + 3*x) +-- subtractIneq (2*y <=? 3*x ~ False) = (-3*x + (-1) + 2*y) +-- @ +subtractIneq + :: (CoreSOP, CoreSOP, Bool) + -> CoreSOP +subtractIneq (x,y,isLE) + | isLE + = mergeSOPAdd y (mergeSOPMul (S [P [I (-1)]]) x) + | otherwise + = mergeSOPAdd x (mergeSOPMul (S [P [I (-1)]]) (mergeSOPAdd y (S [P [I 1]]))) + +-- | Try to reverse the process of 'subtractIneq' +-- +-- E.g. +-- +-- @ +-- subtractIneq (2*y <=? 3*x ~ True) = (-2*y + 3*x) +-- sopToIneq (-2*y+3*x) = Just (2*x <=? 3*x ~ True) +-- @ +sopToIneq + :: CoreSOP + -> Maybe Ineq +sopToIneq (S [P ((I i):l),r]) + | i < 0 + = Just (mergeSOPMul (S [P [I (negate i)]]) (S [P l]),S [r],True) +sopToIneq (S [r,P ((I i:l))]) + | i < 0 + = Just (mergeSOPMul (S [P [I (negate i)]]) (S [P l]),S [r],True) +sopToIneq _ = Nothing + +-- | Give the smallest solution for an inequality +ineqToSubst + :: Ineq + -> Maybe CoreUnify +ineqToSubst (x,S [P [V v]],True) + = Just (SubstItem v x) +ineqToSubst _ + = Nothing + +subtractionToPred + :: (Type,Type) + -> PredType +subtractionToPred (x,y) = + mkPrimEqPred (mkTyConApp typeNatLeqTyCon [y,x]) + (mkTyConApp promotedTrueDataCon []) + -- | A substitution is essentially a list of (variable, 'SOP') pairs, -- but we keep the original 'Ct' that lead to the substitution being -- made, for use when turning the substitution back into constraints. @@ -389,12 +451,19 @@ | i > j = unifiers' ct (S ((P [I (i-j)]):ps1)) (S ps2) -- (a + c) ~ (b + c) ==> [a := b] -unifiers' ct (S ps1) (S ps2) - | null psx = case concat (zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2) of - [] -> unifiers'' ct (S ps1) (S ps2) - ks -> nub ks - | otherwise = unifiers' ct (S ps1'') (S ps2'') +unifiers' ct s1@(S ps1) s2@(S ps2) = case sopToIneq k1 of + Just (s1',s2',_) + | s1' /= s1 || s2' /= s1 + , fromMaybe True (isNatural s1') + , fromMaybe True (isNatural s2') + -> unifiers' ct s1' s2' + _ | null psx + -> case concat (zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2) of + [] -> unifiers'' ct (S ps1) (S ps2) + ks -> nub ks + _ -> unifiers' ct (S ps1'') (S ps2'') where + k1 = subtractIneq (s1,s2,True) ps1' = ps1 \\ psx ps2' = ps2 \\ psx ps1'' | null ps1' = [P [I 0]] @@ -461,6 +530,12 @@ | i >= 0 = isNatural (S [P ps]) | otherwise = return False isNatural (S [P (V _:ps)]) = isNatural (S [P ps]) +isNatural (S [P (E s p:ps)]) = do + sN <- isNatural s + pN <- isNatural (S [p]) + if sN && pN + then isNatural (S [P ps]) + else Nothing -- This is a quick hack, it determines that -- -- > a^b - 1 @@ -482,3 +557,269 @@ _ -> Nothing -- if one is natural and the other isn't, then their sum *might* be natural, -- but we simply cant be sure. + +-- | Try to solve inequalities +solveIneq + :: Word + -- ^ Solving depth + -> Ineq + -- ^ Inequality we want to solve + -> Ineq + -- ^ Given/proven inequality + -> Maybe Bool + -- ^ Solver result + -- + -- * /Nothing/: exhausted solver steps + -- + -- * /Just True/: inequality is solved + -- + -- * /Just False/: solver is unable to solve inequality, note that this does + -- __not__ mean the wanted inequality does not hold. +solveIneq 0 _ _ = Nothing +solveIneq k want@(_,_,True) have@(_,_,True) + | want == have + = Just True + | null solved + = Nothing + | otherwise + = Just (or solved) + where + solved = mapMaybe (uncurry (solveIneq (k - 1))) new + new = mapMaybe (\f -> f want have) ineqRules +solveIneq _ _ _ = Just False + +type Ineq = (CoreSOP, CoreSOP, Bool) +type IneqRule = Ineq -> Ineq -> Maybe (Ineq,Ineq) + +ineqRules + :: [IneqRule] +ineqRules = + [ leTrans + , plusMonotone + , timesMonotone + , powMonotone + , pow2MonotoneSpecial + ] + +-- | Transitivity of inequality +leTrans :: IneqRule +leTrans want@(a,b,le) (x,y,_) + -- want: 1 <=? y ~ True + -- have: 2 <=? y ~ True + -- + -- new want: want + -- new have: 1 <=? y ~ True + | S [P [I a']] <- a + , S [P [I x']] <- x + , x' >= a' + = Just (want,(a,y,le)) + -- want: y <=? 10 ~ True + -- have: y <=? 9 ~ True + -- + -- new want: want + -- new have: y <=? 10 ~ True + | S [P [I b']] <- b + , S [P [I y']] <- y + , y' < b' + = Just (want,(x,b,le)) +leTrans _ _ = Nothing + +-- | Monotonicity of addition +-- +-- We use SOP normalization to apply this rule by e.g.: +-- +-- * Given: (2*x+1) <= (3*x-1) +-- * Turn to: (3*x-1) - (2*x+1) +-- * SOP version: -2 + x +-- * Convert back to inequality: 2 <= x +plusMonotone :: IneqRule +plusMonotone want have + | Just want' <- sopToIneq (subtractIneq want) + , want' /= want + = Just (want',have) + | Just have' <- sopToIneq (subtractIneq have) + , have' /= have + = Just (want,have') +plusMonotone _ _ = Nothing + +-- | Monotonicity of multiplication +timesMonotone :: IneqRule +timesMonotone want@(a,b,le) have@(x,y,_) + -- want: C*a <=? b ~ True + -- have: x <=? y ~ True + -- + -- new want: want + -- new have: C*a <=? C*y ~ True + | S [P a'@(_:_:_)] <- a + , S [P x'] <- x + , S [P y'] <- y + , let ax = a' \\ x' + , let ay = a' \\ y' + -- Ensure we don't repeat this rule over and over + , not (null ax) + , not (null ay) + -- Pick the smallest product + , let az = if length ax <= length ay then S [P ax] else S [P ay] + = Just (want,(mergeSOPMul az x, mergeSOPMul az y,le)) + + -- want: a <=? C*b ~ True + -- have: x <=? y ~ True + -- + -- new want: want + -- new have: C*a <=? C*y ~ True + | S [P b'@(_:_:_)] <- b + , S [P x'] <- x + , S [P y'] <- y + , let bx = b' \\ x' + , let by = b' \\ y' + -- Ensure we don't repeat this rule over and over + , not (null bx) + , not (null by) + -- Pick the smallest product + , let bz = if length bx <= length by then S [P bx] else S [P by] + = Just (want,(mergeSOPMul bz x, mergeSOPMul bz y,le)) + + -- want: a <=? b ~ True + -- have: C*x <=? y ~ True + -- + -- new want: C*a <=? C*b ~ True + -- new have: have + | S [P x'@(_:_:_)] <- x + , S [P a'] <- a + , S [P b'] <- b + , let xa = x' \\ a' + , let xb = x' \\ b' + -- Ensure we don't repeat this rule over and over + , not (null xa) + , not (null xb) + -- Pick the smallest product + , let xz = if length xa <= length xb then S [P xa] else S [P xb] + = Just ((mergeSOPMul xz a, mergeSOPMul xz b,le),have) + + -- want: a <=? b ~ True + -- have: x <=? C*y ~ True + -- + -- new want: C*a <=? C*b ~ True + -- new have: have + | S [P y'@(_:_:_)] <- y + , S [P a'] <- a + , S [P b'] <- b + , let ya = y' \\ a' + , let yb = y' \\ b' + -- Ensure we don't repeat this rule over and over + , not (null ya) + , not (null yb) + -- Pick the smallest product + , let yz = if length ya <= length yb then S [P ya] else S [P yb] + = Just ((mergeSOPMul yz a, mergeSOPMul yz b,le),have) + +timesMonotone _ _ = Nothing + +-- | Monotonicity of exponentiation +powMonotone :: IneqRule +powMonotone want (x, S [P [E yS yP]],le) + = case x of + S [P [E xS xP]] + -- want: XXX + -- have: 2^x <=? 2^y ~ True + -- + -- new want: want + -- new have: x <=? y ~ True + | xS == yS + -> Just (want,(S [xP],S [yP],le)) + -- want: XXX + -- have: x^2 <=? y^2 ~ True + -- + -- new want: want + -- new have: x <=? y ~ True + | xP == yP + -> Just (want,(xS,yS,le)) + -- want: XXX + -- have: 2 <=? 2 ^ x ~ True + -- + -- new want: want + -- new have: 1 <=? x ~ True + _ | x == yS + -> Just (want,(S [P [I 1]],S [yP],le)) + _ -> Nothing + +powMonotone (a,S [P [E bS bP]],le) have + = case a of + S [P [E aS aP]] + -- want: 2^x <=? 2^y ~ True + -- have: XXX + -- + -- new want: x <=? y ~ True + -- new have: have + | aS == bS + -> Just ((S [aP],S [bP],le),have) + -- want: x^2 <=? y^2 ~ True + -- have: XXX + -- + -- new want: x <=? y ~ True + -- new have: have + | aP == bP + -> Just ((aS,bS,le),have) + -- want: 2 <=? 2 ^ x ~ True + -- have: XXX + -- + -- new want: 1 <=? x ~ True + -- new have: XXX + _ | a == bS + -> Just ((S [P [I 1]],S [bP],le),have) + _ -> Nothing + +powMonotone _ _ = Nothing + +-- | Try to get the power-of-2 factors, and apply the monotonicity of +-- exponentiation rule. +-- +-- TODO: I wish we could generalize to find arbitrary factors, but currently +-- I don't know how. +pow2MonotoneSpecial :: IneqRule +pow2MonotoneSpecial (a,b,le) have + -- want: 4 * 4^x <=? 8^x ~ True + -- have: XXX + -- + -- want as pow 2 factors: 2^(2+2*x) <=? 2^(3*x) ~ True + -- + -- new want: 2+2*x <=? 3*x ~ True + -- new have: have + | Just a' <- facSOP 2 a + , Just b' <- facSOP 2 b + = Just ((a',b',le),have) +pow2MonotoneSpecial want (x,y,le) + -- want: XXX + -- have:4 * 4^x <=? 8^x ~ True + -- + -- have as pow 2 factors: 2^(2+2*x) <=? 2^(3*x) ~ True + -- + -- new want: want + -- new have: 2+2*x <=? 3*x ~ True + | Just x' <- facSOP 2 x + , Just y' <- facSOP 2 y + = Just (want,(x',y',le)) +pow2MonotoneSpecial _ _ = Nothing + +-- | Get the power of /N/ factors of a SOP term +facSOP + :: Integer + -- ^ The power /N/ + -> CoreSOP + -> Maybe CoreSOP +facSOP n (S [P ps]) = fmap (S . concat . map unS) (traverse (facSymbol n) ps) +facSOP _ _ = Nothing + +-- | Get the power of /N/ factors of a Symbol +facSymbol + :: Integer + -- ^ The power + -> CoreSymbol + -> Maybe CoreSOP +facSymbol n (I i) + | Just j <- integerLogBase n i + = Just (S [P [I j]]) +facSymbol n (E s p) + | Just s' <- facSOP n s + = Just (mergeSOPMul s' (S [p])) +facSymbol _ _ = Nothing diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs --- a/tests/ErrorTests.hs +++ b/tests/ErrorTests.hs @@ -1,4 +1,5 @@ -{-# LANGUAGE DataKinds, KindSignatures, TemplateHaskell, TypeFamilies, TypeOperators #-} +{-# LANGUAGE DataKinds, GADTs, KindSignatures, ScopedTypeVariables, TemplateHaskell, + TypeApplications, TypeFamilies, TypeOperators #-} {-# OPTIONS_GHC -fdefer-type-errors #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} @@ -159,3 +160,19 @@ ["Expected type: Proxy n -> Proxy (n + d)" ,"Actual type: Proxy n -> Proxy n" ] + +data Fin (n :: Nat) where + FZ :: Fin (n + 1) + FS :: Fin n -> Fin (n + 1) + +test16 :: forall n . Integer -> Fin n +test16 n = case n of + 0 -> FZ + x -> FS (test16 @(n-1) (x-1)) + +test16Errors = + [$(do localeEncoding <- runIO (getLocaleEncoding) + if textEncodingName localeEncoding == textEncodingName utf8 + then litE $ stringL "Couldn't match type ‘1 <=? n’ with ‘'True’" + else litE $ stringL "Couldn't match type `1 <=? n' with 'True" + )] diff --git a/tests/Tests.hs b/tests/Tests.hs --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -263,15 +263,21 @@ proxyInEq6 :: Proxy 1 -> Proxy (a + 3) -> () proxyInEq6 = proxyInEq -proxyEq1 :: Proxy ((2 ^ x) * (2 ^ (x + x))) -> Proxy (2 * (2 ^ ((x + (x + x)) - 1))) +proxyEq1 + :: (1 <= x) + => Proxy ((2 ^ x) * (2 ^ (x + x))) + -> Proxy (2 * (2 ^ ((x + (x + x)) - 1))) proxyEq1 = id -proxyEq2 :: Proxy (((2 ^ x) - 2) * (2 ^ (x + x))) -> Proxy ((2 ^ ((x + (x + x)) - 1)) + ((2 ^ ((x + (x + x)) - 1)) - (2 ^ ((x + x) + 1)))) +proxyEq2 + :: (2 <= x) + => Proxy (((2 ^ x) - 2) * (2 ^ (x + x))) + -> Proxy ((2 ^ ((x + (x + x)) - 1)) + ((2 ^ ((x + (x + x)) - 1)) - (2 ^ ((x + x) + 1)))) proxyEq2 = id proxyEq3 :: forall x y - . ((x + 1) ~ (2 * y)) + . ((x + 1) ~ (2 * y), 1 <= y) => Proxy x -> Proxy y -> Proxy (((2 * (y - 1)) + 1)) @@ -290,6 +296,17 @@ -> Proxy n proxyInEqImplication' _ = id +proxyEqSubst + :: ((n+1) ~ ((n1 + m) + 1), m ~ n1, n1 ~ ((n2 + m1) + 1)) + => Proxy n1 + -> Proxy n2 + -> Proxy m1 + -> Proxy n + -> Proxy m + -> Proxy (1 + (n2 + m1)) + -> Proxy n1 +proxyEqSubst _ _ _ _ _ = id + main :: IO () main = defaultMain tests @@ -329,16 +346,20 @@ ] , testGroup "Equality" [ testCase "((2 ^ x) * (2 ^ (x + x))) ~ (2 * (2 ^ ((x + (x + x)) - 1)))" $ - show (proxyEq1 Proxy) @?= + show (proxyEq1 @1 Proxy) @?= "Proxy" , testCase "(((2 ^ x) - 2) * (2 ^ (x + x))) ~ ((2 ^ ((x + (x + x)) - 1)) + ((2 ^ ((x + (x + x)) - 1)) - (2 ^ ((x + x) + 1))))" $ - show (proxyEq2 Proxy) @?= + show (proxyEq2 @2 Proxy) @?= "Proxy" ] , testGroup "Implications" [ testCase "(x + 1) ~ (2 * y)) implies (((2 * (y - 1)) + 1)) ~ x" $ show (proxyEq3 (Proxy :: Proxy 3) (Proxy :: Proxy 2) Proxy) @?= "Proxy" + , testCase "(n+1) ~ ((n1 + m) + 1), m ~ n1, n1 ~ ((n2 + m1) + 1) implies n1 ~ 1 + (n2 + m1)" $ + show (proxyEqSubst (Proxy :: Proxy 6) (Proxy :: Proxy 2) (Proxy :: Proxy 3) + (Proxy :: Proxy 12) (Proxy :: Proxy 6) (Proxy :: Proxy 6)) @?= + "Proxy" ] , testGroup "Inequality" [ testCase "a <= a+1" $ @@ -372,6 +393,7 @@ , testCase "Unify \"2^k\" with \"7\"" $ testProxy6 `throws` testProxy6Errors , testCase "x ~ y + x" $ testProxy8 `throws` testProxy8Errors , testCase "(CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => n ~ (n+d)" $ (testProxy15 (Proxy :: Proxy 1)) `throws` testProxy15Errors + , testCase "(n - 1) + 1 ~ n implies (1 <= n)" $ test16 `throws` test16Errors , testGroup "Inequality" [ testCase "a+1 <= a" $ testProxy9 `throws` testProxy9Errors , testCase "(a <=? a+1) ~ False" $ testProxy10 `throws` testProxy10Errors