diff --git a/doc/asciidoc/language.adoc b/doc/asciidoc/language.adoc
index 1d960c22d..ed7a9ca6c 100644
--- a/doc/asciidoc/language.adoc
+++ b/doc/asciidoc/language.adoc
@@ -1070,11 +1070,9 @@ Perhaps surprisingly for a specification language, Sail has exception
 support. This is because exceptions as a language feature do sometimes
 appear in vendor ISA pseudocode (they are a feature in Arm's ASL
 language), and such code would be very difficult to translate into
-Sail if Sail did not itself support exceptions. We already translate
-Sail to monadic theorem prover code, so working with a monad that
-supports exceptions is fairly natural. In practice Sail language-level
-exceptions end up being quite a nice tool for implementing processor
-exceptions in ISA specifications.
+Sail if Sail did not itself support exceptions. In practice Sail
+language-level exceptions end up being quite a nice tool for
+implementing processor exceptions in ISA specifications.
 
 For exceptions we have two language features: `throw` statements
 and `try`--`catch` blocks. The throw keyword takes a value of
diff --git a/doc/asciidoc/parser.sed b/doc/asciidoc/parser.sed
index 88b328790..84009847e 100644
--- a/doc/asciidoc/parser.sed
+++ b/doc/asciidoc/parser.sed
@@ -11,6 +11,7 @@
 /Mutual/d
 /Impl/d
 /LcurlyBar/d
+/Monadic/d
 
 s/Pragma/$LINE_DIRECTIVE/g
 s/Fixity/FIXITY_DEF/g
@@ -22,6 +23,7 @@ s/End/end/g
 s/Default/default/g
 s/Scattered/scattered/g
 s/Monadic/monadic/g
+s/Impure/impure/g
 s/Typedef/type/g
 s/Enum/enum/g
 s/With/with/g
diff --git a/doc/examples/riscv_duopod.sail b/doc/examples/riscv_duopod.sail
index 6c2f24d0e..efaf72522 100644
--- a/doc/examples/riscv_duopod.sail
+++ b/doc/examples/riscv_duopod.sail
@@ -116,7 +116,7 @@ overload X = {rX, wX}
 $span end
 
 /* Accessors for memory */
-val MEMr = monadic { lem: "MEMr", coq: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val MEMr = impure { lem: "MEMr", coq: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
    (int('m), int('n), bits('m), bits('m)) -> bits(8 * 'n)
 
 val read_mem : forall 'n, 'n >= 0. (xlenbits, int('n)) -> bits(8 * 'n)
diff --git a/doc/manual.html b/doc/manual.html
index fe97cf4a1..a674fb9ed 100644
--- a/doc/manual.html
+++ b/doc/manual.html
@@ -4,7 +4,7 @@
 <meta charset="UTF-8">
 <meta http-equiv="X-UA-Compatible" content="IE=edge">
 <meta name="viewport" content="width=device-width, initial-scale=1.0">
-<meta name="generator" content="Asciidoctor 2.0.20">
+<meta name="generator" content="Asciidoctor 2.0.18">
 <meta name="author" content="Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Shaked Flur, Kathryn E. Gray, Robert Norton-Wright, Christopher Pulte, Peter Sewell">
 <title>The Sail instruction-set semantics specification language</title>
 <style>
@@ -2656,14 +2656,14 @@ <h2 id="_introduction">Introduction</h2>
 the envelope of architecturally allowed behaviour for sequential code.</p>
 </div>
 <div class="paragraph">
-<p>For x86[<a href="#Intel61">1</a>], the Intel pseudocode is just suggestive,
-with embedded prose, while the AMD descriptions[<a href="#AMD_3_21">2</a>]
-are prose alone. For IBM Power[<a href="#Power3.0B">3</a>], there is
+<p>For x86[.citation]<mark>[<a href="#Intel61">1</a>]</mark>, the Intel pseudocode is just suggestive,
+with embedded prose, while the AMD descriptions[.citation]<mark>[<a href="#AMD_3_21">2</a>]</mark>
+are prose alone. For IBM Power[.citation]<mark>[<a href="#Power3.0B">3</a>]</mark>, there is
 detailed pseudocode which has recently become
-machine-processed[<a href="#Leighton21">4</a>]. For
-Arm[<a href="#armarmv8">5</a>], there is detailed pseudocode, which has
-recently become machine-processed[<a href="#Reid16">6</a>]. For
-MIPS[<a href="#MIPS64-II">7</a>, <a href="#MIPS64-III">8</a>] there is also reasonably detailed
+machine-processed[.citation]<mark>[<a href="#Leighton21">4</a>]</mark>. For
+Arm[.citation]<mark>[<a href="#armarmv8">5</a>]</mark>, there is detailed pseudocode, which has
+recently become machine-processed[.citation]<mark>[<a href="#Reid16">6</a>]</mark>. For
+MIPS[.citation]<mark>[<a href="#MIPS64-II">7</a>, <a href="#MIPS64-III">8</a>]</mark> there is also reasonably detailed
 pseudocode.</p>
 </div>
 <div class="paragraph">
@@ -2721,7 +2721,7 @@ <h2 id="_introduction">Introduction</h2>
 <p>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[<a href="#Lem-icfp2014">9</a>, <a href="#Lemcode">10</a>], a language of type, function, and
+Lem[.citation]<mark>[<a href="#Lem-icfp2014">9</a>, <a href="#Lemcode">10</a>]</mark>, 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
@@ -2783,14 +2783,14 @@ <h2 id="_introduction">Introduction</h2>
 </div>
 <div class="paragraph">
 <p>The MIPS model is hand-written based on the MIPS64 manual version
-2.5[<a href="#MIPS64-II">7</a>, <a href="#MIPS64-III">8</a>],
+2.5[.citation]<mark>[<a href="#MIPS64-II">7</a>, <a href="#MIPS64-III">8</a>]</mark>,
 but covering only the features in the BERI hardware
-reference[<a href="#UCAM-CL-TR-868">11</a>],
-which in turn drew on MIPS4000 and MIPS32[<a href="#MIPS4000">12</a>, <a href="#MIPS32-I">13</a>].</p>
+reference[.citation]<mark>[<a href="#UCAM-CL-TR-868">11</a>]</mark>,
+which in turn drew on MIPS4000 and MIPS32[.citation]<mark>[<a href="#MIPS4000">12</a>, <a href="#MIPS32-I">13</a>]</mark>.</p>
 </div>
 <div class="paragraph">
 <p>The CHERI model is based on that and the CHERI ISA reference manual
-version&#160;5[<a href="#UCAM-CL-TR-891">14</a>]. These two are both
+version&#160;5[.citation]<mark>[<a href="#UCAM-CL-TR-891">14</a>]</mark>. 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
@@ -2905,7 +2905,7 @@ <h2 id="_a_tutorial_risc_v_style_example">A tutorial RISC-V style example</h2>
 </div>
 <div class="listingblock">
 <div class="content">
-<pre class="rouge highlight"><code data-lang="sail"><span class="k">val</span><span class="w"> </span><span class="nf">MEMr</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="k">monadic</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">lem</span><span class="p">:</span><span class="w"> </span><span class="s">"MEMr"</span><span class="p">,</span><span class="w"> </span><span class="n">coq</span><span class="p">:</span><span class="w"> </span><span class="s">"MEMr"</span><span class="p">,</span><span class="w"> </span><span class="mi">_</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="s">"read_ram"</span><span class="w"> </span><span class="p">}</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="k">forall</span><span class="w"> </span><span class="nv">'n</span><span class="w"> </span><span class="nv">'m</span><span class="p">,</span><span class="w"> </span><span class="nv">'n</span><span class="w"> </span><span class="o">&gt;=</span><span class="w"> </span><span class="mi">0</span><span class="o">.</span><span class="w">
+<pre class="rouge highlight"><code data-lang="sail"><span class="k">val</span><span class="w"> </span><span class="nf">MEMr</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="n">impure</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">lem</span><span class="p">:</span><span class="w"> </span><span class="s">"MEMr"</span><span class="p">,</span><span class="w"> </span><span class="n">coq</span><span class="p">:</span><span class="w"> </span><span class="s">"MEMr"</span><span class="p">,</span><span class="w"> </span><span class="mi">_</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="s">"read_ram"</span><span class="w"> </span><span class="p">}</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="k">forall</span><span class="w"> </span><span class="nv">'n</span><span class="w"> </span><span class="nv">'m</span><span class="p">,</span><span class="w"> </span><span class="nv">'n</span><span class="w"> </span><span class="o">&gt;=</span><span class="w"> </span><span class="mi">0</span><span class="o">.</span><span class="w">
    </span><span class="p">(</span><span class="kt">int</span><span class="p">(</span><span class="nv">'m</span><span class="p">),</span><span class="w"> </span><span class="kt">int</span><span class="p">(</span><span class="nv">'n</span><span class="p">),</span><span class="w"> </span><span class="kt">bits</span><span class="p">(</span><span class="nv">'m</span><span class="p">),</span><span class="w"> </span><span class="kt">bits</span><span class="p">(</span><span class="nv">'m</span><span class="p">))</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="kt">bits</span><span class="p">(</span><span class="mi">8</span><span class="w"> </span><span class="o">*</span><span class="w"> </span><span class="nv">'n</span><span class="p">)</span><span class="w">
 
 </span><span class="k">val</span><span class="w"> </span><span class="nf">read_mem</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="k">forall</span><span class="w"> </span><span class="nv">'n</span><span class="p">,</span><span class="w"> </span><span class="nv">'n</span><span class="w"> </span><span class="o">&gt;=</span><span class="w"> </span><span class="mi">0</span><span class="o">.</span><span class="w"> </span><span class="p">(</span><span class="n">xlenbits</span><span class="p">,</span><span class="w"> </span><span class="kt">int</span><span class="p">(</span><span class="nv">'n</span><span class="p">))</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="kt">bits</span><span class="p">(</span><span class="mi">8</span><span class="w"> </span><span class="o">*</span><span class="w"> </span><span class="nv">'n</span><span class="p">)</span><span class="w">
@@ -5127,11 +5127,9 @@ <h3 id="_exceptions">Exceptions</h3>
 support. This is because exceptions as a language feature do sometimes
 appear in vendor ISA pseudocode (they are a feature in Arm&#8217;s ASL
 language), and such code would be very difficult to translate into
-Sail if Sail did not itself support exceptions. We already translate
-Sail to monadic theorem prover code, so working with a monad that
-supports exceptions is fairly natural. In practice Sail language-level
-exceptions end up being quite a nice tool for implementing processor
-exceptions in ISA specifications.</p>
+Sail if Sail did not itself support exceptions. In practice Sail
+language-level exceptions end up being quite a nice tool for
+implementing processor exceptions in ISA specifications.</p>
 </div>
 <div class="paragraph">
 <p>For exceptions we have two language features: <code>throw</code> statements
@@ -5629,7 +5627,10 @@ <h2 id="_the_sail_grammar">The Sail Grammar</h2>
 
 </span><span class="o">&lt;</span><span class="n">typ_no_caret</span><span class="o">&gt;</span><span class="w"> </span><span class="p">::=</span><span class="w"> </span><span class="o">&lt;</span><span class="n">prefix_typ_op</span><span class="o">&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">postfix_typ</span><span class="o">&gt;</span><span class="w"> </span><span class="p">(</span><span class="o">&lt;</span><span class="n">op_no_caret</span><span class="o">&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">prefix_typ_op</span><span class="o">&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">postfix_typ</span><span class="o">&gt;</span><span class="p">)</span><span class="o">*</span><span class="w">
 
-</span><span class="o">&lt;</span><span class="n">typ</span><span class="o">&gt;</span><span class="w"> </span><span class="p">::=</span><span class="w"> </span><span class="o">&lt;</span><span class="n">prefix_typ_op</span><span class="o">&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">postfix_typ</span><span class="o">&gt;</span><span class="w"> </span><span class="p">(</span><span class="o">&lt;</span><span class="n">op</span><span class="o">&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">prefix_typ_op</span><span class="o">&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">postfix_typ</span><span class="o">&gt;</span><span class="p">)</span><span class="o">*</span><span class="w">
+</span><span class="o">&lt;</span><span class="n">typ</span><span class="o">&gt;</span><span class="w"> </span><span class="p">::=</span><span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="o">&lt;</span><span class="n">infix_typ</span><span class="o">&gt;</span><span class="w"> </span><span class="k">then</span><span class="w"> </span><span class="o">&lt;</span><span class="n">infix_typ</span><span class="o">&gt;</span><span class="w"> </span><span class="k">else</span><span class="w"> </span><span class="o">&lt;</span><span class="n">infix_typ</span><span class="o">&gt;</span><span class="w">
+        </span><span class="o">|</span><span class="w"> </span><span class="o">&lt;</span><span class="n">infix_typ</span><span class="o">&gt;</span><span class="w">
+
+</span><span class="o">&lt;</span><span class="n">infix_typ</span><span class="o">&gt;</span><span class="w"> </span><span class="p">::=</span><span class="w"> </span><span class="o">&lt;</span><span class="n">prefix_typ_op</span><span class="o">&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">postfix_typ</span><span class="o">&gt;</span><span class="w"> </span><span class="p">(</span><span class="o">&lt;</span><span class="n">op</span><span class="o">&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">prefix_typ_op</span><span class="o">&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">postfix_typ</span><span class="o">&gt;</span><span class="p">)</span><span class="o">*</span><span class="w">
 
 </span><span class="o">&lt;</span><span class="n">atomic_typ</span><span class="o">&gt;</span><span class="w"> </span><span class="p">::=</span><span class="w"> </span><span class="o">&lt;</span><span class="n">id</span><span class="o">&gt;</span><span class="w">
                </span><span class="o">|</span><span class="w"> </span><span class="mi">_</span><span class="w">
@@ -5775,7 +5776,7 @@ <h2 id="_the_sail_grammar">The Sail Grammar</h2>
                </span><span class="o">|</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="o">&lt;</span><span class="n">exp</span><span class="o">&gt;</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&lt;</span><span class="n">fexp_exp_list</span><span class="o">&gt;</span><span class="w"> </span><span class="p">}</span><span class="w">
                </span><span class="o">|</span><span class="w"> </span><span class="p">[</span><span class="w"> </span><span class="p">]</span><span class="w">
                </span><span class="o">|</span><span class="w"> </span><span class="p">[</span><span class="w"> </span><span class="o">&lt;</span><span class="n">exp_list</span><span class="o">&gt;</span><span class="w"> </span><span class="p">]</span><span class="w">
-               </span><span class="o">|</span><span class="w"> </span><span class="p">[</span><span class="w"> </span><span class="o">&lt;</span><span class="n">exp</span><span class="o">&gt;</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&lt;</span><span class="n">vector_update</span><span class="o">&gt;</span><span class="w"> </span><span class="p">(,</span><span class="w"> </span><span class="o">&lt;</span><span class="n">vector_update</span><span class="o">&gt;</span><span class="p">)</span><span class="o">*</span><span class="w"> </span><span class="p">]</span><span class="w">
+               </span><span class="o">|</span><span class="w"> </span><span class="p">[</span><span class="w"> </span><span class="o">&lt;</span><span class="n">exp</span><span class="o">&gt;</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&lt;</span><span class="n">vector_update_list</span><span class="o">&gt;</span><span class="w"> </span><span class="p">]</span><span class="w">
                </span><span class="o">|</span><span class="w"> </span><span class="p">[|</span><span class="w"> </span><span class="p">|]</span><span class="w">
                </span><span class="o">|</span><span class="w"> </span><span class="p">[|</span><span class="w"> </span><span class="o">&lt;</span><span class="n">exp_list</span><span class="o">&gt;</span><span class="w"> </span><span class="p">|]</span><span class="w">
                </span><span class="o">|</span><span class="w"> </span><span class="p">(</span><span class="w"> </span><span class="o">&lt;</span><span class="n">exp</span><span class="o">&gt;</span><span class="w"> </span><span class="p">)</span><span class="w">
@@ -5795,6 +5796,9 @@ <h2 id="_the_sail_grammar">The Sail Grammar</h2>
                   </span><span class="o">|</span><span class="w"> </span><span class="o">&lt;</span><span class="n">atomic_exp</span><span class="o">&gt;</span><span class="w"> </span><span class="o">..</span><span class="w"> </span><span class="o">&lt;</span><span class="n">atomic_exp</span><span class="o">&gt;</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="o">&lt;</span><span class="n">exp</span><span class="o">&gt;</span><span class="w">
                   </span><span class="o">|</span><span class="w"> </span><span class="o">&lt;</span><span class="n">id</span><span class="o">&gt;</span><span class="w">
 
+</span><span class="o">&lt;</span><span class="n">vector_update_list</span><span class="o">&gt;</span><span class="w"> </span><span class="p">::=</span><span class="w"> </span><span class="o">&lt;</span><span class="n">vector_update</span><span class="o">&gt;</span><span class="w"> </span><span class="p">[,]</span><span class="w">
+                       </span><span class="o">|</span><span class="w"> </span><span class="o">&lt;</span><span class="n">vector_update</span><span class="o">&gt;</span><span class="w"> </span><span class="p">,</span><span class="w"> </span><span class="o">&lt;</span><span class="n">vector_update_list</span><span class="o">&gt;</span><span class="w">
+
 </span><span class="o">&lt;</span><span class="n">funcl_annotation</span><span class="o">&gt;</span><span class="w"> </span><span class="p">::=</span><span class="w"> </span><span class="n">Private</span><span class="w">
                      </span><span class="o">|</span><span class="w"> </span><span class="cp">$[ATTRIBUTE]</span><span class="w">
 
@@ -5842,6 +5846,7 @@ <h2 id="_the_sail_grammar">The Sail Grammar</h2>
              </span><span class="o">|</span><span class="w"> </span><span class="k">type</span><span class="w"> </span><span class="o">&lt;</span><span class="n">id</span><span class="o">&gt;</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="o">&lt;</span><span class="n">typ</span><span class="o">&gt;</span><span class="w">
              </span><span class="o">|</span><span class="w"> </span><span class="k">type</span><span class="w"> </span><span class="o">&lt;</span><span class="n">id</span><span class="o">&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">typaram</span><span class="o">&gt;</span><span class="w"> </span><span class="p">-&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">kind</span><span class="o">&gt;</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="o">&lt;</span><span class="n">typ</span><span class="o">&gt;</span><span class="w">
              </span><span class="o">|</span><span class="w"> </span><span class="k">type</span><span class="w"> </span><span class="o">&lt;</span><span class="n">id</span><span class="o">&gt;</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="o">&lt;</span><span class="n">kind</span><span class="o">&gt;</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="o">&lt;</span><span class="n">typ</span><span class="o">&gt;</span><span class="w">
+             </span><span class="o">|</span><span class="w"> </span><span class="k">type</span><span class="w"> </span><span class="o">&lt;</span><span class="n">id</span><span class="o">&gt;</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="o">&lt;</span><span class="n">kind</span><span class="o">&gt;</span><span class="w">
              </span><span class="o">|</span><span class="w"> </span><span class="k">struct</span><span class="w"> </span><span class="o">&lt;</span><span class="n">id</span><span class="o">&gt;</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="o">&lt;</span><span class="n">struct_fields</span><span class="o">&gt;</span><span class="w"> </span><span class="p">}</span><span class="w">
              </span><span class="o">|</span><span class="w"> </span><span class="k">struct</span><span class="w"> </span><span class="o">&lt;</span><span class="n">id</span><span class="o">&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">typaram</span><span class="o">&gt;</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="o">&lt;</span><span class="n">struct_fields</span><span class="o">&gt;</span><span class="w"> </span><span class="p">}</span><span class="w">
              </span><span class="o">|</span><span class="w"> </span><span class="k">enum</span><span class="w"> </span><span class="o">&lt;</span><span class="n">id</span><span class="o">&gt;</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="o">&lt;</span><span class="n">id</span><span class="o">&gt;</span><span class="w"> </span><span class="p">(</span><span class="o">|</span><span class="w"> </span><span class="o">&lt;</span><span class="n">id</span><span class="o">&gt;</span><span class="p">)</span><span class="o">*</span><span class="w">
@@ -5905,8 +5910,8 @@ <h2 id="_the_sail_grammar">The Sail Grammar</h2>
 </span><span class="o">&lt;</span><span class="n">mapcl</span><span class="o">&gt;</span><span class="w"> </span><span class="p">::=</span><span class="w"> </span><span class="cp">$[ATTRIBUTE]</span><span class="w"> </span><span class="o">&lt;</span><span class="n">mapcl</span><span class="o">&gt;</span><span class="w">
           </span><span class="o">|</span><span class="w"> </span><span class="o">&lt;</span><span class="n">mpexp</span><span class="o">&gt;</span><span class="w"> </span><span class="o">&lt;-&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">mpexp</span><span class="o">&gt;</span><span class="w">
           </span><span class="o">|</span><span class="w"> </span><span class="o">&lt;</span><span class="n">mpexp</span><span class="o">&gt;</span><span class="w"> </span><span class="p">=</span><span class="o">&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">exp</span><span class="o">&gt;</span><span class="w">
-          </span><span class="o">|</span><span class="w"> </span><span class="k">forwards</span><span class="w"> </span><span class="o">&lt;</span><span class="n">mpexp</span><span class="o">&gt;</span><span class="w"> </span><span class="p">=</span><span class="o">&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">exp</span><span class="o">&gt;</span><span class="w">
-          </span><span class="o">|</span><span class="w"> </span><span class="k">backwards</span><span class="w"> </span><span class="o">&lt;</span><span class="n">mpexp</span><span class="o">&gt;</span><span class="w"> </span><span class="p">=</span><span class="o">&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">exp</span><span class="o">&gt;</span><span class="w">
+          </span><span class="o">|</span><span class="w"> </span><span class="k">forwards</span><span class="w"> </span><span class="o">&lt;</span><span class="n">case</span><span class="o">&gt;</span><span class="w">
+          </span><span class="o">|</span><span class="w"> </span><span class="k">backwards</span><span class="w"> </span><span class="o">&lt;</span><span class="n">case</span><span class="o">&gt;</span><span class="w">
 
 </span><span class="o">&lt;</span><span class="n">mapcl_list</span><span class="o">&gt;</span><span class="w"> </span><span class="p">::=</span><span class="w"> </span><span class="o">&lt;</span><span class="n">mapcl</span><span class="o">&gt;</span><span class="w"> </span><span class="p">[,]</span><span class="w">
                </span><span class="o">|</span><span class="w"> </span><span class="o">&lt;</span><span class="n">mapcl</span><span class="o">&gt;</span><span class="w"> </span><span class="p">,</span><span class="w"> </span><span class="o">&lt;</span><span class="n">mapcl_list</span><span class="o">&gt;</span><span class="w">
@@ -5917,7 +5922,7 @@ <h2 id="_the_sail_grammar">The Sail Grammar</h2>
 </span><span class="o">&lt;</span><span class="n">let_def</span><span class="o">&gt;</span><span class="w"> </span><span class="p">::=</span><span class="w"> </span><span class="k">let</span><span class="w"> </span><span class="o">&lt;</span><span class="n">letbind</span><span class="o">&gt;</span><span class="w">
 
 
-</span><span class="o">&lt;</span><span class="n">pure_opt</span><span class="o">&gt;</span><span class="w"> </span><span class="p">::=</span><span class="w"> </span><span class="k">monadic</span><span class="w">
+             </span><span class="o">|</span><span class="w"> </span><span class="n">impure</span><span class="w">
              </span><span class="o">|</span><span class="w"> </span><span class="k">pure</span><span class="w">
 
 </span><span class="o">&lt;</span><span class="n">extern_binding</span><span class="o">&gt;</span><span class="w"> </span><span class="p">::=</span><span class="w"> </span><span class="o">&lt;</span><span class="n">id</span><span class="o">&gt;</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="n">STRING_LITERAL</span><span class="w">
@@ -5974,6 +5979,7 @@ <h2 id="_the_sail_grammar">The Sail Grammar</h2>
             </span><span class="o">|</span><span class="w"> </span><span class="o">&lt;</span><span class="n">overload_def</span><span class="o">&gt;</span><span class="w">
             </span><span class="o">|</span><span class="w"> </span><span class="o">&lt;</span><span class="n">scattered_def</span><span class="o">&gt;</span><span class="w">
             </span><span class="o">|</span><span class="w"> </span><span class="o">&lt;</span><span class="n">default_def</span><span class="o">&gt;</span><span class="w">
+            </span><span class="o">|</span><span class="w"> </span><span class="nb">constraint</span><span class="w"> </span><span class="o">&lt;</span><span class="n">typ</span><span class="o">&gt;</span><span class="w">
             </span><span class="o">|</span><span class="w"> </span><span class="cp">$LINE_DIRECTIVE</span><span class="w">
             </span><span class="o">|</span><span class="w"> </span><span class="kr">termination_measure</span><span class="w"> </span><span class="o">&lt;</span><span class="n">id</span><span class="o">&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">pat</span><span class="o">&gt;</span><span class="w"> </span><span class="p">=</span><span class="w"> </span><span class="o">&lt;</span><span class="n">exp</span><span class="o">&gt;</span><span class="w">
             </span><span class="o">|</span><span class="w"> </span><span class="kr">termination_measure</span><span class="w"> </span><span class="o">&lt;</span><span class="n">id</span><span class="o">&gt;</span><span class="w"> </span><span class="o">&lt;</span><span class="n">loop_measure</span><span class="o">&gt;</span><span class="w"> </span><span class="p">(,</span><span class="w"> </span><span class="o">&lt;</span><span class="n">loop_measure</span><span class="o">&gt;</span><span class="p">)</span><span class="o">*</span><span class="w">
@@ -6045,7 +6051,7 @@ <h2 id="_references">References</h2>
 </div>
 <div id="footer">
 <div id="footer-text">
-Last updated 2023-12-06 21:54:14 UTC
+Last updated 2024-04-29 16:29:17 +0100
 </div>
 </div>
 </body>
diff --git a/lib/concurrency_interface/common.sail b/lib/concurrency_interface/common.sail
index b74696e1b..943c18afc 100644
--- a/lib/concurrency_interface/common.sail
+++ b/lib/concurrency_interface/common.sail
@@ -87,7 +87,7 @@ $include <concurrency_interface/emulator_memory.sail>
 
 $ifdef SYMBOLIC
 val sail_instr_announce
-  = monadic "instr_announce"
+  = impure "instr_announce"
   : forall 'n, 'n > 0.
   bits('n) -> unit
 $else
@@ -101,7 +101,7 @@ $endif
 
 $ifdef SYMBOLIC
 val sail_branch_announce
-  = monadic "branch_announce"
+  = impure "branch_announce"
   : forall 'addrsize, 'addrsize in {32, 64}.
   (int('addrsize), bits('addrsize)) -> unit
 $else
@@ -117,10 +117,10 @@ $endif
   call [sail_end_cycle], to increment the cycle count and indicate the
   end of the current instruction. Cycle 0 is reserved for
   initialisation before executing the first instruction. */
-val sail_end_cycle = monadic "cycle_count" : unit -> unit
+val sail_end_cycle = impure "cycle_count" : unit -> unit
 
 /*! Returns the current cycle count */
-val sail_get_cycle_count = monadic "get_cycle_count" : unit -> int
+val sail_get_cycle_count = impure "get_cycle_count" : unit -> int
 
 $ifdef SYMBOLIC
 val sail_reset_registers = pure "reset_registers" : unit -> unit
diff --git a/lib/concurrency_interface/emulator_memory.sail b/lib/concurrency_interface/emulator_memory.sail
index a5aaf96b8..f30a6f618 100644
--- a/lib/concurrency_interface/emulator_memory.sail
+++ b/lib/concurrency_interface/emulator_memory.sail
@@ -93,14 +93,14 @@ $endif
 
 //! Read memory
 $iftarget isla
-val read_mem# = monadic "read_mem" : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
+val read_mem# = impure "read_mem" : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 $else
 val read_mem# : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
 $ifdef _EMULATOR_MEMORY_PRIMOPS
-val __read_mem# = monadic "emulator_read_mem" : forall 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
+val __read_mem# = impure "emulator_read_mem" : forall 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     (int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
 function read_mem#(_, addrsize, addr, n) = __read_mem#(addrsize, addr, n)
@@ -109,14 +109,14 @@ $endif
 
 //! Read memory, but signal to the emulator that this is an ifetch read
 $iftarget isla
-val read_mem_ifetch# = monadic "read_mem_ifetch" : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
+val read_mem_ifetch# = impure "read_mem_ifetch" : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 $else
 val read_mem_ifetch# : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
 $ifdef _EMULATOR_MEMORY_PRIMOPS
-val __read_mem_ifetch# = monadic "emulator_read_mem_ifetch" : forall 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
+val __read_mem_ifetch# = impure "emulator_read_mem_ifetch" : forall 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     (int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
 function read_mem_ifetch#(_, addrsize, addr, n) = __read_mem_ifetch#(addrsize, addr, n)
@@ -125,14 +125,14 @@ $endif
 
 //! Read memory, and signal to the emulator that this read should be treated as an exclusive access
 $iftarget isla
-val read_mem_exclusive# = monadic "read_mem_exclusive" : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
+val read_mem_exclusive# = impure "read_mem_exclusive" : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 $else
 val read_mem_exclusive# : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
 $ifdef _EMULATOR_MEMORY_PRIMOPS
-val __read_mem_exclusive# = monadic "emulator_read_mem_exclusive" : forall 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
+val __read_mem_exclusive# = impure "emulator_read_mem_exclusive" : forall 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     (int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
 function read_mem_exclusive#(_, addrsize, addr, n) = __read_mem_exclusive#(addrsize, addr, n)
@@ -141,14 +141,14 @@ $endif
 
 //! Write memory
 $iftarget isla
-val write_mem# = monadic "write_mem" : forall ('a: Type) 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
+val write_mem# = impure "write_mem" : forall ('a: Type) 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 $else
 val write_mem# : forall ('a: Type) 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 
 $ifdef _EMULATOR_MEMORY_PRIMOPS
-val __write_mem# = monadic "emulator_write_mem" : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
+val __write_mem# = impure "emulator_write_mem" : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
     (int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 
 function write_mem#(_, addrsize, addr, n, value) = __write_mem#(addrsize, addr, n, value)
@@ -157,22 +157,22 @@ $endif
 
 //! Write memory, and signal to the emulator that this read should be treated as an exclusive access
 $iftarget isla
-val write_mem_exclusive# = monadic "write_mem_exclusive" : forall ('a: Type) 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
+val write_mem_exclusive# = impure "write_mem_exclusive" : forall ('a: Type) 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 $else
 val write_mem_exclusive# : forall ('a: Type) 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 
 $ifdef _EMULATOR_MEMORY_PRIMOPS
-val __write_mem_exclusive# = monadic "emulator_write_mem_exclusive" : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
+val __write_mem_exclusive# = impure "emulator_write_mem_exclusive" : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
     (int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 
 function write_mem_exclusive#(_, addrsize, addr, n, value) = __write_mem_exclusive#(addrsize, addr, n, value)
 $endif
 $endif
 
-val read_tag# = monadic "emulator_read_tag"  : forall 'addrsize, 'addrsize in {32, 64}. (int('addrsize), bits('addrsize)) -> bool
+val read_tag# = impure "emulator_read_tag"  : forall 'addrsize, 'addrsize in {32, 64}. (int('addrsize), bits('addrsize)) -> bool
 
-val write_tag# = monadic "emulator_write_tag" : forall 'addrsize, 'addrsize in {32, 64}. (int('addrsize), bits('addrsize), bool) -> unit
+val write_tag# = impure "emulator_write_tag" : forall 'addrsize, 'addrsize in {32, 64}. (int('addrsize), bits('addrsize), bool) -> unit
 
 $endif
diff --git a/lib/concurrency_interface/read_write.sail b/lib/concurrency_interface/read_write.sail
index 48499e2ae..ec038c4bb 100644
--- a/lib/concurrency_interface/read_write.sail
+++ b/lib/concurrency_interface/read_write.sail
@@ -271,7 +271,7 @@ with
 
 // Used when we want a non memory read/write to appear in Isla's addr relation
 $iftarget isla
-val sail_address_announce = monadic "address_announce" : forall 'addrsize, 'addrsize in {32, 64}. (int('addrsize), bits('addrsize)) -> unit
+val sail_address_announce = impure "address_announce" : forall 'addrsize, 'addrsize in {32, 64}. (int('addrsize), bits('addrsize)) -> unit
 $else
 val sail_address_announce : forall 'addrsize, 'addrsize in {32, 64}. (int('addrsize), bits('addrsize)) -> unit
 
diff --git a/lib/float.sail b/lib/float.sail
index c2df3df1b..545122f8f 100644
--- a/lib/float.sail
+++ b/lib/float.sail
@@ -79,10 +79,10 @@ val round_toward_positive = pure "round_toward_positive" : unit -> rounding_mode
 val round_toward_negative = pure "round_toward_negative" : unit -> rounding_mode
 val round_toward_zero = pure "round_toward_zero" : unit -> rounding_mode
 
-val undefined_float16 = monadic "fp16_undefined" : unit -> float16
-val undefined_float32 = monadic "fp32_undefined" : unit -> float32
-val undefined_float64 = monadic "fp64_undefined" : unit -> float64
-val undefined_float128 = monadic "fp128_undefined" : unit -> float128
+val undefined_float16 = impure "fp16_undefined" : unit -> float16
+val undefined_float32 = impure "fp32_undefined" : unit -> float32
+val undefined_float64 = impure "fp64_undefined" : unit -> float64
+val undefined_float128 = impure "fp128_undefined" : unit -> float128
 
 val fp16_nan = pure "fp16_nan" : unit -> float16
 val fp32_nan = pure "fp32_nan" : unit -> float32
diff --git a/lib/flow.sail b/lib/flow.sail
index 380df09fb..a1e2ff730 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -128,6 +128,6 @@ function __id forall 'n. (x: int('n)) -> int('n) = x
 
 overload __size = {__id}
 
-val __deref = monadic "reg_deref" : forall ('a : Type). register('a) -> 'a
+val __deref = impure "reg_deref" : forall ('a : Type). register('a) -> 'a
 
 $endif
diff --git a/lib/regfp.sail b/lib/regfp.sail
index 413cc2d47..f1d9be4cd 100644
--- a/lib/regfp.sail
+++ b/lib/regfp.sail
@@ -222,55 +222,55 @@ union instruction_kind = {
 }
 
 val __read_mem
-  = monadic { ocaml: "Platform.read_mem", c: "platform_read_mem", _: "read_mem" }
+  = impure { ocaml: "Platform.read_mem", c: "platform_read_mem", _: "read_mem" }
   : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
   (read_kind, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
 val __read_memt
-  = monadic { ocaml: "Platform.read_memt", c: "platform_read_memt", _: "read_memt" }
+  = impure { ocaml: "Platform.read_memt", c: "platform_read_memt", _: "read_memt" }
   : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
   (read_kind, bits('addrsize), int('n)) -> (bits(8 * 'n), bit)
 
 val __write_mem_ea
-  = monadic { ocaml: "Platform.write_mem_ea", c: "platform_write_mem_ea", _: "write_mem_ea" }
+  = impure { ocaml: "Platform.write_mem_ea", c: "platform_write_mem_ea", _: "write_mem_ea" }
   : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
   (write_kind, int('addrsize), bits('addrsize), int('n)) -> unit
 
 val __write_mem
-  = monadic { ocaml: "Platform.write_mem", c: "platform_write_mem", _: "write_mem" }
+  = impure { ocaml: "Platform.write_mem", c: "platform_write_mem", _: "write_mem" }
   : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
   (write_kind, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 
 val __write_memt
-  = monadic { ocaml: "Platform.write_memt", c: "platform_write_memt", _: "write_memt" }
+  = impure { ocaml: "Platform.write_memt", c: "platform_write_memt", _: "write_memt" }
   : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
   (write_kind, bits('addrsize), int('n), bits(8 * 'n), bit) -> bool
 
 val __write_tag
-  = monadic { ocaml: "Platform.write_tag", c: "platform_write_tag", _: "write_tag" }
+  = impure { ocaml: "Platform.write_tag", c: "platform_write_tag", _: "write_tag" }
   : forall 'addrsize, 'addrsize in {32, 64}.
   (write_kind, bits('addrsize), bit) -> bool
 
 val __excl_res
-  = monadic { ocaml: "Platform.excl_res", c: "platform_excl_res", _: "excl_result" }
+  = impure { ocaml: "Platform.excl_res", c: "platform_excl_res", _: "excl_result" }
   : unit -> bool
 
 val __barrier
-  = monadic { ocaml: "Platform.barrier", c: "platform_barrier", _: "barrier" }
+  = impure { ocaml: "Platform.barrier", c: "platform_barrier", _: "barrier" }
   : barrier_kind -> unit
 
 val __branch_announce
-  = monadic { ocaml: "Platform.branch_announce", c: "platform_branch_announce", _ : "branch_announce" }
+  = impure { ocaml: "Platform.branch_announce", c: "platform_branch_announce", _ : "branch_announce" }
   : forall 'addrsize, 'addrsize in {32, 64}.
   (int('addrsize), bits('addrsize)) -> unit
 
 val __cache_maintenance
-  = monadic { ocaml: "Platform.cache_maintenance", c: "platform_cache_maintenance", _ : "cache_maintenance" }
+  = impure { ocaml: "Platform.cache_maintenance", c: "platform_cache_maintenance", _ : "cache_maintenance" }
   : forall 'addrsize, 'addrsize in {32, 64}.
   (cache_op_kind, int('addrsize), bits('addrsize)) -> unit
 
 val __instr_announce
-  = monadic { ocaml: "Platform.instr_announce", c: "platform_instr_announce", _: "instr_announce" }
+  = impure { ocaml: "Platform.instr_announce", c: "platform_instr_announce", _: "instr_announce" }
   : forall 'n, 'n > 0.
   bits('n) -> unit
 
diff --git a/src/lib/format_sail.ml b/src/lib/format_sail.ml
index ad0ff5c0f..0647ff092 100644
--- a/src/lib/format_sail.ml
+++ b/src/lib/format_sail.ml
@@ -559,7 +559,7 @@ module Make (Config : CONFIG) = struct
              ( match vs.extern_opt with
              | Some extern ->
                  space ^^ char '=' ^^ space
-                 ^^ string (if extern.pure then "pure" else "monadic")
+                 ^^ string (if extern.pure then "pure" else "impure")
                  ^^ space
                  ^^ surround indent 1 (char '{')
                       (separate_map (char ',' ^^ break 1) doc_binding extern.bindings)
diff --git a/src/lib/lexer.mll b/src/lib/lexer.mll
index d92864445..940da46a7 100644
--- a/src/lib/lexer.mll
+++ b/src/lib/lexer.mll
@@ -112,6 +112,7 @@ let kw_table =
      ("Order",                   (fun _ -> Order));
      ("Bool",                    (fun _ -> Bool));
      ("pure",                    (fun _ -> Pure));
+     ("impure",                  (fun _ -> Impure));
      ("monadic",                 (fun _ -> Monadic));
      ("register",		 (fun _ -> Register));
      ("return",                  (fun _ -> Return));
diff --git a/src/lib/parser.mly b/src/lib/parser.mly
index 98da75bc1..1454c7dd3 100644
--- a/src/lib/parser.mly
+++ b/src/lib/parser.mly
@@ -222,7 +222,7 @@ let old_bitfield_deprecated ?(bitfield = "<bitfield>") l field =
     ("Old bitfield syntax, use '" ^ replace ^ "' instead")
 
 let warn_extern_effect l =
-  Reporting.warn ~once_from:__POS__ "Deprecated" l "All external bindings should be marked as either monadic or pure"
+  Reporting.warn ~once_from:__POS__ "Deprecated" l "All external bindings should be marked as either pure or impure"
 
 let forwards_mapcl_deprecated l =
   Reporting.warn ~once_from:__POS__ "Deprecated" l "Single direction mapping clause should be prefixed by a direction, either forwards or backwards"
@@ -236,7 +236,7 @@ let set_syntax_deprecated l =
 
 %token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op
 %token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ Int Order Bool Cast
-%token Pure Monadic Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
+%token Pure Impure Monadic Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
 %token Undefined Union Newtype With Val Outcome Constraint Throw Try Catch Exit Bitfield Constant
 %token Repeat Until While Do Mutual Var Ref Configuration TerminationMeasure Instantiation Impl Private
 %token InternalPLet InternalReturn InternalAssume
@@ -1178,6 +1178,8 @@ outcome_spec_def:
 pure_opt:
   | Monadic
     { false }
+  | Impure
+    { false }
   | Pure
     { true }
 
diff --git a/test/c/cheri_capreg.sail b/test/c/cheri_capreg.sail
index c13d5981b..8c9cb3411 100644
--- a/test/c/cheri_capreg.sail
+++ b/test/c/cheri_capreg.sail
@@ -9,7 +9,7 @@ $include <vector_dec.sail>
 
 val "reg_deref" : forall ('a : Type). register('a) -> 'a
 /* sneaky deref with no effect necessary for bitfield writes */
-val _reg_deref = monadic "reg_deref" : forall ('a : Type). register('a) -> 'a
+val _reg_deref = impure "reg_deref" : forall ('a : Type). register('a) -> 'a
 
 val zeros_0 = pure "zeros" : forall 'n. int('n) -> bits('n)
 
diff --git a/test/format/default/val.expect b/test/format/default/val.expect
index 1809c65f2..bdb12c044 100644
--- a/test/format/default/val.expect
+++ b/test/format/default/val.expect
@@ -1,8 +1,8 @@
 default Order dec
 $include <prelude.sail>
 
-val foo = monadic { _: "foo" } : unit -> unit // foo
-val bar = monadic { c: "foo_c", _: "foo" } : (
+val foo = impure { _: "foo" } : unit -> unit // foo
+val bar = impure { c: "foo_c", _: "foo" } : (
         unit,
         unit,
         unit,
diff --git a/test/format/val.sail b/test/format/val.sail
index 24b140f5a..852d3f141 100644
--- a/test/format/val.sail
+++ b/test/format/val.sail
@@ -1,9 +1,9 @@
 default Order dec
 $include <prelude.sail>
 
-val foo = monadic { _: "foo" } : unit -> unit // foo
+val foo = impure { _: "foo" } : unit -> unit // foo
 
-val bar = monadic { c: "foo_c", _: "foo" } : (unit, unit, unit, vector(16, dec, vector(32, dec, int)), unit, unit, unit, vector(32, dec, int)) -> unit
+val bar = impure { c: "foo_c", _: "foo" } : (unit, unit, unit, vector(16, dec, vector(32, dec, int)), unit, unit, unit, vector(32, dec, int)) -> unit
 
 val baz : unit -> unit // baz
 val quuz : unit -> unit
diff --git a/test/ocaml/reg_passing/reg_passing.sail b/test/ocaml/reg_passing/reg_passing.sail
index f7d6ea222..fb7da5b9e 100644
--- a/test/ocaml/reg_passing/reg_passing.sail
+++ b/test/ocaml/reg_passing/reg_passing.sail
@@ -3,7 +3,7 @@ register R1 : int
 register R2 : int
 register R3 : int
 
-val __deref = monadic "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+val __deref = impure "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
 
 val output = {
     ocaml: "(fun (str, n) -> print_endline (str ^ Big_int.to_string n))",
diff --git a/test/typecheck/fail/add_vec_lit_old.sail b/test/typecheck/fail/add_vec_lit_old.sail
index edce299b3..cb0054765 100644
--- a/test/typecheck/fail/add_vec_lit_old.sail
+++ b/test/typecheck/fail/add_vec_lit_old.sail
@@ -1,9 +1,9 @@
 default Order inc
 
-val add_vec = monadic {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int).
+val add_vec = impure {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int).
   (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc)
 
-val add_range = monadic {ocaml: "add_range", lem: "add_range"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
+val add_range = impure {ocaml: "add_range", lem: "add_range"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
 val cast unsigned : forall ('n : Int).
diff --git a/test/typecheck/pass/bool_constraint/v1.expect b/test/typecheck/pass/bool_constraint/v1.expect
index 7e860eba5..dc0e9dfee 100644
--- a/test/typecheck/pass/bool_constraint/v1.expect
+++ b/test/typecheck/pass/bool_constraint/v1.expect
@@ -2,7 +2,7 @@
 27 |val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
    |           ^-----------------------^
    | 
-All external bindings should be marked as either monadic or pure
+All external bindings should be marked as either pure or impure
 
 Type error:
 pass/bool_constraint/v1.sail:12.19-20:
diff --git a/test/typecheck/pass/bool_constraint/v2.expect b/test/typecheck/pass/bool_constraint/v2.expect
index 3449279e3..e21288377 100644
--- a/test/typecheck/pass/bool_constraint/v2.expect
+++ b/test/typecheck/pass/bool_constraint/v2.expect
@@ -2,7 +2,7 @@
 27 |val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
    |           ^-----------------------^
    | 
-All external bindings should be marked as either monadic or pure
+All external bindings should be marked as either pure or impure
 
 Type error:
 pass/bool_constraint/v2.sail:38.4-32:
diff --git a/test/typecheck/pass/bool_constraint/v3.expect b/test/typecheck/pass/bool_constraint/v3.expect
index 668e261be..d19e09be5 100644
--- a/test/typecheck/pass/bool_constraint/v3.expect
+++ b/test/typecheck/pass/bool_constraint/v3.expect
@@ -2,7 +2,7 @@
 27 |val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> 'q. bool('q)}
    |           ^-----------------------^
    | 
-All external bindings should be marked as either monadic or pure
+All external bindings should be marked as either pure or impure
 
 Type error:
 pass/bool_constraint/v3.sail:46.4-32:
diff --git a/test/typecheck/pass/bool_constraint/v4.expect b/test/typecheck/pass/bool_constraint/v4.expect
index 56a30a592..e56dc83ab 100644
--- a/test/typecheck/pass/bool_constraint/v4.expect
+++ b/test/typecheck/pass/bool_constraint/v4.expect
@@ -2,7 +2,7 @@
 27 |val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
    |           ^-----------------------^
    | 
-All external bindings should be marked as either monadic or pure
+All external bindings should be marked as either pure or impure
 
 Type error:
 pass/bool_constraint/v4.sail:46.4-32:
diff --git a/test/typecheck/pass/reg_32_64.sail b/test/typecheck/pass/reg_32_64.sail
index 95b809d2c..6d7e443f1 100644
--- a/test/typecheck/pass/reg_32_64.sail
+++ b/test/typecheck/pass/reg_32_64.sail
@@ -2,7 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-val reg_deref = monadic "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+val reg_deref = impure "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
 
 register R0 : bits(64)
 register R1 : bits(64)
diff --git a/test/typecheck/pass/tuple_assign/v1.sail b/test/typecheck/pass/tuple_assign/v1.sail
index 1bd44ada5..19fc03dc6 100644
--- a/test/typecheck/pass/tuple_assign/v1.sail
+++ b/test/typecheck/pass/tuple_assign/v1.sail
@@ -1,7 +1,7 @@
 default Order dec
 $include <prelude.sail>
 
-val some_tuple = monadic "some_tuple" : unit -> (int, int, int)
+val some_tuple = impure "some_tuple" : unit -> (int, int, int)
 
 val all_updated : unit -> int