Add support for the Sail language (#7304)

This adds support for the [Sail
language](https://github.com/rems-project/sail) - a DSL for defining
ISAs.

It's not quite ready but I need some help. These are the main remaining
issues:

1. When you "link to binary" it does disassemble the binary properly,
but the syntax highlighting and line numbers are broken.


![image](https://github.com/user-attachments/assets/2f4fe12c-49b4-4b26-9cb0-7e1666a7b3a2)

2. If you try to execute the code without a `function main() -> unit =
...` then it gives this error in the compiler output:

```
Internal Compiler Explorer error: Error: spawn /tmp/compiler-explorer-compiler2025025-31052-c8gern.pf8t/model.c EACCES
    at ChildProcess._handle.onexit (node:internal/child_process:285:19)
    at onErrorNT (node:internal/child_process:483:16)
    at process.processTicksAndRejections (node:internal/process/task_queues:82:21)
Compiler returned: -1
```

This is weird - it should give a linker with an undefined reference to
`zmain`.

3. Sail compiles to C, and then I added extra steps to compile that to
binary (if you select `Execute the code`), but as you can see I had to
move the binary back over the C file, so in this case `model.c` is
actually an ELF file. It works but that seems very weird. There is a
`getExecutableFilename()` method I could override, but doing that seems
to make it even more confused.

4. I also had to have a fake flag for `binary` because the `filters`
don't seem to get set correctly when passed to `runCompiler()`. E.g.
`buildExecutable()` doesn't pass them at all. Not sure what is going on
there. Seems to work though.

Any help appreciated!

PS: Sail is a cool language. It has lightweight dependent type for
integers and bit vectors, which I haven't demonstrated in the examples
yet, but they're neat.

---------

Co-authored-by: Matt Godbolt <matt@godbolt.org>

etc/config/sail.amazon.properties

@@ -0,0 +1,22 @@
+compilers=&sail
+
+defaultCompiler=sail_0_18
+
+objdumper=/opt/compiler-explorer/gcc-14.2.0/bin/objdump
+# The C compiler used to compile the generated .c files to a binary.
+cCompiler=/opt/compiler-explorer/gcc-14.2.0/bin/gcc
+
+group.sail.groupName=Sail
+group.sail.compilers=sail_0_18
+group.sail.isSemVer=true
+group.sail.baseName=sail
+
+group.sail.name=Sail
+group.sail.exe=sail
+group.sail.versionFlag=--version
+group.sail.supportsBinary=true
+group.sail.supportsExecute=true
+group.sail.compilerType=sail
+
+compiler.sail_0_18.semver=0.18
+compiler.sail_0_18.exe=/opt/compiler-explorer/sail-0.18/bin/sail

etc/config/sail.defaults.properties

@@ -0,0 +1,11 @@
+compilers=sail
+
+cCompiler=gcc
+
+compiler.sail.name=Sail
+compiler.sail.exe=sail
+compiler.sail.versionFlag=--version
+compiler.sail.supportsBinary=true
+compiler.sail.supportsExecute=true
+compiler.sail.compilerType=sail
+compiler.sail.objdumper=objdump

examples/sail/basics.sail

@@ -0,0 +1,113 @@
+// This example introduces most basic features of Sail.
+/* Comments are C-style. /* Blocks comments can be nested. */ */
+
+// Sail supports configurable indexing endianness. Dec is the most common
+// option. It must be declared globally.
+default Order dec
+
+// C-style includes are supported. `prelude.sail` is from the Sail standard
+// library and includes some common things.
+$include <prelude.sail>
+
+// Global mutable variables are introduced with `register`.
+// They must include a type (int) and can include an initialiser (= 0).
+// `int` is the type for all integers (any size, like in Python).
+// Try changing this to 10000000000000000000000000000000000000000000000000.
+register my_global_int : int = 0
+
+// `nat` is the type for natural numbers (>= 0). Try changing the 3 to -3.
+register not_negative : nat = 3
+
+// There's also a `range(M, N)` type for integers in [M, N] (inclusive).
+// Try changing this to 0
+register month : range(1, 12) = 1
+
+// Immutable globals variables are declared with let.
+// Real numbers are supported, using libgmp (which represents them as
+// arbitrary length integer fractions). Although supported, they are very
+// rarely used in Sail code.
+let pi : real = 3.141
+
+// This is a simple function. Sail is expression-based like Rust, OCaml,
+// Haskell, etc. Braces are not required for function bodies if they are
+// a single expression.
+function add_ints(a : int, b : int) -> int = a + b
+
+// As usual in expression-based languages, if and match are also expressions.
+function max1(a : int, b : int) -> int = if a > b then a else b
+
+// You can use traditional imperative forms too but it isn't recommended.
+function max2(a : int, b : int) -> int = {
+    if a > b then {
+        return a;
+    } else {
+        return b;
+    }
+}
+
+// It has standard ML/Rust style `match`.
+function month_name(month : range(1, 12)) -> string =
+    match month {
+        1 => "Jan",
+        2 => "Feb",
+        // Alternate patterns are not yet supported.
+        // 3 | 4 => "March or April",
+        // _ is a wildcard.
+        _ => "Whatever",
+    }
+
+// You can define a `main()` function which will be compiled to `zmain()` in C.
+// The name mangling system for C is Z-encoding which basically double all
+// z's and prepends a z. E.g. size -> zsizze
+//
+// Main returns `unit` which is like a 0-length tuple. It's used in places you
+// might use `void` in C. Unlike `void` you can make a value of `unit` by writing
+// `()`.
+//
+// Sail will optionally generate a C `main()` function that calls `zmain()`
+// (this code).
+function main() -> unit = {
+    // The standard print function.
+    print_endline("Hello world");
+
+    // `let` introduces immutable variables.
+    let a : int = 5;
+    // They can be shadowed with the same name.
+    let a : string = "5";
+    // Type annotations are not always required - often they can be inferred.
+    let a = 5;
+    // Because they are immutable you cannot do this:
+    a = 6;
+
+    // Mutable variables use `var`.
+    var a : int = 5;
+    // This is now ok.
+    a = 6;
+
+    // One small gotcha is that the inferred type for 5 is int(5). So this
+    var a = 5;
+    // is equivalent to this
+    var a : int(5) = 5;
+    // And because its type is literally the number 5, you can't assign
+    // any other numbers to it.
+    // a = 6; // compile error
+}
+
+// Being aimed at ISA specifications, Sail has very good support for bit vectors.
+function reverse_endianness(word : bits(16)) -> bits(16) =
+    // @ means concatenation. Since we declared `default Order dec` all
+    // of these indices and concatenations happen in Little Endian notational
+    // order. This doesn't mean that the underlying data is Little Endian though.
+    //
+    // .. selects a bit range. This is inclusive. Currently there is no
+    // half-open syntax (8 >.. 0) but this is planned.
+    word[7 .. 0] @ word[15 .. 8]
+
+// Sail has an advanced type system for bit vectors and integers which means
+// they can almost always be checked at compile time.
+//
+// Try changing 7 to 8 here.
+function lowest_byte(word : bits(16)) -> bits(8) = word[7 .. 0]
+
+// Check the other examples for more features. Or see the Sail manual here:
+// https://alasdair.github.io/manual.html

examples/sail/bitfields.sail

@@ -0,0 +1,35 @@
+default Order dec
+
+$include <prelude.sail>
+$include <vector.sail>
+
+// Bitfields are useful for registers. You can take an underlying bitvector
+// and allow naming bits in them.
+
+bitfield Status : bits(32) = {
+    U : 31,
+    // Not all bits need to have a corresponding field, and fields can overlap.
+    A : 0,
+    lowest_byte : 7 .. 0,
+    upper_byte : 31 .. 24,
+}
+
+function main() -> unit = {
+    // To create a new bitfield, use Mk_<name>.
+    var status = Mk_Status(0x00000000);
+
+    // You can update mutable variables (including `register`s) imperatively:
+    status[lowest_byte] = status[upper_byte];
+
+    // You can access the underlying bitvector via the special field `bits`.
+    status.bits = 0x11223344;
+
+    // You can also do functional-style immutable updates.
+    let status = [
+        status with
+        U = 0b1,
+        lowest_byte = 0xFF,
+    ];
+
+    print_endline(bits_str(status.bits));
+}

examples/sail/bitvectors.sail

@@ -0,0 +1,48 @@
+default Order dec
+
+$include <prelude.sail>
+$include <vector.sail>
+
+// Sail has excellent support for bit vectors. These have the type `bits(N)`.
+let status : bits(32) = 0x11223344
+
+// Bit vector literals are written 0x.. or 0b...
+// Leading zeros are significant - the affect the size of the literal.
+// This is ok:
+register byte0 : bits(8) = 0x01
+// This is an error:
+// register byte1 : bits(8) = 0x1
+
+function main() -> unit = {
+    // @ means concatenation. With 'default Order dec' concatenation is written
+    // in Big Endian order.
+    assert(0x12 @ 0x34 == 0x1234);
+
+    // Individual bits or ranges of bits can be accessed like this.
+    // Note that the range is inclusive.
+    assert(status[0] == bitzero);
+    assert(status[7 .. 0] == 0x44);
+
+    // You can update mutable bit vectors like this:
+    byte0[3 .. 0] = 0b1100;
+    // Or in immutable function style:
+    let byte2 = [
+        byte0 with
+        3 .. 0 = 0xA,
+    ];
+
+    // You can convert a bit vector to a string with `bits_str()`. If it is
+    // a multiple of 4 bits it will be printed in hex, otherwise binary.
+    print_endline(bits_str(byte2[2 .. 0]));
+
+    // Pattern matching also supports bit vectors.
+    match byte2 {
+        upper @ 0b010 => {
+            print_endline(bits_str(upper));
+        },
+        0b10 @ lower => {
+            print_endline(bits_str(lower));
+        },
+        _ => (),
+    };
+}

examples/sail/default.sail

@@ -0,0 +1,9 @@
+default Order dec
+
+$include <prelude.sail>
+
+function main() -> unit = {
+    print_endline("Hello world!");
+}
+
+// See the examples for a brief introduction to Sail. Start with `basics.sail`.

examples/sail/match.sail

@@ -0,0 +1,52 @@
+default Order dec
+
+$include <option.sail>
+$include <string.sail>
+
+// Sail has pattern matching similar to Rust, OCaml and other functional languages.
+// A notable difference is that it doesn't support combining identical branches.
+
+function suit_name(suit : range(0, 3)) -> string =
+    match suit {
+        0 => "hearts",
+        1 => "diamonds",
+        2 => "clubs",
+        3 => "spaces",
+    }
+
+// _ is a wildcard
+
+function map_add(a : option(int), b : option(int)) -> option(int) =
+    match (a, b) {
+        (Some(a), Some(b)) => Some(a + b),
+        _ => None(),
+    }
+
+// Sail copies a minor footgun from other functional languages.
+
+function ordinal(x : nat) -> string =
+    match x {
+        0 => "zeroth",
+        1 => "first",
+        2 => "second",
+        3 => "third",
+        other => concat_str(dec_str(other), "th"),
+    }
+
+// Here `other` creates a new variable bound to `x`.
+// Unfortunately it can catch you out. The following code appears correct and
+// will compile (with warnings), but actually the function always returns 2.
+// Rust and OCaml also suffer from this flaw.
+
+let ONE = 1
+let TWO = 2
+let THREE = 3
+
+function add_one(x : range(1, 3)) -> range(2, 4) =
+    match x {
+        ONE => 2,
+        TWO => 3,
+        THREE => 4,
+    }
+
+function main() -> unit = ()

examples/sail/max_array.sail

@@ -0,0 +1,21 @@
+default Order dec
+
+$include <prelude.sail>
+$include <vector.sail>
+
+// This is generic over all fixed-length vectors. They are not dynamically sized.
+function max_array forall 'n . (x : vector('n, int), y : vector('n, int)) -> vector('n, int) = {
+    // vector_init() copies the value to all elements.
+    var m : vector('n, int) = vector_init(0);
+    foreach (i from 0 to ('n - 1)) {
+        m[i] = if x[i] > y[i] then x[i] else y[i];
+    };
+    m
+}
+
+function main() -> unit = {
+    let m = max_array([1, 2, 3], [3, 2, 1]);
+    foreach (i from 0 to (length(m) - 1)) {
+        print_endline(dec_str(m[i]));
+    }
+}

examples/sail/sum_over_array.sail

@@ -0,0 +1,37 @@
+default Order dec
+
+$include <prelude.sail>
+$include <vector.sail>
+
+// This is generic over all fixed-length vectors. `input` is not
+// dynamically sized.
+function sum_array forall 'n . (input : vector('n, int)) -> int = {
+    // Type must be explicitly declared as `int`. If you leave
+    // that out the type will be inferred as `int(0)` and it
+    // can only contain the value 0.
+    var total : int = 0;
+    foreach (i from 0 to (length(input) - 1)) {
+        // You can easily add `+=` operators - Sail has good
+        // support for operator overloading - but it isn't
+        // there by default.
+        total = total + input[i];
+    };
+    total
+}
+
+// You can also use functional style lists, but these are
+// not supported by all backends.
+function sum_array_fp (input : list(int)) -> int =
+    match input {
+        // Empty list. List literals are with [| ... |].
+        [| |] => 0,
+        // Single element.
+        [| el |] => el,
+        // More than one element.
+        head :: tail => head + sum_array_fp(tail),
+    }
+
+function main() -> unit = {
+    print_endline(concat_str("Sum of [1, 2, 3] is ", dec_str(sum_array([1 : int, 2, 3]))));
+    print_endline(concat_str("Sum of [1, 2, 3] is ", dec_str(sum_array_fp([| 1, 2, 3 |]))));
+}

examples/sail/types.sail

@@ -0,0 +1,65 @@
+default Order dec
+
+$include <prelude.sail>
+$include <result.sail>
+$include <vector.sail>
+
+// Basic types are:
+
+// Any integer, limited only by your computer's memory!
+let a : int = 1000000000000000000000000000000000000000000000000000000000000000
+
+// Any natural number (non-negative integer).
+let b : nat = 1000000000000000000000000000000000000000000000000000000000000000
+
+// An inclusive range of integers.
+let c : range(1, 6) = 3
+
+// Strings. Sail only has very basic string support, mainly for logging and
+// assembly/disassembly support.
+let d : string = "hello"
+
+// Boolean
+let e : bool = false
+
+// Unit (like an empty tuple; roughly equivalent to 'void').
+let f : unit = ()
+
+// Bit vector. Note that bit-vector literals are written in hex or binary
+// and leading zeros are significant! 0xF is a 4-bit bitvector, but 0x0F is
+// an 8-bit bitvector. Try changing this to 0xF or 0b1010101.
+let g : bits(8) = 0x0F
+
+// More complex types are:
+
+// Standard functional option and result types.
+let h : option(int) = Some(5)
+let i : option(nat) = None()
+
+let j : result(int, unit) = Ok(5)
+let k : result(int, unit) = Err(())
+
+// Fixed-length vectors.
+let l : vector(4, int) = [1, 2, 3, 4]
+
+// Dynamically sized linked lists.
+let m : list(int) = [|1, 2, 3, 4|]
+
+// Custom enum, union and struct types are supported.
+
+// Enums are not namespaced; so you refer to `Red` directly, not `Primary::Red`.
+enum Primary = { Red, Green, Blue }
+
+// Unions are tagged (same as `enum` in Rust), and decoded using `match`.
+union Instruction = {
+    FullSize   : bits(32),
+    Compressed : bits(16),
+}
+
+struct ExecutionStep = {
+    pc          : bits(32),
+    instruction : Instruction,
+    retired     : bool,
+}
+
+function main() -> unit = ()

lib/compilers/_all.ts

@@ -132,6 +132,7 @@ export {RustCompiler} from './rust.js';
 export {RustcCgGCCCompiler} from './rustc-cg-gcc.js';
 export {SPIRVCompiler} from './spirv.js';
 export {SPIRVToolsCompiler} from './spirv-tools.js';
+export {SailCompiler} from './sail.js';
 export {ScalaCompiler} from './scala.js';
 export {SdccCompiler} from './sdcc.js';
 export {SlangCompiler} from './slang.js';

lib/compilers/sail.ts

@@ -0,0 +1,176 @@
+// Copyright (c) 2025, Compiler Explorer Authors
+// All rights reserved.
+//
+// Redistribution and use in source and binary forms, with or without
+// modification, are permitted provided that the following conditions are met:
+//
+//     * Redistributions of source code must retain the above copyright notice,
+//       this list of conditions and the following disclaimer.
+//     * Redistributions in binary form must reproduce the above copyright
+//       notice, this list of conditions and the following disclaimer in the
+//       documentation and/or other materials provided with the distribution.
+//
+// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+// AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+// IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+// ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
+// LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+// CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+// SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+// INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+// CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+// ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+// POSSIBILITY OF SUCH DAMAGE.
+
+import path from 'node:path';
+import fs from 'fs-extra';
+
+import {CompilationResult, ExecutionOptionsWithEnv} from '../../types/compilation/compilation.interfaces.js';
+import type {PreliminaryCompilerInfo} from '../../types/compiler.interfaces.js';
+import type {ParseFiltersAndOutputOptions} from '../../types/features/filters.interfaces.js';
+import {SelectedLibraryVersion} from '../../types/libraries/libraries.interfaces.js';
+import {BaseCompiler} from '../base-compiler.js';
+import {CompilationEnvironment} from '../compilation-env.js';
+
+export class SailCompiler extends BaseCompiler {
+    // Path to C compiler to use to compile generated C code to binary.
+    private readonly cCompiler: string;
+
+    static get key() {
+        return 'sail';
+    }
+
+    constructor(info: PreliminaryCompilerInfo, env: CompilationEnvironment) {
+        super(info, env);
+
+        this.outputFilebase = 'model';
+        this.cCompiler = this.compilerProps<string>('cCompiler');
+        console.assert(this.cCompiler !== undefined, 'cCompiler not set for Sail compiler');
+    }
+
+    override optionsForFilter(filters: ParseFiltersAndOutputOptions, outputFilename: any) {
+        // Target C backend (and override the default C options, -g etc.).
+        return ['-c'];
+    }
+
+    override async runCompiler(
+        compiler: string,
+        options: string[],
+        inputFilename: string,
+        execOptions: ExecutionOptionsWithEnv,
+        filters?: ParseFiltersAndOutputOptions,
+    ): Promise<CompilationResult> {
+        if (!execOptions) {
+            execOptions = this.getDefaultExecOptions();
+        }
+
+        const tmpDir = path.dirname(inputFilename);
+
+        if (!execOptions.customCwd) {
+            execOptions.customCwd = tmpDir;
+        }
+
+        const fullResult: CompilationResult = {
+            code: 0,
+            timedOut: false,
+            stdout: [],
+            stderr: [],
+            buildsteps: [],
+            inputFilename,
+        };
+
+        const sailResult = await this.doBuildstepAndAddToResult(
+            fullResult,
+            'Sail to C',
+            compiler,
+            [...options, '-o', this.outputFilebase],
+            execOptions,
+        );
+
+        const binary = filters?.binary === true;
+
+        if (sailResult.code !== 0 || !binary) {
+            return fullResult;
+        }
+
+        const outputFilenameC = this.getOutputFilename(tmpDir, this.outputFilebase);
+        const outputFilenameExe = outputFilenameC + '.exe';
+
+        fullResult.executableFilename = outputFilenameExe;
+
+        // Query the sail compiler via `sail -dir` to find out where the
+        // C runtime files are (`sail.c` etc).
+        const sailDirResult = await this.doBuildstepAndAddToResult(
+            fullResult,
+            'Get Sail dir',
+            compiler,
+            ['-dir'],
+            execOptions,
+        );
+
+        if (sailDirResult.code !== 0) {
+            return fullResult;
+        }
+
+        const sailDir = sailDirResult.stdout
+            .map(line => line.text)
+            .join('\n')
+            .trim();
+
+        // Now compile the C file to an executable.
+        const compileResult = await this.doBuildstepAndAddToResult(
+            fullResult,
+            'C to binary',
+            this.cCompiler,
+            [
+                outputFilenameC,
+                // Sail C support files.
+                '-I',
+                `${sailDir}/lib`,
+                `${sailDir}/lib/elf.c`,
+                `${sailDir}/lib/rts.c`,
+                `${sailDir}/lib/sail.c`,
+                `${sailDir}/lib/sail_failure.c`,
+                // Support for .elf.gz files. This has been removed in Sail 0.19
+                // so it isn't needed for future versions.
+                '-lz',
+                // For arbitrary precision integer types.
+                '-lgmp',
+                // Enable optimisations so the assembly isn't hilariously verbose.
+                // Ideally this would be user configurable but we'd need
+                // something like `-Wl,..` to pass options through Sail to
+                // here and that doesn't really exist.
+                '-O',
+                '-o',
+                outputFilenameExe,
+            ],
+            execOptions,
+        );
+
+        // This is weird, but as far as I can tell CE expects the same
+        // output file name when compiling to IR (C in this case)
+        // and when compiling to a binary. If you don't do this it
+        // tries to do nonsensical things like objdumping the C, so we
+        // copy the binary back over the C file.
+        if (compileResult.code === 0 && (await fs.pathExists(outputFilenameExe))) {
+            console.log(`Copying ${outputFilenameExe} to ${outputFilenameC}`);
+            await fs.copyFile(outputFilenameExe, outputFilenameC);
+        }
+
+        return fullResult;
+    }
+
+    override getOutputFilename(dirPath: string, outputFilebase: string, key?: any): string {
+        return path.join(dirPath, `${outputFilebase}.c`);
+    }
+
+    override getLibLinkInfo(
+        filters: ParseFiltersAndOutputOptions,
+        libraries: SelectedLibraryVersion[],
+        toolchainPath: string,
+        dirPath: string,
+    ) {
+        // Prevent any library linking flags from being passed to Sail during compilation.
+        return {libLinks: [], libPathsAsFlags: [], staticLibLinks: []};
+    }
+}

lib/languages.ts

@@ -738,6 +738,17 @@ const definitions: Record<LanguageKey, LanguageDefinition> = {
         monacoDisassembly: null,
         digitSeparator: '_',
     },
+    sail: {
+        name: 'Sail',
+        monaco: 'sail',
+        extensions: ['.sail'],
+        alias: [],
+        logoUrl: 'sail.svg',
+        logoUrlDark: null,
+        formatter: null,
+        previewFilter: null,
+        monacoDisassembly: null,
+    },
     snowball: {
         name: 'Snowball',
         monaco: 'swift',

static/modes/_all.ts

@@ -60,6 +60,7 @@ import './ocaml-mode';
 import './odin-mode';
 import './openclc-mode';
 import './ptx-mode';
+import './sail-mode';
 import './slang-mode';
 import './spice-mode';
 import './spirv-mode';

static/modes/sail-mode.ts

@@ -0,0 +1,225 @@
+// Copyright (c) 2025, Compiler Explorer Authors
+// All rights reserved.
+//
+// Redistribution and use in source and binary forms, with or without
+// modification, are permitted provided that the following conditions are met:
+//
+//     * Redistributions of source code must retain the above copyright notice,
+//       this list of conditions and the following disclaimer.
+//     * Redistributions in binary form must reproduce the above copyright
+//       notice, this list of conditions and the following disclaimer in the
+//       documentation and/or other materials provided with the distribution.
+//
+// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+// AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+// IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+// ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
+// LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+// CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+// SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+// INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+// CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+// ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+// POSSIBILITY OF SUCH DAMAGE.
+
+import * as monaco from 'monaco-editor';
+
+function definition(): monaco.languages.IMonarchLanguage {
+    return {
+        keywords: [
+            'and',
+            'as',
+            'assert',
+            'backwards',
+            'barr',
+            'bitfield',
+            'bitone',
+            'bitzero',
+            'Bool',
+            'by',
+            'cast',
+            'catch',
+            'clause',
+            'config',
+            'configuration',
+            'constant',
+            'constraint',
+            'dec',
+            'default',
+            'depend',
+            'do',
+            'eamem',
+            'effect',
+            'else',
+            'end',
+            'enum',
+            'escape',
+            'exmem',
+            'forall',
+            'foreach',
+            'forwards',
+            'from',
+            'function',
+            'if',
+            'implicit',
+            'impure',
+            'in',
+            'inc',
+            'infix',
+            'infixl',
+            'infixr',
+            'Int',
+            'let',
+            'mapping',
+            'match',
+            'newtype',
+            'nondet',
+            'operator',
+            'Order',
+            'overload',
+            'pure',
+            'ref',
+            'register',
+            'repeat',
+            'return',
+            'rmem',
+            'rmemt',
+            'rreg',
+            'scattered',
+            'sizeof',
+            'struct',
+            'then',
+            'throw',
+            'to',
+            'try',
+            'type',
+            'Type',
+            'undef',
+            'undefined',
+            'union',
+            'unspec',
+            'until',
+            'val',
+            'var',
+            'where',
+            'while',
+            'with',
+            'wmem',
+            'wmv',
+            'wmvt',
+            'wreg',
+        ],
+
+        types: [
+            'vector',
+            'bitvector',
+            'int',
+            'nat',
+            'atom',
+            'range',
+            'unit',
+            'bit',
+            'real',
+            'list',
+            'bool',
+            'string',
+            'bits',
+            'option',
+        ],
+
+        identifier: "[a-zA-Z?_][a-zA-Z?0-9_'#]*",
+
+        // String escape sequences. \\, \", \', \n, \t, \b, \r, \<newline>
+        // Or hex/dec: \xHHH, \DD
+        string_escapes: /\\(?:[\\"'ntbr]|$|x[0-9A-Fa-f]{2}|[0-9]{3})/,
+
+        tokenizer: {
+            root: [
+                // Whitespace.
+                {include: '@whitespace'},
+
+                // Identifiers and keywords.
+                [
+                    /@identifier/,
+                    {
+                        cases: {
+                            '@types': 'type',
+                            '@keywords': 'keyword',
+                            '@default': 'identifier',
+                        },
+                    },
+                ],
+
+                // Special identified used for the not function.
+                [/~/, 'identifier'],
+
+                // Type variable, e.g. 'n
+                [/'@identifier/, 'type'],
+
+                // (operator_chars)+, optionally followed by _identifier.
+                [/[!%&*+\-./:<>=@^|#]+(?:_@identifier)?/, 'operator'],
+
+                // TODO: Handle < > in $include <foo.h> not being an operator.
+                // Although it probably doesn't matter too much that we colour
+                // it incorrectly, just for syntax highlighting.
+
+                // Brackets.
+                [/[{}()[\]<>]/, '@brackets'],
+
+                // Numbers.
+                [/0b[01_]+/, 'number.binary'],
+                [/0x[0-9a-fA-F_]+/, 'number.hex'],
+                [/-?\d*\.\d+/, 'number.float'],
+                [/-?\d+/, 'number'],
+
+                // TODO: is . on it's own a delimiter or an operator?
+
+                // delimiter: after number because of .\d floats
+                [/[;,.]/, 'delimiter'],
+
+                // Unterminated string. Any character except " or \,
+                // or \ followed by any character. Then end of line.
+                // TODO: I think this doesn't mark unclosed multiline
+                // strings as invalid.
+                [/"([^"\\]|\\.)*$/, 'string.invalid'],
+                // Valid string.
+                [/"/, 'string', '@string'],
+            ],
+
+            whitespace: [
+                // Whitespace.
+                [/[ \t\r\n]+/, 'white'],
+                // Start of block comment.
+                [/\/\*/, 'comment', '@block_comment'],
+                // Line comment.
+                [/\/\/.*$/, 'comment'],
+            ],
+
+            block_comment: [
+                // Not / or *, definitely still in the block.
+                // This is not strictly necessary but improves efficiency.
+                [/[^\/*]+/, 'comment'],
+                // /*, push block comment.
+                [/\/\*/, 'comment', '@push'],
+                // */, pop block comment.
+                ['\\*/', 'comment', '@pop'],
+                // Anything else, still a comment.
+                [/./, 'comment'],
+            ],
+
+            string: [
+                // Not \ or " - must still be in the string.
+                [/[^\\"]+/, 'string'],
+                // Valid escape sequences, including escaped new lines.
+                [/@string_escapes/, 'string.escape'],
+                // Any other escape sequence is invalid.
+                [/\\./, 'string.escape.invalid'],
+                // End of string.
+                [/"/, 'string', '@pop'],
+            ],
+        },
+    };
+}
+
+monaco.languages.register({id: 'sail'});
+monaco.languages.setMonarchTokensProvider('sail', definition());

types/languages.interfaces.ts

@@ -87,6 +87,7 @@ export type LanguageKey =
     | 'racket'
     | 'ruby'
     | 'rust'
+    | 'sail'
     | 'scala'
     | 'slang'
     | 'solidity'

views/resources/logos/sail.svg

@@ -0,0 +1,25 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!--
+Sail logo by Jean Pichon, licensed under CC0 1.0
+https://creativecommons.org/publicdomain/zero/1.0/
+-->
+
+<svg
+   version="1.1"
+   viewBox="0 0 210 210"
+   height="210mm"
+   width="210mm"
+   xmlns="http://www.w3.org/2000/svg"
+   xmlns:svg="http://www.w3.org/2000/svg">
+  <g transform="translate(-0.28176534,-75.428589)">
+    <path
+       d="m 94.030424,262.96089 c 0,0 30.994046,-43.46726 43.845236,-74.08333 12.85119,-30.61607 27.97024,-68.79167 27.97024,-68.79167 0,0 -1.88988,52.16072 -1.51191,83.91072 0.37798,31.75 1.88989,49.51487 1.88989,49.51487 z"
+       style="fill:#259dd5;stroke:#ffffff;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4" />
+    <path
+       d="m 46.405423,259.93708 c 0,0 50.64881,-55.94047 69.547617,-86.55654 18.89881,-30.61607 46.1131,-70.30357 46.1131,-70.30357 0,0 -16.63096,47.24702 -20.41072,67.27976 -3.77976,20.03274 -1.88988,54.42857 -1.88988,54.42857 0,0 -13.98512,3.02381 -40.065473,12.85119 -26.080354,9.82738 -53.294644,22.30059 -53.294644,22.30059 z"
+       style="fill:#259dd5;stroke:#ffffff;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4" />
+    <path
+       d="m 19.947093,251.99959 c 0,0 25.70238,-25.70238 66.523805,-74.4613 40.821432,-48.75893 75.595232,-88.446434 75.595232,-88.446434 0,0 -25.3244,57.830354 -34.7738,78.619044 -9.44941,20.78869 -17.38691,44.22322 -17.38691,44.22322 0,0 -42.333327,18.14286 -57.074397,26.08036 -14.74107,7.9375 -32.88393,13.98511 -32.88393,13.98511"
+       style="fill:#259dd5;stroke:#ffffff;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4"/>
+  </g>
+</svg>