import Mathlib
import CSG.DataStructures

/-!
# Semantics of triangle meshes

This file formalizes the geometric interpretation of triangle meshes
representing solids, needed for the formal specification.

We define well-formedness conditions on meshes and use the signed crossing count
of rays to define the solids they bound. -/

namespace CSG

open scoped Classical BigOperators

/-- The set of points of the filled (closed) triangle.

Defined in terms of Mathlib's `convexHull`. -/
def triangleSet (t : Triangle) : Set Point :=
  convexHull ℚ {t.v₀, t.v₁, t.v₂}

/-- The set of points on the edges of a triangle.

Defined in terms of Mathlib's `segment`. -/
def edgeSet (t : Triangle) : Set Point :=
  segment ℚ t.v₀ t.v₁ ∪ segment ℚ t.v₁ t.v₂ ∪ segment ℚ t.v₂ t.v₀

/-- The oriented normal of a face.

The cross product `(v₁ - v₀) × (v₂ - v₀)` of two edge vectors. Note that the
indices of type `Fin 3` are automatically taken modulo `3`.

It is `0` exactly when the three vertices are collinear. -/
def faceNormal (t : Triangle) : Point := fun i =>
    (t.v₁ (i + 1) - t.v₀ (i + 1)) * (t.v₂ (i + 2) - t.v₀ (i + 2))
  - (t.v₁ (i + 2) - t.v₀ (i + 2)) * (t.v₂ (i + 1) - t.v₀ (i + 1))

/-- The dot product of `ℚ³`. -/
def dot (a b : Point) : ℚ := ∑ i, a i * b i

/-- The open ray from `Q` in direction `d` meets the (closed) face `t`. -/
def RayHits (Q d : Point) (t : Triangle) : Prop :=
  ∃ s : ℚ, 0 < s ∧ Q + s • d ∈ triangleSet t

/-- The ray from `Q` in direction `d` is admissible for the mesh `M`: the
  direction is nonzero and the open ray stays clear of every face's edges.

This forces every met face to be crossed *transversally through its relative
interior*.

Also see `exists_admissibleRay` in `CSG/Example.lean`. -/
def AdmissibleRay (M : Mesh) (Q d : Point) : Prop :=
  d ≠ 0 ∧ ∀ i : Fin M.size, ∀ s : ℚ, 0 < s → Q + s • d ∉ edgeSet M[i]

/-- The signed crossing count of the ray from point `Q` in direction `d`.

Every face met by the open ray contributes the sign of the scalar product of
`faceNormal` with `d` — `+1` when the ray crosses along the face's orientation,
`-1` against it. For an admissible ray each met face is crossed transversally,
so its contribution is `±1`.
-/
noncomputable def crossingCount (M : Mesh) (Q d : Point) : ℤ :=
  ∑ i : Fin M.size,
    if RayHits Q d M[i] then
      (if 0 < dot (faceNormal M[i]) d then 1
       else if dot (faceNormal M[i]) d < 0 then -1 else 0)
    else 0

/-- The solid bounded by a mesh: The points from which *every* admissible ray
  reports a nonzero signed crossing count.

Consider the equivalent characterization `solid_eq_exists_ray` for well-formed
meshes and the example `solid_unitCube` in `CSG/Example.lean`.  Note that for a
well-formed mesh the surface is not included in the solid (the *open*
convention). -/
def solid (M : Mesh) : Set Point :=
  { Q | ∀ d, AdmissibleRay M Q d → crossingCount M Q d ≠ 0 }

/-- A mesh has winding number zero or one when every admissible ray from every
  point in space reports a signed crossing count of `0` or `1`.

The mesh bounds its solid with multiplicity one, in its stored orientation. This
rules out e.g. doubly-traversed surfaces (winding `2`) and orientation-reversed
ones (winding `-1`), so such a mesh represents its solid faithfully, with
multiplicity one.
-/
def WindingZeroOrOne (M : Mesh) : Prop :=
  ∀ Q d, AdmissibleRay M Q d →
    crossingCount M Q d = 0 ∨ crossingCount M Q d = 1

/-- The three directed edges of an oriented face, in cyclic order. -/
def faceEdges (t : Triangle) : List (Point × Point) :=
  [(t.v₀, t.v₁), (t.v₁, t.v₂), (t.v₂, t.v₀)]

/-- The multiset of all directed edges over all faces of a mesh. -/
def edgeMultiset (M : Mesh) : Multiset (Point × Point) :=
  ↑(M.toList.flatMap faceEdges)

/-- A mesh is a closed surface with coherently oriented faces: Its directed-edge
  multiset is invariant under reversing every edge, i.e. each directed edge `a →
  b` occurs exactly as often as its reverse `b → a`.

It permits any *balanced* multiplicity (2, 4, 6, …) of faces along one edge —
for example four faces can meet along a shared edge where two solid components
touch — so it is strictly weaker than the 2-manifold condition "exactly two
opposite faces per edge". This weakening is needed so that intersections of any
two well-formed meshes can again be well-formed.

Note that edges subdivided differently on the two sides do *not* match.
-/
def IsClosedOrientedSurface (M : Mesh) : Prop :=
  edgeMultiset M = (edgeMultiset M).map Prod.swap

/-- No face-interior contact: any two *distinct* faces meet only within the
  edges of each.

Although the statement bounds the intersection only by the edges of face `i`,
instantiating it at both `(i, j)` and `(j, i)` confines the intersection to the
edges of *both* faces: no face may reach the relative *interior* of another. -/
def NoFaceInteriorContact (M : Mesh) : Prop :=
  ∀ i j : Fin M.size, i ≠ j → triangleSet M[i] ∩ triangleSet M[j] ⊆ edgeSet M[i]

/-- No degenerate faces: every face's vertices span a genuine triangle.

Nonzero oriented normal, i.e. the vertices are not collinear.
-/
def NoDegenerateFaces (M : Mesh) : Prop :=
  ∀ i : Fin M.size, faceNormal M[i] ≠ 0

/-- The well-formedness precondition for a mesh fed to the intersection
  algorithm.  A mesh is well-formed when it is:

* `IsClosedOrientedSurface` — a closed, coherently oriented surface;
* `WindingZeroOrOne` — every admissible ray from every point reports `0` or `1`;
* `NoFaceInteriorContact` — no face reaches the relative interior of any other;
* `NoDegenerateFaces` — every face is a genuine triangle.

The two middle conditions divide the work of ruling out self-contact:
`NoFaceInteriorContact` forbids crossings and overlaps at face interiors, while
`WindingZeroOrOne` forbids the surface from penetrating into the interior of the
solid. Together they confine self-contact to *touching* along edges and
vertices, with consistent inside/outside.

For non-vacuousness of the `WellFormedMesh` condition, consider
`unitCube_wellFormed` in `CSG/Example.lean` and note that the verified kernel
behind the web demo provably rejects exactly the meshes violating this condition
— see theorems in `CSG/MeshIntersectWithPreconditionCheck.lean`. -/
def WellFormedMesh (M : Mesh) : Prop :=
  IsClosedOrientedSurface M ∧ WindingZeroOrOne M ∧ NoFaceInteriorContact M ∧
    NoDegenerateFaces M

end CSG