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ドライバに関してはこれで（多分）終わりです。次回は証明プログラミングに関する妄想でも書こうかと思ってます。
では
ATS で組み込みドライバを実装してみる②
プログラマの三大美徳
- 怠惰
- 怠惰
- アンド怠惰
スタンド攻撃を受けていて遅くなりました。「ATSで組み込みドライバを作ってみる」第二回です。端子ドライバ本体の解説をして行きたいと思います。
”端子”を”ドライブ”するぞ！
今回はハードウェアべったりな内容なので、詳しく理解したい人はRX110のユーザーズマニュアル（要ユーザー登録）を見ながら読むことをお勧めします。
https://www.renesas.com/ja-jp/doc/products/mpumcu/doc/rx_family/r01uh0421jj0120-rx110.pdf
一応、マニュアルを見ずに読む人にも配慮して書くつもりですが。そんな装備で大丈夫か？
端子
まずは端子を示すデータ種を定義します。
RXシリーズの端子は、0〜Jのポートと0〜7の番号の組み合わせで表現されます。
datasort IOPort = | Port0 of () | Port1 of () | Port2 of () | Port3 of () | Port4 of () | Port5 of () | Port6 of () | Port7 of () | Port8 of () | Port9 of () | PortA of () | PortB of () | PortC of () | PortD of () | PortE of () | PortF of () | PortG of () | PortH of () | PortI of () | PortJ of ()
まずはポートから、0〜Jのポートの定義です。
何も足さない、何も引かないっていう感じの定義ですね。
RX110には存在しないポート（ポート６とかDとか）も有りますが、互換性のために定義しています。
stacst IOPort2int (p:IOPort):int
praxi ioport_eq_int ():[
IOPort2int Port0 == 0 && IOPort2int Port1 == 1 &&
IOPort2int Port2 == 2 && IOPort2int Port3 == 3 &&
IOPort2int Port4 == 4 && IOPort2int Port5 == 5 &&
IOPort2int Port6 == 6 && IOPort2int Port7 == 7 &&
IOPort2int Port8 == 8 && IOPort2int Port9 == 9 &&
IOPort2int PortA == 10 && IOPort2int PortB == 11 &&
IOPort2int PortC == 12 && IOPort2int PortD == 13 &&
IOPort2int PortE == 14 && IOPort2int PortF == 15 &&
IOPort2int PortG == 16 && IOPort2int PortH == 17 &&
IOPort2int PortI == 18 && IOPort2int PortJ == 19
] void
typedef ioport_t (p:IOPort) = int (IOPort2int p)はい、IOPort種からint種に変換する静的な関数IOPort2intを、stacstで定義しています。
関数と言っても中身はすっからかんなので、praxiを使ってintとの対応を定義しています。
ioport_tは、IOPort種に対応するint型を定義するための糖衣構文です。前回のbits_uint_tと同じような奴です。
datasort Pin = Pin of (IOPort,int)
で、端子を示すデータ種Pinを定義します。intには0〜7の制約を掛けたいところですが、「種」の段階でそれを行う方法は無いようです。
typedef pin_t (p:IOPort,n:int) = @(ioport_t p, uint n)
pin_tは、ioport_tと組み合わせてPinに対応する型を定義しています。これも糖衣構文なので、必ずこれを使わなければならない訳ではありません。
あと、組み込み向けであることを考慮して、タプルはアンボックスタプルを採用します。ガベージコレクションなんて組み込みでは使えない場合が多いですし、できれば動的メモリ確保も使わないように書いてゆく予定です。
stadef P0 (n:int):Pin = Pin (Port0,n) stadef P1 (n:int):Pin = Pin (Port1,n) stadef P2 (n:int):Pin = Pin (Port2,n) stadef P3 (n:int):Pin = Pin (Port3,n) stadef P4 (n:int):Pin = Pin (Port4,n) stadef P5 (n:int):Pin = Pin (Port5,n) stadef P6 (n:int):Pin = Pin (Port6,n) stadef P7 (n:int):Pin = Pin (Port7,n) stadef P8 (n:int):Pin = Pin (Port8,n) stadef P9 (n:int):Pin = Pin (Port9,n) stadef PA (n:int):Pin = Pin (PortA,n) stadef PB (n:int):Pin = Pin (PortB,n) stadef PC (n:int):Pin = Pin (PortC,n) stadef PD (n:int):Pin = Pin (PortD,n) stadef PE (n:int):Pin = Pin (PortE,n) stadef PF (n:int):Pin = Pin (PortF,n) stadef PG (n:int):Pin = Pin (PortG,n) stadef PH (n:int):Pin = Pin (PortH,n) stadef PI (n:int):Pin = Pin (PortI,n) stadef PJ (n:int):Pin = Pin (PortJ,n)
Pin型の値を表現するための糖衣構文です。
例えば「Pin (Port0,1）」と書く代わりに「P0(1)」または「P0 1」という風に書けるわけですが、今回書いた中では使ってません。
あれば便利だと思って定義するけど存在を忘れちゃうパターン。
bisectional
レジスタの定義に移る前に、前準備としてbisectionalというデータ種を定義します。
datasort bisectional = bisectional of (int,int)
stadef bisect1 = bisectional (1,0)
dataprop EQBISECTIONAL (bisectional, bisectional) = {r:bisectional} EQBISECTIONAL (r, r)
praxi eqbisectional_make {r,s:bisectional | r == s} () : EQBISECTIONAL (r,s)
praxi bisectional_eq_refl {r:bisectional} () : [r == r] void
praxi bisectional_eq_reduce {n,m:int | n <= INTMAX_HALF} ():
[bisectional (n,m) == bisectional (n+n,m+1)] voidこれは何かって言うと、有理数（分数）型の変種で、分母になる数を２のべき乗数に限定したものです。
「bisectional (n,m)」で、「n/2^m」という意味になります。
「bisectional_eq_reduce」が、約分した数は同じ数だぞ、ということを言っています。あと、bisect1は「1/1」を表すための定義です。
このbisectionalを何に使うのかということですが、実例が無いと解りづらいと思うので、もう少し後で説明します。
さて、上の定義を見て違和感を覚えた人もいるかも知れません。bisectionalに関しては、今まで「propスタイル」でやっていた記述を「boolスタイル」でやっています。
これは、ATSのメーリングリスト（https://groups.google.com/forum/#!topic/ats-lang-users/nOOWnYoo5ko）で「何でpropでやってんだよ、boolのほうが楽だろ おらああぁぁん！？（意訳）」と突っ込まれたせいです。
せっかく指摘してもらっといて何なのですが、boolスタイルはいまいちピンと来ないというか、propスタイルでちまちま証明していくほうが楽しいし、性にあってるような気がする……
boolスタイルとpropスタイルについて知りたい人は、これ（）か、その原文（EFFECTIVATS-PwTP-bool-vs-prop）を読んでみると良いでしょう。
stacst bisectional_add_b : (bisectional,bisectional,bisectional) -> bool
praxi {n1,n2,m:int} bisectional_add_axi ():
[bisectional_add_b (bisectional (n1,m),bisectional (n2,m),bisectional (n1+n2,m))] unit_pbisectional同士の足し算の定義です。
stacst bisectional_half_b : (bisectional,bisectional) -> bool
praxi {n,m:int} bisectional_half_axi ():
[bisectional_half_b (bisectional (n,m),bisectional (n,m+1))] unit_p
praxi {n,m,l:int} bisectional_half_axi_rev {bisectional_half_b (bisectional (n,m),bisectional (n,l))}(): [m+1==l] unit_p今度は割り算・・・ではなく、「半分に割る」ための定義です。
bisectionalの基本的な使い方は、「1/1 → 半分に割る → 割った同士を足す → 約分して元に戻す」という形になります。
何でそんなものが必要なのかは、すぐ後のPMRの説明の中で解説します。
PMR
さて、ここからレジスタに関する定義です。
まずはPMRです。マニュアルをお持ちの方は、17-3-4を開いて下さい（Eテレっぽい口調で）。
端子の機能（汎用入出力／周辺機能）を選択するレジスタです。
PMRは「Port Mode Register」の略みたいです。
absview PMR_BIT_V (Pin,bit,bisectional) ~ 中略 ~ stadef PMR_BIT_IOPORT = O stadef PMR_BIT_PERIPHERAL = I
PMRは、ポートごとに一つのレジスタがあり、レジスタの1ビットが一つの端子に対応しています。つまり、レジスタ一つで8つの端子を制御するわけです。
ですが、8ビット全てを表す定義を作ってしまうと後で分解するのが大変になるため、ここでは1ビット（=端子一つ）の状態を表す「観」を定義しています。後で8つまとめてくっつけます。
「観」については説明すると長くなるのですが、分かりやすく言うと「作ったり消したりするのに制約がある命題」（分かりやすく言えるとは言ってない）です。分かりにくく言うと「線形論理か適用される命題」「弱化規則と縮約規則が適用できない命題」です（こっちは大丈夫！）。
知らないところで作れてしまうと困るので、absviewで定義しています。後で初期値を生成する関数を定義します。
PMR_BIT_IOPORTとPMR_BIT_PERIPHERALは見たまんまの定数定義です。IやOの代わりに使いましょう。文字数は多くなりますが、そんな頻繁に使う定数でもないでしょう。
dataview PMR_V (IOPort,bits) =
{p:IOPort}{b7,b6,b5,b4,b3,b2,b1,b0:bit}
PMR_V (p,Bits8 (b7,b6,b5,b4,b3,b2,b1,b0)) of
(PMR_BIT_V (Pin (p,7),b7,bisect1), PMR_BIT_V (Pin (p,6),b6,bisect1),
PMR_BIT_V (Pin (p,5),b5,bisect1), PMR_BIT_V (Pin (p,4),b4,bisect1),
PMR_BIT_V (Pin (p,3),b3,bisect1), PMR_BIT_V (Pin (p,2),b2,bisect1),
PMR_BIT_V (Pin (p,1),b1,bisect1), PMR_BIT_V (Pin (p,0),b0,bisect1))はい、さっき書いた「まとめてくっつける定義」です。レジスタいっこ分（=ポートいっこ分）のPMR_BIT_Vをまとめています。
長くて一見難しげな定義ですが、よく見れば大したことは言ってません。
PMR_BIT_VとPMR_Vは、スライムとキングスライムのような関係です。PMR_BIT_Vが8つあるとPMR_Vが1つできて、PMR_Vが1つあるとPMR_BIT_Vが8つできます。
absview PMR_PERMISSION (IOPort,bit_permissions)
viewdef PMR_PERMIT (p:IOPort,bs:bits) =
[perms:bit_permissions]
(PMR_PERMISSION (p,perms),BITS_PERMIT_CERTIFICATE (8,perms,bs))PMRには書き込みが制限されるビット（P35とPH7に対応するビット）があるため、書き込み制限を表すための命題（PMR_PERMISSION）を定義します。
勝手に許可を作れてしまうと事実上フリーパスになってしまうので、absviewを使って定義します。これも、後で初期値を生成するための関数を定義します。
PMR_PERMITは「許可済みである証拠」を表す命題です。「PMR_PERMIT (PortA,bs)」という証明があれば、「bsはPortAに対応するPMRに書いて良い」という許可の証拠になります。
これはどうするべきか迷ったのですが、普通の命題（Prop）ではなく観（View）として定義します。レジスタへの書き込み許可が動的に変更されることが一応（具体的に何だったか忘れたけど）あり得るので。
fn {p:IOPort}{bs,cs:bits}
writePMR (!PMR_V (p,bs) >> PMR_V (p,cs),
!PMR_PERMIT (p,cs)
| ioport_t p,bits_uint_t (8,cs))
:<!wrt> void
fn {p:IOPort}{bs,cs:bits}{b:bit}
changePMRBit {bn:int | bn < 8}
(CHANGE_BIT_BITS (8,bs,bn,b,cs),
!PMR_V (p,bs) >> PMR_V (p,cs),
!PMR_PERMIT (p,cs)
| pin_t (p,bn), bit_uint_t b):<!refwrt> void
fn {p:IOPort}{bs:bits}
readPMR (!PMR_V (p,bs) | p:ioport_t p)
:<!ref> bits_uint_t (8,bs)はい、ここで残念なお知らせです。
レジスタへの読み込み／書き込みを行う関数を定義するわけですが、当初の予定ではこれをPMR_BIT_V（ビットひとつ分の観）を受け取る関数として定義する予定でした。
PMRに限らず、IOポートのレジスタは１ポートごとにひとつ用意されています。１ポートには８つの端子があるのですが、この８つの端子は別に隣同士で並んでいるわけではなく、仮に並んでいたとしても、８つの端子をひとまとめにして使うメリットなんて殆どありません（ディップスイッチの１ビット毎に割り当てる位・・・？）。
なので、マルチスレッドで運用するイメージとしては、初期化時に各スレッドに対して必要な端子の観（PMR_BIT_Vとか）を割り振って、そのあとは各スレッドで好き勝手に端子の操作を行う―――という風にしたかったわけです。
わけですが、これが不可能でした。読み込みに関しては問題ないのですが、レジスタ中の１ビットを変更するためには、まずレジスタの値を８ビット全て読み込んで、ビットORで必要なビットを立てて、それを書き戻す必要があるのです。当然ながら、これはアトミックな操作にはなりません。書き戻しの直前に他のスレッドが割り込んで書き換えてしまえば全て終わりです。書き込みの保証もクソもありません。何気ない書き戻しが重要な状態変化を傷つけて、核ミサイルが誤発射とかされて人類は滅亡です。
人類が生き延びるためには、ビットごとの操作を諦めてポートごとの操作をするしかありません。複数のスレッドが同じポートの端子を操作する場合は、セマフォかなんかの同期処理を用意して操作権限を管理するしかありません。ちょーめんどくさいやつです。動作も遅くなります。いいことなんてひとつもありません。
余談ですが、他のSoCではこの問題は解決されているものがあります。あんまり詳しいわけではないのですが、少なくともam335x(これ→http://www.ti.com/jp/lit/pdf/spruh73の5012ページ)なんかでは、同期の必要性を排除するためにビットのセット用／クリア用のレジスタが用意されていたりします。
セット用レジスタでは０に設定したビットが無視されます。逆にクリア用では１に設定したビットが無視されるようになっています。これによって、特定の端子だけを（他の端子の影響を受けずに）操作することができるわけです。
RXも、そういうのを導入してくれるといいんですが・・・。
閑話休題。グチはここらへんにして、関数の説明に戻ります。いっこずつ行きましょう。
fn {p:IOPort}{bs,cs:bits}
writePMR (!PMR_V (p,bs) >> PMR_V (p,cs),
!PMR_PERMIT (p,cs)
| ioport_t p,bits_uint_t (8,cs))
:<!wrt> voidPMRに値を書き込む関数です。
書き込み許可（PMR_PERMIT_V）を示す必要があります。あと、現在のレジスタ観（PMR_V）も必要で、これは実行後に更新されて戻ってきます。
実装をどうするかですが、これはC言語の単純な書き込み関数を用意して、強制型キャストで強引に呼び出すことで解決します。一番下のレイヤーなのでしゃーなしです。
fn {p:IOPort}{bs:bits}
readPMR (!PMR_V (p,bs) | p:ioport_t p)
:<!ref> bits_uint_t (8,bs)読み込み関数です。こっちはPMR_PERMIT_Vを受け取る必要はありません。
読み込み関数の型を見ていると、「bsが初めから解ってるなら、わざわざ読み込む必要なくない？」と言うようなことを思ってしまいがち（思うよね？）ですが、実際にはbsの中身が確定していない場合があるので、そういう時にはreadPMRを呼び出して確定させる必要があります。具象型（bits_uint_t）の動的な値によって静的な値（bits）が決まるわけです。魚を獲ったら針と釣り竿が付いてきた、みたいな感じですね。
fn {p:IOPort}{bs,cs:bits}{b:bit}
changePMRBit {bn:int | bn < 8}
(CHANGE_BIT_BITS (8,bs,bn,b,cs),
!PMR_V (p,bs) >> PMR_V (p,cs),
!PMR_PERMIT (p,cs)
| pin_t (p,bn), bit_uint_t b):<!refwrt> void1ビットごとの書き込みを行う関数です。
内部的にはreadPMRとwritePMRを呼び出すことで実現しています。アトミックな操作では（上で書いた理由のせいで）ないので、マルチスレッド環境では呼び出し側で排他制御を行う必要があります。
また、上の3つの関数は「書き込みが確実に成功すること」と「書き込み以外でレジスタの値が変わらないこと」を前提にした定義です。もしもどちらかの条件が成り立たなくなった場合（ないと思うけど）は、証明の正当性は失われてしまうことに注意してください。
PMR_BIT_Vとbisectional
さて。読者の皆さんはPMR_BIT_Vの定義の中にbisectionalが入っていることに気付いていたでしょうか？ 気付かなかった皆さんは、自分で書いたくせに忘れていた筆者と同レベルのボンクラです。ﾅｶｰﾏ!
先の項で予告していたとおり、ここでbisectionalの用途について解説を行います。
PMR_Vの定義の中で、PMR_BIT_Vの記述がありますが、例えば「(PMR_BIT_V (Pin (p,7),b7,bisect1)」のような形になっていました。"7"の部分が変動するほかは全て同じです。
注目してほしいのは「bisect1」の部分です。PMR_VとPMR_BIT_Vはキングスライムとスライムの関係だと先に書きましたが、PMR_Vの（「bisect1」の部分の）定義からPMR_VとPMR_BIT_Vの間の関係がふたつ導かれます。ひとつは「PMR_Vから分裂した直後のPMR_BIT_Vは、bisect引数が1/1になる」ということであり、もうひとつは「PMR_BIT_Vを合体させてPMR_Vを作るには、PMR_BIT_Vのbisect引数が全て1/1でなければならない」ということです。
ちょっと順番は前後しますが、以上を踏まえて次の定義（ファイル上ではPMR_BIT_Vの辺り）を見てください。
praxi {p:Pin}{b:bit} divide_pmr_bit_v {r,s:bisectional | bisectional_half_b (r,s)}
(PMR_BIT_V (p,b,r)) : (PMR_BIT_V (p,b,s),PMR_BIT_V (p,b,s))
praxi {p:Pin}{b:bit} merge_pmr_bit_v {r,s,t:bisectional | bisectional_add_b (r,s,t)}
(PMR_BIT_V (p,b,r), PMR_BIT_V (p,b,s)):(PMR_BIT_V (p,b,t))divide_pmr_bit_vは、PMR_BIT_Vを「分裂」させて2つのPMR_BIT_Vを作成します。
merge_pmr_bit_vはその逆を行います。すなわち、2つのPMR_BIT_Vを「合体」させて1つのPMR_BIT_Vを作成します。
この時、PMR_BIT_Vのbisect引数は、それぞれ「半分」及び「足し算」されます。
以上から、次のようなPMR_BIT_Vの性質が導かれます。
「PMR_Vは、それぞれのビットに対応する8つのPMR_BIT_Vに変換できる」
「それぞれのPMR_BIT_Vは、いくらでも（divide_pmr_bit_vによって）分割できる」
「PMR_BIT_VからPMR_Vを作成するには、分割したPMR_BIT_Vを全て集めて（merge_pmr_bit_vによって）合体させないといけない」
で、なんのためにこんなものが必要なのかですが。
例えば、ある端子の状態を周期的に確認するスレッドがあるとします。端子の状態を確認するには、PMRが汎用入出力になっている必要があるのですが、前に愚痴っていたとおりRXではビット単位の読み書きを行うことはできません。だからと言ってそのスレッドにPMR_Vを渡してしまうと、他のスレッドが同じPMR_Vを参照できなくなります。他のスレッドが参照するにはいちいち同期をとってPMR_Vを受け渡さなければならなくなり、渡している間はPMR_Vを参照できなません。
端子の状態を確認する度に同期の手間がかかるというのはあまりにも煩雑です。他のスレッドが参照するのが違う端子だと言う場合（大抵はそうでしょう）なら、なおさらです。そもそもこの手の設定というのは、起動時に一度だけ設定して後は全く触らないというケースがほとんどなので、予期せぬ変更に怯えながら状態を確認するような手順を取らなければならないのはナンセンスです。
そこで、そういったケースではPMR_BIT_Vを使います。PMR_BIT_Vならば、ビット毎に分割されているため、違う端子を扱うスレッドには別々の観を与えればそれで済んでしまいます。同じ端子を扱う場合にも、divide_pmr_bit_vを使って分割すれば良いでしょう。
上の方で紹介したとおり、PMR読み書き関数は必ずPMR_Vを引数に取ります。よってPMR_BIT_Vを持っているスレッドは「PMR_BIT_Vが自分の手元にある限り、PMRは変更されない」という保証を得ることになります。「このドラゴンボールが俺の元にある限り、やつらはどれだけ頑張っても神龍を呼び出せないのさ・・・」みたいな状況です。
ちなみに、PMR_BIT_Vを各スレッドに配った後にPMRを変更したくなった場合は、スレッド間の同期を取ってPMR_BIT_Vを全て集めてくる必要があります。非常に面倒くさいです。そんな変更したくならない様に頑張りましょう。
PWPR, PFS
PFS（端子機能制御レジスタ、マニュアルの18-2-2〜11）は、それぞれの端子をどの周辺機能（または汎用入出力）に割り当てるか選択するためのレジスタです。
一度実装しようとしたのですが、このレジスタを変更できるようにすると色々と面倒なことが増えてしまうため、結局廃止（コメントアウト）しました。
absview PFS_V (Pin,bits)
唯一、PFSのレジスタ観（PFS_V）は端子ドライバから参照する必要があるために残してあります。PFSの初期値は必ず汎用入出力になっているため、今回作成した範囲ではレジスタの変更ができなくても支障ありません。
PWPR（書き込みプロテクトレジスタ、マニュアルの18-2-1）はPFSへのハードウェア的な書き込み許可を制御するためのレジスタです。PFSへの書き込みをサポートしないので必要ありません。これもコメントアウトしてあります。
PDR
PDRはポート方向レジスタです。詳しくは、ハードウェアマニュアルの17.3.1を参照して下さい。
「端子ごとの入力/出力を指定するレジスタ」と説明されていますが、より正確に言うと「端子をドライブするかどうかを指定するレジスタ」です。出力に指定しても端子状態を読み込む機能（PIDR）は生きていますし、それが出力した値と一致するとは限りません（回路がオープンになっている場合とか）。
stadef PDR_BIT_WRITABLE = I
stadef PDR_BIT_READ_ONLY = O
absview PDR_BIT_V (Pin,bit,bisectional)
praxi {p:Pin}{b:bit} divide_pdr_bit_v {r,s:bisectional | bisectional_half_b (r,s)}
(PDR_BIT_V (p,b,r)) : (PDR_BIT_V (p,b,s),PDR_BIT_V (p,b,s))
praxi {p:Pin}{b:bit} merge_pdr_bit_v {r,s,t:bisectional | bisectional_add_b (r,s,t)}
(PDR_BIT_V (p,b,r), PDR_BIT_V (p,b,s)):(PDR_BIT_V (p,b,t))
dataview PDR_V (p:IOPort,bits) =
{p:IOPort}{b7,b6,b5,b4,b3,b2,b1,b0:bit}
PDR_V (p,Bits8 (b7,b6,b5,b4,b3,b2,b1,b0)) of
(PDR_BIT_V (Pin (p,7),b7,bisect1), PDR_BIT_V (Pin (p,6),b6,bisect1),
PDR_BIT_V (Pin (p,5),b5,bisect1), PDR_BIT_V (Pin (p,4),b4,bisect1),
PDR_BIT_V (Pin (p,3),b3,bisect1), PDR_BIT_V (Pin (p,2),b2,bisect1),
PDR_BIT_V (Pin (p,1),b1,bisect1), PDR_BIT_V (Pin (p,0),b0,bisect1))
absview PDR_PERMISSION (IOPort,bit_permissions)
viewdef PDR_PERMIT (p:IOPort,bs:bits) =
[perms:bit_permissions]
(PDR_PERMISSION (p,perms),BITS_PERMIT_CERTIFICATE (8,perms,bs))
fn {p:IOPort}{bs,cs:bits}
writePDR (!PDR_V (p,bs) >> PDR_V (p,cs),
!PDR_PERMIT (p,cs)
| ioport_t p,bits_uint_t (8,cs)):<!wrt> void
fn {p:IOPort}{bs,cs:bits}{b:bit}
changePDRBit {bn:int | bn < 8}
(CHANGE_BIT_BITS (8,bs,bn,b,cs),
!PDR_V (p,bs) >> PDR_V (p,cs),
!PDR_PERMIT (p,cs)
| pin_t (p,bn), bit_uint_t b):<!refwrt> void
fn {p:IOPort}{bs:bits}
readPDR (!PDR_V (p,bs) | ioport_t p)
:<!ref> bits_uint_t (8,bs)PDR関連の定義です。さっき言いたいことは大体言って満足したので、解説は省略します。PMRと大体同じです（雑）。
PODR
ポート出力データレジスタです。マニュアルでは17-3-2に書いてあります。
ここに書いた値が端子から出力されるわけですが、PDRの対応するビットが1（出力）になっていないと有効になりません。そこら辺の対応は後で形式化します。
stadef PODR_BIT_HIGH = I
stadef PODR_BIT_GROUND = O
absview PODR_BIT_V (Pin,bit,bisectional)
praxi {p:Pin}{b:bit} divide_podr_bit_v {r,s:bisectional | bisectional_half_b (r,s)}
(PODR_BIT_V (p,b,r)) : (PODR_BIT_V (p,b,s),PODR_BIT_V (p,b,s))
praxi {p:Pin}{b:bit} merge_podr_bit_v {r,s,t:bisectional | bisectional_add_b (r,s,t)}
(PODR_BIT_V (p,b,r), PODR_BIT_V (p,b,s)):(PODR_BIT_V (p,b,t))
dataview PODR_V (p:IOPort,bits) =
{p:IOPort}{b7,b6,b5,b4,b3,b2,b1,b0:bit}
PODR_V (p,Bits8 (b7,b6,b5,b4,b3,b2,b1,b0)) of
(PODR_BIT_V (Pin (p,7),b7,bisect1), PODR_BIT_V (Pin (p,6),b6,bisect1),
PODR_BIT_V (Pin (p,5),b5,bisect1), PODR_BIT_V (Pin (p,4),b4,bisect1),
PODR_BIT_V (Pin (p,3),b3,bisect1), PODR_BIT_V (Pin (p,2),b2,bisect1),
PODR_BIT_V (Pin (p,1),b1,bisect1), PODR_BIT_V (Pin (p,0),b0,bisect1))
absview PODR_PERMISSION (IOPort,bit_permissions)
viewdef PODR_PERMIT (p:IOPort,bs:bits) =
[perms:bit_permissions]
(PODR_PERMISSION (p,perms),BITS_PERMIT_CERTIFICATE (8,perms,bs))
fn {p:IOPort}{bs,cs:bits}
writePODR (!PODR_V (p,bs) >> PODR_V (p,cs),
!PODR_PERMIT (p,cs)
| ioport_t p, bits_uint_t (8,cs)):<!wrt> void = "ext#"
fn {p:IOPort}{bs,cs:bits}{b:bit}
changePODRBit {bn:int | bn < 8}
(CHANGE_BIT_BITS (8,bs,bn,b,cs),
!PODR_V (p,bs) >> PODR_V (p,cs),
!PODR_PERMIT (p,cs)
| pin_t (p,bn), bit_uint_t b):<!refwrt> void
fn {p:IOPort}{bs:bits}
readPODR (!PODR_V (p,bs) | ioport_t p)
:<!ref> bits_uint_t (8,bs)PMRとかと大体同じ定義ですね。ﾄｸﾆｲｳｺﾄﾊﾅｲ。
PIDR
ポート入力データレジスタです。マニュアルの17-3-3です。
PODRと対になるレジスタ・・・と思いがちですが違います。このレジスタは、対応する端子の「現在の信号状態」を自動的に反映するという、やや特殊なレジスタです。PMRやPDRもガン無視して端子状態を反映します。
absprop PIDR_BIT_P (Pin,bit)
dataprop PIDR_P (p:IOPort,bits) =
{p:IOPort}{b7,b6,b5,b4,b3,b2,b1,b0:bit}
PIDR_P (p,Bits8 (b7,b6,b5,b4,b3,b2,b1,b0)) of
(PIDR_BIT_P (Pin (p,7),b7), PIDR_BIT_P (Pin (p,6),b6),
PIDR_BIT_P (Pin (p,5),b5), PIDR_BIT_P (Pin (p,4),b4),
PIDR_BIT_P (Pin (p,3),b3), PIDR_BIT_P (Pin (p,2),b2),
PIDR_BIT_P (Pin (p,1),b1), PIDR_BIT_P (Pin (p,0),b0))PIDRの状態を表す命題です。PMRやPODRとは違い、観ではなく命題として定義しています。
これは、現在の端子状態を厳密に知ることは出来ないためです。まず、PIDRは読み込み専用のレジスタであり、書き込むことは出来ません。レジスタを読み込んだ時の状態を知る以外のことは出来ないわけです。
そして、ある時点でPIDRの値を読んで「その時点での状態」がわかったとしても、次の命令が実行されるまでの間にその状態が持続している可能性はありません。
観にすることによって、「最後に読み込んだ時点の状態」を保証することは出来ますが、それにしたところで最後に読み込んだのが一秒前なのか、一時間前なのかを保証することは出来ません。ならば、取り回しの悪さを我慢してまで観にこだわるより、命題にしてしまったほうが扱いやすいと判断しました。
「ある時点での端子状態」を保証したいような場合は、別の手段で確保すれば良いでしょう。
fn {p:IOPort} readPIDR (ioport_t p)
:<!ref> [bs:bits] (PIDR_P (p,bs) | bits_uint_t (8,bs))読み込み関数です。PMRなどと違い、引数に観や命題を渡す必要はありません。
端子観
やっとここまで来ました。端子の出力状態を表す観（PinOutputView）です。
viewdef PinOutputView (p:Pin,output:bit) = [isel:bit][s,r,t:bisectional] (PFS_V (p,Bits8 (O,isel,O,O,O,O,O,O)), PMR_BIT_V (p,O,s),PDR_BIT_V (p,I,r),PODR_BIT_V (p,output,t))
「PinOutputView (p,b)」とあった場合、端子（p）の出力状態がbであること（trueならHigh、falseならLow）を表してます。
PFS、PMR、PDR、PODRの観を集合して作られているので、端子を「b」の状態にドライブしていることが保証されます。
例えば何かの関数で、処理中にある端子がLow出力であって欲しいというような場合、関数の引数にPinOutputViewを追加すれば良いわけです。PinOutputViewは変更用の観も含んでいるので、自分がそれを握っている限りは他のスレッドなどで出力が変更されないことも保証してくれます。
absprop PinInput (Pin,bit)
fn readPinInput {p:IOPort}{n:int}{isel:bit}{s,r:bisectional}
(!PFS_V (Pin (p,n),Bits8 (O,isel,O,O,O,O,O,O)),
!PMR_BIT_V (Pin (p,n),O,s),!PDR_BIT_V (Pin (p,n),O,r) | pin_t (p,n))
:<!ref> [input:bit] (PinInput (Pin (p,n),input) | bool (input==I))端子の入力を表す抽象命題「PinInput」と、入力状態読み込み関数「readPinInput」です。
注意して欲しいのは、PinInputは「読み込んだ時の状態」を表しているに過ぎないと言うところです。PinOutputViewでは保持している間の出力状態を保証してくれましたが、PinInputではそういった保証はありません。なので、観ではなく命題で表現しています。
初期状態・終了処理
praxi rx110_initial_pmr_views () :
(PMR_V (Port0,Bits8_all0),PMR_V (Port1,Bits8_all0),
PMR_V (Port2,Bits8_all0),PMR_V (Port3,Bits8_all0),
PMR_V (Port4,Bits8_all0),PMR_V (Port5,Bits8_all0),
PMR_V (PortA,Bits8_all0),PMR_V (PortB,Bits8_all0),
PMR_V (PortC,Bits8_all0),PMR_V (PortE,Bits8_all0),
PMR_V (PortH,Bits8_all0),PMR_V (PortJ,Bits8_all0),
PMR_PERMISSION (Port0,BitPerms8_all), PMR_PERMISSION (Port1,BitPerms8_all),
PMR_PERMISSION (Port2,BitPerms8_all), PMR_PERMISSION (Port3,BitPerms8_all),
PMR_PERMISSION (Port4,BitPerms8_all), PMR_PERMISSION (Port5,BitPerms8_all),
PMR_PERMISSION (PortA,BitPerms8_all), PMR_PERMISSION (PortB,BitPerms8_all),
PMR_PERMISSION (PortC,BitPerms8_all), PMR_PERMISSION (PortE,BitPerms8_all),
PMR_PERMISSION (PortH,BitPerms8_all), PMR_PERMISSION (PortJ,BitPerms8_all)
)
praxi rx110_consume_pmr_views (
PMR_V (Port0,Bits8_all0),PMR_V (Port1,Bits8_all0),
PMR_V (Port2,Bits8_all0),PMR_V (Port3,Bits8_all0),
PMR_V (Port4,Bits8_all0),PMR_V (Port5,Bits8_all0),
PMR_V (PortA,Bits8_all0),PMR_V (PortB,Bits8_all0),
PMR_V (PortC,Bits8_all0),PMR_V (PortE,Bits8_all0),
PMR_V (PortH,Bits8_all0),PMR_V (PortJ,Bits8_all0),
PMR_PERMISSION (Port0,BitPerms8_all), PMR_PERMISSION (Port1,BitPerms8_all),
PMR_PERMISSION (Port2,BitPerms8_all), PMR_PERMISSION (Port3,BitPerms8_all),
PMR_PERMISSION (Port4,BitPerms8_all), PMR_PERMISSION (Port5,BitPerms8_all),
PMR_PERMISSION (PortA,BitPerms8_all), PMR_PERMISSION (PortB,BitPerms8_all),
PMR_PERMISSION (PortC,BitPerms8_all), PMR_PERMISSION (PortE,BitPerms8_all),
PMR_PERMISSION (PortH,BitPerms8_all), PMR_PERMISSION (PortJ,BitPerms8_all)
): voidはい、何度か話に出てきた「初期状態の観」をまとめて生成する関数と、生成した観の後始末をする関数です。
rx110_initial_pmr_viewsは、初期状態（全ビット０）のレジスタ観「PMR_V」を生成します。普通は起動時に呼び出すことになるでしょう。作られた観は必ず後始末をしなければいけないので、終了時にrx110_consume_pmr_viewsを呼び出して後始末をします。
Bits8_all0は、全ビットが０のBits８として定義してあります。上の定義では、初期状態のレジスタが全て０で、終了する時にも全て０でなければならないということを表しています。
PMRへの書き込み許可「PMR_PERMISSION」も観として定義したので、ここで初期状態を与えています。BitPerms8_allは、８ビットのどの値も許可するということを意味しています。
割とキモになる定義なのですが、残念ながら、初期状態関数（この例ではrx110_initial_pmr_views）が何回も呼ばれることは禁止できませんでした（ATSでは手段がないっぽい？）。初期状態関数を何回も呼び出すとレジスタ観が無数に手に入って、矛盾した状態が作り放題になってしまいます。これは運用で禁止するしかないようなので、（そんなことはしないと思うけど）気をつけましょう。
なお、終了関数呼び出し後に初期化関数を呼び出すことは特に問題ありません。そのために、終了状態関数の引数に初期状態と同じ制約（終了時には起動時と同じ状態にせよ、という意味になる）をつけてあります。そんな需要があるのか、と思うかも知れませんが、一応、ミスを防止するための意味もあるので。
praxi rx110_initial_pfs_views ():
(PFS_V (Pin (Port0,0),Bits8_all0),PFS_V (Pin (Port0,1),Bits8_all0),
PFS_V (Pin (Port0,2),Bits8_all0),PFS_V (Pin (Port0,3),Bits8_all0),
PFS_V (Pin (Port0,4),Bits8_all0),PFS_V (Pin (Port0,5),Bits8_all0),
PFS_V (Pin (Port0,6),Bits8_all0),PFS_V (Pin (Port0,7),Bits8_all0),
PFS_V (Pin (Port1,0),Bits8_all0),PFS_V (Pin (Port1,1),Bits8_all0),
PFS_V (Pin (Port1,2),Bits8_all0),PFS_V (Pin (Port1,3),Bits8_all0),
PFS_V (Pin (Port1,4),Bits8_all0),PFS_V (Pin (Port1,5),Bits8_all0),
PFS_V (Pin (Port1,6),Bits8_all0),PFS_V (Pin (Port1,7),Bits8_all0),
PFS_V (Pin (Port2,0),Bits8_all0),PFS_V (Pin (Port2,1),Bits8_all0),
PFS_V (Pin (Port2,2),Bits8_all0),PFS_V (Pin (Port2,3),Bits8_all0),
PFS_V (Pin (Port2,4),Bits8_all0),PFS_V (Pin (Port2,5),Bits8_all0),
PFS_V (Pin (Port2,6),Bits8_all0),PFS_V (Pin (Port2,7),Bits8_all0),
PFS_V (Pin (Port3,0),Bits8_all0),PFS_V (Pin (Port3,1),Bits8_all0),
PFS_V (Pin (Port3,2),Bits8_all0),PFS_V (Pin (Port3,3),Bits8_all0),
PFS_V (Pin (Port3,4),Bits8_all0),PFS_V (Pin (Port3,5),Bits8_all0),
PFS_V (Pin (Port3,6),Bits8_all0),PFS_V (Pin (Port3,7),Bits8_all0),
PFS_V (Pin (Port4,0),Bits8_all0),PFS_V (Pin (Port4,1),Bits8_all0),
PFS_V (Pin (Port4,2),Bits8_all0),PFS_V (Pin (Port4,3),Bits8_all0),
PFS_V (Pin (Port4,4),Bits8_all0),PFS_V (Pin (Port4,5),Bits8_all0),
PFS_V (Pin (Port4,6),Bits8_all0),PFS_V (Pin (Port4,7),Bits8_all0),
PFS_V (Pin (Port5,0),Bits8_all0),PFS_V (Pin (Port5,1),Bits8_all0),
PFS_V (Pin (Port5,2),Bits8_all0),PFS_V (Pin (Port5,3),Bits8_all0),
PFS_V (Pin (Port5,4),Bits8_all0),PFS_V (Pin (Port5,5),Bits8_all0),
PFS_V (Pin (Port5,6),Bits8_all0),PFS_V (Pin (Port5,7),Bits8_all0),
PFS_V (Pin (PortA,0),Bits8_all0),PFS_V (Pin (PortA,1),Bits8_all0),
PFS_V (Pin (PortA,2),Bits8_all0),PFS_V (Pin (PortA,3),Bits8_all0),
PFS_V (Pin (PortA,4),Bits8_all0),PFS_V (Pin (PortA,5),Bits8_all0),
PFS_V (Pin (PortA,6),Bits8_all0),PFS_V (Pin (PortA,7),Bits8_all0),
PFS_V (Pin (PortB,0),Bits8_all0),PFS_V (Pin (PortB,1),Bits8_all0),
PFS_V (Pin (PortB,2),Bits8_all0),PFS_V (Pin (PortB,3),Bits8_all0),
PFS_V (Pin (PortB,4),Bits8_all0),PFS_V (Pin (PortB,5),Bits8_all0),
PFS_V (Pin (PortB,6),Bits8_all0),PFS_V (Pin (PortB,7),Bits8_all0),
PFS_V (Pin (PortC,0),Bits8_all0),PFS_V (Pin (PortC,1),Bits8_all0),
PFS_V (Pin (PortC,2),Bits8_all0),PFS_V (Pin (PortC,3),Bits8_all0),
PFS_V (Pin (PortC,4),Bits8_all0),PFS_V (Pin (PortC,5),Bits8_all0),
PFS_V (Pin (PortC,6),Bits8_all0),PFS_V (Pin (PortC,7),Bits8_all0),
PFS_V (Pin (PortE,0),Bits8_all0),PFS_V (Pin (PortE,1),Bits8_all0),
PFS_V (Pin (PortE,2),Bits8_all0),PFS_V (Pin (PortE,3),Bits8_all0),
PFS_V (Pin (PortE,4),Bits8_all0),PFS_V (Pin (PortE,5),Bits8_all0),
PFS_V (Pin (PortE,6),Bits8_all0),PFS_V (Pin (PortE,7),Bits8_all0),
PFS_V (Pin (PortH,0),Bits8_all0),PFS_V (Pin (PortH,1),Bits8_all0),
PFS_V (Pin (PortH,2),Bits8_all0),PFS_V (Pin (PortH,3),Bits8_all0),
PFS_V (Pin (PortH,4),Bits8_all0),PFS_V (Pin (PortH,5),Bits8_all0),
PFS_V (Pin (PortH,6),Bits8_all0),PFS_V (Pin (PortH,7),Bits8_all0),
PFS_V (Pin (PortJ,0),Bits8_all0),PFS_V (Pin (PortJ,1),Bits8_all0),
PFS_V (Pin (PortJ,2),Bits8_all0),PFS_V (Pin (PortJ,3),Bits8_all0),
PFS_V (Pin (PortJ,4),Bits8_all0),PFS_V (Pin (PortJ,5),Bits8_all0),
PFS_V (Pin (PortJ,6),Bits8_all0),PFS_V (Pin (PortJ,7),Bits8_all0)
)
praxi rx110_consume_pfs_views (
PFS_V (Pin (Port0,0),Bits8_all0),PFS_V (Pin (Port0,1),Bits8_all0),
PFS_V (Pin (Port0,2),Bits8_all0),PFS_V (Pin (Port0,3),Bits8_all0),
PFS_V (Pin (Port0,4),Bits8_all0),PFS_V (Pin (Port0,5),Bits8_all0),
PFS_V (Pin (Port0,6),Bits8_all0),PFS_V (Pin (Port0,7),Bits8_all0),
PFS_V (Pin (Port1,0),Bits8_all0),PFS_V (Pin (Port1,1),Bits8_all0),
PFS_V (Pin (Port1,2),Bits8_all0),PFS_V (Pin (Port1,3),Bits8_all0),
PFS_V (Pin (Port1,4),Bits8_all0),PFS_V (Pin (Port1,5),Bits8_all0),
PFS_V (Pin (Port1,6),Bits8_all0),PFS_V (Pin (Port1,7),Bits8_all0),
PFS_V (Pin (Port2,0),Bits8_all0),PFS_V (Pin (Port2,1),Bits8_all0),
PFS_V (Pin (Port2,2),Bits8_all0),PFS_V (Pin (Port2,3),Bits8_all0),
PFS_V (Pin (Port2,4),Bits8_all0),PFS_V (Pin (Port2,5),Bits8_all0),
PFS_V (Pin (Port2,6),Bits8_all0),PFS_V (Pin (Port2,7),Bits8_all0),
PFS_V (Pin (Port3,0),Bits8_all0),PFS_V (Pin (Port3,1),Bits8_all0),
PFS_V (Pin (Port3,2),Bits8_all0),PFS_V (Pin (Port3,3),Bits8_all0),
PFS_V (Pin (Port3,4),Bits8_all0),PFS_V (Pin (Port3,5),Bits8_all0),
PFS_V (Pin (Port3,6),Bits8_all0),PFS_V (Pin (Port3,7),Bits8_all0),
PFS_V (Pin (Port4,0),Bits8_all0),PFS_V (Pin (Port4,1),Bits8_all0),
PFS_V (Pin (Port4,2),Bits8_all0),PFS_V (Pin (Port4,3),Bits8_all0),
PFS_V (Pin (Port4,4),Bits8_all0),PFS_V (Pin (Port4,5),Bits8_all0),
PFS_V (Pin (Port4,6),Bits8_all0),PFS_V (Pin (Port4,7),Bits8_all0),
PFS_V (Pin (Port5,0),Bits8_all0),PFS_V (Pin (Port5,1),Bits8_all0),
PFS_V (Pin (Port5,2),Bits8_all0),PFS_V (Pin (Port5,3),Bits8_all0),
PFS_V (Pin (Port5,4),Bits8_all0),PFS_V (Pin (Port5,5),Bits8_all0),
PFS_V (Pin (Port5,6),Bits8_all0),PFS_V (Pin (Port5,7),Bits8_all0),
PFS_V (Pin (PortA,0),Bits8_all0),PFS_V (Pin (PortA,1),Bits8_all0),
PFS_V (Pin (PortA,2),Bits8_all0),PFS_V (Pin (PortA,3),Bits8_all0),
PFS_V (Pin (PortA,4),Bits8_all0),PFS_V (Pin (PortA,5),Bits8_all0),
PFS_V (Pin (PortA,6),Bits8_all0),PFS_V (Pin (PortA,7),Bits8_all0),
PFS_V (Pin (PortB,0),Bits8_all0),PFS_V (Pin (PortB,1),Bits8_all0),
PFS_V (Pin (PortB,2),Bits8_all0),PFS_V (Pin (PortB,3),Bits8_all0),
PFS_V (Pin (PortB,4),Bits8_all0),PFS_V (Pin (PortB,5),Bits8_all0),
PFS_V (Pin (PortB,6),Bits8_all0),PFS_V (Pin (PortB,7),Bits8_all0),
PFS_V (Pin (PortC,0),Bits8_all0),PFS_V (Pin (PortC,1),Bits8_all0),
PFS_V (Pin (PortC,2),Bits8_all0),PFS_V (Pin (PortC,3),Bits8_all0),
PFS_V (Pin (PortC,4),Bits8_all0),PFS_V (Pin (PortC,5),Bits8_all0),
PFS_V (Pin (PortC,6),Bits8_all0),PFS_V (Pin (PortC,7),Bits8_all0),
PFS_V (Pin (PortE,0),Bits8_all0),PFS_V (Pin (PortE,1),Bits8_all0),
PFS_V (Pin (PortE,2),Bits8_all0),PFS_V (Pin (PortE,3),Bits8_all0),
PFS_V (Pin (PortE,4),Bits8_all0),PFS_V (Pin (PortE,5),Bits8_all0),
PFS_V (Pin (PortE,6),Bits8_all0),PFS_V (Pin (PortE,7),Bits8_all0),
PFS_V (Pin (PortH,0),Bits8_all0),PFS_V (Pin (PortH,1),Bits8_all0),
PFS_V (Pin (PortH,2),Bits8_all0),PFS_V (Pin (PortH,3),Bits8_all0),
PFS_V (Pin (PortH,4),Bits8_all0),PFS_V (Pin (PortH,5),Bits8_all0),
PFS_V (Pin (PortH,6),Bits8_all0),PFS_V (Pin (PortH,7),Bits8_all0),
PFS_V (Pin (PortJ,0),Bits8_all0),PFS_V (Pin (PortJ,1),Bits8_all0),
PFS_V (Pin (PortJ,2),Bits8_all0),PFS_V (Pin (PortJ,3),Bits8_all0),
PFS_V (Pin (PortJ,4),Bits8_all0),PFS_V (Pin (PortJ,5),Bits8_all0),
PFS_V (Pin (PortJ,6),Bits8_all0),PFS_V (Pin (PortJ,7),Bits8_all0)
): void
praxi rx110_initial_pdr_views ():
(PDR_V (Port0,Bits8_all0),PDR_V (Port1,Bits8_all0),
PDR_V (Port2,Bits8_all0),PDR_V (Port3,Bits8_all0),
PDR_V (Port4,Bits8_all0),PDR_V (Port5,Bits8_all0),
PDR_V (PortA,Bits8_all0),PDR_V (PortB,Bits8_all0),
PDR_V (PortC,Bits8_all0),PDR_V (PortE,Bits8_all0),
PDR_V (PortH,Bits8_all0),PDR_V (PortJ,Bits8_all0),
PDR_PERMISSION (Port0,BitPerms8_all), PDR_PERMISSION (Port1,BitPerms8_all),
PDR_PERMISSION (Port2,BitPerms8_all), PDR_PERMISSION (Port3,BitPerms8_all),
PDR_PERMISSION (Port4,BitPerms8_all), PDR_PERMISSION (Port5,BitPerms8_all),
PDR_PERMISSION (PortA,BitPerms8_all), PDR_PERMISSION (PortB,BitPerms8_all),
PDR_PERMISSION (PortC,BitPerms8_all), PDR_PERMISSION (PortE,BitPerms8_all),
PDR_PERMISSION (PortH,BitPerms8_all), PDR_PERMISSION (PortJ,BitPerms8_all)
)
praxi rx110_consume_pdr_views (
PDR_V (Port0,Bits8_all0),PDR_V (Port1,Bits8_all0),
PDR_V (Port2,Bits8_all0),PDR_V (Port3,Bits8_all0),
PDR_V (Port4,Bits8_all0),PDR_V (Port5,Bits8_all0),
PDR_V (PortA,Bits8_all0),PDR_V (PortB,Bits8_all0),
PDR_V (PortC,Bits8_all0),PDR_V (PortE,Bits8_all0),
PDR_V (PortH,Bits8_all0),PDR_V (PortJ,Bits8_all0),
PDR_PERMISSION (Port0,BitPerms8_all), PDR_PERMISSION (Port1,BitPerms8_all),
PDR_PERMISSION (Port2,BitPerms8_all), PDR_PERMISSION (Port3,BitPerms8_all),
PDR_PERMISSION (Port4,BitPerms8_all), PDR_PERMISSION (Port5,BitPerms8_all),
PDR_PERMISSION (PortA,BitPerms8_all), PDR_PERMISSION (PortB,BitPerms8_all),
PDR_PERMISSION (PortC,BitPerms8_all), PDR_PERMISSION (PortE,BitPerms8_all),
PDR_PERMISSION (PortH,BitPerms8_all), PDR_PERMISSION (PortJ,BitPerms8_all)
): void
praxi rx110_initial_podr_views ():
(PODR_V (Port0,Bits8_all0),PODR_V (Port1,Bits8_all0),
PODR_V (Port2,Bits8_all0),PODR_V (Port3,Bits8_all0),
PODR_V (Port4,Bits8_all0),PODR_V (Port5,Bits8_all0),
PODR_V (PortA,Bits8_all0),PODR_V (PortB,Bits8_all0),
PODR_V (PortC,Bits8_all0),PODR_V (PortE,Bits8_all0),
PODR_V (PortH,Bits8_all0),PODR_V (PortJ,Bits8_all0),
PODR_PERMISSION (Port0,BitPerms8_all), PODR_PERMISSION (Port1,BitPerms8_all),
PODR_PERMISSION (Port2,BitPerms8_all), PODR_PERMISSION (Port3,BitPerms8_all),
PODR_PERMISSION (Port4,BitPerms8_all), PODR_PERMISSION (Port5,BitPerms8_all),
PODR_PERMISSION (PortA,BitPerms8_all), PODR_PERMISSION (PortB,BitPerms8_all),
PODR_PERMISSION (PortC,BitPerms8_all), PODR_PERMISSION (PortE,BitPerms8_all),
PODR_PERMISSION (PortH,BitPerms8_all), PODR_PERMISSION (PortJ,BitPerms8_all)
)
praxi rx110_consume_podr_views (
PODR_V (Port0,Bits8_all0),PODR_V (Port1,Bits8_all0),
PODR_V (Port2,Bits8_all0),PODR_V (Port3,Bits8_all0),
PODR_V (Port4,Bits8_all0),PODR_V (Port5,Bits8_all0),
PODR_V (PortA,Bits8_all0),PODR_V (PortB,Bits8_all0),
PODR_V (PortC,Bits8_all0),PODR_V (PortE,Bits8_all0),
PODR_V (PortH,Bits8_all0),PODR_V (PortJ,Bits8_all0),
PODR_PERMISSION (Port0,BitPerms8_all), PODR_PERMISSION (Port1,BitPerms8_all),
PODR_PERMISSION (Port2,BitPerms8_all), PODR_PERMISSION (Port3,BitPerms8_all),
PODR_PERMISSION (Port4,BitPerms8_all), PODR_PERMISSION (Port5,BitPerms8_all),
PODR_PERMISSION (PortA,BitPerms8_all), PODR_PERMISSION (PortB,BitPerms8_all),
PODR_PERMISSION (PortC,BitPerms8_all), PODR_PERMISSION (PortE,BitPerms8_all),
PODR_PERMISSION (PortH,BitPerms8_all), PODR_PERMISSION (PortJ,BitPerms8_all)
): void・・・長い（長い）。
残りのレジスタの分です。長いですね（他人事）。
あと、さっき書き忘れましたが、この定義はRX110の64ピンのパッケージに合わせてあります。もし万が一、他のMCUで使いたい場合は修正または定義の追加を行ってください。
まとめ
えーと、今回で終わりになる予定だったんですが、思いのほか長くなってしまったので次回に続きます。
今回までに作ったドライバーで実際に端子の操作をする処理を作ってみよう、というのが次回の内容です。
では次回
ATS で組み込みドライバを実装してみる
暇なのか
暇じゃないのか
暇なのか
というわけで、ATS言語の勉強も兼ねて、組み込みのドライバを書いてみます。
目標は、できるだけ安全なドライバを作ること。ATSの表現能力や、課題があるとしたら何なのかという事を探ってみることも目的です。
実用性とか、実際に動作するかどうかは、ぶっちゃけ余り気にしません。
まあ、動くようには作るつもりですが、実機も持ってないので……。
ATSとはなんじゃ？ という人は
ATSは、証明プログラミングに対応したプログラミング言語です。
同様の言語は他にもありますが、その中でも「実際に動作するプログラムを記述することを前提にしている」「線形型の仕組みを採用することで、安全なリソース管理手法を提供している」のがATSの特徴です。……の、はずです。
詳しいことは、↓を参照してください。
そもそも、証明プログラミングがわかっていないという人は、↓を見ると良いでしょう。
わからなくても泣かない。
目標
今回はRX-110のドライバ実装を目指してみます。
なんでRXなのかと言うと → 仕事で使ったので扱いやすいから。
なんで110なのかと言うと → 一番単純で実装しやすそうだから。
とりあえずは端子ドライバを実装して、Lチカ/デジタル入力読み込みができるところを目指して行きます。
ビット演算ライブラリ
さて、CPU（正確にはMCUだけど）のレジスタを証明された形で扱うためには、ビット演算を行うための、これまた証明された関数が必要です。
レジスタを扱う関数宣言を一通り定義してみた感じでは、以下の定義が必要なようです。
- 受け取った数値の、指定されたビットをセットする関数
- 受け取った数値の、指定されたビットをクリアする関数
- ビットの書き込み許可をエンコードするための命題
前の2つは普通に実装するだけなら3秒（誇張）でできる関数ですが、証明を入れながら作るとなるとなかなか大変です。
最後の命題は、ほぼ定義だけなのでそんなに大変ではない（なかった）です。
また、ここに書いてあるコードは、github（https://github.com/fujiik102/ats-rx-drivers）に公開してあります。今回の内容に関係するのは、Bit.satsです。
ビット、ビット列
まずは、ビットの定義から。
datasort bit = | O | I datasort bits = BitsNil of () | BitsCons of (bits,bit)
bit種は0か1です。識別子の先頭に数字は使えないので、大文字のOとIで代用しています。
bits種は複数ビットをまとめた定義です。この後、非常に良く使う定義です。
BitsConsの引数がビット列→ビットの順番なのは、複数ビットの定義を行った時に下位ビットを右側にするためです。
要するに、この定義で例えば「0011」を定義すると
BitsCons (BitsCons (BitsCons (BitsCons (BitsNil,O),O),I),I)
のようになります。これが逆に定義されていると、
BitsCons (I,BitsCons (I,BitsCons (O,BitsCons (O,BitsNil))))
となってしまい、非常に分かりづらい事になります。
リトルエンディアンは人類の直感に反する悪夢のような表記（誇張表現）なので、ビット順が逆になっている事に気付かずに定義してしまい、後で慌てて直すハメに陥ったりするのです（1敗）
ビット長
dataprop BITSLEN (bits,int) =
| BITSLENNIL (BitsNil,0) of ()
| {n:int}{b:bit}{bs:bits}
BITSLENCONS (BitsCons (bs,b),n+1) of BITSLEN (bs,n)
praxi bitslen_nat {n:int}{bs:bits} (BITSLEN (bs,n)):[0 <= n] voidビット長に関する証明型の定義です。後述するBITSEQINTが長さに関する定義も含んでいるので、単体では余り使いません。
定義の内容は自明だと思うので、解説は省略します。わからない場合は、↑の方で挙げたページをなんか適当に読んで下さい（適当）
bitslen_natは、「0<=ビット長」という公理を導入しています。自明なように見える事実ですが、やってみた範囲では証明できなかったので、公理にしています。
2017-09-21追記 証明できました。「ビット長＜０」のケースが証明できなかったのですが、帰納法を使って矛盾を作れば良いだけだったようです。
ビット⇔整数の対応
dataprop BITEQINT (bit, int) =
| B0EQ0 (O, 0) of ()
| B1EQ1 (I, 1) of ()
typedef bit_uint_t (b:bit) = [v:int] (BITEQINT (b,v) | uint v)
dataprop BITSEQINT (int, bits, int) =
| BEQNIL (0,BitsNil,0) of ()
| {n:int}{b:bit}{bs:bits}{v,bitv:int | v <= INTMAX_HALF}
BEQCONS (n+1,BitsCons (bs,b),v+v+bitv)
of (BITSEQINT (n,bs,v),BITEQINT (b,bitv))
typedef bits_uint_t (n:int,bs:bits) =
[v:int] (BITSEQINT (n,bs,v) | uint v)（これ、字下げとかはどうするのが正解なんですかね……？）
BITSEQINTは、bits種とint種をつなぐ、キーになる命題です。
1番目の引数でビット列の長さを受け取っています。これは、単純にintだけを指定しても対応するbitsが一意にならない（例えば、1という整数に対応するビット列は「01」、「001」など無数にある）ので、補助のためにつけています。
また、命題をいちいち書くのは煩わしいので、短縮して書くためにbit_uint_tとbits_uint_tを定義しています。bits_uint_tは、関数の定義などでは特に多用します。
ATSのビット演算ではuint型を使うので、int型ではなくuint型に結びつけてあります。
１バイトの簡易表現
stadef Bits8 (b7,b6,b5,b4,b3,b2,b1,b0:bit): bits = BitsCons (BitsCons (BitsCons (BitsCons ( BitsCons (BitsCons (BitsCons (BitsCons ( BitsNil,b7),b6),b5),b4),b3),b2),b1),b0)
bitsの値を表現する際、BitsConsやBitNilを使って書くのは冗長（というか、文字数が多過ぎ）なので、1バイト分のBitsを短く書くための定義です。
RX110のレジスタは基本的に8ビットなので、レジスタの定義では頻繁に使用します。
ビットの変更
dataprop CHANGE_BIT_BITS (int,bits,int,bit,bits) =
| {n:int}{b,c:bit}{bs:bits} CHANGE_BIT_BITS_bas
(n+1,BitsCons (bs,b),0,c,BitsCons (bs,c)) of (BITSLEN (bs,n))
| {n,bn:int}{b,c:bit}{bs,cs:bits}
CHANGE_BIT_BITS_ind(n+1,BitsCons (bs,c),bn+1,b,BitsCons (cs,c))
of CHANGE_BIT_BITS (n,bs,bn,b,cs)CHANGE_BIT_BITSという命題を定義します。(int,bits,int,bit,bits)と5つも引数がありますが、順番に「ビット列の長さ」「変更前のビット列」「変更するビットの番号（0オリジン）」「置き換えるビット」「変更後のビット列」になります。
大雑把に言うと、CHANGE_BIT_BITSは「"変更前のビット列"のどれか1つのビットを置き換えたものが"変更後のビット列"である」という意味の命題です。
"ビット列の長さ"の引数は要らないような……？
まあええわ（適当）
ビットの調査
dataprop TEST_BIT_BITS (bits,int,bit) =
| {bn:int}{b:bit}{bs:bits} TEST_BIT_BITS_bas (BitsCons (bs,b),0,b)
of (BITSLEN (bs,bn))
| {b,c:bit}{bs:bits}{bn:int}
TEST_BIT_BITS_ind (BitsCons (bs,c),bn+1,b) of TEST_BIT_BITS (bs,bn,b)ビット列の何番目が立ってるとか、寝てるとかの状態を表現します。
例えばあるビット列の3番目のビットが立っていれば、TEST_BIT_BITS (bs,3,I)という証明を構成できる（はず）わけです。
逆に、その条件が満たされていてほしいという場合は、関数の引数にTEST_BIT_BITS (bs,3,I)の型を入れておけばよいわけです。
ビット操作関数
で、目的の関数の定義です。
fn {b:bit}{bs:bits}
changeBitBits {n,bn:nat | bn < n; n < INTBITS} (bits_uint_t (n,bs),uint bn,bit_uint_t b)
: [bs':bits] (CHANGE_BIT_BITS (n,bs,bn,b,bs') | bits_uint_t (n,bs'))
fn {bs:bits}
setBitBits {n,bn:nat | bn < n; n < INTBITS} (bits_uint_t (n,bs),uint bn)
: [cs:bits] (CHANGE_BIT_BITS (n,bs,bn,I,cs) | bits_uint_t (n,cs))
fn {bs:bits}
clearBitBits {n,bn:nat | bn < n; n < INTBITS} (bits_uint_t (n,bs),uint bn)
: [bs':bits] (CHANGE_BIT_BITS (n,bs,bn,O,bs') | bits_uint_t (n,bs'))
fn {bs:bits}
testBitBits {n,bn:nat | bn < n}{n < INTBITS} (bits_uint_t (n,bs),uint bn)
: [b:bit] (TEST_BIT_BITS (bs,bn,b) | bool (b==I))勢い余ってビット調査用の関数（testBitBits）も作ってます。
最初の方で書いた必要な関数との対応は、
- 受け取った数値の、指定されたビットをセットする関数
→ setBitBits
- 受け取った数値の、指定されたビットをクリアする関数
→ clearBitBits
です。
より汎用的な関数として、changeBitBitsを定義しています。CHANGE_BIT_BITS命題との対応としては、こちらの方が自然かも知れません。
intの最大値
あと、今までもチラチラ見えてた（BITSEQINTの定義とか）と思いますが、int種の最大値についての定義をしてあります。
#define INTBITS 32 #define INTMAX 2147483647 #define INTMAX_HALF 1073741823 #define UINTMAX_HALF 2147483647
ATSの処理系はint種を扱う時に上限について考慮していないらしく、32ビットで表現できる範囲を越えると簡単に（少なくとも僕が調べたバージョンでは）オーバーフローを起こしてしまいます。
32ビットというのは普通の数としては十分な範囲がありますが、ビット操作を行っていると簡単に越えてしまえる数値です。
悪用を防ぐ手段はないので仕方がないのですが、ケアレスミスで越えてしまった場合に困るかも知れないので、念の為に上記の上限値を使って値の範囲を制限しています。
書き込み許可
次で最後です。
datasort permission = Permit | Prohibit datasort bit_permission = BitPermission of (permission(*of 0*),permission(*of 1*)) datasort bit_permissions = | BitPermsNil of () | BitPermsCons of (bit_permissions,bit_permission)
レジスタの仕様などでは、「このレジスタを書き込む時は必ず0を書き込むこと」など、制限が付いている事がよくあります。
bit_permissionとbit_permissionsは、そういった制限を表現するためのデータ種です。
ビット毎に「0の書き込みの可否」と「1の書き込みの可否」を指定します。ビット毎に4パターンなので、情報量としては4^n(=2^2n)になるわけです。いかにもマシンパワーが必要になりそうな数字ですね！（不安）
stadef BitPermissions8 (b7_0,b7_1,b6_0,b6_1,b5_0,b5_1,b4_0,b4_1,
b3_0,b3_1,b2_0,b2_1,b1_0,b1_1,b0_0,b0_1:permission): bit_permissions =
BitPermsCons (BitPermsCons (BitPermsCons (BitPermsCons (
BitPermsCons (BitPermsCons (BitPermsCons (BitPermsCons (BitPermsNil,
BitPermission (b7_0,b7_1)),BitPermission (b6_0,b6_1)),
BitPermission (b5_0,b5_1)),BitPermission (b4_0,b4_1)),
BitPermission (b3_0,b3_1)),BitPermission (b2_0,b2_1)),
BitPermission (b1_0,b1_1)),BitPermission (b0_0,b0_1))で、１バイト分のbit_permissionsを（なるべく）簡単に宣言するための定義です。
bitsに対してのBits8 と同じようなものです。
書き込み許可→ビットの関係
書き込み許可を表現することはできるようになりましたが、それだけではなんの意味もありません。「その数値は書き込みを許可されているか」判定する仕組みが必要です。
「ビット⇔数値」の対応関係（BITSEQINT）は定義してあるので、あとは「書き込み許可⇔ビット」の関係を定義すれば、芋づる式に「書き込み許可⇔数値」の対応関係を表すことができるようになります。
dataprop BIT_PERMIT_CERTIFICATE (bit_permission,bit) =
| {p1:permission} BITPERMCERT_0 (BitPermission (Permit,p1),O) of ()
| {p0:permission} BITPERMCERT_1 (BitPermission (p0,Permit),I) of ()
dataprop BITS_PERMIT_CERTIFICATE (int,bit_permissions,bits) =
| BITPERMCERTS_NIL (0, BitPermsNil, BitsNil) of ()
| {n:int}{p:bit_permission}{ps:bit_permissions}{b:bit}{bs:bits}
BITPERMCERTS_CONS (n+1,BitPermsCons (ps,p),BitsCons (bs,b))
of (BITS_PERMIT_CERTIFICATE (n,ps,bs),BIT_PERMIT_CERTIFICATE (p,b))BIT_PERMIT_CERTIFICATEとBITS_PERMIT_CERTIFICATEです。「ビットの許可の証明」みたいなニュアンスでしょうか……？（英語力✕）
対象のビットに応じて、0または1の対応する許可を参照します。例えばBIT_PERMIT_CERTIFICATE (p,b)の値があるという事は、「許可"p"は、ビット"b"を許可している」という意味になります。
BITS_PERMIT_CERTIFICATEは、それを1ビットずつ見ているだけです。
まとめ
疲れた（疲れた）
他にも細々した定義がありますが、端子ドライバの定義では使わない（はずです）ので、ここまでにします。
あとはソースを見て各自読み解いてください（丸投げ）
次回は端子ドライバ本体(Pin.satsとPin.dats)の解説を書く予定です。多分ですが、ここまでが大変だっただけで、すぐに書けるだろうと思います。
ではまた次回。
最初の記事
なんか書きたいことがあった時のためにブログを始めました。
プログラミングの話題やアニメの話題を書いてゆく予定です。
やる気はないのでがんばりません。
よろしくお願いします。
