Support monomorphisation with set constrained integers

Also, to support this,
constant propagation for integer multiply,
fix substitution of concrete values for nvars,
size parameters in single argument functions,
fix kind for itself,
add eq_atom to prelude

5 files changed, 68 insertions, 15 deletions

diff --git a/lib/prelude.sail b/lib/prelude.sail
index 92bfb180..a7f6fb2f 100644
--- a/lib/prelude.sail
+++ b/lib/prelude.sail
@@ -266,6 +266,8 @@ overload (deinfix |) [or_bool; bitwise_or]
 
 val extern forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure eq_vec
 
+val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure eq_atom = "eq"
+
 val extern forall Type 'a. ('a, 'a) -> bool effect pure eq
 
 val extern forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure neq_vec
@@ -274,7 +276,7 @@ val extern forall Type 'a. ('a, 'a) -> bool effect pure neq
 
 (*function forall Num 'n, Num 'm, Order 'ord. bool neq_vec (v1, v2) = bool_not(eq_vec(v1, v2))*)
 
-overload (deinfix ==) [eq_vec; eq]
+overload (deinfix ==) [eq_vec; eq_atom; eq]
 overload (deinfix !=) [neq_vec; neq]
 
 val extern forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gteq_vec
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index fa284ffb..05b9efcb 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -494,24 +494,23 @@ let nexp_subst_fns substs =
     | None -> None
     | Some (env,t,eff) -> Some (env,s_t t,eff) (* TODO: what about env? *)
   in
-(*  let rec s_pat (P_aux (p,(l,annot))) =
-    let re p = P_aux (p,(l,(*s_tannot*) annot)) in
+  let rec s_pat (P_aux (p,(l,annot))) =
+    let re p = P_aux (p,(l,s_tannot annot)) in
     match p with
     | P_lit _ | P_wild | P_id _ -> re p
-    | P_var kid -> re p
+    | P_var (p',kid) -> re (P_var (s_pat p',kid))
     | P_as (p',id) -> re (P_as (s_pat p', id))
-    | P_typ (ty,p') -> re (P_typ (ty,s_pat p'))
+    | P_typ (ty,p') -> re (P_typ (s_t ty,s_pat p'))
     | P_app (id,ps) -> re (P_app (id, List.map s_pat ps))
     | P_record (fps,flag) -> re (P_record (List.map s_fpat fps, flag))
     | P_vector ps -> re (P_vector (List.map s_pat ps))
-    | P_vector_indexed ips -> re (P_vector_indexed (List.map (fun (i,p) -> (i,s_pat p)) ips))
     | P_vector_concat ps -> re (P_vector_concat (List.map s_pat ps))
     | P_tup ps -> re (P_tup (List.map s_pat ps))
     | P_list ps -> re (P_list (List.map s_pat ps))
     | P_cons (p1,p2) -> re (P_cons (s_pat p1, s_pat p2))
   and s_fpat (FP_aux (FP_Fpat (id, p), (l,annot))) =
     FP_aux (FP_Fpat (id, s_pat p), (l,s_tannot annot))
-  in*)
+  in
   let rec s_exp (E_aux (e,(l,annot))) =
     let re e = E_aux (e,(l,s_tannot annot)) in
       match e with
@@ -526,7 +525,7 @@ let nexp_subst_fns substs =
       | E_sizeof_internal (l,annot) -> re (E_sizeof_internal (l, s_tannot annot))
       | E_internal_exp_user ((l1,annot1),(l2,annot2)) ->
          re (E_internal_exp_user ((l1, s_tannot annot1),(l2, s_tannot annot2)))
-      | E_cast (t,e') -> re (E_cast (t, s_exp e'))
+      | E_cast (t,e') -> re (E_cast (s_t t, s_exp e'))
       | E_app (id,es) -> re (E_app (id, List.map s_exp es))
       | E_app_infix (e1,id,e2) -> re (E_app_infix (s_exp e1,id,s_exp e2))
       | E_tuple es -> re (E_tuple (List.map s_exp es))
@@ -553,7 +552,7 @@ let nexp_subst_fns substs =
       | E_internal_cast ((l,ann),e) -> re (E_internal_cast ((l,s_tannot ann),s_exp e))
       | E_comment_struc e -> re (E_comment_struc e)
       | E_internal_let (le,e1,e2) -> re (E_internal_let (s_lexp le, s_exp e1, s_exp e2))
-      | E_internal_plet (p,e1,e2) -> re (E_internal_plet ((*s_pat*) p, s_exp e1, s_exp e2))
+      | E_internal_plet (p,e1,e2) -> re (E_internal_plet (s_pat p, s_exp e1, s_exp e2))
       | E_internal_return e -> re (E_internal_return (s_exp e))
       | E_throw e -> re (E_throw (s_exp e))
       | E_try (e,cases) -> re (E_try (s_exp e, List.map s_pexp cases))
@@ -567,12 +566,12 @@ let nexp_subst_fns substs =
       FE_aux (FE_Fexp (id,s_exp e),(l,s_tannot annot))
     and s_pexp = function
       | (Pat_aux (Pat_exp (p,e),(l,annot))) ->
-         Pat_aux (Pat_exp ((*s_pat*) p, s_exp e),(l,s_tannot annot))
+         Pat_aux (Pat_exp (s_pat p, s_exp e),(l,s_tannot annot))
       | (Pat_aux (Pat_when (p,e1,e2),(l,annot))) ->
-         Pat_aux (Pat_when ((*s_pat*) p, s_exp e1, s_exp e2),(l,s_tannot annot))
+         Pat_aux (Pat_when (s_pat p, s_exp e1, s_exp e2),(l,s_tannot annot))
     and s_letbind (LB_aux (lb,(l,annot))) =
       match lb with
-      | LB_val (p,e) -> LB_aux (LB_val ((*s_pat*) p,s_exp e), (l,s_tannot annot))
+      | LB_val (p,e) -> LB_aux (LB_val (s_pat p,s_exp e), (l,s_tannot annot))
     and s_lexp (LEXP_aux (e,(l,annot))) =
       let re e = LEXP_aux (e,(l,s_tannot annot)) in
       match e with
@@ -583,7 +582,7 @@ let nexp_subst_fns substs =
       | LEXP_vector (le,e) -> re (LEXP_vector (s_lexp le, s_exp e))
       | LEXP_vector_range (le,e1,e2) -> re (LEXP_vector_range (s_lexp le, s_exp e1, s_exp e2))
       | LEXP_field (le,id) -> re (LEXP_field (s_lexp le, id))
-  in ((fun x -> x (*s_pat*)),s_exp)
+  in (s_pat,s_exp)
 let nexp_subst_pat substs = fst (nexp_subst_fns substs)
 let nexp_subst_exp substs = snd (nexp_subst_fns substs)
 
@@ -707,6 +706,11 @@ let try_app (l,ann) (id,args) =
     | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] ->
        Some (E_aux (E_lit (L_aux (L_num (shift_left_big_int i (int_of_big_int j)),new_l)),(l,ann)))
     | _ -> None
+  else if is_id "mult_int" then
+    match args with
+    | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] ->
+       Some (E_aux (E_lit (L_aux (L_num (mult_big_int i j),new_l)),(l,ann)))
+    | _ -> None
   else if is_id "ex_int" then
     match args with
     | [E_aux (E_lit lit,(l,_))] -> Some (E_aux (E_lit lit,(l,ann)))
@@ -1240,7 +1244,22 @@ let split_defs splits defs =
        | _ ->
           cannot ()
        )
-    (*|  set constrained numbers TODO *)
+    (* set constrained numbers *)
+    | Typ_app (Id_aux (Id "atom",_), [Typ_arg_aux (Typ_arg_nexp Nexp_aux (value,_),_)]) ->
+       begin
+         let mk_lit i =
+            let lit = L_aux (L_num i,new_l) in
+            P_aux (P_lit lit,(l,annot)),
+            [var,E_aux (E_lit lit,(new_l,annot))]
+         in
+         match value with
+         | Nexp_constant i -> [mk_lit i]
+         | Nexp_var kvar ->
+           let ncs = Env.get_constraints env in
+           let nc = List.fold_left nc_and nc_true ncs in
+           List.map mk_lit (fst (extract_set_nc kvar nc))
+         | _ -> cannot ()
+       end
     | _ -> cannot ()
   in
   
@@ -1781,6 +1800,8 @@ let rewrite_size_parameters env (Defs defs) =
                  let typ = match typ with
                    | Typ_aux (Typ_fn (Typ_aux (Typ_tup ts,l),t2,eff),l2) ->
                       Typ_aux (Typ_fn (Typ_aux (Typ_tup (mapat (replace_type env) to_change ts),l),t2,eff),l2)
+                   | Typ_aux (Typ_fn (typ,t2,eff),l2) ->
+                      Typ_aux (Typ_fn (replace_type env typ,t2,eff),l2)
                    | _ -> replace_type env typ
                  in TypSchm_aux (TypSchm_ts (tq,typ),l)
             in
diff --git a/src/type_check.ml b/src/type_check.ml
index 69d1dcb2..05ba8b66 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -434,7 +434,7 @@ end = struct
         ("real", []);
         ("list", [BK_type]);
         ("string", []);
-        ("itself", [BK_type])
+        ("itself", [BK_nat])
       ]
 
   let bound_typ_id env id =
diff --git a/test/mono/set.sail b/test/mono/set.sail
new file mode 100644
index 00000000..ecc06137
--- /dev/null
+++ b/test/mono/set.sail
@@ -0,0 +1,29 @@
+default Order dec
+
+(* A function which is merely parametrised by a size does not need to be
+   monomorphised *)
+
+val forall 'n, 'n in {32,64}. [:'n:] -> bit[64] effect pure parametric
+
+function parametric(n) = {
+  let (bit['n]) x = exts(0x80000000) in
+  extz(x)
+}
+
+(* But if we do a calculation on the size then we'll need to case split *)
+
+val forall 'n, 'n in {16,32}. [:'n:] -> bit[64] effect pure depends
+
+function depends(n) = {
+  let 'm = 2 * n in
+  let (bit['m]) x = exts(0x80000000) in
+  extz(x)
+}
+
+val unit -> bool effect pure run
+
+function run () =
+  parametric(32) == 0x0000000080000000 &
+  parametric(64) == 0xffffffff80000000 &
+  depends(16) == 0x0000000080000000 &
+  depends(32) == 0xffffffff80000000
diff --git a/test/mono/tests b/test/mono/tests
index b589afe0..27e161cf 100644
--- a/test/mono/tests
+++ b/test/mono/tests
@@ -6,3 +6,4 @@ fnreduce -auto_mono
 varmatch -auto_mono
 vector -auto_mono
 union-exist -auto_mono
+set -auto_mono