Add struct and enum sections to manual

doc/asciidoc/Makefile

@@ -15,6 +15,8 @@ SAIL_DOCS += sail_doc/function_pat.json
 SAIL_DOCS += sail_doc/let_var.json
 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 += module_sail_doc/simple_mod.json
 SAIL_DOCS += module_sail_doc/simple_mod_err.error
 SAIL_DOCS += module_sail_doc/cond.sail_project
@@ -29,26 +31,26 @@ all: manual.html manual.pdf
 
 sail_doc/%.json: ../examples/%.sail
  mkdir -p sail_doc
- sail -no_color -doc -doc_file $< -doc_embed plain -doc_bundle $(notdir $@) $< 2> $(basename $@).warning
+ sail --no-color -doc --doc-file $< --doc-embed plain --doc-bundle $(notdir $@) $< 2> $(basename $@).warning
 
 lib_sail_doc/%.json: ../examples/order_dec.sail ../../lib/%.sail
  mkdir -p lib_sail_doc
  mkdir -p lib_sail_doc/concurrency_interface
- sail -doc -doc_file $< -doc_embed plain -doc_bundle $(patsubst lib_sail_doc/%,%,$@) -o lib_sail_doc $<
+ sail --doc --doc-file $< --doc-embed plain --doc-bundle $(patsubst lib_sail_doc/%,%,$@) -o lib_sail_doc $<
 
 .SECONDEXPANSION:
 
-module_sail_doc/%.json: ../examples/%.sail_project $$(shell sail ../examples/%.sail_project -list_files)
+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 $< --all-modules
 
 module_sail_doc/%.error: ../examples/%.sail_project $$(shell sail ../examples/%.sail_project -list_files)
  mkdir -p module_sail_doc
- -sail -no_color $< 2> $@
+ -sail --no-color $< 2> $@
 
 module_sail_doc/%.sail_project: ../examples/%.sail_project
  mkdir -p module_sail_doc
- sail $< -just_parse_project 1>/dev/null
+ sail $< --just-parse-project 1>/dev/null
  cp $< $@
 
 ordering-tikz.pdf: latex_figures/ordering.tex

doc/asciidoc/introduction.adoc

@@ -9,14 +9,14 @@ They vary in how precise that pseudocode is: in some it is just
 suggestive, while in others it is close to a complete description of
 the envelope of architecturally allowed behaviour for sequential code.
 
-For x86{blank}cite:[Intel61], the Intel pseudocode is just suggestive,
-with embedded prose, while the AMD descriptions{blank}cite:[AMD_3_21]
-are prose alone. For IBM Power{blank}cite:[Power3.0B], there is
+For x86 cite:[Intel61], the Intel pseudocode is just suggestive,
+with embedded prose, while the AMD descriptions cite:[AMD_3_21]
+are prose alone. For IBM Power cite:[Power3.0B], there is
 detailed pseudocode which has recently become
-machine-processed{blank}cite:[Leighton21]. For
-Arm{blank}cite:[armarmv8], there is detailed pseudocode, which has
-recently become machine-processed{blank}cite:[Reid16]. For
-MIPS{blank}cite:[MIPS64-II,MIPS64-III] there is also reasonably detailed
+machine-processed cite:[Leighton21]. For
+Arm cite:[armarmv8], there is detailed pseudocode, which has
+recently become machine-processed cite:[Reid16]. For
+MIPS cite:[MIPS64-II,MIPS64-III] there is also reasonably detailed
 pseudocode.
 
 Sail is intended:
@@ -30,7 +30,7 @@ Sail is intended:
 * To expose the structure needed to combine the sequential ISA
  semantics with the relaxed-memory concurrency models we have
  developed;
- 
+
 * To provide an expressive type system that can statically check the
  bitvector length and indexing computation that arises in these
  specifications, to detect errors and to support code generation,
@@ -57,7 +57,7 @@ and generate:
 * An internal representation of the fully type-annotated
  definition (a deep embedding of the definition) in a form that can
  be executed by the Sail interpreter. These are both expressed in
- Lem{blank}cite:[Lem-icfp2014,Lemcode], a language of type, function, and
+ Lem cite:[Lem-icfp2014,Lemcode], a language of type, function, and
  relation definitions that can be compiled into OCaml and various
  theorem provers. The Sail interpreter can also be used to analyse
  instruction definitions (or partially executed instructions) to
@@ -102,13 +102,13 @@ machine-readable public v8.3 ASL specification footnote:[ARM v8-A
 ARM's specification.
 
 The MIPS model is hand-written based on the MIPS64 manual version
-2.5{blank}cite:[MIPS64-II,MIPS64-III],
+2.5 cite:[MIPS64-II,MIPS64-III],
 but covering only the features in the BERI hardware
-reference{blank}cite:[UCAM-CL-TR-868],
-which in turn drew on MIPS4000 and MIPS32{blank}cite:[MIPS4000,MIPS32-I].
+reference cite:[UCAM-CL-TR-868],
+which in turn drew on MIPS4000 and MIPS32 cite:[MIPS4000,MIPS32-I].
 
 The CHERI model is based on that and the CHERI ISA reference manual
-version{nbsp}5{blank}cite:[UCAM-CL-TR-891]. These two are both
+version{nbsp}5 cite:[UCAM-CL-TR-891]. These two are both
 principally by Norton-Wright; they cover all basic user
 and kernel mode MIPS features sufficient to boot FreeBSD, including a
 TLB, exceptions and a basic UART for console interaction. ISA

doc/asciidoc/language.adoc

@@ -358,6 +358,87 @@ Multi-line strings can be written by escaping the newline character at the end o
 
 sail::multi_line[from=strings,type=function,part=body,dedent]
 
+=== User-defined types
+
+Sail supports various kinds of user-defined types: _structs_,
+_unions_, and _enums_.
+
+==== Structs
+:struct: sail_doc/struct.json
+
+Like in C, structs are used to hold multiple values. Structs are
+created using the `struct` keyword followed by the name of the struct.
+The data the struct contains is then defined following the `=` symbol.
+Each piece of data stored in a struct is called a `field`, and each is
+given a unique name that identifies that piece of data, and can have a
+different type.
+
+The following example struct defines three fields. The first contains
+a bitvector of length 5 and is called `field1`. The second, `field2`
+contains an integer. The third, `field3` contains a string.
+
+sail::My_struct[from=struct,type=type]
+
+We can then construct struct values by using the `struct` keyword and
+providing values for all the fields. The individual fields can be
+accessed using the `.` operator. If the struct is mutable, we can also
+the `.` operator on the left-hand side of an assignment to assign to
+the struct field. For immutable structs, we can update them using the
+`with` keyword, which will create a new struct value with some fields
+changed.
+
+sail::example[from=struct,part=body,dedent]
+
+Structs can have user defined type parameters. The following example
+has an integer parameter `'n` and a type parameter `'a`.
+
+sail::My_other_struct[from=struct,type=type]
+
+The struct can then be instantiated with any length of bitvector for
+the `a_bitvector` field, and any data type for the `something` field,
+including another struct like the `My_struct` type we defined earlier.
+
+sail::poly_example[from=struct,part=body,dedent]
+
+==== Enums
+:enum: sail_doc/enum.json
+
+Sail enumerations are also much like their C counterparts. An enum is
+declared using the `enum` keyword followed by the name of the
+enumeration type. The members of the enumeration are specified as a
+comma-separated list of identifiers between curly braces, like so:
+
+sail::My_enum[from=enum,type=type]
+
+The above style is best when there are a lot of elements in the
+enumeration. We allow enums to be defined in a style similar to
+Haskell, where the identifiers are separated by a vertical bar `|`
+character, like so:
+
+sail::My_short_enum[from=enum,type=type]
+
+This style is better when the enumeration is short and has few
+constructors, however specification authors may prefer to use the
+first style exclusively for consistency.
+
+Sail will automatically generate functions for converting enumeration
+members into numbers, starting with 0 for the first element of the
+enumeration.
+
+sail::enum_example1[from=enum,dedent]
+
+Likewise, there is a function for converting the other way
+
+sail::enum_example2[from=enum,dedent]
+
+If the names of the generated functions are not ideal, then custom
+names can be provided using the `enum_number_conversions` attribute.
+
+sail::ENUM_CONV[from=enum,type=span]
+
+The `no_enum_number_conversions` attribute can be used to disable the
+generation of these functions entirely.
+
 === Pattern matching
 :pattern-match: sail_doc/pattern_matching.json
 :cannot-wildcard: sail_doc/cannot_wildcard.json

doc/examples/enum.sail

@@ -1,7 +1,41 @@
-enum Foo = Bar | Baz | quux
+default Order dec
 
-enum Foo = {
+$include <prelude.sail>
+$include <generic_equality.sail>
+
+enum My_enum = {
+ Foo,
  Bar,
  Baz,
- quux
-}
+ Quux,
+}
+
+enum My_short_enum = A | B | C
+
+val enum_example1 : unit -> unit
+
+function enum_example1() = {
+ assert(num_of_My_enum(Foo) == 0);
+ assert(num_of_My_enum(Bar) == 1);
+ assert(num_of_My_enum(Baz) == 2);
+ assert(num_of_My_enum(Quux) == 3);
+}
+
+val enum_example2 : unit -> unit
+
+function enum_example2() = {
+ assert(My_enum_of_num(0) == Foo)
+}
+
+$span start ENUM_CONV
+$[enum_number_conversions { from_enum = to_number, to_enum = from_number }]
+enum Another_enum = {
+ Member1,
+ Member2,
+}
+
+function custom_conversions() -> unit = {
+ assert(to_number(Member1) == 0);
+ assert(from_number(1) == Member2);
+}
+$span end

doc/examples/struct.sail

@@ -1,5 +1,73 @@
-struct Foo = {
- bar : vector(4, dec, bit),
- baz : int,
- quux : range(0, 9)
-}
+default Order dec
+
+$include <prelude.sail>
+$include <generic_equality.sail>
+
+struct My_struct = {
+ field1 : bits(5),
+ field2 : int,
+ field3 : string,
+}
+
+val example : unit -> unit
+
+function example() = {
+ // Struct literals are created with the struct keyword
+ let s : My_struct = struct {
+ field1 = 0b11111,
+ field2 = 5,
+ field3 = "test",
+ };
+
+ // Accessing a struct field, prints "field1 is 0b11111"
+ print_bits("field1 is ", s.field1);
+
+ // Updating struct fields, creating a new struct variable s2
+ var s2 = { s with field1 = 0b00000, field3 = "a string" };
+
+ // Prints "field1 is 0b00000"
+ print_bits("field1 is ", s2.field1);
+ // Prints "field2 is 5", as field2 was taken from 's' and not modified
+ print_int("field2 is ", s2.field2);
+
+ // Because s2 is mutable we can assign to it
+ s2.field3 = "some string";
+ // Prints "some string"
+ print_endline(s2.field3)
+}
+
+struct My_other_struct('n : Int, 'a : Type) = {
+ a_bitvector : bits('n),
+ something : 'a
+}
+
+val poly_example : unit -> unit
+
+function poly_example() = {
+ var s3 : My_other_struct(2, string) = struct {
+ a_bitvector = 0b00,
+ something = "a string"
+ };
+
+ var s4 : My_other_struct(32, My_struct) = struct {
+ a_bitvector = 0xFFFF_FFFF,
+ something = struct {
+ field1 = 0b11111,
+ field2 = 6,
+ field3 = "nested structs!",
+ }
+ };
+
+ s3.a_bitvector = 0b11;
+
+ // Note that once created, we cannot change a variable's type, so the following is forbidden:
+ // s3.a_bitvector = 0xFFFF_FFFF;
+
+ // Changing the type is also forbidden in a with expression:
+ // let s4 : My_other_struct(32, string) = { s3 with a_bitvector = 0xFFFF_FFFF };
+
+ // If structs are nested, then field accesses can also be nested
+ print_endline(s4.something.field3);
+ // and assignments
+ s4.something.field3 = "another string"
+}