blob: 10cac4edae219c0940fbd1c7dc5c1b5791444adf (
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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
|
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module AST.Sparse.Types where
import AST.Types
import Data.Kind (Type, Constraint)
import Data.Type.Equality
data Sparse t t' where
SpSparse :: Sparse t t' -> Sparse t (TMaybe t')
SpAbsent :: Sparse t TNil
SpPair :: Sparse a a' -> Sparse b b' -> Sparse (TPair a b) (TPair a' b')
SpLEither :: Sparse a a' -> Sparse b b' -> Sparse (TLEither a b) (TLEither a' b')
SpMaybe :: Sparse t t' -> Sparse (TMaybe t) (TMaybe t')
SpArr :: Sparse t t' -> Sparse (TArr n t) (TArr n t')
SpScal :: Sparse (TScal t) (TScal t)
deriving instance Show (Sparse t t')
class ApplySparse f where
applySparse :: Sparse t t' -> f t -> f t'
instance ApplySparse STy where
applySparse (SpSparse s) t = STMaybe (applySparse s t)
applySparse SpAbsent _ = STNil
applySparse (SpPair s1 s2) (STPair t1 t2) = STPair (applySparse s1 t1) (applySparse s2 t2)
applySparse (SpLEither s1 s2) (STLEither t1 t2) = STLEither (applySparse s1 t1) (applySparse s2 t2)
applySparse (SpMaybe s) (STMaybe t) = STMaybe (applySparse s t)
applySparse (SpArr s) (STArr n t) = STArr n (applySparse s t)
applySparse SpScal t = t
instance ApplySparse SMTy where
applySparse (SpSparse s) t = SMTMaybe (applySparse s t)
applySparse SpAbsent _ = SMTNil
applySparse (SpPair s1 s2) (SMTPair t1 t2) = SMTPair (applySparse s1 t1) (applySparse s2 t2)
applySparse (SpLEither s1 s2) (SMTLEither t1 t2) = SMTLEither (applySparse s1 t1) (applySparse s2 t2)
applySparse (SpMaybe s) (SMTMaybe t) = SMTMaybe (applySparse s t)
applySparse (SpArr s) (SMTArr n t) = SMTArr n (applySparse s t)
applySparse SpScal t = t
class IsSubType s where
type IsSubTypeSubject (s :: k -> k -> Type) (f :: k -> Type) :: Constraint
subtApply :: IsSubTypeSubject s f => s t t' -> f t -> f t'
subtTrans :: s a b -> s b c -> s a c
subtFull :: IsSubTypeSubject s f => f t -> s t t
instance IsSubType (:~:) where
type IsSubTypeSubject (:~:) f = ()
subtApply = gcastWith
subtTrans = trans
subtFull _ = Refl
instance IsSubType Sparse where
type IsSubTypeSubject Sparse f = f ~ SMTy
subtApply = applySparse
subtTrans s1 (SpSparse s2) = SpSparse (subtTrans s1 s2)
subtTrans _ SpAbsent = SpAbsent
subtTrans (SpPair s1a s1b) (SpPair s2a s2b) = SpPair (subtTrans s1a s2a) (subtTrans s1b s2b)
subtTrans (SpLEither s1a s1b) (SpLEither s2a s2b) = SpLEither (subtTrans s1a s2a) (subtTrans s1b s2b)
subtTrans (SpSparse s1) (SpMaybe s2) = SpSparse (subtTrans s1 s2)
subtTrans (SpMaybe s1) (SpMaybe s2) = SpMaybe (subtTrans s1 s2)
subtTrans (SpArr s1) (SpArr s2) = SpArr (subtTrans s1 s2)
subtTrans SpScal SpScal = SpScal
subtFull = spDense
spDense :: SMTy t -> Sparse t t
spDense SMTNil = SpAbsent
spDense (SMTPair t1 t2) = SpPair (spDense t1) (spDense t2)
spDense (SMTLEither t1 t2) = SpLEither (spDense t1) (spDense t2)
spDense (SMTMaybe t) = SpMaybe (spDense t)
spDense (SMTArr _ t) = SpArr (spDense t)
spDense (SMTScal _) = SpScal
isDense :: SMTy t -> Sparse t t' -> Maybe (t :~: t')
isDense SMTNil SpAbsent = Just Refl
isDense _ SpSparse{} = Nothing
isDense _ SpAbsent = Nothing
isDense (SMTPair t1 t2) (SpPair s1 s2)
| Just Refl <- isDense t1 s1, Just Refl <- isDense t2 s2 = Just Refl
| otherwise = Nothing
isDense (SMTLEither t1 t2) (SpLEither s1 s2)
| Just Refl <- isDense t1 s1, Just Refl <- isDense t2 s2 = Just Refl
| otherwise = Nothing
isDense (SMTMaybe t) (SpMaybe s)
| Just Refl <- isDense t s = Just Refl
| otherwise = Nothing
isDense (SMTArr _ t) (SpArr s)
| Just Refl <- isDense t s = Just Refl
| otherwise = Nothing
isDense (SMTScal _) SpScal = Just Refl
isAbsent :: Sparse t t' -> Bool
isAbsent (SpSparse s) = isAbsent s
isAbsent SpAbsent = True
isAbsent (SpPair s1 s2) = isAbsent s1 && isAbsent s2
isAbsent (SpLEither s1 s2) = isAbsent s1 && isAbsent s2
isAbsent (SpMaybe s) = isAbsent s
isAbsent (SpArr s) = isAbsent s
isAbsent SpScal = False
|
