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_p

bisectional同士の足し算の定義です。

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> void

PMRに値を書き込む関数です。
書き込み許可（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> void

1ビットごとの書き込みを行う関数です。
内部的には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で使いたい場合は修正または定義の追加を行ってください。

まとめ

えーと、今回で終わりになる予定だったんですが、思いのほか長くなってしまったので次回に続きます。
今回までに作ったドライバーで実際に端子の操作をする処理を作ってみよう、というのが次回の内容です。

では次回