From 8e98087a9efda603cc5d5e4dbdffc2446d7480f1 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 12 Sep 2024 18:43:10 +0100 Subject: [PATCH] Documentation: Add union example Adjust Sail options to use the more typical style --- doc/asciidoc/Makefile | 1 + doc/asciidoc/language.adoc | 64 ++++++++- doc/asciidoc/manual.adoc | 1 + doc/asciidoc/modules.adoc | 4 +- doc/asciidoc/usage.adoc | 107 +++++++------- doc/examples/union.sail | 57 ++++++++ doc/manual.html | 286 +++++++++++++++++++++++++++++-------- 7 files changed, 408 insertions(+), 112 deletions(-) create mode 100644 doc/examples/union.sail diff --git a/doc/asciidoc/Makefile b/doc/asciidoc/Makefile index d329d001e..9c5a41d84 100644 --- a/doc/asciidoc/Makefile +++ b/doc/asciidoc/Makefile @@ -17,6 +17,7 @@ SAIL_DOCS += sail_doc/list.json SAIL_DOCS += sail_doc/bitvector_and_generic.json SAIL_DOCS += sail_doc/struct.json SAIL_DOCS += sail_doc/enum.json +SAIL_DOCS += sail_doc/union.json SAIL_DOCS += module_sail_doc/simple_mod.json SAIL_DOCS += module_sail_doc/simple_mod_err.error SAIL_DOCS += module_sail_doc/cond.sail_project diff --git a/doc/asciidoc/language.adoc b/doc/asciidoc/language.adoc index da340dc42..e760b8c9d 100644 --- a/doc/asciidoc/language.adoc +++ b/doc/asciidoc/language.adoc @@ -439,12 +439,70 @@ sail::ENUM_CONV[from=enum,type=span] The `no_enum_number_conversions` attribute can be used to disable the generation of these functions entirely. +==== Unions +:union: sail_doc/union.json + +Structs provide us a way to group multiple pieces of related data, for example + +sail::rectangle[from=union,type=type] + +defines a type `rectangle` that has both a width _and_ a height. The +other logical way to combine data is if we want to say we have some +data _or_ some other data, like if we wanted to represent a shape that +could be a circle _or_ a rectangle. In Sail, we use a _union_ for this. + +sail::SHAPE[from=union,type=span] + +NOTE: While structs are ubiquitous in programming languages, the +equivalent feature for safely representing disjunctions of types is +often a second-class afterthought or even absent entirely. The +requirement to safely represent disjunctions of types is why C's +`union` feature is something different to what we want here, which is +sometimes called _tagged_ unions or _variants_ to distinguish them +from the unsafe C construct. C++ is therefore a good example of a +language where structs are first class, but `std::variant` is +relegated to a library feature. + +This defines a type with two _constructors_ `Rectangle` and `Circle`. +Constructors are used like functions with a single argument, as so: + +sail::example[from=union] + +To destructure unions, we typically use _pattern matching_ to handle +each case in the union separately. This will be discussed in detail in +<>. + +Constructors in Sail always have a single argument. If we want a +constructor in a union type to contain no information, then we can use +the `unit` type. For a constructor with multiple arguments we can use +a tuple type. We provide some syntax sugar that allows writing +constructor applications with either tuple or unit argument types as +if they were functions with multiple arguments or no arguments +respectively. + +sail::EX_UNIT[from=union,type=span] + +In our shape example, we defined `rectangle` and `circle` as two +separate structs, but if we wanted we could declare those structs +inline + +sail::shape2[from=union,type=type] + +Behind the scenes, Sail will just generate separate struct +definitions, so we use this type in exactly the same was as we did +previously. + +As with structs, we can define polymorphic union types, like + +sail::either[from=union,type=type] + === Pattern matching :pattern-match: sail_doc/pattern_matching.json :cannot-wildcard: sail_doc/cannot_wildcard.json -Like most functional languages, Sail supports pattern matching via the -`match` keyword. For example: +Like most functional languages, and an increasing number of imperative +languages like Rust, Sail supports _pattern matching_ via the `match` +keyword. For example: sail::example[from=pattern-match,part=body,dedent] @@ -706,7 +764,7 @@ keyword within a block. Like let-bound variables, mutable variables are lexically scoped, so they only exist within the block that declared them. -Technically, unless the `-strict_var` option is used Sail also allows +Technically, unless the `--strict-var` option is used Sail also allows mutable variables to be implicitly declared, like so: [source,sail] diff --git a/doc/asciidoc/manual.adoc b/doc/asciidoc/manual.adoc index 16d736490..a4505bdeb 100644 --- a/doc/asciidoc/manual.adoc +++ b/doc/asciidoc/manual.adoc @@ -8,6 +8,7 @@ Alasdair Armstrong; Thomas Bauereiss; Brian Campbell; Shaked Flur; Kathryn E. Gr :title-logo-image: image:../../etc/logo/sail_logo_square.svg[top=25%,align=center,pdfwidth=2in] :docinfo: shared :toc: left +:toclevels: 4 :stylesheet: manual.css == Introduction diff --git a/doc/asciidoc/modules.adoc b/doc/asciidoc/modules.adoc index 34809425d..be0f7480b 100644 --- a/doc/asciidoc/modules.adoc +++ b/doc/asciidoc/modules.adoc @@ -118,7 +118,7 @@ sense in this example. === Working with Makefiles -The `-list_files` option can be used to list all the files within a +The `--list-files` option can be used to list all the files within a project file, which allows them to be used in a Makefile prerequisite. As an example, to build the module examples in this very manual, we use the rule below to generate documentation indexes (which our @@ -131,7 +131,7 @@ file. module_sail_doc/%.json: ../examples/%.sail_project $$(shell sail ../examples/%.sail_project -list_files) mkdir -p module_sail_doc - sail -doc $(addprefix -doc_file ,$(shell sail $< -list_files)) -doc_embed plain -doc_bundle $(notdir $@) -o module_sail_doc $< + sail --doc $(addprefix -doc_file ,$(shell sail $< --list-files)) --doc-embed plain --doc-bundle $(notdir $@) -o module_sail_doc $< ---- === Conditional compilation within modules diff --git a/doc/asciidoc/usage.adoc b/doc/asciidoc/usage.adoc index 57145d98d..d1558a5b2 100644 --- a/doc/asciidoc/usage.adoc +++ b/doc/asciidoc/usage.adoc @@ -42,16 +42,12 @@ For more complex projects, a module hierarchy can be defined. See the === Sail options -For command line arguments, by default Sail accepts arguments of -the form `‑long_opt`, i.e. leading with a single `-` and words -separated by `_`. For those who find this departure from standard -convention distasteful, you can define the `SAIL_NEW_CLI` environment -variable, and all such options will be formatted as -`‑‑long‑opt` (short opts like `‑o` will remain -unchanged). For backwards compatibility reasons, this default is hard -to change. +For backwards compatibility reasons, Sail accepts arguments of the +form `-long_opt`, i.e. leading with a single `-` and words +separated by `_`. Such an option will be treated the same as +`--long-opt`. -For a list of all options, one can call Sail as `sail -help`. +For a list of all options, one can call Sail as `sail --help`. <<< === C compilation @@ -82,14 +78,14 @@ There are several Sail options that affect the C output: * `-O` turns on optimisations. The generated C code will be quite slow unless this flag is set. -* `-Oconstant_fold` apply constant folding optimisations. +* `--Oconstant-fold` apply constant folding optimisations. -* `-c_include` Supply additional header files to be included in the +* `--c-include` Supply additional header files to be included in the generated C. -* `-c_no_main` Do not generate a `main()` function. +* `--c-no-main` Do not generate a `main()` function. -* `-static` Mark generated C functions as static where possible. This +* `--static` Mark generated C functions as static where possible. This is useful for measuring code coverage. <<< @@ -100,34 +96,34 @@ to provide working SystemVerilog. Furthermore, it is intended for hardware model checking against a hand-written design. Sail is not a hardware description language! -To compile Sail into SystemVerilog, the `-sv` option is used. The `-o` +To compile Sail into SystemVerilog, the `--sv` option is used. The `-o` option provides a prefix that is used on the various generated files. There are several options for the SystemVerilog output: -* `-sv_output_dir` Generate all files in the specified directory +* `--sv-output-dir` Generate all files in the specified directory -* `-sv_include` Add an include directive to the generated SystemVerilog +* `--sv-include` Add an include directive to the generated SystemVerilog -* `-sv_verilate` Can be used as either `-sv_verilate run` or - `-sv_verilate compile`. If used Sail will automatically invoke +* `--sv-verilate` Can be used as either `--sv-verilate run` or + `--sv-verilate compile`. If used Sail will automatically invoke https://www.veripool.org/verilator/[verilator] on the generated SystemVerilog -* `-sv_lines` Output SystemVerilog `line directives to aid debugging. +* `--sv-lines` Output SystemVerilog `line directives to aid debugging. -* `-sv_int_size` Set the maximum integer size allowed in the specification. +* `--sv-int-size` Set the maximum integer size allowed in the specification. -* `-sv_bits_size` Bound the maximum bitvector width on the generated SystemVerilog. +* `--sv-bits-size` Bound the maximum bitvector width on the generated SystemVerilog. -* `-sv_specialize` The `-sv_specialize n` option will perform `n` +* `--sv-specialize` The `--sv-specialize n` option will perform `n` rounds of specialisation on the Sail code before generating SystemVerilog. This will make bitvectors more monomorphic, but at the cost of code duplication. The are various other options that control various minutae about the -generated SystemVerilog, see `sail -help` for more details. +generated SystemVerilog, see `sail --help` for more details. <<< @@ -138,10 +134,10 @@ changes to source made by the tool and use at your own risk! Sail supports automatic code formatting similar to tools like `go fmt` or `rustfmt`. This is built into Sail itself, and can be used via the -`-fmt` flag. To format a file `my_file.sail`, we would use the command: +`--fmt` flag. To format a file `my_file.sail`, we would use the command: [source,sh] ---- -sail -fmt my_file.sail +sail --fmt my_file.sail ---- Note that Sail does not attempt to type-check files when formatting @@ -151,7 +147,7 @@ type-check. However, it is perfectly fine to pass multiple files like so: [source,sh] ---- -sail -fmt file1.sail file2.sail file3.sail +sail --fmt file1.sail file2.sail file3.sail ---- The one exception is if a file uses a custom infix operator, then the @@ -161,18 +157,18 @@ uses it. So if `my_file.sail` uses an operator declared in expressions correctly), we would be required to do: [source,sh] ---- -sail -fmt operator.sail my_file.sail +sail --fmt operator.sail my_file.sail ---- This will format both files. If we want to avoid formatting -`operator.sail`, we could either use `-fmt_skip`, like so: +`operator.sail`, we could either use `--fmt-skip`, like so: [source,sh] ---- -sail -fmt_skip operator.sail -fmt operator.sail my_file.sail +sail --fmt-skip operator.sail --fmt operator.sail my_file.sail ---- -or the `-fmt_only` option, like so: +or the `--fmt-only` option, like so: [source,sh] ---- -sail -fmt_only my_file.sail -fmt operator.sail my_file.sail +sail --fmt-only my_file.sail --fmt operator.sail my_file.sail ---- Both of these options can be passed multiple times if required. @@ -182,7 +178,7 @@ as: ---- include::../../test/format/default/config.json[] ---- -which is passed to sail with the `-config` flag. +which is passed to sail with the `--config` flag. The various keys supported under the `"fmt"` key are as follows: @@ -215,10 +211,10 @@ starting Sail with `sail -i`. Sail will still handle any other command line arguments as per usual. To use Sail files within the interpreter they must be passed on the command line as if they were being compiled normally. One can also pass a list of commands to the -interpreter by using the `-is` flag, as +interpreter by using the `--is` flag, as [source,sh] ---- -sail -is +sail --is ---- where `` contains a list of commands. Once inside the interactive mode, a list of available commands can be accessed by @@ -236,27 +232,34 @@ indicated by starting with the letter `d`. * `-help` Print a list of options. -* `-no_warn` Turn off warnings. +* `--no-warn` Turn off warnings. -* `-enum_casts` Allow elements of enumerations to be +* `--enum-casts` Allow elements of enumerations to be automatically cast to numbers. -* `-memo_z3` Memoize calls to the Z3 solver. This can greatly improve +* `--memo-z3` Memoize calls to the Z3 solver. This can greatly improve typechecking times if you are repeatedly typechecking the same specification while developing it. -* `-no_lexp_bounds_check` Turn off bounds checking in the left hand - side of assignments. +* `--no-lexp-bounds-check` Turn off bounds checking in the left hand + side of assignments. This option only exists for some Sail translated + from ASL (as ASL does not do compile-time bounds checking here). -* `-undefined_gen` Generate functions that create undefined values of - user-defined types. Every type `T` will get a `undefined_T` function - created for it. This flag is set automatically by some backends that - want to re-write `undefined`. - -* `-just_check` Force Sail to terminate immediately after +* `--just-check` Force Sail to terminate immediately after typechecking. -* `-dtc_verbose ` Make the typechecker print a +* `--require-version`. Check that the Sail version is newer than the + specified version, if not Sail will print an error and exit with a + non-zero exit code. + +<<< +=== Debug options + +These options are mostly used for debugging the Sail compiler itself. +They are included as they might be useful for those writing custom Sail +plugins. These options are all prefixed with `d`. + +* `--dtc-verbose ` Make the typechecker print a trace of typing judgements. If the verbosity level is 1, then this should only include fairly readable judgements about checking and inference rules. If verbosity is 2 then it will include a large @@ -264,14 +267,20 @@ indicated by starting with the letter `d`. diagnose tricky type-errors, especially if the error message isn't very good. -* `-ddump_tc_ast` Write the typechecked AST to stdout after +* `--ddump-initial-ast` Write the AST out immediately after parsing + and desugaring. + +* `--ddump-tc-ast` Write the typechecked AST to stdout after typechecking -* `-ddump_rewrite_ast ` Write the AST out after each +* `--ddump-side-effects` Print inferred information about function + side effects + +* `--ddump-rewrite-ast ` Write the AST out after each re-writing pass. The output from each pass is placed in a file starting with `prefix`. -* `-dmagic_hash` Allow the `#` symbol in identifiers. It's +* `--dmagic-hash` Allow the `#` symbol in identifiers. It's currently used as a magic symbol to separate generated identifiers from those the user can write, so this option allows for the output of the various other debugging options to be fed back into Sail. The diff --git a/doc/examples/union.sail b/doc/examples/union.sail new file mode 100644 index 000000000..cc1511fbd --- /dev/null +++ b/doc/examples/union.sail @@ -0,0 +1,57 @@ +default Order dec + +$include + +struct rectangle = { + width : int, + height : int, +} + +$span start SHAPE +struct circle = { radius : int } + +union shape = { + Rectangle : rectangle, + Circle : circle, +} +$span end + +val example : unit -> unit + +function example() = { + // Construct a shape using the Rectangle constructor + let r : shape = Rectangle(struct { width = 30, height = 20 }); + + // Construct a shape using the Circle constructor + // Note that we can allow the 'shape' type to be inferred + let c = Circle(struct { radius = 15 }); +} + +$span start EX_UNIT +union example_unit_constructor = { + Foo : (int, string), + Bar : unit, +} + +// Using a constructor with a tuple type +let x1 = Foo(2, "a string") + +// Note that the above is equivalent to +let x2 = Foo((2, "a string")) + +// Using a unit-type constructor +let y1 = Bar() + +// Similarly, equivalent to +let y2 = Bar(()) +$span end + +union shape2 = { + Rectangle2 : { width : int, height : int }, + Circle2 : { radius : int }, +} + +union either('a, 'b) = { + Left : 'a, + Right : 'b, +} diff --git a/doc/manual.html b/doc/manual.html index fe5b0cd15..3eca5140a 100644 --- a/doc/manual.html +++ b/doc/manual.html @@ -2599,6 +2599,7 @@

The Sail instruction-set semantics specification language

  • Automatic formatting (Experimental)
  • Interactive mode
  • Other options
    • +
  • Debug options
  • The Sail Language @@ -2613,14 +2614,36 @@

    The Sail instruction-set semantics specification language

  • The list type
  • Tuples
  • Strings
    • -
  • User-defined types
    • -
  • Pattern matching
    • +
  • User-defined types + +
    • +
  • Pattern matching + +
  • Matching in let and function arguments
  • Type patterns
  • Mutable variables
  • Assignment and l-values
  • Bitfields
    • -
  • Operators
    • +
  • Operators + +
  • Ad-hoc overloading
  • Mappings
  • Sizeof and constraint
    • @@ -3050,17 +3073,13 @@

    Usage

    Sail options

    -

    For command line arguments, by default Sail accepts arguments of -the form ‑long_opt, i.e. leading with a single - and words -separated by _. For those who find this departure from standard -convention distasteful, you can define the SAIL_NEW_CLI environment -variable, and all such options will be formatted as -‑‑long‑opt (short opts like ‑o will remain -unchanged). For backwards compatibility reasons, this default is hard -to change.

    +

    For backwards compatibility reasons, Sail accepts arguments of the +form -long_opt, i.e. leading with a single - and words +separated by _. Such an option will be treated the same as +--long-opt.

    -

    For a list of all options, one can call Sail as sail -help.

    +

    For a list of all options, one can call Sail as sail --help.

    @@ -3107,17 +3126,17 @@

    C compilation

    unless this flag is set.

  • -

    -Oconstant_fold apply constant folding optimisations.

    +

    --Oconstant-fold apply constant folding optimisations.

  • -

    -c_include Supply additional header files to be included in the +

    --c-include Supply additional header files to be included in the generated C.

  • -

    -c_no_main Do not generate a main() function.

    +

    --c-no-main Do not generate a main() function.

  • -

    -static Mark generated C functions as static where possible. This +

    --static Mark generated C functions as static where possible. This is useful for measuring code coverage.

    • @@ -3142,7 +3161,7 @@

    SystemVerilog compilation (Expe
    -

    To compile Sail into SystemVerilog, the -sv option is used. The -o +

    To compile Sail into SystemVerilog, the --sv option is used. The -o option provides a prefix that is used on the various generated files.

    @@ -3151,28 +3170,28 @@

    SystemVerilog compilation (Expe
    • -

      -sv_output_dir Generate all files in the specified directory

      +

      --sv-output-dir Generate all files in the specified directory

    • -

      -sv_include Add an include directive to the generated SystemVerilog

      +

      --sv-include Add an include directive to the generated SystemVerilog

    • -

      -sv_verilate Can be used as either -sv_verilate run or --sv_verilate compile. If used Sail will automatically invoke +

      --sv-verilate Can be used as either --sv-verilate run or +--sv-verilate compile. If used Sail will automatically invoke verilator on the generated SystemVerilog

    • -

      -sv_lines Output SystemVerilog `line directives to aid debugging.

      +

      --sv-lines Output SystemVerilog `line directives to aid debugging.

    • -

      -sv_int_size Set the maximum integer size allowed in the specification.

      +

      --sv-int-size Set the maximum integer size allowed in the specification.

    • -

      -sv_bits_size Bound the maximum bitvector width on the generated SystemVerilog.

      +

      --sv-bits-size Bound the maximum bitvector width on the generated SystemVerilog.

    • -

      -sv_specialize The -sv_specialize n option will perform n +

      --sv-specialize The --sv-specialize n option will perform n rounds of specialisation on the Sail code before generating SystemVerilog. This will make bitvectors more monomorphic, but at the cost of code duplication.

      @@ -3181,7 +3200,7 @@

      SystemVerilog compilation (Expe

    The are various other options that control various minutae about the -generated SystemVerilog, see sail -help for more details.

    +generated SystemVerilog, see sail --help for more details.

    @@ -3203,11 +3222,11 @@

    Automatic formatting (Experimental)<

    Sail supports automatic code formatting similar to tools like go fmt or rustfmt. This is built into Sail itself, and can be used via the --fmt flag. To format a file my_file.sail, we would use the command:

    +--fmt flag. To format a file my_file.sail, we would use the command:

    -
    sail -fmt my_file.sail
    +
    sail --fmt my_file.sail
    @@ -3219,7 +3238,7 @@

    Automatic formatting (Experimental)<

    -
    sail -fmt file1.sail file2.sail file3.sail
    +
    sail --fmt file1.sail file2.sail file3.sail
    @@ -3231,24 +3250,24 @@

    Automatic formatting (Experimental)<

    -
    sail -fmt operator.sail my_file.sail
    +
    sail --fmt operator.sail my_file.sail

    This will format both files. If we want to avoid formatting -operator.sail, we could either use -fmt_skip, like so:

    +operator.sail, we could either use --fmt-skip, like so:

    -
    sail -fmt_skip operator.sail -fmt operator.sail my_file.sail
    +
    sail --fmt-skip operator.sail --fmt operator.sail my_file.sail
    -

    or the -fmt_only option, like so:

    +

    or the --fmt-only option, like so:

    -
    sail -fmt_only my_file.sail -fmt operator.sail my_file.sail
    +
    sail --fmt-only my_file.sail --fmt operator.sail my_file.sail
    @@ -3272,7 +3291,7 @@

    Automatic formatting (Experimental)<

    -

    which is passed to sail with the -config flag.

    +

    which is passed to sail with the --config flag.

    The various keys supported under the "fmt" key are as follows:

    @@ -3317,11 +3336,11 @@

    Interactive mode

    command line arguments as per usual. To use Sail files within the interpreter they must be passed on the command line as if they were being compiled normally. One can also pass a list of commands to the -interpreter by using the -is flag, as

    +interpreter by using the --is flag, as

    -
    sail -is <file>
    +
    sail --is <file>
    @@ -3348,33 +3367,46 @@

    Other options

    -help Print a list of options.

  • -

    -no_warn Turn off warnings.

    +

    --no-warn Turn off warnings.

  • -

    -enum_casts Allow elements of enumerations to be +

    --enum-casts Allow elements of enumerations to be automatically cast to numbers.

  • -

    -memo_z3 Memoize calls to the Z3 solver. This can greatly improve +

    --memo-z3 Memoize calls to the Z3 solver. This can greatly improve typechecking times if you are repeatedly typechecking the same specification while developing it.

  • -

    -no_lexp_bounds_check Turn off bounds checking in the left hand -side of assignments.

    +

    --no-lexp-bounds-check Turn off bounds checking in the left hand +side of assignments. This option only exists for some Sail translated +from ASL (as ASL does not do compile-time bounds checking here).

  • -

    -undefined_gen Generate functions that create undefined values of -user-defined types. Every type T will get a undefined_T function -created for it. This flag is set automatically by some backends that -want to re-write undefined.

    +

    --just-check Force Sail to terminate immediately after +typechecking.

  • -

    -just_check Force Sail to terminate immediately after -typechecking.

    +

    --require-version. Check that the Sail version is newer than the +specified version, if not Sail will print an error and exit with a +non-zero exit code.

    • + +
    +
    + +
    +

    Debug options

    +
    +

    These options are mostly used for debugging the Sail compiler itself. +They are included as they might be useful for those writing custom Sail +plugins. These options are all prefixed with d.

    +
    +
    +
    • -

      -dtc_verbose <verbosity> Make the typechecker print a +

      --dtc-verbose <verbosity> Make the typechecker print a trace of typing judgements. If the verbosity level is 1, then this should only include fairly readable judgements about checking and inference rules. If verbosity is 2 then it will include a large @@ -3383,16 +3415,24 @@

      Other options

      very good.

    • -

      -ddump_tc_ast Write the typechecked AST to stdout after +

      --ddump-initial-ast Write the AST out immediately after parsing +and desugaring.

      +
      • +
    • +

      --ddump-tc-ast Write the typechecked AST to stdout after typechecking

    • -

      -ddump_rewrite_ast <prefix> Write the AST out after each +

      --ddump-side-effects Print inferred information about function +side effects

      +
      • +
    • +

      --ddump-rewrite-ast <prefix> Write the AST out after each re-writing pass. The output from each pass is placed in a file starting with prefix.

    • -

      -dmagic_hash Allow the # symbol in identifiers. It’s +

      --dmagic-hash Allow the # symbol in identifiers. It’s currently used as a magic symbol to separate generated identifiers from those the user can write, so this option allows for the output of the various other debugging options to be fed back into Sail. The @@ -4157,12 +4197,142 @@

      Enums

      generation of these functions entirely.

    +
    +

    Unions

    +
    +

    Structs provide us a way to group multiple pieces of related data, for example

    +
    +
    +
    +
    struct rectangle = {
+    width : int,
+    height : int,
+}
    +
    +
    +
    +

    defines a type rectangle that has both a width and a height. The +other logical way to combine data is if we want to say we have some +data or some other data, like if we wanted to represent a shape that +could be a circle or a rectangle. In Sail, we use a union for this.

    +
    +
    +
    +
    struct circle = { radius : int }
+
+union shape = {
+    Rectangle : rectangle,
+    Circle : circle,
+}
    +
    +
    +
    + + + + + +
    +
    Note
    +    		 +While structs are ubiquitous in programming languages, the +equivalent feature for safely representing disjunctions of types is +often a second-class afterthought or even absent entirely. The +requirement to safely represent disjunctions of types is why C’s +union feature is something different to what we want here, which is +sometimes called tagged unions or variants to distinguish them +from the unsafe C construct. C++ is therefore a good example of a +language where structs are first class, but std::variant is +relegated to a library feature. +
    +
    +
    +

    This defines a type with two constructors Rectangle and Circle. +Constructors are used like functions with a single argument, as so:

    +
    +
    +
    +
    function example() = {
+    // Construct a shape using the Rectangle constructor
+    let r : shape = Rectangle(struct { width = 30, height = 20 });
+
+    // Construct a shape using the Circle constructor
+    // Note that we can allow the 'shape' type to be inferred
+    let c = Circle(struct { radius = 15 });
+}
    +
    +
    +
    +

    To destructure unions, we typically use pattern matching to handle +each case in the union separately. This will be discussed in detail in +Pattern matching.

    +
    +
    +

    Constructors in Sail always have a single argument. If we want a +constructor in a union type to contain no information, then we can use +the unit type. For a constructor with multiple arguments we can use +a tuple type. We provide some syntax sugar that allows writing +constructor applications with either tuple or unit argument types as +if they were functions with multiple arguments or no arguments +respectively.

    +
    +
    +
    +
    union example_unit_constructor = {
+  Foo : (int, string),
+  Bar : unit,
+}
+
+// Using a constructor with a tuple type
+let x1 = Foo(2, "a string")
+
+// Note that the above is equivalent to
+let x2 = Foo((2, "a string"))
+
+// Using a unit-type constructor
+let y1 = Bar()
+
+// Similarly, equivalent to
+let y2 = Bar(())
    +
    +
    +
    +

    In our shape example, we defined rectangle and circle as two +separate structs, but if we wanted we could declare those structs +inline

    +
    +
    +
    +
    union shape2 = {
+    Rectangle2 : { width : int, height : int },
+    Circle2 : { radius : int },
+}
    +
    +
    +
    +

    Behind the scenes, Sail will just generate separate struct +definitions, so we use this type in exactly the same was as we did +previously.

    +
    +
    +

    As with structs, we can define polymorphic union types, like

    +
    +
    +
    +
    union either('a, 'b) = {
+    Left : 'a,
+    Right : 'b,
+}
    +
    +
    +

    Pattern matching

    -

    Like most functional languages, Sail supports pattern matching via the -match keyword. For example:

    +

    Like most functional languages, and an increasing number of imperative +languages like Rust, Sail supports pattern matching via the match +keyword. For example:

    @@ -4674,7 +4844,7 @@

    Mutable variables

    they only exist within the block that declared them.

    -

    Technically, unless the -strict_var option is used Sail also allows +

    Technically, unless the --strict-var option is used Sail also allows mutable variables to be implicitly declared, like so:

    @@ -5645,7 +5815,7 @@

    Modules

    Working with Makefiles

    -

    The -list_files option can be used to list all the files within a +

    The --list-files option can be used to list all the files within a project file, which allows them to be used in a Makefile prerequisite. As an example, to build the module examples in this very manual, we use the rule below to generate documentation indexes (which our @@ -5658,7 +5828,7 @@

    Working with Makefiles

    module_sail_doc/%.json: ../examples/%.sail_project $$(shell sail ../examples/%.sail_project -list_files) mkdir -p module_sail_doc - sail -doc $(addprefix -doc_file ,$(shell sail $< -list_files)) -doc_embed plain -doc_bundle $(notdir $@) -o module_sail_doc $< + sail --doc $(addprefix -doc_file ,$(shell sail $< --list-files)) --doc-embed plain --doc-bundle $(notdir $@) -o module_sail_doc $<
    @@ -6268,7 +6438,7 @@

    References