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, 0 insertions, 1 deletions

diff --git a/src/process_file.ml b/src/process_file.ml
index c3d0be0e..ca013077 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -388,7 +388,6 @@ let rewrite rewriters defs =
      raise (Reporting.err_typ l (Type_error.string_of_type_error err))
 
 let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
-let rewrite_undefined bitvectors = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined bitvectors x)]
 let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem
 let rewrite_ast_coq = rewrite Rewrites.rewrite_defs_coq
 let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml