blob: 40829f342b7f7e817b68df5536f3483635d3881e (
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
|
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)
|
