Specify casing on built-in types - #7933
Conversation
kwxm
added
Plutus Core
Specification
Builtins
No Changelog Required
| \label{sec:builtin-casing} | ||
| In concrete implementations, some built-in types may admit \textit{casing}, | ||
| which allows them to be used as the scrutinee of the \texttt{case} construct. | ||
| One can write $\kase{M}{M_1 \ldots M_n}$ where $M$ evaluates to a |
There was a problem hiding this comment.
I've numbered branches from 1 to n here, rather than 0 to n-1. This allows us to use the case n=0 for the empty sequence, and avoids a lot of ?-1's elsewhere. What's annoying is that when we case on an integer, 0 selects the first branch, 1 the second branch, and so on, so we we have to have a k+1 there. That's only needed in one place though, as opposed to multiple -1's if we start from 0.
| built-in type $T \in \Uni$ we assume that there is a \textit{branch bound} | ||
| $\maxbranch(T) \in \N \disj \{\infty\}$ and a \textit{matching function} | ||
| $$ | ||
| \match{T}: \denote{T} \rightarrow \N \times \denote{\Uni}^* \disj \{\errorX\}. |
There was a problem hiding this comment.
I'm allowing the matching functions to return ⨯ here, signalling an error. We don't actually need that at the moment, but I think we will when/if @SeungheonOh's PR #7914 gets merged, since that will only work for Constr, and that'll have to be dealt with inside the matching function.
| % here. \ContinuedFloat makes the second part keep the same figure number and | ||
| % continue the subfigure lettering. | ||
| \begin{figure}[H]\ContinuedFloat | ||
| \begin{subfigure}[c]{\linewidth} |
There was a problem hiding this comment.
This renders pretty badly, taking up almost the entire width of the page. I couldn't think of a more compact way to do it though.
| \caption[]{A CEK machine for Plutus Core (continued)} | ||
| \end{figure} | ||
|
|
||
| \paragraph{Optimisations.} The machine presented above is suboptimal in a number |
There was a problem hiding this comment.
We talked about whether to include the implementation's optimisations in the specification, and I think we decided against it. This is my excuse for the discrepancies between the specification and the implementation. If we were really keen we could formalise both versions in Agda and prove that they produce the same results (although costs will unfortunately differ).
1 participant
This adds a specification of the built-in casing mechanism. There's a PDF attached. The main changes are
data, which isn't merged yet and definitely isn't available on the chain).A later PR will update the stuff about versions (PV/LL/etc) at the start of Chapter 4 since that's now a bit out of date.
plutus-core-specification.pdf
I was going to add a changelog entry for this, but we don't have a changelog for documentation and the specification isn't included in the release.