diff options
| -rw-r--r-- | .circleci/config.yml | 4 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 3 | ||||
| -rw-r--r-- | .travis.yml | 3 | ||||
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | Makefile.ci | 1 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 6 | ||||
| -rwxr-xr-x | dev/ci/ci-pidetop.sh | 13 | ||||
| -rwxr-xr-x | dev/ci/ci-vst.sh | 10 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 7 | ||||
| -rw-r--r-- | engine/evd.ml | 32 | ||||
| -rw-r--r-- | engine/universes.ml | 58 | ||||
| -rw-r--r-- | tactics/tactics.ml | 5 | ||||
| -rw-r--r-- | test-suite/success/intros.v | 24 |
13 files changed, 111 insertions, 61 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index f811f26e1..451b711be 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -209,6 +209,9 @@ jobs: mtac2: <<: *ci-template + pidetop: + <<: *ci-template + sf: <<: *ci-template environment: @@ -266,6 +269,7 @@ workflows: - iris-lambda-rust: *req-main - ltac2: *req-main - math-comp: *req-main + - pidetop: *req-main - sf: *req-main - unimath: *req-main - vst: *req-main diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 6b42ac7eb..d16dc5b78 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -363,6 +363,9 @@ ci-math-comp: ci-mtac2: <<: *ci-template +ci-pidetop: + <<: *ci-template + ci-sf: <<: *ci-template variables: diff --git a/.travis.yml b/.travis.yml index 99e50dc72..fce19f9d9 100644 --- a/.travis.yml +++ b/.travis.yml @@ -120,6 +120,9 @@ matrix: - TEST_TARGET="ci-mtac2" - if: NOT (type = pull_request) env: + - TEST_TARGET="ci-pidetop" + - if: NOT (type = pull_request) + env: - TEST_TARGET="ci-sf" - if: NOT (type = pull_request) env: @@ -19,6 +19,12 @@ Vernacular Commands - Removed deprecated commands Arguments Scope and Implicit Arguments (not the option). Use the Arguments command instead. +Tactics + +- Introduction tactics "intro"/"intros" on a goal which is an + existential variable now force a refinement of the goal into a + dependent product rather than failing. + Tactic language - Support for fix/cofix added in Ltac "match" and "lazymatch". diff --git a/Makefile.ci b/Makefile.ci index 37b14ed91..78fec466c 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -29,6 +29,7 @@ CI_TARGETS=ci-bignums \ ci-math-classes \ ci-math-comp \ ci-mtac2 \ + ci-pidetop \ ci-sf \ ci-tlc \ ci-unimath \ diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 5cee72cc7..1ae2ad0ac 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -156,3 +156,9 @@ ######################################################################## : "${fcsl_pcm_CI_BRANCH:=master}" : "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm.git}" + +######################################################################## +# pidetop +######################################################################## +: "${pidetop_CI_BRANCH:=v8.9}" +: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop.git}" diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh new file mode 100755 index 000000000..d04b9637c --- /dev/null +++ b/dev/ci/ci-pidetop.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +# $0 is not the safest way, but... +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +pidetop_CI_DIR="${CI_BUILD_DIR}/pidetop" + +git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}" + +( cd "${pidetop_CI_DIR}" && coq_makefile -f Make -o Makefile.top && make -f Makefile.top "-j${NJOBS}" && make install-toploop -f Makefile.top ) + +echo -en '4\nexit' | coqtop -main-channel stdfds -toploop pidetop diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 3817edf0c..79001c547 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -8,10 +8,6 @@ VST_CI_DIR="${CI_BUILD_DIR}/VST" # opam install -j ${NJOBS} -y menhir git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}" -# HACK: from the upstream makefile: -# -# default_target: _CoqProject version.vo msl veric floyd progs -# -# We have to omit progs as otherwise we timeout on Travis; once we -# move to Gitlab we will able to just use `make` -( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true _CoqProject version.vo msl veric floyd ) +# We have to omit progs as otherwise we timeout on Travis; on Gitlab +# we will be able to just use `make` +( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true -o progs ) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index a3d06ae04..6c1b1c08c 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -634,7 +634,12 @@ puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` or ``n`` is such that ``Hn`` or ``Xn`` is a fresh identifier. In both cases, the new subgoal is :g:`U`. -If the goal is neither a product nor starting with a let definition, +If the goal is an existential variable, ``intro`` forces the resolution of the +existential variable into a dependent product :math:`\forall`:g:`x:?X, ?Y`, puts +:g:`x:?X` in the local context and leaves :g:`?Y` as a new subgoal allowed to +depend on :g:`x`. + +If the goal is neither a product, nor starting with a let definition, nor an existential variable, the tactic ``intro`` applies the tactic ``hnf`` until the tactic ``intro`` can be applied or the goal is not head-reducible. diff --git a/engine/evd.ml b/engine/evd.ml index 6dcec2760..af22de5cd 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1290,30 +1290,14 @@ module MiniEConstr = struct let unsafe_eq = Refl let to_constr ?(abort_on_undefined_evars=true) sigma c = - let rec to_constr c = match Constr.kind c with - | Evar ev -> - begin match safe_evar_value sigma ev with - | Some c -> to_constr c - | None -> - if abort_on_undefined_evars then - anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term") - else - Constr.map (fun c -> to_constr c) c - end - | Sort (Sorts.Type u) -> - let u' = normalize_universe sigma u in - if u' == u then c else mkSort (Sorts.sort_of_univ u') - | Const (c', u) when not (Univ.Instance.is_empty u) -> - let u' = normalize_universe_instance sigma u in - if u' == u then c else mkConstU (c', u') - | Ind (i, u) when not (Univ.Instance.is_empty u) -> - let u' = normalize_universe_instance sigma u in - if u' == u then c else mkIndU (i, u') - | Construct (co, u) when not (Univ.Instance.is_empty u) -> - let u' = normalize_universe_instance sigma u in - if u' == u then c else mkConstructU (co, u') - | _ -> Constr.map (fun c -> to_constr c) c - in to_constr c + let evar_value = + if not abort_on_undefined_evars then fun ev -> safe_evar_value sigma ev + else fun ev -> + match safe_evar_value sigma ev with + | Some _ as v -> v + | None -> anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term") + in + Universes.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c let of_named_decl d = d let unsafe_to_named_decl d = d diff --git a/engine/universes.ml b/engine/universes.ml index e98708724..0410d1aea 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -592,35 +592,6 @@ let subst_univs_constr = CProfile.profile2 subst_univs_constr_key subst_univs_constr else subst_univs_constr -let subst_univs_fn_puniverses lsubst (c, u as cu) = - let u' = Instance.subst_fn lsubst u in - if u' == u then cu else (c, u') - -let nf_evars_and_universes_opt_subst f subst = - let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in - let lsubst = level_subst_of subst in - let rec aux c = - match kind c with - | Evar (evk, args) -> - let args = Array.map aux args in - (match try f (evk, args) with Not_found -> None with - | None -> c - | Some c -> aux c) - | Const pu -> - let pu' = subst_univs_fn_puniverses lsubst pu in - if pu' == pu then c else mkConstU pu' - | Ind pu -> - let pu' = subst_univs_fn_puniverses lsubst pu in - if pu' == pu then c else mkIndU pu' - | Construct pu -> - let pu' = subst_univs_fn_puniverses lsubst pu in - if pu' == pu then c else mkConstructU pu' - | Sort (Type u) -> - let u' = Univ.subst_univs_universe subst u in - if u' == u then c else mkSort (sort_of_univ u') - | _ -> Constr.map aux c - in aux - let fresh_universe_context_set_instance ctx = if ContextSet.is_empty ctx then LMap.empty, ctx else @@ -679,6 +650,35 @@ let normalize_opt_subst ctx = type universe_opt_subst = Universe.t option universe_map +let subst_univs_fn_puniverses f (c, u as cu) = + let u' = Instance.subst_fn f u in + if u' == u then cu else (c, u') + +let nf_evars_and_universes_opt_subst f subst = + let subst = normalize_univ_variable_opt_subst (ref subst) in + let lsubst = level_subst_of subst in + let rec aux c = + match kind c with + | Evar (evk, args) -> + let args = Array.map aux args in + (match try f (evk, args) with Not_found -> None with + | None -> mkEvar (evk, args) + | Some c -> aux c) + | Const pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkConstU pu' + | Ind pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkIndU pu' + | Construct pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkConstructU pu' + | Sort (Type u) -> + let u' = Univ.subst_univs_universe subst u in + if u' == u then c else mkSort (sort_of_univ u') + | _ -> Constr.map aux c + in aux + let make_opt_subst s = fun x -> (match Univ.LMap.find x s with diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3a20c3fc4..59c035e83 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -979,6 +979,11 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = | LetIn (name,b,t,u) when not dep_flag || not (noccurn sigma 1 u) -> let name = find_name false (LocalDef (name,b,t)) name_flag gl in build_intro_tac name move_flag tac + | Evar ev when force_flag -> + let sigma, t = Evardefine.define_evar_as_product sigma ev in + Tacticals.New.tclTHEN + (Proofview.Unsafe.tclEVARS sigma) + (intro_then_gen name_flag move_flag force_flag dep_flag tac) | _ -> begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct)) (* Note: red_in_concl includes betaiotazeta and this was like *) diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index a329894aa..d37ad9f52 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -127,4 +127,28 @@ induction 1 as (n,H,IH). exact Logic.I. Qed. +(* Make "intro"/"intros" progress on existential variables *) +Module Evar. + +Goal exists (A:Prop), A. +eexists. +unshelve (intro x). +- exact nat. +- exact (x=x). +- auto. +Qed. + +Goal exists (A:Prop), A. +eexists. +unshelve (intros x). +- exact nat. +- exact (x=x). +- auto. +Qed. + +Definition d := ltac:(intro x; exact (x*x)). + +Definition d' : nat -> _ := ltac:(intros;exact 0). + +End Evar. |