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.

1 files changed, 2 insertions, 3 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)]