Ray tracing in Agda

Colour.agda

open import Agda.Builtin.Float

record Colour : Set where
  constructor colour
  field
    r g b : Float
    

raytracer.agda

open import Agda.Builtin.IO
open import Agda.Builtin.Unit
open import Agda.Builtin.String
open import Agda.Builtin.Float
open import Agda.Builtin.Nat renaming (Nat to ℕ)

open import Colour
open import Vec

postulate
  putStr   : String → IO ⊤

_>>_ = primStringAppend
infixr 1 _>>_

{-# FOREIGN GHC import qualified Data.Text.IO as Text #-}
{-# COMPILE GHC putStr = Text.putStr #-}

IMAGE_WIDTH = 640
IMAGE_HEIGHT = 480

pixels : Vec Colour (IMAGE_WIDTH * IMAGE_HEIGHT)
pixels = fill (colour 0.0 0.5 0.8) (IMAGE_WIDTH * IMAGE_HEIGHT)

main : IO ⊤
main = putStr (newlineDelim (map colourToString pixels))
  where
    colourToString : Colour → String
    colourToString (colour r g b) = primShowFloat r
                                    >> " " >> primShowFloat g
                                    >> " " >> primShowFloat b
    joinNewline  : String → String → String
    joinNewline s t = s >> "\n" >> t
    newlineDelim : ∀{n} → Vec String n → String
    newlineDelim {n} xs = foldr joinNewline xs ""

Vec.agda

open import Agda.Builtin.Nat renaming (Nat to ℕ)

infixr 5 _∷_

data Vec (A : Set) : ℕ → Set where
  []  : Vec A zero
  _∷_ : ∀{n} → A → Vec A n → Vec A (suc n)

fill : {A : Set} → A → (n : ℕ) → Vec A n
fill x zero = []
fill x (suc n) = x ∷ fill x n

map : ∀{n} {A B : Set} → (A → B) → Vec A n → Vec B n
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs


foldr : ∀{n} {A B : Set} → (A → B → B) → Vec A n → B → B
foldr _∘_ [] y = y
foldr _∘_ (x ∷ xs) y = x ∘ (foldr _∘_ xs y)

foldl : ∀{n} {A B : Set} → (B → A → B) → Vec A n → B → B
foldl _∘_ [] y = y
foldl _∘_ (x ∷ xs) y = foldl _∘_ xs y ∘ x

Vector.agda

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Float
  renaming
    ( primFloatPlus  to _+_
    ; primFloatTimes to _*_
    ; primFloatDiv   to _/_
    ; primFloatSqrt  to sqrt
    ; primFloatEquality to _==_ )

record Vector : Set where
  constructor vector
  field
    x y z : Float

_•_ : Vector → Vector → Float
(vector x y z) • (vector x′ y′ z′) = (x * x′) + ((y * y′) + (z * z′))

‖_‖² : Vector → Float
‖ v ‖² = v • v

‖_‖ : Vector → Float
‖ v ‖ = sqrt ‖ v ‖²

record UnitVector : Set where
  constructor unitvector
  field
    v    : Vector
    unit : ‖ v ‖ == 1.0 ≡ true

normalise : Vector → UnitVector
normalise v@(vector x y z) = unitvector normalised isNormalised
  where
    normalised : Vector
    Vector.x normalised = x / ‖ v ‖
    Vector.y normalised = y / ‖ v ‖
    Vector.z normalised = z / ‖ v ‖
    postulate isNormalised : ‖ normalised ‖ == 1.0 ≡ true