Various monomorphisation fixes

- Handle more combinations of patterns and expressions in constant
  propagation
- Remove dead code after throw() in monomorphisation
- Use correct val specs and environments when analysing and
  pretty-printing function clauses

3 files changed, 53 insertions, 4 deletions

diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml
index 00b3d192..e785aa93 100644
--- a/src/constant_propagation.ml
+++ b/src/constant_propagation.ml
@@ -663,6 +663,10 @@ let const_props target defs ref_vars =
     | "or_bool", ([E_aux (E_lit (L_aux (L_true, _)), _) as e_true; _] |
                   [_; E_aux (E_lit (L_aux (L_true, _)), _) as e_true]) ->
        e_true
+    | _, [E_aux (E_vector [], _); e']
+    | _, [e'; E_aux (E_vector [], _)]
+      when is_overload_of (mk_id "append") ->
+       e'
     | _, _ when List.for_all Constant_fold.is_constant args ->
        const_fold exp
     | _, [arg] when is_overload_of (mk_id "__size") ->
@@ -733,6 +737,10 @@ let const_props target defs ref_vars =
               (Reporting.print_err lit_l "Monomorphisation"
                  "Unexpected kind of literal for var match"; GiveUp)
          end
+      | E_lit ((L_aux ((L_bin _ | L_hex _), _) as lit)), P_vector _ ->
+         let mk_bitlit lit = E_aux (E_lit lit, (Generated l, mk_tannot env bit_typ no_effect)) in
+         let lits' = List.map mk_bitlit (vector_string_to_bit_list lit) in
+         check_exp_pat (E_aux (E_vector lits', (l, annot))) pat
       | E_lit _, _ ->
          (Reporting.print_err l' "Monomorphisation"
             "Unexpected kind of pattern for literal"; GiveUp)
@@ -744,6 +752,7 @@ let const_props target defs ref_vars =
               if lit_match (lit,lit') then DoesMatch ([],[]) else DoesNotMatch
            | E_aux (E_lit l,_), P_aux (P_id var,_) when pat_id_is_variable env var ->
               DoesMatch ([var, e],[])
+           | _, P_aux (P_wild, _) -> DoesMatch ([],[])
            | _ -> GiveUp) es ps in
          let final = List.fold_left (fun acc m -> match acc, m with
            | _, GiveUp -> GiveUp
@@ -755,6 +764,10 @@ let const_props target defs ref_vars =
             (Reporting.print_err l "Monomorphisation"
                "Unexpected kind of pattern for vector literal"; GiveUp)
          | _ -> final)
+      | E_vector _, P_lit ((L_aux ((L_bin _ | L_hex _), _) as lit)) ->
+         let mk_bitlit lit = P_aux (P_lit lit, (Generated l, mk_tannot env bit_typ no_effect)) in
+         let lits' = List.map mk_bitlit (vector_string_to_bit_list lit) in
+         check_exp_pat exp (P_aux (P_vector lits', (l, annot)))
       | E_vector _, _ ->
          (Reporting.print_err l "Monomorphisation"
             "Unexpected kind of pattern for vector literal"; GiveUp)
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 4b7ed20c..e49ef4f5 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -577,6 +577,8 @@ let stop_at_false_assertions e =
        end
     | E_assert (e1,_) when exp_false e1 ->
        ea, Some (typ_of_annot ann)
+    | E_throw e ->
+       ea, Some (typ_of_annot ann)
     | _ -> ea, None
   in fst (exp e)
 
@@ -1969,6 +1971,37 @@ let refine_dependency env (E_aux (e,(l,annot)) as exp) pexps =
      (match mk_subrange_pattern vannot vstart vend with
      | Some mk_pat -> check_dep id mk_pat
      | None -> None)
+  (* TODO: Aborted attempt at considering bitvector concatenations when
+     refining dependencies.  Needs corresponding support in constant
+     propagation to work. *)
+  (* | E_app (append, [vec1; vec2])
+    when is_id (env_of exp) (Id "append") append ->
+     (* If the expression is a concatenation resulting in a small enough bitvector,
+        perform a (total) case split on the sub-vectors *)
+     let vec_len v = try Util.option_map Big_int.to_int (get_constant_vec_len (env_of exp) v) with _ -> None in
+     let pow2 n = Big_int.pow_int (Big_int.of_int 2) n in
+     let size_set len1 len2 = Big_int.mul (pow2 len1) (pow2 len2) in
+     begin match (vec_len (typ_of exp), vec_len (typ_of vec1), vec_len (typ_of vec2)) with
+       | (Some len, Some len1, Some len2)
+         when Big_int.less_equal (size_set len1 len2) (Big_int.of_int size_set_limit) ->
+          let recur = refine_dependency env in
+          (* Create pexps with dummy bodies (ignored by the recursive call) *)
+          let mk_pexps len =
+            let mk_pexp lit =
+              let (_, ord, _) = vector_typ_args_of (typ_of exp) in
+              let tannot = mk_tannot (env_of exp) (bitvector_typ (nint len) ord) no_effect in
+              let pat = P_aux (P_lit lit, (Generated l, tannot)) in
+              let exp = E_aux (E_lit (mk_lit L_unit), (Generated l, empty_tannot)) in
+              Pat_aux (Pat_exp (pat, exp), (Generated l, empty_tannot))
+            in
+            List.map mk_pexp (make_vectors len)
+          in
+          begin match (recur vec1 (mk_pexps len1), recur vec2 (mk_pexps len2)) with
+            | (Some deps1, Some deps2) -> Some (dmerge deps1 deps2)
+            | _ -> None
+          end
+       | _ -> None
+     end *)
   | _ -> None
 
 let simplify_size_nexp env typ_env (Nexp_aux (ne,l) as nexp) =
@@ -2586,7 +2619,7 @@ let print_result r =
 let analyse_funcl debug tenv constants (FCL_aux (FCL_Funcl (id,pexp),(l,_))) =
   let _ = if debug > 2 then print_endline (string_of_id id) else () in
   let pat,guard,body,_ = destruct_pexp pexp in
-  let (tq,_) = Env.get_val_spec id tenv in
+  let (tq,_) = Env.get_val_spec_orig id tenv in
   let set_assertions = find_set_assertions body in
   let _ = if debug > 2 then print_set_assertions set_assertions in
   let aenv = initial_env id l tq pat body set_assertions constants in
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 581872ee..3b53d466 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1367,8 +1367,11 @@ let doc_fun_body_lem ctxt exp =
   then align (string "catch_early_return" ^//^ parens (doc_exp))
   else doc_exp
 
-let doc_funcl_lem type_env (FCL_aux(FCL_Funcl(id, pexp), annot)) =
-  let typ = typ_of_annot annot in
+let doc_funcl_lem type_env (FCL_aux(FCL_Funcl(id, pexp), ((l, _) as annot))) =
+  let (tq, typ) =
+    try Env.get_val_spec_orig id type_env with
+    | _ -> raise (unreachable l __POS__ ("Could not get val-spec of " ^ string_of_id id))
+  in
   let arg_typs = match typ with
     | Typ_aux (Typ_fn (arg_typs, typ_ret, _), _) -> arg_typs
     | Typ_aux (_, l) -> raise (unreachable l __POS__ "Non-function type for funcl")
@@ -1411,7 +1414,7 @@ let rec doc_fundef_lem type_env (FD_aux(FD_function(r, typa, efa, fcls),fannot)
   match fcls with
   | [] -> failwith "FD_function with empty function list"
   | FCL_aux (FCL_Funcl(id, pexp),annot) :: _
-     when not (Env.is_extern id (env_of_annot annot) "lem") ->
+     when not (Env.is_extern id type_env "lem") ->
     (* Output "rec" modifier if function calls itself.  Mutually recursive
        functions are handled separately by doc_mutrec_lem. *)
     let is_funcl_rec =