blob: 9015d14d22a1524aafe87f44235201d04484bee5 (
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
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
|
module Core.Reduction
import Core.Environment
import Core.Declarative
import Core.Term
import Core.Term.NormalForm
import Core.Term.Substitution
import Core.Term.Thinned
import Core.Thinning
-- Definition ------------------------------------------------------------------
public export
data TermStep : Env n -> Term n -> Term n -> Term n -> Type where
AppStep :
TermStep env t u (Pi a b) ->
TermWf env v a ->
---
TermStep env (App t v) (App u v) (subst b $ Wkn (id _) :< pure v)
PiBeta :
TypeWf env a ->
TermWf (env :< pure a) t b ->
TermWf env u a ->
---
TermStep env
(App (Abs t) u)
(subst t $ Wkn (id _) :< pure u)
(subst b $ Wkn (id _) :< pure u)
ConvStep :
TermStep env t u a ->
TypeConv env a b ->
---
TermStep env t u b
public export
TypeStep : Env n -> Term n -> Term n -> Type
TypeStep env a b = TermStep env a b Set
public export
data ReflTransClosure : (refl : a -> Type) -> (step : a -> a -> Type) -> a -> a -> Type where
Refl :
{0 refl : a -> Type} ->
refl x ->
---
ReflTransClosure refl step x x
Step :
{0 step : a -> a -> Type} ->
step x y ->
ReflTransClosure refl step y z ->
---
ReflTransClosure refl step x z
public export
TypeReduce : Env n -> Term n -> Term n -> Type
TypeReduce env = ReflTransClosure (TypeWf env) (TypeStep env)
public export
TermReduce : Env n -> Term n -> Term n -> Term n -> Type
TermReduce env t u a = ReflTransClosure (\t => TermWf env t a) (\t, u => TermStep env t u a) t u
%name TermStep step
%name ReflTransClosure steps
-- Respects Environment Quotient -----------------------------------------------
export
termStepRespEq : TermStep env1 t u a -> env1 =~= env2 -> TermStep env2 t u a
termStepRespEq (AppStep step tmWf) prf =
AppStep
(termStepRespEq step prf)
(termWfRespEq tmWf prf)
termStepRespEq (PiBeta tyWf tmWf tmWf1) prf =
PiBeta
(typeWfRespEq tyWf prf)
(termWfRespEq tmWf $ prf :< Refl)
(termWfRespEq tmWf1 prf)
termStepRespEq (ConvStep step tyConv) prf =
ConvStep
(termStepRespEq step prf)
(typeConvRespEq tyConv prf)
export
typeStepRespEq : TypeStep env1 a b -> env1 =~= env2 -> TypeStep env2 a b
typeStepRespEq = termStepRespEq
export
typeRedRespEq : TypeReduce env1 a b -> env1 =~= env2 -> TypeReduce env2 a b
typeRedRespEq (Refl tyWf) prf = Refl (typeWfRespEq tyWf prf)
typeRedRespEq (Step step steps) prf = Step (typeStepRespEq step prf) (typeRedRespEq steps prf)
export
termRedRespEq : TermReduce env1 t u a -> env1 =~= env2 -> TermReduce env2 t u a
termRedRespEq (Refl tmWf) prf = Refl (termWfRespEq tmWf prf)
termRedRespEq (Step step steps) prf = Step (termStepRespEq step prf) (termRedRespEq steps prf)
-- Reduction Subsumed by Conversion --------------------------------------------
export
termStepImpliesConv : TermStep env t u a -> TermConv env t u a
termStepImpliesConv (AppStep step tmWf) = AppConv (termStepImpliesConv step) (ReflTm tmWf)
termStepImpliesConv (PiBeta tyWf tmWf tmWf1) = PiBeta tyWf tmWf tmWf1
termStepImpliesConv (ConvStep step tyConv) = ConvConv (termStepImpliesConv step) tyConv
export
typeStepImpliesConv : TypeStep env a b -> TypeConv env a b
typeStepImpliesConv = LiftConv . termStepImpliesConv
export
typeRedImpliesConv : TypeReduce env a b -> TypeConv env a b
typeRedImpliesConv (Refl tyWf) = ReflTy tyWf
typeRedImpliesConv (Step step steps) =
TransTy
(typeStepImpliesConv step)
(typeRedImpliesConv steps)
export
termRedImpliesConv : TermReduce env t u a -> TermConv env t u a
termRedImpliesConv (Refl tmWf) = ReflTm tmWf
termRedImpliesConv (Step step steps) =
TransTm
(termStepImpliesConv step)
(termRedImpliesConv steps)
-- Subject Typing --------------------------------------------------------------
export
termStepImpliesSubjectWf : TermStep env t u a -> TermWf env t a
termStepImpliesSubjectWf (AppStep step tmWf) = AppWf (termStepImpliesSubjectWf step) tmWf
termStepImpliesSubjectWf (PiBeta tyWf tmWf tmWf1) = AppWf (AbsWf tyWf tmWf) tmWf1
termStepImpliesSubjectWf (ConvStep step tyConv) = ConvWf (termStepImpliesSubjectWf step) tyConv
export
typeStepImpliesSubjectWf : TypeStep env a b -> TypeWf env a
typeStepImpliesSubjectWf = LiftWf . termStepImpliesSubjectWf
-- Whnfs Do Not Reduce ---------------------------------------------------------
export
whnfNoTermStep : Whnf t -> Not (TermStep env t u a)
whnfNoTermStep (Ntrl (App n)) (AppStep step tmWf) = whnfNoTermStep (Ntrl n) step
whnfNoTermStep (Ntrl (App n)) (PiBeta tyWf tmWf tmWf1) impossible
whnfNoTermStep n (ConvStep step tyConv) = whnfNoTermStep n step
export
whnfNoTypeStep : Whnf a -> Not (TypeStep env a b)
whnfNoTypeStep = whnfNoTermStep
export
whnfTypeRedStays : Whnf a -> TypeReduce env a b -> a = b
whnfTypeRedStays n (Refl tyWf) = Refl
whnfTypeRedStays n (Step step steps) = absurd (whnfNoTypeStep n step)
export
whnfTermRedStays : Whnf t -> TermReduce env t u a -> t = u
whnfTermRedStays n (Refl tmWf) = Refl
whnfTermRedStays n (Step step steps) = absurd (whnfNoTermStep n step)
|
