blob: 22a9a391c8959de1c44c9dbde2e6c061f5cee455 (
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
|
module Total.Term
import public Data.SnocList.Elem
import public Thinning
%prefix_record_projections off
infixr 10 ~>
public export
data Ty : Type where
N : Ty
(~>) : Ty -> Ty -> Ty
%name Ty ty
public export
data Term : SnocList Ty -> Ty -> Type where
Var : (i : Elem ty ctx) -> Term ctx ty
Abs : Term (ctx :< ty) ty' -> Term ctx (ty ~> ty')
App : {ty : Ty} -> Term ctx (ty ~> ty') -> Term ctx ty -> Term ctx ty'
Zero : Term ctx N
Suc : Term ctx N -> Term ctx N
Rec : Term ctx N -> Term ctx ty -> Term ctx (ty ~> ty) -> Term ctx ty
%name Term t, u, v
wkn : Term ctx ty -> ctx `Thins` ctx' -> Term ctx' ty
wkn (Var i) thin = Var (index thin i)
wkn (Abs t) thin = Abs (wkn t $ keep thin)
wkn (App t u) thin = App (wkn t thin) (wkn u thin)
wkn Zero thin = Zero
wkn (Suc t) thin = Suc (wkn t thin)
wkn (Rec t u v) thin = Rec (wkn t thin) (wkn u thin) (wkn v thin)
public export
data Terms : SnocList Ty -> SnocList Ty -> Type where
Base : ctx `Thins` ctx' -> Terms ctx' ctx
(:<) : Terms ctx' ctx -> Term ctx' ty -> Terms ctx' (ctx :< ty)
%name Terms sub
index : Terms ctx' ctx -> Elem ty ctx -> Term ctx' ty
index (Base thin) i = Var (index thin i)
index (sub :< t) Here = t
index (sub :< t) (There i) = index sub i
wknAll : Terms ctx' ctx -> ctx' `Thins` ctx'' -> Terms ctx'' ctx
wknAll (Base thin') thin = Base (thin . thin')
wknAll (sub :< t) thin = wknAll sub thin :< wkn t thin
export
subst : Term ctx ty -> Terms ctx' ctx -> Term ctx' ty
subst (Var i) sub = index sub i
subst (Abs t) sub = Abs (subst t $ wknAll sub (Drop Id) :< Var Here)
subst (App t u) sub = App (subst t sub) (subst u sub)
subst Zero sub = Zero
subst (Suc t) sub = Suc (subst t sub)
subst (Rec t u v) sub = Rec (subst t sub) (subst u sub) (subst v sub)
restrict : Terms ctx'' ctx' -> ctx `Thins` ctx' -> Terms ctx'' ctx
restrict (Base thin') thin = Base (thin' . thin)
restrict (sub :< t) Id = sub :< t
restrict (sub :< t) (Drop thin) = restrict sub thin
restrict (sub :< t) (Keep thin) = restrict sub thin :< t
(.) : Terms ctx'' ctx' -> Terms ctx' ctx -> Terms ctx'' ctx
sub2 . (Base thin) = restrict sub2 thin
sub2 . (sub1 :< t) = sub2 . sub1 :< subst t sub2
|
