-
Notifications
You must be signed in to change notification settings - Fork 0
/
TypeSafety.agda
68 lines (53 loc) · 1.95 KB
/
TypeSafety.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
{-
MonoRef.Dynamics.Simple.EvStore.TypeSafety assembles a proof of progress and provides
the full type safety proof.
-}
module MonoRef.Dynamics.Simple.EvStore.TypeSafety where
open import Data.Nat using (ℕ ; suc)
open import Relation.Nullary using (yes ; no)
open import MonoRef.Dynamics.Simple.Error
open import MonoRef.Dynamics.Simple.EvStore.EvolvingStoreProgress
open import MonoRef.Dynamics.Simple.EvStore.NormalStoreProgress
open import MonoRef.Dynamics.Simple.EvStore.ProgressDef
open import MonoRef.Dynamics.Simple.EvStore.ReflTransClosure
open import MonoRef.Dynamics.Simple.EvStore.SReduction
open import MonoRef.Dynamics.Simple.Value
open import MonoRef.Dynamics.Simple.EvStore.Store
open import MonoRef.Dynamics.Simple.TargetWithoutBlame
open import MonoRef.Static.Context
progress : ∀ {Σ A} → (M : Σ ∣ ∅ ⊢ A) → (ν : Store Σ) → Progress M ν
progress e ν
with normalStoreP ν
... | yes ν-NS = progress-normal-store e ν ν-NS
... | no ν-¬NS
with progress-evolving-store ν ν-¬NS
... | step ¬μ red = step (state-reduce ¬μ red)
data Gas : Set where
gas : ℕ → Gas
data Finished {Σ A} (N : Σ ∣ ∅ ⊢ A) : Set where
done :
Value N
----------
→ Finished N
error :
Error N
----------
→ Finished N
diverge :
----------
Finished N
data TypeSafety {Σ A} (L : Σ ∣ ∅ ⊢ A) (ν : Store Σ) : Set where
intro : ∀ {Σ'} {N : Σ' ∣ ∅ ⊢ A} {ν' : Store Σ'}
→ L , ν ↠ N , ν'
→ Finished N
--------------
→ TypeSafety L ν
type-safety : ∀ {Σ A} → Gas → (L : Σ ∣ ∅ ⊢ A) → (ν : Store Σ) → TypeSafety L ν
type-safety (gas 0) e ν = intro ↠-refl diverge
type-safety (gas (suc x)) e ν
with progress e ν
... | done v = intro ↠-refl (done v)
... | error err = intro ↠-refl (error err)
... | step {ν' = ν'} {N = N} red
with type-safety (gas x) N ν'
... | intro steps fin = intro (↠-trans red steps) fin