blob: 7bbd524d23110865a638f78c49f55c75560a167c (
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
|
module Inky.Term.Rename
import Inky.Term
import Flap.Data.List
import Flap.Data.SnocList.Thinning
public export
data Thins : Mode -> Mode -> Type where
NoSugar : NoSugar `Thins` NoSugar
Sugar : qtCtx1 `Thins` qtCtx2 -> Sugar qtCtx1 `Thins` Sugar qtCtx2
Quote : ctx2 `Thins` ctx3 -> Quote ctx1 ctx2 `Thins` Quote ctx1 ctx3
export
rename :
mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
Term mode meta tyCtx tmCtx ->
Term mode' meta tyCtx tmCtx'
renameList :
mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
List (Term mode meta tyCtx tmCtx) ->
List (Term mode' meta tyCtx tmCtx')
renameAll :
mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
(ts : Context (Term mode meta tyCtx tmCtx)) ->
All (Assoc0 $ Term mode' meta tyCtx tmCtx') ts.names
renameBranches :
mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
(ts : Context (x ** Term mode meta tyCtx (tmCtx :< x))) ->
All (Assoc0 (x ** Term mode' meta tyCtx (tmCtx' :< x))) ts.names
renameTy' :
mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
Ty' mode meta tyCtx tmCtx ->
Ty' mode' meta tyCtx tmCtx'
renameBoundTy' :
mode `Thins` mode' -> tmCtx `Thins` tmCtx' ->
BoundTy' mode meta tyCtx tmCtx ->
BoundTy' mode' meta tyCtx tmCtx'
rename f g (Annot m e a) = Annot m (rename f g e) (renameTy' f g a)
rename f g (Var m i) = Var m (index g i)
rename f g (Let m e (x ** t)) = Let m (rename f g e) (x ** rename f (Keep g) t)
rename f g (LetTy m a (x ** t)) =
case f of
NoSugar => LetTy m a (x ** rename f g t)
Sugar _ => LetTy m a (x ** rename f g t)
rename f g (Abs m (bound ** t)) = Abs m (bound ** rename f (g <>< lengthOf bound) t)
rename f g (App m e ts) = App m (rename f g e) (renameList f g ts)
rename f g (Tup m (MkRow ts fresh)) = Tup m (fromAll (renameAll f g ts) fresh)
rename f g (Prj m e l) = Prj m (rename f g e) l
rename f g (Inj m l t) = Inj m l (rename f g t)
rename f g (Case m e (MkRow ts fresh)) =
Case m (rename f g e) (fromAll (renameBranches f g ts) fresh)
rename f g (Roll m t) = Roll m (rename f g t)
rename f g (Unroll m e) = Unroll m (rename f g e)
rename f g (Fold m e (x ** t)) = Fold m (rename f g e) (x ** rename f (Keep g) t)
rename f g (Map m a b c) = Map m (renameBoundTy' f g a) (renameTy' f g b) (renameTy' f g c)
rename (Sugar f) g (QuasiQuote m t) = QuasiQuote m (rename (Quote g) f t)
rename (Quote f) g (Unquote m t) = Unquote m (rename (Sugar g) f t)
rename (Sugar f) g (QAbs m (bound ** t)) =
QAbs m (bound ** rename (Sugar (f <>< lengthOf bound)) g t)
rename (Sugar f) g (Lit m k) = Lit m k
rename (Sugar f) g (Suc m t) = Suc m (rename (Sugar f) g t)
rename (Sugar f) g (List m ts) = List m (renameList (Sugar f) g ts)
rename (Sugar f) g (Cons m t u) = Cons m (rename (Sugar f) g t) (rename (Sugar f) g u)
rename (Sugar f) g (Str m str) = Str m str
rename (Sugar f) g (FoldCase m e (MkRow ts fresh)) =
FoldCase m (rename (Sugar f) g e) (fromAll (renameBranches (Sugar f) g ts) fresh)
renameList f g [] = []
renameList f g (t :: ts) = rename f g t :: renameList f g ts
renameAll f g [<] = [<]
renameAll f g (ts :< (x :- t)) = renameAll f g ts :< (x :- rename f g t)
renameBranches f g [<] = [<]
renameBranches f g (ts :< (l :- (x ** t))) =
renameBranches f g ts :< (l :- (x ** rename f (Keep g) t))
renameTy' NoSugar g a = a
renameTy' (Sugar f) g a = a
renameTy' (Quote f) g t = rename (Sugar g) f t
renameBoundTy' NoSugar g xa = xa
renameBoundTy' (Sugar f) g xa = xa
renameBoundTy' (Quote f) g t = rename (Sugar g) f t
|
