ghc-typelits-natnormalise 0.5.10 → 0.6
raw patch · 6 files changed
+624/−68 lines, 6 filesdep +transformersdep ~ghc-tcplugins-extraPVP ok
version bump matches the API change (PVP)
Dependencies added: transformers
Dependency ranges changed: ghc-tcplugins-extra
API changes (from Hackage documentation)
+ GHC.TypeLits.Normalise.Unify: ineqToSubst :: Ineq -> Maybe CoreUnify
+ GHC.TypeLits.Normalise.Unify: solveIneq :: Word -> Ineq -> Ineq -> Maybe Bool
+ GHC.TypeLits.Normalise.Unify: subtractIneq :: (CoreSOP, CoreSOP, Bool) -> CoreSOP
+ GHC.TypeLits.Normalise.Unify: subtractionToPred :: (Type, Type) -> PredType
- GHC.TypeLits.Normalise.Unify: normaliseNat :: Type -> CoreSOP
+ GHC.TypeLits.Normalise.Unify: normaliseNat :: Type -> Writer [(Type, Type)] CoreSOP
Files
- CHANGELOG.md +21/−0
- ghc-typelits-natnormalise.cabal +3/−2
- src/GHC/TypeLits/Normalise.hs +197/−43
- src/GHC/TypeLits/Normalise/Unify.hs +358/−17
- tests/ErrorTests.hs +18/−1
- tests/Tests.hs +27/−5
CHANGELOG.md view
@@ -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
ghc-typelits-natnormalise.cabal view
@@ -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
src/GHC/TypeLits/Normalise.hs view
@@ -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 <http://hackage.haskell.org/package/mezzo mezzo>+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
src/GHC/TypeLits/Normalise/Unify.hs view
@@ -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
tests/ErrorTests.hs view
@@ -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"+ )]
tests/Tests.hs view
@@ -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