Re-factor initial check

Mostly this is to change how we desugar types in order to make us more
flexible with what we can parse as a valid constraint as
type. Previously the structure of the initial check forced some
awkward limitations on what was parseable due to how the parse AST is
set up.

As part of this, I've taken the de-scattering of scattered functions
out of the initial check, and moved it to a re-writing step after
type-checking, where I think it logically belongs. This doesn't change
much right now, but opens up some more possibilities in the future:
Since scattered functions are now typechecked normally, any future
module system for Sail would be able to handle them specially, and the
Latex documentation backend can now document scattered functions
explicitly, rather than relying on hackish 'de-scattering' logic to
present documentation as the functions originally appeared.

This has one slight breaking change which is that union clauses must
appear before their uses in scattered functions, so

union ast = Foo : unit

function clause execute(Foo())

is ok, but

function clause execute(Foo())

union ast = Foo : unit

is not. Previously this worked because the de-scattering moved union
clauses upwards before type-checking, but as this now happens after
type-checking they must appear in the correct order. This doesn't
occur in ARM, RISC-V, MIPS, but did appear in Cheri and I submitted a
pull request to re-order the places where it happens.

1 files changed, 10 insertions, 5 deletions

diff --git a/language/sail.ott b/language/sail.ott
index 168998ad..a0b02a1c 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -954,18 +954,23 @@ default_spec :: 'DT_' ::=
 scattered_def :: 'SD_' ::=
   {{ com scattered function and union type definitions }}
   {{ aux _ annot }} {{ auxparam 'a }}
-  | scattered function rec_opt tannot_opt effect_opt id   :: :: scattered_function 
+  | scattered function rec_opt tannot_opt effect_opt id   :: :: function
 {{ texlong }} {{ com scattered function definition header }}
 
-  | function clause funcl  :: :: scattered_funcl  
+  | function clause funcl  :: :: funcl
 {{ texlong }} {{ com scattered function definition clause }}
 
-  | scattered typedef id name_scm_opt = const union typquant :: :: scattered_variant 
+  | scattered typedef id name_scm_opt = const union typquant :: :: variant
 {{ texlong }} {{ com scattered union definition header }}
 
-  | union id member type_union  :: :: scattered_unioncl 
+  | union id member type_union :: :: unioncl
 {{ texlong }} {{ com scattered union definition member }}
-  | end id  :: :: scattered_end
+
+  | scattered mapping id : tannot_opt :: :: mapping
+
+  | mapping clause id = mapcl :: :: mapcl
+
+  | end id  :: :: end
 {{ texlong }} {{ com scattered definition end }}
 
 reg_id :: 'RI_' ::=