equational-reasoning 0.5.0.0 → 0.5.1.0

raw patch · 3 files changed

+87/−69 lines, 3 filesdep +semigroupsdep ~containersdep ~singletonsdep ~template-haskellPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: semigroups

Dependency ranges changed: containers, singletons, template-haskell, th-desugar, th-extras

API changes (from Hackage documentation)

Files

• Proof/Induction.hs +23/−35
• Proof/Propositional/TH.hs +49/−26
• equational-reasoning.cabal +15/−8

@@ -1,21 +1,21 @@-{-# LANGUAGE DataKinds, FlexibleContexts, GADTs, PolyKinds, RankNTypes #-}-{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators              #-}-{-# LANGUAGE UndecidableInstances, ViewPatterns                        #-}+{-# 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.Applicative-import Control.Monad-import Data.Char-import Data.Either-import Data.List-import Data.Singletons-import Language.Haskell.TH-import Language.Haskell.TH.Lib--capitalize :: String -> String-capitalize (x :xs) = toUpper x : xs-capitalize _ = error "capitalize"+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]@@ -41,10 +41,9 @@   eparams <- forM paramTs $ \ty ->     case getTyConName ty of       Just nm | nm == dName -> Right <$> newName "t"-      _ -> Left <$> newName "a"+      _       -> Left <$> newName "a"   xs <- replicateM (length paramTs) $ newName "x"-  let freeVars = lefts eparams-      subCases = [[t| Sing $(varT t) -> $(varT p) $(varT t) |] | t <- rights eparams ]+  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@@ -58,28 +57,17 @@   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 (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+    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 _ = []+    extractParams _                        = []  toT :: TypeQ -> TypeQ -> TypeQ a `toT` b = arrowT `appT` a `appT` b--getFreeVarT :: Type -> [Name]-getFreeVarT (AppT a b) = getFreeVarT a ++ getFreeVarT b-getFreeVarT (SigT a _) = getFreeVarT a-getFreeVarT (ForallT tvs _ t) = getFreeVarT t \\ map tyVarName tvs-getFreeVarT (VarT n)   = [n]-getFreeVarT _          = []--tyVarName :: TyVarBndr -> Name-tyVarName (PlainTV n) = n-tyVarName (KindedTV n _) = n  getTyConName :: Type -> Maybe Name getTyConName (AppT a _)    = getTyConName a

@@ -1,5 +1,5 @@-{-# LANGUAGE ExplicitNamespaces, MultiWayIf, PatternGuards, TemplateHaskell #-}-{-# LANGUAGE TupleSections                                                  #-}+{-# LANGUAGE CPP, ExplicitNamespaces, MultiWayIf, PatternGuards #-}+{-# LANGUAGE TemplateHaskell, TupleSections                     #-} module Proof.Propositional.TH where import Proof.Propositional.Empty import Proof.Propositional.Inhabited@@ -10,20 +10,20 @@ import           Data.Map                    (Map) import qualified Data.Map                    as M import           Data.Maybe                  (fromJust)-import           Data.Monoid                 ((<>))+import           Data.Semigroup              (Semigroup (..)) 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)+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)   -- | Macro to automatically derive @'Empty'@ instance for@@ -110,11 +110,16 @@     (const $ const [])  fieldsVars :: DConFields -> [DType]-fieldsVars (DNormalC fs) = map snd fs-fieldsVars (DRecC fs) = map (\(_,_,c) -> c) fs+#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  resolveSubsts :: [DType] -> DInfo -> Q (DCxt, [DCon])-resolveSubsts args info = do+resolveSubsts args info =   case info of     (DTyConI (DDataD _ cxt _ tvbs dcons _) _) -> do       let dic = M.fromList $ zip (map dtvbToName tvbs) args@@ -135,12 +140,24 @@     <*> mapM (substTy dic) mPhantom  substFields :: SubstDic -> DConFields -> Q DConFields-substFields subst (DNormalC fs) = DNormalC <$> mapM (runKleisli $ second $ Kleisli $ substTy subst) fs+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 (DRecC fs) =   DRecC <$> forM fs (\(a,b,c) -> (a, b ,) <$> substTy subst c)  dtvbToName :: DTyVarBndr -> Name-dtvbToName (DPlainTV n) = n+dtvbToName (DPlainTV n)    = n dtvbToName (DKindedTV n _) = n  splitType :: DType -> Maybe ([Name], Name, [DType])@@ -157,12 +174,14 @@ 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+instance Semigroup EqlJudge where+  NonEqual    <> _        = NonEqual+  Undecidable <> NonEqual = NonEqual+  Undecidable <> _        = Undecidable+  Equal       <> m        = m +instance Monoid EqlJudge where+  mappend = (<>)   mempty = Equal  compareType :: DType -> DType -> Q EqlJudge@@ -193,7 +212,7 @@       bd <- compareType' t s'       return (pd <> bd)   | otherwise = return NonEqual-compareType' (DForallT _ _ _) _   = return NonEqual+compareType' DForallT{} _   = return NonEqual compareType' (DAppT t1 t2) (DAppT s1 s2)   = (<>) <$> compareType' t1 s1 <*> compareType' t2 s2 compareType' (DConT t) (DConT s)@@ -241,3 +260,7 @@   | Just (DConT t) <- M.lookup p dic = return $ DConPr t   | otherwise = return prd substPred _ t = return t++++

@@ -1,23 +1,31 @@ name: equational-reasoning-version: 0.5.0.0+version: 0.5.1.0 cabal-version: >=1.8 build-type: Simple license: BSD3 license-file: LICENSE-copyright: (c) Hiromi ISHII 2013-2014+copyright: (c) Hiromi ISHII 2013-2018 maintainer: konn.jinro_at_gmail.com synopsis: Proof assistant for Haskell using DataKinds & PolyKinds description:     A simple convenient library to write equational / preorder proof as in Agda. category: Math author: Hiromi ISHII-tested-with: GHC ==7.10.3 GHC ==8.0.1+tested-with: GHC ==8.0.2 GHC ==8.2.2 GHC ==8.4.1  source-repository head     type: git     location: git://github.com/konn/equational-reasoning-in-haskell.git  library+    +    if impl(ghc >=8.4)+        build-depends:+            th-desugar ==1.8.*+    else+        build-depends:+            semigroups ==0.18.*,+            th-desugar >=1.6 && <1.8     exposed-modules:         Proof.Equational         Proof.Propositional@@ -26,12 +34,11 @@         Proof.Propositional.Empty     build-depends:         base ==4.*,-        containers >=0.5,-        template-haskell >=2.11.1.0,-        th-desugar >=1.6,-        th-extras >=0.0.0.4,+        containers ==0.5.*,+        template-haskell >=2.11 && <2.14,+        th-extras ==0.0.*,         void >=0.6 && <0.8,-        singletons >=2.1 && <2.4+        singletons >=2.1 && <2.5     other-modules:         Proof.Internal.THCompat         Proof.Propositional.TH