blob: 18069041de2130ad16459b5436e58e5390248a86 (
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
112
113
114
115
116
117
118
119
120
|
module CC.Term
import CC.Name
import CC.Thinning
-- Definition ------------------------------------------------------------------
public export
Context : Type
Context = SnocList Name
public export
data IsVar : Nat -> Name -> Context -> Type where
Here : (eq : m ~~ n) -> IsVar 0 m (ctx :< n)
There : IsVar k n ctx -> IsVar (S k) n (ctx :< _)
public export
data Term : Context -> Type where
Var : (k : Nat) -> (0 n : Name) -> (0 prf : IsVar k n ctx) -> Term ctx
Abs : (n : Name) -> Term (ctx :< n) -> Term ctx
App : Term ctx -> Term ctx -> Term ctx
Let : (n : Name) -> Term ctx -> Term (ctx :< n) -> Term ctx
public export
data Value : Context -> Type
public export
data Neutral : Context -> Type
public export
data Closure : Context -> Type
public export
data Env : (local, global : Context) -> Type where
Lin : Env [<] global
(:<) : Env local global -> (p : (Name, Lazy (Value global))) -> Env (local :< fst p) global
data Closure : Context -> Type where
Close : (n : Name) -> Env local global -> Term (local :< n) -> Closure global
data Value where
Ntrl : Neutral ctx -> Value ctx
VAbs : Closure ctx -> Value ctx
data Neutral where
VVar : (k : Nat) -> (0 n : Name) -> (0 prf : IsVar k n ctx) -> Neutral ctx
VApp : Neutral ctx -> Lazy (Value ctx) -> Neutral ctx
%name IsVar prf
%name Term t, u
%name Value v
%name Neutral n
%name Closure close
%name Env env
-- Operations ------------------------------------------------------------------
export
index : Env local global -> (k : Nat) -> (0 prf : IsVar k n local) -> Value global
index (env :< (n, v)) 0 (Here eq) = v
index (env :< _) (S k) (There prf) = index env k prf
-- Weakening -------------------------------------------------------------------
wknVar' :
forall src, tgt.
{0 thin : src `Thins` tgt} ->
(k : Nat) ->
(0 prf : IsVar k n src) ->
View thin ->
Nat
wknVar' k prf (Drop thin) = S (wknVar' k prf (view thin))
wknVar' 0 (Here eq) (Keep thin) = 0
wknVar' (S k) (There prf) (Keep thin) = S (wknVar' k prf (view thin))
wknIsVar' :
forall src, tgt, k.
{0 thin : src `Thins` tgt} ->
(prf : IsVar k n src) ->
(view : View thin) ->
IsVar (wknVar' k prf view) n tgt
wknIsVar' prf (Drop thin) = There (wknIsVar' prf (view thin))
wknIsVar' (Here eq) (Keep thin) = Here eq
wknIsVar' (There prf) (Keep thin) = There (wknIsVar' prf (view thin))
export
wknVar : src `Thins` tgt -> {k : Nat} -> (0 prf : IsVar k n src) -> Nat
wknVar thin {k} prf = wknVar' k prf (view thin)
export
wknIsVar :
(prf : IsVar k n src) ->
(thin : src `Thins` tgt) ->
IsVar (wknVar thin prf) n tgt
wknIsVar prf thin = wknIsVar' prf (view thin)
export
wknTerm : Term src -> src `Thins` tgt -> Term tgt
wknTerm (Var k n prf) thin = Var (wknVar thin prf) n (wknIsVar prf thin)
wknTerm (Abs n t) thin = Abs n (wknTerm t (keep thin))
wknTerm (App t u) thin = App (wknTerm t thin) (wknTerm u thin)
wknTerm (Let n t u) thin = Let n (wknTerm t thin) (wknTerm u (keep thin))
export
wknNtrl : Neutral src -> src `Thins` tgt -> Neutral tgt
export
wknVal : Value src -> src `Thins` tgt -> Value tgt
export
wknClose : Closure src -> src `Thins` tgt -> Closure tgt
export
wknEnv : Env local src -> src `Thins` tgt -> Env local tgt
wknNtrl (VVar k n prf) thin = VVar (wknVar thin prf) n (wknIsVar prf thin)
wknNtrl (VApp n v) thin = VApp (wknNtrl n thin) (wknVal v thin)
wknVal (Ntrl n) thin = Ntrl (wknNtrl n thin)
wknVal (VAbs close) thin = VAbs (wknClose close thin)
wknClose (Close n env t) thin = Close n (wknEnv env thin) t
wknEnv [<] thin = [<]
wknEnv (env :< (n, v)) thin = wknEnv env thin :< (n, wknVal v thin)
|
