Gears Agda
context を使った meta compuationでの並列実行
条件の記述は良いが、soundness がまだだめ
なおしかた不明 -> 証明したい仕様を継続の入力で受ければ良いことがわかった。
Gears Agda で記述した codeGear/dataGearを CbC に変換する
Agdaの reflection の機能を使う。Agda の termを構文解析できる。それを
Agda の print monad を使って CbC 生成する
ということは、Monad 二つ使うことになる。なんらかの Monad combinator が必要。
allocator を meta 計算で実装する必要がある(GCも
Gears Agda のメモリ
GearsAgdaではNatのアドレスをkeyとする
Context に入れるが実行時に同じものを常にコピー
Contents addressableにすることが可能
codeTable N → code
dataIndex data → N
globalData N → data
一段のcallよりも、全部、par goto にして、複数のcontext で
call を実現する
戻る時には、futureの同期みたいなのがいる
待ち状態のcontext
futureの参照はmemoryに対して起きる
そこで待てば良いが…
memoryの参照はnormal levelで起きないなら
stubで起きるはず
future使わずにCPS変換しても良い