ATS で組み込みドライバを実装してみる③
「――何かを怠けるのに、理由が要るかい？」
はい、ATSでRXの端子ドライバを書いてみる③。今回で最終回です。
今回は、今まで準備してきた道具を使って、端子を操作する簡単なプログラム（証明付き）を書いてみます。
仕様
まずは、どんなプログラムを書くのかを決めねばなりません。↓のようなものを目指します。
① 起動する。
② P00端子に500ミリ秒間Highを出力する。
③ P00端子に250ミリ秒間Lowを出力する。
④ P00端子に400ミリ秒間Highを出力する。
⑤ P00端子にLowを出力する。
⑥ 終了する。
端子の番号は（見てわかる通り）適当です。もし、この端子の先にLEDが繋がっていれば、それが2回点灯することになります。いわゆるLチカです。
では次に、この仕様を型によって表現します。そのためにいくつか新しい定義を行います。
出力履歴
datasort output_duration = output_duration of (bit,int) datasort output_history = | output_hist_nil of () | output_hist_cons of (output_history,output_duration)
データ種を2つ定義します。
output_durationは、bitとintの引数を取り、bitの出力（1ならHigh、0ならLow）がintミリ秒続いたということを表します。
output_historyは、output_durationの配列です。
absview OutputDurationView (Pin,output_duration)
dataview OutputHistoryView (Pin,output_history) =
| {p:Pin}{d:output_duration}{hist:output_history}
OutputHistCons (p,output_hist_cons (hist,d))
of (OutputDurationView (p,d),OutputHistoryView (p,hist))
extern fn {p:Pin} newOutputHistoryView ():<> //<lin>
(OutputHistoryView (p,output_hist_nil) | void)データ種だけあっても仕方がないので、対応する観を定義します。
OutputDurationViewは、指定されたPinとoutput_durationに対応する観です。例えば「P26端子にHigh出力を400ミリ秒行った」というような事を表します。
OutputHistoryViewは、OutputDurationViewの配列です。
newOutputHistoryViewは、出力履歴の観（OutputHistoryView）を生成する関数です。これはあくまで空の観を生成するものであり、任意の観を自由に生成できるわけではありません。
空の出力履歴だけ作れても役には立ちませんので、履歴を追加するための関数を作成します。
extern fun wait_impl (term_millisec:uint): void = "ext#"
extern fn {pin:Pin}{b:bit}{hist:output_history}{t:int}
wait (!PinOutputView (pin,b),
!OutputHistoryView (pin,hist) >>
OutputHistoryView (pin,output_hist_cons (hist,output_duration (b,t)))
| term_millisec:uint t)
: void
implement {pin}{b}{hist}{t}
wait (output_v,hist_v | term_millisec)
= let
val+ () = wait_impl (term_millisec)
prval () = $UN.castview2void (hist_v)
in endはい、今回のキモになる定義です。
wait関数は、動的な動きだけで言えば、指定されたミリ秒数（term_millisec）だけ待機するだけの関数です。sleepとかdeleyとか、そんな名前の良くある関数と同等です。
違うのは静的な部分です。PinOutputViewとOutputHistoryViewという、2つの観型の引数を取ります。PinOutputViewはそのまま返しますが、OutputHistoryViewに関しては変更が加わったものを返します。
OutputHistoryViewは、OutputDurationViewの配列だと先に説明しましたが、wait関数は、受け取った出力履歴（OutputHistoryView）に出力の持続状態（OutputDurationView）の要素を一つ追加したものを返します。
追加されるOutputDurationViewは、PinOutputViewに対応する端子と出力状態、term_millisecに対応する出力期間を持ちます。
つまり、端子の出力状態（PinOutputView）を設定してwait関数を呼び出すと、その出力状態を持つ履歴が追加されるわけです。
厳密な話をすれば、wait関数を呼び出す前に再度出力状態を変えてしまうことが可能です。例えば、出力状態を何回も変更してからwait関数を呼び出した場合、最後の（wait関数を呼び出した時点の）状態しか履歴に現れないことになるわけですが、今回はそこは多めに見ることにします。実際、その状態で時間はほとんど（ナノ秒とかマイクロ秒とかの単位）進まないわけですし、普通は問題ないでしょう。
wait関数の中身ですが、wait_impl関数を呼んでいるだけです。wait_implは外部で定義することにします。
extern praxi {p:Pin} consumeOutputHistory // <lin>
(OutputHistoryView (p,
output_hist_cons (
output_hist_cons (
output_hist_cons (
output_hist_cons (output_hist_nil,
output_duration (I,500)),
output_duration (O,250)),
output_duration (I,400)),
output_duration (O,0)))): void「仕様」のところで書いた仕様を表す定義です。
OutputHistoryViewは観なので、一度生成してしまったら、消費しない限りそのプログラムはコンパイルを通りません。
そこで、OutputHistoryViewを消費する手段（ここでは、上記のconsumeOutputHistory関数）をひとつだけ用意することで、「その関数の型が許すような出力履歴が存在すること」を強制できるわけです。
ここでは、先ほど書いた仕様の②〜⑤を満たすような出力履歴を強制するようにしています。唯一、Pinについては可変にしていますが、これはその方が融通が効くだろうと言う判断です。
ゲームで例えると、洞窟の入り口かなんかが閉じられて、「このパズルを解かない限り、このダンジョンからは出られないぜ。くくくくく・・・」と悪役が親切に説明してくれるイベントのような状況です。
この場合は、newOutputHistoryView関数を呼び出すことで洞窟の入り口が閉じてしまい、引数として満足するような値を用意してconsumeOutputHistory関数を呼び出せれば、そこから抜け出せる（コンパイルが通る）というわけです。
そういうイベントって、詰み防止のためなのか回復手段とかが無駄に充実していて、却ってヌルい場合が多いですよね（ゲームでは）。
また、厳密な話をすると、この方法はいくつか穴があります。そもそもnewOutputHistoryView関数を呼び出さなければ普通にコンパイルが通ってしまうとか、OutputHistoryViewを複数個生成されてしまうことを防げない、とか色々ありますが、ここでは「そんな面倒くさいことする奴はおらんやろ」という仮定をおくことで全て不問に付します。どうせキャストされれば全部回避できちゃうし。
実装
細かい証明周りの定義とかあるのですが、省略します。
以下、main0関数の定義です。
implement main0 () = let
〜 中略 〜
prval (hist | ()) = newOutputHistoryView ()
prval podr_permit = (podr0perm,podr_cert01)
val+ () = writePODR (podr0,podr_permit | 0,beqint01)
prval (podr0perm,_) = podr_permit
prval PODR_V (podr07,podr06,podr05,podr04,podr03,podr02,podr01,podr00) = podr0
prval outview = (pfs00,pmr00,pdr00,podr00)
val+ () = wait (outview,hist | i2u 500)
prval (pfs00,pmr00,pdr00,podr00) = outview
prval podr0 = PODR_V (podr07,podr06,podr05,podr04,podr03,podr02,podr01,podr00)
prval podr_permit = (podr0perm,podr_cert00)
val+ () = writePODR (podr0,podr_permit | 0,beqint00)
prval (podr0perm,_) = podr_permit
prval PODR_V (podr07,podr06,podr05,podr04,podr03,podr02,podr01,podr00) = podr0
prval outview = (pfs00,pmr00,pdr00,podr00)
val+ () = wait (outview,hist | i2u 250)
prval (pfs00,pmr00,pdr00,podr00) = outview
prval podr0 = PODR_V (podr07,podr06,podr05,podr04,podr03,podr02,podr01,podr00)
prval podr_permit = (podr0perm,podr_cert01)
val+ () = writePODR (podr0,podr_permit | 0,beqint01)
prval (podr0perm,_) = podr_permit
prval PODR_V (podr07,podr06,podr05,podr04,podr03,podr02,podr01,podr00) = podr0
prval outview = (pfs00,pmr00,pdr00,podr00)
val+ () = wait (outview,hist | i2u 400)
prval (pfs00,pmr00,pdr00,podr00) = outview
prval podr0 = PODR_V (podr07,podr06,podr05,podr04,podr03,podr02,podr01,podr00)
prval podr_permit = (podr0perm,podr_cert00)
val+ () = writePODR (podr0,podr_permit | 0,beqint00)
prval (podr0perm,_) = podr_permit
prval PODR_V (podr07,podr06,podr05,podr04,podr03,podr02,podr01,podr00) = podr0
prval outview = (pfs00,pmr00,pdr00,podr00)
val+ () = wait (outview,hist | i2u 0)
prval (pfs00,pmr00,pdr00,podr00) = outview
prval podr0 = PODR_V (podr07,podr06,podr05,podr04,podr03,podr02,podr01,podr00)
prval () = consumeOutputHistory (hist)
〜 後略 〜
in end長すぎるので重要なところ以外はカットしました。
main0関数の定義です。長いです。アホみたいにちゃんとした証明を書こうとするとこういうことになるという、反面教師にでもするといいんじゃないでしょうか。
略した部分は、ほとんどが端子関係の初期化と後始末です。
重要なのはnewOutputHistoryView関数を呼び出す部分からconsumeOutputHistory関数を呼び出す部分までです（それでも長いけど）。
丁寧に見ていけば、「端子の状態設定→wait関数呼び出し」を繰り返して、目的の出力履歴をちまちまと作っていく様子が解ると思います。
まとめ
ﾔｯﾀｿﾞﾄﾞﾝﾄﾞｺﾄﾞｰﾝ!
というわけで「ATSで書くRXドライバ」、とりあえず完成しました。
完成と言っても実機での確認をしていないので、本当にちゃんと動くか？ っていうと、実はあんまり自信はないです。
証明は割ときっちりやっているので動く”はず”ですが、経験から言って動かしたことのないコードにそこまで自信は持てません。
じゃあ証明なんて意味無いじゃん、と思うかも知れませんが、こういう証明は「動く前」よりも「動いた後」に効いてくるんじゃないかと思ってます。
仕事でコーディングをしていて一番怖いのは「全く動かないコード」よりも「一見動いているように見えるが、実は問題を起こしているコード」です。動いているコードを比べた時、証明済みかどうかでその信頼性は全く違います。
証明 vs. テスト
テストをちゃんと書くのとどう違うの？ という疑問もあると思います。
結論から言うと、ほとんど変わりません。しっかりと書かれたテストというのは、証明とほぼ同じ信頼性をコードに与えてくれます。
問題は「テストをしっかり書くにはスキルと注意力が必要」ということです。
証明機能付き言語でのコーディングを経験した人なら感覚的にわかると思うのですが、しっかりと型付けをされたコードというのは、型を書いた人間が想定していなかった細かいケースまで勝手にカバーしてくれます。人間が「暗黙の了解」として省いてしまうような部分を、小姑のようにいちいち指摘してくれます。
型付けしたコードをいざ証明しようとして、「そんなレアケースある？」というようなケースまで証明しなければいけないということは良くある話です。そして、よくよく考えてみると、それはカバーしなければいけない、「実際にありえる」ケースだったりするのです（そうでなかったりもするけど）。
テストと証明の違いには、他にも「無限のパターンをテストはできないが、証明はできる」というのもあるのですが、上記が一番の違いだと僕は思っています。テストは「書いた人の想定した範囲しかカバーできない」ですが、証明は「想定外の範囲までカバーしてくれる」のです。
小学校の下駄箱に注意力を置き忘れてきた僕のような人間には、絶対に必要な性質がそこにはあるのです。
とは言え、現状では証明にかかるコストが高すぎます。
もっと環境整備が進めば解りませんが、現状では「注意しながらテストを書く」のが最良の方法になってしまうと思います。自動証明早よ。
ATSについてまとめ
ATSの評価ですが、やれることは非常に面白い反面、ガッツリ証明しようとしたりすると非常に辛いです。
特に辛いのは、簡単に通るはずの証明が、コンパイルしてみると「通らないぞ」って言われて、それが通らない理由が分からない、というケースです。大抵はちょっとしたケアレスミスなんですが、そこに辿り着くまでが本当に辛いです。
まあ、ただ、「ATSはそういう言語じゃないぞ」というのが正解なのだと思います。簡単な型注釈だけを使って、本格的な証明が必要なときはpraxiでも使ってごまかせば良い、というのが本来の使い方なのでしょう。
一方、線形型の仕組みは非常に面白いです。あれは良いものです。リソース管理をするのには本当に最適ですし、型の内容を自分でカスタマイズできるというのも良いです。使い方を考えているだけで最高に楽しいです。
＊急募＊『自制心』
あと、「証明が辛いさん」「高コスト」とさんざん書きましたが、「じゃあ、やらなきゃいいじゃん」と思われるかも知れません。
確かにそうなんですが、実際の作業はそう上手く行きません。↓の失敗事例をご覧ください。
① 型を眺めていて、そんなに難しい証明ではないような気がし始める。
② 簡単に証明できるならやっといた方がいいな、と思い、試してみる。
③ やってる内に夢中になってしまう。もし解ければ⑦へ、解けなければ④へ。
④ 諦めて他のことを始める。
⑤ あそこをこうしたらいいんじゃね？ と思いつく。
⑥ 思いついたアイデアを試しはじめる。③へ。
⑦ イヤッホオオオオウ！
こうなります。
特に、サイクルを何度も繰り返した末に⑦まで行ってしまうと重症です。気分は証明ジャンキーです。他の未証明な型を探して「これも証明できないかな？」とか考え始めて、また、③あたりからやり直しです。死ぬほど疲れます。
①か②あたりで踏みとどまれるような自制心を持ちましょう（僕が）。
証明が面白いのが悪い。
まとめのまとめ
さて、書きたいことはだいたい書いたと思います。まとめとしては
- 「証明は辛いけど面白いけど辛い」
- 「線形型はいいぞ」
- 「RenesasはOR/AND用のレジスタを作れ」
- 「自動証明早よ」
というところです。
RXドライバに関してはこれで（多分）終わりです。次回は証明プログラミングに関する妄想でも書こうかと思ってます。
では
