blob: 690e38cae0aeba89b85f3605ff2989090cd50f05 (
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
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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
|
module Inky.Term.Substitution
import Data.List.Quantifiers
import Inky.Data.List
import Inky.Term
public export
thin : ctx1 `Thins` ctx2 -> Term mode m tyCtx ctx1 -> Term mode m tyCtx ctx2
public export
thinList : ctx1 `Thins` ctx2 -> List (Term mode m tyCtx ctx1) -> List (Term mode m tyCtx ctx2)
public export
thinAll : ctx1 `Thins` ctx2 -> Context (Term mode m tyCtx ctx1) -> Context (Term mode m tyCtx ctx2)
public export
thinAllNames :
(f : ctx1 `Thins` ctx2) -> (ts : Context (Term mode m tyCtx ctx1)) ->
(thinAll f ts).names = ts.names
public export
thinBranches :
ctx1 `Thins` ctx2 ->
Context (x ** Term mode m tyCtx (ctx1 :< x)) ->
Context (x ** Term mode m tyCtx (ctx2 :< x))
public export
thinBranchesNames :
(f : ctx1 `Thins` ctx2) -> (ts : Context (x ** Term mode m tyCtx (ctx1 :< x))) ->
(thinBranches f ts).names = ts.names
thin f (Annot meta t a) = Annot meta (thin f t) a
thin f (Var meta i) = Var meta (index f i)
thin f (Let meta e (x ** t)) = Let meta (thin f e) (x ** thin (Keep f) t)
thin f (LetTy meta a (x ** t)) = LetTy meta a (x ** thin f t)
thin f (Abs meta (bound ** t)) = Abs meta (bound ** thin (f <>< lengthOf bound) t)
thin f (App meta e ts) = App meta (thin f e) (thinList f ts)
thin f (Tup meta (MkRow ts fresh)) =
Tup meta (MkRow (thinAll f ts) (rewrite thinAllNames f ts in fresh))
thin f (Prj meta e l) = Prj meta (thin f e) l
thin f (Inj meta l t) = Inj meta l (thin f t)
thin f (Case meta t (MkRow ts fresh)) =
Case meta (thin f t) (MkRow (thinBranches f ts) (rewrite thinBranchesNames f ts in fresh))
thin f (Roll meta t) = Roll meta (thin f t)
thin f (Unroll meta e) = Unroll meta (thin f e)
thin f (Fold meta e (x ** t)) = Fold meta (thin f e) (x ** thin (Keep f) t)
thin f (Map meta (x ** a) b c) = Map meta (x ** a) b c
thinList f [] = []
thinList f (t :: ts) = thin f t :: thinList f ts
thinAll f [<] = [<]
thinAll f (ts :< (l :- t)) = thinAll f ts :< (l :- thin f t)
thinAllNames f [<] = Refl
thinAllNames f (ts :< (l :- t)) = cong (:< l) $ thinAllNames f ts
thinBranches f [<] = [<]
thinBranches f (ts :< (l :- (x ** t))) = thinBranches f ts :< (l :- (x ** thin (Keep f) t))
thinBranchesNames f [<] = Refl
thinBranchesNames f (ts :< (l :- (x ** t))) = cong (:< l) $ thinBranchesNames f ts
public export
thinTy : ctx1 `Thins` ctx2 -> Term mode m ctx1 tmCtx -> Term mode m ctx2 tmCtx
public export
thinTyList : ctx1 `Thins` ctx2 -> List (Term mode m ctx1 tmCtx) -> List (Term mode m ctx2 tmCtx)
public export
thinTyAll : ctx1 `Thins` ctx2 -> Context (Term mode m ctx1 tmCtx) -> Context (Term mode m ctx2 tmCtx)
public export
thinTyAllNames :
(f : ctx1 `Thins` ctx2) -> (ts : Context (Term mode m ctx1 tmCtx)) ->
(thinTyAll f ts).names = ts.names
public export
thinTyBranches :
ctx1 `Thins` ctx2 ->
Context (x ** Term mode m ctx1 (tmCtx :< x)) ->
Context (x ** Term mode m ctx2 (tmCtx :< x))
public export
thinTyBranchesNames :
(f : ctx1 `Thins` ctx2) -> (ts : Context (x ** Term mode m ctx1 (tmCtx :< x))) ->
(thinTyBranches f ts).names = ts.names
thinTy f (Annot meta t a) = Annot meta (thinTy f t) (rename f a)
thinTy f (Var meta i) = Var meta i
thinTy f (Let meta e (x ** t)) = Let meta (thinTy f e) (x ** thinTy f t)
thinTy f (LetTy meta a (x ** t)) = LetTy meta (rename f a) (x ** thinTy (Keep f) t)
thinTy f (Abs meta (bound ** t)) = Abs meta (bound ** thinTy f t)
thinTy f (App meta e ts) = App meta (thinTy f e) (thinTyList f ts)
thinTy f (Tup meta (MkRow ts fresh)) =
Tup meta (MkRow (thinTyAll f ts) (rewrite thinTyAllNames f ts in fresh))
thinTy f (Prj meta e l) = Prj meta (thinTy f e) l
thinTy f (Inj meta l t) = Inj meta l (thinTy f t)
thinTy f (Case meta t (MkRow ts fresh)) =
Case meta (thinTy f t) (MkRow (thinTyBranches f ts) (rewrite thinTyBranchesNames f ts in fresh))
thinTy f (Roll meta t) = Roll meta (thinTy f t)
thinTy f (Unroll meta e) = Unroll meta (thinTy f e)
thinTy f (Fold meta e (x ** t)) = Fold meta (thinTy f e) (x ** thinTy f t)
thinTy f (Map meta (x ** a) b c) = Map meta (x ** rename (Keep f) a) (rename f b) (rename f c)
thinTyList f [] = []
thinTyList f (t :: ts) = thinTy f t :: thinTyList f ts
thinTyAll f [<] = [<]
thinTyAll f (ts :< (l :- t)) = thinTyAll f ts :< (l :- thinTy f t)
thinTyAllNames f [<] = Refl
thinTyAllNames f (ts :< (l :- t)) = cong (:< l) $ thinTyAllNames f ts
thinTyBranches f [<] = [<]
thinTyBranches f (ts :< (l :- (x ** t))) = thinTyBranches f ts :< (l :- (x ** thinTy f t))
thinTyBranchesNames f [<] = Refl
thinTyBranchesNames f (ts :< (l :- (x ** t))) = cong (:< l) $ thinTyBranchesNames f ts
public export
Env : Mode -> Type -> SnocList String -> SnocList String -> SnocList String -> Type
Env mode m tyCtx ctx1 ctx2 = All (Assoc0 $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
public export
Env' : Mode -> Type -> SnocList String -> List String -> SnocList String -> Type
Env' mode m tyCtx ctx1 ctx2 = All (Assoc0 $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
public export
thinEnv :
ctx2 `Thins` ctx3 ->
Env mode m tyCtx ctx1 ctx2 ->
Env mode m tyCtx ctx1 ctx3
thinEnv f = mapProperty (map $ bimap (index f) (thin $ f))
public export
lift :
Env mode m tyCtx ctx1 ctx2 ->
Env mode m tyCtx (ctx1 :< x) (ctx2 :< x)
lift f = thinEnv (Drop Id) f :< (x :- Left (%% x))
public export
sub :
Env mode m tyCtx ctx1 ctx2 ->
Term mode m tyCtx ctx1 -> Term mode m tyCtx ctx2
public export
subList :
Env mode m tyCtx ctx1 ctx2 ->
List (Term mode m tyCtx ctx1) -> List (Term mode m tyCtx ctx2)
public export
subAll :
Env mode m tyCtx ctx1 ctx2 ->
Context (Term mode m tyCtx ctx1) -> Context (Term mode m tyCtx ctx2)
public export
subAllNames :
(f : Env mode m tyCtx ctx1 ctx2) ->
(ts : Context (Term mode m tyCtx ctx1)) -> (subAll f ts).names = ts.names
public export
subBranches :
Env mode m tyCtx ctx1 ctx2 ->
Context (x ** Term mode m tyCtx (ctx1 :< x)) ->
Context (x ** Term mode m tyCtx (ctx2 :< x))
public export
subBranchesNames :
(f : Env mode m tyCtx ctx1 ctx2) ->
(ts : Context (x ** Term mode m tyCtx (ctx1 :< x))) -> (subBranches f ts).names = ts.names
public export
keepBound :
forall ctx. {0 bound : List String} ->
LengthOf bound -> Env' mode m tyCtx bound (ctx <>< bound)
keepBound Z = []
keepBound (S len) = (_ :- Left (index (dropFish Id len) (toVar Here))) :: keepBound len
sub f (Annot meta t a) = Annot meta (sub f t) a
sub f (Var meta i) = either (Var meta) id (indexAll i.pos f).value
sub f (Let meta e (x ** t)) = Let meta (sub f e) (x ** sub (lift f) t)
sub f (LetTy meta a (x ** t)) = LetTy meta a (x ** sub (mapProperty (map $ map $ thinTy (Drop Id)) f) t)
sub f (Abs meta (bound ** t)) =
let len = lengthOf bound in
Abs meta (bound ** sub (thinEnv (dropFish Id len) f <>< keepBound len) t)
sub f (App meta e ts) = App meta (sub f e) (subList f ts)
sub f (Tup meta (MkRow ts fresh)) =
Tup meta (MkRow (subAll f ts) (rewrite subAllNames f ts in fresh))
sub f (Prj meta e l) = Prj meta (sub f e) l
sub f (Inj meta l t) = Inj meta l (sub f t)
sub f (Case meta t (MkRow ts fresh)) =
Case meta (sub f t) (MkRow (subBranches f ts) (rewrite subBranchesNames f ts in fresh))
sub f (Roll meta t) = Roll meta (sub f t)
sub f (Unroll meta e) = Unroll meta (sub f e)
sub f (Fold meta e (x ** t)) = Fold meta (sub f e) (x ** sub (lift f) t)
sub f (Map meta (x ** a) b c) = Map meta (x ** a) b c
subList f [] = []
subList f (t :: ts) = sub f t :: subList f ts
subAll f [<] = [<]
subAll f (ts :< (l :- t)) = subAll f ts :< (l :- sub f t)
subAllNames f [<] = Refl
subAllNames f (ts :< (l :- t)) = cong (:< l) $ subAllNames f ts
subBranches f [<] = [<]
subBranches f (ts :< (l :- (x ** t))) = subBranches f ts :< (l :- (x ** sub (lift f) t))
subBranchesNames f [<] = Refl
subBranchesNames f (ts :< (l :- (x ** t))) = cong (:< l) $ subBranchesNames f ts
|
