Improvements to sail n_constraints

1) Added a new construct to the expression level: constraint. This is the
essentially the boolean form of sizeof. Whereas sizeof takes a nexp
and has type [:'n:], constraint takes a n_constraint and returns a
boolean. The hope is this will allow for flow typing to be represented
more explicitly in the generatated sail from ASL.

For example we could have something like:

default Order dec

val bit[64] -> unit effect pure test64

val forall 'n, ('n = 32 | 'n = 64 | 'n = 10) & 'n != 43. bit['n] -> unit effect pure test

function forall 'n. unit test addr =
{
  if constraint('n = 32) then {
    ()
  } else {
    assert(constraint('n = 64), "64-bit mode");
    test64(addr)
  }
}

2) The other thing this example demonstrates is that flow constraints
now work with assert and not just if. Even though flow typing will
only guarantee us that 'n != 32 in the else branch, the assert gives
us 'n = 64. This is very useful as it's a common idiom in the ARM
spec to guarantee such things with an assert.

3) Added != to the n_constraint language

4) Changed the n_constraint language to add or and and as constructs
in constraints. Previously one could have a list of conjuncts each of
which were simple inequalites or set constraints, now one can do for
example:

val forall 'n, ('n = 32 | 'n = 64) & 'n in {32, 64}. bit['n] -> unit effect pure test

This has the very nice upside that every n_constraint can now be
negatated when flow-typing if statements. Note also that 'in' has been
introduced as a synonym for 'IN' in the constraint 'n in {32,64}. The
use of a block capital keyword was a bit odd there because all the
other keywords are lowercase.

1 files changed, 10 insertions, 6 deletions

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index d4278b56..c674735d 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -49,9 +49,6 @@ open Pretty_print_common
  * PPrint-based source-to-source pretty printer
 ****************************************************************************)
 
-
-
-
 let doc_bkind (BK_aux(k,_)) =
   string (match k with
   | BK_type -> "Type"
@@ -62,13 +59,18 @@ let doc_bkind (BK_aux(k,_)) =
 let doc_kind (K_aux(K_kind(klst),_)) =
   separate_map (spaces arrow) doc_bkind klst
 
-let doc_nexp_constraint (NC_aux(nc,_)) = match nc with
+let rec doc_nexp_constraint (NC_aux(nc,_)) = match nc with
   | NC_fixed(n1,n2) -> doc_op equals (doc_nexp n1) (doc_nexp n2)
+  | NC_not_equal (n1, n2) -> doc_op (string "!=") (doc_nexp n1) (doc_nexp n2)
   | NC_bounded_ge(n1,n2) -> doc_op (string ">=") (doc_nexp n1) (doc_nexp n2)
   | NC_bounded_le(n1,n2) -> doc_op (string "<=") (doc_nexp n1) (doc_nexp n2)
   | NC_nat_set_bounded(v,bounds) ->
       doc_op (string "IN") (doc_var v)
-        (braces (separate_map comma_sp doc_int bounds))
+             (braces (separate_map comma_sp doc_int bounds))
+  | NC_or (nc1, nc2) ->
+     parens (separate space [doc_nexp_constraint nc1; string "|"; doc_nexp_constraint nc2])
+  | NC_and (nc1, nc2) ->
+     separate space [doc_nexp_constraint nc1; string "&"; doc_nexp_constraint nc2]
 
 let doc_qi (QI_aux(qi,_)) = match qi with
   | QI_const n_const -> doc_nexp_constraint n_const
@@ -293,7 +295,9 @@ let doc_exp, doc_let =
       let cases = separate_map (break 1) doc_case pexps in
       surround 2 1 opening cases rbrace
   | E_sizeof n ->
-    separate space [string "sizeof"; doc_nexp n]
+     separate space [string "sizeof"; doc_nexp n]
+  | E_constraint nc ->
+     string "constraint" ^^ parens (doc_nexp_constraint nc)
   | E_exit e ->
     separate space [string "exit"; atomic_exp e;]
   | E_return e ->