blob: 5a9622e1b9a321497cff76e3f3750db076d89ec2 (
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
|
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
typeStepDeterministic : TypeStep env a b -> TypeStep env a c -> b = c
typeRedDeterministic : TypeRed env a b -> TypeRed env a c -> Whnf b -> Whnf c -> b = c
termRedDeterministic : TermRed env t u a -> TermRed env t v b -> Whnf u -> Whnf v -> u = v
|
