Simplify flow typing code in typechecker

3 files changed, 18 insertions, 41 deletions

diff --git a/lib/ocaml_rts/sail_lib.ml b/lib/ocaml_rts/sail_lib.ml
index 6876ec35..e3a77edf 100644
--- a/lib/ocaml_rts/sail_lib.ml
+++ b/lib/ocaml_rts/sail_lib.ml
@@ -441,6 +441,9 @@ let sqrt_real x = real_of_string (string_of_float (sqrt (Num.float_of_num x)))
 let print_int (str, x) =
   prerr_endline (str ^ string_of_big_int x)
 
+let print_bits (str, xs) =
+  prerr_endline (str ^ string_of_bits xs)
+
 let reg_deref r = !r
 
 let string_of_zbit = function
diff --git a/src/type_check.ml b/src/type_check.ml
index 589a5cf7..b8af9fa1 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1819,22 +1819,10 @@ let destruct_atom (Typ_aux (typ_aux, _)) =
 
 exception Not_a_constraint;;
 
-let rec assert_nexp env (E_aux (exp_aux, _)) =
-  match exp_aux with
-  | E_sizeof nexp -> nexp
-  | E_id id ->
-     begin
-       match Env.lookup_id id env with
-       | Local (Immutable, typ) ->
-          begin
-            match destruct_atom_nexp env typ with
-            | Some nexp -> nexp
-            | None -> raise Not_a_constraint
-          end
-       | _ -> raise Not_a_constraint
-     end
-  | E_lit (L_aux (L_num n, _)) -> nconstant n
-  | _ -> raise Not_a_constraint
+let rec assert_nexp env exp =
+  match destruct_atom_nexp env (typ_of exp) with
+  | Some nexp -> nexp
+  | None -> raise Not_a_constraint
 
 let rec assert_constraint env (E_aux (exp_aux, _) as exp) =
   match exp_aux with
@@ -1898,24 +1886,8 @@ let apply_flow_constraint = function
      (restrict_range_lower c nexp,
       restrict_range_upper (pred_big_int c) (nexp_simp (nminus nexp (nconstant 1))))
 
-let rec infer_flow env (E_aux (exp_aux, (l, _))) =
+let rec infer_flow env (E_aux (exp_aux, (l, _)) as exp) =
   match exp_aux with
-  | E_app (f, [x; y]) when string_of_id f = "lteq_atom_atom" ->
-     let Some n1 = destruct_atom_nexp env (typ_of x) in
-     let Some n2 = destruct_atom_nexp env (typ_of y) in
-     [], [nc_lteq n1 n2]
-  | E_app (f, [x; y]) when string_of_id f = "gteq_atom_atom" ->
-     let Some n1 = destruct_atom_nexp env (typ_of x) in
-     let Some n2 = destruct_atom_nexp env (typ_of y) in
-     [], [nc_gteq n1 n2]
-  | E_app (f, [x; y]) when string_of_id f = "lt_atom_atom" ->
-     let Some n1 = destruct_atom_nexp env (typ_of x) in
-     let Some n2 = destruct_atom_nexp env (typ_of y) in
-     [], [nc_lt n1 n2]
-  | E_app (f, [x; y]) when string_of_id f = "gt_atom_atom" ->
-     let Some n1 = destruct_atom_nexp env (typ_of x) in
-     let Some n2 = destruct_atom_nexp env (typ_of y) in
-     [], [nc_gt n1 n2]
   | E_app (f, [E_aux (E_id v, _); y]) when string_of_id f = "lt_range_atom" ->
      let kid = Env.fresh_kid env in
      begin
@@ -1946,7 +1918,7 @@ let rec infer_flow env (E_aux (exp_aux, (l, _))) =
        | Some (c, nexp) -> [(v, Flow_gteq (c, nexp))], []
        | _ -> [], []
      end
-  | _ -> [], []
+  | _ -> try [], [assert_constraint env exp] with Not_a_constraint -> [], []
 
 let rec add_flows b flows env =
   match flows with
diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail
index cf9bb2f6..b56ce7e2 100644
--- a/test/ocaml/prelude.sail
+++ b/test/ocaml/prelude.sail
@@ -4,11 +4,11 @@ type bits ('n : Int) = vector('n - 1, 'n, dec, bit)
 
 infix 4 ==
 
-val eq_atom = "eq_int" : (atom('n), atom('m)) -> bool
-val lteq_atom = "lteq" : (atom('n), atom('m)) -> bool
-val gteq_atom = "gteq" : (atom('n), atom('m)) -> bool
-val lt_atom = "lt" : (atom('n), atom('m)) -> bool
-val gt_atom = "gt" : (atom('n), atom('m)) -> bool
+val eq_atom = "eq_int" : forall 'n 'm. (atom('n), atom('m)) -> bool
+val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
+val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
+val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool
+val gt_atom = "gt" : forall 'n 'm. (atom('n), atom('m)) -> bool
 
 val eq_int = "eq_int" : (int, int) -> bool
 
@@ -173,7 +173,7 @@ val sub_vec_int = "sub_vec_int" : forall 'n. (bits('n), int) -> bits('n)
 
 val sub_real = "sub_real" : (real, real) -> real
 
-val negate_range = "minus_big_int" : forall 'n. range('n, 'm) -> range(- 'm, - 'n)
+val negate_range = "minus_big_int" : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n)
 
 val negate_int = "minus_big_int" : int -> int
 
@@ -283,4 +283,6 @@ val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0.
 
 val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
 
-val print_int = "print_int" : (string, int) -> unit
+val "print_int" : (string, int) -> unit
+
+val "print_bits" : forall 'n. (string, bits('n)) -> unit
\ No newline at end of file