Browse Source

Finish execution model.

gas-move-test
Thomas Kerber 10 months ago
parent
commit
393ac3ba1c
Signed by: Thomas Kerber <t.kerber@ed.ac.uk> GPG Key ID: 8489B911F9ED617B
1 changed files with 7 additions and 9 deletions
  1. 7
    9
      Yggdrasil/World.agda

+ 7
- 9
Yggdrasil/World.agda View File

@@ -1,12 +1,13 @@
module Yggdrasil.World where

open import Data.Bool using (Bool)
open import Data.Empty using (⊥-elim)
open import Data.List using (List; _∷_; []; map)
open import Data.Maybe using (Maybe; nothing; just)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
open import Level using (Level) renaming (suc to lsuc)
open import Yggdrasil.List using (_∈_; here; there)

@@ -55,11 +56,12 @@ data _⊑_ {ℓ : Level} : (Γ₁ Γ₂ : WorldType ℓ) → Set (lsuc ℓ) wher
here : ∀ {Γ} → Γ ⊑ Γ
there : ∀ {Γ₁ Γ₂ Γ₃} → Γ₂ ∈ chld (node Γ₃) → Γ₁ ⊑ Γ₂ → Γ₁ ⊑ Γ₃

⊑-trans : ∀ {ℓ} {Γ₁ Γ₂ Γ₃ : WorldType ℓ} → Γ₁ ⊑ Γ₂ → Γ₂ ⊑ Γ₃ → Γ₁ ⊑ Γ₃
⊑-trans ⊑Γ here = ⊑Γ
⊑-trans ⊑Γ (there Γ′∈ ⊑Γ′) = there Γ′∈ (⊑-trans ⊑Γ ⊑Γ′)

⊑-right : ∀ {ℓ} {Γ₁ Γ₂ Γ₃ : WorldType ℓ} → Γ₂ ⊑ Γ₃ → Γ₁ ∈ chld (node Γ₂) → Γ₁ ⊑ Γ₃
⊑-right here ∈Γ = there ∈Γ here
⊑-right (there Γ′∈ ⊑Γ′) ∈Γ = ?
⊑-right Γ⊑ ∈Γ = ⊑-trans (there ∈Γ here) Γ⊑

data Action↯ {ℓ} Γ where
call↯ : ∀ {Γ′} {f : Call ℓ (node Γ′)} → f ∈ (adv Γ′) → Γ′ ⊑ Γ → (x : Call.A f) →
@@ -121,13 +123,6 @@ exec↓ : ∀ {ℓ Γ₁ Γ₂ A} → Oracle Γ₁ → Action↓ Γ₂ A → Wor
exec↑ : ∀ {ℓ Γ₁ Γ₂ N A} → Oracle Γ₁ → Action↑ N A → WorldState {ℓ} Γ₁ →
Γ₂ ⊑ Γ₁ → N ≡ node Γ₂ → ℕ → Maybe (A × WorldState {ℓ} Γ₁)



exec (strat (inj₁ α) O) Σ g = exec↯ O α Σ g
exec (strat (inj₂ α) O) Σ g = exec↓ O α Σ here g

@@ -145,9 +140,6 @@ exec↓ O (call↓ {f = f} f∈ x) Σ ⊑Γ (suc g) = let
Σ′ = set ⊑Γ Σ σ′
in exec↑ O α Σ′ ⊑Γ refl g

--Oracle Γ = ∀ {q} → q ∈↑ Γ → (x : Query.A q) → Action Γ (Query.B q x)
--path : ∀ {Γ′} → Γ′ ⊑ Γ → q ∈ qry (node Γ′) → q ∈↑ Γ

-- NOTE: Gas is only used for termination here, it is NOT a computational model.
exec↑ _ _ _ _ _ zero = nothing
exec↑ O abort Σ ⊑Γ N≡ (suc g) = nothing

Loading…
Cancel
Save