import Mathlib
import SessionCoTypes.Coinductive.LocalTypeC
import SessionTypes.LocalTypeR

set_option linter.dupNamespace false


/-
The Problem. We have two representations of local types: the inductive
LocalTypeR (finite, pattern-matchable) and the coinductive LocalTypeC
(potentially infinite, M-type). We need to embed inductive types into
the coinductive world for equivalence proofs and bisimulation.

Solution Structure. Define a recursive embedding `toCoind : LocalTypeR → LocalTypeC`
that maps each inductive constructor to its smart constructor counterpart.
Prove simp lemmas for each constructor case.
-/

namespace SessionCoTypes.Coinductive

open SessionTypes.GlobalType
open SessionTypes.LocalTypeR

/-! ## Embedding -/

mutual
  /-- Embed an inductive local type into the coinductive representation.
      This is a structure-preserving map: end → mkEnd, var → mkVar, etc. -/
  def toCoind : LocalTypeR → LocalTypeC
    | .end       => mkEnd
    | .var x     => mkVar x
    | .mu x body => mkMu x (toCoind body)
    | .send p bs => mkSend p (toCoindBranches bs)
    | .recv p bs => mkRecv p (toCoindBranches bs)

  /-- Embed a list of branches, converting each continuation. -/
  def toCoindBranches : List BranchR → List (Label × LocalTypeC)
    | []             => []
    | (lb, _vt, t) :: rest => (lb, toCoind t) :: toCoindBranches rest
end

/-! ## Simp Lemmas -/

@[simp] theorem to_coind_end : toCoind .end = mkEnd := rfl
@[simp] theorem to_coind_var (x : String) : toCoind (.var x) = mkVar x := rfl
@[simp] theorem to_coind_mu (x : String) (body : LocalTypeR) :
    toCoind (.mu x body) = mkMu x (toCoind body) := rfl
@[simp] theorem to_coind_send (p : String) (bs : List BranchR) :
    toCoind (.send p bs) = mkSend p (toCoindBranches bs) := rfl
@[simp] theorem to_coind_recv (p : String) (bs : List BranchR) :
    toCoind (.recv p bs) = mkRecv p (toCoindBranches bs) := rfl

end SessionCoTypes.Coinductive
