Module Nuscrlib.LiteratureSyntax

A Multiparty Session Type representation that is similar to those used in the literature

type global =
  1. | BranchG of {
    1. g_br_from : Names.RoleName.t;
    2. g_br_to : Names.RoleName.t;
    3. g_br_cont : global cont_list;
    }
    (*

    p -> q : { l_i(S_i) . G_i }_{i \in I}

    *)
  2. | MuG of Names.TypeVariableName.t * global
    (*

    mu t. G

    *)
  3. | TVarG of Names.TypeVariableName.t
    (*

    t

    *)
  4. | EndG
    (*

    end

    *)

Global Types with basic features, in a form that is similar to those seen in standard literature. (No choice constructor, all choices are directed)

type local =
  1. | SendL of Names.RoleName.t * local cont_list
    (*

    !p { l_i(S_i) . L_i }_{i \in I}

    *)
  2. | RecvL of Names.RoleName.t * local cont_list
    (*

    ?p { l_i(S_i) . L_i }_{i \in I}

    *)
  3. | MuL of Names.TypeVariableName.t * local
    (*

    mu t. L

    *)
  4. | TVarL of Names.TypeVariableName.t
    (*

    t

    *)
  5. | EndL
    (*

    end

    *)
val from_gtype : Gtype.t -> global

Convert from a Gtype.t

val from_ltype : Ltype.t -> local

Convert from a Ltype.t

val show_gtype_mpstk : global -> Base.string

Output the global type in a form recognised by MPSTK. https://github.com/alcestes/mpstk

val show_ltype_mpstk : local -> Base.string

Output the local type in a form recognised by MPSTK. https://github.com/alcestes/mpstk