Browse Source

Start constructing world.

gas-move-test
Thomas Kerber 6 months ago
parent
commit
85e9f09f32
Signed by: Thomas Kerber <t.kerber@ed.ac.uk> GPG Key ID: 8489B911F9ED617B
4 changed files with 53 additions and 0 deletions
  1. 1
    0
      Yggdrasil.agda
  2. 9
    0
      Yggdrasil/List.agda
  3. 41
    0
      Yggdrasil/World.agda
  4. 2
    0
      yggdrasil.agda-lib

+ 1
- 0
Yggdrasil.agda View File

@@ -0,0 +1 @@
1
+module Yggdrasil where

+ 9
- 0
Yggdrasil/List.agda View File

@@ -0,0 +1,9 @@
1
+module Yggdrasil.List where
2
+
3
+open import Data.List using (List; _∷_)
4
+open import Level using (Level)
5
+
6
+data _∈_ {ℓ : Level} {A : Set ℓ} : A → List A → Set ℓ where
7
+  --here : {x : A} {xs : List A} → (x ∷ xs) ∈ x 
8
+  --there : {x y : A} {xs : List A} → xs ∈ y → (x ∷ xs) ∈ y
9
+

+ 41
- 0
Yggdrasil/World.agda View File

@@ -0,0 +1,41 @@
1
+module Yggdrasil.World where
2
+
3
+open import Data.List using (List; _∷_; []; map)
4
+open import Data.Product using (_×_)
5
+open import Level using (Level; suc)
6
+open import Yggdrasil.List using (_∈_)
7
+
8
+record WorldType (ℓ : Level) : Set (suc ℓ)
9
+data Action {ℓ : Level} : (WorldType ℓ) → Set ℓ → Set (suc ℓ)
10
+
11
+record Call (ℓ : Level) (Σ : Set ℓ) (Γ : List (WorldType ℓ)) : Set (suc ℓ) where
12
+  field
13
+    A : Set ℓ
14
+    B : A → Set ℓ
15
+    δ : Σ → (x : A) → Σ × B x
16
+
17
+record WorldType ℓ where
18
+  inductive
19
+  field
20
+    root : Set ℓ
21
+    children : List (WorldType ℓ)
22
+    adv  : List (Call ℓ root children)
23
+    hon  : List (Call ℓ root children)
24
+
25
+open WorldType
26
+
27
+data Action {ℓ} where
28
+  abort : ∀ {W A} → Action W A
29
+  pure  : ∀ {W A} → A → Action W A
30
+  call  : ∀ {W f} → f ∈ (hon W) → (x : Call.A f) → Action W (Call.B f x)
31
+
32
+data WorldState {ℓ : Level} : WorldType ℓ → Set (suc ℓ)
33
+data WorldStates {ℓ : Level} : List (WorldType ℓ) → Set (suc ℓ)
34
+
35
+data WorldStates {ℓ} where
36
+  [] : WorldStates []
37
+  _∷_ : {W : WorldType ℓ} {Ws : List (WorldType ℓ)} → WorldState W →
38
+    WorldStates Ws → WorldStates (W ∷ Ws)
39
+
40
+data WorldState {ℓ} where
41
+  node : {T : WorldType ℓ} → root T → WorldStates (children T) → WorldState T

+ 2
- 0
yggdrasil.agda-lib View File

@@ -0,0 +1,2 @@
1
+depend: standard-library
2
+include: .

Loading…
Cancel
Save