A few additional tests

5 files changed, 94 insertions, 1 deletions

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 43fa3719..65702764 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -139,6 +139,8 @@ let rec ctyp_of_typ ctx typ =
   | Typ_id id when string_of_id id = "string" -> CT_string
   | Typ_id id when string_of_id id = "real"   -> CT_real
 
+  | Typ_app (id, _) when string_of_id id = "atom_bool" -> CT_bool
+
   | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" ->
      begin match destruct_range Env.empty typ with
      | None -> assert false (* Checked if range type in guard *)
diff --git a/src/type_check.ml b/src/type_check.ml
index 3cfa4bb6..df074567 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -264,7 +264,6 @@ let destruct_exist typ =
   | Some (kids, nc, nexp) -> Some (List.map (mk_kopt K_int) kids, nc, atom_typ nexp)
   | None -> destruct_exist' typ
 
-
 let adding = Util.("Adding " |> darkgray |> clear)
 
 (**************************************************************************)
@@ -1327,6 +1326,7 @@ and typ_arg_frees ?exs:(exs=KidSet.empty) (A_aux (typ_arg_aux, l)) =
   | A_nexp n -> nexp_frees ~exs:exs n
   | A_typ typ -> typ_frees ~exs:exs typ
   | A_order ord -> order_frees ord
+  | A_bool nc -> tyvars_of_constraint nc
 
 let rec nexp_identical (Nexp_aux (nexp1, _)) (Nexp_aux (nexp2, _)) =
   match nexp1, nexp2 with
diff --git a/test/c/custom_flow.expect b/test/c/custom_flow.expect
new file mode 100644
index 00000000..cf275436
--- /dev/null
+++ b/test/c/custom_flow.expect
@@ -0,0 +1,5 @@
+1
+2
+3
+4
+4
diff --git a/test/c/custom_flow.sail b/test/c/custom_flow.sail
new file mode 100644
index 00000000..43c980d6
--- /dev/null
+++ b/test/c/custom_flow.sail
@@ -0,0 +1,43 @@
+val "print_endline" : string -> unit
+
+val operator <= = {
+  coq: "Z.leb",
+  _: "lteq"
+} : forall 'n 'm. (int('n), int('m)) -> bool('n <= 'm)
+
+function test1 forall 'n 'm. (n: int('n), m: int('m)) -> unit = {
+  if n <= m then {
+    _prove(constraint('n <= 'm));
+    print_endline("1");
+  } else {
+    print_endline("2");
+    _prove(constraint('n > 'm));
+  }
+}
+
+val and_bool = {
+  coq: "andb",
+  _: "and_bool"
+} : forall ('p: Bool) ('q: Bool). (bool('p), bool('q)) -> bool('p & 'q)
+
+overload operator & = {and_bool}
+
+function test2 forall 'n 'm. (n: int('n), m: int('m)) -> unit = {
+  let x = n <= m & n <= 20;
+  if x then {
+    _prove(constraint('n <= 20));
+    _prove(constraint('n <= 'm));
+    print_endline("3")
+  } else {
+    _prove(constraint('n > 'm | 'n > 20));
+    print_endline("4")
+  }
+}
+
+function main((): unit) -> unit = {
+  test1(1, 2);
+  test1(2, 1);
+  test2(1, 2);
+  test2(2, 1);
+  test2(21, 0)
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/custom_flow.sail b/test/typecheck/pass/custom_flow.sail
new file mode 100644
index 00000000..43c980d6
--- /dev/null
+++ b/test/typecheck/pass/custom_flow.sail
@@ -0,0 +1,43 @@
+val "print_endline" : string -> unit
+
+val operator <= = {
+  coq: "Z.leb",
+  _: "lteq"
+} : forall 'n 'm. (int('n), int('m)) -> bool('n <= 'm)
+
+function test1 forall 'n 'm. (n: int('n), m: int('m)) -> unit = {
+  if n <= m then {
+    _prove(constraint('n <= 'm));
+    print_endline("1");
+  } else {
+    print_endline("2");
+    _prove(constraint('n > 'm));
+  }
+}
+
+val and_bool = {
+  coq: "andb",
+  _: "and_bool"
+} : forall ('p: Bool) ('q: Bool). (bool('p), bool('q)) -> bool('p & 'q)
+
+overload operator & = {and_bool}
+
+function test2 forall 'n 'm. (n: int('n), m: int('m)) -> unit = {
+  let x = n <= m & n <= 20;
+  if x then {
+    _prove(constraint('n <= 20));
+    _prove(constraint('n <= 'm));
+    print_endline("3")
+  } else {
+    _prove(constraint('n > 'm | 'n > 20));
+    print_endline("4")
+  }
+}
+
+function main((): unit) -> unit = {
+  test1(1, 2);
+  test1(2, 1);
+  test2(1, 2);
+  test2(2, 1);
+  test2(21, 0)
+}
\ No newline at end of file