import Batteries.Data.Rat.Basic

/-!
# Data structures for triangle meshes

This file defines the data structures at the algorithm interface.  The verified
implementation is free to convert to more efficient representations and to use
accelerating structures internally.

We work in rational `3`-space `ℚ³` to allow for exact computation.  This loses
nothing when characterizing the intersection, since intersections of rational
triangles are rational. -/

namespace CSG

/-- A point of rational `3`-space `ℚ³`.

In the formal specification, Mathlib automatically endows this with a
vector-space structure. -/
abbrev Point : Type := Fin 3 → Rat

/-- A triangle is a triple of vertices, oriented by its vertex order (winding).
  -/
structure Triangle where
  v₀ : Point
  v₁ : Point
  v₂ : Point

/-- A triangle mesh: an array of triangles.

See `WellFormedMesh` and `solid` in `CSG/Def.lean` for conditions and geometric
semantics. -/
abbrev Mesh : Type := Array Triangle

end CSG