コンパイラ読み会2日目 Agda

LLVM clang のコード生成部も読んでたんですが、最終的なアセンブラ生成は

　　IRを指定Archのコードに変換するだけ

だったので、割とつまらなかった。いや、Arch毎の命令記述はかなり謎なんですけどね。それはGCCも同じではあるが。

こういう部分ってCPUが自分で用意しろと思わなくもない。アセンブラの多様性とかいるのか?

Agdaの方は、やっぱり

　　Haskell code の読み方がわからない

って問題が。割と苦労して、Agdaの最新コードを singularity の中に構築するのはできたんですが、

　　Traceの方法がわからん

gdb で trace するっていう手もあるらしいが...

ghci で、Agdaの Main.hsを読み込むってのもやってみましたが、できないことはないっぽいが、

　　構文定義の問題があるらしく、いろいろ見ながら作る必要があるらしい。

結局、ソースコードみながら、ここから TypeCheck みたいなのは見つけたんですが、

　　そこが実行されるかどうかは良く分からない

いや、そこここに、liftIO 使った print 文がコメントアウトされてるので、そういうものなのかも。

if [[ -f /singularity ]]; then
prompt="%S+%s%m%S+%s$SINGULARITY_NAME:r%S+%s%n "
tty= $SINGULARITY_NAME:r
fi

みたいなコードを入れると singularity とそうでないのを区別できてよいらしい。