Binary Dependent Session Types

staload "./libsession.sats"

stadef proto_eq = pmsg(1,int)::pmsg(1,int)::pmsg(0,bool)::pend(1)
stadef proto_eq_dep = pquan(1,lam (n:int) => pquan(1,lam (m:int) => pmsg(1,int n)::pmsg(1, int m)::pmsg(0, bool (m==n))::pend(1)))


extern fun eq_cli (session(1,proto_eq)): void
extern fun eq_srv (session(0,proto_eq)): void 

implement eq_cli (session) = let 
    val _ = session_send (session, 1)
    val _ = session_send (session, 2)
    val result = session_recv (session)
    val _ = println! result
in 
    session_close (session)
end 

implement eq_srv (session) = let 
    val a = session_recv (session)
    val b = session_recv (session)
    val _ = session_send (session, a = b)
in 
    session_wait (session)
end

extern fun eq_dep_cli (session(1,proto_eq_dep)): void 
extern fun eq_dep_srv (session(0,proto_eq_dep)): void 

implement eq_dep_cli (session) = let 
    val session = session_unify (session)
    val session = session_unify (session)
    val a = 1
    val b = 2
    val _ = session_send (session, a)
    val _ = session_send (session, b)
    val result = session_recv (session)
in 
    session_close (session)
end

implement eq_dep_srv (session) = let 
    val session = session_exify (session)
    val session = session_exify (session)
    val a = session_recv (session)
    val b = session_recv (session)
    val _ = session_send (session, ~(a != b))
in 
    session_wait (session)
end