Merge useWani with master

[DaisukeBekki]

useWani branchをmaster branchとmergeするためのPRです。 今回の大きなupdateとして、以下が挙げられます。

1. DTS.Prover.Wani.Prove.prove' と、DTS.TypeCheckerのtypeInfer/typeCheck関数で呼び出される自動証明器の型を DTS.QueryTypes.Prover型として合わせた（今後、neuralWani等もこの型に合わせる）
2. DTS以下、4つの依存型理論を別モジュールとして用意した：DTTdeBruijn, DTTwithName, UDTTdeBruijn, UDTTwithName
   • deBruijnが付くモジュールではde Bruijn indexを用い、withNameが付くモジュールでは変数名がついている
   • UDTTとは、DTTにAsp, Lamvec, Appvecの3つのコンストラクタが加わったもの
   • deBruin <-> withName間の変換は、fromDeBruijn...関数、toDeBruijn...関数で実現
   • DTT <-> UDTT間の変換は、toUDTT, toDTT関数で実現
   • GADTsによるPretermの定義は廃止
   • Wani内では（おそらく）DTTdeBruijnのみ参照すればよい

それに伴って以下の微修正も行いました。

• CCGパーザのSignatureは（UDTTではなく）DTTで記述するものとした（Template.hsやMyLexicon.hsを大幅修正）
• Aspコンストラクタの第一引数であったindexを廃止
• DTTにentity type, disjoint union typeを追加

今後の作業としては、以下を予定しています。

1. prove'関数のテスト
2. typeInfer/typeCheck関数のテスト
3. DTS.NaturalLanguageInference.checkInference関数の開発（今回のupdateの主目的）
4. mergeKWJA branchとのマージ（これによりJumanが必要なくなるので、ABCIにインストールできるようになる）
5. backwardRule branchとのマージ（＝Waniの最新版）

要望等ありましたら、お知らせください。