Skip to content

Commit c3105fb

Browse files
deyaaeldeendeyaaeldeen
committed
adding progress
1 parent 78118a4 commit c3105fb

File tree

6 files changed

+232
-18
lines changed

6 files changed

+232
-18
lines changed

‎MonoRef/Dynamics/Efficient/StdStore/Reduction.agda‎

Lines changed: 20 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -173,12 +173,23 @@ data _,_,_⟶_,_,_ {Σ T} : ∀ {Σ₁ Σ₂ Σ₃} {Σ₁⊑ₕΣ : Σ₁ ⊑
173173
⟶⟹rtti⊑Σ (prog-reduce red) = ⟶ₑ⟹rtti⊑Σ red
174174
⟶⟹rtti⊑Σ (state-reduce red) = from⊑ₕ (⟶ₛ⟹rtti⊑Σ red)
175175

176-
⟶⟹qst : ∀ {Σ Σ₁ Σ₂ Σ₃ A} {Q : List (SuspendedCast Σ)} {Q' : List (SuspendedCast Σ₂)}
177-
{Σ₁⊑ₕΣ : Σ₁ ⊑ₕ Σ} {Σ₃⊑ₕΣ₂ : Σ₃ ⊑ₕ Σ₂} {M : proj₁ (merge' Σ₁⊑ₕΣ Q) ∣ ∅ ⊢ A}
178-
{μ : Store (proj₁ (merge' Σ₁⊑ₕΣ Q)) Σ₁}
179-
{M' : proj₁ (merge' Σ₃⊑ₕΣ₂ Q') ∣ ∅ ⊢ A}
180-
{μ' : Store (proj₁ (merge' Σ₃⊑ₕΣ₂ Q')) Σ₃}
181-
→ Q , M , μ ⟶ Q' , M' , μ'
182-
→ QueueStoreTyping Σ₁⊑ₕΣ Q
183-
⟶⟹qst (prog-reduce red) = normal
184-
⟶⟹qst (state-reduce {Q = Q} {A∈Σ = A∈Σ} red) = evolving Q A∈Σ
176+
⟶ₑ⟹qst : ∀ {bc Σ Σ' A} {Q : List (SuspendedCast Σ')} {μ : Store Σ Σ}
177+
{μ' : Store (proj₁ (merge Q)) Σ'}
178+
{M : Σ ∣ ∅ ⊢ A} {M' : proj₁ (merge Q) ∣ ∅ ⊢ A}
179+
→ bc / M , μ ⟶ₑ Q , M' , μ'
180+
→ QueueStoreTyping ⊑ₕ-refl Q
181+
⟶ₑ⟹qst (switch red) = ⟶ₑ⟹qst red
182+
⟶ₑ⟹qst (β-pure _) = normal
183+
⟶ₑ⟹qst (β-mono red) = ⟶ᵢₘ⟹qst red
184+
⟶ₑ⟹qst (cast/succeed {c = c} v sc)
185+
with apply-cast ⊑ₕ-refl [] v c | sc
186+
... | _ | intro Q' v'
187+
with Q'
188+
... | [] = normal
189+
... | cast A∈Σ _ ∷ Q'' = evolving Q'' A∈Σ
190+
⟶ₑ⟹qst (cast/fail v sc) = normal
191+
⟶ₑ⟹qst compose-casts = normal
192+
⟶ₑ⟹qst (ξ F red) = ⟶ₑ⟹qst red
193+
⟶ₑ⟹qst (ξ-cast red) = ⟶ₑ⟹qst red
194+
⟶ₑ⟹qst (ξ-error ξ₁) = normal
195+
⟶ₑ⟹qst ξ-cast-error = normal

‎MonoRef/Dynamics/Efficient/StdStore/TypeSafety.agda‎

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
{-
2+
3+
MonoRef.Dynamics.Efficient.StdStore.TypeSafety assembles a proof of progress
4+
and provides the full type safety proof.
5+
6+
-}
7+
8+
module MonoRef.Dynamics.Efficient.StdStore.TypeSafety where
9+
10+
open import Data.List using (List ; _∷_ ; [])
11+
open import Data.Nat using (ℕ ; suc)
12+
open import Data.Product using (proj₁)
13+
open import Relation.Nullary using (yes ; no)
14+
15+
open import MonoRef.Dynamics.Efficient.Error
16+
open import MonoRef.Dynamics.Efficient.StdStore.SuspendedCast
17+
open import MonoRef.Dynamics.Efficient.StdStore.ReflTransClosure
18+
open import MonoRef.Dynamics.Efficient.StdStore.Reduction
19+
open import MonoRef.Dynamics.Efficient.StdStore.Store
20+
open import MonoRef.Dynamics.Efficient.StdStore.NormalStoreProgress
21+
open import MonoRef.Dynamics.Efficient.StdStore.ProgressDef
22+
open import MonoRef.Dynamics.Efficient.StdStore.ProgProgressDef
23+
open import MonoRef.Dynamics.Efficient.StdStore.SuspendedCastProgress hiding (Progress)
24+
open import MonoRef.Dynamics.Efficient.TargetWithoutBlame
25+
open import MonoRef.Static.Context
26+
27+
28+
progress : ∀ {Σ Σ₁ A} {Σ₁⊑ₕΣ : Σ₁ ⊑ₕ Σ}
29+
→ (Q : List (SuspendedCast Σ))
30+
→ QueueStoreTyping Σ₁⊑ₕΣ Q
31+
→ (M : proj₁ (merge' Σ₁⊑ₕΣ Q) ∣ ∅ ⊢ A)
32+
→ (μ : Store (proj₁ (merge' Σ₁⊑ₕΣ Q)) Σ₁)
33+
→ Progress Q M μ
34+
progress .[] normal e μ
35+
with progress-normal-store e μ
36+
... | step-d R = step (prog-reduce R)
37+
... | step-a R = step (prog-reduce R)
38+
... | done v = done v
39+
... | error x = error x
40+
progress {Σ₁⊑ₕΣ = Σ₁⊑ₕΣ} (cast A∈Σ B ∷ Q) (evolving Q A∈Σ) e μ
41+
with suspended-cast-progress Σ₁⊑ₕΣ A∈Σ B Q μ
42+
... | step R = step (state-reduce R)
43+
44+
data Gas : Set where
45+
gas : ℕ → Gas
46+
47+
data Finished {Σ A} (N : Σ ∣ ∅ ⊢ A) : Set where
48+
49+
done :
50+
Value N
51+
----------
52+
→ Finished N
53+
54+
error :
55+
Error N
56+
----------
57+
→ Finished N
58+
59+
diverge :
60+
----------
61+
Finished N
62+
63+
data TypeSafety {Σ Σ₁ A} {Σ₁⊑ₕΣ : Σ₁ ⊑ₕ Σ}
64+
(Q : List (SuspendedCast Σ))
65+
(L : proj₁ (merge' Σ₁⊑ₕΣ Q) ∣ ∅ ⊢ A)
66+
(μ : Store (proj₁ (merge' Σ₁⊑ₕΣ Q)) Σ₁) : Set where
67+
68+
intro : ∀ {Σ₂ Σ₃} {Σ₃⊑ₕΣ₂ : Σ₃ ⊑ₕ Σ₂} {Q' : List (SuspendedCast Σ₂)}
69+
{μ' : Store (proj₁ (merge' Σ₃⊑ₕΣ₂ Q')) Σ₃}
70+
{N : proj₁ (merge' Σ₃⊑ₕΣ₂ Q') ∣ ∅ ⊢ A}
71+
→ Q , L , μ ↠ Q' , N , μ'
72+
→ Finished N
73+
----------------
74+
→ TypeSafety Q L μ
75+
76+
type-safety : ∀ {Σ Σ₁ A} {Σ₁⊑ₕΣ : Σ₁ ⊑ₕ Σ}
77+
→ Gas
78+
→ (Q : List (SuspendedCast Σ))
79+
→ QueueStoreTyping Σ₁⊑ₕΣ Q
80+
→ (L : proj₁ (merge' Σ₁⊑ₕΣ Q) ∣ ∅ ⊢ A)
81+
→ (μ : Store (proj₁ (merge' Σ₁⊑ₕΣ Q)) Σ₁)
82+
→ TypeSafety Q L μ
83+
type-safety (gas 0) Q qst L μ = intro ↠-refl diverge
84+
type-safety (gas (suc x)) Q qst L μ
85+
with progress Q qst L μ
86+
... | done v = intro ↠-refl (done v)
87+
... | error err = intro ↠-refl (error err)
88+
... | step {Q' = Q'} {μ' = μ'} {N = N} red
89+
with type-safety (gas x) Q' {!!} N μ'
90+
... | intro steps fin = intro (↠-trans red steps) fin

‎MonoRef/Dynamics/Reduction/StdStore/MonoReduction.agda‎

Lines changed: 18 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ module MonoRef.Dynamics.Reduction.StdStore.MonoReduction
55
(Inert : ∀ {A B} → A ⟹ B → Set)
66
where
77

8-
open import Data.List using (List ; [] ; _∷ʳ_)
8+
open import Data.List using (List ; [] ; _∷ʳ_ ; _∷_)
99
open import Data.List.All using (map)
1010
open import Data.List.Membership.Propositional using (_∈_)
1111
open import Data.Product using (proj₁ ; proj₂)
@@ -147,3 +147,20 @@ module ParamMonoReduction
147147
⟶ᵢₘ⟹Σ'⊑Σ (β-:= _ _ _ c) = from⊑ₕ (proj₂ (merge (proj₁ (get-val-from-successful-cast c))))
148148
⟶ᵢₘ⟹Σ'⊑Σ (β-:=/failed _ _ _ _) = StoreTypingProgress-refl
149149
⟶ᵢₘ⟹Σ'⊑Σ {Σ} {A = Ref A} (β-ref _) = from⊑ₗ (∷ʳ-⊒ A Σ)
150+
151+
⟶ᵢₘ⟹qst : ∀ {Σ Σ' A} {Q : List (SuspendedCast Σ')} {μ : Store Σ Σ}
152+
{μ' : Store (proj₁ (merge Q)) Σ'}
153+
{M : Σ ∣ ∅ ⊢ A} {M' : proj₁ (merge Q) ∣ ∅ ⊢ A}
154+
→ M , μ ⟶ᵢₘ Q , M' , μ'
155+
→ QueueStoreTyping ⊑ₕ-refl Q
156+
⟶ᵢₘ⟹qst (β-!ₛ _) = normal
157+
⟶ᵢₘ⟹qst (β-! _ _) = normal
158+
⟶ᵢₘ⟹qst (β-:=ₛ _ _) = normal
159+
⟶ᵢₘ⟹qst {μ = μ} (β-:= {B = B} _ R V c)
160+
with apply-cast ⊑ₕ-refl [] V (make-coercion B (store-lookup-rtti/ref R μ)) | c
161+
... | _ | intro Q' v'
162+
with Q'
163+
... | [] = normal
164+
... | cast A∈Σ B' ∷ w = evolving w A∈Σ
165+
⟶ᵢₘ⟹qst (β-:=/failed _ _ _ _) = normal
166+
⟶ᵢₘ⟹qst {Σ} {A = Ref A} (β-ref _) = normal

‎MonoRef/Dynamics/Reduction/StdStore/StateReduction.agda‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -206,11 +206,11 @@ module ParamStateReduction/Pre
206206
⟶⟹rtti⊑Σ {Σ₁⊑ₕΣ = Σ₁⊑ₕΣ} (state/discard _ _) = Σ₁⊑ₕΣ
207207

208208
⟶⟹Σ'⊑Σ : ∀ {Σ Σ₁ Σ₂ T A B} {Q Q' : List (SuspendedCast Σ)} {A∈Σ : A ∈ Σ}
209-
{Σ₁⊑ₕΣ : Σ₁ ⊑ₕ Σ} {M : proj₁ (merge' Σ₁⊑ₕΣ (cast A∈Σ B ∷ Q)) ∣ ∅ ⊢ T}
210-
{μ : Store (proj₁ (merge' Σ₁⊑ₕΣ (cast A∈Σ B ∷ Q))) Σ₁}
211-
{Σ₂⊑ₕΣ₁ : Σ₂ ⊑ₕ Σ₁}
212-
{M' : (proj₁ (merge' (⊑ₕ-trans Σ₂⊑ₕΣ₁ Σ₁⊑ₕΣ) Q')) ∣ ∅ ⊢ T}
213-
{μ' : Store (proj₁ (merge' (⊑ₕ-trans Σ₂⊑ₕΣ₁ Σ₁⊑ₕΣ) Q')) Σ₂}
209+
{Σ₁⊑ₕΣ : Σ₁ ⊑ₕ Σ} {M : proj₁ (merge' Σ₁⊑ₕΣ (cast A∈Σ B ∷ Q)) ∣ ∅ ⊢ T}
210+
{μ : Store (proj₁ (merge' Σ₁⊑ₕΣ (cast A∈Σ B ∷ Q))) Σ₁}
211+
{Σ₂⊑ₕΣ₁ : Σ₂ ⊑ₕ Σ₁}
212+
{M' : (proj₁ (merge' (⊑ₕ-trans Σ₂⊑ₕΣ₁ Σ₁⊑ₕΣ) Q')) ∣ ∅ ⊢ T}
213+
{μ' : Store (proj₁ (merge' (⊑ₕ-trans Σ₂⊑ₕΣ₁ Σ₁⊑ₕΣ) Q')) Σ₂}
214214
→ _,_,_⟶_,_,_ {A∈Σ = A∈Σ} {Σ₁⊑ₕΣ = Σ₁⊑ₕΣ} Q M μ Q' M' μ'
215215
→ proj₁ (merge' (⊑ₕ-trans Σ₂⊑ₕΣ₁ Σ₁⊑ₕΣ) Q') ⊑ₕ Σ
216216
⟶⟹Σ'⊑Σ {Q' = Q'} {Σ₁⊑ₕΣ = Σ₁⊑ₕΣ} {Σ₂⊑ₕΣ₁ = Σ₂⊑ₕΣ₁} red =

‎MonoRef/Dynamics/Simple/StdStore/ProgressDef.agda‎

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
module MonoRef.Dynamics.Simple.StdStore.ProgressDef where
22

33
open import Data.List using (List)
4+
open import Data.Product using (proj₁)
45

56
open import MonoRef.Dynamics.Simple.Error
67
open import MonoRef.Dynamics.Simple.StdStore.SuspendedCast
@@ -11,11 +12,16 @@ open import MonoRef.Dynamics.Simple.TargetWithoutBlame
1112
open import MonoRef.Static.Context
1213

1314

14-
data Progress {Σ Σ₂ Σ₃ A} (Q : List (SuspendedCast Σ)) (M : Σ₃ ∣ ∅ ⊢ A) (μ : Store Σ₃ Σ₂) : Set where
15+
data Progress {Σ Σ₁ A} {Σ₁⊑ₕΣ : Σ₁ ⊑ₕ Σ}
16+
(Q : List (SuspendedCast Σ))
17+
(M : proj₁ (merge' Σ₁⊑ₕΣ Q) ∣ ∅ ⊢ A)
18+
(μ : Store (proj₁ (merge' Σ₁⊑ₕΣ Q)) Σ₁) : Set where
1519

16-
step : ∀ {Σ₄ Σ₅} {μ' : Store Σ₅ Σ₄} {N : Σ₅ ∣ ∅ ⊢ A} {Q' : List (SuspendedCast Σ)}
20+
step : ∀ {Σ₂ Σ₃} {Σ₃⊑ₕΣ₂ : Σ₃ ⊑ₕ Σ₂} {Q' : List (SuspendedCast Σ₂)}
21+
{μ' : Store (proj₁ (merge' Σ₃⊑ₕΣ₂ Q')) Σ₃}
22+
{N : proj₁ (merge' Σ₃⊑ₕΣ₂ Q') ∣ ∅ ⊢ A}
1723
→ Q , M , μ ⟶ Q' , N , μ'
18-
-----------------------
24+
-------------------------
1925
→ Progress Q M μ
2026

2127
done :

‎MonoRef/Dynamics/Simple/StdStore/TypeSafety.agda‎

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
{-
2+
3+
MonoRef.Dynamics.Simple.StdStore.TypeSafety assembles a proof of progress and
4+
provides the full type safety proof.
5+
6+
-}
7+
8+
module MonoRef.Dynamics.Simple.StdStore.TypeSafety where
9+
10+
open import Data.List using (List ; _∷_ ; [])
11+
open import Data.Nat using (ℕ ; suc)
12+
open import Data.Product using (proj₁)
13+
open import Relation.Nullary using (yes ; no)
14+
15+
open import MonoRef.Dynamics.Simple.Error
16+
open import MonoRef.Dynamics.Simple.StdStore.SuspendedCast
17+
open import MonoRef.Dynamics.Simple.StdStore.NormalStoreProgress
18+
open import MonoRef.Dynamics.Simple.StdStore.ProgressDef
19+
open import MonoRef.Dynamics.Simple.StdStore.ProgProgressDef
20+
open import MonoRef.Dynamics.Simple.StdStore.Reduction
21+
open import MonoRef.Dynamics.Simple.StdStore.ReflTransClosure
22+
open import MonoRef.Dynamics.Simple.StdStore.SuspendedCastProgress hiding (Progress)
23+
open import MonoRef.Dynamics.Simple.Value
24+
open import MonoRef.Dynamics.Simple.StdStore.Store
25+
open import MonoRef.Dynamics.Simple.TargetWithoutBlame
26+
open import MonoRef.Static.Context
27+
28+
29+
progress : ∀ {Σ Σ₁ A} {Σ₁⊑ₕΣ : Σ₁ ⊑ₕ Σ}
30+
→ (Q : List (SuspendedCast Σ))
31+
→ QueueStoreTyping Σ₁⊑ₕΣ Q
32+
→ (M : proj₁ (merge' Σ₁⊑ₕΣ Q) ∣ ∅ ⊢ A)
33+
→ (μ : Store (proj₁ (merge' Σ₁⊑ₕΣ Q)) Σ₁)
34+
→ Progress Q M μ
35+
progress .[] normal e μ
36+
with progress-normal-store e μ
37+
... | step R = step (prog-reduce R)
38+
... | done v = done v
39+
... | error x = error x
40+
progress {Σ₁⊑ₕΣ = Σ₁⊑ₕΣ} (cast A∈Σ B ∷ Q) (evolving Q A∈Σ) e μ
41+
with suspended-cast-progress Σ₁⊑ₕΣ A∈Σ B Q μ
42+
... | step R = step (state-reduce R)
43+
44+
data Gas : Set where
45+
gas : ℕ → Gas
46+
47+
data Finished {Σ A} (N : Σ ∣ ∅ ⊢ A) : Set where
48+
49+
done :
50+
Value N
51+
----------
52+
→ Finished N
53+
54+
error :
55+
Error N
56+
----------
57+
→ Finished N
58+
59+
diverge :
60+
----------
61+
Finished N
62+
63+
data TypeSafety {Σ Σ₁ A} {Σ₁⊑ₕΣ : Σ₁ ⊑ₕ Σ}
64+
(Q : List (SuspendedCast Σ))
65+
(L : proj₁ (merge' Σ₁⊑ₕΣ Q) ∣ ∅ ⊢ A)
66+
(μ : Store (proj₁ (merge' Σ₁⊑ₕΣ Q)) Σ₁) : Set where
67+
68+
intro : ∀ {Σ₂ Σ₃} {Σ₃⊑ₕΣ₂ : Σ₃ ⊑ₕ Σ₂} {Q' : List (SuspendedCast Σ₂)}
69+
{μ' : Store (proj₁ (merge' Σ₃⊑ₕΣ₂ Q')) Σ₃}
70+
{N : proj₁ (merge' Σ₃⊑ₕΣ₂ Q') ∣ ∅ ⊢ A}
71+
→ Q , L , μ ↠ Q' , N , μ'
72+
→ Finished N
73+
----------------
74+
→ TypeSafety Q L μ
75+
76+
type-safety : ∀ {Σ Σ₁ A} {Σ₁⊑ₕΣ : Σ₁ ⊑ₕ Σ}
77+
→ Gas
78+
→ (Q : List (SuspendedCast Σ))
79+
→ QueueStoreTyping Σ₁⊑ₕΣ Q
80+
→ (L : proj₁ (merge' Σ₁⊑ₕΣ Q) ∣ ∅ ⊢ A)
81+
→ (μ : Store (proj₁ (merge' Σ₁⊑ₕΣ Q)) Σ₁)
82+
→ TypeSafety Q L μ
83+
type-safety (gas 0) Q qst L μ = intro ↠-refl diverge
84+
type-safety (gas (suc x)) Q qst L μ
85+
with progress Q qst L μ
86+
... | done v = intro ↠-refl (done v)
87+
... | error err = intro ↠-refl (error err)
88+
... | step {Q' = Q'} {μ' = μ'} {N = N} red
89+
with type-safety (gas x) Q' {!!} N μ'
90+
... | intro steps fin = intro (↠-trans red steps) fin

0 commit comments

Comments
 (0)