1
1
mirror of https://github.com/juspay/jrec.git synced 2024-09-11 10:25:32 +03:00

Add append

This commit is contained in:
Sridhar Ratnakumar 2020-08-19 19:42:44 -04:00
parent 747dfb5eb0
commit 9649572445
2 changed files with 29 additions and 2 deletions

View File

@ -4,10 +4,11 @@
module JRec
( unField,
union,
(:=) (..),
Rec,
pattern Rec,
append,
union,
)
where
@ -39,7 +40,24 @@ unField _ (_ R.:= value) = value
-- Other operations
----------------------------------------------------------------------------
-- Append records
-- Appends records, without removing duplicates.
--
-- Left-biased. Does not sort.
append ::
forall lhs rhs res.
( KnownNat (R.RecSize lhs),
KnownNat (R.RecSize rhs),
KnownNat (R.RecSize lhs + R.RecSize rhs),
res ~ R.RecAppend lhs rhs,
R.RecCopy lhs lhs res,
R.RecCopy rhs rhs res
) =>
Rec lhs ->
Rec rhs ->
Rec res
append = R.combine
-- Merges records, removing duplicates (TODO)
--
-- Left-biased. Does not sort.
--

View File

@ -39,6 +39,15 @@ spec = do
`shouldBe` (Rec (#u := True, #a := 8))
setA2 (Rec (#u := True, #a := 5, #b := 6))
`shouldBe` (Rec (#u := True, #a := 8, #b := 6))
describe "append" $ do
it "simple append" $ do
Rec (#a := 1) `append` Rec (#b := 2)
`shouldBe` Rec (#a := 1, #b := 2)
it "append with duplicates" $ do
let r1 = Rec (#b := 5, #a := 6)
r2 = Rec (#c := 7, #a := 8)
r1 `union` r2
`shouldBe` Rec (#b := 5, #a := 8, #c := 7, #a := 8)
describe "union" $ do
it "simple union" $ do
Rec (#a := 1) `union` Rec (#b := 2)