mirror of
https://github.com/clockworklabs/SpacetimeDB.git
synced 2026-05-14 11:48:28 -04:00
Tyler Cloutier
158 lines
6.5 KiB
TeX
158 lines
6.5 KiB
TeX
% !TeX root = spec.tex
|
|
|
|
\def\hex#1{\texttt{0x#1}}
|
|
\let\T=\mathtt
|
|
\let\NT=\mathit
|
|
\let\V=\textsf
|
|
\let\F=\operatorname
|
|
\let\v=\mathit
|
|
\def\specdef#1{& \T{#1} & ::= &}
|
|
\def\uN{\T{u\mathit{N}}}
|
|
\def\iN{\T{i\mathit{N}}}
|
|
\def\iff{\text{if }}
|
|
|
|
\begin{array}{llclll}
|
|
& \T{Bool} & ::= &
|
|
\hex{00} & \Rightarrow & \V{true} \\ &&|&
|
|
\hex{01} & \Rightarrow & \V{false}
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\begin{array}{llclll}
|
|
& \T{U\v{N}} & ::= &
|
|
x{:}\uN & \Rightarrow & x
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
|
|
\begin{array}{llclll}
|
|
& \T{I\v{N}} & ::= &
|
|
x{:}\uN & \Rightarrow & \F{twoscomplement}(x)
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\begin{array}{llclll}
|
|
& \T{F32} & ::= &
|
|
x{:}\T{u32} & \Rightarrow & \F{from\_bits}(x)
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\begin{array}{llclll}
|
|
& \T{F64} & ::= &
|
|
x{:}\T{u64} & \Rightarrow & \F{from\_bits}(x)
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\begin{array}{llclll}
|
|
& \T{vec}(\T{B}) & ::= &
|
|
n{:}\T{u32} ~~ (x{:}\T{B})^n & \Rightarrow & x^n
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\begin{array}{llclll}
|
|
& \T{Array}(\T{E}) & ::= &
|
|
e^*{:}\T{vec}(E) & \Rightarrow & [e^*]
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\begin{array}{llclll}
|
|
& \T{String} & ::= &
|
|
b^*{:}\T{vec}(\T{u8}) & \Rightarrow & \F{from\_utf8}(b^*)
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\begin{array}{llclll}
|
|
& \T{Map}(\T{K},\T{V}) & ::= &
|
|
e^*{:}\T{vec}(\T{map\_element}(\T{K},\T{V})) & \Rightarrow & \{e^*\}
|
|
% TODO: should this be \iff is_sorted(e*) ?
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\begin{array}{llclll}
|
|
& \T{map\_element}(\T{K},\T{V}) & ::= &
|
|
k{:}\T{K} ~~ v{:}\T{V} & \Rightarrow & \{ \V{key}~k, \V{value}~v \}
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\begin{array}{llcllll}
|
|
& \T{Sum}_{\mathord{\V{ty}{:}\V{sumtype}}} & ::= &
|
|
i{:}\T{u8} ~~ v{:}\V{ty.variants}[i]\V{.algebraic\_type} & \Rightarrow & \{ \V{tag}~i, \V{value}~v \} & (\iff i < |\V{ty.variants}|)
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\begin{array}{llclll}
|
|
& \T{Product}_{\V{ty}{:}\V{producttype}} & ::= &
|
|
(v{:}\V{ty.elements}[i]\V{.algebraic\_type})^{|\V{ty.elements}|} & \Rightarrow & [v^{|\V{ty.elements}|}]
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\text{for example/reference, below is \texttt{AlgebraicType} expanded into the above value specification:}
|
|
\\{}\\
|
|
|
|
\begin{array}{llclll}
|
|
& \T{typespace} & ::= &
|
|
r{:}\T{u32} ~~ t^*{:}\T{vec}(\T{algebraictype}) & \Rightarrow & \{ \V{root}~r, \V{types}~[t^*] \}
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\begin{array}{llclll}
|
|
& \T{algebraictype} & ::= &
|
|
\hex{00} ~~ x{:}\T{sumtype} & \Rightarrow & \V{sumtype}~x \\ &&|&
|
|
\hex{01} ~~ x{:}\T{producttype} & \Rightarrow & \V{producttype}~x \\ &&|&
|
|
\hex{02} ~~ x{:}\T{builtintype} & \Rightarrow & \V{builtintype}~x \\ &&|&
|
|
\hex{04} ~~ x{:}\T{u32} & \Rightarrow & \V{typeref}~x
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\begin{array}{llclll}
|
|
& \T{option}(\T{B}) & ::= &
|
|
\hex{00} ~~ x{:}\T{B} & \Rightarrow & \V{some}~x \\ &&|&
|
|
\hex{01} & \Rightarrow & \V{none}
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\begin{array}{llclll}
|
|
& \T{sumtype} & ::= &
|
|
v^*{:}\T{vec}(\T{sumtypevariant}) & \Rightarrow & \{ \V{variants}~[v^*] \}
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\begin{array}{llclll}
|
|
& \T{sumtypevariant} & ::= &
|
|
n{:}\T{option}(\T{String}) ~~ t{:}\T{algebraictype} & \Rightarrow & \{ \V{name}~n, \V{algebraic\_type}~t \}
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\begin{array}{llclll}
|
|
& \T{producttype} & ::= &
|
|
e^*{:}\T{vec}(\T{producttypeelement}) & \Rightarrow & \{ \V{elements}~[e^*] \}
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\begin{array}{llclll}
|
|
& \T{producttypeelement} & ::= &
|
|
n{:}\T{option}(\T{String}) ~~ t{:}\T{algebraictype} & \Rightarrow & \{ \V{name}~n, \V{algebraic\_type}~t \}
|
|
\end{array}
|
|
\\{}\\
|
|
|
|
\begin{array}{llclll}
|
|
& \T{builtintype} & ::= &
|
|
\hex{00} & \Rightarrow & \V{bool} \\ &&|&
|
|
\hex{01} & \Rightarrow & \V{i8} \\ &&|&
|
|
\hex{02} & \Rightarrow & \V{u8} \\ &&|&
|
|
\hex{03} & \Rightarrow & \V{i16} \\ &&|&
|
|
\hex{04} & \Rightarrow & \V{u16} \\ &&|&
|
|
\hex{05} & \Rightarrow & \V{i32} \\ &&|&
|
|
\hex{06} & \Rightarrow & \V{u32} \\ &&|&
|
|
\hex{07} & \Rightarrow & \V{i64} \\ &&|&
|
|
\hex{08} & \Rightarrow & \V{u64} \\ &&|&
|
|
\hex{09} & \Rightarrow & \V{i128} \\ &&|&
|
|
\hex{0A} & \Rightarrow & \V{u128} \\ &&|&
|
|
\hex{0B} & \Rightarrow & \V{f32} \\ &&|&
|
|
\hex{0C} & \Rightarrow & \V{f64} \\ &&|&
|
|
\hex{0D} & \Rightarrow & \V{string} \\ &&|&
|
|
\hex{0E} ~~ t{:}\T{algebraictype} & \Rightarrow & \V{array}~\{ \V{ty}~t \} \\ &&|&
|
|
\hex{0F} ~~ k{:}\T{algebraictype} ~~ v{:}\T{algebraictype} & \Rightarrow & \V{map}~\{ \V{key\_ty}~k, \V{ty}~v\}
|
|
\end{array}
|
|
\\{}\\
|