summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHiromiIshii <>2018-03-09 05:26:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2018-03-09 05:26:00 (GMT)
commit81eb66ddf2473b3a3b64d9a3dae228b0a849c988 (patch)
tree7c36232d2166c3f7301d4de9359789d8f2f8d0ef
parent8083f20f86ee77bee5fa2cd42de61666ae2f64c3 (diff)
version 0.5.1.00.5.1.0
-rw-r--r--Proof/Induction.hs58
-rw-r--r--Proof/Propositional/TH.hs75
-rw-r--r--equational-reasoning.cabal23
3 files changed, 87 insertions, 69 deletions
diff --git a/Proof/Induction.hs b/Proof/Induction.hs
index c1b4cc4..deec01f 100644
--- a/Proof/Induction.hs
+++ b/Proof/Induction.hs
@@ -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 @@ buildCase fname size dName p (nth, dCon) = do
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,29 +57,18 @@ buildCase fname size dName p (nth, dCon) = do
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
getTyConName (SigT a _) = getTyConName a
diff --git a/Proof/Propositional/TH.hs b/Proof/Propositional/TH.hs
index ab3e312..74a689d 100644
--- a/Proof/Propositional/TH.hs
+++ b/Proof/Propositional/TH.hs
@@ -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.Foldable (asum)
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 @@ buildProveClause =
(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 @@ substDCon dic (DCon forall'd cxt conName fields mPhantom) =
<*> 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 @@ 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
+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 @@ compareType' (DForallT tTvBs tCxt t) (DForallT sTvBs sCxt s)
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 @@ substPred dic prd@(DVarPr p)
| 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 29eaefb..c3639bf 100644
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -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 @@ library
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