blob: 7ed72ca241039ef09a8fa4cfd9a29e7354486fea (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
|
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
module T13750a where
import Unsafe.Coerce
type family AnyT :: * where {}
type family AnyList :: [*] where {}
newtype NP (xs :: [*]) = NP [AnyT]
data IsNP (xs :: [*]) where
IsNil :: IsNP '[]
IsCons :: x -> NP xs -> IsNP (x ': xs)
isNP :: NP xs -> IsNP xs
isNP (NP xs) =
if null xs
then unsafeCoerce IsNil
else unsafeCoerce (IsCons (head xs) (NP (tail xs)))
pattern Nil :: () => (xs ~ '[]) => NP xs
pattern Nil <- (isNP -> IsNil)
where
Nil = NP []
pattern (:*) :: () => (xs' ~ (x ': xs)) => x -> NP xs -> NP xs'
pattern x :* xs <- (isNP -> IsCons x xs)
where
x :* NP xs = NP (unsafeCoerce x : xs)
infixr 5 :*
data NS (xs :: [[*]]) = NS !Int (NP AnyList)
data IsNS (xs :: [[*]]) where
IsZ :: NP x -> IsNS (x ': xs)
IsS :: NS xs -> IsNS (x ': xs)
isNS :: NS xs -> IsNS xs
isNS (NS i x)
| i == 0 = unsafeCoerce (IsZ (unsafeCoerce x))
| otherwise = unsafeCoerce (IsS (NS (i - 1) x))
pattern Z :: () => (xs' ~ (x ': xs)) => NP x -> NS xs'
pattern Z x <- (isNS -> IsZ x)
where
Z x = NS 0 (unsafeCoerce x)
pattern S :: () => (xs' ~ (x ': xs)) => NS xs -> NS xs'
pattern S p <- (isNS -> IsS p)
|
