equational-reasoning 0.4.0.0 → 0.4.1.0

raw patch · 3 files changed

+36/−7 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Proof/Equational.hs +17/−5
• Proof/Propositional.hs +18/−1
• equational-reasoning.cabal +1/−1

@@ -16,7 +16,7 @@                           -- * Conversion between equalities                         , fromRefl, fromLeibniz, reflToLeibniz, leibnizToRefl                           -- * Coercion-                        , coerce, coerce'+                        , coerce, coerce', withRefl                           -- * Re-exported modules                         , module Data.Singletons, module Data.Proxy                         ) where@@ -136,19 +136,31 @@ -- Using this function instead of pattern-matching on equality proof, -- you can reduce the overhead introduced by run-time proof. coerce :: (a :=: b) -> f a -> f b-coerce Refl a = unsafeCoerce a+coerce _ a = unsafeCoerce a {-# INLINE[1] coerce #-}  -- | Coercion for identity types. coerce' :: a :=: b -> a -> b-coerce' Refl a = unsafeCoerce a+coerce' _ a = unsafeCoerce a {-# INLINE[1] coerce' #-}  {-# RULES-"coerce/unsafeCoerce" forall xs.+"coerce/unsafeCoerce" [~1] forall xs.   coerce xs = unsafeCoerce-"coerce'/unsafeCoerce" forall xs.+"coerce'/unsafeCoerce" [~1] forall xs.   coerce' xs = unsafeCoerce+  #-}++-- | Solves equality constraint without explicit coercion.+--   It has the same effect as @'Data.Type.Equality.gcastWith'@,+--   but some hacks is done to reduce runtime overhead.+withRefl :: forall a b r. a :~: b -> (a ~ b => r) -> r+withRefl _ r = case unsafeCoerce (Refl :: () :~: ()) :: a :~: b of+  Refl -> r+{-# INLINE [1] withRefl #-}+{-# RULES+"withRefl/unsafeCoerce" [~1] forall x.+  withRefl x = unsafeCoerce   #-}  class Proposition (f :: k -> *) where

@@ -1,7 +1,7 @@ {-# LANGUAGE DataKinds, DeriveDataTypeable, EmptyCase, ExplicitForAll     #-} {-# LANGUAGE ExplicitNamespaces, FlexibleInstances, GADTs, KindSignatures #-} {-# LANGUAGE LambdaCase, PolyKinds, StandaloneDeriving, TemplateHaskell   #-}-{-# LANGUAGE TypeOperators                                                #-}+{-# LANGUAGE TypeOperators, RankNTypes                                    #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Provides type synonyms for logical connectives. module Proof.Propositional@@ -22,6 +22,7 @@ import Data.Type.Equality ((:~:)) import Data.Typeable      (Typeable) import Data.Void+import Unsafe.Coerce  type a /\ b = (a, b) type a \/ b = Either a b@@ -73,6 +74,14 @@ data IsTrue (b :: Bool) where   Witness :: IsTrue 'True +withWitness :: IsTrue b -> (b ~ 'True => r) -> r+withWitness Witness r = r+{-# INLINE [1] withWitness #-}+{-# RULES+"withWitness/coercion" [~1] forall x.+  withWitness x = unsafeCoerce+  #-}+ deriving instance Show (IsTrue b) deriving instance Eq   (IsTrue b) deriving instance Ord  (IsTrue b)@@ -85,6 +94,14 @@  refute [t| 0 :~: 1 |] refute [t| () :~: Int |]+refute [t| 'True :~: 'False |]+refute [t| 'False :~: 'True |]+refute [t| 'LT :~: 'GT |]+refute [t| 'LT :~: 'EQ |]+refute [t| 'EQ :~: 'LT |]+refute [t| 'EQ :~: 'GT |]+refute [t| 'GT :~: 'LT |]+refute [t| 'GT :~: 'EQ |]  prove [t| Bool |] prove [t| Int |]

@@ -2,7 +2,7 @@ --  documentation, see http://haskell.org/cabal/users-guide/  name:                equational-reasoning-version:             0.4.0.0+version:             0.4.1.0 synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds description:         A simple convenient library to write equational / preorder proof as in Agda. license:             BSD3