10 files changed, 183 insertions, 4 deletions
diff --git a/lib/prelude.sail b/lib/prelude.sail
index b5ba261d..f3637945 100644
--- a/lib/prelude.sail
+++ b/lib/prelude.sail
@@ -161,15 +161,19 @@ val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_
 val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom
 val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom
 val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range
-val forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lteq_atom_atom
 val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range
 val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range
 val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range
 
-overload (deinfix >=) [gteq_range_atom; gteq_atom_range; gteq_vec; gteq_int]
-overload (deinfix >) [gt_vec; gt_int]
+val forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lteq_atom_atom
+val forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure gteq_atom_atom
+val forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lt_atom_atom
+val forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure gt_atom_atom
+
+overload (deinfix >=) [gteq_atom_atom; gteq_range_atom; gteq_atom_range; gteq_vec; gteq_int]
+overload (deinfix >) [gt_atom_atom; gt_vec; gt_int]
 overload (deinfix <=) [lteq_atom_atom; lteq_range_atom; lteq_atom_range; lteq_vec; lteq_int]
-overload (deinfix <) [lt_vec; lt_int]
+overload (deinfix <) [lt_atom_atom; lt_vec; lt_int]
 
 val (int, int) -> int effect pure quotient
 
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index 133c6db7..5a0735fb 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -1650,6 +1650,7 @@ and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ =
   end
 
 and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) =
+  typ_print ("Binding " ^ string_of_typ typ);
   let annot_pat pat typ = P_aux (pat, (l, Some (env, typ, no_effect))) in
   let switch_typ (P_aux (pat_aux, (l, Some (env, _, eff)))) typ = P_aux (pat_aux, (l, Some (env, typ, eff))) in
   let bind_tuple_pat (tpats, env) pat typ =
@@ -1842,6 +1843,25 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
           annot_lexp (LEXP_tup tlexps) typ, env
        | _ -> typ_error l "Cannot bind tuple l-expression against non tuple type"
      end
+  | LEXP_vector_range (LEXP_aux (LEXP_id v, _), exp1, exp2) ->
+     begin
+       let is_immutable, vtyp = match Env.lookup_id v env with
+         | Unbound -> typ_error l "Cannot assign to element of unbound vector"
+         | Enum _ -> typ_error l "Cannot vector assign to enumeration element"
+         | Local (Immutable, vtyp) -> true, vtyp
+         | Local (Mutable, vtyp) | Register vtyp -> false, vtyp
+       in
+       let access = infer_exp env (E_aux (E_app (mk_id "vector_subrange", [E_aux (E_id v, (l, ())); exp1; exp2]), (l, ()))) in
+       let E_aux (E_app (_, [_; inferred_exp1; inferred_exp2]), _) = access in
+       match typ_of access with
+       | Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_typ deref_typ, _)]), _) when string_of_id id = "register" ->
+          subtyp l env typ deref_typ;
+          annot_lexp (LEXP_vector_range (annot_lexp_effect (LEXP_id v) vtyp (mk_effect [BE_wreg]), inferred_exp1, inferred_exp2)) typ, env
+       | _ when not is_immutable ->
+          subtyp l env typ (typ_of access);
+          annot_lexp (LEXP_vector_range (annot_lexp (LEXP_id v) vtyp, inferred_exp1, inferred_exp2)) typ, env
+       | _ -> typ_error l ("Bad vector assignment: " ^ string_of_lexp lexp)
+     end
   (* Not sure about this case... can the left lexp be anything other than an identifier? *)
   | LEXP_vector (LEXP_aux (LEXP_id v, _), exp) ->
      begin
@@ -2257,6 +2277,12 @@ and propagate_lexp_effect_aux = function
      let propagated_lexp = propagate_lexp_effect lexp in
      let propagated_exp = propagate_exp_effect exp in
      LEXP_vector (propagated_lexp, propagated_exp), union_effects (effect_of propagated_exp) (effect_of_lexp propagated_lexp)
+  | LEXP_vector_range (lexp, exp1, exp2) ->
+     let propagated_lexp = propagate_lexp_effect lexp in
+     let propagated_exp1 = propagate_exp_effect exp1 in
+     let propagated_exp2 = propagate_exp_effect exp2 in
+     LEXP_vector_range (propagated_lexp, propagated_exp1, propagated_exp2),
+     union_effects (collect_effects [propagated_exp1; propagated_exp2]) (effect_of_lexp propagated_lexp)
   | LEXP_field (lexp, id) ->
      let propagated_lexp = propagate_lexp_effect lexp in
      LEXP_field (propagated_lexp, id),effect_of_lexp propagated_lexp
diff --git a/test/typecheck/fail/set_spsr1.sail b/test/typecheck/fail/set_spsr1.sail
new file mode 100644
index 00000000..27c343b2
--- /dev/null
+++ b/test/typecheck/fail/set_spsr1.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
+  (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
+  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec
+
+overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
+
+register bit[32] SPSR_EL2
+
+function unit set_SPSR_hyp (bit[32]) val_name =
+{
+  (bit[32]) r := val_name;
+  SPSR_EL2[30..0] := r
+}
diff --git a/test/typecheck/fail/set_spsr2.sail b/test/typecheck/fail/set_spsr2.sail
new file mode 100644
index 00000000..00493444
--- /dev/null
+++ b/test/typecheck/fail/set_spsr2.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
+  (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
+  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec
+
+overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
+
+register bit[32] SPSR_EL2
+
+function unit set_SPSR_hyp (bit[32]) val_name =
+{
+  (bit[32]) r := val_name;
+  SPSR_EL2[0..31] := r
+}
diff --git a/test/typecheck/fail/set_spsr3.sail b/test/typecheck/fail/set_spsr3.sail
new file mode 100644
index 00000000..c3a6208e
--- /dev/null
+++ b/test/typecheck/fail/set_spsr3.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
+  (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
+  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec
+
+overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
+
+register bit[32] SPSR_EL2
+
+function unit set_SPSR_hyp (bit[32]) val_name =
+{
+  (bit[32]) r := val_name;
+  SPSR_EL2[32..1] := r
+}
diff --git a/test/typecheck/fail/set_spsr4.sail b/test/typecheck/fail/set_spsr4.sail
new file mode 100644
index 00000000..65596b59
--- /dev/null
+++ b/test/typecheck/fail/set_spsr4.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
+  (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
+  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec
+
+overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
+
+register bit[31] SPSR_EL2
+
+function unit set_SPSR_hyp (bit[32]) val_name =
+{
+  (bit[32]) r := val_name;
+  SPSR_EL2[31..0] := r
+}
diff --git a/test/typecheck/fail/set_spsr5.sail b/test/typecheck/fail/set_spsr5.sail
new file mode 100644
index 00000000..d8a6588c
--- /dev/null
+++ b/test/typecheck/fail/set_spsr5.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
+  (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
+  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec
+
+overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
+
+register bit[32] SPSR_EL2
+
+function unit set_SPSR_hyp (bit[16]) val_name =
+{
+  (bit[32]) r := val_name;
+  SPSR_EL2[31..0] := r
+}
diff --git a/test/typecheck/pass/set_spsr.sail b/test/typecheck/pass/set_spsr.sail
new file mode 100644
index 00000000..b30343a2
--- /dev/null
+++ b/test/typecheck/pass/set_spsr.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l.
+  (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1.
+  (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec
+
+overload vector_subrange [vector_subrange_inc; vector_subrange_dec]
+
+register bit[32] SPSR_EL2
+
+function unit set_SPSR_hyp (bit[32]) val_name =
+{
+  (bit[32]) r := val_name;
+  SPSR_EL2[31..0] := r
+}
diff --git a/test/typecheck/pass/simple_scattered.sail b/test/typecheck/pass/simple_scattered.sail
new file mode 100644
index 00000000..41479888
--- /dev/null
+++ b/test/typecheck/pass/simple_scattered.sail
@@ -0,0 +1,20 @@
+
+default Order dec
+
+scattered typedef ast = const union forall Num 'datasize, Num 'destsize, Num 'regsize.
+
+val forall Num 'datasize, Num 'destsize, Num 'regsize.
+  ast<'datasize,'destsize,'regsize> -> unit effect pure execute
+
+scattered function forall Num 'datasize, Num 'destsize, Num 'regsize. unit execute
+
+union ast member (bit[8], bit['regsize]) test
+
+function clause execute (test (x, y)) =
+{
+  return ()
+}
+
+end ast
+
+end execute
diff --git a/test/typecheck/pass/simple_scattered2.sail b/test/typecheck/pass/simple_scattered2.sail
new file mode 100644
index 00000000..8cd26e95
--- /dev/null
+++ b/test/typecheck/pass/simple_scattered2.sail
@@ -0,0 +1,27 @@
+
+default Order dec
+
+scattered typedef ast = const union forall Num 'datasize, Num 'destsize, Num 'regsize.
+
+val forall Num 'datasize, Num 'destsize, Num 'regsize.
+  ast<'datasize,'destsize,'regsize> -> unit effect pure execute
+
+scattered function forall Num 'datasize, Num 'destsize, Num 'regsize. unit execute
+
+union ast member (bit[8], bit['regsize]) test
+
+function clause execute (test (x, y)) =
+{
+  return ()
+}
+
+union ast member int test2
+
+function clause execute (test2(x)) =
+{
+  return ()
+}
+
+end ast
+
+end execute