summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHiromiIshii <>2019-02-05 16:06:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2019-02-05 16:06:00 (GMT)
commit9ac0ea5df8fee9a0f2c306d2a5b3bb67df96e51a (patch)
tree82bac8481c460e360da93b602ab4231bbf7cbd01
parent06416ee45e4b7158de91fb678af1ba2d10c759b0 (diff)
version 0.6.0.00.6.0.0
-rw-r--r--Proof/Equational.hs29
-rw-r--r--Proof/Induction.hs82
-rw-r--r--equational-reasoning.cabal6
3 files changed, 17 insertions, 100 deletions
diff --git a/Proof/Equational.hs b/Proof/Equational.hs
index 00468e4..862cb92 100644
--- a/Proof/Equational.hs
+++ b/Proof/Equational.hs
@@ -18,10 +18,9 @@ module Proof.Equational ( (:~:)(..), (:=:)
-- * 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 @@ data Leibniz a b = Leibniz { apply :: forall f. f a -> f b }
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 @@ instance Equality Leibniz where
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 @@ eq =>= (_ `Because` eq') = transitivity eq' eq
(===) = (=<=)
{-# 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 @@ admitted = undefined
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@.
diff --git a/Proof/Induction.hs b/Proof/Induction.hs
deleted file mode 100644
index deec01f..0000000
--- a/Proof/Induction.hs
+++ /dev/null
@@ -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."
diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal
index 6b0f2fa..30fbe33 100644
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -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 @@ source-repository head
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 @@ library
, 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