equational-reasoning 0.2.0.7 → 0.3.0.0

raw patch · 4 files changed

+117/−71 lines, 4 filesdep −taggeddep ~singletonsdep ~template-haskellPVP ok

version bump matches the API change (PVP)

Dependencies removed: tagged

Dependency ranges changed: singletons, template-haskell

API changes (from Hackage documentation)

Files

• Proof/Equational.hs +58/−55
• Proof/Induction.hs +6/−4
• Proof/Internal/THCompat.hs +46/−0
• equational-reasoning.cabal +7/−12

@@ -1,18 +1,18 @@-{-# LANGUAGE CPP, DataKinds, FlexibleContexts, GADTs, PolyKinds, RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TypeFamilies          #-}-{-# LANGUAGE TypeOperators, TypeSynonymInstances, KindSignatures            #-}-module Proof.Equational (-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707-                         (:~:)(..), (:=:)-#else-                         (:=:)(..), (:~:)+{-# LANGUAGE CPP, DataKinds, FlexibleContexts, GADTs, KindSignatures #-}+{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables              #-}+{-# LANGUAGE StandaloneDeriving, TypeFamilies, TypeOperators         #-}+{-# LANGUAGE TypeSynonymInstances, UndecidableInstances              #-}+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800+{-# LANGUAGE ConstrainedClassMethods, TypeFamilyDependencies #-} #endif+module Proof.Equational ( (:~:)(..), (:=:)                         , sym, trans                         , Equality(..), Preorder(..), reflexivity'-                        ,(:\/:), (:/\:), (=<=), (=>=), (=~=), Leibniz(..)+                        , (:\/:), (:/\:), (=<=), (=>=), (=~=), Leibniz(..)                         , Reason(..), because, by, (===), start, byDefinition                         , admitted, Proxy(..), cong, cong'-                        , Proposition(..), (:~>), FromBool (..)+                        , Proposition(..), HVec(..), FromBool (..)+                        , applyNAry, applyNAry', fromBool'                           -- * Conversion between equalities                         , fromRefl, fromLeibniz, reflToLeibniz, leibnizToRefl                           -- * Coercion@@ -22,10 +22,8 @@                         ) where import Data.Proxy import Data.Singletons-import Unsafe.Coerce-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 import Data.Type.Equality hiding (apply)-#endif+import Unsafe.Coerce  infix 4 :=: type a :\/: b = Either a b@@ -34,39 +32,8 @@ type a :/\: b = (a, b) infixr 3 :/\: -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 707-data a :=: b where-  Refl :: a :=: a-type (:~:) = (:=:)-infix 4 :~:-trans :: a :=: b -> b :=: c -> a :=: c-trans Refl Refl = Refl--sym :: a :=: b -> b :=: a-sym Refl = Refl--deriving instance Eq   (a :=: b)-deriving instance Show (a :=: b)-deriving instance Ord  (a :=: b)--instance a ~ b => Read (a :=: b) where-  readsPrec d = readParen (d > 10) (\r -> [(Refl, s) | ("Refl",s) <- lex r ])--instance a ~ b => Enum (a :=: b) where-  toEnum 0 = Refl-  toEnum _ = error "toEnum: bad argument"--  fromEnum Refl = 0--instance a ~ b => Bounded (a :=: b) where-  minBound = Refl-  maxBound = Refl--#else type (:=:) = (:~:)-#endif - data Leibniz a b = Leibniz { apply :: forall f. f a -> f b }  leibnizToRefl :: Leibniz a b -> a :=: b@@ -184,24 +151,60 @@   coerce' xs = unsafeCoerce   #-} --#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 class Proposition (f :: k -> *) where-  type OriginalProp (f :: k -> *) (n :: k) :: *    -#else-class Proposition f where-  type OriginalProp f n :: *-#endif+  type OriginalProp (f :: k -> *) (n :: k) :: *   unWrap :: f n -> OriginalProp f n   wrap   :: OriginalProp f n -> f n -type family   (xs :: [*]) :~> (a :: *) :: *-type instance '[]       :~> a = a-type instance (x ': xs) :~> a = x -> (xs :~> a)+data HVec (xs :: [*]) where+  HNil :: HVec '[]+  (:-) :: x -> HVec xs -> HVec (x ': xs) +infixr 9 :-+type family (xs :: [*]) :~> (a :: *) :: * where+  '[]       :~> a = a+  (x ': xs) :~> a = x -> (xs :~> a)+ infixr 1 :~> +data HVecView (xs :: [*]) :: * where+  HNilView  :: HVecView '[]+  HConsView :: Proxy t -> HVecView ts -> HVecView (t ': ts)++deriving instance Show (HVecView xs)++class KnownTypeList (xs :: [*]) where+  viewHVec' :: HVecView xs++instance KnownTypeList '[] where+  viewHVec' = HNilView++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' HNilView f = f HNil+apply' (HConsView Proxy ts) f = \a -> withKnownTypeList ts $+  apply' ts (\ts' -> f $ a :- ts')++applyNAry :: forall ts c. KnownTypeList ts => (HVec ts -> c) -> ts :~> c+applyNAry = apply' (viewHVec' :: HVecView ts)++applyNAry' :: KnownTypeList ts => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c+applyNAry' _ _ = applyNAry+ class FromBool (c :: *) where   type Predicate c :: Bool   type Args c :: [*]-  fromBool :: Predicate c ~ True => Args c :~> 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' pxyc = applyNAry' (Proxy :: Proxy (Args c)) pxyc fromBool

@@ -2,6 +2,8 @@ {-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators              #-} {-# LANGUAGE UndecidableInstances, ViewPatterns                        #-} module Proof.Induction (genInduction) where+import Proof.Internal.THCompat+ import Control.Applicative import Control.Monad import Data.Char@@ -19,7 +21,7 @@ genInduction :: Name -> String -> Q [Dec] genInduction typ fname0 = do   let fname = mkName fname0-  TyConI (normalizeDec -> DataD _ dName _ dCons _) <- reify typ+  TyConI (normalizeDec -> DataDCompat _ dName _ dCons _) <- reify typ   p <- newName "p"   ans <- mapM (buildCase fname (length dCons) dName p) $ zip [0..] dCons   let (cls, ts) = unzip ans@@ -50,7 +52,7 @@   sig <- if null params then tbdy else forallT (map (either plainTV plainTV) eparams) (cxt []) tbdy   cs <- replicateM size $ newName "case"   let body | null subCases = varE (cs !! nth)-           | otherwise = appsE $ varE (cs !! nth) : +           | otherwise = appsE $ varE (cs !! nth) :                replicate (length subCases) (appsE $ varE fname : map varE cs)                ++ [ appsE (varE ssName : map varE xs)]   cl <- clause (map varP cs ++ [conP sName $ map varP xs]) (normalB body) []@@ -87,6 +89,6 @@ getTyConName _             = Nothing  normalizeDec :: Dec -> Dec-normalizeDec d@(DataD _ _ _ _ _) = d-normalizeDec (NewtypeD ctx name tvbs con names) = DataD ctx name tvbs [con] names+normalizeDec d@DataDCompat {} = d+normalizeDec (NewtypeDCompat ctx name tvbs con names) = mkDataD ctx name tvbs [con] names normalizeDec _ = error "not data definition."

@@ -0,0 +1,46 @@+{-# 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+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800+        Nothing cons (map ConT names)+#else+        cons names+#endif+++typeName :: Type -> Name+typeName (VarT n) = n+typeName (ConT n) = n+typeName (PromotedT n) = n+typeName (TupleT n) = tupleTypeName n+typeName (UnboxedTupleT n) = unboxedTupleTypeName n+typeName ArrowT = ''(->)+typeName EqualityT = ''(~)+typeName ListT = ''[]+typeName (PromotedTupleT n) = tupleDataName n+typeName PromotedNilT = '[]+typeName PromotedConsT = '(:)+typeName ConstraintT = ''Constraint+typeName _ = error "No names!"++pattern DataDCompat cxt name tvbndrs cons names <-+  DataD cxt 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+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800+        _ con (map typeName -> names)+#else+        con names+#endif

@@ -2,7 +2,7 @@ --  documentation, see http://haskell.org/cabal/users-guide/  name:                equational-reasoning-version:             0.2.0.7+version:             0.3.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@@ -12,9 +12,7 @@ copyright:           (c) Hiromi ISHII 2013-2014 category:            Math build-type:          Simple-tested-with:         GHC == 7.6.3,-                     GHC == 7.8.3, GHC == 7.8.4,-                     GHC == 7.10.2+tested-with:         GHC == 7.10.3, GHC == 8.0.1 cabal-version:       >=1.8  source-repository head@@ -23,14 +21,11 @@  library   exposed-modules:     Proof.Equational, Proof.Propositional, Proof.Induction+  other-modules:       Proof.Internal.THCompat   build-depends:       base             >= 4      && < 5                ,       void             >= 0.6    && < 0.8-               ,       template-haskell >= 2.8    && < 2.11-  if impl(ghc < 7.8)-    build-depends:     singletons       == 0.8.*-                 ,     tagged           >= 0.6+               ,       template-haskell+  if impl(ghc < 7.10)+    build-depends:     singletons       >= 0.8    && < 1.2   else-    if impl(ghc < 7.10)-      build-depends:     singletons       >= 0.8    && < 1.2-    else-      build-depends:     singletons       == 2.0.*+    build-depends:     singletons       >= 2.1    && < 2.3