2022-02-12 01:33:41 +03:00
|
|
|
```ucm:hide
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> builtins.merge
|
2022-02-12 01:33:41 +03:00
|
|
|
```
|
|
|
|
|
|
|
|
|
|
```unison
|
|
|
|
|
structural ability Split where
|
|
|
|
|
skip! : x
|
|
|
|
|
both : a -> a -> a
|
|
|
|
|
|
|
|
|
|
Split.append : '{Split, g} a -> '{Split, g} a -> '{Split, g} a
|
|
|
|
|
Split.append s1 s2 _ = force (both s1 s2)
|
|
|
|
|
|
|
|
|
|
force a = !a
|
|
|
|
|
|
|
|
|
|
Split.zipSame : '{Split, g} a -> '{Split, g} b -> '{Split, g} (a, b)
|
|
|
|
|
Split.zipSame sa sb _ =
|
|
|
|
|
go : '{Split,g2} y -> Request {Split} x ->{Split,g2} (x,y)
|
|
|
|
|
go sb = cases
|
|
|
|
|
{ a } -> (a, !sb)
|
|
|
|
|
{ skip! -> _ } -> skip!
|
|
|
|
|
{ both la ra -> k } ->
|
|
|
|
|
handle !sb with cases
|
|
|
|
|
{ _ } -> skip!
|
|
|
|
|
{ skip! -> k } -> skip!
|
|
|
|
|
{ both lb rb -> k2 } ->
|
|
|
|
|
force (Split.append
|
|
|
|
|
(zipSame '(k la) '(k2 lb))
|
|
|
|
|
(zipSame '(k ra) '(k2 rb)))
|
|
|
|
|
|
|
|
|
|
handle !sa with go sb
|
|
|
|
|
```
|
