Fix all compiler warning except in lem pretty printer and monomorphisation

7 files changed, 62 insertions, 135 deletions

diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 98efa4ce..254af4d7 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -102,6 +102,8 @@ let doc_effect (BE_aux (e,_)) =
   | BE_wmem -> "wmem"
   | BE_wmv  -> "wmv"
   | BE_wmvt  -> "wmvt"
+  | BE_lset -> "lset"
+  | BE_lret -> "lret"
   | BE_eamem -> "eamem"
   | BE_exmem -> "exmem"
   | BE_barr -> "barr"
@@ -133,51 +135,12 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
   | Typ_tup typs -> parens (separate_map comma_sp app_typ typs)
   | _ -> app_typ ty
   and app_typ ((Typ_aux (t, _)) as ty) = match t with
-  (*TODO Need to un bid-endian-ify this here, since both can transform to the shorthand, especially with <: and :> *)
-  (* Special case simple vectors to improve legibility
-   * XXX we assume big-endian here, as usual *)
-(*
-  | Typ_app(Id_aux (Id "vector", _), [
-      Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _);
-      Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant m, _)), _);
-      Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_inc, _)), _);
-      Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) ->
-    (doc_id id) ^^ (brackets (if n = 0 then doc_int m else doc_op colon (doc_int n) (doc_int (n+m-1))))
-  | Typ_app(Id_aux (Id "vector", _), [
-      Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _);
-      Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant m, _)), _);
-      Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _);
-      Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) ->
-    (doc_id id) ^^ (brackets (if n = m-1 then doc_int m else doc_op colon (doc_int n) (doc_int (m+1 -n))))
-  | Typ_app(Id_aux (Id "vector", _), [
-      Typ_arg_aux(Typ_arg_nexp
-                    (Nexp_aux(Nexp_minus (Nexp_aux(Nexp_constant n, _),
-                                          Nexp_aux(Nexp_constant 1, _)),_)),_);
-      Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant m, _)), _);
-      Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _);
-      Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) ->
-    (doc_id id) ^^ (brackets (if n = m then doc_int m else doc_op colon (doc_int m) (doc_int (n-1))))
-  | Typ_app(Id_aux (Id "vector", _), [
-      Typ_arg_aux(Typ_arg_nexp
-                    (Nexp_aux(Nexp_minus (n', Nexp_aux((Nexp_constant 1), _)),_) as n_n),_);
-      Typ_arg_aux(Typ_arg_nexp m_nexp, _);
-      Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _);
-      Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) ->
-    (doc_id id) ^^ (brackets (if n' = m_nexp then nexp m_nexp else doc_op colon (nexp m_nexp) (nexp n_n)))
-  | Typ_app(Id_aux (Id "vector", _), [
-      Typ_arg_aux(Typ_arg_nexp
-                  (Nexp_aux(Nexp_sum (n', Nexp_aux((Nexp_constant -1), _)),_) as n_n),_);
-      Typ_arg_aux(Typ_arg_nexp m_nexp, _);
-      Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _);
-      Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) ->
-    (doc_id id) ^^ (brackets (if n' = m_nexp then nexp m_nexp else doc_op colon (nexp m_nexp) (nexp n_n)))
- *)
   | Typ_app(Id_aux (Id "range", _), [
     Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _);
     Typ_arg_aux(Typ_arg_nexp m, _);]) ->
     (squarebars (if Big_int.equal n Big_int.zero then nexp m else doc_op colon (doc_int n) (nexp m)))
   | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
-    (squarecolons (nexp n))
+     (squarecolons (nexp n))
   | Typ_app(id,args) ->
       (* trailing space to avoid >> token in case of nested app types *)
       (doc_id id) ^^ (angles (separate_map comma_sp doc_typ_arg args)) ^^ space
@@ -185,7 +148,7 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
   and atomic_typ ((Typ_aux (t, _)) as ty) = match t with
   | Typ_id id  -> doc_id id
   | Typ_var v  -> doc_var v
-  | Typ_app _ | Typ_tup _ | Typ_fn _ ->
+  | Typ_app _ | Typ_tup _ | Typ_fn _ | Typ_exist _ ->
       (* exhaustiveness matters here to avoid infinite loops
        * if we add a new Typ constructor *)
       group (parens (typ ty))
@@ -219,6 +182,7 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
   and atomic_nexp_typ ((Nexp_aux(n,_)) as ne) = match n with
     | Nexp_var v -> doc_var v
     | Nexp_id i  -> braces (doc_id i)
+    | Nexp_app (op, args) -> doc_id op ^^ parens (separate_map (comma ^^ space) nexp args)
     | Nexp_constant i -> if Big_int.less i Big_int.zero then parens(doc_int i) else doc_int i
     | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _->
       group (parens (nexp ne))
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 110c0b31..bcf997d4 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -150,6 +150,7 @@ and pp_format_nexp_lem (Nexp_aux(n,l)) =
   (match n with
    | Nexp_id(i) -> "(Nexp_id " ^ pp_format_id_lem i ^ ")"
    | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")"
+   | Nexp_app(op,args) -> "(Nexp_app [" ^ Util.string_of_list ", " pp_format_nexp_lem args ^ "])"
    | Nexp_constant(i) -> "(Nexp_constant " ^ (lemnum Big_int.to_string i) ^ ")"
    | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
    | Nexp_minus(n1,n2) -> "(Nexp_minus " ^ (pp_format_nexp_lem n1)^ " " ^ (pp_format_nexp_lem n2) ^ ")"
@@ -406,6 +407,9 @@ and pp_lem_exp ppf (E_aux(e,(l,annot)) as exp) =
     | E_case(exp,pexps) ->
       fprintf ppf "@[<0>(E_aux (E_case %a [%a]) (%a, %a))@]"
         pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps pp_lem_l l pp_annot annot
+    | E_try(exp,pexps) ->
+      fprintf ppf "@[<0>(E_aux (E_try %a [%a]) (%a, %a))@]"
+        pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps pp_lem_l l pp_annot annot
     | E_let(leb,exp) -> fprintf ppf "@[<0>(E_aux (E_let %a %a) (%a, %a))@]"
                           pp_lem_let leb pp_lem_exp exp pp_lem_l l pp_annot annot
     | E_assign(lexp,exp) -> fprintf ppf "@[<0>(E_aux (E_assign %a %a) (%a, %a))@]"
@@ -416,30 +420,12 @@ and pp_lem_exp ppf (E_aux(e,(l,annot)) as exp) =
       fprintf ppf "@[<0>(E_aux (E_constraint %a) (%a, %a))@]" pp_lem_nexp_constraint nc pp_lem_l l pp_annot annot
     | E_exit exp ->
       fprintf ppf "@[<0>(E_aux (E_exit %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot
+    | E_throw exp ->
+      fprintf ppf "@[<0>(E_aux (E_throw %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot
     | E_return exp ->
       fprintf ppf "@[<0>(E_aux (E_return %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot
     | E_assert(c,msg) ->
       fprintf ppf "@[<0>(E_aux (E_assert %a %a) (%a, %a))@]" pp_lem_exp c pp_lem_exp msg pp_lem_l l pp_annot annot
-      (*
-    | E_internal_exp ((l, Base((_,t),_,_,_,_,bindings))) ->
-      (*TODO use bindings where appropriate*)
-      (match t.t with
-        | Tapp("register",[TA_typ {t=Tapp("vector",[TA_nexp _;TA_nexp r;_;_])}])
-        | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) ->
-          (match r.nexp with
-          | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]"
-                                       kwd (lemnum string_of_int (Big_int.to_int bi)) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob))
-          | Nvar v -> fprintf ppf  "@[<0>(E_aux (E_id (Id_aux (Id \"%a\") %a)) (%a,%a))@]"
-                                     kwd v pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob))
-          | _ ->  raise (Reporting_basic.err_unreachable l "Internal exp given vector without known length"))
-        | Tapp("implicit",[TA_nexp r]) ->
-          (match r.nexp with
-            | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]"
-                                       kwd (lemnum string_of_int (Big_int.to_int bi)) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob))
-            | Nvar v -> fprintf ppf "@[<0>(E_aux (E_id (Id_aux (Id \"%a\") %a)) (%a,%a))@]"
-                                     kwd v pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob))
-            | _ -> raise (Reporting_basic.err_unreachable l "Internal_exp given implicit without variable or const"))
-        | _ ->  raise (Reporting_basic.err_unreachable l "Internal exp given non-vector or implicit")*)
     | E_comment _ | E_comment_struc _ ->
       fprintf ppf "@[(E_aux (E_lit (L_aux L_unit %a)) (%a,%a))@]" pp_lem_l l pp_lem_l l pp_annot annot
     | E_internal_cast _ | E_internal_exp _ ->
@@ -455,6 +441,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot)) as exp) =
     | E_internal_plet (pat,exp1,exp2) ->
       fprintf ppf "@[<0>(E_aux (E_internal_plet %a %a %a) (%a, %a))@]"
         pp_lem_pat pat pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_l l pp_annot annot
+    | E_internal_value _ -> raise (Reporting_basic.err_unreachable l "Found internal_value")
   in
   print_e ppf e
 
@@ -500,12 +487,8 @@ let pp_lem_default ppf (DT_aux(df,l)) =
 
 (* FIXME *)
 let pp_lem_spec ppf (VS_aux(v,(l,annot))) =
-  let print_spec ppf v =
-    match v with
-    | VS_val_spec(ts,id,ext_opt,is_cast) ->
-       (* FIXME: None *)
-      fprintf ppf "@[<0>(%a %a %a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id (pp_option_lem quot_string) None pp_bool_lem is_cast
-    | _ -> failwith "Invalid valspec"
+  let print_spec ppf (VS_val_spec(ts, id, ext_opt, is_cast)) =
+    fprintf ppf "@[<0>(%a %a %a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id (pp_option_lem quot_string) None pp_bool_lem is_cast
   in
   fprintf ppf "@[<0>(VS_aux %a (%a, %a))@]" print_spec v pp_lem_l l pp_annot annot
 
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 8302c32d..b7cd3761 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -347,27 +347,6 @@ let doc_exp, doc_let =
   | E_app_infix(l,op,r) ->
       failwith ("unexpected app_infix operator " ^ (pp_format_id op))
   (* doc_op (doc_id op) (exp l) (exp r) *)
-  | E_comment s -> comment (string s)
-  | E_comment_struc e -> comment (exp e)
-                                 (*
-  | E_internal_exp((l, Base((_,t),_,_,_,_,bindings))) -> (*TODO use bindings, and other params*)
-    (match t.t with
-      | Tapp("register",[TA_typ {t=Tapp("vector",[TA_nexp _;TA_nexp r;_;_])}])
-      | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) ->
-        (match r.nexp with
-          | Nvar v -> utf8string v
-          | Nconst bi -> utf8string (Big_int.Big_int.to_string bi)
-          | _ ->  raise (Reporting_basic.err_unreachable l
-                           ("Internal exp given vector without known length, instead given " ^ n_to_string r)))
-      | Tapp("implicit",[TA_nexp r]) ->
-        (match r.nexp with
-          | Nconst bi -> utf8string (Big_int.Big_int.to_string bi)
-          | Nvar v -> utf8string v
-          | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given implicit without var or const"))
-      | _ ->  raise (Reporting_basic.err_unreachable l ("Internal exp given non-vector, non-implicit " ^ t_to_string t)))
-  | E_internal_exp_user _ -> raise (Reporting_basic.err_unreachable Unknown ("internal_exp_user not rewritten away"))
-  | E_internal_cast ((_, Overload (_, _,_ )), _) | E_internal_exp _ -> assert false
-                                  *)
   | E_internal_return exp1 ->
       separate space [string "internal_return"; exp exp1]
   | _ -> failwith ("Cannot print: " ^ Ast_util.string_of_exp expr)
@@ -415,16 +394,14 @@ let doc_default (DT_aux(df,_)) = match df with
   | DT_typ(ts,id) -> separate space [string "default"; doc_typscm ts; doc_id id]
   | DT_order(ord) -> separate space [string "default"; string "Order"; doc_ord ord]
 
-let doc_spec (VS_aux(v,_)) = match v with
-  | VS_val_spec(ts,id,ext_opt,is_cast) ->
-     let cast_pp = if is_cast then [string "cast"] else [] in
-     (* This sail syntax only supports a single extern name, so just use the ocaml version *)
-     let extern_kwd_pp, id_pp = match ext_opt "ocaml" with
-       | Some ext -> [string "extern"], doc_op equals (doc_id id) (dquotes (string (ext)))
-       | None -> [], doc_id id
-     in
-     separate space ([string "val"] @ cast_pp @ extern_kwd_pp @ [doc_typscm ts] @ [id_pp])
-  | _ -> failwith "Invalid valspec"
+let doc_spec (VS_aux (VS_val_spec (ts, id, ext_opt, is_cast), _)) =
+  let cast_pp = if is_cast then [string "cast"] else [] in
+  (* This sail syntax only supports a single extern name, so just use the ocaml version *)
+  let extern_kwd_pp, id_pp = match ext_opt "ocaml" with
+    | Some ext -> [string "extern"], doc_op equals (doc_id id) (dquotes (string (ext)))
+    | None -> [], doc_id id
+  in
+  separate space ([string "val"] @ cast_pp @ extern_kwd_pp @ [doc_typscm ts] @ [id_pp])
 
 let doc_namescm (Name_sect_aux(ns,_)) = match ns with
   | Name_sect_none -> empty
@@ -555,6 +532,7 @@ let rec doc_def def = group (match def with
   | DEF_comm (DC_comm s) -> comment (string s)
   | DEF_comm (DC_comm_struct d) -> comment (doc_def d)
   | DEF_fixity _ -> empty
+  | DEF_internal_mutrec _ -> failwith "Cannot print internal mutrec"
   ) ^^ hardline
 
 let doc_defs (Defs(defs)) =
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 468b3a84..a639dd3f 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -130,11 +130,11 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
     | E_record_update(e,fexps) ->
       union_effects (effect_of e) (effect_of_fexps fexps)
     | E_field (e,_) -> effect_of e
-    | E_case (e,pexps) ->
+    | E_case (e,pexps) | E_try (e,pexps) ->
       List.fold_left union_effects (effect_of e) (List.map effect_of_pexp pexps)
     | E_let (lb,e) -> union_effects (effect_of_lb lb) (effect_of e)
     | E_assign (lexp,e) -> union_effects (effect_of_lexp lexp) (effect_of e)
-    | E_exit e -> union_effects eff (effect_of e)
+    | E_exit e | E_throw e -> union_effects eff (effect_of e)
     | E_return e -> union_effects eff (effect_of e)
     | E_sizeof _ | E_sizeof_internal _ | E_constraint _ -> no_effect
     | E_assert (c,m) -> union_effects eff (union_eff_exps [c; m])
@@ -147,6 +147,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
         (union_effects (effect_of e1) (effect_of e2))
     | E_internal_plet (_,e1,e2) -> union_effects (effect_of e1) (effect_of e2)
     | E_internal_return e1 -> effect_of e1
+    | E_internal_value v -> no_effect
   in
   E_aux (e, (l, Some (env, typ, effsum)))
 | None ->
@@ -205,24 +206,6 @@ let fix_eff_lb (LB_aux (lb,((l,_) as annot))) = match snd annot with
 | None ->
   LB_aux (lb, (l, None))
 
-let effectful_effs = function
-  | Effect_aux (Effect_set effs, _) ->
-    List.exists
-      (fun (BE_aux (be,_)) ->
-       match be with
-       | BE_nondet | BE_unspec | BE_undef | BE_lset -> false
-       | _ -> true
-      ) effs
-  | _ -> true
-
-let effectful eaux = effectful_effs (effect_of (propagate_exp_effect eaux))
-let effectful_pexp pexp = effectful_effs (snd (propagate_pexp_effect pexp))
-
-(* let id_to_string (Id_aux(id,l)) =
-  match id with
-    | Id(s) -> s
-    | DeIid(s) -> s *)
-
 let explode s =
   let rec exp i l = if i < 0 then l else exp (i - 1) (s.[i] :: l) in
   exp (String.length s - 1) []
@@ -526,6 +509,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
   ; e_internal_let           : 'lexp * 'exp * 'exp -> 'exp_aux
   ; e_internal_plet          : 'pat * 'exp * 'exp -> 'exp_aux
   ; e_internal_return        : 'exp -> 'exp_aux
+  ; e_internal_value         : Value.value -> 'exp_aux
   ; e_aux                    : 'exp_aux * 'a annot -> 'exp
   ; lEXP_id                  : id -> 'lexp_aux
   ; lEXP_memory              : id * 'exp list -> 'lexp_aux
@@ -600,6 +584,7 @@ let rec fold_exp_aux alg = function
   | E_internal_plet (pat,e1,e2) ->
      alg.e_internal_plet (fold_pat alg.pat_alg pat, fold_exp alg e1, fold_exp alg e2)
   | E_internal_return e -> alg.e_internal_return (fold_exp alg e)
+  | E_internal_value v -> alg.e_internal_value v
 and fold_exp alg (E_aux (exp_aux,annot)) = alg.e_aux (fold_exp_aux alg exp_aux, annot)
 and fold_lexp_aux alg = function
   | LEXP_id id -> alg.lEXP_id id
@@ -670,6 +655,7 @@ let id_exp_alg =
   ; e_internal_let = (fun (lexp, e2, e3) -> E_internal_let (lexp,e2,e3))
   ; e_internal_plet = (fun (pat, e1, e2) -> E_internal_plet (pat,e1,e2))
   ; e_internal_return = (fun e -> E_internal_return e)
+  ; e_internal_value = (fun v -> E_internal_value v)
   ; e_aux = (fun (e,annot) -> E_aux (e,annot))
   ; lEXP_id = (fun id -> LEXP_id id)
   ; lEXP_memory = (fun (id,es) -> LEXP_memory (id,es))
@@ -771,6 +757,7 @@ let compute_exp_alg bot join =
   ; e_internal_plet = (fun ((vp,pat), (v1,e1), (v2,e2)) ->
     (join_list [vp;v1;v2], E_internal_plet (pat,e1,e2)))
   ; e_internal_return = (fun (v,e) -> (v, E_internal_return e))
+  ; e_internal_value = (fun v -> (bot, E_internal_value v))
   ; e_aux = (fun ((v,e),annot) -> (v, E_aux (e,annot)))
   ; lEXP_id = (fun id -> (bot, LEXP_id id))
   ; lEXP_memory = (fun (id,es) -> split_join (fun es -> LEXP_memory (id,es)) es)
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 09dddb95..faa6a81a 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -145,6 +145,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
  ; e_internal_let           : 'lexp * 'exp * 'exp -> 'exp_aux
  ; e_internal_plet          : 'pat * 'exp * 'exp -> 'exp_aux
  ; e_internal_return        : 'exp -> 'exp_aux
+ ; e_internal_value         : Value.value -> 'exp_aux
  ; e_aux                    : 'exp_aux * 'a annot -> 'exp
  ; lEXP_id                  : id -> 'lexp_aux
  ; lEXP_memory              : id * 'exp list -> 'lexp_aux
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 2b5df2a2..8c0526fe 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -102,7 +102,6 @@ let effectful_effs = function
        | BE_nondet | BE_unspec | BE_undef | BE_lset -> false
        | _ -> true
       ) effs
-  | _ -> true
 
 let effectful eaux = effectful_effs (effect_of (propagate_exp_effect eaux))
 let effectful_pexp pexp = effectful_effs (snd (propagate_pexp_effect pexp))
@@ -366,6 +365,7 @@ let rewrite_sizeof (Defs defs) =
     ; e_internal_let = (fun ((lexp,lexp'), (e2,e2'), (e3,e3')) -> (E_internal_let (lexp,e2,e3), E_internal_let (lexp',e2',e3')))
     ; e_internal_plet = (fun (pat, (e1,e1'), (e2,e2')) -> (E_internal_plet (pat,e1,e2), E_internal_plet (pat,e1',e2')))
     ; e_internal_return = (fun (e,e') -> (E_internal_return e, E_internal_return e'))
+    ; e_internal_value = (fun v -> (E_internal_value v, E_internal_value v))
     ; e_aux = (fun ((e,e'),annot) -> (E_aux (e,annot), E_aux (e',annot)))
     ; lEXP_id = (fun id -> (LEXP_id id, LEXP_id id))
     ; lEXP_memory = (fun (id,es) -> let (es, es') = List.split es in (LEXP_memory (id,es), LEXP_memory (id,es')))
@@ -942,6 +942,7 @@ let rec pat_to_exp (P_aux (pat,(l,annot))) =
   | P_wild -> raise (Reporting_basic.err_unreachable l
       "pat_to_exp given wildcard pattern")
   | P_as (pat,id) -> rewrap (E_id id)
+  | P_var (pat, _) -> pat_to_exp pat
   | P_typ (_,pat) -> pat_to_exp pat
   | P_id id -> rewrap (E_id id)
   | P_app (id,pats) -> rewrap (E_app (id, List.map pat_to_exp pats))
@@ -1030,7 +1031,7 @@ let bitwise_and_exp exp1 exp2 =
 
 let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with
 | P_lit _ | P_wild | P_id _ -> false
-| P_as (pat,_) | P_typ (_,pat) -> contains_bitvector_pat pat
+| P_as (pat,_) | P_typ (_,pat) | P_var (pat,_) -> contains_bitvector_pat pat
 | P_vector _ | P_vector_concat _ ->
     let typ = Env.base_typ_of (env_of_annot annot) (typ_of_annot annot) in
     is_bitvector_typ typ
@@ -1333,7 +1334,7 @@ let rewrite_fun_guarded_pats rewriters (FD_aux (FD_function (r,t,e,funcls),(l,fd
          (pat,guard,exp,annot) in
        let cs = rewrite_guarded_clauses l (List.map clause funcls) in
        List.map (fun (pat,exp,annot) ->
-         FCL_aux (FCL_Funcl(id,construct_pexp (pat,None,exp,(Unknown,None))),annot)) cs
+         FCL_aux (FCL_Funcl(id,construct_pexp (pat,None,exp,(Parse_ast.Unknown,None))),annot)) cs
      | _ -> funcls (* TODO is the empty list possible here? *) in
    FD_aux (FD_function(r,t,e,funcls),(l,fdannot))
 
@@ -1765,6 +1766,7 @@ let rewrite_fix_val_specs (Defs defs) =
          let args_t' = rewrite_typ_nexp_ids (env_of exp) (pat_typ_of pat) in
          let ret_t' = rewrite_typ_nexp_ids (env_of exp) (typ_of exp) in
          (tq, Typ_aux (Typ_fn (args_t', ret_t', eff'), a)), eff'
+      | _ -> assert false (* find_vs must return a function type *)
     in
     let annot = add_effect_annot annot eff in
     (Bindings.add id vs val_specs,
@@ -2288,7 +2290,7 @@ let rewrite_defs_letbind_effects  =
        let exp3 = n_exp_term newreturn exp3 in
        k (rewrap (E_if (exp1,exp2,exp3))))
     | E_for (id,start,stop,by,dir,body) ->
-       n_exp_name start (fun start -> 
+       n_exp_name start (fun start ->
        n_exp_name stop (fun stop ->
        n_exp_name by (fun by ->
        let body = n_exp_term (effectful body) body in
@@ -2305,19 +2307,19 @@ let rewrite_defs_letbind_effects  =
        n_exp_name exp2 (fun exp2 ->
        k (rewrap (E_vector_access (exp1,exp2)))))
     | E_vector_subrange (exp1,exp2,exp3) ->
-       n_exp_name exp1 (fun exp1 -> 
-       n_exp_name exp2 (fun exp2 -> 
+       n_exp_name exp1 (fun exp1 ->
+       n_exp_name exp2 (fun exp2 ->
        n_exp_name exp3 (fun exp3 ->
        k (rewrap (E_vector_subrange (exp1,exp2,exp3))))))
     | E_vector_update (exp1,exp2,exp3) ->
-       n_exp_name exp1 (fun exp1 -> 
-       n_exp_name exp2 (fun exp2 -> 
+       n_exp_name exp1 (fun exp1 ->
+       n_exp_name exp2 (fun exp2 ->
        n_exp_name exp3 (fun exp3 ->
        k (rewrap (E_vector_update (exp1,exp2,exp3))))))
     | E_vector_update_subrange (exp1,exp2,exp3,exp4) ->
-       n_exp_name exp1 (fun exp1 -> 
-       n_exp_name exp2 (fun exp2 -> 
-       n_exp_name exp3 (fun exp3 -> 
+       n_exp_name exp1 (fun exp1 ->
+       n_exp_name exp2 (fun exp2 ->
+       n_exp_name exp3 (fun exp3 ->
        n_exp_name exp4 (fun exp4 ->
        k (rewrap (E_vector_update_subrange (exp1,exp2,exp3,exp4)))))))
     | E_vector_append (exp1,exp2) ->
@@ -2327,14 +2329,14 @@ let rewrite_defs_letbind_effects  =
     | E_list exps ->
        n_exp_nameL exps (fun exps ->
        k (rewrap (E_list exps)))
-    | E_cons (exp1,exp2) -> 
+    | E_cons (exp1,exp2) ->
        n_exp_name exp1 (fun exp1 ->
        n_exp_name exp2 (fun exp2 ->
        k (rewrap (E_cons (exp1,exp2)))))
     | E_record fexps ->
        n_fexps fexps (fun fexps ->
        k (rewrap (E_record fexps)))
-    | E_record_update (exp1,fexps) -> 
+    | E_record_update (exp1,fexps) ->
        n_exp_name exp1 (fun exp1 ->
        n_fexps fexps (fun fexps ->
        k (rewrap (E_record_update (exp1,fexps)))))
@@ -2343,11 +2345,16 @@ let rewrite_defs_letbind_effects  =
        k (rewrap (E_field (exp1,id))))
     | E_case (exp1,pexps) ->
        let newreturn = List.exists effectful_pexp pexps in
-       n_exp_name exp1 (fun exp1 -> 
+       n_exp_name exp1 (fun exp1 ->
        n_pexpL newreturn pexps (fun pexps ->
        k (rewrap (E_case (exp1,pexps)))))
+    | E_try (exp1,pexps) ->
+       let newreturn = List.exists effectful_pexp pexps in
+       n_exp_name exp1 (fun exp1 ->
+       n_pexpL newreturn pexps (fun pexps ->
+       k (rewrap (E_try (exp1,pexps)))))
     | E_let (lb,body) ->
-       n_lb lb (fun lb -> 
+       n_lb lb (fun lb ->
        rewrap (E_let (lb,n_exp body k)))
     | E_sizeof nexp ->
        k (rewrap (E_sizeof nexp))
@@ -2360,6 +2367,7 @@ let rewrite_defs_letbind_effects  =
        n_exp_name exp1 (fun exp1 ->
        k (rewrap (E_assign (lexp,exp1)))))
     | E_exit exp' -> k (E_aux (E_exit (n_exp_term (effectful exp') exp'),annot))
+    | E_throw exp' -> k (E_aux (E_throw (n_exp_term (effectful exp') exp'),annot))
     | E_assert (exp1,exp2) ->
        n_exp_name exp1 (fun exp1 ->
        n_exp_name exp2 (fun exp2 ->
@@ -2376,11 +2384,13 @@ let rewrite_defs_letbind_effects  =
     | E_internal_return exp1 ->
        n_exp_name exp1 (fun exp1 ->
        k (rewrap (E_internal_return exp1)))
+    | E_internal_value v ->
+       k (rewrap (E_internal_value v))
     | E_comment str ->
-      k (rewrap (E_comment str))
+       k (rewrap (E_comment str))
     | E_comment_struc exp' ->
        n_exp exp' (fun exp' ->
-               k (rewrap (E_comment_struc exp')))
+       k (rewrap (E_comment_struc exp')))
     | E_return exp' ->
        n_exp_name exp' (fun exp' ->
        k (rewrap (E_return exp')))
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 7386e9fa..81296027 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -577,6 +577,10 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function
   | DEF_fixity _ -> mt,mt
   | DEF_overload (id,ids) -> init_env (string_of_id id), List.fold_left (fun ns id -> Nameset.add (string_of_id id) ns) mt ids
   | DEF_default def -> mt,mt
+  | DEF_internal_mutrec fdefs ->
+     let fvs = List.map (fv_of_fun consider_var) fdefs in
+     List.fold_left Nameset.union Nameset.empty (List.map fst fvs),
+     List.fold_left Nameset.union Nameset.empty (List.map snd fvs)
   | DEF_scattered sdef -> fv_of_scattered consider_var consider_scatter_as_one all_defs sdef
   | DEF_reg_dec rdec -> fv_of_rd consider_var rdec
   | DEF_comm _ -> mt,mt