图像的光栅化
图像的光栅化
提问于 2022-10-22 07:29:46
我有一个函数ℚ -> ℚ -> Bool，取一个笛卡儿坐标，true代表黑色，false代表白色。有没有任何现有的库，我可以使用它“栅格”到一个位图图像？
回答 2
Stack Overflow用户
发布于 2022-10-23 09:56:43
PBM文件格式是一种非常简单的基于文本的图像文件格式。有关说明，请参见https://en.wikipedia.org/wiki/Netpbm。编写代码来生成PBM文件很容易。
对于函数λ x y → x ≤ᵇ y，下面的代码输出以下PBM文件内容：
P1
20 10
1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0
1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0
1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0
1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0
1 1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 这两行的含义如下：
P1是一个神奇的数字，用来标识文件format.20 10是图像的宽度和高度。- 剩余的每一行代表图像的一行。
1表示黑色像素，0表示白色像素。
将上述内容放入.pbm文件(例如，test.pbm)中，您就可以在支持PBM文件的图像处理工具中打开这些内容。
makePBM函数获取要生成的图像的宽度和高度，ℚ中的x和y起点，在ℚ中对x和y方向上的每个像素执行的步骤，以及要计算的ℚ → ℚ → Bool函数。
只需要--guardedness，因为我将IO用于演示目的。
{-# OPTIONS --guardedness #-}
module Raster where
open import Data.Bool using (Bool ; if_then_else_)
open import Data.Nat using (ℕ ; zero ; suc)
open import Data.Nat.Show using (show)
open import Data.Rational using (ℚ ; 0ℚ ; 1ℚ ; _+_ ; _≤ᵇ_)
open import Data.String using (String ; _++_)
open import IO using (Main ; run ; putStrLn)
-- width height offset-x offset-y step-x step-y function
makePBM : (w h : ℕ) → (ox oy sx sy : ℚ) → (ℚ → ℚ → Bool) → String
makePBM w h ox oy sx sy f = header ++ bitmap h oy
where
header : String
header = "P1\n" ++ show w ++ " " ++ show h ++ "\n"
row : (n : ℕ) → (x y : ℚ) → String
row zero x y = "\n"
row (suc n) x y = pixel ++ " " ++ row n (x + sx) y
where pixel = if f x y then "1" else "0"
bitmap : (n : ℕ) → (y : ℚ) → String
bitmap zero y = ""
bitmap (suc n) y = row w ox y ++ bitmap n (y + sy)
testPBM : String
testPBM = makePBM 20 10 0ℚ 0ℚ 1ℚ 1ℚ (λ x y → x ≤ᵇ y)
main : Main
main = run (putStrLn testPBM)Stack Overflow用户
发布于 2022-10-23 04:29:14
如果有的话我会很惊讶的。我不知道在Agda中有任何关于图像处理的工作。
尽管如此，这应该是相对容易做到的。
- 从包含
i第四行和j第四列的(i,j)的Data.Vec.Functional中创建Vector (Vector ℕ m) n类型的m x n矩阵。
- 映射每个(i，j)到图像中所需的坐标范围。
- 映射整个矩阵上的函数
f : ℚ -> ℚ -> Bool。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/74161810
复制相关文章
相似问题
腾讯云开发者
