equational-reasoning 0.5.1.0 → 0.5.1.1

raw patch · 4 files changed

+55/−46 lines, 4 filesdep ~containersdep ~singletonsdep ~template-haskellPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

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

API changes (from Hackage documentation)

- Proof.Equational: type :=: = (:~:)

- Proof.Propositional: instance Proof.Propositional.Inhabited.Inhabited (GHC.Base.Maybe a)

+ Proof.Equational: infix 4 :=:

+ Proof.Equational: infixr 2 :\/:

+ Proof.Equational: infixr 3 :/\:

+ Proof.Equational: infixr 9 :-

+ Proof.Equational: type (:=:) = (:~:)

+ Proof.Propositional: infixr 2 \/

+ Proof.Propositional: infixr 3 /\

+ Proof.Propositional: instance Proof.Propositional.Inhabited.Inhabited (GHC.Maybe.Maybe a)

- Proof.Equational: Proxy :: Proxy k

+ Proof.Equational: Proxy :: Proxy

- Proof.Equational: [Refl] :: (:~:) k a a

+ Proof.Equational: [Refl] :: forall k (a :: k) (b :: k). () => a :~: a

- Proof.Equational: coerce' :: a :=: b -> a -> b

+ Proof.Equational: coerce' :: (a :=: b) -> a -> b

- Proof.Equational: cong :: forall f a b. Proxy f -> a :=: b -> f a :=: f b

+ Proof.Equational: cong :: forall f a b. Proxy f -> (a :=: b) -> f a :=: f b

- Proof.Equational: cong' :: (Sing m -> Sing (f m)) -> a :=: b -> f a :=: f b

+ Proof.Equational: cong' :: (Sing m -> Sing (f m)) -> (a :=: b) -> f a :=: f b

- Proof.Equational: data Proxy k (t :: k) :: forall k. () => k -> *

+ Proof.Equational: data Proxy (t :: k) :: forall k. () => k -> Type

- Proof.Equational: fromRefl :: (Preorder eq, SingI b) => a :=: b -> eq a b

+ Proof.Equational: fromRefl :: (Preorder eq, SingI b) => (a :=: b) -> eq a b

- Proof.Equational: reflToLeibniz :: a :=: b -> Leibniz a b

+ Proof.Equational: reflToLeibniz :: (a :=: b) -> Leibniz a b

- Proof.Equational: sym :: () => (:~:) k a b -> (:~:) k b a

+ Proof.Equational: sym :: () => (a :~: b) -> b :~: a

- Proof.Equational: trans :: () => (:~:) k a b -> (:~:) k b c -> (:~:) k a c

+ Proof.Equational: trans :: () => (a :~: b) -> (b :~: c) -> a :~: c

- Proof.Equational: withRefl :: forall a b r. a :~: b -> (a ~ b => r) -> r

+ Proof.Equational: withRefl :: forall a b r. (a :~: b) -> (a ~ b => r) -> r

- Proof.Propositional: andAssocL :: a /\ (b /\ c) -> (a /\ b) /\ c

+ Proof.Propositional: andAssocL :: (a /\ (b /\ c)) -> (a /\ b) /\ c

- Proof.Propositional: andAssocR :: (a /\ b) /\ c -> a /\ (b /\ c)

+ Proof.Propositional: andAssocR :: ((a /\ b) /\ c) -> a /\ (b /\ c)

- Proof.Propositional: andElimL :: a /\ b -> a

+ Proof.Propositional: andElimL :: (a /\ b) -> a

- Proof.Propositional: andElimR :: a /\ b -> b

+ Proof.Propositional: andElimR :: (a /\ b) -> b

- Proof.Propositional: orAssocL :: a \/ (b \/ c) -> (a \/ b) \/ c

+ Proof.Propositional: orAssocL :: (a \/ (b \/ c)) -> (a \/ b) \/ c

- Proof.Propositional: orAssocR :: (a \/ b) \/ c -> a \/ (b \/ c)

+ Proof.Propositional: orAssocR :: ((a \/ b) \/ c) -> a \/ (b \/ c)

- Proof.Propositional: orElim :: a \/ b -> (a -> c) -> (b -> c) -> c

+ Proof.Propositional: orElim :: (a \/ b) -> (a -> c) -> (b -> c) -> c

Proof/Equational.hs view

@@ -157,7 +157,7 @@ withRefl :: forall a b r. a :~: b -> (a ~ b => r) -> r withRefl _ r = case unsafeCoerce (Refl :: () :~: ()) :: a :~: b of   Refl -> r-{-# INLINE [1] withRefl #-}+{-# NOINLINE withRefl #-} {-# RULES "withRefl/unsafeCoerce" [~1] forall x.   withRefl x = unsafeCoerce

Proof/Propositional.hs view

@@ -1,7 +1,7 @@ {-# LANGUAGE DataKinds, DeriveDataTypeable, EmptyCase, ExplicitForAll     #-} {-# LANGUAGE ExplicitNamespaces, FlexibleInstances, GADTs, KindSignatures #-}-{-# LANGUAGE LambdaCase, PolyKinds, StandaloneDeriving, TemplateHaskell   #-}-{-# LANGUAGE TypeOperators, RankNTypes                                    #-}+{-# LANGUAGE LambdaCase, PolyKinds, RankNTypes, StandaloneDeriving        #-}+{-# LANGUAGE TemplateHaskell, TypeOperators                               #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Provides type synonyms for logical connectives. module Proof.Propositional@@ -76,7 +76,7 @@  withWitness :: IsTrue b -> (b ~ 'True => r) -> r withWitness Witness r = r-{-# INLINE [1] withWitness #-}+{-# NOINLINE withWitness #-} {-# RULES "withWitness/coercion" [~1] forall x.   withWitness x = unsafeCoerce

Proof/Propositional/TH.hs view

@@ -25,7 +25,6 @@                                               dsReify, expandType, substTy,                                               sweeten) - -- | Macro to automatically derive @'Empty'@ instance for --   concrete (variable-free) types which may contain products. refute :: TypeQ -> DecsQ@@ -121,7 +120,11 @@ resolveSubsts :: [DType] -> DInfo -> Q (DCxt, [DCon]) resolveSubsts args info =   case info of-    (DTyConI (DDataD _ cxt _ tvbs dcons _) _) -> do+    (DTyConI (DDataD _ cxt _ tvbs+#if MIN_VERSION_th_desugar(1,9,0)+              _+#endif+             dcons _) _) -> do       let dic = M.fromList $ zip (map dtvbToName tvbs) args       (cxt , ) <$> mapM (substDCon dic) dcons     -- (DTyConI (DOpenTypeFamilyD n) _) ->  return []@@ -137,7 +140,11 @@ substDCon dic (DCon forall'd cxt conName fields mPhantom) =   DCon forall'd cxt conName     <$> substFields dic fields+#if MIN_VERSION_th_desugar(1,9,0)+    <*> substTy dic mPhantom+#else     <*> mapM (substTy dic) mPhantom+#endif  substFields :: SubstDic -> DConFields -> Q DConFields substFields subst@@ -169,8 +176,11 @@ splitType DArrowT = Just ([], ''(->), []) splitType (DLitT _) = Nothing splitType DWildCardT = Nothing+#if !MIN_VERSION_th_desugar(1,9,0) splitType DStarT = Nothing+#endif + data EqlJudge = NonEqual | Undecidable | Equal               deriving (Read, Show, Eq, Ord) @@ -225,7 +235,9 @@   | t == s    = return Equal   | otherwise = return NonEqual compareType' (DLitT _) _ = return NonEqual+#if !MIN_VERSION_th_desugar(1,9,0) compareType' DStarT DStarT = return NonEqual+#endif compareType' _ _ = return NonEqual  compareCxt :: DCxt -> DCxt -> Q EqlJudge@@ -251,6 +263,10 @@   | l == r = return Equal   | otherwise = return NonEqual comparePred (DConPr _) _ = return NonEqual+#if MIN_VERSION_th_desugar(1,9,0)+comparePred (DForallPr _ _ _) (DForallPr _ _ _) = return Undecidable+comparePred (DForallPr{}) _ = return NonEqual+#endif  substPred :: SubstDic -> DPred -> Q DPred substPred dic (DAppPr p1 p2) = DAppPr <$> substPred dic p1 <*> (expandType =<< substTy dic p2)

equational-reasoning.cabal view

@@ -1,46 +1,39 @@-name: equational-reasoning-version: 0.5.1.0-cabal-version: >=1.8-build-type: Simple-license: BSD3-license-file: LICENSE-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 ==8.0.2 GHC ==8.2.2 GHC ==8.4.1+-- Initial equational-reasoning.cabal generated by cabal init.  For further+--  documentation, see http://haskell.org/cabal/users-guide/ +name:                equational-reasoning+version:             0.5.1.1+synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds+description:         A simple convenient library to write equational / preorder proof as in Agda.+license:             BSD3+license-file:        LICENSE+author:              Hiromi ISHII+maintainer:          konn.jinro_at_gmail.com+copyright:           (c) Hiromi ISHII 2013-2018+category:            Math+build-type:          Simple+tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.1, GHC == 8.6.3+cabal-version:       >=1.8+ 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-        Proof.Induction-        Proof.Propositional.Inhabited-        Proof.Propositional.Empty-    build-depends:-        base ==4.*,-        containers ==0.5.*,-        template-haskell >=2.11 && <2.14,-        th-extras ==0.0.*,-        void >=0.6 && <0.8,-        singletons >=2.1 && <2.5-    other-modules:-        Proof.Internal.THCompat-        Proof.Propositional.TH-    ghc-options: -Wall-+  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+                     , containers       >= 0.5    && < 0.7+                     , template-haskell >= 2.11   && < 2.16+                     , th-extras        == 0.0.*+                     , void             >= 0.6    && < 0.8+                     , singletons       >= 2.1    && < 2.6+  if impl(ghc >= 8.4)+     build-depends:    th-desugar       >= 1.6 && < 1.11+  else+     build-depends:    semigroups       == 0.18.*+     build-depends:    th-desugar       >= 1.6 && < 1.11