3SAT.swift

// swift -Xfrontend -debug-constraints

infix operator ^&&^ : LogicalConjunctionPrecedence
infix operator ^||^ : LogicalConjunctionPrecedence

struct T{}
struct F{}

func λ(_ f : (T) -> ()) {
  print("true")
  f(T())
}
func λ(_ f : (F) -> ()) {
  print("false")
  f(F())
}

// MARK: Trinary operators

func ^||^(_ : T, _ : T) -> (T) -> T { return { _ in T() } }
func ^||^(_ : T, _ : T) -> (F) -> T { return { _ in T() } }
func ^||^(_ : T, _ : F) -> (T) -> T { return { _ in T() } }
func ^||^(_ : T, _ : F) -> (F) -> T { return { _ in T() } }
func ^||^(_ : F, _ : T) -> (T) -> T { return { _ in T() } }
func ^||^(_ : F, _ : T) -> (F) -> T { return { _ in T() } }
func ^||^(_ : F, _ : F) -> (T) -> T { return { _ in T() } }
func ^||^(_ : F, _ : F) -> (F) -> F { return { _ in F() } }

func ^||^(_ : (T) -> T, _ : T) -> T { return T() }
func ^||^(_ : (T) -> T, _ : F) -> T { return T() }
func ^||^(_ : (T) -> F, _ : T) -> T { return T() }
func ^||^(_ : (T) -> F, _ : F) -> T { return T() }
func ^||^(_ : (F) -> T, _ : T) -> T { return T() }
func ^||^(_ : (F) -> T, _ : F) -> T { return T() }
func ^||^(_ : (F) -> F, _ : T) -> T { return T() }
func ^||^(_ : (F) -> F, _ : F) -> F { return F() }

// MARK: Binary operators

func ^&&^(_ : T, _ : T) -> T { return T() }
func ^&&^(_ : T, _ : F) -> F { return F() }
func ^&&^(_ : F, _ : T) -> F { return F() }
func ^&&^(_ : F, _ : F) -> F { return F() }

// MARK: Unary operators

prefix func !(_ : T) -> F { return F() }
prefix func !(_ : F) -> T { return T() }


func assert(true : T) {}
func assert(false : F) {}

λ { x1 in
  λ { x2 in
    λ { x3 in
      assert(true: (x1 ^||^ x2 ^||^ !x3) ^&&^ (x1 ^||^ !x2 ^||^ x3) ^&&^ (!x1 ^||^ !x2 ^||^ x3) ^&&^ (!x1 ^||^ !x2 ^||^ !x3))
    }
  }
}