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 という斜め上な解決策を思いついたが…うむむ…