typecheck

TDTTの型検査器．

build

Stackというツールを用いる． 各OS毎にビルド済みのバイナリも配付されている． Stackは，$HOME/.stackのみをいじるので，不要になった場合はこのディレクトリを削除する．

次でビルドされる．

stack setup
stack build

次で，型検査器tcが$HOME/.local/binにインストールされる．

stack install

usage

./testにいくつか型検査のテストを設置した． 次のように型検査できる．

$HOME/.local/bin/tc ./test/test1.tc

型検査が真の場合はTrue， 偽の場合にはFalseと反例の入力木を示す．

uninstall

次で全てを削除する．

rm -rf $HOME/.stack
rm -rf $HOME/.local/bin/tc

profiling

次のようにビルドするとプロファイリング機能が付加される． ただし型検査は遅くなる．

stack clean
stack build --executable-profiling --library-profiling --ghc-options="-fprof-auto -rtsopts"
stack install

./tc.profにプロファイリング結果が残る．

$HOME/.local/bin/tc +RTS -P -RTS test/test1.tc

source

次のような構成である．

• src ライブラリが詰っている．
  • src/Atom 状態や木など基本的な型とその関数．
  • src/Parser 型検査のための外部DSLのパーサの実装．
  • src/Set 集合を意味するStateSetの定義とその関数．
  • src/Ta 木オートマトンに関する定義
    • src/Ta/Ata Alternating Tree Automatonに関する型と関数．
    • src/Ta/Nd Tree Automatonに関する型と関数．
  • src/Tt 木トランスデューサに関する定義
• app メイン関数が詰っている．
• test 型検査器tcに与えられるサンプルプログラム．