blob: 82637eefcb5241d3721559fe190ee64b19dcca40 (
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
|
module Soat.Data.Sublist
import public Control.Relation
import Data.List.Elem
import Soat.Data.Product
%default total
infix 5 ++
public export
data Sublist : Rel (List a) where
Nil : Sublist [] ys
(::) : (mem : Elem x ys) -> (mems : Sublist xs ys) -> Sublist (x :: xs) ys
public export
curry : xs `Sublist` ys -> forall x . Elem x xs -> Elem x ys
curry (mem :: mems) Here = mem
curry (mem :: mems) (There y) = curry mems y
public export
uncurry : {xs : List a} -> (forall x . Elem x xs -> Elem x ys) -> xs `Sublist` ys
uncurry {xs = []} f = []
uncurry {xs = (x :: xs)} f = f Here :: uncurry (f . There)
public export
Reflexive (List a) Sublist where
reflexive = uncurry id
public export
Transitive (List a) Sublist where
transitive f g = uncurry (curry g . curry f)
public export
elemJoinL : Elem x xs -> Elem x (xs ++ ys)
elemJoinL Here = Here
elemJoinL (There elem) = There (elemJoinL elem)
public export
elemJoinR : (xs : List a) -> Elem x ys -> Elem x (xs ++ ys)
elemJoinR [] elem = elem
elemJoinR (x :: xs) elem = There (elemJoinR xs elem)
public export
elemSplit : (xs : List a) -> Elem x (xs ++ ys) -> Either (Elem x xs) (Elem x ys)
elemSplit [] elem = Right elem
elemSplit (x :: xs) Here = Left Here
elemSplit (x :: xs) (There elem) = bimap There id (elemSplit xs elem)
public export
(++) : {xs, ys, us : List a}
-> xs `Sublist` ys -> us `Sublist` vs -> (xs ++ us) `Sublist` (ys ++ vs)
(++) mems mems' = uncurry
(either (elemJoinL . curry mems) (elemJoinR ys . curry mems') . elemSplit xs)
public export
shuffle : is `Sublist` js -> x ^ js -> x ^ is
shuffle [] xs = []
shuffle (mem :: mems) xs = index xs mem :: shuffle mems xs
|
