-
Notifications
You must be signed in to change notification settings - Fork 0
/
NormalStoreProgress.agda
148 lines (126 loc) · 8.49 KB
/
NormalStoreProgress.agda
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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
module MonoRef.Dynamics.Simple.EvStore.NormalStoreProgress where
open import Data.Empty using (⊥-elim)
open import MonoRef.Dynamics.Simple.Coercions
open import MonoRef.Dynamics.Simple.Error
open import MonoRef.Dynamics.Simple.EvStore.CastProgress
open import MonoRef.Dynamics.Simple.EvStore.ProgressDef
open import MonoRef.Dynamics.Simple.EvStore.SReduction
open import MonoRef.Dynamics.Simple.EvStore.Store
open import MonoRef.Dynamics.Simple.Frames
open import MonoRef.Dynamics.Simple.Substitution
open import MonoRef.Dynamics.Simple.TargetWithoutBlame
open import MonoRef.Static.Context
open import MonoRef.Static.Types
progress-normal-store : ∀ {Σ A}
→ (e : Σ ∣ ∅ ⊢ A) → (μ : Store Σ) → NormalStore μ → Progress e μ
progress-normal-store (` ()) _ _
progress-normal-store (ƛ e) _ _ = done (V-ƛ e)
progress-normal-store (e₁ · e₂) ν μ-evd with progress-normal-store e₁ ν μ-evd
... | step (prog-reduce x e₁⟶e₁') = step (prog-reduce x (cong (ξ-appₗ e₂) e₁⟶e₁'))
... | step (cast-reduce e₁⟶e₁') = step (cast-reduce (cong (ξ-appₗ e₂) e₁⟶e₁'))
... | step (state-reduce ¬NS _) = ⊥-elim (¬NS μ-evd)
... | done v with progress-normal-store e₂ ν μ-evd
... | step (prog-reduce x e₂⟶e₂') = step (prog-reduce x (cong (ξ-appᵣ e₁) e₂⟶e₂'))
... | step (cast-reduce e₂⟶e₂') = step (cast-reduce (cong (ξ-appᵣ e₁) e₂⟶e₂'))
... | step (state-reduce ¬NS _) = ⊥-elim (¬NS μ-evd)
progress-normal-store (_ · _) _ μ-evd | done (V-ƛ _) | done v' =
step (prog-reduce μ-evd (β-pure (β-ƛ v')))
progress-normal-store (_ · _) _ μ-evd | done (V-cast v I-⇒) | done v' =
step (prog-reduce μ-evd (β-pure (β-ƛₚ v v')))
... | error E-error = step (prog-reduce μ-evd (cong-error (ξ-appᵣ e₁)))
progress-normal-store (.error · e₂) ν μ-evd | error E-error =
step (prog-reduce μ-evd (cong-error (ξ-appₗ e₂)))
progress-normal-store `zero _ _ = done V-zero
progress-normal-store (`suc e) ν μ-evd with progress-normal-store e ν μ-evd
... | step (prog-reduce x e⟶e') = step (prog-reduce x (cong ξ-suc e⟶e'))
... | step (cast-reduce e⟶e') = step (cast-reduce (cong ξ-suc e⟶e'))
... | step (state-reduce ¬NS _) = ⊥-elim (¬NS μ-evd)
... | done x = done (V-suc x)
... | error E-error = step (prog-reduce μ-evd (cong-error ξ-suc))
progress-normal-store (case p z s) ν μ-evd with progress-normal-store p ν μ-evd
... | step (prog-reduce μ-evd' e⟶e') =
step (prog-reduce μ-evd' (cong (ξ-caseₚ z s) e⟶e'))
... | step (cast-reduce e⟶e') = step (cast-reduce (cong (ξ-caseₚ z s) e⟶e'))
... | step (state-reduce ¬NS _) = ⊥-elim (¬NS μ-evd)
... | error E-error = step (prog-reduce μ-evd (cong-error (ξ-caseₚ z s)))
... | done V-zero = step (prog-reduce μ-evd (β-pure β-zero))
... | done (V-suc v) = step (prog-reduce μ-evd (β-pure (β-suc v)))
... | done (V-cast _ ())
progress-normal-store (ref A e) ν μ-evd with progress-normal-store e ν μ-evd
... | step (prog-reduce x e⟶e') = step (prog-reduce x (cong (ξ-ref A) e⟶e'))
... | step (cast-reduce e⟶e') = step (cast-reduce (cong (ξ-ref A) e⟶e'))
... | step (state-reduce ¬NS _) = ⊥-elim (¬NS μ-evd)
progress-normal-store {Σ = Σ} {A = Ref A} (ref A e) ν μ-evd | done v =
step (prog-reduce μ-evd (β-mono (β-ref v)))
... | error E-error = step (prog-reduce μ-evd (cong-error (ξ-ref A)))
progress-normal-store (e₁ `× e₂) ν μ-evd with progress-normal-store e₁ ν μ-evd
... | step (prog-reduce x e⟶e') = step (prog-reduce x (cong (ξ-×ₗ e₂) e⟶e'))
... | step (cast-reduce e⟶e') = step (cast-reduce (cong (ξ-×ₗ e₂) e⟶e'))
... | step (state-reduce ¬NS _) = ⊥-elim (¬NS μ-evd)
... | error E-error = step (prog-reduce μ-evd (cong-error (ξ-×ₗ e₂)))
... | done v₁ with progress-normal-store e₂ ν μ-evd
... | step (prog-reduce x e⟶e') = step (prog-reduce x (cong (ξ-×ᵣ e₁) e⟶e'))
... | step (cast-reduce e⟶e') = step (cast-reduce (cong (ξ-×ᵣ e₁) e⟶e'))
... | step (state-reduce ¬NS _) = ⊥-elim (¬NS μ-evd)
... | done v₂ = done (V-pair v₁ v₂)
... | error E-error = step (prog-reduce μ-evd (cong-error (ξ-×ᵣ e₁)))
progress-normal-store (π₁ e) ν μ-evd with progress-normal-store e ν μ-evd
... | step (prog-reduce x e⟶e') = step (prog-reduce x (cong ξ-πₗ e⟶e'))
... | step (cast-reduce e⟶e') = step (cast-reduce (cong ξ-πₗ e⟶e'))
... | step (state-reduce ¬NS _) = ⊥-elim (¬NS μ-evd)
... | done (V-pair v₁ v₂) = step (prog-reduce μ-evd (β-pure (β-π₁ v₁ v₂)))
... | done (V-cast _ ())
... | error E-error = step (prog-reduce μ-evd (cong-error ξ-πₗ))
progress-normal-store (π₂ e) ν μ-evd with progress-normal-store e ν μ-evd
... | step (prog-reduce x e⟶e') = step (prog-reduce x (cong ξ-πᵣ e⟶e'))
... | step (cast-reduce e⟶e') = step (cast-reduce (cong ξ-πᵣ e⟶e'))
... | step (state-reduce ¬NS _) = ⊥-elim (¬NS μ-evd)
... | done (V-pair v₁ v₂) = step (prog-reduce μ-evd (β-pure (β-π₂ v₁ v₂)))
... | done (V-cast _ ())
... | error E-error = step (prog-reduce μ-evd (cong-error ξ-πᵣ))
progress-normal-store (addr mem Σ'⊑Σ) _ _ = done (V-addr mem Σ'⊑Σ)
progress-normal-store ((!ₛ e) A-static) ν μ-evd with progress-normal-store e ν μ-evd
... | step (prog-reduce x e⟶e') = step (prog-reduce x (cong (ξ-!ₛ A-static) e⟶e'))
... | step (cast-reduce e⟶e') = step (cast-reduce (cong (ξ-!ₛ A-static) e⟶e'))
... | step (state-reduce ¬NS _) = ⊥-elim (¬NS μ-evd)
... | done v = step (prog-reduce μ-evd (β-mono (β-!ₛ v)))
... | error E-error = step (prog-reduce μ-evd (cong-error (ξ-!ₛ A-static)))
progress-normal-store ((e₁ :=ₛ e₂) A-static) ν μ-evd with progress-normal-store e₁ ν μ-evd
... | step (prog-reduce x e⟶e') = step (prog-reduce x (cong (ξ-:=ₛₗ A-static e₂) e⟶e'))
... | step (cast-reduce e⟶e') = step (cast-reduce (cong (ξ-:=ₛₗ A-static e₂) e⟶e'))
... | step (state-reduce ¬NS _) = ⊥-elim (¬NS μ-evd)
... | error E-error = step (prog-reduce μ-evd (cong-error (ξ-:=ₛₗ A-static e₂)))
... | done v₁ with progress-normal-store e₂ ν μ-evd
... | step (prog-reduce x e⟶e') = step (prog-reduce x (cong (ξ-:=ₛᵣ A-static e₁) e⟶e'))
... | step (cast-reduce e⟶e') = step (cast-reduce (cong (ξ-:=ₛᵣ A-static e₁) e⟶e'))
... | step (state-reduce ¬NS _) = ⊥-elim (¬NS μ-evd)
... | done v₂ = step (prog-reduce μ-evd (β-mono (β-:=ₛ v₁ v₂)))
... | error E-error = step (prog-reduce μ-evd (cong-error (ξ-:=ₛᵣ A-static e₁)))
progress-normal-store (! A x e) ν μ-evd with progress-normal-store e ν μ-evd
... | step (prog-reduce w e⟶e') = step (prog-reduce w (cong (ξ-! A x) e⟶e'))
... | step (cast-reduce e⟶e') = step (cast-reduce (cong (ξ-! A x) e⟶e'))
... | step (state-reduce ¬NS _) = ⊥-elim (¬NS μ-evd)
... | done v = step (prog-reduce μ-evd (β-mono (β-! x v)))
... | error E-error = step (prog-reduce μ-evd (cong-error (ξ-! A x)))
progress-normal-store (:= A x e₁ e₂) ν μ-evd with progress-normal-store e₁ ν μ-evd
... | step (prog-reduce w e⟶e') = step (prog-reduce w (cong (ξ-:=ₗ A x e₂) e⟶e'))
... | step (cast-reduce e⟶e') = step (cast-reduce (cong (ξ-:=ₗ A x e₂) e⟶e'))
... | step (state-reduce ¬NS _) = ⊥-elim (¬NS μ-evd)
... | error E-error = step (prog-reduce μ-evd (cong-error (ξ-:=ₗ A x e₂)))
... | done v₁ with progress-normal-store e₂ ν μ-evd
... | step (prog-reduce w e⟶e') = step (prog-reduce w (cong (ξ-:=ᵣ A x e₁) e⟶e'))
... | step (cast-reduce e⟶e') = step (cast-reduce (cong (ξ-:=ᵣ A x e₁) e⟶e'))
... | step (state-reduce ¬NS _) = ⊥-elim (¬NS μ-evd)
... | done v₂ = step (prog-reduce μ-evd (β-mono (β-:= x v₁ v₂)))
... | error E-error = step (prog-reduce μ-evd (cong-error (ξ-:=ᵣ A x e₁)))
progress-normal-store unit _ _ = done V-unit
progress-normal-store error _ _ = error E-error
progress-normal-store (e < c >) ν μ-evd with progress-normal-store e ν μ-evd
... | step (prog-reduce x e⟶e') = step (prog-reduce x (cong (ξ-<> c) e⟶e'))
... | step (cast-reduce e⟶e') = step (cast-reduce (cong (ξ-<> c) e⟶e'))
... | step (state-reduce ¬NS _) = ⊥-elim (¬NS μ-evd)
... | error E-error = step (prog-reduce μ-evd (cong-error (ξ-<> c)))
... | done v
with ⟶ᶜprogress v c ν
... | step s = step (cast-reduce s)
... | done x = done x