@@ -6,7 +6,6 @@ module Data.Schematic.Migration where
66import Data.Kind
77import Data.Schematic.Path
88import Data.Schematic.Schema
9−import Data.Schematic.Utils
109import Data.Singletons.Prelude hiding (All)
1110import Data.Singletons.TypeLits
1211import Data.Vinyl hiding (Dict)
@@ -89,47 +88,22 @@ type family Migratable (rs :: [(Revision, Schema)]) :: Constraint where
8988 Migratable ('(r,s) ': '[]) = (TopLevel s, SingI s)
9089 -- Migratable '[] = ('True ~ 'False)
9190
92−-- data NonEmpty a = a :| [a]
93−
94−-- data instance Sing (ne :: NonEmpty a) where
95−-- SNECons :: Known (Sing e), Known (Sing l))=> Sing (e :: k) -> Sing (l :: [k]) -> Sing (e ':| l)
96−
97−data Revisions = Revisions
98− Schema -- top version
99− [(Revision, Schema)]
100−
101−data instance Sing (rs :: Revisions) where
102− SRevisions
103− :: (SingI schema, SingI rps, Known (Dict (ElemOf schema prs)))
104− => Sing schema
105− -> Sing rps
106− -> Sing ('Revisions schema rps)
107−
108−-- -- | Heterogenous list with a proof of element schema included in the list itself.
109−-- data ElemList :: k -> [k] -> Type where
110−-- Singl :: Known (Sing schema) => Sing schema -> ElemList schema '[schema]
111−-- KeepProof :: Known (Sing new) => Sing new -> ElemList schema ss -> ElemList schema (new ': ss)
112−-- NewProof :: Known (Sing new) => Sing new -> ElemList schema ss -> ElemList new (new ': ss)
113−
11491type family ElemOf (e :: k) (l :: [(a,k)]) :: Constraint where
11592 ElemOf e '[] = 'True ~ 'False
11693 ElemOf e ( '(a, e) ': es) = ()
11794 ElemOf e (n ': es) = ElemOf e es
11895
11996-- | Extracts revision/schema pairs from @Versioned@ in reverse order.
120−type family AllVersions (vd :: Versioned) :: Revisions where
121− AllVersions ('Versioned s ms) = AllVersions' ('Revisions s '[ '("initial", s) ]) ms
97+type family AllVersions (vd :: Versioned) :: [(Revision, Schema)] where
98+ AllVersions ('Versioned s ms) = AllVersions' '[ '("initial", s) ] ms
12299
123−type family AllVersions' (acc :: Revisions) (ms :: [Migration]) :: Revisions where
124− AllVersions' acc '[] = acc
125− AllVersions' ('Revisions tv rs) (m ': ms) =
126− AllVersions' ('Revisions (Snd (ApplyMigration m tv)) (rs :++ '[(ApplyMigration m tv)])) ms
100+type family AllVersions' (acc :: [(Revision, Schema)]) (ms :: [Migration]) = (r :: [(Revision, Schema)]) where
101+ AllVersions' acc '[] = acc
102+ AllVersions' ( '(rh, sh) ': tl ) (m ': ms) =
103+ AllVersions' ( ApplyMigration m sh ': tl ) ms
127104
128−type family TopVersion (rs :: Revisions) :: Schema where
129− TopVersion ('Revisions s rs) = s
130−
131−type family SchemaPairs (rs :: Revisions) :: [(Revision, Schema)] where
132− SchemaPairs ('Revisions s rs) = rs
105+type family TopVersion (rs :: [(Revision, Schema)]) :: Schema where
106+ TopVersion ( '(rh, sh) ': tl) = sh
133107
134108class MigrateSchema (a :: Schema) (b :: Schema) where
135109 migrate :: JsonRepr a -> JsonRepr b
@@ -180,6 +154,14 @@ data instance Sing (v :: Versioned) where
180154 -> Sing (ms :: [Migration]) -- a bunch of migrations
181155 -> Sing ('Versioned s ms)
182156
157+-- data MList ms where
158+-- MSing :: proxy a -> MList '[a]
159+-- MCons :: Dict (MigrateSchema h a) -> proxy a -> MList (h ': tl) -> MList (a ': h ': tl)
160+
161+-- data MList ms where
162+-- MSing :: proxy a -> MList '[a]
163+-- MCons :: (JsonRepr h -> JsonRepr a) -> proxy a -> MList (h ': tl) -> MList (a ': h ': tl)
164+
183165type SchemaExample
184166 = 'SchemaObject
185167 '[ '("foo", 'SchemaArray '[ 'AEq 1] ( 'SchemaNumber '[ 'NGt 10 ]))
@@ -195,3 +177,9 @@ jsonExample = ReprObject $
195177 FieldRepr (ReprText "foo")
196178 :& FieldRepr (ReprOptional (Just (ReprText "bar")))
197179 :& RNil
180+
181+
182+-- tail :: [a] -> [a]
183+-- sTail :: Sing s -> Sing (Tail s)
184+-- :: (Head (Tail foo))
185+-- sHead (sTail foo)