#「if構文はできるだけ右に延びるように括弧が省略される」を
#ReadPで対応しようとしてハマッたあげく、
#Parsec素直に使え!!という結論になった。
#でもやっぱり、問題はそこじゃない。 < いまここ
#ちなみに私のやったAgdaではその辺の優先順位は結構適当に付けていったら大体は文句なかった.
#Agda最強
#heyheyの宣伝忘れた.
#Agdaってパーザ簡単に書けるの？
#あー、そうか書いてないな
#Agdaでは構成子とオペレータでDSLっぽくしてて、その命題を手で解いて（証明して）、それをshowすることでオンライン演習用の表示にした.
#という流れになってて、問題をパースして自動証明するみたいなことはしてない.
#HaskellでTypeLevelで書くときはそんな感じでやりたいんだけど、showを定義するのがむずかしい。
#確かにshowするのは難しいか。
#証明オブジェクトを貰ってshowすると言っても、命題も印字しないといけなくて、それがagdaだと手が届くのでどってことないんだけど。
#そっか。
#例えばML2の場合だと
#判断のshowが型としてshowJudge⇓ : ∀ {ε e v} → ε ⊢ e ⇓ v → Stringとなってて
#{}の中は暗黙引数なんだけど
#ε ⊢ e ⇓ vに相当する証明オブジェクトを貰ったとしても{ε e v}のそれぞれの型も分かるのでshowが印字しようと思えばいける
#showDerivation⇓ {ε} {e} {v} p = showEnv ε ++ " |- " ++ showExp e ++ " evalto " ++ showValue v ++ " by " ++ showJudge⇓ p
#EvalML2のshowなんだけど,pが証明オブジェクトで、それ以外の{}の中のはそのpの型から分かる環境とか式とか値で、それを使って判断の型ε ⊢ e ⇓ vが出来ているからこいつを使って命題部分の印字が出来る
#Haskellだと証明オブジェクトからその証明オブジェクトの型であるところの命題に関する情報を取得するのが難しそう。Typeableでどこまで手に入るのか知らないけど。
haskell-ja > Archives > 2016/01/31