diff options
-rw-r--r-- | .travis.yml | 2 | ||||
-rw-r--r-- | Makefile.ci | 3 | ||||
-rw-r--r-- | dev/ci/ci-basic-overlay.sh | 13 | ||||
-rwxr-xr-x | dev/ci/ci-bedrock-facade.sh | 10 | ||||
-rwxr-xr-x | dev/ci/ci-bedrock-src.sh | 10 | ||||
-rw-r--r-- | pretyping/constr_matching.ml | 79 | ||||
-rw-r--r-- | test-suite/bugs/closed/5377.v | 54 |
7 files changed, 148 insertions, 23 deletions
diff --git a/.travis.yml b/.travis.yml index 72ce17a09..adaae5487 100644 --- a/.travis.yml +++ b/.travis.yml @@ -28,6 +28,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 b055ada8e..4c4606aff 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 336ce9d8f..e0851816c 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -95,6 +95,18 @@ : ${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 ######################################################################## : ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/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 000000000..95cfa3073 --- /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 000000000..532611d4b --- /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 ) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index efe03bc2e..d55350622 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -83,32 +83,71 @@ let add_binders na1 na2 binding_vars (names, terms as subst) = let rec build_lambda sigma vars ctx m = match vars with | [] -> - let len = List.length ctx in - EConstr.Vars.lift (-1 * len) m + if Vars.closed0 sigma m then m else raise PatternMatchingFailure | n :: vars -> - let open EConstr in (* 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 = Vars.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 sigma 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 sigma 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 sigma 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 sigma 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 000000000..130d9f9ab --- /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. |