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

diff --git a/src/ast_util.mli b/src/ast_util.mli
index 8902c39c..0adda3ef 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -44,6 +44,9 @@
 
 open Ast
 
+val mk_nc : n_constraint_aux -> n_constraint
+val mk_nexp : nexp_aux -> nexp
+
 (* Functions to map over the annotations in sub-expressions *)
 val map_exp_annot : ('a annot -> 'b annot) -> 'a exp -> 'b exp
 val map_pat_annot : ('a annot -> 'b annot) -> 'a pat -> 'b pat
@@ -96,6 +99,22 @@ module BE : sig
   val compare : base_effect -> base_effect -> int
 end
 
+module IdSet : sig
+  include Set.S with type elt = id
+end
+
+module KidSet : sig
+  include Set.S with type elt = kid
+end
+
+module KBindings : sig
+  include Map.S with type key = kid
+end
+
+module Bindings : sig
+  include Map.S with type key = id
+end
+
 val is_number : typ -> bool
 val is_vector_typ : typ -> bool
 val is_bit_typ : typ -> bool