https://qiita.com/e869120/items/92f19314ac5ea9a1e82a

gistfile1.txt

命令列Cと状態{m, h, w, d, p}の遷移から成るPainter Programmingの小ステップ意味論を考える｡
要素が{0, 1}から成るHxW行列が得られる｡

`M`atrix, `H`eight, `W`idth, `D`irection[←↓↑→], `P`rogram stack

init = { m = H x Wの000...0, h = 1, w = 1, d = →, P = []}

## 補助関数
edge_HW → H _ = true
edge_HW ← 1 _ = true
edge_HW ↓ _ W = true
edge_HW ↑ _ 1 = true
edge_HW _ _ _ = false

rotate d = d を90度回転
flip_hw m = mのh行w列目をflip
fetch_paren C = Cの先頭から最初のparenまでを取ってくる
jump_paren C = Cの先頭から最初のparenまでを取り除く

## 意味論
[F::C] { m = _, h = _, w = W, d = d, p = _ } as st when edge_HW d h w = C st
[F::C] { m = _, h = h, w = _, d = →, p = _ } = C { m = _, h = h + 1, w = _, d = →, p = _ }
[F::C] { m = _, h = h, w = _, d = ←, p = _ } = C { m = _, h = h - 1, w = _, d = ←, p = _ }
[F::C] { m = _, h = _, w = w, d = ↑, p = _ } = C { m = _, h = _, w = w + 1, d = ↑, p = _ }
[F::C] { m = _, h = _, w = w, d = ↓, p = _ } = C { m = _, h = _, w = w - 1, d = ↓, p = _ }

[L::C] { m = _, h = _, w = _, d = d, p = _ } = C { m = _, h = _, w = _, d = rotate d, p = _ }
[R::C] st = [L::L::L::C] st
[!::C] { m = m, h = h, w = w, d = _, p = _ } = C { m = flip_hw m, h = h, w = w, d = _, p = _ }
[(::C] { m = _, h = h, w = w, d = _, p = p } when m_{hw} = 0  = C { m = _, h = _, w = _, d = _, p = fetch_) C :: p }
[(::C] { m = _, h = h, w = w, d = _, p = p } as st = jump_( C st
[)::C] { m = _, h = _, w = _, d = _, p = P ++ p } = ( :: P ++ C { m = _, h = _, w = _, d = _, p = p }
[ [::C ] { m = _, h = h, w = w, d = d, p = p } when edge_HW d h w = C { m = _, h = h, w = w, d = d, p = p }
[ [::C ] { m = _, h = _, w = _, d = _, p = p } = C { m = _, h = _, w = _, d = _, p = fetch_] C :: p }
[ ]::C ] { m = _, h = _, w = _, d = _, p = P ++ p } = [ :: P ++ C { m = _, h = _, w = _, d = _, p = p }
[ empty ] st = [empty] st