equational-reasoning 0.3.0.0 → 0.4.0.0

raw patch · 7 files changed

+431/−26 lines, 7 filesdep +containersdep +th-desugardep ~singletonsPVP ok

version bump matches the API change (PVP)

Dependencies added: containers, th-desugar

Dependency ranges changed: singletons

API changes (from Hackage documentation)

Files

• Proof/Equational.hs +3/−6
• Proof/Internal/THCompat.hs +7/−7
• Proof/Propositional.hs +58/−6
• Proof/Propositional/Empty.hs +59/−0
• Proof/Propositional/Inhabited.hs +51/−0
• Proof/Propositional/TH.hs +243/−0
• equational-reasoning.cabal +10/−7

@@ -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

@@ -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

@@ -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 {}

@@ -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

@@ -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

@@ -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

@@ -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