blob: 00abc31ab519eafb30a5678f6372c1c3cc7acf27 (
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
|
module Total.Term.CoDebruijn
import public Data.SnocList.Elem
import public Thinning
import Syntax.PreorderReasoning
import Total.Term
%prefix_record_projections off
public export
data CoTerm : Ty -> SnocList Ty -> Type where
Var : CoTerm ty [<ty]
Abs : Binds [<ty] (CoTerm ty') ctx -> CoTerm (ty ~> ty') ctx
App : {ty : Ty} -> Pair (CoTerm (ty ~> ty')) (CoTerm ty) ctx -> CoTerm ty' ctx
Zero : CoTerm N [<]
Suc : CoTerm N ctx -> CoTerm N ctx
Rec : Pair (CoTerm N) (Pair (CoTerm ty) (CoTerm (ty ~> ty))) ctx -> CoTerm ty ctx
%name CoTerm t, u, v
public export
FullTerm : Ty -> SnocList Ty -> Type
FullTerm ty ctx = Thinned (CoTerm ty) ctx
export
var : Len ctx => Elem ty ctx -> FullTerm ty ctx
var i = Var `Over` point i
export
abs : FullTerm ty' (ctx :< ty) -> FullTerm (ty ~> ty') ctx
abs = map Abs . MkBound (S Z)
export
app : {ty : Ty} -> FullTerm (ty ~> ty') ctx -> FullTerm ty ctx -> FullTerm ty' ctx
app t u = map App (MkPair t u)
export
zero : Len ctx => FullTerm N ctx
zero = Zero `Over` empty
export
suc : FullTerm N ctx -> FullTerm N ctx
suc = map Suc
export
rec : FullTerm N ctx -> FullTerm ty ctx -> FullTerm (ty ~> ty) ctx -> FullTerm ty ctx
rec t u v = map Rec $ MkPair t (MkPair u v)
export
wkn : FullTerm ty ctx -> ctx `Thins` ctx' -> FullTerm ty ctx'
wkn (t `Over` thin) thin' = t `Over` thin' . thin
public export
data CoTerms : SnocList Ty -> SnocList Ty -> Type where
Base : ctx `Thins` ctx' -> CoTerms ctx ctx'
(:<) : CoTerms ctx ctx' -> FullTerm ty ctx' -> CoTerms (ctx :< ty) ctx'
%name CoTerms sub
export
shift : CoTerms ctx ctx' -> CoTerms ctx (ctx' :< ty)
shift (Base thin) = Base (Drop thin)
shift (sub :< (t `Over` thin)) = shift sub :< (t `Over` Drop thin)
export
lift : Len ctx' => CoTerms ctx ctx' -> CoTerms (ctx :< ty) (ctx' :< ty)
lift sub = shift sub :< var Here
export
restrict : CoTerms ctx' ctx'' -> ctx `Thins` ctx' -> CoTerms ctx ctx''
restrict (Base thin') thin = Base (thin' . thin)
restrict (sub :< t) (Drop thin) = restrict sub thin
restrict (sub :< t) (Keep thin) = restrict sub thin :< t
export
subst : Len ctx' => FullTerm ty ctx -> CoTerms ctx ctx' -> FullTerm ty ctx'
subst' : Len ctx' => CoTerm ty ctx -> CoTerms ctx ctx' -> FullTerm ty ctx'
subst (t `Over` thin) sub = subst' t (restrict sub thin)
subst' t (Base thin) = t `Over` thin
subst' Var (sub :< t) = t
subst' (Abs (MakeBound t (Drop Empty))) sub@(_ :< _) = abs (subst' t $ shift sub)
subst' (Abs (MakeBound t (Keep Empty))) sub@(_ :< _) = abs (subst' t $ lift sub)
subst' (App (MakePair t u _)) sub@(_ :< _) = app (subst t sub) (subst u sub)
subst' (Suc t) sub@(_ :< _) = suc (subst' t sub)
subst' (Rec (MakePair t (MakePair u v _ `Over` thin) _)) sub@(_ :< _) =
rec (subst t sub) (subst u (restrict sub thin)) (subst v (restrict sub thin))
toTerm : CoTerm ty ctx -> ctx `Thins` ctx' -> Term ctx' ty
toTerm Var thin = Var (index thin Here)
toTerm (Abs (MakeBound t (Drop Empty))) thin = Abs (toTerm t (Drop thin))
toTerm (Abs (MakeBound t (Keep Empty))) thin = Abs (toTerm t (Keep thin))
toTerm (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin =
App (toTerm t (thin . thin1)) (toTerm u (thin . thin2))
toTerm Zero thin = Zero
toTerm (Suc t) thin = Suc (toTerm t thin)
toTerm
(Rec
(MakePair
(t `Over` thin1)
(MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin') _))
thin =
Rec
(toTerm t (thin . thin1))
(toTerm u ((thin . thin') . thin2))
(toTerm v ((thin . thin') . thin3))
export
Cast (FullTerm ty ctx) (Term ctx ty) where
cast (t `Over` thin) = toTerm t thin
|
