blob: 6846d8028a2eeb0e23b852325272096678ebe590 (
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
|
module Core.Term.Substitution
import Core.Term
import Core.Term.Thinned
import Core.Thinning
infix 4 =~=
-- Definition ------------------------------------------------------------------
public export
data Subst : Nat -> Nat -> Type where
Wkn : m `Thins` n -> Subst m n
(:<) : Subst m n -> Thinned n -> Subst (S m) n
namespace Eq
public export
data (=~=) : Subst m n -> Subst m n -> Type where
Refl : sub =~= sub
(:<) : sub1 =~= sub2 -> t =~= u -> sub1 :< t =~= sub2 :< u
%name Subst sub
%name Eq.(=~=) prf
-- Indexing --------------------------------------------------------------------
public export
index : Subst m n -> Fin m -> Thinned n
index (Wkn thin) i = Var i `Over` thin
index (sub :< t) FZ = t
index (sub :< t) (FS i) = index sub i
-- Weakening -------------------------------------------------------------------
public export
wkn : Subst k m -> m `Thins` n -> Subst k n
wkn (Wkn thin') thin = Wkn (thin . thin')
wkn (sub :< t) thin = wkn sub thin :< wkn t thin
-- Constructors ----------------------------------------------------------------
public export
lift : Subst m n -> Subst (S m) (S n)
lift sub = wkn sub (drop $ id n) :< (Var 0 `Over` id (S n))
-- Substitution ----------------------------------------------------------------
public export
subst : Term m -> Subst m n -> Term n
subst (Var i) sub = expand $ index sub i
subst Set sub = Set
subst (Pi t u) sub = Pi (subst t sub) (subst u $ lift sub)
subst (Abs t) sub = Abs (subst t $ lift sub)
subst (App t u) sub = App (subst t sub) (subst u sub)
|
