blob: 21e6ee53a8d482198fe4c383a9f12d6b3f6be387 (
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
|
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
typeStepImpliesTypeConv : TypeStep env a b -> TypeConv env a b
typeRedImpliesTypeConv : TypeRed env a b -> TypeConv env a b
termRedImpliesTermConv : TermRed env t u a -> TermConv env t u a
-- Subject Typing --------------------------------------------------------------
termStepImpliesSubjectWf : TermStep env t u a -> TermWf env t a
typeStepImpliesSubjectWf : TypeStep env a b -> TypeWf env a
-- Whnfs Do Not Reduce ---------------------------------------------------------
-- Cannot step from whnf
termStepWhnfImpossible : Whnf t -> Not (TermStep env t u a)
typeStepWhnfImpossible : Whnf a -> Not (TypeStep env a b)
-- Reduction starting from whnf goes nowhere
typeRedWhnfStays : Whnf a -> TypeRed env a b -> a = b
termRedWhnfStays : Whnf t -> TermRed env t u a -> t = u
-- 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
|
