More OCaml test cases

Improved handling of try/catch

Better handling of unprovable constraints when the environment contains
false

5 files changed, 13 insertions, 4 deletions

diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index e56060da..ac6f6ef3 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -112,6 +112,7 @@ let ocaml_string_comma = string " ^ \", \" ^ "
 
 let rec ocaml_string_typ (Typ_aux (typ_aux, _)) arg =
   match typ_aux with
+  | Typ_id id when string_of_id id = "exception" -> string "Printexc.to_string" ^^ space ^^ arg
   | Typ_id id -> ocaml_string_of id ^^ space ^^ arg
   | Typ_app (id, []) -> ocaml_string_of id ^^ space ^^ arg
   | Typ_app (id, [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id eid, _)), _)])
@@ -199,6 +200,7 @@ let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) =
   | P_list pats -> brackets (separate_map (semi ^^ space) (ocaml_pat ctx) pats)
   | P_wild -> string "_"
   | P_as (pat, id) -> separate space [ocaml_pat ctx pat; string "as"; zencode ctx id]
+  | P_app (id, pats) -> zencode_upper ctx id ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_pat ctx) pats)
   | _ -> string ("PAT<" ^ string_of_pat pat ^ ">")
 
 let begin_end doc = group (string "begin" ^^ nest 2 (break 1 ^^ doc) ^/^ string "end")
@@ -234,6 +236,9 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
   | E_case (exp, pexps) ->
      begin_end (separate space [string "match"; ocaml_atomic_exp ctx exp; string "with"]
                 ^/^ ocaml_pexps ctx pexps)
+  | E_try (exp, pexps) ->
+     begin_end (separate space [string "try"; ocaml_atomic_exp ctx exp; string "with"]
+                ^/^ ocaml_pexps ctx pexps)
   | E_assign (lexp, exp) -> ocaml_assignment ctx lexp exp
   | E_if (c, t, e) -> separate space [string "if"; ocaml_atomic_exp ctx c;
                                       string "then"; ocaml_atomic_exp ctx t;
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 3063b73d..88fb17a5 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -509,6 +509,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
   ; e_record_update          : 'exp * 'fexps -> 'exp_aux
   ; e_field                  : 'exp * id -> 'exp_aux
   ; e_case                   : 'exp * 'pexp list -> 'exp_aux
+  ; e_try                    : 'exp * 'pexp list -> 'exp_aux
   ; e_let                    : 'letbind * 'exp -> 'exp_aux
   ; e_assign                 : 'lexp * 'exp -> 'exp_aux
   ; e_sizeof                 : nexp -> 'exp_aux
@@ -578,6 +579,7 @@ let rec fold_exp_aux alg = function
   | E_record_update (e,fexps) -> alg.e_record_update (fold_exp alg e, fold_fexps alg fexps)
   | E_field (e,id) -> alg.e_field (fold_exp alg e, id)
   | E_case (e,pexps) -> alg.e_case (fold_exp alg e, List.map (fold_pexp alg) pexps)
+  | E_try (e,pexps) -> alg.e_try (fold_exp alg e, List.map (fold_pexp alg) pexps)
   | E_let (letbind,e) -> alg.e_let (fold_letbind alg letbind, fold_exp alg e)
   | E_assign (lexp,e) -> alg.e_assign (fold_lexp alg lexp, fold_exp alg e)
   | E_sizeof nexp -> alg.e_sizeof nexp
@@ -651,6 +653,7 @@ let id_exp_alg =
   ; e_record_update = (fun (e1,fexp) -> E_record_update (e1,fexp))
   ; e_field = (fun (e1,id) -> (E_field (e1,id)))
   ; e_case = (fun (e1,pexps) -> E_case (e1,pexps))
+  ; e_try = (fun (e1,pexps) -> E_try (e1,pexps))
   ; e_let = (fun (lb,e2) -> E_let (lb,e2))
   ; e_assign = (fun (lexp,e2) -> E_assign (lexp,e2))
   ; e_sizeof = (fun nexp -> E_sizeof nexp)
@@ -747,6 +750,9 @@ let compute_exp_alg bot join =
   ; e_case = (fun ((v1,e1),pexps) ->
     let (vps,pexps) = List.split pexps in
     (join_list (v1::vps), E_case (e1,pexps)))
+  ; e_try = (fun ((v1,e1),pexps) ->
+    let (vps,pexps) = List.split pexps in
+    (join_list (v1::vps), E_try (e1,pexps)))
   ; e_let = (fun ((vl,lb),(v2,e2)) -> (join vl v2, E_let (lb,e2)))
   ; e_assign = (fun ((vl,lexp),(v2,e2)) -> (join vl v2, E_assign (lexp,e2)))
   ; e_sizeof = (fun nexp -> (bot, E_sizeof nexp))
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 6f8c6396..dc592a4d 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -128,6 +128,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
  ; e_record_update          : 'exp * 'fexps -> 'exp_aux
  ; e_field                  : 'exp * id -> 'exp_aux
  ; e_case                   : 'exp * 'pexp list -> 'exp_aux
+ ; e_try                    : 'exp * 'pexp list -> 'exp_aux
  ; e_let                    : 'letbind * 'exp -> 'exp_aux
  ; e_assign                 : 'lexp * 'exp -> 'exp_aux
  ; e_sizeof                 : nexp -> 'exp_aux
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 738d0d20..424931c3 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -349,6 +349,7 @@ let rewrite_sizeof (Defs defs) =
     ; e_record_update = (fun ((e1,e1'),(fexp,fexp')) -> (E_record_update (e1,fexp), E_record_update (e1',fexp')))
     ; e_field = (fun ((e1,e1'),id) -> (E_field (e1,id), E_field (e1',id)))
     ; e_case = (fun ((e1,e1'),pexps) -> let (pexps, pexps') = List.split pexps in (E_case (e1,pexps), E_case (e1',pexps')))
+    ; e_try = (fun ((e1,e1'),pexps) -> let (pexps, pexps') = List.split pexps in (E_try (e1,pexps), E_try (e1',pexps')))
     ; e_let = (fun ((lb,lb'),(e2,e2')) -> (E_let (lb,e2), E_let (lb',e2')))
     ; e_assign = (fun ((lexp,lexp'),(e2,e2')) -> (E_assign (lexp,e2), E_assign (lexp',e2')))
     ; e_sizeof = (fun nexp -> (E_sizeof nexp, E_sizeof nexp))
diff --git a/src/type_check.ml b/src/type_check.ml
index d91a46cd..5bd633ee 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1182,11 +1182,7 @@ let prove env (NC_aux (nc_aux, _) as nc) =
   | NC_equal (nexp1, nexp2) when compare_const eq_big_int (nexp_simp nexp1) (nexp_simp nexp2) -> true
   | NC_bounded_le (nexp1, nexp2) when compare_const le_big_int (nexp_simp nexp1) (nexp_simp nexp2) -> true
   | NC_bounded_ge (nexp1, nexp2) when compare_const ge_big_int (nexp_simp nexp1) (nexp_simp nexp2) -> true
-  | NC_equal (nexp1, nexp2) when compare_const (fun c1 c2 -> not (eq_big_int c1 c2)) (nexp_simp nexp1) (nexp_simp nexp2) -> false
-  | NC_bounded_le (nexp1, nexp2) when compare_const gt_big_int (nexp_simp nexp1) (nexp_simp nexp2) -> false
-  | NC_bounded_ge (nexp1, nexp2) when compare_const lt_big_int (nexp_simp nexp1) (nexp_simp nexp2) -> false
   | NC_true -> true
-  | NC_false -> false
   | _ -> prove_z3 env nc
 
 let rec subtyp_tnf env tnf1 tnf2 =