From 1fb4d1ef961f056e3575c5e034cace85f2340509 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 15 Apr 2017 22:51:20 +0200
Subject: Fix bug #5377: @? patterns broken.

---
 pretyping/constr_matching.ml  | 78 ++++++++++++++++++++++++++++++++-----------
 test-suite/bugs/closed/5377.v | 54 ++++++++++++++++++++++++++++++
 2 files changed, 113 insertions(+), 19 deletions(-)
 create mode 100644 test-suite/bugs/closed/5377.v

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 886a982634..3c47cfdc4b 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -80,31 +80,71 @@ let add_binders na1 na2 binding_vars (names, terms as subst) =
 
 let rec build_lambda vars ctx m = match vars with
 | [] ->
-  let len = List.length ctx in
-  lift (-1 * len) m
+  if Vars.closed0 m then m else raise PatternMatchingFailure
 | n :: vars ->
   (* change [ x1 ... xn y z1 ... zm |- t ] into
      [ x1 ... xn z1 ... zm |- lam y. t ] *)
   let len = List.length ctx in
-  let init i =
-    if i < pred n then mkRel (i + 2)
-    else if Int.equal i (pred n) then mkRel 1
-    else mkRel (i + 1)
-  in
-  let m = substl (List.init len init) m in
   let pre, suf = List.chop (pred n) ctx in
-  match suf with
+  let (na, t, suf) = match suf with
   | [] -> assert false
-  | (_, na, t) :: suf ->
-    let map i = if i > n then pred i else i in
-    let vars = List.map map vars in
-    (** Check that the abstraction is legal *)
-    let frels = free_rels t in
-    let brels = List.fold_right Int.Set.add vars Int.Set.empty in
-    let () = if not (Int.Set.subset frels brels) then raise PatternMatchingFailure in
-    (** Create the abstraction *)
-    let m = mkLambda (na, t, m) in
-    build_lambda vars (pre @ suf) m
+  | (_, na, t) :: suf -> (na, t, suf)
+  in
+  (** Check that the abstraction is legal by generating a transitive closure of
+      its dependencies. *)
+  let is_nondep t clear = match clear with
+  | [] -> true
+  | _ ->
+    let rels = free_rels t in
+    let check i b = b || not (Int.Set.mem i rels) in
+    List.for_all_i check 1 clear
+  in
+  let fold (_, _, t) clear = is_nondep t clear :: clear in
+  (** Produce a list of booleans: true iff we keep the hypothesis *)
+  let clear = List.fold_right fold pre [false] in
+  let clear = List.drop_last clear in
+  (** If the conclusion depends on a variable we cleared, failure *)
+  let () = if not (is_nondep m clear) then raise PatternMatchingFailure in
+  (** Create the abstracted term *)
+  let fold (k, accu) keep =
+    if keep then
+      let k = succ k in
+      (k, Some k :: accu)
+    else (k, None :: accu)
+  in
+  let keep, shift = List.fold_left fold (0, []) clear in
+  let shift = List.rev shift in
+  let map = function
+  | None -> mkProp (** dummy term *)
+  | Some i -> mkRel (i + 1)
+  in
+  (** [x1 ... xn y z1 ... zm] -> [x1 ... xn f(z1) ... f(zm) y] *)
+  let subst =
+    List.map map shift @
+    mkRel 1 ::
+    List.mapi (fun i _ -> mkRel (i + keep + 2)) suf
+  in
+  let map i (id, na, c) =
+    let i = succ i in
+    let subst = List.skipn i subst in
+    let subst = List.map (fun c -> Vars.lift (- i) c) subst in
+    (id, na, substl subst c)
+  in
+  let pre = List.mapi map pre in
+  let pre = List.filter_with clear pre in
+  let m = substl subst m in
+  let map i =
+    if i > n then i - n + keep
+    else match List.nth shift (i - 1) with
+    | None ->
+      (** We cleared a variable that we wanted to abstract! *)
+      raise PatternMatchingFailure
+    | Some k -> k
+  in
+  let vars = List.map map vars in
+  (** Create the abstraction *)
+  let m = mkLambda (na, Vars.lift keep t, m) in
+  build_lambda vars (pre @ suf) m
 
 let rec extract_bound_aux k accu frels ctx = match ctx with
 | [] -> accu
diff --git a/test-suite/bugs/closed/5377.v b/test-suite/bugs/closed/5377.v
new file mode 100644
index 0000000000..130d9f9abf
--- /dev/null
+++ b/test-suite/bugs/closed/5377.v
@@ -0,0 +1,54 @@
+Goal ((forall (t : Type) (x y : t),
+          True ->
+          x = y)) -> False.
+Proof.
+  intro HG.
+  let P := lazymatch goal with
+  | [ H : forall t x y, True -> @?P t x y
+                        |- _ ]
+    => P
+  end in
+  pose (f := P).
+  unify f (fun (t : Type) (x y : t) => x = y).
+Abort.
+
+Goal True.
+Proof.
+let c := lazymatch constr:(fun (T : nat -> Type) (y : nat) (_ : T y) => y) with
+         | fun _ y _ => @?C y => C
+         end in
+pose (f := c).
+unify f (fun n : nat => n).
+Abort.
+
+Goal (forall x : nat, x = x -> x = x \/ x = x) -> True.
+Proof.
+intro.
+let P := lazymatch goal with
+| [ H : forall y, @?P y -> @?P y \/ _ |- _ ]
+  => P
+end in
+pose (f := P).
+unify f (fun x : nat => x = x).
+Abort.
+
+Goal (forall x : nat, x = x -> x = x \/ x = x) -> True.
+Proof.
+intro.
+lazymatch goal with
+| [ H : forall y, @?P y -> @?Q y \/ _ |- _ ]
+  => idtac
+end.
+Abort.
+
+Axiom eq : forall {T} (_ : T), Prop.
+
+Goal forall _ : (forall t (_ : eq t) (x : t), eq x), Prop.
+Proof.
+intro.
+let P := lazymatch goal with
+| [ H : forall t _ x, @?P t x |- _ ]
+  => P
+end in
+pose (f := P).
+Abort.
-- 
cgit v1.2.3


From b07f7a2ac4f23a29d1762b4f78fc1506925a5019 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 19 Apr 2017 17:41:31 -0400
Subject: Add bedrock targets src and facade

---
 .travis.yml                 |  2 ++
 Makefile.ci                 |  3 +--
 dev/ci/ci-basic-overlay.sh  | 13 ++++++++++++-
 dev/ci/ci-bedrock-facade.sh | 10 ++++++++++
 dev/ci/ci-bedrock-src.sh    | 10 ++++++++++
 5 files changed, 35 insertions(+), 3 deletions(-)
 create mode 100755 dev/ci/ci-bedrock-facade.sh
 create mode 100755 dev/ci/ci-bedrock-src.sh

diff --git a/.travis.yml b/.travis.yml
index 81f50af0a0..77aac23b78 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -27,6 +27,8 @@ env:
   - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
   - TEST_TARGET="validate"                           TW="travis_wait"
   - TEST_TARGET="validate"   COMPILER="4.02.3+32bit" TW="travis_wait"
+  - TEST_TARGET="ci-bedrock-src"
+  - TEST_TARGET="ci-bedrock-facade"
   - TEST_TARGET="ci-color"
   - TEST_TARGET="ci-compcert"
   - TEST_TARGET="ci-coquelicot"
diff --git a/Makefile.ci b/Makefile.ci
index b055ada8e5..4c4606aff6 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -1,11 +1,10 @@
 CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \
            ci-color ci-math-classes ci-tlc ci-fiat-crypto ci-fiat-parsers \
            ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq \
-           ci-unimath ci-vst
+           ci-unimath ci-vst ci-bedrock-src ci-bedrock-facade
 
 .PHONY: $(CI_TARGETS)
 
 # Generic rule, we use make to easy travis integraton with mixed rules
 $(CI_TARGETS): ci-%:
 	./dev/ci/ci-$*.sh
-
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 336ce9d8f1..e0851816ce 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -94,6 +94,18 @@
 : ${fiat_crypto_CI_BRANCH:=master}
 : ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}
 
+########################################################################
+# bedrock_src
+########################################################################
+: ${bedrock_src_CI_BRANCH:=master}
+: ${bedrock_src_CI_GITURL:=https://github.com/JasonGross/bedrock.git}
+
+########################################################################
+# bedrock_facade
+########################################################################
+: ${bedrock_facade_CI_BRANCH:=master}
+: ${bedrock_facade_CI_GITURL:=https://github.com/JasonGross/bedrock.git}
+
 ########################################################################
 # CoLoR
 ########################################################################
@@ -109,4 +121,3 @@
 ########################################################################
 : ${tlc_CI_BRANCH:=master}
 : ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git}
-
diff --git a/dev/ci/ci-bedrock-facade.sh b/dev/ci/ci-bedrock-facade.sh
new file mode 100755
index 0000000000..95cfa3073f
--- /dev/null
+++ b/dev/ci/ci-bedrock-facade.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+bedrock_facade_CI_DIR=${CI_BUILD_DIR}/bedrock-facade
+
+git_checkout ${bedrock_facade_CI_BRANCH} ${bedrock_facade_CI_GITURL} ${bedrock_facade_CI_DIR}
+
+( cd ${bedrock_facade_CI_DIR} && make -j ${NJOBS} facade )
diff --git a/dev/ci/ci-bedrock-src.sh b/dev/ci/ci-bedrock-src.sh
new file mode 100755
index 0000000000..532611d4b3
--- /dev/null
+++ b/dev/ci/ci-bedrock-src.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+bedrock_src_CI_DIR=${CI_BUILD_DIR}/bedrock-src
+
+git_checkout ${bedrock_src_CI_BRANCH} ${bedrock_src_CI_GITURL} ${bedrock_src_CI_DIR}
+
+( cd ${bedrock_src_CI_DIR} && make -j ${NJOBS} src )
-- 
cgit v1.2.3


From cb635eab423cde23757725593ffdfb98f4016881 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 7 Mar 2017 18:13:07 +0100
Subject: Fix an optimization failure in tclPROGRESS.

Due to code reworking, a fastpath got anihilated because the slow path
was computed altogether. We now only compute the slow check whenever the
quick one fails.
---
 engine/proofview.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/engine/proofview.ml b/engine/proofview.ml
index c01879765b..2e6266cf15 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -828,14 +828,12 @@ let tclPROGRESS t =
   let quick_test =
     initial.solution == final.solution && initial.comb == final.comb
   in
-  let exhaustive_test =
+  let test =
+    quick_test ||
     Util.List.for_all2eq begin fun i f ->
       Progress.goal_equal initial.solution i final.solution f
     end initial.comb final.comb
   in
-  let test =
-    quick_test || exhaustive_test
-  in
   if not test then
     tclUNIT res
   else
-- 
cgit v1.2.3