equational-reasoning 0.0.1.0 → 0.0.3.0
raw patch · 3 files changed
+127/−7 lines, 3 filesdep +template-haskell
Dependencies added: template-haskell
Files
- Proof/Equational.hs +28/−1
- Proof/Induction.hs +92/−0
- equational-reasoning.cabal +7/−6
Proof/Equational.hs view
@@ -4,13 +4,18 @@ module Proof.Equational ((:=:)(..), Equality(..), Preorder(..), reflexivity' ,(:\/:), (:/\:), (=>=), (=~=), Leibniz(..) , Reason(..), because, by, (===), start, byDefinition- , admitted, Proxy(..), cong, cong', fromRefl+ , admitted, Proxy(..), cong, cong' , Proposition(..), (:~>), FromBool (..)+ -- * Conversion between equalities+ , fromRefl, fromLeibniz, reflToLeibniz, leibnizToRefl+ -- * Coercion+ , coerce, coerce' -- * Re-exported modules , module Data.Singletons, module Data.Proxy ) where import Data.Proxy import Data.Singletons+import Unsafe.Coerce infix 4 :=: type a :\/: b = Either a b@@ -24,9 +29,18 @@ 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, SingRep a) => Leibniz a b -> eq a b+fromLeibniz eq = apply eq (reflexivity sing)+ fromRefl :: (Preorder eq, SingRep b) => a :=: b -> eq a b fromRefl Refl = reflexivity' +reflToLeibniz :: a :=: b -> Leibniz a b+reflToLeibniz Refl = Leibniz id+ deriving instance Show (a :=: b) class Preorder (eq :: k -> k -> *) where@@ -97,6 +111,19 @@ cong' :: (Sing m -> Sing (f m)) -> a :=: b -> f a :=: f b cong' _ Refl = Refl++-- | Type coercion. 'coerce' is using @unsafeCoerce a@.+-- So, please, please do not provide the @undefined@ as the proof.+-- 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+{-# INLINE coerce #-}++-- | Coercion for identity types.+coerce' :: a :=: b -> a -> b+coerce' Refl a = unsafeCoerce a+{-# INLINE coerce' #-} class Proposition f where type OriginalProp f n :: *
+ Proof/Induction.hs view
@@ -0,0 +1,92 @@+{-# LANGUAGE DataKinds, FlexibleContexts, GADTs, PolyKinds, RankNTypes #-}+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators #-}+{-# LANGUAGE UndecidableInstances, ViewPatterns #-}+module Proof.Induction (genInduction) where+import Control.Applicative+import Control.Monad+import Data.Char+import Data.Either+import Data.List+import Data.Singletons+import Language.Haskell.TH+import Language.Haskell.TH.Lib++capitalize :: String -> String+capitalize (x :xs) = toUpper x : xs+capitalize _ = error "capitalize"++-- | @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 -> DataD _ 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 freeVars = lefts eparams+ 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++getFreeVarT :: Type -> [Name]+getFreeVarT (AppT a b) = getFreeVarT a ++ getFreeVarT b+getFreeVarT (SigT a _) = getFreeVarT a+getFreeVarT (ForallT tvs _ t) = getFreeVarT t \\ map tyVarName tvs+getFreeVarT (VarT n) = [n]+getFreeVarT _ = []++tyVarName :: TyVarBndr -> Name+tyVarName (PlainTV n) = n+tyVarName (KindedTV n _) = n++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@(DataD _ _ _ _ _) = d+normalizeDec (NewtypeD ctx name tvbs con names) = DataD ctx name tvbs [con] names+normalizeDec _ = error "not data definition."
equational-reasoning.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: equational-reasoning-version: 0.0.1.0+version: 0.0.3.0 synopsis: Proof assistant for Haskell using DataKinds & PolyKinds -- description: license: BSD3@@ -15,9 +15,10 @@ cabal-version: >=1.8 library- exposed-modules: Proof.Equational, Proof.Propositional- build-depends: base == 4.6.*- , singletons == 0.8.*- , tagged == 0.6.*- , void == 0.6.*+ exposed-modules: Proof.Equational, Proof.Propositional, Proof.Induction+ build-depends: base == 4.6.*+ , singletons == 0.8.*+ , tagged == 0.6.*+ , void == 0.6.*+ , template-haskell == 2.8.*