/-!
# Diagnostic messages for the well-formedness check

For each of the four conditions of `WellFormedMesh`, we define a message stating
that it is violated.

See `CSG/WellFormedCheck.lean` and `CSG/MeshIntersectWithPreconditionCheck.lean`
for the functions that use these messages and the theorems that certify that
when these functions return such a message, the corresponding condition is
indeed violated.
-/

namespace CSG

/-- A mesh fails `IsClosedOrientedSurface`. -/
def msgNotClosed : String :=
  "The input mesh is not a closed oriented surface: its directed edges are not balanced (the IsClosedOrientedSurface precondition is violated)."

/-- A mesh fails `NoDegenerateFaces`. -/
def msgDegenerateFace : String :=
  "The input mesh has a degenerate face: the three vertices of some face are collinear (the NoDegenerateFaces precondition is violated)."

/-- A mesh fails `NoFaceInteriorContact`. -/
def msgFaceInteriorContact : String :=
  "The input mesh has faces in interior contact: some face reaches the relative interior of another face (the NoFaceInteriorContact precondition is violated)."

/-- A mesh fails `WindingZeroOrOne`. -/
def msgWindingNotZeroOrOne : String :=
  "The input mesh does not bound its solid with multiplicity one: some admissible ray reports a signed crossing count other than 0 or 1, e.g. from an inside-out orientation or a doubly-covered volume (the WindingZeroOrOne precondition is violated)."

end CSG
