From 272d9565ef7f48baa0982a291c7fde8497ab0cd9 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 5 Dec 2018 20:49:38 +0000
Subject: 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.
---
 src/parse_ast.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'src/parse_ast.ml')

diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 38854d48..79d90635 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -494,13 +494,13 @@ dec_spec_aux =  (* Register declarations *)
 type 
 scattered_def_aux =  (* Function and type union definitions that can be spread across
          a file. Each one must end in $_$ *)
-   SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
- | SD_scattered_funcl of funcl (* scattered function definition clause *)
- | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
- | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
- | SD_scattered_mapping of id * tannot_opt
- | SD_scattered_mapcl of id * mapcl
- | SD_scattered_end of id (* scattered definition end *)
+   SD_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
+ | SD_funcl of funcl (* scattered function definition clause *)
+ | SD_variant of id * name_scm_opt * typquant (* scattered union definition header *)
+ | SD_unioncl of id * type_union (* scattered union definition member *)
+ | SD_mapping of id * tannot_opt
+ | SD_mapcl of id * mapcl
+ | SD_end of id (* scattered definition end *)
 
 
 type 
-- 
cgit v1.2.3