equational-reasoning 0.5.1.1 → 0.6.0.0

raw patch · 3 files changed

+17/−100 lines, 3 filesdep −singletonsdep ~th-desugarPVP ok

version bump matches the API change (PVP)

Dependencies removed: singletons

Dependency ranges changed: th-desugar

API changes (from Hackage documentation)

Files

• Proof/Equational.hs +14/−15
• Proof/Induction.hs +0/−82
• equational-reasoning.cabal +3/−3

@@ -18,10 +18,9 @@                           -- * Coercion                         , coerce, coerce', withRefl                           -- * Re-exported modules-                        , module Data.Singletons, module Data.Proxy+                        , module Data.Proxy                         ) where import Data.Proxy-import Data.Singletons import Data.Type.Equality hiding (apply) import Unsafe.Coerce @@ -39,17 +38,17 @@ leibnizToRefl :: Leibniz a b -> a :=: b leibnizToRefl eq = apply eq Refl -fromLeibniz :: (Preorder eq, SingI a) => Leibniz a b -> eq a b-fromLeibniz eq = apply eq (reflexivity sing)+fromLeibniz :: (Preorder eq) => Leibniz a b -> eq a b+fromLeibniz eq = apply eq (reflexivity Proxy) -fromRefl :: (Preorder eq, SingI b) => a :=: b -> eq a b+fromRefl :: (Preorder eq) => a :=: b -> eq a b fromRefl Refl = reflexivity'  reflToLeibniz :: a :=: b -> Leibniz a b reflToLeibniz Refl = Leibniz id  class Preorder (eq :: k -> k -> *) where-  reflexivity  :: Sing a -> eq a a+  reflexivity  :: proxy a -> eq a a   transitivity :: eq a b  -> eq b c -> eq a c  class Preorder eq => Equality (eq :: k -> k -> *) where@@ -85,12 +84,12 @@ newtype Flip f a b = Flip { unFlip :: f b a }  data Reason eq x y where-  Because :: Sing y -> eq x y -> Reason eq x y+  Because :: proxy y -> eq x y -> Reason eq x y -reflexivity' :: (SingI x, Preorder r) => r x x-reflexivity' = reflexivity sing+reflexivity' :: (Preorder r) => r x x+reflexivity' = reflexivity Proxy -by, because :: Sing y -> eq x y -> Reason eq x y+by, because :: proxy y -> eq x y -> Reason eq x y because = Because by      = Because @@ -112,14 +111,14 @@ (===) = (=<=) {-# SPECIALISE INLINE[1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-} -(=~=) :: r x y -> Sing y -> r x y+(=~=) :: r x y -> proxy y -> r x y eq =~= _ = eq -start :: Preorder eq => Sing a -> eq a a+start :: Preorder eq => proxy a -> eq a a start = reflexivity -byDefinition :: (SingI a, Preorder eq) => eq a a-byDefinition = reflexivity sing+byDefinition :: (Preorder eq) => eq a a+byDefinition = reflexivity Proxy  admitted :: Reason eq x y admitted = undefined@@ -128,7 +127,7 @@ cong :: forall f a b. Proxy f -> a :=: b -> f a :=: f b cong Proxy Refl = Refl -cong' :: (Sing m -> Sing (f m)) -> a :=: b -> f a :=: f b+cong' :: (pxy m -> pxy (f m)) -> a :=: b -> f a :=: f b cong' _ Refl =  Refl  -- | Type coercion. 'coerce' is using @unsafeCoerce a@.

@@ -1,82 +0,0 @@-{-# 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.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]-genInduction typ fname0 = do-  let fname = mkName fname0-  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-  t <- newName "t"-  sig <- sigD fname $ forallT [plainTV p, plainTV t] (cxt []) $-           foldr toT ([t| Sing $(varT t) -> $(varT p) $(varT t) |]) $ map return ts-  dec <- funD fname (map return cls)-  return [sig, dec]--buildCase :: Name -> Int -> Name -> Name -> (Int, Con) -> Q (Clause, Type)-buildCase _ _ _ _ (_, ForallC _ _ _) = error "Existential types are not supported yet."-buildCase fname size dName p (nth, dCon) = do-  let paramTs = extractParams dCon-      conName = extractName dCon-      sName = mkName $ 'S' : nameBase conName-      ssName = mkName $ 's' : nameBase conName-  eparams <- forM paramTs $ \ty ->-    case getTyConName ty of-      Just nm | nm == dName -> Right <$> newName "t"-      _       -> Left <$> newName "a"-  xs <- replicateM (length paramTs) $ newName "x"-  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-           | otherwise   = foldr toT ([t| Sing $(promCon) -> $(varT p `appT` promCon) |]) subCases-  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) :-               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) []-  return (cl, sig)-  where-    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-    extractParams (InfixC (_, t) _ (_, s)) = [t,s]-    extractParams _                        = []--toT :: TypeQ -> TypeQ -> TypeQ-a `toT` b = arrowT `appT` a `appT` b--getTyConName :: Type -> Maybe Name-getTyConName (AppT a _)    = getTyConName a-getTyConName (SigT a _)    = getTyConName a-getTyConName (ConT nam)    = Just nam-getTyConName (PromotedT n) = Just n-getTyConName _             = Nothing--normalizeDec :: Dec -> Dec-normalizeDec d@DataDCompat {} = d-normalizeDec (NewtypeDCompat ctx name tvbs con names) = mkDataD ctx name tvbs [con] names-normalizeDec _ = error "not data definition."

@@ -2,9 +2,10 @@ --  documentation, see http://haskell.org/cabal/users-guide/  name:                equational-reasoning-version:             0.5.1.1+version:             0.6.0.0 synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds description:         A simple convenient library to write equational / preorder proof as in Agda.+                     Since 0.6.0.0, this no longer depends on @singletons@ package, and the @Proof.Induction@ module goes to @equational-reasoning-induction@ package. license:             BSD3 license-file:        LICENSE author:              Hiromi ISHII@@ -20,7 +21,7 @@     location: git://github.com/konn/equational-reasoning-in-haskell.git  library-  exposed-modules:     Proof.Equational, Proof.Propositional, Proof.Induction+  exposed-modules:     Proof.Equational, Proof.Propositional                      , Proof.Propositional.Inhabited                      , Proof.Propositional.Empty   other-modules:       Proof.Internal.THCompat@@ -31,7 +32,6 @@                      , 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