Coq: solve some constraint/type errors with AArch64

- hints for dotp
- handle exists separately when trying eauto to keep search depth low
- more uniform existential handling (i.e., we now handle all existentials
  in the way we used to only handle existentials around atoms)

3 files changed, 60 insertions, 13 deletions

diff --git a/aarch64/aarch64_extras.v b/aarch64/aarch64_extras.v
index 45c5e3ce..00ca8601 100644
--- a/aarch64/aarch64_extras.v
+++ b/aarch64/aarch64_extras.v
@@ -142,3 +142,32 @@ rewrite Z.quot_mul; auto with zarith.
 Qed.
 Hint Resolve mul_quot_8_helper : sail.
 
+(* For aarch64_vector_arithmetic_binary_uniform_mul_int_dotp *)
+Lemma quot4_ge {esize x} : 4 <= esize -> x = Z.quot esize 4 -> x >= 0.
+intros.
+apply Z.le_ge.
+subst.
+apply Z.quot_pos; omega.
+Qed.
+(* except that only proving the hard bit leads to an anomaly...
+Hint Resolve quot4_ge : sail.*)
+Lemma dotp_lemma {datasize esize x} :
+ 8 = datasize \/ 16 = datasize \/ 32 = datasize \/ 64 = datasize \/ 128 = datasize \/ False ->
+ 4 <= esize -> x = Z.quot esize 4 -> datasize >= 0 /\ x >= 0.
+intros.
+split.
+* omega.
+* eauto using quot4_ge.
+Qed.
+Hint Resolve dotp_lemma : sail.
+
+
+Lemma quot4_gt {esize x} : 4 <= esize -> x = Z.quot esize 4 -> x > 0.
+intros.
+apply Z.lt_gt.
+subst.
+apply Z.quot_str_pos.
+omega.
+Qed.
+Hint Resolve quot4_gt : sail.
+
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index c1ca8c6c..a91b2299 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1079,6 +1079,28 @@ Lemma True_right {P:Prop} : (P /\ True) <-> P.
 tauto.
 Qed.
 
+(* Turn exists into metavariables like eexists, except put in dummy values when
+   the variable is unused.  This is used so that we can use eauto with a low
+   search bound that doesn't include the exists.  (Not terribly happy with
+   how this works...) *)
+Ltac drop_exists :=
+repeat
+  match goal with |- @ex Z ?p =>
+   let a := eval hnf in (p 0) in
+   let b := eval hnf in (p 1) in
+   match a with b => exists 0 | _ => eexists end
+  end.
+(*
+  match goal with |- @ex Z (fun x => @?p x) =>
+   let xx := fresh "x" in
+   evar (xx : Z);
+   let a := eval hnf in (p xx) in
+   match a with context [xx] => eexists | _ => exists 0 end;
+   instantiate (xx := 0);
+   clear xx
+  end.
+*)
+
 Ltac prepare_for_solver :=
 (*dump_context;*)
  clear_irrelevant_defns;
@@ -1130,7 +1152,7 @@ prepare_for_solver;
  | apply ArithFact_mword; assumption
  | constructor; omega with Z
    (* The datatypes hints give us some list handling, esp In *)
- | constructor; eauto 3 with datatypes zarith sail
+ | constructor; drop_exists; eauto 3 with datatypes zarith sail
  | constructor; idtac "Unable to solve constraint"; dump_context; fail
  ].
 (* Add an indirection so that you can redefine run_solver to fail to get
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index a61562e1..1614d8de 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -666,7 +666,7 @@ let is_ctor env id = match Env.lookup_id id env with
 let is_auto_decomposed_exist env typ =
   let typ = expand_range_type typ in
   match destruct_exist env typ with
-  | Some (kids, nc, (Typ_aux (Typ_app (id, _),_) as typ')) when string_of_id id = "atom" -> Some typ'
+  | Some (_, _, typ') -> Some typ'
   | _ -> None
 
 (*Note: vector concatenation, literal vectors, indexed vectors, and record should
@@ -1270,13 +1270,8 @@ let doc_exp, doc_let =
          | Local (_,typ) ->
             let exp_typ = expand_range_type (Env.expand_synonyms env typ) in
             let () =
-              debug ctxt (lazy ("Variable " ^ string_of_id id ^ " with type " ^ string_of_typ typ));
-              debug ctxt (lazy ("  expands to " ^ string_of_typ exp_typ))
-            in
-            let proj = match exp_typ with
-              | Typ_aux (Typ_exist _,_) -> true
-              | _ -> false
-            in if proj then string "projT1" ^^ doc_id id else doc_id id
+              debug ctxt (lazy ("Variable " ^ string_of_id id ^ " with type " ^ string_of_typ typ))
+            in doc_id id
          | _ -> doc_id id
        end
     | E_lit lit -> doc_lit lit
@@ -1456,6 +1451,10 @@ let doc_exp, doc_let =
        raise (report l __POS__ "E_vars should have been removed before pretty-printing")
     | E_internal_plet (pat,e1,e2) ->
        begin
+         let () =
+           debug ctxt (lazy ("Internal plet, pattern " ^ string_of_pat pat));
+           debug ctxt (lazy (" type of e1 " ^ string_of_typ (typ_of e1)))
+         in
          match pat, e1, e2 with
          | (P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _)),
            (E_aux (E_assert (assert_e1,assert_e2),_)), _ ->
@@ -1505,10 +1504,7 @@ let doc_exp, doc_let =
                     when not (is_enum (env_of e1) id) ->
                       let full_typ = (expand_range_type typ) in
                       let binder = match destruct_exist (env_of e1) full_typ with
-                        | Some ([kid], nc,
-                                Typ_aux (Typ_app (Id_aux (Id "atom",_),
-                                                  [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_))
-                            when Kid.compare kid kid' == 0 ->
+                        | Some _ ->
                            squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ])
                         | _ ->
                            parens (separate space [doc_id id; colon; doc_typ ctxt typ])