Fix up some edge cases with the bitvector/polyvector split

Mostly in the Coq backend, plus a few testcases that use bitvector
builtins on poly-vectors (which works on some backends, but not Coq).
Also handle some additional list inclusion proofs in Coq.

1 files changed, 25 insertions, 30 deletions

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 58c71e82..5e8c7145 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1233,9 +1233,10 @@ let condition_produces_constraint ctxt exp =
    dependent pair with a proof that the result is the expected integer.  This
    is redundant for basic arithmetic functions and functions which we unfold
    in the constraint solver. *)
-let no_proof_fns = ["Z.add"; "Z.sub"; "Z.opp"; "Z.mul"; "Z.rem"; "length_mword"; "length";
-                      "negb"; "andb"; "orb";
-                      "Z.leb"; "Z.geb"; "Z.ltb"; "Z.gtb"; "Z.eqb"]
+let no_proof_fns = ["Z.add"; "Z.sub"; "Z.opp"; "Z.mul"; "Z.rem";
+                    "length_mword"; "length"; "vec_length";
+                    "negb"; "andb"; "orb";
+                    "Z.leb"; "Z.geb"; "Z.ltb"; "Z.gtb"; "Z.eqb"]
 
 let is_no_proof_fn env id =
   if Env.is_extern id env "coq"
@@ -1388,12 +1389,11 @@ let doc_exp, doc_let =
            let in_typ = match destruct_exist_plain in_typ with Some (_,_,t) -> t | None -> in_typ in
            let autocast =
              (* Avoid using helper functions which simplify the nexps *)
-             is_bitvector_typ in_typ && is_bitvector_typ out_typ &&
-               match in_typ, out_typ with
-               | Typ_aux (Typ_app (_,[A_aux (A_nexp n1,_);_;_]),_),
-                 Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) ->
-                  not (similar_nexps ctxt (env_of exp) n1 n2)
-               | _ -> false
+             match in_typ, out_typ with
+             | Typ_aux (Typ_app (Id_aux (Id "bitvector",_),[A_aux (A_nexp n1,_);_]),_),
+               Typ_aux (Typ_app (Id_aux (Id "bitvector",_),[A_aux (A_nexp n2,_);_]),_) ->
+                not (similar_nexps ctxt (env_of exp) n1 n2)
+             | _ -> false
            in
            let exp_pp = expV (want_parens || autocast || Util.is_some build_ex) exp in
            let exp_pp =
@@ -1733,10 +1733,9 @@ let doc_exp, doc_let =
             let typ_from_fn' = match typ_from_fn with Typ_aux (Typ_exist (_,_,t),_) -> t  | t -> t in
             let autocast =
               (* Avoid using helper functions which simplify the nexps *)
-              is_bitvector_typ typ_of_arg' && is_bitvector_typ typ_from_fn' &&
               match typ_of_arg', typ_from_fn' with
-              | Typ_aux (Typ_app (_,[A_aux (A_nexp n1,_);_;_]),_),
-                Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) ->
+              | Typ_aux (Typ_app (Id_aux (Id "bitvector",_),[A_aux (A_nexp n1,_);_]),_),
+                Typ_aux (Typ_app (Id_aux (Id "bitvector",_),[A_aux (A_nexp n2,_);_]),_) ->
                  not (similar_nexps ctxt env n1 n2)
               | _ -> false
             in
@@ -1807,10 +1806,9 @@ let doc_exp, doc_let =
             in
             let autocast =
               (* Avoid using helper functions which simplify the nexps *)
-              is_bitvector_typ in_typ && is_bitvector_typ out_typ &&
               match in_typ, out_typ with
-              | Typ_aux (Typ_app (_,[A_aux (A_nexp n1,_);_;_]),_),
-                Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) ->
+              | Typ_aux (Typ_app (Id_aux (Id "bitvector",_),[A_aux (A_nexp n1,_);_]),_),
+                Typ_aux (Typ_app (Id_aux (Id "bitvector",_),[A_aux (A_nexp n2,_);_]),_) ->
                  not (similar_nexps ctxt env n1 n2)
               | _ -> false
             in pack,unpack,autocast
@@ -1877,12 +1875,11 @@ let doc_exp, doc_let =
             let ann_typ = expand_range_type (Env.expand_synonyms env ann_typ) in
             let autocast =
               (* Avoid using helper functions which simplify the nexps *)
-              is_bitvector_typ exp_typ && is_bitvector_typ ann_typ &&
-                match exp_typ, ann_typ with
-                | Typ_aux (Typ_app (_,[A_aux (A_nexp n1,_);_;_]),_),
-                  Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) ->
-                   not (similar_nexps ctxt env n1 n2)
-                | _ -> false
+              match exp_typ, ann_typ with
+              | Typ_aux (Typ_app (Id_aux (Id "bitvector",_),[A_aux (A_nexp n1,_);_]),_),
+                Typ_aux (Typ_app (Id_aux (Id "bitvector",_),[A_aux (A_nexp n2,_);_]),_) ->
+                 not (similar_nexps ctxt env n1 n2)
+              | _ -> false
             in
             let () =
               debug ctxt (lazy ("Variable " ^ string_of_id id ^ " with type " ^ string_of_typ typ));
@@ -1914,19 +1911,17 @@ let doc_exp, doc_let =
        let inner_ex,_,inner_typ' = classify_ex_type ctxt env inner_typ in
        let autocast_out =
          (* Avoid using helper functions which simplify the nexps *)
-         is_bitvector_typ outer_typ' && is_bitvector_typ cast_typ' &&
-           match outer_typ', cast_typ' with
-           | Typ_aux (Typ_app (_,[A_aux (A_nexp n1,_);_;_]),_),
-         Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) ->
+         match outer_typ', cast_typ' with
+         | Typ_aux (Typ_app (Id_aux (Id "bitvector",_),[A_aux (A_nexp n1,_);_]),_),
+           Typ_aux (Typ_app (Id_aux (Id "bitvector",_),[A_aux (A_nexp n2,_);_]),_) ->
               not (similar_nexps ctxt env n1 n2)
            | _ -> false
        in
        let autocast_in =
          (* Avoid using helper functions which simplify the nexps *)
-         is_bitvector_typ inner_typ' && is_bitvector_typ cast_typ' &&
-           match inner_typ', cast_typ' with
-           | Typ_aux (Typ_app (_,[A_aux (A_nexp n1,_);_;_]),_),
-         Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) ->
+         match inner_typ', cast_typ' with
+         | Typ_aux (Typ_app (Id_aux (Id "bitvector",_),[A_aux (A_nexp n1,_);_]),_),
+           Typ_aux (Typ_app (Id_aux (Id "bitvector",_),[A_aux (A_nexp n2,_);_]),_) ->
               not (similar_nexps ctxt env n1 n2)
            | _ -> false
        in
@@ -2053,7 +2048,7 @@ let doc_exp, doc_let =
             align (group expspp) in
        let epp = brackets expspp in
        let (epp,aexp_needed) =
-         if is_bit_typ etyp then
+         if is_bitvector_typ t then
            let bepp = string "vec_of_bits" ^^ space ^^ align epp in
            (align (group (prefix 0 1 bepp (doc_tannot ctxt (env_of full_exp) false t))), true)
          else