summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHiromiIshii <>2016-07-27 12:45:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2016-07-27 12:45:00 (GMT)
commitfe6c74a70e579403f01a3eb1f6ef83debb40e58f (patch)
tree63d8428e3aa029291de7ee2c96dcf569447ad895
parent7638798b0e68bebb07a6c1111b4de90b2be9fa87 (diff)
version 0.4.0.00.4.0.0
-rw-r--r--Proof/Equational.hs9
-rw-r--r--Proof/Internal/THCompat.hs14
-rw-r--r--Proof/Propositional.hs64
-rw-r--r--Proof/Propositional/Empty.hs59
-rw-r--r--Proof/Propositional/Inhabited.hs51
-rw-r--r--Proof/Propositional/TH.hs243
-rw-r--r--equational-reasoning.cabal17
7 files changed, 431 insertions, 26 deletions
diff --git a/Proof/Equational.hs b/Proof/Equational.hs
index c3099f3..adc5065 100644
--- a/Proof/Equational.hs
+++ b/Proof/Equational.hs
@@ -112,7 +112,7 @@ eq =>= (_ `Because` eq') = transitivity eq' eq
(===) = (=<=)
{-# SPECIALISE INLINE[1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
-(=~=) :: Preorder r => r x y -> Sing y -> r x y
+(=~=) :: r x y -> Sing y -> r x y
eq =~= _ = eq
start :: Preorder eq => Sing a -> eq a a
@@ -182,15 +182,12 @@ instance KnownTypeList '[] where
instance KnownTypeList ts => KnownTypeList (t ': ts) where
viewHVec' = HConsView Proxy viewHVec'
-viewHVec :: KnownTypeList ts => HVec ts -> HVecView ts
-viewHVec _ = viewHVec'
-
newtype Magic (xs :: [*]) a = Magic { _viewHVec' :: KnownTypeList xs => 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' :: (KnownTypeList ts) => HVecView ts -> (HVec ts -> c) -> ts :~> c
+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')
@@ -206,5 +203,5 @@ class FromBool (c :: *) where
type Args 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' :: 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
diff --git a/Proof/Internal/THCompat.hs b/Proof/Internal/THCompat.hs
index b801219..d923a33 100644
--- a/Proof/Internal/THCompat.hs
+++ b/Proof/Internal/THCompat.hs
@@ -1,12 +1,12 @@
{-# LANGUAGE CPP, PatternSynonyms, TemplateHaskell, ViewPatterns #-}
module Proof.Internal.THCompat where
import Language.Haskell.TH
-import Language.Haskell.TH.Syntax
+
import GHC.Exts (Constraint)
mkDataD :: Cxt -> Name -> [TyVarBndr] -> [Con] -> [Name] -> Dec
-mkDataD cxt name tvbndrs cons names =
- DataD cxt name tvbndrs
+mkDataD ctx name tvbndrs cons names =
+ DataD ctx name tvbndrs
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
Nothing cons (map ConT names)
#else
@@ -29,16 +29,16 @@ typeName PromotedConsT = '(:)
typeName ConstraintT = ''Constraint
typeName _ = error "No names!"
-pattern DataDCompat cxt name tvbndrs cons names <-
- DataD cxt name tvbndrs
+pattern DataDCompat ctx name tvbndrs cons names <-
+ DataD ctx name tvbndrs
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
_ cons (map typeName -> names)
#else
cons names
#endif
-pattern NewtypeDCompat cxt name tvbndrs con names <-
- NewtypeD cxt name tvbndrs
+pattern NewtypeDCompat ctx name tvbndrs con names <-
+ NewtypeD ctx name tvbndrs
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
_ con (map typeName -> names)
#else
diff --git a/Proof/Propositional.hs b/Proof/Propositional.hs
index 915f61e..f000e8a 100644
--- a/Proof/Propositional.hs
+++ b/Proof/Propositional.hs
@@ -1,10 +1,26 @@
-{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds, DeriveDataTypeable, EmptyCase, ExplicitForAll #-}
+{-# LANGUAGE ExplicitNamespaces, FlexibleInstances, GADTs, KindSignatures #-}
+{-# LANGUAGE LambdaCase, PolyKinds, StandaloneDeriving, 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
- ) where
+module Proof.Propositional
+ ( type (/\), type (\/), Not, exfalso, orIntroL
+ , orIntroR, orElim, andIntro, andElimL
+ , andElimR, orAssocL, orAssocR
+ , andAssocL, andAssocR, IsTrue(..)
+ , Empty(..), withEmpty, withEmpty'
+ , refute
+ , Inhabited (..), withInhabited
+ , prove
+ ) where
+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
type a /\ b = (a, b)
@@ -50,3 +66,39 @@ orAssocR :: (a \/ b) \/ c -> a \/ (b \/ c)
orAssocR (Left (Left a)) = Left a
orAssocR (Left (Right b)) = Right (Left b)
orAssocR (Right c) = Right (Right c)
+
+
+-- | Utility type to convert type-level (@'Bool'@-valued) predicate function
+-- into concrete witness data-type.
+data IsTrue (b :: Bool) where
+ Witness :: IsTrue 'True
+
+deriving instance Show (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 |]
+
+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 {}
diff --git a/Proof/Propositional/Empty.hs b/Proof/Propositional/Empty.hs
new file mode 100644
index 0000000..652f8b8
--- /dev/null
+++ b/Proof/Propositional/Empty.hs
@@ -0,0 +1,59 @@
+{-# 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)
+import GHC.Generics
+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.
+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
+ 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
+ geliminate (K1 a) = eliminate a
+
+instance GEmpty V1 where
+ geliminate = \ case {}
+
+deriving instance (Empty a, Empty b) => Empty (Either a b)
+deriving instance Empty Void
+
+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
+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
+withEmpty' neg k = unsafeCoerce (MagicEmpty k :: MagicEmpty a b) neg
diff --git a/Proof/Propositional/Inhabited.hs b/Proof/Propositional/Inhabited.hs
new file mode 100644
index 0000000..a44c6e0
--- /dev/null
+++ b/Proof/Propositional/Inhabited.hs
@@ -0,0 +1,51 @@
+{-# 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
+import GHC.Generics
+import Unsafe.Coerce (unsafeCoerce)
+
+-- | Types with at least one inhabitant, dual to @'Proof.Propositional.Empty'@.
+-- | Current GHC doesn't provide selective-instance,
+-- hence we don't @'Empty'@ provide instances
+-- for sum types in a generic deriving (DeriveAnyClass).
+--
+-- To derive an instance for each concrete types,
+-- use @'Proof.Propositional.prove'@.
+--
+-- Since 0.4.0.0.
+class Inhabited a where
+ 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
+ gtrivial = M1 gtrivial
+
+instance (GInhabited f, GInhabited g) => GInhabited (f :*: g) where
+ gtrivial = gtrivial :*: gtrivial
+
+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
+ trivial = const trivial
+
+newtype MagicInhabited a b = MagicInhabited (Inhabited a => b)
+
+withInhabited :: forall a b. a -> (Inhabited a => b) -> b
+withInhabited wit k = unsafeCoerce (MagicInhabited k :: MagicInhabited a b) wit
diff --git a/Proof/Propositional/TH.hs b/Proof/Propositional/TH.hs
new file mode 100644
index 0000000..ab3e312
--- /dev/null
+++ b/Proof/Propositional/TH.hs
@@ -0,0 +1,243 @@
+{-# LANGUAGE ExplicitNamespaces, MultiWayIf, PatternGuards, TemplateHaskell #-}
+{-# LANGUAGE TupleSections #-}
+module Proof.Propositional.TH where
+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.Monoid ((<>))
+import Data.Type.Equality ((:~:) (..))
+import Language.Haskell.TH (DecsQ, Lit (CharL, IntegerL))
+import Language.Haskell.TH (Name, Q, TypeQ, isInstance)
+import Language.Haskell.TH (newName, ppr)
+import Language.Haskell.TH.Desugar (DClause (..), DCon (..))
+import Language.Haskell.TH.Desugar (DConFields (..), DCxt, DDec (..))
+import Language.Haskell.TH.Desugar (DExp (..), DInfo (..))
+import Language.Haskell.TH.Desugar (DLetDec (DFunD))
+import Language.Haskell.TH.Desugar (DPat (DConPa, DVarPa), DPred (..))
+import Language.Haskell.TH.Desugar (DTyVarBndr (..), DType (..))
+import Language.Haskell.TH.Desugar (Overlap (Overlapping), desugar)
+import Language.Haskell.TH.Desugar (dsReify, expandType, substTy)
+import Language.Haskell.TH.Desugar (sweeten)
+
+
+-- | 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]
+ ]
+ if tyName == ''(:~:)
+ then do
+ let [l, r] = args
+ 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)
+ 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.
+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]
+ ]
+ isNum <- isInstance ''Num [sweeten tp]
+
+ 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
+ (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 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
+
+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])
+
+buildProveClause :: DCon -> Q (Maybe DClause)
+buildProveClause =
+ buildClause
+ ''Inhabited (const $ return ())
+ (const $ const $ DVarE 'trivial)
+ (\ con args -> foldl DAppE (DConE con) <$> sequence args )
+ (const $ const [])
+
+fieldsVars :: DConFields -> [DType]
+fieldsVars (DNormalC fs) = map snd fs
+fieldsVars (DRecC fs) = map (\(_,_,c) -> c) fs
+
+resolveSubsts :: [DType] -> DInfo -> Q (DCxt, [DCon])
+resolveSubsts args info = do
+ case info of
+ (DTyConI (DDataD _ cxt _ tvbs dcons _) _) -> do
+ let dic = M.fromList $ zip (map dtvbToName tvbs) args
+ (cxt , ) <$> mapM (substDCon dic) dcons
+ -- (DTyConI (DOpenTypeFamilyD n) _) -> return []
+ -- (DTyConI (DClosedTypeFamilyD _ ddec2) minst) -> return []
+ -- (DTyConI (DDataFamilyD _ ddec2) minst) -> return []
+ -- (DTyConI (DDataInstD _ ddec2 ddec3 ddec4 ddec5 ddec6) minst) -> return []
+ (DTyConI _ _) -> fail "Not supported data ty"
+ _ -> fail "Please pass data-type"
+
+type SubstDic = Map Name DType
+
+substDCon :: SubstDic -> DCon -> Q DCon
+substDCon dic (DCon forall'd cxt conName fields mPhantom) =
+ DCon forall'd cxt conName
+ <$> substFields dic fields
+ <*> mapM (substTy dic) mPhantom
+
+substFields :: SubstDic -> DConFields -> Q DConFields
+substFields subst (DNormalC fs) = DNormalC <$> 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
+
+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 (DSigT t _) = splitType t
+splitType (DVarT _) = Nothing
+splitType (DConT n) = Just ([], n, [])
+splitType DArrowT = Just ([], ''(->), [])
+splitType (DLitT _) = Nothing
+splitType DWildCardT = Nothing
+splitType DStarT = Nothing
+
+data EqlJudge = NonEqual | Undecidable | Equal
+ deriving (Read, Show, Eq, Ord)
+
+instance Monoid EqlJudge where
+ NonEqual `mappend` _ = NonEqual
+ Undecidable `mappend` NonEqual = NonEqual
+ Undecidable `mappend` _ = Undecidable
+ Equal `mappend` m = m
+
+ mempty = Equal
+
+compareType :: DType -> DType -> Q EqlJudge
+compareType t0 s0 = do
+ t <- expandType t0
+ s <- expandType s0
+ 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' (DVarT t) (DVarT s)
+ | 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)
+ | 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
+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
+ | 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
+ | otherwise = return NonEqual
+compareType' (DLitT _) _ = return NonEqual
+compareType' DStarT DStarT = return NonEqual
+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)
+ | 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
+
+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
+ | otherwise = return prd
+substPred _ t = return t
diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal
index 5f11b68..ab1ed0d 100644
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -2,7 +2,7 @@
-- documentation, see http://haskell.org/cabal/users-guide/
name: equational-reasoning
-version: 0.3.0.0
+version: 0.4.0.0
synopsis: Proof assistant for Haskell using DataKinds & PolyKinds
description: A simple convenient library to write equational / preorder proof as in Agda.
license: BSD3
@@ -21,11 +21,14 @@ source-repository head
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
- , void >= 0.6 && < 0.8
- , template-haskell
- if impl(ghc < 7.10)
- build-depends: singletons >= 0.8 && < 1.2
- else
- build-depends: singletons >= 2.1 && < 2.3
+ , containers >= 0.5
+ , template-haskell
+ , th-desugar >= 1.6
+ , void >= 0.6 && < 0.8
+ build-depends: singletons >= 2.1 && < 2.3