I am trying to code functional semantics for IMP with parallel proactive planning, as presented in section 4 of the next paper .
I am using Agda 2.5.2 and the standard 0.13 library. In addition, all code is available on the following gist .
First of all, I defined the syntax of the language in question as inductive types.
data Exp (n : ℕ) : Set where $_ : ℕ → Exp n Var : Fin n → Exp n _⊕_ : Exp n → Exp n → Exp n data Stmt (n : ℕ) : Set where skip : Stmt n _≔_ : Fin n → Exp n → Stmt n _▷_ : Stmt n → Stmt n → Stmt n iif_then_else_ : Exp n → Stmt n → Stmt n → Stmt n while_do_ : Exp n → Stmt n → Stmt n _∥_ : Stmt n → Stmt n → Stmt n atomic : Stmt n → Stmt n await_do_ : Exp n → Stmt n → Stmt n
A state is just a vector of natural numbers, and the semantics of the expression are simple.
σ_ : ℕ → Set σ n = Vec ℕ n ⟦_,_⟧ : ∀ {n} → Exp n → σ n → ℕ ⟦ $ n , s ⟧ = n ⟦ Var v , s ⟧ = lookup vs ⟦ e ⊕ e' , s ⟧ = ⟦ e , s ⟧ + ⟦ e' , s ⟧
Then I determined the type of repetition, which is a kind of delayed computation.
data Res (n : ℕ) : Set where ret : (st : σ n) → Res n δ : (r : ∞ (Res n)) → Res n _∨_ : (lr : ∞ (Res n)) → Res n yield : (s : Stmt n)(st : σ n) → Res n
Next, following 1 , I define sequential and parallel execution of statements
evalSeq : ∀ {n} → Stmt n → Res n → Res n evalSeq s (ret st) = yield s st evalSeq s (δ r) = δ (♯ (evalSeq s (♭ r))) evalSeq s (l ∨ r) = ♯ evalSeq s (♭ l) ∨ ♯ evalSeq s (♭ r) evalSeq s (yield s' st) = yield (s ▷ s') st evalParL : ∀ {n} → Stmt n → Res n → Res n evalParL s (ret st) = yield s st evalParL s (δ r) = δ (♯ evalParL s (♭ r)) evalParL s (l ∨ r) = ♯ evalParL s (♭ l) ∨ ♯ evalParL s (♭ r) evalParL s (yield s' st) = yield (s ∥ s') st evalParR : ∀ {n} → Stmt n → Res n → Res n evalParR s (ret st) = yield s st evalParR s (δ r) = δ (♯ evalParR s (♭ r)) evalParR s (l ∨ r) = ♯ evalParR s (♭ l) ∨ ♯ evalParR s (♭ r) evalParR s (yield s' st) = yield (s' ∥ s) st
So far so good. Then I need to define an expression evaluation function mutually with the operation in order to close (perform suspended calculations) when resuming.
mutual close : ∀ {n} → Res n → Res n close (ret st) = ret st close (δ r) = δ (♯ close (♭ r)) close (l ∨ r) = ♯ close (♭ l) ∨ ♯ close (♭ r) close (yield s st) = δ (♯ eval s st) eval : ∀ {n} → Stmt n → σ n → Res n eval skip st = ret st eval (x ≔ e) st = δ (♯ (ret (st [ x ]≔ ⟦ e , st ⟧ ))) eval (s ▷ s') st = evalSeq s (eval s' st) eval (iif e then s else s') st with ⟦ e , st ⟧ ...| zero = δ (♯ yield s' st) ...| suc n = δ (♯ yield s st) eval (while e do s) st with ⟦ e , st ⟧ ...| zero = δ (♯ ret st) ...| suc n = δ (♯ yield (s ▷ while e do s) st ) eval (s ∥ s') st = (♯ evalParR s' (eval s st)) ∨ (♯ evalParL s (eval s' st)) eval (atomic s) st = {!!} -- δ (♯ close (eval s st)) eval (await e do s) st = {!!}
Integrity Check Agda complains when I try to fill a hole in the eval expression for the atomic constructor using δ (♯ close (eval s st)) , stating that the completion check fails for multiple points in both the eval and close functions.
My questions on this issue:
1) Why does the Agda end check complain about these definitions? It seems to me that the call to δ (♯ close (eval s st)) beautiful, since this is done in a less constructive way.
2) The current Agda language documentation says that this kind of musical notation based on monetization is an “old” monument in Agda. He recommends using co-inductive recordings and copies. I looked around, but I could not find examples of copies outside streams and monad delays. My question is: is it possible to imagine repetitions using co-inductive notes and copywriters?