rzk-0.11.3: An experimental proof assistant for synthetic ∞-categories
Safe HaskellSafe-Inferred
LanguageHaskell2010

Rzk.Render.Geometry

Description

The geometry behind the SVG rendering of cubes, and nothing else.

Rzk renders a (sub)shape of a cube as an SVG diagram: the vertices, edges and faces of the unit cube are projected to the plane through a camera, and each of them is labelled with the term that inhabits it. This module holds the part of that story which knows nothing about terms: the projection matrices, the camera, and renderCube, which draws a cube given only a function saying what (if anything) to draw on each of its parts.

Nothing here mentions the type checker, so it is shared by both term representations during the free-foil migration.

Synopsis

Documentation

type PointId = String Source #

The name of a vertex of the unit cube, as a string of coordinates (e.g. "010").

type ShapeId = [PointId] Source #

The name of a subshape of the unit cube: its vertices, in order, joined by dashes (e.g. "000-011" for an edge, "000" for a vertex).

type Point2D a = (a, a) Source #

type Point3D a = (a, a, a) Source #

type Edge3D a = (Point3D a, Point3D a) Source #

type Face3D a = (Point3D a, Point3D a, Point3D a) Source #

data CubeCoords2D a b Source #

Constructors

CubeCoords2D 

Fields

data Matrix3D a Source #

Constructors

Matrix3D a a a a a a a a a 

data Matrix4D a Source #

Constructors

Matrix4D a a a a a a a a a a a a a a a a 

data Vector3D a Source #

Constructors

Vector3D a a a 

data Vector4D a Source #

Constructors

Vector4D a a a a 

data Camera a Source #

Constructors

Camera 

point3Dto2D :: Floating a => Camera a -> a -> Point3D a -> (Point2D a, a) Source #

data RenderObjectData Source #

What to draw on one part (vertex, edge or face) of a cube.

hideTermData :: Bool -> String -> RenderObjectData -> RenderObjectData Source #

Apply the term-hiding policy to a cell's render data: drop the <title> (the full term) from every cell, and blank the visible label of a proof-coloured (interior) cell. Boundary cells (coloured otherwise) keep their given labels. A no-op when not hiding.