Samizdat/NoFilter.agda at main · pigworker/Samizdat · GitHub

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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
module NoFilter where

_-_ : forall {i j k}{A : Set i}{B : A -> Set j}{C : (a : A) -> B a -> Set k}
  (f : (a : A) -> B a)
  (g : {a : A} -> (b : B a) -> C a b)
  (a : A) -> C a (f a)
(f - g) a = g (f a)

data Nat : Set where
  ze : Nat
  su : Nat -> Nat

data _<=_ : Nat -> Nat -> Set where
  no : forall {n m} -> n <= m ->    n <= su m
  su : forall {n m} -> n <= m -> su n <= su m
  ze : ze <= ze

data Vec (X : Set) : Nat -> Set where
  [] : Vec X ze
  _,-_ : forall {n} -> X -> Vec X n -> Vec X (su n)

_<?_ : forall {X n m} -> n <= m -> Vec X m -> Vec X n
no th <? (x ,- xs) = th <? xs
su th <? (x ,- xs) = x ,- (th <? xs)
ze <? [] = []

data _<#>_ : forall {i j n} -> i <= n -> j <= n -> Set where
  nosu : forall {i j n}{th : i <= n}{ph : j <= n} -> th <#> ph -> no th <#> su ph
  suno : forall {i j n}{th : i <= n}{ph : j <= n} -> th <#> ph -> su th <#> no ph
  ze   : ze <#> ze

_!>_<!_ : forall {X i j n}{th : i <= n}{ph : j <= n}
  -> Vec X i -> th <#> ph -> Vec X j -> Vec X n
xs !> nosu p <! (x ,- ys) = x ,- (xs !> p <! ys)
(x ,- xs) !> suno p <! ys = x ,- (xs !> p <! ys)
[] !> ze <! [] = []

record _><_ (S : Set)(T : S -> Set) : Set where
  constructor _,_
  field
    fst : S
    snd : T fst
open _><_ public

data Zeroey : Set where
record Zero : Set where
  constructor wrong
  field
    .bad : Zeroey
record One : Set where constructor <>
data Two : Set where ff tt : Two

_<ft>_ : forall {l}{P : Two -> Set l} -> P ff -> P tt -> (b : Two) -> P b
(f <ft> t) ff = f
(f <ft> t) tt = t

_*_ : Set -> Set -> Set
S * T = S >< \ _ -> T

_+_ : Set -> Set -> Set
S + T = Two >< (S <ft> T)

record Mebbes : Set1 where
  field
    Naw : Set
    Aye : Set
    wha : Naw + Aye
    .ain : Naw -> Aye -> Zero
open Mebbes public

[Vec_] : forall {X n} -> (X -> Set) -> Vec X n -> Set
[Vec P ] [] = One
[Vec P ] (x ,- xs) = P x * [Vec P ] xs

data Filter {X : Set}(D : X -> Mebbes){n : Nat} : Vec X n -> Set where
  filtered : forall {i j}{th : i <= n}{ph : j <= n}
    -> (ns : Vec X i)
    -> [Vec D - Naw ] ns
    -> (p : th <#> ph)
    -> (as : Vec X j)
    -> [Vec D - Aye ] as
    -> Filter D (ns !> p <! as)

filter : forall {X : Set}(D : X -> Mebbes){n : Nat}(xs : Vec X n) -> Filter D xs
filter D [] = filtered [] <> ze [] <>
filter D (x ,- xs) with D x .wha | filter D xs
... | ff , z | filtered ns np p as ap = filtered (x ,- ns) (z , np) (suno p) as ap
... | tt , z | filtered ns np p as ap = filtered ns np  (nosu p) (x ,- as) (z , ap)