equational-reasoning 0.7.0.3 → 0.7.1.0
raw patch · 7 files changed
+337/−371 lines, 7 filesdep ~basedep ~containersdep ~template-haskellPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: base, containers, template-haskell, th-desugar
API changes (from Hackage documentation)
- Proof.Equational: class Preorder eq => Equality (eq :: k -> k -> Type)
+ Proof.Equational: class (Preorder eq) => Equality (eq :: k -> k -> Type)
Files
- Changelog.md +5/−0
- Proof/Equational.hs +55/−56
- Proof/Propositional.hs +35/−36
- Proof/Propositional/Empty.hs +48/−32
- Proof/Propositional/Inhabited.hs +37/−21
- Proof/Propositional/TH.hs +150/−220
- equational-reasoning.cabal +7/−6
Changelog.md view
@@ -1,6 +1,11 @@ Changelog ========== +## 0.7.1.0++- Supports GHC 9.10 and 9.12+- Drops support for GHC <9.2+ ## 0.7.0.2 - Supports GHC 9.8
Proof/Equational.hs view
@@ -15,53 +15,52 @@ #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800 {-# LANGUAGE ConstrainedClassMethods, TypeFamilyDependencies #-} #endif-module Proof.Equational- ( (:~:) (..),- (:=:),- sym,- trans,- Equality (..),- Preorder (..),- reflexivity',- (:\/:),- (:/\:),- (=<=),- (=>=),- (=~=),- Leibniz (..),- Reason (..),- because,- by,- (===),- start,- byDefinition,- admitted,- Proxy (..),- cong,- cong',- Proposition (..),- HVec (..),- FromBool (..),- applyNAry,- applyNAry',- fromBool',+module Proof.Equational (+ (:~:) (..),+ (:=:),+ sym,+ trans,+ Equality (..),+ Preorder (..),+ reflexivity',+ (:\/:),+ (:/\:),+ (=<=),+ (=>=),+ (=~=),+ Leibniz (..),+ Reason (..),+ because,+ by,+ (===),+ start,+ byDefinition,+ admitted,+ Proxy (..),+ cong,+ cong',+ Proposition (..),+ HVec (..),+ FromBool (..),+ applyNAry,+ applyNAry',+ fromBool', - -- * Conversion between equalities- fromRefl,- fromLeibniz,- reflToLeibniz,- leibnizToRefl,+ -- * Conversion between equalities+ fromRefl,+ fromLeibniz,+ reflToLeibniz,+ leibnizToRefl, - -- * Coercion- coerce,- coerceInner,- coerce',- withRefl,+ -- * Coercion+ coerce,+ coerceInner,+ coerce',+ withRefl, - -- * Re-exported modules- module Data.Proxy,- )-where+ -- * Re-exported modules+ module Data.Proxy,+) where import Data.Kind (Type) import Data.Proxy@@ -98,7 +97,7 @@ reflexivity :: proxy a -> eq a a transitivity :: eq a b -> eq b c -> eq a c -class Preorder eq => Equality (eq :: k -> k -> Type) where+class (Preorder eq) => Equality (eq :: k -> k -> Type) where symmetry :: eq a b -> eq b a instance Preorder (:=:) where@@ -146,22 +145,22 @@ infix 5 `because` -(=<=) :: Preorder r => r x y -> Reason r y z -> r x z+(=<=) :: (Preorder r) => r x y -> Reason r y z -> r x z eq =<= (_ `Because` eq') = transitivity eq eq' {-# SPECIALIZE INLINE [1] (=<=) :: x :~: y -> Reason (:~:) y z -> x :~: z #-} -(=>=) :: Preorder r => r y z -> Reason r x y -> r x z+(=>=) :: (Preorder r) => r y z -> Reason r x y -> r x z eq =>= (_ `Because` eq') = transitivity eq' eq {-# SPECIALIZE INLINE [1] (=>=) :: y :~: z -> Reason (:~:) x y -> x :~: z #-} -(===) :: Equality eq => eq x y -> Reason eq y z -> eq x z+(===) :: (Equality eq) => eq x y -> Reason eq y z -> eq x z (===) = (=<=) {-# SPECIALIZE INLINE [1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-} (=~=) :: r x y -> proxy y -> r x y eq =~= _ = eq -start :: Preorder eq => proxy a -> eq a a+start :: (Preorder eq) => proxy a -> eq a a start = reflexivity byDefinition :: (Preorder eq) => eq a a@@ -207,7 +206,7 @@ It has the same effect as @'Data.Type.Equality.gcastWith'@, but some hacks is done to reduce runtime overhead. -}-withRefl :: forall a b r. a :~: b -> (a ~ b => r) -> r+withRefl :: forall a b r. a :~: b -> ((a ~ b) => r) -> r withRefl _ = gcastWith (unsafeCoerce (Refl :: () :~: ()) :: a :~: b) class Proposition (f :: k -> Type) where@@ -239,12 +238,12 @@ instance KnownTypeList '[] where viewHVec' = HNilView -instance KnownTypeList ts => KnownTypeList (t ': ts) where+instance (KnownTypeList ts) => KnownTypeList (t ': ts) where viewHVec' = HConsView Proxy viewHVec' -newtype Magic (xs :: [Type]) a = Magic {_viewHVec' :: KnownTypeList xs => a}+newtype Magic (xs :: [Type]) a = Magic {_viewHVec' :: (KnownTypeList xs) => a} -withKnownTypeList :: forall a xs. HVecView xs -> (KnownTypeList xs => a) -> a+withKnownTypeList :: forall a xs. HVecView xs -> ((KnownTypeList xs) => a) -> a withKnownTypeList xs f = (unsafeCoerce (Magic f :: Magic xs a) :: HVecView xs -> a) xs apply' :: HVecView ts -> (HVec ts -> c) -> ts :~> c@@ -253,16 +252,16 @@ withKnownTypeList ts $ apply' ts (\ts' -> f $ a :- ts') -applyNAry :: forall ts c. KnownTypeList ts => (HVec ts -> c) -> ts :~> c+applyNAry :: forall ts c. (KnownTypeList ts) => (HVec ts -> c) -> ts :~> c applyNAry = apply' (viewHVec' :: HVecView ts) -applyNAry' :: KnownTypeList ts => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c+applyNAry' :: (KnownTypeList ts) => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c applyNAry' _ _ = applyNAry class FromBool (c :: Type) where type Predicate c :: Bool type Args c :: [Type]- fromBool :: Predicate c ~ 'True => HVec (Args c) -> c+ fromBool :: (Predicate c ~ 'True) => HVec (Args c) -> c fromBool' :: forall proxy c. (KnownTypeList (Args c), FromBool c, Predicate c ~ 'True) => proxy c -> Args c :~> c fromBool' pxyc = applyNAry' (Proxy :: Proxy (Args c)) pxyc fromBool
Proof/Propositional.hs view
@@ -16,32 +16,31 @@ {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Provides type synonyms for logical connectives.-module Proof.Propositional- ( type (/\),- type (\/),- Not,- exfalso,- orIntroL,- orIntroR,- orElim,- andIntro,- andElimL,- andElimR,- orAssocL,- orAssocR,- andAssocL,- andAssocR,- IsTrue (..),- withWitness,- Empty (..),- withEmpty,- withEmpty',- refute,- Inhabited (..),- withInhabited,- prove,- )-where+module Proof.Propositional (+ type (/\),+ type (\/),+ Not,+ exfalso,+ orIntroL,+ orIntroR,+ orElim,+ andIntro,+ andElimL,+ andElimR,+ orAssocL,+ orAssocR,+ andAssocL,+ andAssocR,+ IsTrue (..),+ withWitness,+ Empty (..),+ withEmpty,+ withEmpty',+ refute,+ Inhabited (..),+ withInhabited,+ prove,+) where import Data.Data (Data) import Data.Type.Equality (gcastWith, (:~:) (..))@@ -105,7 +104,7 @@ data IsTrue (b :: Bool) where Witness :: IsTrue 'True -withWitness :: forall b r. IsTrue b -> (b ~ 'True => r) -> r+withWitness :: forall b r. IsTrue b -> ((b ~ 'True) => r) -> r withWitness _ = gcastWith (unsafeCoerce (Refl :: () :~: ()) :: b :~: 'True) {-# NOINLINE withWitness #-} @@ -126,14 +125,14 @@ refute [t|0 :~: 1|] refute [t|() :~: Int|]-refute [t| 'True :~: 'False|]-refute [t| 'False :~: 'True|]-refute [t| 'LT :~: 'GT|]-refute [t| 'LT :~: 'EQ|]-refute [t| 'EQ :~: 'LT|]-refute [t| 'EQ :~: 'GT|]-refute [t| 'GT :~: 'LT|]-refute [t| 'GT :~: 'EQ|]+refute [t|'True :~: 'False|]+refute [t|'False :~: 'True|]+refute [t|'LT :~: 'GT|]+refute [t|'LT :~: 'EQ|]+refute [t|'EQ :~: 'LT|]+refute [t|'EQ :~: 'GT|]+refute [t|'GT :~: 'LT|]+refute [t|'GT :~: 'EQ|] prove [t|Bool|] prove [t|Int|]@@ -150,4 +149,4 @@ prove [t|IsTrue 'True|] instance Empty (IsTrue 'False) where- eliminate = \case+ eliminate = \case {}
Proof/Propositional/Empty.hs view
@@ -1,59 +1,75 @@-{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}-{-# LANGUAGE DataKinds, DefaultSignatures, DeriveAnyClass, EmptyCase #-}-{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances #-}-{-# LANGUAGE GADTs, KindSignatures, LambdaCase, PolyKinds #-}-{-# LANGUAGE StandaloneDeriving, TupleSections, TypeOperators #-}-module Proof.Propositional.Empty (Empty(..), withEmpty, withEmpty') where-import Data.Void (Void, absurd)+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeOperators #-}++module Proof.Propositional.Empty (Empty (..), withEmpty, withEmpty') where++import Data.Void (Void, absurd) import GHC.Generics-import Unsafe.Coerce (unsafeCoerce)+import Unsafe.Coerce (unsafeCoerce) --- | Type-class for types without inhabitants, dual to @'Proof.Propositional.Inhabited'@.--- Current GHC doesn't provide selective-instance,--- hence we don't @'Empty'@ provide instances--- for product types in a generic deriving (DeriveAnyClass).--- --- To derive an instance for each concrete types,--- use @'Proof.Propositional.refute'@.------ Since 0.4.0.0.+{- | Type-class for types without inhabitants, dual to @'Proof.Propositional.Inhabited'@.+ Current GHC doesn't provide selective-instance,+ hence we don't @'Empty'@ provide instances+ for product types in a generic deriving (DeriveAnyClass).++ To derive an instance for each concrete types,+ use @'Proof.Propositional.refute'@.++ Since 0.4.0.0.+-} class Empty a where eliminate :: a -> x- default eliminate :: (Generic a, GEmpty (Rep a)) => a -> x eliminate = geliminate . from class GEmpty f where geliminate :: f a -> x -instance GEmpty f => GEmpty (M1 i t f) where+instance (GEmpty f) => GEmpty (M1 i t f) where geliminate (M1 a) = geliminate a instance (GEmpty f, GEmpty g) => GEmpty (f :+: g) where geliminate (L1 a) = geliminate a geliminate (R1 b) = geliminate b -instance Empty c => GEmpty (K1 i c) where+instance (Empty c) => GEmpty (K1 i c) where geliminate (K1 a) = eliminate a instance GEmpty V1 where- geliminate = \ case {}+ geliminate = \case {} deriving instance (Empty a, Empty b) => Empty (Either a b)+ deriving instance Empty Void -newtype MagicEmpty e a = MagicEmpty (Empty e => a)+newtype MagicEmpty e a = MagicEmpty ((Empty e) => a) --- | Giving falsity witness by proving @'Void'@ from @a@.--- See also 'withEmpty''.------ Since 0.4.0.0-withEmpty :: forall a b. (a -> Void) -> (Empty a => b) -> b+{- | Giving falsity witness by proving @'Void'@ from @a@.+ See also 'withEmpty''.++ Since 0.4.0.0+-}+withEmpty :: forall a b. (a -> Void) -> ((Empty a) => b) -> b withEmpty neg k = unsafeCoerce (MagicEmpty k :: MagicEmpty a b) (absurd . neg) --- | Giving falsity witness by showing @a@ entails everything.--- See also 'withEmpty'.------ Since 0.4.0.0-withEmpty' :: forall a b. (forall c. a -> c) -> (Empty a => b) -> b+{- | Giving falsity witness by showing @a@ entails everything.+ See also 'withEmpty'.++ Since 0.4.0.0+-}+withEmpty' :: forall a b. (forall c. a -> c) -> ((Empty a) => b) -> b withEmpty' neg k = unsafeCoerce (MagicEmpty k :: MagicEmpty a b) neg
Proof/Propositional/Inhabited.hs view
@@ -1,21 +1,35 @@-{-# LANGUAGE DataKinds, DefaultSignatures, DeriveAnyClass, EmptyCase #-}-{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances #-}-{-# LANGUAGE GADTs, KindSignatures, LambdaCase, PolyKinds, RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TupleSections #-}-{-# LANGUAGE TypeOperators #-}-module Proof.Propositional.Inhabited (Inhabited(..), withInhabited) where+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeOperators #-}++module Proof.Propositional.Inhabited (Inhabited (..), withInhabited) where+ import GHC.Generics import Unsafe.Coerce (unsafeCoerce) --- | Types with at least one inhabitant, dual to @'Proof.Propositional.Empty'@.--- Currently, GHC doesn't provide a selective-instance,--- hence we can't generically derive @'Inhabited'@ instances--- for sum types (i.e. by @DeriveAnyClass@).------ To derive an instance for each concrete types,--- use @'Proof.Propositional.prove'@.------ Since 0.4.0.0.+{- | Types with at least one inhabitant, dual to @'Proof.Propositional.Empty'@.+ Currently, GHC doesn't provide a selective-instance,+ hence we can't generically derive @'Inhabited'@ instances+ for sum types (i.e. by @DeriveAnyClass@).++ To derive an instance for each concrete types,+ use @'Proof.Propositional.prove'@.++ Since 0.4.0.0.+-} class Inhabited a where -- | A /generic/ inhabitant of type @'a'@, which means that -- one cannot assume anything about the value of @'trivial'@@@ -24,34 +38,36 @@ -- * is of type @a@, and -- * doesn't contain any partial values. trivial :: a- default trivial :: (Generic a, GInhabited (Rep a)) => a trivial = to gtrivial class GInhabited f where gtrivial :: f a -instance GInhabited f => GInhabited (M1 i t f) where+instance (GInhabited f) => GInhabited (M1 i t f) where gtrivial = M1 gtrivial instance (GInhabited f, GInhabited g) => GInhabited (f :*: g) where gtrivial = gtrivial :*: gtrivial -instance Inhabited c => GInhabited (K1 i c) where+instance (Inhabited c) => GInhabited (K1 i c) where gtrivial = K1 trivial instance GInhabited U1 where gtrivial = U1 deriving instance Inhabited ()+ deriving instance (Inhabited a, Inhabited b) => Inhabited (a, b)+ deriving instance (Inhabited a, Inhabited b, Inhabited c) => Inhabited (a, b, c)+ deriving instance (Inhabited a, Inhabited b, Inhabited c, Inhabited d) => Inhabited (a, b, c, d) -instance Inhabited b => Inhabited (a -> b) where+instance (Inhabited b) => Inhabited (a -> b) where trivial = const trivial -newtype MagicInhabited a b = MagicInhabited (Inhabited a => b)+newtype MagicInhabited a b = MagicInhabited ((Inhabited a) => b) -withInhabited :: forall a b. a -> (Inhabited a => b) -> b+withInhabited :: forall a b. a -> ((Inhabited a) => b) -> b withInhabited wit k = unsafeCoerce (MagicInhabited k :: MagicInhabited a b) wit
Proof/Propositional/TH.hs view
@@ -1,160 +1,182 @@-{-# LANGUAGE CPP, ExplicitNamespaces, MultiWayIf, PatternGuards #-}-{-# LANGUAGE TemplateHaskell, TupleSections, ViewPatterns #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE ViewPatterns #-}+ module Proof.Propositional.TH where++import Control.Arrow (Kleisli (..), second)+import Control.Monad (forM, zipWithM)+import Data.Foldable (asum)+import Data.Functor (void)+import Data.Map (Map)+import qualified Data.Map as M+import Data.Maybe (fromJust)+import Data.Type.Equality ((:~:) (..))+import Language.Haskell.TH (+ DecsQ,+ Lit (CharL, IntegerL),+ Name,+ Q,+ TypeQ,+ isInstance,+ newName,+ ppr,+ )+import Language.Haskell.TH.Desugar (DClause (..), DCon (..), DConFields (..), DCxt, DDec (..), DExp (..), DForallTelescope (..), DInfo (..), DLetDec (DFunD), DPat (DConP, DVarP), DPred, DTyVarBndr (..), DType (..), Overlap (Overlapping), desugar, dsReify, expandType, substTy, sweeten) import Proof.Propositional.Empty import Proof.Propositional.Inhabited -import Control.Arrow (Kleisli (..), second)-import Control.Monad (forM, zipWithM)-import Data.Foldable (asum)-import Data.Map (Map)-import qualified Data.Map as M-import Data.Maybe (fromJust)-import Data.Type.Equality ((:~:) (..))-import Language.Haskell.TH (DecsQ, Lit (CharL, IntegerL),- Name, Q, TypeQ, isInstance,- newName, ppr)-import Language.Haskell.TH.Desugar (DClause (..), DCon (..),- DConFields (..), DCxt, DDec (..),- DExp (..), DInfo (..),- DLetDec (DFunD),-#if MIN_VERSION_th_desugar(1,10,0)- DPat (DConP, DVarP), DPred,+#if MIN_VERSION_th_desugar(1,18,0)+import Language.Haskell.TH.Desugar (dLamE, dCaseE) #else- DPat (DConPa, DVarPa), DPred(..),-#endif-#if MIN_VERSION_th_desugar(1,12,0)- DForallTelescope(..),-#endif-- DTyVarBndr (..), DType (..),- Overlap (Overlapping), desugar,- dsReify, expandType, substTy,- sweeten)-#if !MIN_VERSION_base(4,13,0)-import Data.Semigroup (Semigroup (..))-#endif-#if MIN_VERSION_th_desugar(1,12,0)-import Data.Functor (void)+import Language.Haskell.TH.Desugar (DMatch) #endif +mkDInstanceD ::+ Maybe Overlap ->+ DCxt ->+ DType ->+ [DDec] ->+ DDec+mkDInstanceD ovl ctx dtype ddecs = DInstanceD ovl Nothing ctx dtype ddecs --- | Macro to automatically derive @'Empty'@ instance for--- concrete (variable-free) types which may contain products.+{- | Macro to automatically derive @'Empty'@ instance for+ concrete (variable-free) types which may contain products.+-} refute :: TypeQ -> DecsQ refute tps = do tp <- expandType =<< desugar =<< tps let Just (_, tyName, args) = splitType tp- mkInst dxt cls = return $ sweeten- [DInstanceD (Just Overlapping)-#if MIN_VERSION_th_desugar(1,10,0)- Nothing-#endif- dxt- (DAppT (DConT ''Empty) (foldl DAppT (DConT tyName) args))- [DLetDec $ DFunD 'eliminate cls]- ]+ mkInst dxt cls =+ return $+ sweeten+ [ mkDInstanceD+ (Just Overlapping)+ dxt+ (DAppT (DConT ''Empty) (foldl DAppT (DConT tyName) args))+ [DLetDec $ DFunD 'eliminate cls]+ ] if tyName == ''(:~:) then do let [l, r] = args- v <- newName "_v"+ v <- newName "_v" dist <- compareType l r case dist of- NonEqual -> mkInst [] [DClause [] $ DLamE [v] (DCaseE (DVarE v) []) ]- Equal -> fail $ "Equal: " ++ show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)- Undecidable -> fail $ "No enough info to check non-equality: " ++- show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)+ NonEqual -> mkInst [] [DClause [] $ dLamE' [v] (dCaseE (DVarE v) [])]+ Equal -> fail $ "Equal: " ++ show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)+ Undecidable ->+ fail $+ "No enough info to check non-equality: "+ ++ show (ppr $ sweeten l)+ ++ " ~ "+ ++ show (ppr $ sweeten r) else do (dxt, cons) <- resolveSubsts args . fromJust =<< dsReify tyName Just cls <- sequence <$> mapM buildRefuteClause cons mkInst dxt cls --- | Macro to automatically derive @'Inhabited'@ instance for--- concrete (variable-free) types which may contain sums.+#if !MIN_VERSION_th_desugar(1,18,0)+dCaseE :: DExp -> [DMatch] -> DExp+dCaseE = DCaseE+#endif++dLamE' :: [Name] -> DExp -> DExp+#if MIN_VERSION_th_desugar(1,18,0)+dLamE' = dLamE . map DVarP+#else+dLamE' = DLamE+#endif++{- | Macro to automatically derive @'Inhabited'@ instance for+ concrete (variable-free) types which may contain sums.+-} prove :: TypeQ -> DecsQ prove tps = do tp <- expandType =<< desugar =<< tps let Just (_, tyName, args) = splitType tp- mkInst dxt cls = return $ sweeten- [DInstanceD (Just Overlapping)-#if MIN_VERSION_th_desugar(1,10,0)- Nothing-#endif- dxt- (DAppT (DConT ''Inhabited) (foldl DAppT (DConT tyName) args))- [DLetDec $ DFunD 'trivial cls]- ]+ mkInst dxt cls =+ return $+ sweeten+ [ mkDInstanceD+ (Just Overlapping)+ dxt+ (DAppT (DConT ''Inhabited) (foldl DAppT (DConT tyName) args))+ [DLetDec $ DFunD 'trivial cls]+ ] isNum <- isInstance ''Num [sweeten tp] - if | isNum -> mkInst [] [DClause [] $ DLitE $ IntegerL 0 ]- | tyName == ''Char -> mkInst [] [DClause [] $ DLitE $ CharL '\NUL']- | tyName == ''(:~:) -> do+ if+ | isNum -> mkInst [] [DClause [] $ DLitE $ IntegerL 0]+ | tyName == ''Char -> mkInst [] [DClause [] $ DLitE $ CharL '\NUL']+ | tyName == ''(:~:) -> do let [l, r] = args dist <- compareType l r case dist of- NonEqual -> fail $ "Equal: " ++ show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)- Equal -> mkInst [] [DClause [] $ DConE 'Refl ]- Undecidable -> fail $ "No enough info to check non-equality: " ++- show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)- | otherwise -> do+ NonEqual -> fail $ "Equal: " ++ show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)+ Equal -> mkInst [] [DClause [] $ DConE 'Refl]+ Undecidable ->+ fail $+ "No enough info to check non-equality: "+ ++ show (ppr $ sweeten l)+ ++ " ~ "+ ++ show (ppr $ sweeten r)+ | otherwise -> do (dxt, cons) <- resolveSubsts args . fromJust =<< dsReify tyName Just cls <- asum <$> mapM buildProveClause cons mkInst dxt [cls] -buildClause :: Name -> (DType -> Q b) -> (DType -> b -> DExp)- -> (Name -> [Maybe DExp] -> Maybe DExp) -> (Name -> [b] -> [DPat])- -> DCon -> Q (Maybe DClause)+buildClause ::+ Name ->+ (DType -> Q b) ->+ (DType -> b -> DExp) ->+ (Name -> [Maybe DExp] -> Maybe DExp) ->+ (Name -> [b] -> [DPat]) ->+ DCon ->+ Q (Maybe DClause) buildClause clsName genPlaceHolder buildFactor flattenExps toPats (DCon _ _ cName flds _) = do let tys = fieldsVars flds varDic <- mapM genPlaceHolder tys fmap (DClause $ toPats cName varDic) . flattenExps cName <$> zipWithM tryProc tys varDic where tryProc ty name = do- isEmpty <- isInstance clsName . (:[]) $ sweeten ty- return $ if isEmpty- then Just $ buildFactor ty name- else Nothing+ isEmpty <- isInstance clsName . (: []) $ sweeten ty+ return $+ if isEmpty+ then Just $ buildFactor ty name+ else Nothing buildRefuteClause :: DCon -> Q (Maybe DClause) buildRefuteClause = buildClause- ''Empty (const $ newName "_x")- (const $ (DVarE 'eliminate `DAppE`) . DVarE) (const asum)-#if MIN_VERSION_th_desugar(1,13,0)+ ''Empty+ (const $ newName "_x")+ (const $ (DVarE 'eliminate `DAppE`) . DVarE)+ (const asum) (\cName ps -> [DConP cName [] $ map DVarP ps])-#elif MIN_VERSION_th_desugar(1,10,0)- (\cName ps -> [DConP cName $ map DVarP ps])-#else- (\cName ps -> [DConPa cName $ map DVarPa ps])-#endif buildProveClause :: DCon -> Q (Maybe DClause)-buildProveClause =+buildProveClause = buildClause- ''Inhabited (const $ return ())+ ''Inhabited+ (const $ return ()) (const $ const $ DVarE 'trivial)- (\ con args -> foldl DAppE (DConE con) <$> sequence args )+ (\con args -> foldl DAppE (DConE con) <$> sequence args) (const $ const []) fieldsVars :: DConFields -> [DType]-#if MIN_VERSION_th_desugar(1,8,0)-fieldsVars (DNormalC _ fs)-#else-fieldsVars (DNormalC fs)-#endif- = map snd fs-fieldsVars (DRecC fs) = map (\(_,_,c) -> c) fs+fieldsVars (DNormalC _ fs) = map snd fs+fieldsVars (DRecC fs) = map (\(_, _, c) -> c) fs resolveSubsts :: [DType] -> DInfo -> Q (DCxt, [DCon]) resolveSubsts args info = case info of- (DTyConI (DDataD _ cxt _ tvbs-#if MIN_VERSION_th_desugar(1,9,0)- _-#endif- dcons _) _) -> do+ DTyConI (DDataD _ cxt _ tvbs _ dcons _) _ -> do let dic = M.fromList $ zip (map dtvbToName tvbs) args- (cxt , ) <$> mapM (substDCon dic) dcons+ (cxt,) <$> mapM (substDCon dic) dcons -- (DTyConI (DOpenTypeFamilyD n) _) -> return [] -- (DTyConI (DClosedTypeFamilyD _ ddec2) minst) -> return [] -- (DTyConI (DDataFamilyD _ ddec2) minst) -> return []@@ -168,63 +190,38 @@ substDCon dic (DCon forall'd cxt conName fields mPhantom) = DCon forall'd cxt conName <$> substFields dic fields-#if MIN_VERSION_th_desugar(1,9,0) <*> substTy dic mPhantom-#else- <*> mapM (substTy dic) mPhantom-#endif substFields :: SubstDic -> DConFields -> Q DConFields-substFields subst-#if MIN_VERSION_th_desugar(1,8,0)- (DNormalC fixi fs)-#else- (DNormalC fs)-#endif- =-#if MIN_VERSION_th_desugar(1,8,0)- DNormalC fixi <$>-#else- DNormalC <$>-#endif- mapM (runKleisli $ second $ Kleisli $ substTy subst) fs+substFields+ subst+ (DNormalC fixi fs) =+ DNormalC fixi+ <$> mapM (runKleisli $ second $ Kleisli $ substTy subst) fs substFields subst (DRecC fs) =- DRecC <$> forM fs (\(a,b,c) -> (a, b ,) <$> substTy subst c)+ DRecC <$> forM fs (\(a, b, c) -> (a,b,) <$> substTy subst c) splitType :: DType -> Maybe ([Name], Name, [DType])-#if MIN_VERSION_th_desugar(1,11,0) splitType (DConstrainedT _ t) = splitType t-#if MIN_VERSION_th_desugar(1,12,0)-splitType (DForallT (unTelescope -> vs) t) -#else-splitType (DForallT _ vs t) -#endif-#else-splitType (DForallT vs _ t) -#endif- = (\(a,b,c) -> (map dtvbToName vs ++ a, b, c)) <$> splitType t-splitType (DAppT t1 t2) = (\(a,b,c) -> (a, b, c ++ [t2])) <$> splitType t1+splitType (DForallT (unTelescope -> vs) t) =+ (\(a, b, c) -> (map dtvbToName vs ++ a, b, c)) <$> splitType t+splitType (DAppT t1 t2) = (\(a, b, c) -> (a, b, c ++ [t2])) <$> splitType t1 splitType (DSigT t _) = splitType t splitType (DVarT _) = Nothing splitType (DConT n) = Just ([], n, []) splitType DArrowT = Just ([], ''(->), []) splitType (DLitT _) = Nothing splitType DWildCardT = Nothing-#if !MIN_VERSION_th_desugar(1,9,0)-splitType DStarT = Nothing-#elif MIN_VERSION_th_desugar(1,10,0) splitType (DAppKindT _ _) = Nothing-#endif - data EqlJudge = NonEqual | Undecidable | Equal- deriving (Read, Show, Eq, Ord)+ deriving (Read, Show, Eq, Ord) instance Semigroup EqlJudge where- NonEqual <> _ = NonEqual+ NonEqual <> _ = NonEqual Undecidable <> NonEqual = NonEqual- Undecidable <> _ = Undecidable- Equal <> m = m+ Undecidable <> _ = Undecidable+ Equal <> m = m instance Monoid EqlJudge where mappend = (<>)@@ -237,69 +234,50 @@ compareType' t s compareType' :: DType -> DType -> Q EqlJudge-compareType' (DSigT t1 t2) (DSigT s1 s2)- = (<>) <$> compareType' t1 s1 <*> compareType' t2 s2-compareType' (DSigT t _) s- = compareType' t s-compareType' t (DSigT s _)- = compareType' t s+compareType' (DSigT t1 t2) (DSigT s1 s2) =+ (<>) <$> compareType' t1 s1 <*> compareType' t2 s2+compareType' (DSigT t _) s =+ compareType' t s+compareType' t (DSigT s _) =+ compareType' t s compareType' (DVarT t) (DVarT s)- | t == s = return Equal+ | t == s = return Equal | otherwise = return Undecidable compareType' (DVarT _) _ = return Undecidable compareType' _ (DVarT _) = return Undecidable compareType' DWildCardT _ = return Undecidable compareType' _ DWildCardT = return Undecidable-#if MIN_VERSION_th_desugar(1,11,0) compareType' (DConstrainedT tCxt t) (DConstrainedT sCxt s) = do pd <- compareCxt tCxt sCxt bd <- compareType' t s return (pd <> bd)-compareType' DConstrainedT{} _ = return NonEqual-#if MIN_VERSION_th_desugar(1,12,0)+compareType' DConstrainedT {} _ = return NonEqual compareType' (DForallT (unTelescope -> tTvBs) t) (DForallT (unTelescope -> sTvBs) s)-#else-compareType' (DForallT _ tTvBs t) (DForallT _ sTvBs s)-#endif | length tTvBs == length sTvBs = do let dic = M.fromList $ zip (map dtvbToName sTvBs) (map (DVarT . dtvbToName) tTvBs) s' <- substTy dic s bd <- compareType' t s' return bd | otherwise = return NonEqual-#else-compareType' (DForallT tTvBs tCxt t) (DForallT sTvBs sCxt s)- | length tTvBs == length sTvBs = do- let dic = M.fromList $ zip (map dtvbToName sTvBs) (map (DVarT . dtvbToName) tTvBs)- s' <- substTy dic s- pd <- compareCxt tCxt =<< mapM (substPred dic) sCxt- bd <- compareType' t s'- return (pd <> bd)- | otherwise = return NonEqual-#endif-compareType' DForallT{} _ = return NonEqual-compareType' (DAppT t1 t2) (DAppT s1 s2)- = (<>) <$> compareType' t1 s1 <*> compareType' t2 s2+compareType' DForallT {} _ = return NonEqual+compareType' (DAppT t1 t2) (DAppT s1 s2) =+ (<>) <$> compareType' t1 s1 <*> compareType' t2 s2 compareType' (DConT t) (DConT s)- | t == s = return Equal+ | t == s = return Equal | otherwise = return NonEqual compareType' (DConT _) _ = return NonEqual compareType' DArrowT DArrowT = return Equal compareType' DArrowT _ = return NonEqual compareType' (DLitT t) (DLitT s)- | t == s = return Equal+ | t == s = return Equal | otherwise = return NonEqual compareType' (DLitT _) _ = return NonEqual-#if !MIN_VERSION_th_desugar(1,9,0)-compareType' DStarT DStarT = return NonEqual-#endif compareType' _ _ = return NonEqual compareCxt :: DCxt -> DCxt -> Q EqlJudge compareCxt l r = mconcat <$> zipWithM comparePred l r comparePred :: DPred -> DPred -> Q EqlJudge-#if MIN_VERSION_th_desugar(1,10,0) comparePred DWildCardT _ = return Undecidable comparePred _ DWildCardT = return Undecidable comparePred (DVarT l) (DVarT r)@@ -319,71 +297,23 @@ | l == r = return Equal | otherwise = return NonEqual comparePred (DConT _) _ = return NonEqual-#if MIN_VERSION_th_desugar(1,12,0) comparePred (DForallT _ _) (DForallT _ _) = return Undecidable-#else-comparePred (DForallT _ _ _) (DForallT _ _ _) = return Undecidable-#endif-comparePred (DForallT{}) _ = return NonEqual+comparePred (DForallT {}) _ = return NonEqual comparePred _ _ = fail "Kind error: Expecting type-level predicate"-#else-comparePred DWildCardPr _ = return Undecidable-comparePred _ DWildCardPr = return Undecidable-comparePred (DVarPr l) (DVarPr r)- | l == r = return Equal-comparePred (DVarPr _) _ = return Undecidable-comparePred _ (DVarPr _) = return Undecidable-comparePred (DSigPr l t) (DSigPr r s) =- (<>) <$> compareType' t s <*> comparePred l r-comparePred (DSigPr l _) r = comparePred l r-comparePred l (DSigPr r _) = comparePred l r-comparePred (DAppPr l1 l2) (DAppPr r1 r2) = do- l2' <- expandType l2- r2' <- expandType r2- (<>) <$> comparePred l1 r1 <*> compareType' l2' r2'-comparePred (DAppPr _ _) _ = return NonEqual-comparePred (DConPr l) (DConPr r)- | l == r = return Equal- | otherwise = return NonEqual-comparePred (DConPr _) _ = return NonEqual-#if MIN_VERSION_th_desugar(1,9,0)-comparePred (DForallPr _ _ _) (DForallPr _ _ _) = return Undecidable-comparePred (DForallPr{}) _ = return NonEqual-#endif-#endif substPred :: SubstDic -> DPred -> Q DPred-#if MIN_VERSION_th_desugar(1,10,0) substPred dic (DAppT p1 p2) = DAppT <$> substPred dic p1 <*> (expandType =<< substTy dic p2)-substPred dic (DSigT p knd) = DSigT <$> substPred dic p <*> (expandType =<< substTy dic knd)+substPred dic (DSigT p knd) = DSigT <$> substPred dic p <*> (expandType =<< substTy dic knd) substPred dic prd@(DVarT p) | Just (DVarT t) <- M.lookup p dic = return $ DVarT t | Just (DConT t) <- M.lookup p dic = return $ DConT t | otherwise = return prd substPred _ t = return t-#else-substPred dic (DAppPr p1 p2) = DAppPr <$> substPred dic p1 <*> (expandType =<< substTy dic p2)-substPred dic (DSigPr p knd) = DSigPr <$> substPred dic p <*> (expandType =<< substTy dic knd)-substPred dic prd@(DVarPr p)- | Just (DVarT t) <- M.lookup p dic = return $ DVarPr t- | Just (DConT t) <- M.lookup p dic = return $ DConPr t- | otherwise = return prd-substPred _ t = return t-#endif -{- FOURMOLU_DISABLE -}-#if MIN_VERSION_th_desugar(1,12,0) dtvbToName :: DTyVarBndr flag -> Name-dtvbToName (DPlainTV n _) = n+dtvbToName (DPlainTV n _) = n dtvbToName (DKindedTV n _ _) = n-#else-dtvbToName :: DTyVarBndr -> Name-dtvbToName (DPlainTV n) = n-dtvbToName (DKindedTV n _) = n-#endif -#if MIN_VERSION_th_desugar(1,12,0) unTelescope :: DForallTelescope -> [DTyVarBndr ()] unTelescope (DForallVis vis) = map void vis unTelescope (DForallInvis vis) = map void vis-#endif
equational-reasoning.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.4 name: equational-reasoning-version: 0.7.0.3+version: 0.7.1.0 synopsis: Proof assistant for Haskell using DataKinds & PolyKinds description: A simple convenient library to write equational / preorder proof as in Agda.@@ -14,7 +14,7 @@ category: Math build-type: Simple tested-with:- ghc ==9.0.2 || ==9.2.8 || ==9.4.8 || ==9.6.5 || ==9.8.2+ ghc ==9.2.8 || ==9.4.8 || ==9.6.5 || ==9.8.4 || ==9.10.1 || ==9.12.1 extra-doc-files: Changelog.md@@ -25,6 +25,7 @@ location: git://github.com/konn/equational-reasoning-in-haskell.git library+ -- cabal-gild: discover ./Proof/**/*.hs --exclude Proof/Propositional/TH.hs exposed-modules: Proof.Equational Proof.Propositional@@ -34,10 +35,10 @@ other-modules: Proof.Propositional.TH ghc-options: -Wall build-depends:- base >=4 && <5,- containers >=0.5 && <0.7,- template-haskell >=2.11 && <2.23,- th-desugar >=1.8 && <1.18,+ base >=4.13 && <5,+ containers >=0.5 && <0.8,+ template-haskell >=2.11 && <2.24,+ th-desugar >=1.13 && <1.19, void >=0.6 && <0.8, default-language: Haskell2010