Add some explanations to free monad documentation

1 files changed, 37 insertions, 13 deletions

diff --git a/lib/isabelle/manual/Manual.thy b/lib/isabelle/manual/Manual.thy
index db960cf9..53175ec9 100644
--- a/lib/isabelle/manual/Manual.thy
+++ b/lib/isabelle/manual/Manual.thy
@@ -308,16 +308,25 @@ instances.\<close>
 
 subsubsection \<open>Free Monad \label{sec:free-monad}\<close>
 
-text \<open>In addition to the state monad, the Sail library defines a monad in the theory @{theory Prompt_monad}
-that is essentially a (flattened) free monad of an effect datatype.  A monadic expression either
-returns a pure value @{term a}, denoted @{term "Done a"}, or it has an effect.  The latter can be
-a failure or an exception, or an effect together with a continuation.  For example,
-@{term \<open>Read_reg ''PC'' k\<close>} represents a request to read the register @{term PC} and continue as
-@{term k}, which is a function that takes the register value as a parameter and returns another
-monadic expression.  The complete set of supported effects is captured in the following datatype:
+text \<open>In addition to the state monad, the theory @{theory Prompt_monad} defines a free monad of an
+effect datatype.  A monadic expression either returns a pure value @{term a}, denoted
+@{term "Done a"}, or it has an effect.  The latter can be a failure or an exception, or an effect
+together with a continuation.  For example, @{term \<open>Read_reg ''PC'' k\<close>} represents a request to
+read the register @{term PC} and continue as @{term k}, which is a function that takes the
+register value as a parameter and returns another monadic expression.  Another example is
+@{term "Undefined k"}, which requests a Boolean value from the execution context, e.g.~to resolve
+an undefined bit to a concrete value.  Again, the value is expected to be passed as an argument to
+the continuation @{term k}.  The complete set of supported monadic outcomes is captured in the
+following datatype:
 
 @{datatype [display] monad}
 
+The effects are designed to be usable as an interface to relaxed memory models.  For example,
+@{term Footprint} tells the memory model that the register footprint of the instruction should be
+re-calculated.  The Boolean parameters of the continuations of the @{term Write_memv},
+@{term Write_tag}, and @{term Excl_res} effects allow the memory model to inform the instruction
+whether a memory write has succeeded (or may succeed).
+
 The same set of combinators and wrappers as for the state monad is defined for this monad.  The
 names are the same, but without the suffix @{term S}, e.g.~@{term read_reg}, @{term write_mem_val},
 @{term undefined_bool}, @{term throw}, @{term try_catch}, etc.~(with the exception of the loop
@@ -330,22 +339,37 @@ complication is that, in general, this requires a single type that can subsume a
 registers occurring in a specification.  Otherwise, it would not be possible to find a single
 instantiation of the @{type monad} type to assign to a function that involves reading or writing
 multiple registers with different types, for example.  To solve this problem, the translation from
-Sail to Lem generates a union type @{typ register_value} including all register types of the given
-specification.  For example, in the case of the RISC-V duopod, this is\<^footnote>\<open>The @{term Regval_list}
-and @{term Regval_option} constructors are not actually used in the RISC-V duopod, but they are
-always generated by default.\<close>
+Sail to Lem generates a union type @{typ register_value} with constructors for all register base
+types of the given specification and the built-in type constructors @{term vector}, @{type list},
+and @{type option}.  In the case of the RISC-V duopod, this is
 
 @{datatype [display] register_value}
 
+For example, a value of the (complete) @{term Xs} register file (whose Sail type is
+@{verbatim "vector(32, dec, vector(64, dec, bit))"}) is represented as @{term "Regval_vector (32, False, xs)"},
+where @{term xs} is a list of words wrapped in @{term Regval_vector_64_dec_bit}.
+
 Sail also generates conversion functions to and from @{type register_value}, e.g.
 
 @{term [source, show_types] "regval_of_vector_64_dec_bit :: 64 word \<Rightarrow> register_value"} \\
 @{term [source, show_types] "vector_64_dec_bit_of_regval :: register_value \<Rightarrow> 64 word option"}
 
-where the latter is partial.  The matching pair of conversion functions for each register is
-recorded in its @{type register_ref} record, e.g.
+where the latter is partial.
+The conversion functions for @{term Regval_vector}, @{term Regval_list}, and @{term Regval_option}
+are higher-order functions that take the corresponding conversion function for the encapsulated
+type as a parameter, e.g.
+
+@{term [source, show_types] "regval_of_vector :: ('a \<Rightarrow> register_value) \<Rightarrow> int \<Rightarrow> bool \<Rightarrow> 'a list \<Rightarrow> register_value"} \\
+@{term [source, show_types] "vector_of_regval :: (register_value \<Rightarrow> 'a option) \<Rightarrow> register_value \<Rightarrow> 'a list option"}
+
+The latter only returns a value if \emph{all} elements of the vector can be successfully converted
+from @{typ register_value} to @{typ "'a"}.
+
+For each register, the matching pair of conversion functions is recorded in its
+@{type register_ref} record, e.g.
 
 @{thm [display] PC_ref_def}
+@{thm [display] Xs_ref_def}
 
 The @{term read_reg} wrapper, for example, takes such a reference as a parameter, generates a
 @{term Read_reg} effect with the register name, and casts the register value received as input via