import CSG.Def
import CSG.MeshIntersect
import CSG.WellFormedCheckMsg
import CSG.Impl.MeshIntersectWithPreconditionCheck
import CSG.Proof.MeshIntersectM2

/-!
# Precondition-checking mesh intersection and its specification

This file exposes and specifies `meshIntersectWithPreconditionCheck` that checks
the preconditions on the inputs at runtime before computing the intersection. We
verify the behavior of this function in all cases, so it can be run on untrusted
input meshes.

If the function does not return an error, the output mesh is guaranteed to
follow the intersection specification and to be itself well-formed.  It errors
exactly when an input is not well-formed, with a message naming a violated
precondition.

The four error strings are defined in `CSG/WellFormedCheckMsg.lean`.

The implementation lives in `CSG/Impl/`. The proofs live in `CSG/Proof/`.
-/

namespace CSG

/-- Mesh intersection with precondition check.

Decides `WellFormedMesh` of each input, returning `Except.error msg` naming a
failing precondition, or returning the intersection mesh when both inputs are
well-formed. See specification in theorems below.
-/
def meshIntersectWithPreconditionCheck (M₁ M₂ : Mesh) : Except String Mesh :=
  Impl.MeshIntersectWithPreconditionCheck.run
    msgNotClosed msgDegenerateFace msgFaceInteriorContact msgWindingNotZeroOrOne
    M₁ M₂

/--
If the function returns a mesh `M`, then the solid bounded by the returned mesh
`M` equals the intersection of the input solids, and `M` is itself a well-formed
mesh.  No hypotheses on the inputs are needed. -/
theorem meshIntersectWithPreconditionCheck_ok_spec (M₁ M₂ M : Mesh)
    (h : meshIntersectWithPreconditionCheck M₁ M₂ = Except.ok M) :
    solid M = solid M₁ ∩ solid M₂ ∧ WellFormedMesh M :=
  Proof.MeshIntersectM2.run_ok_spec
    msgNotClosed msgDegenerateFace msgFaceInteriorContact msgWindingNotZeroOrOne
    M₁ M₂ M h

/--
Well-formed inputs are always accepted.
-/
theorem meshIntersectWithPreconditionCheck_ok_of_wellFormed (M₁ M₂ : Mesh)
    (h₁ : WellFormedMesh M₁) (h₂ : WellFormedMesh M₂) :
    meshIntersectWithPreconditionCheck M₁ M₂ = Except.ok (meshIntersect M₁ M₂) :=
  Proof.MeshIntersectM2.run_ok_of_wellFormed
    msgNotClosed msgDegenerateFace msgFaceInteriorContact msgWindingNotZeroOrOne
    M₁ M₂ h₁ h₂

/--
Every message the function emits is one of the four canonical strings, and the
precondition it names is genuinely violated by at least one of the two inputs.
-/
theorem meshIntersectWithPreconditionCheck_error_sound (M₁ M₂ : Mesh)
    (msg : String)
    (h : meshIntersectWithPreconditionCheck M₁ M₂ = Except.error msg) :
    (msg = msgNotClosed ∧ (¬ IsClosedOrientedSurface M₁ ∨ ¬ IsClosedOrientedSurface M₂)) ∨
    (msg = msgDegenerateFace ∧ (¬ NoDegenerateFaces M₁ ∨ ¬ NoDegenerateFaces M₂)) ∨
    (msg = msgFaceInteriorContact ∧
      (¬ NoFaceInteriorContact M₁ ∨ ¬ NoFaceInteriorContact M₂)) ∨
    (msg = msgWindingNotZeroOrOne ∧
      (¬ WindingZeroOrOne M₁ ∨ ¬ WindingZeroOrOne M₂)) :=
  Proof.MeshIntersectM2.run_error_sound
    msgNotClosed msgDegenerateFace msgFaceInteriorContact msgWindingNotZeroOrOne
    M₁ M₂ msg h

/-- If either input is not well-formed, the function always returns some error.
  -/
theorem meshIntersectWithPreconditionCheck_error_of_not_wellFormed (M₁ M₂ : Mesh)
    (h : ¬ WellFormedMesh M₁ ∨ ¬ WellFormedMesh M₂) :
    ∃ msg, meshIntersectWithPreconditionCheck M₁ M₂ = Except.error msg :=
  Proof.MeshIntersectM2.run_error_of_not_wellFormed
    msgNotClosed msgDegenerateFace msgFaceInteriorContact msgWindingNotZeroOrOne
    M₁ M₂ h

end CSG
