import RoleFlow.Flow.Basic
import RoleFlow.FrontSem

/-! # The swaps of the flow signature

`add` is the swappable operation (`Swap`): `add(a, b)` consumes `a`, and `add(b, a)` consumes `b`.
It commutes with log-weight `0`, so the flow model is lawful for the front end. -/

namespace RoleFlow.Flow

open FS

/-- `add` (not `sub`). -/
def isAdd : {as bs : List FS} → FOp as bs → Bool
  | _, _, .add _ false => true
  | _, _, _ => false

instance : Swap flowSig where
  swappable := isAdd
  sorts o h := by cases o <;> simp [isAdd] at h; exact ⟨_, rfl⟩
  k_one o h := by cases o <;> simp [isAdd] at h; exact ⟨_, rfl, rfl⟩

/-- `add` commutes, and its log-weight is `0`. -/
theorem swapLawful : Swap.Lawful flowModel.toModel := by
  intro as bs o hs Γ a b h h' v
  cases o <;> simp [Swap.swappable, isAdd] at hs
  rename_i n inv; cases inv <;> simp at hs
  refine ⟨?_, rfl⟩
  simp only [flowModel, semOp, Val.pick, Val.head_cons, Val.tail_cons, negIf]
  congr 1; funext i; exact add_comm _ _

end RoleFlow.Flow