LambdaIFCStar/src/Simulator/Simulator.agda at master · Gradual-Typing/LambdaIFCStar · GitHub

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
module Simulator.Simulator where

open import Data.Unit
open import Data.Nat
open import Data.List
open import Data.Bool renaming (Bool to 𝔹; _≟_ to _≟ᵇ_)
open import Data.Maybe
open import Data.Product using (_×_; ∃-syntax; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Function using (case_of_)

open import Common.Utils
open import Common.Types
open import Common.BlameLabels
open import Surface.SurfaceLang
open import Surface.Precision
open import CC.CCStatics renaming (Term to CCTerm;
  `_ to var; $_of_ to const_of_; ƛ⟦_⟧_˙_of_ to lam⟦_⟧_˙_of_; !_ to *_)
open import CC.Compile renaming (compile to 𝒞; compilation-preserves-type to 𝒞-pres)
open import CC.Reduction
open import CC.TypeSafety
open import CC.BigStep
open import CC.MultiStep renaming (multi-trans to _↠_)
open import Memory.Heap CCTerm Value

open import Simulator.AST
open import Simulator.CheckPrecision


sim-helper : ∀ {Σ gc A} M μ
  → [] ; Σ ; gc ; low ⊢ M ⦂ A
  → Σ ⊢ μ → (t : AST) → (k : ℕ)
    ------------------------------------------
  → Maybe (ℕ × ∃[ N ] ∃[ μ′ ] (M ∣ μ ∣ low —↠ N ∣ μ′))
sim-helper {A = A} M μ ⊢M ⊢μ t 0 =
  if (check-⊑? (to-ast M ⊢M A) t) then just ⟨ 0 , M , μ , M ∣ μ ∣ _ ∎ ⟩ else nothing
sim-helper {A = A} M μ ⊢M ⊢μ t (suc k-1) =
  if (check-⊑? (to-ast M ⊢M A) t) then just ⟨ 0 , M , μ , M ∣ μ ∣ _ ∎ ⟩
    else
    (case progress low M ⊢M μ ⊢μ of λ where
      (step {N} {μ′} M→N) →
        let ⟨ Σ′ , Σ′⊇Σ , ⊢N , ⊢μ′ ⟩ = preserve ⊢M ⊢μ (low≾ _) M→N in
        do
          ⟨ n , N′ , μ″ , N↠N′ ⟩ ← sim-helper N μ′ ⊢N ⊢μ′ t k-1
          just ⟨ 1 + n , N′ , μ″ , M ∣ _ ∣ _ —→⟨ M→N ⟩ N↠N′ ⟩
      (done v)      {- M is value already -} → nothing
      (err E-error) {- M is an error -}      → nothing)

{-
          M′
          ⊔|
  M —↠ₙ N
-}
step-left : ∀ {Σ Σ′ gc gc′ A A′} M M′ μ₁
  → (⊢M  : [] ; Σ  ; gc  ; low ⊢ M  ⦂ A)
  → (⊢M′ : [] ; Σ′ ; gc′ ; low ⊢ M′ ⦂ A′)
  → (⊢μ₁ : Σ ⊢ μ₁)
    ---------------------------------------------------
  → Maybe (ℕ × ∃[ N ] ∃[ μ₂ ] (M ∣ μ₁ ∣ low —↠ N ∣ μ₂))
step-left {A = A} {A′} M M′ μ₁ ⊢M ⊢M′ ⊢μ₁ =
  sim-helper M μ₁ ⊢M ⊢μ₁ (to-ast M′ ⊢M′ A′) magic-num

step-right : ∀ {Σ Σ′ gc gc′ A A′} M M′ μ₁ μ₁′
  → (⊢M  : [] ; Σ  ; gc  ; low ⊢ M  ⦂ A)
  → (⊢M′ : [] ; Σ′ ; gc′ ; low ⊢ M′ ⦂ A′)
  → (⊢μ₁  : Σ  ⊢ μ₁)
  → (⊢μ₁′ : Σ′ ⊢ μ₁′)
  → (k : ℕ)  -- gas: steps left for the right side
  → (n : ℕ)  -- steps taken on the left side
  → (n′ : ℕ) -- steps taken on the right side
    ------------------------------------------------------------
  → (ℕ × ∃[ N ]  ∃[ μ₂  ] (M  ∣ μ₁  ∣ low —↠ N  ∣ μ₂ )) ×
     (ℕ × ∃[ N′ ] ∃[ μ₂′ ] (M′ ∣ μ₁′ ∣ low —↠ N′ ∣ μ₂′)) ×
     (List (ℕ × ℕ))
step-right M M′ μ₁ μ₁′ ⊢M ⊢M′ ⊢μ ⊢μ₁′ 0 n n′ =
  -- we run out of gas and can't further proceed on the more precise side,
  -- - or either side
  ⟨ ⟨ 0 , M , μ₁ , _ ∣ _ ∣ _ ∎ ⟩ , ⟨ 0 , M′ , μ₁′ , _ ∣ _ ∣ _ ∎ ⟩ , [] ⟩
step-right M M′ μ₁ μ₁′ ⊢M ⊢M′ ⊢μ₁ ⊢μ₁′ (suc k-1) n₀ n₀′ =
  -- the more precise side (right) takes one step
  case progress low M′ ⊢M′ μ₁′ ⊢μ₁′ of λ where
  (step {N′} {μ₂′} M′→N′) →
    let ⟨ _ , _ , ⊢N′ , ⊢μ₂′ ⟩ = preserve ⊢M′ ⊢μ₁′ (low≾ _) M′→N′ in
    case step-left M N′ μ₁ ⊢M ⊢N′ ⊢μ₁ of λ where
    -- `step-left` recursively steps on the less precise side
    {-
      M′ —→  N′
      ⊔|       ⊔|
      M  —↠ₙ N
    -}
    (just ⟨ n , N , μ₂ , M↠N ⟩) →
      let ⟨ _ , _ , ⊢N , ⊢μ₂ ⟩ = multi-pres ⊢M ⊢μ₁ (low≾ _) M↠N in
      let ⟨ ⟨ n₁ , N₁ , μ₃ , N↠N₁ ⟩ ,
            ⟨ n₁′ , N₁′ , μ₃′ , N′↠N₁′ ⟩ ,
            s ⟩ = step-right N N′ μ₂ μ₂′ ⊢N ⊢N′ ⊢μ₂ ⊢μ₂′ k-1 (n + n₀) (1 + n₀′) in
      ⟨ ⟨ n + n₁ , N₁ , μ₃ , M↠N ↠ N↠N₁ ⟩ ,
        ⟨ 1 + n₁′ , N₁′ , μ₃′ , _ ∣ _ ∣ _ —→⟨ M′→N′ ⟩ N′↠N₁′ ⟩ ,
        ⟨ n + n₀ , 1 + n₀′ ⟩ ∷ s ⟩
    nothing →
      -- if we can't find N to stay in simulation
      -- we don't go anywhere else
      ⟨ ⟨ 0 , M , μ₁ , _ ∣ _ ∣ _ ∎ ⟩ ,
        ⟨ 1 , N′ , μ₂′ , _ ∣ _ ∣ _ —→⟨ M′→N′ ⟩ _ ∣ _ ∣ _ ∎ ⟩ ,
        [] ⟩
  _ → -- if M′ is a value or an error
    ⟨ ⟨ 0 , M , μ₁ , _ ∣ _ ∣ _ ∎ ⟩ ,
      ⟨ 0 , M′ , μ₁′ , _ ∣ _ ∣ _ ∎ ⟩ ,
      [] ⟩

simulator : ∀ {A A′} (M M′ : Term)
  → [] ; l low ⊢ᴳ M  ⦂ A
  → [] ; l low ⊢ᴳ M′ ⦂ A′
    -------------------------------------------------------------------
  → (ℕ × ∃[ N₁  ] ∃[ N₂  ] ∃[ μ  ] (N₁  ∣ ∅ ∣ low —↠ N₂  ∣ μ )) ×
     (ℕ × ∃[ N₁′ ] ∃[ N₂′ ] ∃[ μ′ ] (N₁′ ∣ ∅ ∣ low —↠ N₂′ ∣ μ′)) ×
     (List (ℕ × ℕ))
simulator {A} {A′} M M′ ⊢M ⊢M′ =
  let N₁  = 𝒞 M ⊢M   ; ⊢N₁  = 𝒞-pres M ⊢M   in
  let N₁′ = 𝒞 M′ ⊢M′ ; ⊢N₁′ = 𝒞-pres M′ ⊢M′ in
  if check-⊑? (to-ast N₁ ⊢N₁ A) (to-ast N₁′ ⊢N₁′ A′) then
    (let ⟨ ⟨ n , N₂ , μ , N₁↠N₂ ⟩ ,
           ⟨ n′ , N₂′ , μ′ , N₁′↠N₂′ ⟩ ,
           s ⟩ = step-right N₁ N₁′ ∅ ∅ ⊢N₁ ⊢N₁′ ⊢μ-nil ⊢μ-nil magic-num 0 0 in
     ⟨ ⟨ n , N₁ , N₂ , μ , N₁↠N₂ ⟩ , ⟨ n′ , N₁′ , N₂′ , μ′ , N₁′↠N₂′ ⟩ , ⟨ 0 , 0 ⟩ ∷ s ⟩)
    else ⟨ ⟨ 0 , N₁ , N₁ , ∅ , _ ∣ _ ∣ _ ∎ ⟩ , ⟨ 0 , N₁′ , N₁′ , ∅ , _ ∣ _ ∣ _ ∎ ⟩ , [] ⟩