diff --git a/Proof/Equational.hs b/Proof/Equational.hs --- a/Proof/Equational.hs +++ b/Proof/Equational.hs @@ -112,7 +112,7 @@ (===) = (=<=) {-# 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 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 @@ 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 --- 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 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 --- 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 (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 --- /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 --- /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 --- /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 --- 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 @@ 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