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

diff --git a/src/process_file.ml b/src/process_file.ml
index efa2ec55..b2054f40 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -81,10 +81,16 @@ let parse_file (f : string) : Parse_ast.defs =
       | Lexer.LexError(s,p) ->
           raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s)))
 
+
 (*Should add a flag to say whether we want to consider Oinc or Odec the default order *)
 let convert_ast (defs : Parse_ast.defs) : (Type_internal.tannot Ast.defs * kind Envmap.t * Ast.order)=
   Initial_check.to_ast Nameset.empty Type_internal.initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown)) defs
 
+let load_file env f =
+  let ast = parse_file f in
+  let (ast, _, _) = convert_ast ast in
+  Type_check_new.check env ast
+
 let opt_new_typecheck = ref false
 let opt_just_check = ref false
 let opt_ddump_tc_ast = ref false