on master help sign in
Implement insertOrSet
02deba9Sridhar Ratnakumar
src/JRec.hs+17−14
@@ -10,6 +10,7 @@ module JRec
10 append,
10 append,
11 union,
11 union,
12 insert,
12 insert,
13+ insertOrSet
13 )
14 )
14where
15where
15
16
@@ -95,21 +96,23 @@ insert ::
95 Rec lts -> Rec res
96 Rec lts -> Rec res
96insert = R.combine . Rec
97insert = R.combine . Rec
97
98
98−--insertOrSet ::
99+-- | Insert a field into a record. Set it if it already exists
99−-- forall label value rhs res.
100−-- ( KnownNat (R.RecSize rhs),
101−-- KnownNat (R.RecTyIdxH 0 label res),
102−-- KnownNat (1 + R.RecSize rhs),
103−-- KnownSymbol label,
104−-- res ~ R.Union '[label := value] rhs,
105−-- value ~ R.RecTy label res,
106−-- R.RecCopy rhs rhs res
107−-- ) =>
108−-- label := value ->
109−-- Rec rhs ->
110−-- Rec res
111−--insertOrSet = union . Rec
112--
100--
101+-- O(n) type check complexity.
102+insertOrSet ::
103+ forall label value rhs res.
104+ ( KnownNat (R.RecSize rhs),
105+ KnownNat (R.RecSize res),
106+ KnownNat (R.RecTyIdxH 0 label res),
107+ KnownSymbol label,
108+ value ~ R.RecTy label res,
109+ R.Reverse (R.Insert (label := value) (R.Reverse rhs)) ~ res,
110+ R.RecCopy rhs rhs res
111+ ) =>
112+ label := value ->
113+ Rec rhs ->
114+ Rec res
115+insertOrSet = R.insert
113
116
114----------------------------------------------------------------------------
117----------------------------------------------------------------------------
115-- Generic
118-- Generic
src/JRec/Internal.hs+41−7
@@ -222,18 +222,23 @@ type family KeyDoesNotExist (l :: Symbol) (lts :: [*]) :: Constraint where
222 )
222 )
223 KeyDoesNotExist q (l := t ': lts) = KeyDoesNotExist q lts
223 KeyDoesNotExist q (l := t ': lts) = KeyDoesNotExist q lts
224
224
225+type family Reverse (xs :: [*]) where
226+ Reverse '[] = '[]
227+ Reverse (x ': xs) = RecAppend (Reverse xs) '[x]
228+
225type family Insert (a :: *) (xs :: [*]) where
229type family Insert (a :: *) (xs :: [*]) where
226− Insert (a := t) '[] = a := t ': '[]
230+ Insert x '[] = x ': '[]
227− Insert (a := t1) (a := t2 ': xs) = a := t1 ': xs
231+ Insert (a := v) (a := _ ': xs) = a := v ': xs
228− Insert (a := t1) (x := t2 ': xs) = x := t2 ': Insert (a := t1) xs
232+ Insert a (x ': xs) = x ': Insert a xs
229
233
230type family Union xs ys where
234type family Union xs ys where
231 Union xs '[] = xs
235 Union xs '[] = xs
232 Union xs (y := t ': ys) = Union (Insert (y := t) xs) ys
236 Union xs (y := t ': ys) = Union (Insert (y := t) xs) ys
233
237
238+-- TODO: Rename to `Append`, because it just deals with general type list?
234type family RecAppend lhs rhs where
239type family RecAppend lhs rhs where
235 RecAppend '[] rhs = rhs
240 RecAppend '[] rhs = rhs
236− RecAppend (x := t ': xs) rhs = x := t ': RecAppend xs rhs
241+ RecAppend (x ': xs) rhs = x ': RecAppend xs rhs
237
242
238type family RecSize (lts :: [*]) :: Nat where
243type family RecSize (lts :: [*]) :: Nat where
239 RecSize '[] = 0
244 RecSize '[] = 0
@@ -394,9 +399,7 @@ combine lts rts =
394 (# s''''#, a# #) -> (# s''''#, MkRec a# #)
399 (# s''''#, a# #) -> (# s''''#, MkRec a# #)
395{-# INLINE combine #-}
400{-# INLINE combine #-}
396
401
397−-- | Union two records
402+-- | Union two records (left-biased)
398−--
399−-- NOTE: changed from original superrecord to not require a 'Sort'
400union ::
403union ::
401 forall lhs rhs res.
404 forall lhs rhs res.
402 ( KnownNat (RecSize lhs),
405 ( KnownNat (RecSize lhs),
@@ -426,6 +429,37 @@ union lts rts =
426 (# s''''#, a# #) -> (# s''''#, MkRec a# #)
429 (# s''''#, a# #) -> (# s''''#, MkRec a# #)
427{-# INLINE union #-}
430{-# INLINE union #-}
428
431
432+-- | Insert a field
433+--
434+-- Insert at beginning, unless the field already exists, in which case set it
435+-- directly.
436+insert ::
437+ forall l v rhs res.
438+ ( KnownNat (RecSize rhs),
439+ KnownNat (RecSize res),
440+ res ~ Reverse (Insert (l := v) (Reverse rhs)),
441+ RecCopy '[l := v] '[l := v] res,
442+ RecCopy rhs rhs res
443+ ) =>
444+ l := v ->
445+ Rec rhs ->
446+ Rec res
447+insert (l := v) rts =
448+ let !(I# size#) =
449+ fromIntegral $ natVal' (proxy# :: Proxy# (RecSize res))
450+ in runST' $
451+ ST $ \s# ->
452+ case newSmallArray# size# (error "No value") s# of
453+ (# s'#, arr# #) ->
454+ case recCopyInto (Proxy :: Proxy rhs) rts (Proxy :: Proxy res) arr# s'# of
455+ s''# ->
456+ case recCopyInto (Proxy :: Proxy '[l := v]) (unsafeRCons (l := v) $ unsafeRNil 1) (Proxy :: Proxy res) arr# s''# of
457+ s'''# ->
458+ case unsafeFreezeSmallArray# arr# s'''# of
459+ (# s''''#, a# #) -> (# s''''#, MkRec a# #)
460+{-# INLINE insert #-}
461+
462+
429
463
430-- | Alias for 'combine'
464-- | Alias for 'combine'
431(++:) ::
465(++:) ::
test/JRecSpec.hs+7−7
@@ -77,10 +77,10 @@ spec = do
77 -- `shouldBe` Rec (#a := 1, #b := 2, #a := 0, #c := 3)
77 -- `shouldBe` Rec (#a := 1, #b := 2, #a := 0, #c := 3)
78 it "duplicate insert should be disallowed" $ do
78 it "duplicate insert should be disallowed" $ do
79 pendingWith "TODO"
79 pendingWith "TODO"
80−-- describe "insertOrSet" $ do
80+ describe "insertOrSet" $ do
81−-- it "distinct" $ do
81+ it "distinct" $ do
82−-- insertOrSet (#a := 1) (Rec (#b := 2, #c := 3))
82+ insertOrSet (#a := 1) (Rec (#b := 2, #c := 3))
83−-- `shouldBe` Rec (#a := 1, #b := 2, #c := 3)
83+ `shouldBe` Rec (#a := 1, #b := 2, #c := 3)
84−-- it "overwrite" $ do
84+ it "overwrite" $ do
85−-- insertOrSet (#c := 1) (Rec (#b := 2, #c := 3))
85+ insertOrSet (#c := 1) (Rec (#b := 2, #c := 3))
86−-- `shouldBe` Rec (#b := 2, #c := 1)
86+ `shouldBe` Rec (#b := 2, #c := 1)