blob: b50b8c22917a8279a461030072c96581691d7fc1 (
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
|
module Core.Reduction
import Core.Context
import Core.Declarative
import Core.Term
import Core.Term.Environment
import Core.Term.NormalForm
import Core.Term.Substitution
public export
data TermStep : Env sx -> Term sx -> Term sx -> Term sx -> Type where
PiBeta :
TypeWf env f ->
TermWf (env :< f) t g ->
TermWf env u f ->
---
TermStep env (App (Abs n t) u) (subst t $ sub1 u) (subst g $ sub1 u)
AppStep :
TermStep env t u (Pi n f g) ->
TermWf env a f ->
---
TermStep env (App t a) (App u a) (subst g $ sub1 a)
StepConv :
TermStep env t u a ->
TypeConv env a b ->
---
TermStep env t u b
public export
TypeStep : Env sx -> Term sx -> Term sx -> Type
TypeStep env a b = TermStep env a b Set
namespace Type
public export
data TypeRed : Env sx -> Term sx -> Term sx -> Type where
Stay : TypeWf env a -> TypeRed env a a
(::) : TypeStep env a b -> TypeRed env b c -> TypeRed env a c
namespace Term
public export
data TermRed : Env sx -> Term sx -> Term sx -> Term sx -> Type where
Stay : TermWf env t a -> TermRed env t t a
(::) : TermStep env t u a -> TermRed env u v a -> TermRed env t v a
%name TypeStep step
%name TermStep step
%name TypeRed steps
%name TermRed steps
-- Reduction Subsumed by Conversion --------------------------------------------
termStepImpliesTermConv : TermStep env t u a -> TermConv env t u a
termStepImpliesTermConv (PiBeta wf wf1 wf2) = PiBeta wf wf1 wf2
termStepImpliesTermConv (AppStep step wf) = AppConv (termStepImpliesTermConv step) (ReflTerm wf)
termStepImpliesTermConv (StepConv step conv) = ConvTermConv (termStepImpliesTermConv step) conv
typeStepImpliesTypeConv : TypeStep env a b -> TypeConv env a b
typeStepImpliesTypeConv step = LiftConv (termStepImpliesTermConv step)
typeRedImpliesTypeConv : TypeRed env a b -> TypeConv env a b
typeRedImpliesTypeConv (Stay wf) = ReflType wf
typeRedImpliesTypeConv (step :: steps) =
TransType
(typeStepImpliesTypeConv step)
(typeRedImpliesTypeConv steps)
termRedImpliesTermConv : TermRed env t u a -> TermConv env t u a
termRedImpliesTermConv (Stay wf) = ReflTerm wf
termRedImpliesTermConv (step :: steps) =
TransTerm
(termStepImpliesTermConv step)
(termRedImpliesTermConv steps)
-- Subject Typing --------------------------------------------------------------
termStepImpliesSubjectWf : TermStep env t u a -> TermWf env t a
termStepImpliesSubjectWf (PiBeta wf wf1 wf2) = AppTerm (AbsTerm wf wf1) wf2
termStepImpliesSubjectWf (AppStep step wf) = AppTerm (termStepImpliesSubjectWf step) wf
termStepImpliesSubjectWf (StepConv step conv) = ConvTerm (termStepImpliesSubjectWf step) conv
typeStepImpliesSubjectWf : TypeStep env a b -> TypeWf env a
typeStepImpliesSubjectWf step = LiftType (termStepImpliesSubjectWf step)
-- Whnfs Do Not Reduce ---------------------------------------------------------
-- Cannot step from whnf
termStepWhnfImpossible : Whnf t -> Not (TermStep env t u a)
termStepWhnfImpossible n (StepConv step conv) = termStepWhnfImpossible n step
termStepWhnfImpossible (Ntrl (App n)) (PiBeta wf wf1 wf2) impossible
termStepWhnfImpossible (Ntrl (App n)) (AppStep step wf) = termStepWhnfImpossible (Ntrl n) step
typeStepWhnfImpossible : Whnf a -> Not (TypeStep env a b)
typeStepWhnfImpossible = termStepWhnfImpossible
-- Reduction starting from whnf goes nowhere
typeRedWhnfStays : Whnf a -> TypeRed env a b -> a = b
typeRedWhnfStays n (Stay wf) = Refl
typeRedWhnfStays n (step :: steps) = absurd $ typeStepWhnfImpossible n step
termRedWhnfStays : Whnf t -> TermRed env t u a -> t = u
termRedWhnfStays n (Stay wf) = Refl
termRedWhnfStays n (step :: steps) = absurd $ termStepWhnfImpossible n step
-- Reduction is Deterministic --------------------------------------------------
termStepDeterministic : TermStep env t u a -> TermStep env t v b -> u = v
termStepDeterministic (StepConv step conv) step1 = termStepDeterministic step step1
termStepDeterministic step (StepConv step1 conv) = termStepDeterministic step step1
termStepDeterministic (PiBeta _ _ _) (PiBeta _ _ _) = Refl
termStepDeterministic (PiBeta _ _ _) (AppStep step _) = absurd $ termStepWhnfImpossible Abs step
termStepDeterministic (AppStep step _) (PiBeta _ _ _) = absurd $ termStepWhnfImpossible Abs step
termStepDeterministic (AppStep step _) (AppStep step1 _) =
cong (flip App _) $
termStepDeterministic step step1
typeStepDeterministic : TypeStep env a b -> TypeStep env a c -> b = c
typeStepDeterministic = termStepDeterministic
typeRedDeterministic : TypeRed env a b -> TypeRed env a c -> Whnf b -> Whnf c -> b = c
typeRedDeterministic (Stay _) red n m = typeRedWhnfStays n red
typeRedDeterministic red (Stay _) n m = sym $ typeRedWhnfStays m red
typeRedDeterministic (step :: steps) (step1 :: steps1) n m =
let steps1' = rewrite typeStepDeterministic step step1 in steps1 in
typeRedDeterministic steps steps1' n m
termRedDeterministic : TermRed env t u a -> TermRed env t v b -> Whnf u -> Whnf v -> u = v
termRedDeterministic (Stay _) red n m = termRedWhnfStays n red
termRedDeterministic red (Stay _) n m = sym $ termRedWhnfStays m red
termRedDeterministic (step :: steps) (step1 :: steps1) n m =
let steps1' : TermRed env _ v b = rewrite termStepDeterministic step step1 in steps1 in
termRedDeterministic steps steps1' n m
|
