Fix regressions in OCaml output

Recent patches have made the rewriter more strict about performing
type correct rewrites. This is mostly a good thing but did cause some
problems with the ocaml backend.

Currently the sizeof rewriter doesn't seem to preserve type
correctness - I suspect this is because when it resolves the sizeofs,
it generates constraints that are true, but not in a form where the
typechecker can see that they are true. I disabled the re-check after
the sizeof rewriting pass to fix this. Maybe we don't want to do this
anyway because it's slow.

Changes to function clauses with guards + monomorphisation changed how
the typechecker handles literal patterns. I added a rewriting pass to
rewrite literals to guarded equality checks, which is run before
generating ocaml.

The rewriter currently uses Env.empty in a view places. This can cause
bugs because Env.empty is a totally unitialised environment that
doesn't satisfy invariants we expect of an environment. This should be
changed to initial_env and it shouldn't be exported, I fixed a few
cases where this caused things to go wrong, but it should probably not
be exported from Type_check.ml.

5 files changed, 61 insertions, 14 deletions

diff --git a/src/process_file.ml b/src/process_file.ml
index 2d2cbe76..68e5786e 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -229,9 +229,8 @@ let rewrite_step defs (name,rewriter) =
 
 let rewrite rewriters defs =
   try List.fold_left rewrite_step defs rewriters with
-  | Type_check.Type_error (_, err) ->
-     prerr_endline (Type_check.string_of_type_error err);
-     exit 1
+  | Type_check.Type_error (l, err) ->
+     raise (Reporting_basic.err_typ l (Type_check.string_of_type_error err))
 
 let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
 let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined !opt_lem_mwords x)]
diff --git a/src/rewriter.ml b/src/rewriter.ml
index abe351d4..3063b73d 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -80,7 +80,7 @@ let effect_of_pexp (Pat_aux (pexp,(_,a))) = match a with
     | Pat_when (_, g, e) -> union_effects (effect_of g) (effect_of e))
 let effect_of_lb (LB_aux (_,(_,a))) = effect_of_annot a
 
-let simple_annot l typ = (gen_loc l, Some (Env.empty, typ, no_effect))
+let simple_annot l typ = (gen_loc l, Some (initial_env, typ, no_effect))
 
 let rec small (E_aux (exp,_)) = match exp with
   | E_id _
@@ -265,12 +265,12 @@ let rewrite_pexp rewriters =
   | (Pat_aux (Pat_when(p, e, e'), pannot)) ->
      Pat_aux (Pat_when(rewriters.rewrite_pat rewriters p, rewrite e, rewrite e'), pannot)
 
-let rewrite_pat rewriters (P_aux (pat,(l,annot))) =
+let rewrite_pat rewriters (P_aux (pat,(l,annot)) as orig_pat) =
   let rewrap p = P_aux (p,(l,annot)) in
   let rewrite = rewriters.rewrite_pat rewriters in
   match pat with
   | P_lit (L_aux ((L_hex _ | L_bin _) as lit,_)) ->
-    let ps =  List.map (fun p -> P_aux (P_lit p, simple_annot l bit_typ))
+    let ps =  List.map (fun p -> P_aux (P_lit p, (l, Some (pat_env_of orig_pat, bit_typ, no_effect))))
         (vector_string_to_bit_list l lit) in
     rewrap (P_vector ps)
   | P_lit _ | P_wild | P_id _ | P_var _ -> rewrap pat
@@ -286,7 +286,7 @@ let rewrite_pat rewriters (P_aux (pat,(l,annot))) =
   | P_list pats -> rewrap (P_list (List.map rewrite pats))
   | P_cons (pat1, pat2) -> rewrap (P_cons (rewrite pat1, rewrite pat2))
 
-let rewrite_exp rewriters (E_aux (exp,(l,annot))) =
+let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) =
   let rewrap e = E_aux (e,(l,annot)) in
   let rewrite = rewriters.rewrite_exp rewriters in
   match exp with
@@ -294,7 +294,7 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot))) =
   | E_block exps -> rewrap (E_block (List.map rewrite exps))
   | E_nondet exps -> rewrap (E_nondet (List.map rewrite exps))
   | E_lit (L_aux ((L_hex _ | L_bin _) as lit,_)) ->
-    let es = List.map (fun p -> E_aux (E_lit p, simple_annot l bit_typ))
+    let es = List.map (fun p -> E_aux (E_lit p, (l, Some (env_of orig_exp, bit_typ, no_effect))))
         (vector_string_to_bit_list l lit) in
     rewrap (E_vector es)
   | E_id _ | E_lit _  -> rewrap exp
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 280c67c6..738d0d20 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -512,7 +512,8 @@ let rewrite_sizeof (Defs defs) =
   let (params_map, defs) = List.fold_left rewrite_sizeof_def
                                           (Bindings.empty, []) defs in
   let defs = List.map (rewrite_sizeof_valspec params_map) defs in
-  fst (check initial_env (Defs defs))
+  Defs defs
+(* fst (check initial_env (Defs defs)) *)
 
 let rewrite_defs_remove_assert defs =
   let e_assert ((E_aux (eaux, (l, _)) as exp), str) = match eaux with
@@ -1863,8 +1864,10 @@ let rewrite_constraint =
     | NC_or (nc1, nc2) -> E_app_infix (rewrite_nc nc1, mk_id "|", rewrite_nc nc2)
     | NC_false -> E_lit (mk_lit L_false)
     | NC_true -> E_lit (mk_lit L_true)
-    | NC_set (kid, ints) ->
-       unaux_exp (rewrite_nc (List.fold_left (fun nc int -> nc_or nc (nc_eq (nvar kid) (nconstant int))) nc_true ints))
+    | NC_set (kid, []) -> E_lit (mk_lit (L_false))
+    | NC_set (kid, int :: ints) ->
+       let kid_eq kid int = nc_eq (nvar kid) (nconstant int) in
+       unaux_exp (rewrite_nc (List.fold_left (fun nc int -> nc_or nc (kid_eq kid int)) (kid_eq kid int) ints))
   in
   let rewrite_e_aux (E_aux (e_aux, _) as exp) =
     match e_aux with
@@ -2460,7 +2463,46 @@ let rewrite_defs_internal_lets =
     ; rewrite_defs = rewrite_defs_base
     }
 
-             
+let rewrite_defs_pat_lits =
+  let rewrite_pexp (Pat_aux (pexp_aux, annot) as pexp) =
+    let guards = ref [] in
+    let counter = ref 0 in
+
+    let rewrite_pat = function
+      | P_lit lit, p_annot ->
+         let env = env_of_annot p_annot in
+         let typ = typ_of_annot p_annot in
+         let id = mk_id ("p" ^ string_of_int !counter ^ "#") in
+         let guard = mk_exp (E_app_infix (mk_exp (E_id id), mk_id "==", mk_exp (E_lit lit))) in
+         let guard = check_exp (Env.add_local id (Immutable, typ) env) guard bool_typ in
+         guards := guard :: !guards;
+         incr counter;
+         P_aux (P_id id, p_annot)
+      | p_aux, p_annot -> P_aux (p_aux, p_annot)
+    in
+
+    match pexp_aux with
+    | Pat_exp (pat, exp) ->
+       begin
+         let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat } pat in
+         match !guards with
+         | [] -> pexp
+         | (g :: gs) ->
+            let guard_annot = (fst annot, Some (env_of exp, bool_typ, no_effect)) in
+            Pat_aux (Pat_when (pat, List.fold_left (fun g g' -> E_aux (E_app (mk_id "and_bool", [g; g']), guard_annot)) g gs, exp), annot)
+       end
+    | Pat_when (pat, guard, exp) ->
+       begin
+         let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat } pat in
+         let guard_annot = (fst annot, Some (env_of exp, bool_typ, no_effect)) in
+         Pat_aux (Pat_when (pat, List.fold_left (fun g g' -> E_aux (E_app (mk_id "and_bool", [g; g']), guard_annot)) guard !guards, exp), annot)
+       end
+  in
+
+  let alg = { id_exp_alg with pat_aux = (fun (pexp_aux, annot) -> rewrite_pexp (Pat_aux (pexp_aux, annot))) } in
+  rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) }
+
+
 (* Now all expressions have no blocks anymore, any term is a sequence of let-expressions,
  * internal let-expressions, or internal plet-expressions ended by a term that does not
  * access memory or registers and does not update variables *)
@@ -2901,17 +2943,19 @@ let rewrite_defs_lem = [
 
 let rewrite_defs_ocaml = [
     (* ("top_sort_defs", top_sort_defs); *)
-  (* ("undefined", rewrite_undefined); *)
+    (* ("undefined", rewrite_undefined); *)
+  ("no_effect_check", (fun defs -> opt_no_effects := true; defs));
+  ("pat_lits", rewrite_defs_pat_lits);
   ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
   ("tuple_assignments", rewrite_tuple_assignments);
   ("simple_assignments", rewrite_simple_assignments);
   ("remove_vector_concat", rewrite_defs_remove_vector_concat);
+  ("exp_lift_assign", rewrite_defs_exp_lift_assign);
   ("constraint", rewrite_constraint);
   ("trivial_sizeof", rewrite_trivial_sizeof);
   ("sizeof", rewrite_sizeof);
   ("simple_types", rewrite_simple_types);
   ("overload_cast", rewrite_overload_cast);
-  ("exp_lift_assign", rewrite_defs_exp_lift_assign);
   (* ("separate_numbs", rewrite_defs_separate_numbs) *)
   ]
 
diff --git a/src/type_check.ml b/src/type_check.ml
index 05ba8b66..c29ba9c8 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1812,6 +1812,8 @@ let rec assert_constraint env (E_aux (exp_aux, _) as exp) =
   match exp_aux with
   | E_constraint nc ->
      Some nc
+  | E_lit (L_aux (L_true, _)) -> Some nc_true
+  | E_lit (L_aux (L_false, _)) -> Some nc_true
   | E_app (op, [x; y]) when string_of_id op = "or_bool" ->
      option_binop nc_or (assert_constraint env x) (assert_constraint env y)
   | E_app (op, [x; y]) when string_of_id op = "and_bool" ->
diff --git a/src/type_check.mli b/src/type_check.mli
index a4537750..92949c85 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -95,6 +95,8 @@ module Env : sig
 
   val get_locals : t -> (mut * typ) Bindings.t
 
+  val add_local : id -> mut * typ -> t -> t
+
   (* Check if a local variable is mutable. Throws Type_error if it
      isn't a local variable. Probably best to use Env.lookup_id
      instead *)