Add rewriting step for numeral patterns

Pattern matching against literal numbers is not well supported by Lem or
Isabelle.  This rewriting step turns them into guarded patterns (which can be
picked up by the guarded pattern rewriting to if-expressions).

1 files changed, 40 insertions, 7 deletions

diff --git a/src/rewrites.ml b/src/rewrites.ml
index 424931c3..a42335b9 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1028,6 +1028,12 @@ let bitwise_and_exp exp1 exp2 =
   let andid = Id_aux (Id "and_bool", gen_loc l) in
   annot_exp (E_app(andid,[exp1;exp2])) l (env_of exp1) bool_typ
 
+let compose_guard_opt g1 g2 = match g1, g2 with
+  | Some g1, Some g2 -> Some (bitwise_and_exp g1 g2)
+  | Some g1, None -> Some g1
+  | None, Some g2 -> Some g2
+  | None, None -> None
+
 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
@@ -1122,13 +1128,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) =
       annot_exp (E_let (letbind,body)) l env (typ_of body)) in
     (letexp, letbind) in
 
-  let compose_guards guards =
-    let conj g1 g2 = match g1, g2 with
-      | Some g1, Some g2 -> Some (bitwise_and_exp g1 g2)
-      | Some g1, None -> Some g1
-      | None, Some g2 -> Some g2
-      | None, None -> None in
-    List.fold_right conj guards None in
+  let compose_guards guards = List.fold_right compose_guard_opt guards None in
 
   let flatten_guards_decls gd =
     let (guards,decls,letbinds) = Util.split3 gd in
@@ -1294,6 +1294,38 @@ let rewrite_defs_remove_bitvector_pats (Defs defs) =
     Defs (List.flatten (List.map rewrite_def defs))
     (* )) *)
 
+(* Rewrite literal number patterns to guarded patterns
+   Those numeral patterns are not handled very well by Lem (or Isabelle)
+ *)
+let rewrite_defs_remove_numeral_pats =
+  let p_lit = function
+    | L_aux (L_num n, l) ->
+       let id = fresh_id "l__" Parse_ast.Unknown in
+       let annot_exp e_aux typ = E_aux (e_aux, simple_annot l typ) in
+       let guard =
+         annot_exp (E_app_infix (
+           annot_exp (E_id id) (atom_typ (nconstant n)),
+           mk_id "==",
+           simple_num l n
+         )) bool_typ in
+       (Some guard, P_id id)
+    | lit -> (None, P_lit lit) in
+  let guard_pat =
+    fold_pat { (compute_pat_alg None compose_guard_opt) with p_lit = p_lit } in
+  let pat_aux (pexp_aux, a) =
+    let pat,guard,exp,a = destruct_pexp (Pat_aux (pexp_aux, a)) in
+    let guard',pat = guard_pat pat in
+    match compose_guard_opt guard guard' with
+    | Some g -> Pat_aux (Pat_when (pat, g, exp), a)
+    | None -> Pat_aux (Pat_exp (pat, exp), a) in
+  let exp_alg = { id_exp_alg with pat_aux = pat_aux } in
+  let rewrite_exp _ = fold_exp exp_alg in
+  let rewrite_funcl (FCL_aux (FCL_Funcl (id, pexp), annot)) =
+    FCL_aux (FCL_Funcl (id, fold_pexp exp_alg pexp), annot) in
+  let rewrite_fun _ (FD_aux (FD_function (r_o, t_o, e_o, funcls), a)) =
+    FD_aux (FD_function (r_o, t_o, e_o, List.map rewrite_funcl funcls), a) in
+  rewrite_defs_base
+    { rewriters_base with rewrite_exp = rewrite_exp; rewrite_fun = rewrite_fun }
 
 (* Remove pattern guards by rewriting them to if-expressions within the
    pattern expression. *)
@@ -2921,6 +2953,7 @@ let rewrite_defs_lem = [
   (* ("simple_assignments", rewrite_simple_assignments); *)
   ("remove_vector_concat", rewrite_defs_remove_vector_concat);
   ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats);
+  ("remove_numeral_pats", rewrite_defs_remove_numeral_pats);
   ("guarded_pats", rewrite_defs_guarded_pats);
   ("exp_lift_assign", rewrite_defs_exp_lift_assign);
   ("register_ref_writes", rewrite_register_ref_writes);