open import GeneralLemmas using (Dec; _≡_)
module DKrivine
(Node : Set)
(_≟_ : (n n' : Node) → Dec (n ≡ n'))
where
open import GeneralLemmas
open import Heap
open import Lambda Node
open import Relation
open import Tagged
RPtr = Ptr × Node
Closure Env : Set
data StackElem : Set where
arg : Closure → StackElem
if0 : Closure → Closure → StackElem
op₂ : (ℕ → ℕ → ℕ) → Closure → StackElem
op₁ : (ℕ → ℕ) → StackElem
Closure = Term × Env
ContPtr = RPtr
data EnvElem : Set where
local : Closure → EnvElem
remote : ContPtr → ℕ → EnvElem
local-inj : ∀ {c₁ c₂} → local c₁ ≡ local c₂ → c₁ ≡ c₂
local-inj refl = refl
remote-inj : ∀ {ptr₁ n₁ ptr₂ n₂} → remote ptr₁ n₁ ≡ remote ptr₂ n₂ → ptr₁ ≡ ptr₂ × n₁ ≡ n₂
remote-inj refl = refl , refl
Env = List EnvElem
Stack = List StackElem × Maybe (ContPtr × ℕ × ℕ)
ContHeap = Heap Stack
Thread = Term × Env × Stack
Machine = Maybe Thread × ContHeap
data Msg : Set where
REMOTE : Term → Node → ContPtr → ℕ → Msg
VAR : ContPtr → ℕ → ContPtr → ℕ → Msg
RETURN : ContPtr → ℕ → ℕ → Msg
_⊢_▸_ : {A : Set} → Node → Heap A → A → Heap A × RPtr
i ⊢ h ▸ x = (let (h' , ptr) = h ▸ x in h' , (ptr , i))
num-args : Stack → ℕ
num-args ([] , nothing) = 0
num-args ([] , just (contptr , numargs , argstaken)) = numargs
num-args (arg x ∷ s , r) = 1 + num-args (s , r)
num-args (if0 x x₁ ∷ s , r) = 0
num-args (op₂ x x₁ ∷ s , r) = 0
num-args (op₁ x ∷ s , r) = 0
stack-index : Stack → ℕ → Maybe EnvElem
stack-index (if0 x x₁ ∷ s , r) n = nothing
stack-index (op₂ x x₁ ∷ s , r) n = nothing
stack-index (op₁ x ∷ s , r) n = nothing
stack-index (arg c ∷ s , r) zero = just (local c)
stack-index (arg c ∷ s , r) (suc i) = stack-index (s , r) i
stack-index ([] , nothing) i = nothing
stack-index ([] , just (contptr , zero , argstaken)) i = nothing
stack-index ([] , just (contptr , suc numargs , argstaken)) zero = just (remote contptr argstaken)
stack-index ([] , just (contptr , suc numargs , argstaken)) (suc i) = stack-index ([] , just (contptr , numargs , suc argstaken)) i
drop-stack : Stack → ℕ → Maybe Stack
drop-stack (s , r) zero = just (s , r)
drop-stack ([] , just (contptr , zero , drop)) (suc i) = nothing
drop-stack ([] , just (contptr , suc numargs , drop)) (suc i) = drop-stack ([] , just (contptr , numargs , suc drop)) i
drop-stack ([] , nothing) (suc i) = nothing
drop-stack (arg x ∷ s , r) (suc i) = drop-stack (s , r) i
drop-stack (x ∷ s , r) (suc i) = nothing
data _⊢_⟶DKrivine<_>_ (i : Node) : Machine → Tagged Msg → Machine → Set where
POPARG : ∀ {t e c s r conth} →
i ⊢ (just (ƛ t , e , arg c ∷ s , r) , conth) ⟶DKrivine< silent > (just (t , local c ∷ e , s , r) , conth)
PUSHARG : ∀ {t t' e s r conth} →
i ⊢ (just ((t $ t') , e , s , r) , conth) ⟶DKrivine< silent > (just (t , e , arg (t' , e) ∷ s , r) , conth)
VAR : ∀ {n e s r conth t e'} → lookup n e ≡ just (local (t , e')) →
i ⊢ (just (var n , e , s , r) , conth) ⟶DKrivine< silent > (just (t , e' , s , r) , conth)
COND : ∀ {b t f e s r conth} →
i ⊢ (just (if0 b then t else f , e , s , r), conth) ⟶DKrivine< silent > (just (b , e , if0 (t , e) (f , e) ∷ s , r) , conth)
COND-0 : ∀ {e t e' f s r conth} →
i ⊢ (just (lit 0 , e , if0 (t , e') f ∷ s , r) , conth) ⟶DKrivine< silent > (just (t , e' , s , r) , conth)
COND-suc : ∀ {n e t e' f s r conth} →
i ⊢ (just (lit (suc n) , e , if0 t (f , e') ∷ s , r) , conth) ⟶DKrivine< silent > (just (f , e' , s , r) , conth)
OP : ∀ {f t t' e s r conth} →
i ⊢ (just (op f t t' , e , s , r) , conth) ⟶DKrivine< silent > (just (t , e , op₂ f (t' , e) ∷ s , r) , conth)
OP₂ : ∀ {n e f t e' s r conth} →
i ⊢ (just (lit n , e , op₂ f (t , e') ∷ s , r) , conth) ⟶DKrivine< silent > (just (t , e' , op₁ (f n) ∷ s , r) , conth)
OP₁ : ∀ {n e f s r conth} →
i ⊢ (just (lit n , e , op₁ f ∷ s , r) , conth) ⟶DKrivine< silent > (just (lit (f n) , [] , s , r) , conth)
POPARG-remote : ∀ {t e contptr args drop conth} →
i ⊢ (just (ƛ t , e , [] , just (contptr , suc args , drop)) , conth) ⟶DKrivine< silent >
(just (t , remote contptr drop ∷ e , [] , just (contptr , args , suc drop)) , conth)
REMOTE-send : ∀ {t i' e s conth} → let (conth' , contptr) = i ⊢ conth ▸ s in
i ⊢ (just (t at i' , e , s) , conth) ⟶DKrivine< send (REMOTE t i' contptr (num-args s)) >
(nothing , conth')
REMOTE-receive : ∀ {conth t contptr numargs} →
i ⊢ (nothing , conth) ⟶DKrivine< receive (REMOTE t i contptr numargs) > (just (t , [] , [] , just (contptr , numargs , 0)) , conth)
VAR-send : ∀ {n e s rcontptr index conth} → lookup n e ≡ just (remote rcontptr index) → let (conth' , contptr) = i ⊢ conth ▸ s in
i ⊢ (just (var n , e , s) , conth) ⟶DKrivine< send (VAR rcontptr index contptr (num-args s)) > (nothing , conth')
VAR-receive : ∀ {conth contptr s n rcontptr numargs el} → conth ! contptr ≡ just s → stack-index s n ≡ just el →
i ⊢ (nothing , conth) ⟶DKrivine< receive (VAR (contptr , i) n rcontptr numargs) >
(just (var 0 , el ∷ [] , [] , just (rcontptr , numargs , 0)) , conth)
RETURN-send : ∀ {n e contptr drop conth} →
i ⊢ (just (lit n , e , [] , just (contptr , 0 , drop)) , conth) ⟶DKrivine< send (RETURN contptr n drop) > (nothing , conth)
RETURN-receive : ∀ {conth contptr s s' n drop} → conth ! contptr ≡ just s → drop-stack s drop ≡ just s' →
i ⊢ (nothing , conth) ⟶DKrivine< receive (RETURN (contptr , i) n drop) > (just (lit n , [] , s') , conth)
open import Network Node _≟_ _⊢_⟶DKrivine<_>_ public
initial-network-sync : Term → Node → SyncNetwork
initial-network-sync t i = update (λ i' → (nothing , ∅)) i (just (t , [] , [] , nothing), ∅)
initial-network-async : Term → Node → AsyncNetwork
initial-network-async c i = initial-network-sync c i , []