Alloyのリファクタリングで悩む日記
ある関係cell : Col -> Row -> Colorがあった時に
all c: SomeColSet : some_pred[cell [c, r]] all r: SomeRowSet : some_pred[cell [c, r]]
これをまとめる方法が難しい。cellのタプルの1番目がcであるような集合はc.cellだからこうはできる。
all c: SomeColSet : some_pred[cell [c, r]] all r: SomeRowSet : some_pred[c.cell [r]]
c: SomeColSetの方も同じようにfoo [c]の形にしたいんだが3要素のタプルの真ん中で絞り込むとかどうやるんだ…
内包表記はUnary Setにしか使えないから
{x: cell | univ.x.univ = r}
はダメ。自分自身を結合したらいいんじゃないかと
r.((univ.(cell.univ))->(cell.univ.univ)->(univ.(univ.cell)))
を試してみたが(->)は直積なので「自分自身を結合」じゃない。うむむ…。
こうやると、中身は述語なのに宣言が関数だから怒られてしまう。述語を満たすようなrを返す、というのはどう表現するのか。
fun filter_middle(rs: Int->Int->Int, key: Int): Int->Int{ some r: Int->Int{ all x: Int { x.rs[key] = r[x] } } }
追記
値域限定でできるんじゃないかと思ったが値域限定もUnaryしか取れない。
cell: Col->Color->Row という斜め上な解決策を思いついたが…うむむ…