View Source ElixirST.ST (ElixirST v0.8.3)
Manipulate Session Type (ST) data.
Session type definitions:
! = send
? = receive
& = branch (or external choice)
+ = (internal) choiceSession types accept the following grammar:
S =
!label(types, ...).S
| ?label(types, ...).S
| &{?label(types, ...).S, ...}
| +{!label(types, ...).S, ...}
| rec X.(S)
| X
| endNote: The session type end is optional, therefore !Hello() and !Hello().end are equivalent.
X refers to to a variable which can be called later in a recursion operation.
rec X.(S) refers to recursion, or looping - when X is called, it is replaced with the whole session type
rec X.(S).
Some session types examples:
!Hello() # Sends {:Hello}
?Ping(number) # Receives {:Ping, value}, where values has to be a number
&{?Option1().!Hello(), ?Option2()} # Receive either {:Option1} or {:Option2}. If it
# receives the former, then it sends {:Hello}. If it
# receives {:Option2}, then it terminates.
rec X.(&{?Stop().end, ?Retry().X}) # The actor is able to receive multiple {:Retry},
# and terminates when it receives {:Stop}.Internal representation of session types take the form of the following structs:
%Send{label, types, next}%Recv{label, types, next}%Choice{choices}%Branch{branches}%Recurse{label, body}%Call_Recurse{label}%Terminate{}
The labels and types are of type label/0 and types/0, respectively. next, choices, branches and body have the type
session_type/0.
Parser
Parses an input string to session types (as Elixir data).
Simple example
iex> s = "!Hello(Number)"
...> ElixirST.ST.string_to_st(s)
%ElixirST.ST.Send{label: :Hello, next: %ElixirST.ST.Terminate{}, types: [:number]}Another example
iex> s = "rec X.(&{?Ping().!Pong().X, ?Quit().end})"
...> ElixirST.ST.string_to_st(s)
%ElixirST.ST.Recurse{
label: :X,
body: %ElixirST.ST.Branch{
branches: %{
Ping: %ElixirST.ST.Recv{
label: :Ping,
next: %ElixirST.ST.Send{label: :Pong, next: %ElixirST.ST.Call_Recurse{label: :X}, types: []},
types: []
},
Quit: %ElixirST.ST.Recv{label: :Quit, next: %ElixirST.ST.Terminate{}, types: []}
}
}
}Summary
Types
Abstract Syntax Tree (AST)
Label for sending/receiving statements. Should be of the form of an atom.
Type for name and arity keys.
A session type list of session operations.
Session types when stored as tuples. Useful for when converting from Erlang records.
Native types accepted in the send/receive statements. E.g. !Ping(integer)
Functions
Returns the dual of the given session type.
Converts s session type to a string. To do the opposite, use string_to_st/1.
Converts the current session type to a string. E.g. ?Hello().!hi() would return ?Hello() only.
Converts a string to a session type. To do the opposite, use st_to_string/1.
May throw a runtime error message if parsing fails.
Takes a session type (starting with a recursion, e.g. rec X.(...)) and outputs a single unfold of X.
Types
@type ast() :: Macro.t()
Abstract Syntax Tree (AST)
@type label() :: atom()
Label for sending/receiving statements. Should be of the form of an atom.
@type name_arity() :: {label(), non_neg_integer()}
Type for name and arity keys.
@type session_type() :: %ElixirST.ST.Send{label: label(), next: session_type(), types: types()} | %ElixirST.ST.Recv{label: label(), next: session_type(), types: types()} | %ElixirST.ST.Choice{choices: %{required(label()) => session_type()}} | %ElixirST.ST.Branch{branches: %{required(label()) => session_type()}} | %ElixirST.ST.Recurse{ body: session_type(), label: label(), outer_recurse: term() } | %ElixirST.ST.Call_Recurse{label: label()} | %ElixirST.ST.Terminate{}
A session type list of session operations.
@type session_type_tuple() :: {:send, atom(), [atom()], session_type_tuple()} | {:recv, atom(), [atom()], session_type_tuple()} | {:choice, [session_type_tuple()]} | {:branch, [session_type_tuple()]} | {:call, atom()} | {:recurse, atom(), session_type_tuple()} | {:terminate}
Session types when stored as tuples. Useful for when converting from Erlang records.
@type types() :: [
:atom
| :binary
| :bitstring
| :boolean
| :exception
| :float
| :function
| :integer
| :list
| :map
| nil
| :number
| :pid
| :port
| :reference
| :struct
| :tuple
| :string
]
Native types accepted in the send/receive statements. E.g. !Ping(integer)
Functions
@spec dual(session_type()) :: session_type()
Returns the dual of the given session type.
Changes that are made:
- Receive <-> Send
- Branch <-> Choice
Examples
iex> st_string = "!Ping(Number).?Pong(String)"
...> st = ElixirST.Parser.parse(st_string)
...> st_dual = ElixirST.ST.dual(st)
...> ElixirST.ST.st_to_string(st_dual)
"?Ping(number).!Pong(string)"@spec dual?(session_type(), session_type()) :: boolean()
@spec equal?(session_type(), session_type()) :: boolean()
@spec st_to_string(session_type()) :: String.t()
Converts s session type to a string. To do the opposite, use string_to_st/1.
Examples
iex> s = "rec x.(&{?Hello(number), ?Retry().X})"
...> st = ElixirST.ST.string_to_st(s)
...> ElixirST.ST.st_to_string(st)
"rec x.(&{?Hello(number), ?Retry().X})"@spec st_to_string_current(session_type()) :: String.t()
Converts the current session type to a string. E.g. ?Hello().!hi() would return ?Hello() only.
Examples
iex> s = "?Hello(number).?Retry()"
...> st = ElixirST.ST.string_to_st(s)
...> ElixirST.ST.st_to_string_current(st)
"?Hello(number)"@spec string_to_st(String.t()) :: session_type()
Converts a string to a session type. To do the opposite, use st_to_string/1.
May throw a runtime error message if parsing fails.
Examples
iex> s = "?Ping().!Pong()"
...> ElixirST.ST.string_to_st(s)
%ElixirST.ST.Recv{
label: :Ping,
next: %ElixirST.ST.Send{label: :Pong, next: %ElixirST.ST.Terminate{}, types: []},
types: []
}@spec unfold(session_type()) :: session_type()
Takes a session type (starting with a recursion, e.g. rec X.(...)) and outputs a single unfold of X.
Examples
iex> st = "rec X.(!A().X)"
...> session_type = ElixirST.ST.string_to_st(st)
...> unfolded = ElixirST.ST.unfold(session_type)
...> ElixirST.ST.st_to_string(unfolded)
"!A().rec X.(!A().X)"