open import GeneralLemmas using (Dec; _≡_) module DCESH (Node : Set) (_≟_ : (n n' : Node) → Dec (n ≡ n')) where open import GeneralLemmas open import Heap open import Lambda open Term Node open import MachineCode Node as MachineCode open import Relation open import Tagged RPtr = Ptr × Node ClosPtr = RPtr mutual Closure = Code × Env data Value : Set where nat : ℕ → Value clos : ClosPtr → Value Env = List Value ClosHeap = Heap Closure data StackElem : Set where val : Value → StackElem cont : Closure → StackElem ContPtr = RPtr Stack = List StackElem × Maybe ContPtr ContHeap = Heap (Closure × Stack) Thread = Code × Env × Stack Machine = Maybe Thread × ClosHeap × ContHeap data Msg : Set where REMOTE : Code → Node → ContPtr → Msg RETURN : ContPtr → Value → Msg APPLY : ClosPtr → Value → ContPtr → Msg _⊢_▸_ : {A : Set} → Node → Heap A → A → Heap A × RPtr i ⊢ h ▸ x = let (h' , ptr) = h ▸ x in h' , (ptr , i) data _⊢_⟶Machine<_>_ (i : Node) : Machine → Tagged Msg → Machine → Set where VAR : ∀ {n c e s v r clh conth} → lookup n e ≡ just v → i ⊢ (just (VAR n SEQ c , e , s , r) , clh , conth) ⟶Machine< silent > (just (c , e , val v ∷ s , r), clh , conth) CLOSURE : ∀ {c' c e s r clh conth} → let (clh' , rclptr) = i ⊢ clh ▸ (c' , e) in i ⊢ (just (CLOSURE c' SEQ c , e , s , r) , clh , conth) ⟶Machine< silent > (just (c , e , val (clos rclptr) ∷ s , r) , clh' , conth) APPLY : ∀ {c e v c' e' s r clptr clh conth} → clh ! clptr ≡ just (c' , e') → i ⊢ (just (APPLY SEQ c , e , val v ∷ val (clos (clptr , i)) ∷ s , r), clh , conth) ⟶Machine< silent > (just (c' , v ∷ e' , cont (c , e) ∷ s , r), clh , conth) RETURN : ∀ {e v c e' s r clh conth} → i ⊢ (just (RETURN , e , val v ∷ cont (c , e') ∷ s , r), clh , conth) ⟶Machine< silent > (just (c , e' , val v ∷ s , r), clh , conth) LIT : ∀ {n c e s r clh conth} → i ⊢ (just (LIT n SEQ c , e , s , r) , clh , conth) ⟶Machine< silent > (just (c , e , val (nat n) ∷ s , r), clh , conth) PRIMOP : ∀ {f c e n₁ n₂ s r clh conth} → i ⊢ (just (PRIMOP f SEQ c , e , val (nat n₁) ∷ val (nat n₂) ∷ s , r), clh , conth) ⟶Machine< silent > (just (c , e , val (nat (f n₁ n₂)) ∷ s , r), clh , conth) COND-0 : ∀ {c c' e s r clh conth} → i ⊢ (just (COND c c' , e , val (nat 0) ∷ s , r), clh , conth) ⟶Machine< silent > (just (c , e , s , r), clh , conth) COND-suc : ∀ {c c' e n s r clh conth} → i ⊢ (just (COND c c' , e , val (nat (suc n)) ∷ s , r), clh , conth) ⟶Machine< silent > (just (c' , e , s , r), clh , conth) REMOTE-send : ∀ {c' i' c e s r clh conth} → let (conth' , rptr) = i ⊢ conth ▸ ((c , e), s , r) in i ⊢ (just (REMOTE c' i' SEQ c , e , s , r) , clh , conth) ⟶Machine< send (REMOTE c' i' rptr) > (nothing , clh , conth') REMOTE-receive : ∀ {clh conth c rcontptr} → i ⊢ (nothing , clh , conth) ⟶Machine< receive (REMOTE c i rcontptr) > (just (c , [] , [] , just rcontptr), clh , conth) APPLY-send : ∀ {c e v clptr j s r clh conth} → i ≢ j → let (conth' , rcontptr) = i ⊢ conth ▸ ((c , e) , s , r) in i ⊢ (just (APPLY SEQ c , e , val v ∷ val (clos (clptr , j)) ∷ s , r), clh , conth) ⟶Machine< send (APPLY (clptr , j) v rcontptr) > (nothing , clh , conth') APPLY-receive : ∀ {clh conth clptr v rcontptr c e} → clh ! clptr ≡ just (c , e) → i ⊢ (nothing , clh , conth) ⟶Machine< receive (APPLY (clptr , i) v rcontptr) > (just (c , v ∷ e , [] , just rcontptr), clh , conth) RETURN-send : ∀ {e v rcontptr clh conth} → i ⊢ (just (RETURN , e , val v ∷ [] , just rcontptr) , clh , conth) ⟶Machine< send (RETURN rcontptr v) > (nothing , clh , conth) RETURN-receive : ∀ {clh conth contptr v c e s r} → conth ! contptr ≡ just ((c , e), s , r) → i ⊢ (nothing , clh , conth) ⟶Machine< receive (RETURN (contptr , i) v) > (just (c , e , val v ∷ s , r), clh , conth) open import Network Node _≟_ _⊢_⟶Machine<_>_ public initial-network-sync : Code → Node → SyncNetwork initial-network-sync c i = update (λ i' → (nothing , ∅ , ∅)) i (just (c , [] , [] , nothing), ∅ , ∅) initial-network-async : Code → Node → AsyncNetwork initial-network-async c i = initial-network-sync c i , []