Wrap given element into a constructor with the given name.

Mentioned constructor must have only one field.

Since labels interpretable by OverloadedLabels extension cannot start with capital latter, prepend constructor name with letter "c" (see examples below).

Like instrWrap but only works for contructors with a single field. Results in a type error if a constructor with no field is used instead.

Wrap a haskell value into a constructor with the given name.

This is symmetric to instrWrap.

Pattern-match on the given datatype.

Lift an instruction to case clause.

You should write out constructor name corresponding to the clause explicitly. Prefix constructor name with "c" letter, otherwise your label will not be recognized by Haskell parser. Passing constructor name can be circumvented but doing so is not recomended as mentioning contructor name improves readability and allows avoiding some mistakes.

Unwrap a constructor with the given name.

Rules which apply to instrWrap function work here as well. Although, unlike instrWrap, this function does not work for nullary constructors.

Try to unwrap a constructor with the given name.

In what different case branches differ - related constructor name and input stack type which the branch starts with.

Type information about single case clause.

List of CaseClauseParams required to pattern match on the given type.

Which branch to choose in generic tree representation: left, straight or right. S is used when there is one constructor with one field (something newtype-like).

The reason why we need S can be explained by this example: data A = A1 B | A2 Integer data B = B Bool Now we may search for A1 constructor or B constructor. Without S in both cases path will be the same ([L]).

Path to a leaf (some field or constructor) in generic tree representation.

We support only two scenarious - constructor with one field and without fields. Nonetheless, it's not that sad since for sum types we can't even assign names to fields if there are many (the style guide prohibits partial records).

Get something as field of the given constructor.

Push field to stack, if any.

To use AppendCtorField not only here for T-based stacks, but also later in Lorentz with Type-based stacks we need the following property.

Proof of AppendCtorFieldAxiom.

Get type of constructor fields (one or zero) referred by given datatype and name.

Expect referred constructor to have only one field (in form of constraint) and extract its type.

Expect referred constructor to have only one field (otherwise compile error is raised) and extract its type.

Whether given type represents an atomic Michelson value.