-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathdemo.txt
125 lines (108 loc) · 4.34 KB
/
demo.txt
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
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
Max list length: 3
refine = { <a:[<>]> | 0 <= len val.a }
simple = <a:[<>]>
i(val) = val
Validated!
refine = { <a:[<>]> | len val.a <= 0 }
simple = <a:<>>
i(val) = <
a = []
>
Validated!
refine = { <a:[<>], b:[<>]> | len val.a <= len val.b }
simple = <a:<0:[<α:<>, β:<>>]>, b:[<>]>
i(val) = <
a = map (λx. proj_{α} x) proj_{0} proj_{a} val,
b = map (λx. proj_{β} x) proj_{0} proj_{a} val ++ proj_{b} val
>
Validated!
refine = { <a:[<>], b:[<>]> | 2len val.a <= 3len val.b }
simple = <a:<0:[<α:<1:<>, 2:<>, 3:<>>, β:<1:<>, 2:<>>>]>, b:[<>]>
i(val) = <
a = flatten_3 map (λx. proj_{α} x) proj_{0} proj_{a} val,
b = flatten_2 map (λx. proj_{β} x) proj_{0} proj_{a} val ++ proj_{b} val
>
Validated!
refine = { <a:[<>], b:[<>], c:[<>]> | len val.a + len val.b <= len val.c }
simple = <a:<0:[<α:<>, β:<>>]>, b:<0:[<α:<>, β:<>>]>, c:[<>]>
i(val) = <
a = map (λx. proj_{α} x) proj_{0} proj_{a} val,
b = map (λx. proj_{α} x) proj_{0} proj_{b} val,
c = map (λx. proj_{β} x) proj_{0} proj_{a} val ++ map (λx. proj_{β} x) proj_{0} proj_{b} val ++ proj_{c} val
>
Validated!
refine = { <a:[<>], b:[<>], c:[<>]> | len val.a <= len val.b + len val.c }
simple = <a:<0:[<α:<>, β:<>>], 1:[<α:<>, β:<>>]>, b:[<>], c:[<>]>
i(val) = <
a = map (λx. proj_{α} x) proj_{0} proj_{a} val ++ map (λx. proj_{α} x) proj_{1} proj_{a} val,
b = map (λx. proj_{β} x) proj_{0} proj_{a} val ++ proj_{b} val,
c = map (λx. proj_{β} x) proj_{1} proj_{a} val ++ proj_{c} val
>
Validated!
refine = { <a:[<>], b:[<>], c:[<>], d:[<>]> | len val.a + 2len val.b <= 3len val.c + len val.d }
simple = <a:<0:[<α:<1:<>, 2:<>, 3:<>>, β:<>>], 1:[<α:<>, β:<>>]>, b:<0:[<α:<1:<>, 2:<>, 3:<>>, β:<1:<>, 2:<>>>], 1:[<α:<>, β:<1:<>, 2:<>>>]>, c:[<>], d:[<>]>
i(val) = <
a = flatten_3 map (λx. proj_{α} x) proj_{0} proj_{a} val ++ map (λx. proj_{α} x) proj_{1} proj_{a} val,
b = flatten_3 map (λx. proj_{α} x) proj_{0} proj_{b} val ++ map (λx. proj_{α} x) proj_{1} proj_{b} val,
c = map (λx. proj_{β} x) proj_{0} proj_{a} val ++ flatten_2 map (λx. proj_{β} x) proj_{0} proj_{b} val ++ proj_{c} val,
d = map (λx. proj_{β} x) proj_{1} proj_{a} val ++ flatten_2 map (λx. proj_{β} x) proj_{1} proj_{b} val ++ proj_{d} val
>
Validated!
refine = { { <a:[<>], b:[<>]> | len val.a <= len val.b } | len val.b <= len val.a }
simple = <a:<0:[<α:<>, β:<>>]>, b:<>>
i(val) = <
a = map (λx. proj_{α} x) proj_{0} proj_{a} val,
b = map (λx. proj_{β} x) proj_{0} proj_{a} val
>
Validated!
refine = { { { <a:[<>], b:[<>], c:[<>]> | len val.a <= len val.b } | len val.b <= len val.c } | len val.c <= len val.a }
simple = <a:<0:<0:[<α:<α:<>, β:<>>, β:<>>]>>, b:<0:<>>, c:<>>
i(val) = <
a = map (λx. proj_{α} x) map (λx. proj_{α} x) proj_{0} proj_{0} proj_{a} val,
b = map (λx. proj_{β} x) map (λx. proj_{α} x) proj_{0} proj_{0} proj_{a} val ++ map (λx. proj_{α} x) [],
c = map (λx. proj_{β} x) proj_{0} proj_{0} proj_{a} val ++ map (λx. proj_{β} x) []
>
Validated!
refine = { <a:[<>], b:[<>]> | len val.a <= len val.b V len val.b <= len val.a }
simple = <a:<0:[<α:<>, β:<>>]>, b:[<>]> + <a:[<>], b:<0:[<α:<>, β:<>>]>>
i(val) = Case val of
Left x1 -> <
a = map (λx. proj_{α} x) proj_{0} proj_{a} x1,
b = map (λx. proj_{β} x) proj_{0} proj_{a} x1 ++ proj_{b} x1
>;
Right x2 -> <
a = map (λx. proj_{β} x) proj_{0} proj_{b} x2 ++ proj_{a} x2,
b = map (λx. proj_{α} x) proj_{0} proj_{b} x2
>
Validated!
refine = { <> + <> | match(Left T) }
simple = <>
i(val) = Left val
Validated!
refine = { <> + <> | match(Left T) V match(Right T) }
simple = <> + <>
i(val) = val
Validated!
refine = { <> + <> | match(Left T) V match(Right T) }
simple = <> + <>
i(val) = val
Validated!
refine = { [<>] | match([]) }
simple = <>
i(val) = []
Validated!
refine = { [<>] | match(T :: T) }
simple = <hd:<>, tl:[<>]>
i(val) = <>::proj_{tl} val
Validated!
refine = { [<> + <>] | match(match(Left T) :: match([])) }
simple = <hd:<>, tl:<>>
i(val) = Left <>::[]
Validated!
refine = { [<a:[<>], b:[<>]>] | match(len val.a <= len val.b :: len val <= 0) }
simple = <hd:<a:<0:[<α:<>, β:<>>]>, b:[<>]>, tl:<>>
i(val) = <
a = map (λx. proj_{α} x) proj_{0} proj_{a} proj_{hd} val,
b = map (λx. proj_{β} x) proj_{0} proj_{a} proj_{hd} val ++ proj_{b} proj_{hd} val
>::[]
Validated!