blob: b6e2eb0239ef3c90834581fc416af3ef3174ffe3 (
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
|
module Core.Reduction
import Core.Environment
import Core.Declarative
import Core.Term
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)
|
