blob: 248c44fe7ad9fbaa574c2bacb3af56f4c0d3a15d (
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
|
module Core.Term.Substitution
import Core.Context
import Core.Var
import Core.Term
import Core.Thinning
-- Definition ------------------------------------------------------------------
public export
data Subst : Context -> Context -> Type where
Base : sx `Thins` sy -> Subst sx sy
(:<) : Subst sx sy -> (sz `Thins` sy, Term sz) -> Subst (sx :< x) sy
%name Subst sub
-- Constructors ----------------------------------------------------------------
public export
sub1 : Term sx -> Subst (sx :< n) sx
sub1 t = Base (id sx) :< (id sx, t)
-- Operations ------------------------------------------------------------------
export
index : Subst sx sy -> Var sx -> Term sy
doIndex : Subst sx sy -> (sz `Thins` sy, Term sz) -> {0 i : Var (sx :< n)} -> View i -> Term sy
index (Base thin) i = Var $ wkn i thin
index (sub :< p) i = doIndex sub p (view i)
doIndex sub (thin, t) Here = wkn t thin
doIndex sub p (There i) = index sub i
public export
wkn : Subst sx sy -> sy `Thins` sz -> Subst sx sz
wkn (Base thin') thin = Base (thin . thin')
wkn (sub :< (thin', t)) thin = wkn sub thin :< (thin . thin', t)
public export
lift : Subst sx sy -> (0 n : Name) -> Subst (sx :< n) (sy :< n)
lift sub n = wkn sub (drop (id sy) n) :< (id _, Var here)
public export
subst : Term sx -> Subst sx sy -> Term sy
subst (Var i) sub = index sub i
subst Set sub = Set
subst (Pi n t u) sub = Pi n (subst t sub) (subst u $ lift sub n)
subst (Abs n t) sub = Abs n (subst t $ lift sub n)
subst (App t u) sub = App (subst t sub) (subst u sub)
|
