From 2c01cb787a1e2cc02972edec5e8f1e2eb7e9a0d4 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 2 May 2024 05:23:03 +0100 Subject: [PATCH] Purge all mentions of the word that must not be named Previously we documented that when binding to theorem prover definitions, one has to destinguish between 'a -> b' and 'a -> M b', for a Sail function 'a -> b' Notably, this is because Sail does not infact use monads in any significant way, so the information has to be given only when the rubber meets the theorem prover road. For users of Sail who are not binding to custom theorem prover definitions, this is mostly irrelevant, but this saves the pain of users pressing Ctrl+f "monad' in the manual and leaving with misconceptions. As part of this we change 'monadic' to 'impure' everywhere user-facing (which is barely anywhere in the first place) --- doc/asciidoc/language.adoc | 8 +-- doc/asciidoc/parser.sed | 2 + doc/examples/riscv_duopod.sail | 2 +- doc/manual.html | 56 ++++++++++--------- lib/concurrency_interface/common.sail | 8 +-- .../emulator_memory.sail | 24 ++++---- lib/concurrency_interface/read_write.sail | 2 +- lib/float.sail | 8 +-- lib/flow.sail | 2 +- lib/regfp.sail | 22 ++++---- src/lib/format_sail.ml | 2 +- src/lib/lexer.mll | 1 + src/lib/parser.mly | 6 +- test/c/cheri_capreg.sail | 2 +- test/format/default/val.expect | 4 +- test/format/val.sail | 4 +- test/ocaml/reg_passing/reg_passing.sail | 2 +- test/typecheck/fail/add_vec_lit_old.sail | 4 +- test/typecheck/pass/bool_constraint/v1.expect | 2 +- test/typecheck/pass/bool_constraint/v2.expect | 2 +- test/typecheck/pass/bool_constraint/v3.expect | 2 +- test/typecheck/pass/bool_constraint/v4.expect | 2 +- test/typecheck/pass/reg_32_64.sail | 2 +- test/typecheck/pass/tuple_assign/v1.sail | 2 +- 24 files changed, 90 insertions(+), 81 deletions(-) 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 @@ - + The Sail instruction-set semantics specification language