summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGaborGreif <>2017-10-12 08:22:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2017-10-12 08:22:00 (GMT)
commit17d73f2fd0e812abf8bc31d2e10da2415fee90d6 (patch)
tree4dc61b6b13a974508b1c2c9da1505aad037909bf
parent6811f99e8a16f4e6aff077a7c1f6bf3a5c4099c5 (diff)
version 0.10.1
-rw-r--r--Main.hs13
-rw-r--r--TyFamWitnesses.hs23
-rw-r--r--tyfam-witnesses.cabal12
3 files changed, 26 insertions, 22 deletions
diff --git a/Main.hs b/Main.hs
index 4c90623..faef0ea 100644
--- a/Main.hs
+++ b/Main.hs
@@ -52,18 +52,16 @@ stuffwant2 = [d|
|]
stuffhave3 = [d| data Peano = Z | S Peano
- type family ToPeano (n :: Nat) :: Peano where ToPeano 0 = Z; ToPeano 1 = S Z
+ type family ToPeano (n :: Nat) :: Peano where ToPeano 0 = Z; ToPeano n = S (ToPeano (n-1))
type family FromPeano (p :: Peano) :: Nat where FromPeano Z = 0; FromPeano (S n) = 1 + FromPeano n
|]
witnesses [d| data Peano = Z | S Peano
- type family ToPeano (n :: Nat) :: Peano where ToPeano 0 = Z; ToPeano 1 = S Z
- --type family FromPeano (p :: Peano) :: Nat where FromPeano Z = 0; FromPeano (S n) = 1 + FromPeano n
+ type family ToPeano (n :: Nat) :: Peano where ToPeano 0 = Z; ToPeano n = S (ToPeano (n-1))
+ type family FromPeano (p :: Peano) :: Nat where FromPeano Z = 0; FromPeano (S n) = 1 + FromPeano n
|]
-witnesses [d| type family FromPeano (p :: Peano) :: Nat where FromPeano Z = 0; FromPeano (S n) = 1 + FromPeano n
- |]
deriving instance Show (FromPeanoRefl n)
@@ -113,3 +111,8 @@ Just (t4r, (($ 'o').($ elem) -> t4@True)) = lemma "joe" (typeOf $ member @Char)
Just (t4'r, (($ 'x').($ elem) -> t4'@False)) = lemma "joe" (typeOf $ member @Char) (typeOf "joe")
t0@Nothing = lemma "joe" (typeOf ord) (typeOf "joe")
+
+
+Just u0 = reify_FromPeano (typeRep @Z)
+Just u1 = reify_FromPeano (typeRep @(S Z))
+Just u2 = reify_FromPeano (typeRep @(S (S Z)))
diff --git a/TyFamWitnesses.hs b/TyFamWitnesses.hs
index e0b7586..fbce1d5 100644
--- a/TyFamWitnesses.hs
+++ b/TyFamWitnesses.hs
@@ -11,8 +11,7 @@
-- - remove the `Lift Exp` hack (or revert to what I had before),
-- see https://ghc.haskell.org/t/14296
-- - clients need to activate ScopedTypeVariables
--- - stuffhave3 in Main.hs won't create reify_ToPeano
--- - stuffhave3 in Main.hs errors in TyFamWitnesses.hs:(120,9)-(128,43): Non-exhaustive
+-- - type family a /=/ b where, how to name the artifacts?
module TyFamWitnesses (witnesses, stuffhave, stuffhave1, stuffhave2, pattern Lifted, pattern Fun') where
import GHC.Exts
@@ -71,20 +70,20 @@ stuffwant = [d| data FooRefl a b where FooRefl0 :: (Foo a a ~ Int) => FooRefl a
witnesses :: DecsQ -> DecsQ
witnesses decsQ =
do decs <- decsQ
- datasNames <- sequence (wantHave <$> decs)
- let (datas, names) = let dns = mapMaybe id datasNames in (fst <$> dns, snd <$> dns)
- funcs <- sequence (zipWith wantHave2 names decs)
+ datasNames <- sequence (buildGADT <$> decs)
+ let (datas, namesConstrsFams) = let dns = mapMaybe id datasNames in unzip dns
+ funcs <- sequence (buildReifier <$> namesConstrsFams)
pure $ decs ++ datas ++ concat funcs
-wantHave :: Dec -> Q (Maybe (Dec, (Name, [Exp])))
-wantHave (ClosedTypeFamilyD (TypeFamilyHead name tyvars _ Nothing) clauses) =
+buildGADT :: Dec -> Q (Maybe (Dec, (Name, [Exp], Dec)))
+buildGADT fam@(ClosedTypeFamilyD (TypeFamilyHead name tyvars _ Nothing) clauses) =
do ns <- sequence constrNames
n <- newName (occ ++ "Refl")
- pure (pure (DataD [] n tyvars Nothing (constrs ns n) [], (n, ConE <$> ns)))
+ pure (pure (DataD [] n tyvars Nothing (constrs ns n) [], (n, ConE <$> ns, fam)))
where Name (OccName occ) _ = name
constrs ns n = zipWith (clauseToCtor name n) ns clauses
constrNames = take (length clauses) $ generateConstrNames name
-wantHave _ = pure Nothing
+buildGADT _ = pure Nothing
generateConstrNames :: Name -> [Q Name]
generateConstrNames (Name (OccName occ) _) = (\n -> newName (occ ++ show n)) <$> [0..]
@@ -96,8 +95,8 @@ instance Lift Exp where lift = pure
pattern TRACE <- ((`traceShow` ()) -> ())
-wantHave2 :: (Name, [Exp]) -> Dec -> DecsQ
-wantHave2 (dname, constrs) (ClosedTypeFamilyD (TypeFamilyHead name formals _ Nothing) clauses) =
+buildReifier :: (Name, [Exp], Dec) -> DecsQ
+buildReifier (dname, constrs, ClosedTypeFamilyD (TypeFamilyHead name formals _ Nothing) clauses) =
do n <- newName ("reify_" ++ occ)
tyr <- [t|TypeRep|]
mbe <- [t|Maybe|]
@@ -167,7 +166,7 @@ wantHave2 (dname, constrs) (ClosedTypeFamilyD (TypeFamilyHead name formals _ Not
tv how (PlainTV formal) = how formal
tv how (KindedTV formal _) = how formal
appliedFormals = foldl' AppT (ConT dname) formalsTypes
-wantHave2 _ _ = pure []
+buildReifier _ = pure []
pattern AppArrowT l r = AppT (AppT ArrowT l) r
infixr 1 `AppArrowT`
diff --git a/tyfam-witnesses.cabal b/tyfam-witnesses.cabal
index 86b9b98..a555c53 100644
--- a/tyfam-witnesses.cabal
+++ b/tyfam-witnesses.cabal
@@ -1,21 +1,23 @@
name: tyfam-witnesses
-version: 0.0.0.1
+version: 0.1
synopsis: Provide proof witnesses for closed type family evaluation
-description: Template Haskell routine for generating form type family @Foo@
+description: Template Haskell routine for generating from type family 'Foo'
.
[@FooRefl@]: a GADT capturing the equalities of each type family clause
- [@reify_Foo@]: a function that analyses @TypeRep@s and reifies the matching clause as a @FooRefl@
+ [@reify_Foo@]: a function that analyses 'TypeRep's and reifies the matching clause as a 'FooRefl'
.
- Note that @Type.Reflection@ is new with GHC v8.2!
+ Note that 'Type.Reflection' is new with GHC v8.2!
license: MIT
license-file: LICENSE
author: Gabor Greif
maintainer: ggreif+tyfam@gmail.com
copyright: © Gabor Greif, 2017
category: Development
+stability: experimental
+
build-type: Simple
--- extra-source-files:
cabal-version: >=1.10
+tested-with: GHC == 8.2.1
library
exposed-modules: TyFamWitnesses