equational-reasoning 0.5.1.1 → 0.7.1.0
raw patch · 10 files changed
Files
- Changelog.md +25/−0
- Proof/Equational.hs +147/−99
- Proof/Induction.hs +0/−82
- Proof/Internal/THCompat.hs +0/−87
- Proof/Propositional.hs +92/−61
- Proof/Propositional/Empty.hs +48/−32
- Proof/Propositional/Inhabited.hs +37/−21
- Proof/Propositional/TH.hs +185/−148
- README.md +30/−0
- equational-reasoning.cabal +39/−34
+ Changelog.md view
@@ -0,0 +1,25 @@+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+- Drops support for GHC <9++## 0.6.0.3++- Support for GHC >= 8.10++## 0.6.0.2++- Adds support for th-desugar-1.11++## 0.6.0.1++- Supports GHC 8.8.+- Adds support for th-desugar-1.10 (Thanks: Justin Le @mstksg)
Proof/Equational.hs view
@@ -1,72 +1,117 @@-{-# LANGUAGE CPP, DataKinds, FlexibleContexts, GADTs, KindSignatures #-}-{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving, TypeFamilies, TypeOperators #-}-{-# LANGUAGE TypeSynonymInstances, UndecidableInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-}+ #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'- -- * Conversion between equalities- , fromRefl, fromLeibniz, reflToLeibniz, leibnizToRefl- -- * Coercion- , coerce, coerce', withRefl- -- * Re-exported modules- , module Data.Singletons, module Data.Proxy- ) where+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,++ -- * Coercion+ coerce,+ coerceInner,+ coerce',+ withRefl,++ -- * Re-exported modules+ module Data.Proxy,+) where++import Data.Kind (Type) import Data.Proxy-import Data.Singletons import Data.Type.Equality hiding (apply) import Unsafe.Coerce infix 4 :=:+ type a :\/: b = Either a b+ infixr 2 :\/: type a :/\: b = (a, b)+ infixr 3 :/\: type (:=:) = (:~:) -data Leibniz a b = Leibniz { apply :: forall f. f a -> f b }+data Leibniz a b = Leibniz {apply :: forall f. f a -> f b} leibnizToRefl :: Leibniz a b -> a :=: b leibnizToRefl eq = apply eq Refl -fromLeibniz :: (Preorder eq, SingI a) => Leibniz a b -> eq a b-fromLeibniz eq = apply eq (reflexivity sing)+fromLeibniz :: (Preorder eq) => Leibniz a b -> eq a b+fromLeibniz eq = apply eq (reflexivity Proxy) -fromRefl :: (Preorder eq, SingI b) => a :=: b -> eq a b+fromRefl :: (Preorder eq) => a :=: b -> eq a b fromRefl Refl = reflexivity' reflToLeibniz :: a :=: b -> Leibniz a b reflToLeibniz Refl = Leibniz id -class Preorder (eq :: k -> k -> *) where- reflexivity :: Sing a -> eq a a- transitivity :: eq a b -> eq b c -> eq a c+class Preorder (eq :: k -> k -> Type) where+ reflexivity :: proxy a -> eq a a+ transitivity :: eq a b -> eq b c -> eq a c -class Preorder eq => Equality (eq :: k -> k -> *) where- symmetry :: eq a b -> eq b a+class (Preorder eq) => Equality (eq :: k -> k -> Type) where+ symmetry :: eq a b -> eq b a instance Preorder (:=:) where- {-# SPECIALISE instance Preorder (:=:) #-}+ {-# SPECIALIZE instance Preorder (:=:) #-} transitivity Refl Refl = Refl- {-# INLINE[1] transitivity #-}+ {-# INLINE [1] transitivity #-} - reflexivity _ = Refl- {-# INLINE[1] reflexivity #-}+ reflexivity _ = Refl+ {-# INLINE [1] reflexivity #-} instance Equality (:=:) where- {-# SPECIALISE instance Equality (:~:) #-}- symmetry Refl = Refl- {-# INLINE[1] symmetry #-}+ {-# SPECIALIZE instance Equality (:~:) #-}+ symmetry Refl = Refl+ {-# INLINE [1] symmetry #-} instance Preorder (->) where reflexivity _ = id@@ -80,46 +125,46 @@ transitivity (Leibniz aEqb) (Leibniz bEqc) = Leibniz $ bEqc . aEqb instance Equality Leibniz where- symmetry eq = unFlip $ apply eq $ Flip leibniz_refl+ symmetry eq = unFlip $ apply eq $ Flip leibniz_refl -newtype Flip f a b = Flip { unFlip :: f b a }+newtype Flip f a b = Flip {unFlip :: f b a} data Reason eq x y where- Because :: Sing y -> eq x y -> Reason eq x y+ Because :: proxy y -> eq x y -> Reason eq x y -reflexivity' :: (SingI x, Preorder r) => r x x-reflexivity' = reflexivity sing+reflexivity' :: (Preorder r) => r x x+reflexivity' = reflexivity Proxy -by, because :: Sing y -> eq x y -> Reason eq x y+by, because :: proxy y -> eq x y -> Reason eq x y because = Because-by = Because+by = Because infixl 4 ===, =<=, =~=, =>=+ infix 5 `Because`+ 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'--{-# SPECIALISE INLINE[1] (=<=) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}+{-# 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--{-# SPECIALISE INLINE[1] (=>=) :: y :~: z -> Reason (:~:) x y -> x :~: z #-}+{-# 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 (===) = (=<=)-{-# SPECIALISE INLINE[1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}+{-# SPECIALIZE INLINE [1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-} -(=~=) :: r x y -> Sing y -> r x y+(=~=) :: r x y -> proxy y -> r x y eq =~= _ = eq -start :: Preorder eq => Sing a -> eq a a+start :: (Preorder eq) => proxy a -> eq a a start = reflexivity -byDefinition :: (SingI a, Preorder eq) => eq a a-byDefinition = reflexivity sing+byDefinition :: (Preorder eq) => eq a a+byDefinition = reflexivity Proxy admitted :: Reason eq x y admitted = undefined@@ -128,92 +173,95 @@ cong :: forall f a b. Proxy f -> a :=: b -> f a :=: f b cong Proxy Refl = Refl -cong' :: (Sing m -> Sing (f m)) -> a :=: b -> f a :=: f b-cong' _ Refl = Refl+cong' :: (pxy m -> pxy (f m)) -> a :=: b -> f a :=: f b+cong' _ Refl = Refl --- | Type coercion. 'coerce' is using @unsafeCoerce a@.--- So, please, please do not provide the @undefined@ as the proof.--- Using this function instead of pattern-matching on equality proof,--- you can reduce the overhead introduced by run-time proof.-coerce :: (a :=: b) -> f a -> f b-coerce _ a = unsafeCoerce a-{-# INLINE[1] coerce #-}+{- | Type coercion. 'coerce' is using @unsafeCoerce a@.+ So, please, please do not provide the @undefined@ as the proof.+ Using this function instead of pattern-matching on equality proof,+ you can reduce the overhead introduced by run-time proof.+-}+coerceInner, coerce :: (a :=: b) -> f a -> f b+{-# DEPRECATED coerce "Use coerceInner instead" #-}+coerce = coerceInner+{-# INLINE coerce #-}+coerceInner _ = unsafeCoerce+{-# INLINE [1] coerceInner #-} -- | Coercion for identity types. coerce' :: a :=: b -> a -> b-coerce' _ a = unsafeCoerce a-{-# INLINE[1] coerce' #-}+coerce' _ = unsafeCoerce+{-# INLINE [1] coerce' #-} {-# RULES "coerce/unsafeCoerce" [~1] forall xs.- coerce xs = unsafeCoerce+ coerceInner xs =+ unsafeCoerce "coerce'/unsafeCoerce" [~1] forall xs.- coerce' xs = unsafeCoerce+ coerce' xs =+ unsafeCoerce #-} --- | Solves equality constraint without explicit coercion.--- 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 _ r = case unsafeCoerce (Refl :: () :~: ()) :: a :~: b of- Refl -> r-{-# NOINLINE withRefl #-}-{-# RULES-"withRefl/unsafeCoerce" [~1] forall x.- withRefl x = unsafeCoerce- #-}+{- | Solves equality constraint without explicit coercion.+ 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 _ = gcastWith (unsafeCoerce (Refl :: () :~: ()) :: a :~: b) -class Proposition (f :: k -> *) where- type OriginalProp (f :: k -> *) (n :: k) :: *+class Proposition (f :: k -> Type) where+ type OriginalProp (f :: k -> Type) (n :: k) :: Type unWrap :: f n -> OriginalProp f n- wrap :: OriginalProp f n -> f n+ wrap :: OriginalProp f n -> f n -data HVec (xs :: [*]) where+data HVec (xs :: [Type]) where HNil :: HVec '[] (:-) :: x -> HVec xs -> HVec (x ': xs) infixr 9 :--type family (xs :: [*]) :~> (a :: *) :: * where- '[] :~> a = a++type family (xs :: [Type]) :~> (a :: Type) :: Type where+ '[] :~> a = a (x ': xs) :~> a = x -> (xs :~> a) infixr 1 :~> -data HVecView (xs :: [*]) :: * where- HNilView :: HVecView '[]+data HVecView (xs :: [Type]) :: Type where+ HNilView :: HVecView '[] HConsView :: Proxy t -> HVecView ts -> HVecView (t ': ts) deriving instance Show (HVecView xs) -class KnownTypeList (xs :: [*]) where+class KnownTypeList (xs :: [Type]) where viewHVec' :: HVecView xs 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 :: [*]) 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 apply' HNilView f = f HNil-apply' (HConsView Proxy ts) f = \a -> withKnownTypeList ts $- apply' ts (\ts' -> f $ a :- ts')+apply' (HConsView Proxy ts) f = \a ->+ 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 :: *) where+class FromBool (c :: Type) where type Predicate c :: Bool- type Args c :: [*]- fromBool :: Predicate c ~ 'True => HVec (Args c) -> c+ type Args c :: [Type]+ 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' :: 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/Induction.hs
@@ -1,82 +0,0 @@-{-# LANGUAGE DataKinds, ExplicitNamespaces, FlexibleContexts, GADTs #-}-{-# LANGUAGE PolyKinds, RankNTypes, TemplateHaskell, TypeFamilies #-}-{-# LANGUAGE TypeOperators, UndecidableInstances, ViewPatterns #-}-module Proof.Induction (genInduction) where-import Proof.Internal.THCompat--import Control.Monad (forM, replicateM)-import Data.Either (rights)-import Data.Singletons (Sing)-import Language.Haskell.TH (Clause, Con (ForallC, InfixC, NormalC, RecC))-import Language.Haskell.TH (TypeQ, appT, appT, appsE, appsE, arrowT, arrowT)-import Language.Haskell.TH (clause, clause, conP, conP, cxt, cxt, forallT)-import Language.Haskell.TH (funD, funD, mkName, nameBase, newName)-import Language.Haskell.TH (normalB, normalB, promotedT, promotedT, reify)-import Language.Haskell.TH (sigD, sigD, varE, varE, varP, varP, varT, varT)-import Language.Haskell.TH (Dec, Info (TyConI), Name, Q)-import Language.Haskell.TH (Type (AppT, ConT, PromotedT, SigT))-import Language.Haskell.TH.Lib (plainTV)---- | @genInduction ''Type "inductionT"@ defines the induction scheme for @Type@ named @inductionT@.-genInduction :: Name -> String -> Q [Dec]-genInduction typ fname0 = do- let fname = mkName fname0- TyConI (normalizeDec -> DataDCompat _ dName _ dCons _) <- reify typ- p <- newName "p"- ans <- mapM (buildCase fname (length dCons) dName p) $ zip [0..] dCons- let (cls, ts) = unzip ans- t <- newName "t"- sig <- sigD fname $ forallT [plainTV p, plainTV t] (cxt []) $- foldr toT ([t| Sing $(varT t) -> $(varT p) $(varT t) |]) $ map return ts- dec <- funD fname (map return cls)- return [sig, dec]--buildCase :: Name -> Int -> Name -> Name -> (Int, Con) -> Q (Clause, Type)-buildCase _ _ _ _ (_, ForallC _ _ _) = error "Existential types are not supported yet."-buildCase fname size dName p (nth, dCon) = do- let paramTs = extractParams dCon- conName = extractName dCon- sName = mkName $ 'S' : nameBase conName- ssName = mkName $ 's' : nameBase conName- eparams <- forM paramTs $ \ty ->- case getTyConName ty of- Just nm | nm == dName -> Right <$> newName "t"- _ -> Left <$> newName "a"- xs <- replicateM (length paramTs) $ newName "x"- let subCases = [[t| Sing $(varT t) -> $(varT p) $(varT t) |] | t <- rights eparams ]- params <- mapM (either varT varT) eparams- let promCon = foldl appT (promotedT conName) (map return params)- tbdy | null subCases = foldr toT ([t| $(varT p `appT` promCon) |]) subCases- | otherwise = foldr toT ([t| Sing $(promCon) -> $(varT p `appT` promCon) |]) subCases- sig <- if null params then tbdy else forallT (map (either plainTV plainTV) eparams) (cxt []) tbdy- cs <- replicateM size $ newName "case"- let body | null subCases = varE (cs !! nth)- | otherwise = appsE $ varE (cs !! nth) :- replicate (length subCases) (appsE $ varE fname : map varE cs)- ++ [ appsE (varE ssName : map varE xs)]- cl <- clause (map varP cs ++ [conP sName $ map varP xs]) (normalB body) []- return (cl, sig)- where- extractName (NormalC n _) = n- extractName (RecC n _) = n- extractName (InfixC _ n _) = n- extractName _ = error "I don't know name!"- extractParams (NormalC _ sts) = map snd sts- extractParams (RecC _ vsts) = map (\(_,_,c) -> c) vsts- extractParams (InfixC (_, t) _ (_, s)) = [t,s]- extractParams _ = []--toT :: TypeQ -> TypeQ -> TypeQ-a `toT` b = arrowT `appT` a `appT` b--getTyConName :: Type -> Maybe Name-getTyConName (AppT a _) = getTyConName a-getTyConName (SigT a _) = getTyConName a-getTyConName (ConT nam) = Just nam-getTyConName (PromotedT n) = Just n-getTyConName _ = Nothing--normalizeDec :: Dec -> Dec-normalizeDec d@DataDCompat {} = d-normalizeDec (NewtypeDCompat ctx name tvbs con names) = mkDataD ctx name tvbs [con] names-normalizeDec _ = error "not data definition."
− Proof/Internal/THCompat.hs
@@ -1,87 +0,0 @@-{-# LANGUAGE CPP, PatternSynonyms, TemplateHaskell, ViewPatterns #-}-{-# LANGUAGE DeriveDataTypeable, DeriveGeneric #-}-module Proof.Internal.THCompat where-import Language.Haskell.TH-import Language.Haskell.TH.Extras--import GHC.Exts (Constraint)--#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 802-import GHC.Generics-import Data.Data-#endif--#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 802-data DerivClause = DerivClause (Maybe DerivStrategy) Cxt- deriving (Eq, Data, Ord, Show, Generic)-data DerivStrategy = StockStrategy- | AnyclassStrategy- | NewtypeStrategy- deriving (Eq, Data, Ord, Show, Generic)-#endif--dcToNames :: DerivClause -> [Name]-dcToNames (DerivClause _ ct) = map headOfType ct--dcToCxt :: DerivClause -> Cxt-dcToCxt (DerivClause _ ct) = ct---mkDataD :: Cxt -> Name -> [TyVarBndr] -> [Con] -> [DerivClause] -> Dec-mkDataD ctx name tvbndrs cons dc =- DataD ctx name tvbndrs-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800- Nothing cons -#if __GLASGOW_HASKELL__ < 802- (concatMap dcToCxt dc)-#else- dc-#endif-#else- cons (concatMap dcToNames dc)-#endif---typeName :: Type -> Name-typeName (VarT n) = n-typeName (ConT n) = n-typeName (PromotedT n) = n-typeName (TupleT n) = tupleTypeName n-typeName (UnboxedTupleT n) = unboxedTupleTypeName n-typeName ArrowT = ''(->)-typeName EqualityT = ''(~)-typeName ListT = ''[]-typeName (PromotedTupleT n) = tupleDataName n-typeName PromotedNilT = '[]-typeName PromotedConsT = '(:)-typeName ConstraintT = ''Constraint-typeName _ = error "No names!"--pattern DataDCompat :: Cxt -> Name -> [TyVarBndr] -> [Con] -> [DerivClause] -> Dec-pattern DataDCompat ctx name tvbndrs cons dcs <-- DataD ctx name tvbndrs-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800- _ cons -#if __GLASGOW_HASKELL__ < 802- (pure . DerivClause Nothing -> dcs)-#else - dcs-#endif-#else- cons (DerivClause Nothing . map ConT -> dc)-#endif--pattern NewtypeDCompat :: Cxt -> Name -> [TyVarBndr] -> Con -> [DerivClause] -> Dec-pattern NewtypeDCompat ctx name tvbndrs con dcs <-- NewtypeD ctx name tvbndrs-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800- _ con-#if __GLASGOW_HASKELL__ < 802- (pure . DerivClause Nothing -> dcs)-#else- dcs-#endif-#else- con- (DerivClause Nothing . map ConT -> dcs)-#endif
Proof/Propositional.hs view
@@ -1,34 +1,64 @@-{-# LANGUAGE DataKinds, DeriveDataTypeable, EmptyCase, ExplicitForAll #-}-{-# LANGUAGE ExplicitNamespaces, FlexibleInstances, GADTs, KindSignatures #-}-{-# LANGUAGE LambdaCase, PolyKinds, RankNTypes, StandaloneDeriving #-}-{-# LANGUAGE TemplateHaskell, TypeOperators #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE ExplicitForAll #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeOperators #-} {-# 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, (:~:) (..))+import Data.Typeable (Typeable)+import Data.Void import Proof.Propositional.Empty import Proof.Propositional.Inhabited import Proof.Propositional.TH--import Data.Data (Data)-import Data.Type.Equality ((:~:))-import Data.Typeable (Typeable)-import Data.Void import Unsafe.Coerce type a /\ b = (a, b)+ type a \/ b = Either a b-type Not a = a -> Void +type Not a = a -> Void+ infixr 2 \/+ infixr 3 /\ exfalso :: a -> Not a -> b@@ -53,69 +83,70 @@ andElimR = snd andAssocL :: a /\ (b /\ c) -> (a /\ b) /\ c-andAssocL (a,(b,c)) = ((a,b), c)+andAssocL (a, (b, c)) = ((a, b), c) andAssocR :: (a /\ b) /\ c -> a /\ (b /\ c)-andAssocR ((a,b),c) = (a,(b,c))+andAssocR ((a, b), c) = (a, (b, c)) orAssocL :: a \/ (b \/ c) -> (a \/ b) \/ c-orAssocL (Left a) = Left (Left a)-orAssocL (Right (Left b)) = Left (Right b)+orAssocL (Left a) = Left (Left a)+orAssocL (Right (Left b)) = Left (Right b) orAssocL (Right (Right c)) = Right c orAssocR :: (a \/ b) \/ c -> a \/ (b \/ c)-orAssocR (Left (Left a)) = Left a+orAssocR (Left (Left a)) = Left a orAssocR (Left (Right b)) = Right (Left b)-orAssocR (Right c) = Right (Right c)-+orAssocR (Right c) = Right (Right c) --- | Utility type to convert type-level (@'Bool'@-valued) predicate function--- into concrete witness data-type.+{- | Utility type to convert type-level (@'Bool'@-valued) predicate function+ into concrete witness data-type.+-} data IsTrue (b :: Bool) where Witness :: IsTrue 'True -withWitness :: IsTrue b -> (b ~ 'True => r) -> r-withWitness Witness r = r+withWitness :: forall b r. IsTrue b -> ((b ~ 'True) => r) -> r+withWitness _ = gcastWith (unsafeCoerce (Refl :: () :~: ()) :: b :~: 'True) {-# NOINLINE withWitness #-}-{-# RULES-"withWitness/coercion" [~1] forall x.- withWitness x = unsafeCoerce- #-} deriving instance Show (IsTrue b)-deriving instance Eq (IsTrue b)-deriving instance Ord (IsTrue b)++deriving instance Eq (IsTrue b)++deriving instance Ord (IsTrue b)+ deriving instance Read (IsTrue 'True)+ deriving instance Typeable IsTrue+ deriving instance Data (IsTrue 'True) instance {-# OVERLAPPABLE #-} (Inhabited a, Empty b) => Empty (a -> b) where eliminate f = eliminate (f trivial) -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|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|] -prove [t| Bool |]-prove [t| Int |]-prove [t| Integer |]-prove [t| Word |]-prove [t| Double |]-prove [t| Float |]-prove [t| Char |]-prove [t| Ordering |]-prove [t| forall a. [a] |]-prove [t| Rational |]-prove [t| forall a. Maybe a |]-prove [t| forall n. n :~: n |]-prove [t| IsTrue 'True |]+prove [t|Bool|]+prove [t|Int|]+prove [t|Integer|]+prove [t|Word|]+prove [t|Double|]+prove [t|Float|]+prove [t|Char|]+prove [t|Ordering|]+prove [t|forall a. [a]|]+prove [t|Rational|]+prove [t|forall a. Maybe a|]+prove [t|forall n. n :~: n|]+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,132 +1,182 @@-{-# LANGUAGE CPP, ExplicitNamespaces, MultiWayIf, PatternGuards #-}-{-# LANGUAGE TemplateHaskell, TupleSections #-}+{-# 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.Semigroup (Semigroup (..))-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),- DPat (DConPa, DVarPa), DPred (..),- DTyVarBndr (..), DType (..),- Overlap (Overlapping), desugar,- dsReify, expandType, substTy,- sweeten)+#if MIN_VERSION_th_desugar(1,18,0)+import Language.Haskell.TH.Desugar (dLamE, dCaseE)+#else+import Language.Haskell.TH.Desugar (DMatch)+#endif --- | Macro to automatically derive @'Empty'@ instance for--- concrete (variable-free) types which may contain products.+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.+-} refute :: TypeQ -> DecsQ refute tps = do tp <- expandType =<< desugar =<< tps let Just (_, tyName, args) = splitType tp- mkInst dxt cls = return $ sweeten- [DInstanceD (Just Overlapping) 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) 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)- (\cName ps -> [DConPa cName $ map DVarPa ps])+ ''Empty+ (const $ newName "_x")+ (const $ (DVarE 'eliminate `DAppE`) . DVarE)+ (const asum)+ (\cName ps -> [DConP cName [] $ map DVarP ps]) 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 defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 804-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 []@@ -140,55 +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 defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 804- (DNormalC fs)-#else- (DNormalC fixi fs)-#endif- =-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 804- DNormalC <$>-#else- DNormalC fixi <$>-#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)--dtvbToName :: DTyVarBndr -> Name-dtvbToName (DPlainTV n) = n-dtvbToName (DKindedTV n _) = n+ DRecC <$> forM fs (\(a, b, c) -> (a,b,) <$> substTy subst c) splitType :: DType -> Maybe ([Name], Name, [DType])-splitType (DForallT 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 (DConstrainedT _ t) = splitType t+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-#endif-+splitType (DAppKindT _ _) = Nothing 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 = (<>)@@ -201,82 +234,86 @@ 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-compareType' (DForallT tTvBs tCxt t) (DForallT sTvBs sCxt s)+compareType' (DConstrainedT tCxt t) (DConstrainedT sCxt s) = do+ pd <- compareCxt tCxt sCxt+ bd <- compareType' t s+ return (pd <> bd)+compareType' DConstrainedT {} _ = return NonEqual+compareType' (DForallT (unTelescope -> tTvBs) t) (DForallT (unTelescope -> sTvBs) 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)+ return bd | otherwise = return NonEqual-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-comparePred DWildCardPr _ = return Undecidable-comparePred _ DWildCardPr = return Undecidable-comparePred (DVarPr l) (DVarPr r)+comparePred DWildCardT _ = return Undecidable+comparePred _ DWildCardT = return Undecidable+comparePred (DVarT l) (DVarT r) | l == r = return Equal-comparePred (DVarPr _) _ = return Undecidable-comparePred _ (DVarPr _) = return Undecidable-comparePred (DSigPr l t) (DSigPr r s) =+comparePred (DVarT _) _ = return Undecidable+comparePred _ (DVarT _) = return Undecidable+comparePred (DSigT l t) (DSigT 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+comparePred (DSigT l _) r = comparePred l r+comparePred l (DSigT r _) = comparePred l r+comparePred (DAppT l1 l2) (DAppT r1 r2) = do l2' <- expandType l2 r2' <- expandType r2 (<>) <$> comparePred l1 r1 <*> compareType' l2' r2'-comparePred (DAppPr _ _) _ = return NonEqual-comparePred (DConPr l) (DConPr r)+comparePred (DAppT _ _) _ = return NonEqual+comparePred (DConT l) (DConT 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+comparePred (DConT _) _ = return NonEqual+comparePred (DForallT _ _) (DForallT _ _) = return Undecidable+comparePred (DForallT {}) _ = return NonEqual+comparePred _ _ = fail "Kind error: Expecting type-level predicate" substPred :: SubstDic -> DPred -> Q DPred-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+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 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 --+dtvbToName :: DTyVarBndr flag -> Name+dtvbToName (DPlainTV n _) = n+dtvbToName (DKindedTV n _ _) = n +unTelescope :: DForallTelescope -> [DTyVarBndr ()]+unTelescope (DForallVis vis) = map void vis+unTelescope (DForallInvis vis) = map void vis
+ README.md view
@@ -0,0 +1,30 @@+Agda-style Equational Reasoning in Haskell by Data Kinds+=========================================================+[](https://travis-ci.org/konn/equational-reasoning-in-haskell) [](https://hackage.haskell.org/package/equational-reasoning)++What is this?+--------------+This library provides means to prove equations in Haskell.+You can prove equations in Agda's EqReasoning like style.++See blow for an example:++```haskell+plusZeroL :: SNat m -> Zero :+: m :=: m+plusZeroL SZero = Refl+plusZeroL (SSucc m) =+ start (SZero %+ (SSucc m))+ === SSucc (SZero %+ m) `because` plusSuccR SZero m+ === SSucc m `because` succCongEq (plusZeroL m)++```++It also provides some utility functions to use an induction.++For more detail, please read source codes!+++TODOs+------++* Automatic generation for induction schema for any inductive types.
equational-reasoning.cabal view
@@ -1,39 +1,44 @@--- Initial equational-reasoning.cabal generated by cabal init. For further--- documentation, see http://haskell.org/cabal/users-guide/+cabal-version: 3.4+name: equational-reasoning+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.+ Since 0.6.0.0, this no longer depends on @singletons@ package, and the @Proof.Induction@ module goes to @equational-reasoning-induction@ package. -name: equational-reasoning-version: 0.5.1.1-synopsis: Proof assistant for Haskell using DataKinds & PolyKinds-description: A simple convenient library to write equational / preorder proof as in Agda.-license: BSD3-license-file: LICENSE-author: Hiromi ISHII-maintainer: konn.jinro_at_gmail.com-copyright: (c) Hiromi ISHII 2013-2018-category: Math-build-type: Simple-tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.1, GHC == 8.6.3-cabal-version: >=1.8+license: BSD-3-Clause+license-file: LICENSE+author: Hiromi ISHII+maintainer: konn.jinro_at_gmail.com+copyright: (c) Hiromi ISHII 2013-2020+category: Math+build-type: Simple+tested-with:+ ghc ==9.2.8 || ==9.4.8 || ==9.6.5 || ==9.8.4 || ==9.10.1 || ==9.12.1 +extra-doc-files:+ Changelog.md+ README.md+ source-repository head- type: git- location: git://github.com/konn/equational-reasoning-in-haskell.git+ type: git+ location: git://github.com/konn/equational-reasoning-in-haskell.git library- exposed-modules: Proof.Equational, Proof.Propositional, Proof.Induction- , Proof.Propositional.Inhabited- , Proof.Propositional.Empty- other-modules: Proof.Internal.THCompat- , Proof.Propositional.TH- ghc-options: -Wall- build-depends: base >= 4 && < 5- , containers >= 0.5 && < 0.7- , template-haskell >= 2.11 && < 2.16- , th-extras == 0.0.*- , void >= 0.6 && < 0.8- , singletons >= 2.1 && < 2.6- if impl(ghc >= 8.4)- build-depends: th-desugar >= 1.6 && < 1.11- else- build-depends: semigroups == 0.18.*- build-depends: th-desugar >= 1.6 && < 1.11+ -- cabal-gild: discover ./Proof/**/*.hs --exclude Proof/Propositional/TH.hs+ exposed-modules:+ Proof.Equational+ Proof.Propositional+ Proof.Propositional.Empty+ Proof.Propositional.Inhabited++ other-modules: Proof.Propositional.TH+ ghc-options: -Wall+ build-depends:+ 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