diff options
58 files changed, 1253 insertions, 1111 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index b1a805b59e..de0de4cf83 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-11-08-V1" + CACHEKEY: "bionic_coq-V2018-12-05-V1" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -89,18 +89,37 @@ after_script: - set +e +# Template for building Coq + stdlib, typical use: overload the switch .dune-template: &dune-template - dependencies: [] stage: build + dependencies: [] + script: + - set -e + - make -f Makefile.dune world + - set +e + variables: + OPAM_SWITCH: edge artifacts: name: "$CI_JOB_NAME" paths: - _build/ expire_in: 1 week + +.dune-ci-template: &dune-ci-template + stage: test + dependencies: + - build:egde:dune:dev script: - set -e + - echo 'start:coq.test' - make -f Makefile.dune "$DUNE_TARGET" + - echo 'end:coq.test' - set +e + variables: &dune-ci-template-vars + OPAM_SWITCH: edge + artifacts: &dune-ci-template-artifacts + name: "$CI_JOB_NAME" + expire_in: 1 month # every non build job must set dependencies otherwise all build # artifacts are used together and we may get some random Coq. To that @@ -221,9 +240,6 @@ build:edge+flambda: build:egde:dune:dev: <<: *dune-template - variables: - OPAM_SWITCH: edge - DUNE_TARGET: world build:base+async: <<: *build-template @@ -291,15 +307,23 @@ doc:refman: dependencies: - build:base +doc:refman:dune: + <<: *dune-ci-template + variables: + <<: *dune-ci-template-vars + DUNE_TARGET: refman-html + artifacts: + <<: *dune-ci-template-artifacts + paths: + - _build/default/doc/sphinx_build/html + doc:ml-api:odoc: - stage: test - dependencies: - - build:egde:dune:dev - script: make -f Makefile.dune apidoc + <<: *dune-ci-template variables: - OPAM_SWITCH: edge + <<: *dune-ci-template-vars + DUNE_TARGET: apidoc artifacts: - name: "$CI_JOB_NAME" + <<: *dune-ci-template-artifacts paths: - _build/default/_doc/ diff --git a/CHANGES.md b/CHANGES.md index 8cb71f19ea..4fafb9a18a 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -88,6 +88,8 @@ Vernacular commands - The `Automatic Introduction` option has been removed and is now the default. +- `Arguments` now accepts names for arguments provided with `extra_scopes`. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: diff --git a/Makefile.build b/Makefile.build index 0a73562467..34d7ce42f7 100644 --- a/Makefile.build +++ b/Makefile.build @@ -575,11 +575,11 @@ module Gramext = Gramlib__Gramext \ module Grammar = Gramlib__Grammar" > $@ gramlib/.pack/gramlib__P%: gramlib/p% | gramlib/.pack - cp -a $< $@ - sed -e "1i # 1 \"$<\"" -i $@ + printf '# 1 "%s"\n' $< > $@ + cat $< >> $@ gramlib/.pack/gramlib__G%: gramlib/g% | gramlib/.pack - cp -a $< $@ - sed -e "1i # 1 \"$<\"" -i $@ + printf '# 1 "%s"\n' $< > $@ + cat $< >> $@ # Specific rules for gramlib to pack it Dune / OCaml 4.08 style GRAMOBJS=$(addsuffix .cmo, $(GRAMFILES)) diff --git a/Makefile.dune b/Makefile.dune index 2293c69c38..4baf3402f1 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -1,7 +1,10 @@ # -*- mode: makefile -*- # Dune Makefile for Coq -.PHONY: help voboot states world watch check quickbyte quickopt test-suite release apidoc ocheck ireport clean +.PHONY: help voboot states world watch check # Main developer targets +.PHONY: quickbyte quickopt # Partial / quick developer targets +.PHONY: test-suite refman-html apidoc release # Accesory targets +.PHONY: ocheck ireport clean # Maintenance targets # use DUNEOPT=--display=short for a more verbose build # DUNEOPT=--display=short @@ -10,15 +13,20 @@ BUILD_CONTEXT=_build/default help: @echo "Welcome to Coq's Dune-based build system. Targets are:" - @echo " - states: build a minimal functional coqtop" - @echo " - world: build all binaries and libraries" - @echo " - watch: build all binaries and libraries [continuous build]" - @echo " - check: build all ML files as fast as possible [requires Dune >= 1.5.0]" - @echo " - quickbyte: build main ML files [coqtop + plugins + ide + printers] using the bytecode compiler" - @echo " - quickopt: build main ML files [coqtop + plugins + ide + printers] using the optimizing compiler" - @echo " - test-suite: run Coq's test suite" - @echo " - release: build Coq in release mode" - @echo " - apidoc: build ML API documentation" + @echo "" + @echo " - states: build a minimal functional coqtop" + @echo " - world: build all binaries and libraries" + @echo " - watch: build all binaries and libraries [continuous build]" + @echo " - check: build all ML files as fast as possible" + @echo "" + @echo " - quickbyte: build main ML files [coqtop + plugins + ide + printers] using the bytecode compiler" + @echo " - quickopt: build main ML files [coqtop + plugins + ide + printers] using the optimizing compiler" + @echo "" + @echo " - test-suite: run Coq's test suite" + @echo " - refman-html: build Coq's reference manual [HTML version]" + @echo " - apidoc: build ML API documentation" + @echo " - release: build Coq in release mode" + @echo "" @echo " - ocheck: build for all supported OCaml versions [requires OPAM]" @echo " - ireport: build with optimized flambda settings and emit an inline report" @echo " - clean: remove build directory and autogenerated files" @@ -55,12 +63,15 @@ quickopt: voboot test-suite: voboot dune runtest $(DUNEOPT) -release: voboot - dune build $(DUNEOPT) -p coq +refman-html: voboot + dune build @refman-html apidoc: voboot dune build $(DUNEOPT) @doc +release: voboot + dune build $(DUNEOPT) -p coq + ocheck: voboot dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index ef10bf827d..c823db956d 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -8,264 +8,155 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Sorts -open Pp open Declarations open Environ open Names -open CErrors open Univ open Util -open Constr -let check_kind env ar u = - match Constr.kind (snd (Reduction.dest_prod env ar)) with - | Sort (Sorts.Type u') when Univ.Universe.equal u' (Univ.Universe.make u) -> () - | _ -> failwith "not the correct sort" +[@@@ocaml.warning "+9+27"] -let check_polymorphic_arity env params par = - let pl = par.template_param_levels in - let rec check_p env pl params = - let open Context.Rel.Declaration in - match pl, params with - Some u::pl, LocalAssum (na,ty)::params -> - check_kind env ty u; - check_p (push_rel (LocalAssum (na,ty)) env) pl params - | None::pl,d::params -> check_p (push_rel d env) pl params - | [], _ -> () - | _ -> failwith "check_poly: not the right number of params" in - check_p env pl (List.rev params) +exception InductiveMismatch of MutInd.t * string -let conv_ctxt_prefix env (ctx1:rel_context) ctx2 = - let rec chk env rctx1 rctx2 = - let open Context.Rel.Declaration in - match rctx1, rctx2 with - (LocalAssum (_,ty1) as d1)::rctx1', LocalAssum (_,ty2)::rctx2' -> - Reduction.conv env ty1 ty2; - chk (push_rel d1 env) rctx1' rctx2' - | (LocalDef (_,bd1,ty1) as d1)::rctx1', LocalDef (_,bd2,ty2)::rctx2' -> - Reduction.conv env ty1 ty2; - Reduction.conv env bd1 bd2; - chk (push_rel d1 env) rctx1' rctx2' - | [],_ -> () - | _ -> failwith "non convertible contexts" in - chk env (List.rev ctx1) (List.rev ctx2) +let check mind field b = if not b then raise (InductiveMismatch (mind,field)) -(* check information related to inductive arity *) -let typecheck_arity env params inds = - let nparamargs = Context.Rel.nhyps params in - let nparamdecls = Context.Rel.length params in - let check_arity arctxt = function - | RegularArity mar -> - let ar = mar.mind_user_arity in - let _ = Typeops.infer_type env ar in - Reduction.conv env (Term.it_mkProd_or_LetIn (Constr.mkSort mar.mind_sort) arctxt) ar; - ar - | TemplateArity par -> - check_polymorphic_arity env params par; - Term.it_mkProd_or_LetIn (Constr.mkSort(Sorts.Type par.template_level)) arctxt +let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = + let open Entries in + let nparams = List.length mb.mind_params_ctxt in (* include letins *) + let mind_entry_record = match mb.mind_record with + | NotRecord -> None | FakeRecord -> Some None + | PrimRecord data -> Some (Some (Array.map pi1 data)) in - let env_arities = - Array.fold_left - (fun env_ar ind -> - let ar_ctxt = ind.mind_arity_ctxt in - let _ = Typeops.check_context env ar_ctxt in - conv_ctxt_prefix env params ar_ctxt; - (* Arities (with params) are typed-checked here *) - let arity = check_arity ar_ctxt ind.mind_arity in - (* mind_nrealargs *) - let nrealargs = Context.Rel.nhyps ar_ctxt - nparamargs in - if ind.mind_nrealargs <> nrealargs then - failwith "bad number of real inductive arguments"; - let nrealargs_ctxt = Context.Rel.length ar_ctxt - nparamdecls in - if ind.mind_nrealdecls <> nrealargs_ctxt then - failwith "bad length of real inductive arguments signature"; - (* We do not need to generate the universe of full_arity; if - later, after the validation of the inductive definition, - full_arity is used as argument or subject to cast, an - upper universe will be generated *) - let id = ind.mind_typename in - let env_ar' = push_rel (Context.Rel.Declaration.LocalAssum (Name id, arity)) env_ar in - env_ar') - env - inds in - let env_ar_par = push_rel_context params env_arities in - env_arities, env_ar_par - -(* Check that the subtyping information inferred for inductive types in the block is correct. *) -(* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) -let check_subtyping cumi paramsctxt env arities = - let numparams = Context.Rel.nhyps paramsctxt in - (* In [env] we already have [ Var(0) ... Var(n-1) |- cst ] available. - We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n] - and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together - with the cumulativity constraints [ cumul_cst ]. *) - let uctx = ACumulativityInfo.univ_context cumi in - let len = AUContext.size uctx in - let inst = Instance.of_array @@ Array.init len (fun i -> Level.var (i + len)) in - - let other_context = ACumulativityInfo.univ_context cumi in - let uctx_other = UContext.make (inst, AUContext.instantiate inst other_context) in - let cumul_cst = - Array.fold_left_i (fun i csts var -> - match var with - | Variance.Irrelevant -> csts - | Variance.Covariant -> Constraint.add (Level.var i,Le,Level.var (i+len)) csts - | Variance.Invariant -> Constraint.add (Level.var i,Eq,Level.var (i+len)) csts) - Constraint.empty (ACumulativityInfo.variance cumi) + let mind_entry_universes = match mb.mind_universes with + | Monomorphic_ind univs -> Monomorphic_ind_entry univs + | Polymorphic_ind auctx -> Polymorphic_ind_entry (AUContext.names auctx, AUContext.repr auctx) + | Cumulative_ind auctx -> + Cumulative_ind_entry (AUContext.names (ACumulativityInfo.univ_context auctx), + ACumulativityInfo.repr auctx) in - let env = Environ.push_context uctx_other env in - let env = Environ.add_constraints cumul_cst env in - let dosubst = Vars.subst_instance_constr inst in - (* process individual inductive types: *) - Array.iter (fun { mind_user_lc = lc; mind_arity = arity } -> - match arity with - | RegularArity { mind_user_arity = full_arity} -> - Indtypes.check_subtyping_arity_constructor env dosubst full_arity numparams true; - Array.iter (fun cnt -> Indtypes.check_subtyping_arity_constructor env dosubst cnt numparams false) lc - | TemplateArity _ -> - anomaly ~label:"check_subtyping" - Pp.(str "template polymorphism and cumulative polymorphism are not compatible") - ) arities - -(* An inductive definition is a "unit" if it has only one constructor - and that all arguments expected by this constructor are - logical, this is the case for equality, conjunction of logical properties -*) -let is_unit constrsinfos = - match constrsinfos with (* One info = One constructor *) - | [|constrinfos|] -> Univ.is_type0m_univ constrinfos - | [||] -> (* type without constructors *) true - | _ -> false - -let small_unit constrsinfos = - let issmall = Array.for_all Univ.is_small_univ constrsinfos - and isunit = is_unit constrsinfos in - issmall, isunit - -let all_sorts = [InProp;InSet;InType] -let small_sorts = [InProp;InSet] -let logical_sorts = [InProp] - -let allowed_sorts issmall isunit s = - match Sorts.family s with - (* Type: all elimination allowed *) - | InType -> all_sorts - - (* Small Set is predicative: all elimination allowed *) - | InSet when issmall -> all_sorts + let mind_entry_inds = Array.map_to_list (fun ind -> + let mind_entry_arity, mind_entry_template = match ind.mind_arity with + | RegularArity ar -> + let ctx, arity = Term.decompose_prod_n_assum nparams ar.mind_user_arity in + ignore ctx; (* we will check that the produced user_arity is equal to the input *) + arity, false + | TemplateArity ar -> + let ctx = ind.mind_arity_ctxt in + let ctx = List.firstn (List.length ctx - nparams) ctx in + Term.mkArity (ctx, Sorts.sort_of_univ ar.template_level), true + in + { + mind_entry_typename = ind.mind_typename; + mind_entry_arity; + mind_entry_template; + mind_entry_consnames = Array.to_list ind.mind_consnames; + mind_entry_lc = Array.map_to_list (fun c -> + let ctx, c = Term.decompose_prod_n_assum nparams c in + ignore ctx; (* we will check that the produced user_lc is equal to the input *) + c + ) ind.mind_user_lc; + }) + mb.mind_packets + in + { + mind_entry_record; + mind_entry_finite = mb.mind_finite; + mind_entry_params = mb.mind_params_ctxt; + mind_entry_inds; + mind_entry_universes; + mind_entry_private = mb.mind_private; + } + +let check_arity env ar1 ar2 = match ar1, ar2 with + | RegularArity ar, RegularArity {mind_user_arity;mind_sort} -> + Constr.equal ar.mind_user_arity mind_user_arity && + Sorts.equal ar.mind_sort mind_sort + | TemplateArity ar, TemplateArity {template_param_levels;template_level} -> + List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels && + UGraph.check_leq (universes env) template_level ar.template_level + (* template_level is inferred by indtypes, so functor application can produce a smaller one *) + | (RegularArity _ | TemplateArity _), _ -> false + +(* Use [eq_ind_chk] because when we rebuild the recargs we have lost + the knowledge of who is the canonical version. + Try with to see test-suite/coqchk/include.v *) +let eq_recarg a1 a2 = match a1, a2 with + | Norec, Norec -> true + | Mrec i1, Mrec i2 -> eq_ind_chk i1 i2 + | Imbr i1, Imbr i2 -> eq_ind_chk i1 i2 + | (Norec | Mrec _ | Imbr _), _ -> false + +let eq_reloc_tbl = Array.equal (fun x y -> Int.equal (fst x) (fst y) && Int.equal (snd x) (snd y)) + +let check_packet env mind ind + { mind_typename; mind_arity_ctxt; mind_arity; mind_consnames; mind_user_lc; + mind_nrealargs; mind_nrealdecls; mind_kelim; mind_nf_lc; + mind_consnrealargs; mind_consnrealdecls; mind_recargs; mind_nb_constant; + mind_nb_args; mind_reloc_tbl } = + let check = check mind in + + ignore mind_typename; (* passed through *) + check "mind_arity_ctxt" (Context.Rel.equal Constr.equal ind.mind_arity_ctxt mind_arity_ctxt); + check "mind_arity" (check_arity env ind.mind_arity mind_arity); + ignore mind_consnames; (* passed through *) + check "mind_user_lc" (Array.equal Constr.equal ind.mind_user_lc mind_user_lc); + check "mind_nrealargs" Int.(equal ind.mind_nrealargs mind_nrealargs); + check "mind_nrealdecls" Int.(equal ind.mind_nrealdecls mind_nrealdecls); + check "mind_kelim" (List.equal Sorts.family_equal ind.mind_kelim mind_kelim); + + check "mind_nf_lc" (Array.equal Constr.equal ind.mind_nf_lc mind_nf_lc); + (* NB: here syntactic equality is not just an optimisation, we also + care about the shape of the terms *) + + check "mind_consnrealargs" (Array.equal Int.equal ind.mind_consnrealargs mind_consnrealargs); + check "mind_consnrealdecls" (Array.equal Int.equal ind.mind_consnrealdecls mind_consnrealdecls); + + check "mind_recargs" (Rtree.equal eq_recarg ind.mind_recargs mind_recargs); + + check "mind_nb_args" Int.(equal ind.mind_nb_args mind_nb_args); + check "mind_nb_constant" Int.(equal ind.mind_nb_constant mind_nb_constant); + check "mind_reloc_tbl" (eq_reloc_tbl ind.mind_reloc_tbl mind_reloc_tbl); - (* Large Set is necessarily impredicative: forbids large elimination *) - | InSet -> small_sorts + () - (* Unitary/empty Prop: elimination to all sorts are realizable *) - (* unless the type is large. If it is large, forbids large elimination *) - (* which otherwise allows simulating the inconsistent system Type:Type *) - | InProp when isunit -> if issmall then all_sorts else small_sorts +let check_same_record r1 r2 = match r1, r2 with + | NotRecord, NotRecord | FakeRecord, FakeRecord -> true + | PrimRecord r1, PrimRecord r2 -> + (* The kernel doesn't care about the names, we just need to check + that the saved types are correct. *) + Array.for_all2 (fun (_,_,tys1) (_,_,tys2) -> + Array.equal Constr.equal tys1 tys2) + r1 r2 + | (NotRecord | FakeRecord | PrimRecord _), _ -> false + +let check_inductive env mind mb = + let entry = to_entry mb in + let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps; + mind_nparams; mind_nparams_rec; mind_params_ctxt; mind_universes; + mind_private; mind_typing_flags; } + = + (* Locally set the oracle for further typechecking *) + let env = Environ.set_oracle env mb.mind_typing_flags.conv_oracle in + Indtypes.check_inductive env mind entry + in + let check = check mind in - (* Other propositions: elimination only to Prop *) - | InProp -> logical_sorts + Array.iter2 (check_packet env mind) mb.mind_packets mind_packets; + check "mind_record" (check_same_record mb.mind_record mind_record); + check "mind_finite" (mb.mind_finite == mind_finite); + check "mind_ntypes" Int.(equal mb.mind_ntypes mind_ntypes); + check "mind_hyps" (Context.Named.equal Constr.equal mb.mind_hyps mind_hyps); + check "mind_nparams" Int.(equal mb.mind_nparams mind_nparams); -let check_predicativity env s small level = - match s, engagement env with - Type u, _ -> - (* let u' = fresh_local_univ () in *) - (* let cst = *) - (* merge_constraints (enforce_leq u u' empty_constraint) *) - (* (universes env) in *) - if not (UGraph.check_leq (universes env) level u) then - failwith "impredicative Type inductive type" - | Set, ImpredicativeSet -> () - | Set, _ -> - if not small then failwith "impredicative Set inductive type" - | Prop,_ -> () + check "mind_nparams_rec" (mb.mind_nparams_rec <= mind_nparams_rec); + (* module substitution can increase the real number of recursively + uniform parameters, so be tolerant and use [<=]. *) -let sort_of_ind = function - | RegularArity mar -> mar.mind_sort - | TemplateArity par -> Type par.template_level + check "mind_params_ctxt" (Context.Rel.equal Constr.equal mb.mind_params_ctxt mind_params_ctxt); + ignore mind_universes; (* Indtypes did the necessary checking *) + ignore mind_private; (* passed through Indtypes *) -let compute_elim_sorts env_ar params arity lc = - let inst = Context.Rel.to_extended_list Constr.mkRel 0 params in - let env_params = push_rel_context params env_ar in - let lc = Array.map - (fun c -> - Reduction.hnf_prod_applist env_params (Vars.lift (Context.Rel.length params) c) inst) - lc in - let s = sort_of_ind arity in - let infos = Array.map (Indtypes.infos_and_sort env_params) lc in - let (small,unit) = small_unit infos in - (* We accept recursive unit types... *) - (* compute the max of the sorts of the products of the constructor type *) - let min = if Array.length lc > 1 then Universe.type0 else Universe.type0m in - let level = Array.fold_left (fun max l -> Universe.sup max l) min infos in - check_predicativity env_ar s small level; - allowed_sorts small unit s + ignore mind_typing_flags; + (* TODO non oracle flags *) -let typecheck_one_inductive env params mip = - (* mind_typename and mind_consnames not checked *) - (* mind_reloc_tbl, mind_nb_constant, mind_nb_args not checked (VM) *) - (* mind_arity_ctxt, mind_arity, mind_nrealargs DONE (typecheck_arity) *) - (* mind_user_lc *) - let _ = Array.map (Typeops.infer_type env) mip.mind_user_lc in - (* mind_nf_lc *) - let _ = Array.map (Typeops.infer_type env) mip.mind_nf_lc in - Array.iter2 (Reduction.conv env) mip.mind_nf_lc mip.mind_user_lc; - (* mind_consnrealdecls *) - let check_cons_args c n = - let ctx,_ = Term.decompose_prod_assum c in - if n <> Context.Rel.length ctx - Context.Rel.length params then - failwith "bad number of real constructor arguments" in - Array.iter2 check_cons_args mip.mind_nf_lc mip.mind_consnrealdecls; - (* mind_kelim: checked by positivity criterion ? *) - let sorts = - compute_elim_sorts env params mip.mind_arity mip.mind_nf_lc in - let reject_sort s = not (List.mem_f Sorts.family_equal s sorts) in - if List.exists reject_sort mip.mind_kelim then - failwith "elimination not allowed"; - (* mind_recargs: checked by positivity criterion *) - () - -let check_inductive env kn mib = - Flags.if_verbose Feedback.msg_notice (str " checking mutind block: " ++ MutInd.print kn); - (* check mind_constraints: should be consistent with env *) - let env0 = - match mib.mind_universes with - | Monomorphic_ind _ -> env - | Polymorphic_ind auctx -> - let uctx = Univ.AUContext.repr auctx in - Environ.push_context uctx env - | Cumulative_ind cumi -> - let uctx = Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi) in - Environ.push_context uctx env - in - (* Locally set the oracle for further typechecking *) - let env0 = Environ.set_oracle env0 mib.mind_typing_flags.conv_oracle in - (* check mind_record : TODO ? check #constructor = 1 ? *) - (* check mind_finite : always OK *) - (* check mind_ntypes *) - if Array.length mib.mind_packets <> mib.mind_ntypes then - user_err Pp.(str "not the right number of packets"); - (* check mind_params_ctxt *) - let params = mib.mind_params_ctxt in - let _ = Typeops.check_context env0 params in - (* check mind_nparams *) - if Context.Rel.nhyps params <> mib.mind_nparams then - user_err Pp.(str "number the right number of parameters"); - (* mind_packets *) - (* - check arities *) - let env_ar, env_ar_par = typecheck_arity env0 params mib.mind_packets in - (* - check constructor types *) - Array.iter (typecheck_one_inductive env_ar params) mib.mind_packets; - (* check the inferred subtyping relation *) - let () = - match mib.mind_universes with - | Monomorphic_ind _ | Polymorphic_ind _ -> () - | Cumulative_ind acumi -> - check_subtyping acumi params env_ar mib.mind_packets - in - (* check mind_nparams_rec: positivity condition *) - let packets = Array.map (fun p -> (p.mind_typename, Array.to_list p.mind_consnames, p.mind_user_lc, (p.mind_arity_ctxt,p.mind_arity))) mib.mind_packets in - let _ = Indtypes.check_positivity ~chkpos:true kn env_ar_par mib.mind_params_ctxt mib.mind_finite packets in - (* check mind_equiv... *) - (* Now we can add the inductive *) - add_mind kn mib env + add_mind mind mb env diff --git a/checker/checkInductive.mli b/checker/checkInductive.mli index 17ca0d4583..ab54190967 100644 --- a/checker/checkInductive.mli +++ b/checker/checkInductive.mli @@ -8,10 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(*i*) open Names open Environ -(*i*) + +exception InductiveMismatch of MutInd.t * string +(** Some field of the inductive is different from what the kernel infers. *) (*s The following function does checks on inductive declarations. *) diff --git a/checker/checker.ml b/checker/checker.ml index da6a61de1c..167258f8bb 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -302,6 +302,10 @@ let explain_exn = function (* let ctx = Check.get_env() in hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*) + + | CheckInductive.InductiveMismatch (mind,field) -> + hov 0 (MutInd.print mind ++ str ": field " ++ str field ++ str " is incorrect.") + | Assert_failure (s,b,e) -> hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ (if s = "" then mt () diff --git a/config/dune b/config/dune index cc993b97c9..c146e7df67 100644 --- a/config/dune +++ b/config/dune @@ -7,7 +7,7 @@ ; Dune doesn't use configure's output, but it is still necessary for ; some Coq files to work; will be fixed in the future. (rule - (targets coq_config.ml Makefile) + (targets coq_config.ml coq_config.py Makefile) (mode fallback) (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX)) (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no)))) diff --git a/coq-refman.opam b/coq-refman.opam new file mode 100644 index 0000000000..b9500243a3 --- /dev/null +++ b/coq-refman.opam @@ -0,0 +1,39 @@ +synopsis: "The Coq Proof Assistant --- Reference Manual" +description: """ +Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. + +This package provides the Coq Reference Manual. +""" +opam-version: "2.0" +maintainer: "The Coq development team <coqdev@inria.fr>" +authors: "The Coq development team, INRIA, CNRS, and contributors." +homepage: "https://coq.inria.fr/" +bug-reports: "https://github.com/coq/coq/issues" +dev-repo: "https://github.com/coq/coq.git" +license: "Open Publication License" + +depends: [ + "dune" { build } + "coq" { build } +] + +build-env: [ + [ COQ_CONFIGURE_PREFIX = "%{prefix}" ] +] + +build: [ + [ "dune" "build" "@refman" "-j" jobs ] +] + +# Would be better to have a *-conf package? +depexts: [ + [ "sphinx" ] + [ "sphinx_rtd_theme" ] + [ "beautifulsoup4" ] + [ "antlr4-python3-runtime"] + [ "pexpect" ] + [ "sphinxcontrib-bibtex" ] +] diff --git a/default.nix b/default.nix index eeab388cb4..89d69cc40f 100644 --- a/default.nix +++ b/default.nix @@ -23,8 +23,8 @@ { pkgs ? (import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/69522a0acf8e840e8b6ac0a9752a034ab74eb3c0.tar.gz"; - sha256 = "12k80gd4lkw9h9y1szvmh0jmh055g3b6wnphmx4ab1qdwlfaylnx"; + url = "https://github.com/NixOS/nixpkgs/archive/958a6c6dd39b0d6628e1408e798a8f1308f2f3e1.tar.gz"; + sha256 = "0vs6k4jn0rbdfzaxmh3xh64q213326680i9g3cjgr7l9y6h6m5sy"; }) {}) , ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_06 , buildIde ? true diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index 33feeed45c..8489bcfc3a 100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -55,7 +55,7 @@ IF DEFINED HTTP_PROXY ( )
REM see -cygrepo in ReadMe.txt
-SET CYGWIN_REPOSITORY=http://ftp.inf.tu-dresden.de/software/windows/cygwin32
+SET CYGWIN_REPOSITORY=http://mirror.easyname.at/cygwin
REM see -cygcache in ReadMe.txt
SET CYGWIN_LOCAL_CACHE_WFMT=%BATCHDIR%cygwin_cache
diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index cda369fb1b..470d07b27d 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -13,4 +13,4 @@ eval "$(opam env)" opam install -y num ocamlfind ounit # Full regular Coq Build -cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= # && make validate +cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte # && make -C test-suite all INTERACTIVE= # && make validate diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 3fc6dce4e5..f1020e5f8e 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-11-08-V1" +# CACHEKEY: "bionic_coq-V2018-12-05-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -37,7 +37,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.4.0 ounit.2.0.8 odoc.1.3.0" \ +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.1 ounit.2.0.8 odoc.1.3.0" \ CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. diff --git a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh new file mode 100644 index 0000000000..f532fdfc52 --- /dev/null +++ b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9172" ] || [ "$CI_BRANCH" = "proof_rework" ]; then + + ltac2_CI_REF=proof_rework + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + mtac2_CI_REF=proof_rework + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + +fi diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 3609171b82..01c32041d2 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -10,9 +10,9 @@ Coq can now be built using [Dune](https://github.com/ocaml/dune). ## Quick Start -Dune >= 1.5.0 is recommended, see `dune-project` for the minimum -required version; type `dune build` to build the base Coq -libraries. No call to `./configure` is needed. +Usually, using the latest version of Dune is recommended, see +`dune-project` for the minimum required version; type `dune build` to +build the base Coq libraries. No call to `./configure` is needed. Dune will get confused if it finds leftovers of in-tree compilation, so please be sure your tree is clean from objects files generated by @@ -63,11 +63,16 @@ ml files in quick mode. Dune also provides targets for documentation, testing, and release builds, please see below. -## Documentation and test targets +## Documentation and testing targets Coq's test-suite can be run with `dune runtest`. -The documentation target is not implemented in Dune yet. +There is preliminary support to build the API documentation and +reference manual in HTML format, use `dune build {@doc,@refman-html}` +to generate them. + +So far these targets will build the documentation artifacts, however +no install rules are generated yet. ## Developer shell diff --git a/doc/dune b/doc/dune new file mode 100644 index 0000000000..54ffa87205 --- /dev/null +++ b/doc/dune @@ -0,0 +1,24 @@ +(rule + (targets sphinx_build) + (deps + ; We could use finer dependencies here so the build is faster: + ; + ; - vo files: generated by sphinx after parsing the doc, promoted, + ; - Static files: + ; + %{bin:coqdoc} etc... + ; + config/coq_config.py + ; + tools/coqdoc/coqdoc.css + (package coq) + (source_tree sphinx) + (source_tree tools)) + (action (run sphinx-build -j4 -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + +(alias + (name refman-html) + (deps sphinx_build)) + +; The install target still needs more work. +; (install +; (section doc) +; (package coq-refman) +; (files sphinx_build)) diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index e681d0f3ff..39047f4f23 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -61,7 +61,7 @@ extensions = [ # Change this to "info" or "warning" to get notifications about undocumented Coq # objects (objects with no contents). -report_undocumented_coq_objects = None +report_undocumented_coq_objects = "warning" # Add any paths that contain templates here, relative to this directory. templates_path = ['_templates'] diff --git a/doc/sphinx/dune b/doc/sphinx/dune new file mode 100644 index 0000000000..fff025c919 --- /dev/null +++ b/doc/sphinx/dune @@ -0,0 +1 @@ +(dirs :standard _static) diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 9fbac95f0c..b664eb4ec5 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -418,30 +418,29 @@ each point of use, e.g., the above definition can be written: Prenex Implicits null. Definition all_null (s : list T) := all null s. -Better yet, it can be omitted entirely, since ``all_null s`` isn’t much of -an improvement over ``all null s``. +Better yet, it can be omitted entirely, since :g:`all_null s` isn’t much of +an improvement over :g:`all null s`. The syntax of the new declaration is -.. cmd:: Prenex Implicits {+ @ident} +.. cmd:: Prenex Implicits {+ @ident__i} -Let us denote :math:`c_1` … :math:`c_n` the list of identifiers given to a -``Prenex Implicits`` command. The command checks that each ci is the name of -a functional constant, whose implicit arguments are prenex, i.e., the first -:math:`n_i > 0` arguments of :math:`c_i` are implicit; then it assigns -``Maximal Implicit`` status to these arguments. + This command checks that each :n:`@ident__i` is the name of a functional + constant, whose implicit arguments are prenex, i.e., the first + :math:`n_i > 0` arguments of :n:`@ident__i` are implicit; then it assigns + ``Maximal Implicit`` status to these arguments. -As these prenex implicit arguments are ubiquitous and have often large -display strings, it is strongly recommended to change the default -display settings of |Coq| so that they are not printed (except after -a ``Set Printing All`` command). All |SSR| library files thus start -with the incantation + As these prenex implicit arguments are ubiquitous and have often large + display strings, it is strongly recommended to change the default + display settings of |Coq| so that they are not printed (except after + a ``Set Printing All`` command). All |SSR| library files thus start + with the incantation -.. coqtop:: all undo + .. coqtop:: all undo - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. Anonymous arguments @@ -601,25 +600,21 @@ resemble ML-like definitions of polymorphic functions. Abbreviations ~~~~~~~~~~~~~ -The |SSR| set tactic performs abbreviations: it introduces a -defined constant for a subterm appearing in the goal and/or in the -context. - -|SSR| extends the set tactic by supplying: - - -+ an open syntax, similarly to the pose tactic; -+ a more aggressive matching algorithm; -+ an improved interpretation of wildcards, taking advantage of the - matching algorithm; -+ an improved occurrence selection mechanism allowing to abstract only - selected occurrences of a term. +.. tacn:: set @ident {? : @term } := {? @occ_switch } @term + :name: set (ssreflect) + The |SSR| ``set`` tactic performs abbreviations: it introduces a + defined constant for a subterm appearing in the goal and/or in the + context. -The general syntax of this tactic is + |SSR| extends the :tacn:`set` tactic by supplying: -.. tacn:: set @ident {? : @term } := {? @occ_switch } @term - :name: set (ssreflect) + + an open syntax, similarly to the :tacn:`pose (ssreflect)` tactic; + + a more aggressive matching algorithm; + + an improved interpretation of wildcards, taking advantage of the + matching algorithm; + + an improved occurrence selection mechanism allowing to abstract only + selected occurrences of a term. .. prodn:: occ_switch ::= { {? + %| - } {* @num } } @@ -903,23 +898,15 @@ Basic localization ~~~~~~~~~~~~~~~~~~ It is possible to define an abbreviation for a term appearing in the -context of a goal thanks to the in tactical. - -A tactic of the form: +context of a goal thanks to the ``in`` tactical. .. tacv:: set @ident := @term in {+ @ident} -introduces a defined constant called ``x`` in the context, and folds it in -the context entries mentioned on the right hand side of ``in``. -The body of ``x`` is the first subterm matching these context entries -(taken in the given order). - -A tactic of the form: - -.. tacv:: set @ident := @term in {+ @ident} * - -matches term and then folds ``x`` similarly in all the given context entries -but also folds ``x`` in the goal. + This variant of :tacn:`set (ssreflect)` introduces a defined constant + called :token:`ident` in the context, and folds it in + the context entries mentioned on the right hand side of ``in``. + The body of :token:`ident` is the first subterm matching these context + entries (taken in the given order). .. example:: @@ -932,7 +919,10 @@ but also folds ``x`` in the goal. Lemma test x t (Hx : x = 3) : x + t = 4. set z := 3 in Hx. -If the localization also mentions the goal, then the result is the following one: +.. tacv:: set @ident := @term in {+ @ident} * + + This variant matches :token:`term` and then folds :token:`ident` similarly + in all the given context entries but also folds :token:`ident` in the goal. .. example:: @@ -945,7 +935,7 @@ If the localization also mentions the goal, then the result is the following one Lemma test x t (Hx : x = 3) : x + t = 4. set z := 3 in Hx * . -Indeed, remember that 4 is just a notation for (S 3). + Indeed, remember that 4 is just a notation for (S 3). The use of the ``in`` tactical is not limited to the localization of abbreviations: for a complete description of the in tactical, see @@ -1202,77 +1192,82 @@ context manipulations and the main backward chaining tool. The move tactic. ```````````````` -The move tactic, in its defective form, behaves like the primitive ``hnf`` -|Coq| tactic. For example, such a defective: - .. tacn:: move :name: move -exposes the first assumption in the goal, i.e. its changes the -goal ``not False`` into ``False -> False``. + This tactic, in its defective form, behaves like the :tacn:`hnf` tactic. + + .. example:: -More precisely, the ``move`` tactic inspects the goal and does nothing -(``idtac``) if an introduction step is possible, i.e. if the goal is a -product or a ``let…in``, and performs ``hnf`` otherwise. + .. coqtop:: reset all -Of course this tactic is most often used in combination with the -bookkeeping tacticals (see section :ref:`introduction_ssr` and :ref:`discharge_ssr`). These -combinations mostly subsume the :tacn:`intros`, :tacn:`generalize`, :tacn:`revert`, :tacn:`rename`, -:tacn:`clear` and :tacn:`pattern` tactics. + Require Import ssreflect. + Goal not False. + move. + + More precisely, the :tacn:`move` tactic inspects the goal and does nothing + (:tacn:`idtac`) if an introduction step is possible, i.e. if the goal is a + product or a ``let … in``, and performs :tacn:`hnf` otherwise. + + Of course this tactic is most often used in combination with the bookkeeping + tacticals (see section :ref:`introduction_ssr` and :ref:`discharge_ssr`). + These combinations mostly subsume the :tacn:`intros`, :tacn:`generalize`, + :tacn:`revert`, :tacn:`rename`, :tacn:`clear` and :tacn:`pattern` tactics. The case tactic ``````````````` -The ``case`` tactic performs *primitive case analysis* on (co)inductive -types; specifically, it destructs the top variable or assumption of -the goal, exposing its constructor(s) and its arguments, as well as -setting the value of its type family indices if it belongs to a type -family (see section :ref:`type_families_ssr`). +.. tacn:: case + :name: case (ssreflect) + + This tactic performs *primitive case analysis* on (co)inductive + types; specifically, it destructs the top variable or assumption of + the goal, exposing its constructor(s) and its arguments, as well as + setting the value of its type family indices if it belongs to a type + family (see section :ref:`type_families_ssr`). -The |SSR| case tactic has a special behavior on equalities. If the -top assumption of the goal is an equality, the case tactic “destructs” -it as a set of equalities between the constructor arguments of its -left and right hand sides, as per the tactic injection. For example, -``case`` changes the goal:: + The |SSR| case tactic has a special behavior on equalities. If the + top assumption of the goal is an equality, the case tactic “destructs” + it as a set of equalities between the constructor arguments of its + left and right hand sides, as per the tactic injection. For example, + ``case`` changes the goal:: - (x, y) = (1, 2) -> G. + (x, y) = (1, 2) -> G. -into:: + into:: - x = 1 -> y = 2 -> G. + x = 1 -> y = 2 -> G. -Note also that the case of |SSR| performs ``False`` elimination, even -if no branch is generated by this case operation. Hence the command: -``case.`` on a goal of the form ``False -> G`` will succeed and -prove the goal. + Note also that the case of |SSR| performs :g:`False` elimination, even + if no branch is generated by this case operation. Hence the tactic + :tacn:`case` on a goal of the form :g:`False -> G` will succeed and + prove the goal. The elim tactic ``````````````` -The ``elim`` tactic performs inductive elimination on inductive types. The -defective: - .. tacn:: elim :name: elim (ssreflect) -tactic performs inductive elimination on a goal whose top assumption -has an inductive type. + This tactic performs inductive elimination on inductive types. In its + defective form, the tactic performs inductive elimination on a goal whose + top assumption has an inductive type. -.. example:: + .. example:: - .. coqtop:: reset + .. coqtop:: reset - From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. - .. coqtop:: all + .. coqtop:: all - Lemma test m : forall n : nat, m <= n. - elim. + Lemma test m : forall n : nat, m <= n. + elim. .. _apply_ssr: @@ -1280,27 +1275,25 @@ has an inductive type. The apply tactic ```````````````` -The ``apply`` tactic is the main backward chaining tactic of the proof -system. It takes as argument any :token:`term` and applies it to the goal. -Assumptions in the type of :token:`term` that don’t directly match the goal -may generate one or more subgoals. - -In fact the |SSR| tactic: - -.. tacn:: apply +.. tacn:: apply {? @term } :name: apply (ssreflect) -is a synonym for:: + This is the main backward chaining tactic of the proof system. + It takes as argument any :token:`term` and applies it to the goal. + Assumptions in the type of :token:`term` that don’t directly match the goal + may generate one or more subgoals. + + In its defective form, this tactic is a synonym for:: - intro top; first [refine top | refine (top _) | refine (top _ _) | …]; clear top. + intro top; first [refine top | refine (top _) | refine (top _ _) | …]; clear top. -where ``top`` is a fresh name, and the sequence of refine tactics tries to -catch the appropriate number of wildcards to be inserted. Note that -this use of the refine tactic implies that the tactic tries to match -the goal up to expansion of constants and evaluation of subterms. + where :g:`top` is a fresh name, and the sequence of :tacn:`refine` tactics + tries to catch the appropriate number of wildcards to be inserted. Note that + this use of the :tacn:`refine` tactic implies that the tactic tries to match + the goal up to expansion of constants and evaluation of subterms. -|SSR|’s apply has a special behavior on goals containing -existential metavariables of sort Prop. +:tacn:`apply (ssreflect)` has a special behavior on goals containing +existential metavariables of sort :g:`Prop`. .. example:: @@ -1348,6 +1341,7 @@ The general syntax of the discharging tactical ``:`` is: .. tacn:: @tactic {? @ident } : {+ @d_item } {? @clear_switch } :name: ... : ... (ssreflect) + :undocumented: .. prodn:: d_item ::= {? @occ_switch %| @clear_switch } @term @@ -1502,8 +1496,8 @@ The abstract tactic .. tacn:: abstract: {+ d_item} :name: abstract (ssreflect) -This tactic assigns an abstract constant previously introduced with the ``[: -name ]`` intro pattern (see section :ref:`introduction_ssr`). + This tactic assigns an abstract constant previously introduced with the + :n:`[: @ident ]` intro pattern (see section :ref:`introduction_ssr`). In a goal like the following:: @@ -1553,6 +1547,7 @@ whose general syntax is .. tacn:: @tactic => {+ @i_item } :name: => + :undocumented: .. prodn:: i_item ::= @i_pattern %| @s_item %| @clear_switch %| {? %{%} } /@term @@ -1803,136 +1798,132 @@ Type families ~~~~~~~~~~~~~ When the top assumption of a goal has an inductive type, two specific -operations are possible: the case analysis performed by the ``case`` +operations are possible: the case analysis performed by the :tacn:`case` tactic, and the application of an induction principle, performed by -the ``elim`` tactic. When this top assumption has an inductive type, which +the :tacn:`elim` tactic. When this top assumption has an inductive type, which is moreover an instance of a type family, |Coq| may need help from the user to specify which occurrences of the parameters of the type should be substituted. -A specific ``/`` switch indicates the type family parameters of the type -of a :token:`d_item` immediately following this ``/`` switch, -using the syntax: - .. tacv:: case: {+ @d_item } / {+ @d_item } - :name: case (ssreflect) + elim: {+ @d_item } / {+ @d_item } + + A specific ``/`` switch indicates the type family parameters of the type + of a :token:`d_item` immediately following this ``/`` switch. + The :token:`d_item` on the right side of the ``/`` switch are discharged as + described in section :ref:`discharge_ssr`. The case analysis or elimination + will be done on the type of the top assumption after these discharge + operations. + + Every :token:`d_item` preceding the ``/`` is interpreted as arguments of this + type, which should be an instance of an inductive type family. These terms + are not actually generalized, but rather selected for substitution. + Occurrence switches can be used to restrict the substitution. If a term is + left completely implicit (e.g. writing just ``_``), then a pattern is + inferred looking at the type of the top assumption. This allows for the + compact syntax: -.. tacv:: elim: {+ @d_item } / {+ @d_item } + .. coqtop:: in -The :token:`d_item` on the right side of the ``/`` switch are discharged as -described in section :ref:`discharge_ssr`. The case analysis or elimination -will be done on the type of the top assumption after these discharge -operations. + case: {2}_ / eqP. -Every :token:`d_item` preceding the ``/`` is interpreted as arguments of this -type, which should be an instance of an inductive type family. These terms -are not actually generalized, but rather selected for substitution. -Occurrence switches can be used to restrict the substitution. If a term is -left completely implicit (e.g. writing just ``_``), then a pattern is -inferred looking at the type of the top assumption. This allows for the -compact syntax: + where ``_`` is interpreted as ``(_ == _)`` since + ``eqP T a b : reflect (a = b) (a == b)`` and reflect is a type family with + one index. -.. coqtop:: in + Moreover if the :token:`d_item` list is too short, it is padded with an + initial sequence of ``_`` of the right length. - case: {2}_ / eqP. + .. example:: -where ``_`` is interpreted as ``(_ == _)`` since -``eqP T a b : reflect (a = b) (a == b)`` and reflect is a type family with -one index. + Here is a small example on lists. We define first a function which + adds an element at the end of a given list. -Moreover if the :token:`d_item` list is too short, it is padded with an -initial sequence of ``_`` of the right length. + .. coqtop:: reset -.. example:: + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. - Here is a small example on lists. We define first a function which - adds an element at the end of a given list. + .. coqtop:: all - .. coqtop:: reset + Require Import List. + Section LastCases. + Variable A : Type. + Implicit Type l : list A. + Fixpoint add_last a l : list A := + match l with + | nil => a :: nil + | hd :: tl => hd :: (add_last a tl) end. - From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + Then we define an inductive predicate for case analysis on lists + according to their last element: - .. coqtop:: all + .. coqtop:: all - Require Import List. - Section LastCases. - Variable A : Type. - Implicit Type l : list A. - Fixpoint add_last a l : list A := - match l with - | nil => a :: nil - | hd :: tl => hd :: (add_last a tl) end. + Inductive last_spec : list A -> Type := + | LastSeq0 : last_spec nil + | LastAdd s x : last_spec (add_last x s). - Then we define an inductive predicate for case analysis on lists - according to their last element: + Theorem lastP : forall l : list A, last_spec l. + Admitted. - .. coqtop:: all + We are now ready to use ``lastP`` in conjunction with ``case``. - Inductive last_spec : list A -> Type := - | LastSeq0 : last_spec nil - | LastAdd s x : last_spec (add_last x s). + .. coqtop:: all - Theorem lastP : forall l : list A, last_spec l. - Admitted. + Lemma test l : (length l) * 2 = length (l ++ l). + case: (lastP l). - We are now ready to use ``lastP`` in conjunction with ``case``. + Applied to the same goal, the command: + ``case: l / (lastP l).`` + generates the same subgoals but ``l`` has been cleared from both contexts. - .. coqtop:: all + Again applied to the same goal, the command. - Lemma test l : (length l) * 2 = length (l ++ l). - case: (lastP l). + .. coqtop:: none - Applied to the same goal, the command: - ``case: l / (lastP l).`` - generates the same subgoals but ``l`` has been cleared from both contexts. + Abort. - Again applied to the same goal, the command. + .. coqtop:: all - .. coqtop:: none + Lemma test l : (length l) * 2 = length (l ++ l). + case: {1 3}l / (lastP l). - Abort. - - .. coqtop:: all - - Lemma test l : (length l) * 2 = length (l ++ l). - case: {1 3}l / (lastP l). - - Note that selected occurrences on the left of the ``/`` - switch have been substituted with l instead of being affected by - the case analysis. + Note that selected occurrences on the left of the ``/`` + switch have been substituted with l instead of being affected by + the case analysis. -The equation name generation feature combined with a type family / -switch generates an equation for the *first* dependent :token:`d_item` -specified by the user. Again starting with the above goal, the -command: + The equation name generation feature combined with a type family ``/`` + switch generates an equation for the *first* dependent :token:`d_item` + specified by the user. Again starting with the above goal, the + command: -.. example:: + .. example:: - .. coqtop:: none + .. coqtop:: none - Abort. + Abort. - .. coqtop:: all + .. coqtop:: all - Lemma test l : (length l) * 2 = length (l ++ l). - case E: {1 3}l / (lastP l) => [|s x]. - Show 2. + Lemma test l : (length l) * 2 = length (l ++ l). + case E: {1 3}l / (lastP l) => [|s x]. + Show 2. -There must be at least one :token:`d_item` to the left of the / switch; this -prevents any confusion with the view feature. However, the :token:`d_item` -to the right of the ``/`` are optional, and if they are omitted the first -assumption provides the instance of the type family. + There must be at least one :token:`d_item` to the left of the ``/`` switch; this + prevents any confusion with the view feature. However, the :token:`d_item` + to the right of the ``/`` are optional, and if they are omitted the first + assumption provides the instance of the type family. -The equation always refers to the first :token:`d_item` in the actual tactic -call, before any padding with initial ``_``. Thus, if an inductive type -has two family parameters, it is possible to have|SSR| generate an -equation for the second one by omitting the pattern for the first; -note however that this will fail if the type of the second parameter -depends on the value of the first parameter. + The equation always refers to the first :token:`d_item` in the actual tactic + call, before any padding with initial ``_``. Thus, if an inductive type + has two family parameters, it is possible to have|SSR| generate an + equation for the second one by omitting the pattern for the first; + note however that this will fail if the type of the second parameter + depends on the value of the first parameter. Control flow @@ -1991,13 +1982,14 @@ closed tactic fails to prove its subgoal. It is hence recommended practice that the proof of any subgoal should end with a tactic which *fails if it does not solve the current goal*, -like discriminate, contradiction or assumption. +like :tacn:`discriminate`, :tacn:`contradiction` or :tacn:`assumption`. In fact, |SSR| provides a generic tactical which turns any tactic -into a closing one (similar to now). Its general syntax is: +into a closing one (similar to :tacn:`now`). Its general syntax is: .. tacn:: by @tactic :name: by + :undocumented: The Ltac expression :n:`by [@tactic | [@tactic | …]` is equivalent to :n:`[by @tactic | by @tactic | ...]` and this form should be preferred @@ -2014,39 +2006,29 @@ with a ``by``, like in: .. tacn:: done :name: done -The :tacn:`by` tactical is implemented using the user-defined, and extensible -:tacn:`done` tactic. This :tacn:`done` tactic tries to solve the current goal by some -trivial means and fails if it doesn’t succeed. Indeed, the tactic -expression :n:`by @tactic` is equivalent to :n:`@tactic; done`. + The :tacn:`by` tactical is implemented using the user-defined, and extensible + :tacn:`done` tactic. This :tacn:`done` tactic tries to solve the current goal by some + trivial means and fails if it doesn’t succeed. Indeed, the tactic + expression :n:`by @tactic` is equivalent to :n:`@tactic; done`. -Conversely, the tactic + Conversely, the tactic ``by [ ]`` is equivalent to :tacn:`done`. -.. coqtop:: + The default implementation of the done tactic, in the ``ssreflect.v`` + file, is: - by [ ]. + .. coqdoc:: -is equivalent to: + Ltac done := + trivial; hnf; intros; solve + [ do ![solve [trivial | apply: sym_equal; trivial] + | discriminate | contradiction | split] + | case not_locked_false_eq_true; assumption + | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. -.. coqtop:: - - done. - -The default implementation of the done tactic, in the ``ssreflect.v`` -file, is: - -.. coqtop:: in - - Ltac done := - trivial; hnf; intros; solve - [ do ![solve [trivial | apply: sym_equal; trivial] - | discriminate | contradiction | split] - | case not_locked_false_eq_true; assumption - | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. - -The lemma ``not_locked_false_eq_true`` is needed to discriminate -*locked* boolean predicates (see section :ref:`locking_ssr`). The iterator -tactical do is presented in section :ref:`iteration_ssr`. This tactic can be -customized by the user, for instance to include an ``auto`` tactic. + The lemma :g:`not_locked_false_eq_true` is needed to discriminate + *locked* boolean predicates (see section :ref:`locking_ssr`). The iterator + tactical do is presented in section :ref:`iteration_ssr`. This tactic can be + customized by the user, for instance to include an :tacn:`auto` tactic. A natural and common way of closing a goal is to apply a lemma which is the exact one needed for the goal to be solved. The defective form @@ -2063,7 +2045,7 @@ is equivalent to: do [done | by move=> top; apply top]. where ``top`` is a fresh name assigned to the top assumption of the goal. -This applied form is supported by the : discharge tactical, and the +This applied form is supported by the ``:`` discharge tactical, and the tactic: .. coqtop:: in @@ -2106,57 +2088,47 @@ is equivalent to: Selectors ~~~~~~~~~ -When composing tactics, the two tacticals ``first`` and ``last`` let the user -restrict the application of a tactic to only one of the subgoals -generated by the previous tactic. This covers the frequent cases where -a tactic generates two subgoals one of which can be easily disposed -of. - -This is another powerful way of linearization of scripts, since it -happens very often that a trivial subgoal can be solved in a less than -one line tactic. For instance, the tactic: - -.. tacn:: @tactic ; last by @tactic - :name: last - -tries to solve the last subgoal generated by the first -tactic using the given second tactic, and fails if it does not succeed. -Its analogue - -.. tacn:: @tactic ; first by @tactic - :name: first (ssreflect) - -tries to solve the first subgoal generated by the first tactic using the -second given tactic, and fails if it does not succeed. +.. tacn:: last + first + :name: last; first (ssreflect) + + When composing tactics, the two tacticals ``first`` and ``last`` let the user + restrict the application of a tactic to only one of the subgoals + generated by the previous tactic. This covers the frequent cases where + a tactic generates two subgoals one of which can be easily disposed + of. + + This is another powerful way of linearization of scripts, since it + happens very often that a trivial subgoal can be solved in a less than + one line tactic. For instance, :n:`@tactic ; last by @tactic` + tries to solve the last subgoal generated by the first + tactic using the given second tactic, and fails if it does not succeed. + Its analogue :n:`@tactic ; first by @tactic` + tries to solve the first subgoal generated by the first tactic using the + second given tactic, and fails if it does not succeed. |SSR| also offers an extension of this facility, by supplying -tactics to *permute* the subgoals generated by a tactic. The tactic: - -.. tacv:: @tactic; last first - -inverts the order of the subgoals generated by tactic. It is -equivalent to: - -.. tacv:: @tactic; first last +tactics to *permute* the subgoals generated by a tactic. -More generally, the tactic: +.. tacv:: last first + first last + :name: last first; first last -.. tacn:: @tactic; last @num first - :name: last first + These two equivalent tactics invert the order of the subgoals in focus. -where :token:`num` is a |Coq| numeral, or an Ltac variable -denoting a |Coq| -numeral, having the value k. It rotates the n subgoals G1 , …, Gn -generated by tactic. The first subgoal becomes Gn + 1 − k and the -circular order of subgoals remains unchanged. + .. tacv:: last @num first -Conversely, the tactic: + If :token:`num`\'s value is :math:`k`, + this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n` + in focus. The first subgoal becomes :math:`G_{n + 1 − k}` and the + circular order of subgoals remains unchanged. -.. tacn:: @tactic; first @num last - :name: first last + .. tacn:: first @num last -rotates the n subgoals G1 , …, Gn generated by tactic in order that -the first subgoal becomes Gk . + If :token:`num`\'s value is :math:`k`, + this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n` + in focus. The first subgoal becomes :math:`G_k` and the circular order + of subgoals remains unchanged. Finally, the tactics ``last`` and ``first`` combine with the branching syntax of Ltac: if the tactic generates n subgoals on a given goal, @@ -2200,16 +2172,14 @@ to the others. Iteration ~~~~~~~~~ -|SSR| offers an accurate control on the repetition of tactics, -thanks to the do tactical, whose general syntax is: - -.. tacn:: do {? @mult } ( @tactic | [ {+| @tactic } ] ) +.. tacn:: do {? @num } ( @tactic | [ {+| @tactic } ] ) :name: do (ssreflect) -where :token:`mult` is a *multiplier*. + This tactical offers an accurate control on the repetition of tactics. + :token:`mult` is a *multiplier*. -Brackets can only be omitted if a single tactic is given *and* a -multiplier is present. + Brackets can only be omitted if a single tactic is given *and* a + multiplier is present. A tactic of the form: @@ -2274,6 +2244,7 @@ already presented the *localization* tactical in, whose general syntax is: .. tacn:: @tactic in {+ @ident} {? * } :name: in + :undocumented: where :token:`ident` is a name in the context. On the left side of ``in``, @@ -2318,17 +2289,15 @@ of a local definition during the generalization phase, the name of the local definition must be written between parentheses, like in ``rewrite H in H1 (def_n) H2.`` -From |SSR| 1.5 the grammar for the in tactical has been extended -to the following one: - .. tacv:: @tactic in {+ @clear_switch | {? @ } @ident | ( @ident ) | ( {? @ } @ident := @c_pattern ) } {? * } -In its simplest form the last option lets one rename hypotheses that -can’t be cleared (like section variables). For example, ``(y := x)`` -generalizes over ``x`` and reintroduces the generalized variable under the -name ``y`` (and does not clear ``x``). -For a more precise description of this form of localization refer -to :ref:`advanced_generalization_ssr`. + This is the most general form of the ``in`` tactical. + In its simplest form the last option lets one rename hypotheses that + can’t be cleared (like section variables). For example, ``(y := x)`` + generalizes over ``x`` and reintroduces the generalized variable under the + name ``y`` (and does not clear ``x``). + For a more precise description of this form of localization refer + to :ref:`advanced_generalization_ssr`. .. _structure_ssr: @@ -2352,25 +2321,23 @@ intermediate statement. The have tactic. ```````````````` -The main |SSR| forward reasoning tactic is the ``have`` tactic. It can -be use in two modes: one starts a new (sub)proof for an intermediate -result in the main proof, and the other provides explicitly a proof -term for this intermediate step. - -In the first mode, the syntax of have in its defective form is: - .. tacn:: have : @term :name: have -This tactic supports open syntax for :token:`term`. Applied to a goal ``G``, it -generates a first subgoal requiring a proof of ``term`` in the context of -``G``. The second generated subgoal is of the form ``term -> G``, where term -becomes the new top assumption, instead of being introduced with a -fresh name. At the proof-term level, the have tactic creates a β -redex, and introduces the lemma under a fresh name, automatically -chosen. + This is the main |SSR| forward reasoning tactic. It can + be used in two modes: one starts a new (sub)proof for an intermediate + result in the main proof, and the other provides explicitly a proof + term for this intermediate step. + + This tactic supports open syntax for :token:`term`. Applied to a goal ``G``, it + generates a first subgoal requiring a proof of :token:`term` in the context of + ``G``. The second generated subgoal is of the form :n:`term -> G`, where term + becomes the new top assumption, instead of being introduced with a + fresh name. At the proof-term level, the have tactic creates a β + redex, and introduces the lemma under a fresh name, automatically + chosen. -Like in the case of the ``pose`` tactic (see section :ref:`definitions_ssr`), the types of +Like in the case of the :n:`pose (ssreflect)` tactic (see section :ref:`definitions_ssr`), the types of the holes are abstracted in term. .. example:: @@ -2425,6 +2392,7 @@ The behavior of the defective have tactic makes it possible to generalize it in the following general construction: .. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @ssr_binder } } {? : @term } {? := @term | by @tactic } + :undocumented: Open syntax is supported for both :token:`term`. For the description of :token:`i_item` and :token:`s_item` see section @@ -2433,6 +2401,7 @@ have tactic, which opens a sub-proof for an intermediate result, uses tactics of the form: .. tacv:: have @clear_switch @i_item : @term by @tactic + :undocumented: which behave like: @@ -2446,7 +2415,7 @@ allows to reuse a name of the context, possibly used by the proof of the assumption, to introduce the new assumption itself. -The``by`` feature is especially convenient when the proof script of the +The ``by`` feature is especially convenient when the proof script of the statement is very short, basically when it fits in one line like in: .. coqtop:: in @@ -2503,13 +2472,13 @@ term for the intermediate lemma, using tactics of the form: .. tacv:: have {? @ident } := term -This tactic creates a new assumption of type the type of :token:`term`. -If the -optional :token:`ident` is present, this assumption is introduced under the -name :token:`ident`. Note that the body of the constant is lost for the user. + This tactic creates a new assumption of type the type of :token:`term`. + If the + optional :token:`ident` is present, this assumption is introduced under the + name :token:`ident`. Note that the body of the constant is lost for the user. -Again, non inferred implicit arguments and explicit holes are -abstracted. + Again, non inferred implicit arguments and explicit holes are + abstracted. .. example:: @@ -2781,9 +2750,9 @@ hypothesis and by pointing at the elements of the initial goals which should be generalized. The general syntax of without loss is: .. tacn:: wlog {? suff } {? @clear_switch } {? @i_item } : {* @ident } / @term - :name: wlog -.. tacv:: without loss {? suff } {? @clear_switch } {? @i_item } : {* @ident } / @term - :name: without loss + without loss {? suff } {? @clear_switch } {? @i_item } : {* @ident } / @term + :name: wlog; without loss + :undocumented: where each :token:`ident` is a constant in the context of the goal. Open syntax is supported for :token:`term`. @@ -2791,8 +2760,8 @@ of the goal. Open syntax is supported for :token:`term`. In its defective form: .. tacv:: wlog: / @term -.. tacv:: without loss: / @term - + without loss: / @term + :undocumented: on a goal G, it creates two subgoals: a first one to prove the formula (term -> G) -> G and a second one to prove the formula @@ -2873,6 +2842,7 @@ The complete syntax for the items on the left hand side of the ``/`` separator is the following one: .. tacv:: wlog … : {? @clear_switch | {? @ } @ident | ( {? @ } @ident := @c_pattern) } / @term + :undocumented: Clear operations are intertwined with generalization operations. This helps in particular avoiding dependency issues while generalizing some @@ -2957,8 +2927,9 @@ The general form of an |SSR| rewrite tactic is: .. tacn:: rewrite {+ @rstep } :name: rewrite (ssreflect) + :undocumented: -The combination of a rewrite tactic with the in tactical (see section +The combination of a rewrite tactic with the ``in`` tactical (see section :ref:`localization_ssr`) performs rewriting in both the context and the goal. A rewrite step :token:`rstep` has the general form: @@ -3692,14 +3663,12 @@ definition. rewrite /=. unlock lid. -We provide a special tactic unlock for unfolding such definitions -while removing “locks”, e.g., the tactic: - .. tacn:: unlock {? @occ_switch } @ident :name: unlock -replaces the occurrence(s) of :token:`ident` coded by the -:token:`occ_switch` with the corresponding body. + This tactic unfolds such definitions while removing “locks”, i.e. it + replaces the occurrence(s) of :token:`ident` coded by the + :token:`occ_switch` with the corresponding body. We found that it was usually preferable to prevent the expansion of some functions by the partial evaluation switch ``/=``, unless this @@ -3775,103 +3744,102 @@ which the function is supplied: .. tacn:: congr {? @num } @term :name: congr -This tactic: - + This tactic: + checks that the goal is a Leibniz equality; + matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints; + generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. -The goal can be a non dependent product ``P -> Q``. In that case, the -system asserts the equation ``P = Q``, uses it to solve the goal, and -calls the ``congr`` tactic on the remaining goal ``P = Q``. This can be useful -for instance to perform a transitivity step, like in the following -situation. + The goal can be a non dependent product ``P -> Q``. In that case, the + system asserts the equation ``P = Q``, uses it to solve the goal, and + calls the ``congr`` tactic on the remaining goal ``P = Q``. This can be useful + for instance to perform a transitivity step, like in the following + situation. -.. example:: + .. example:: - .. coqtop:: reset + .. coqtop:: reset - From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. - Section Test. + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + Section Test. - .. coqtop:: all + .. coqtop:: all - Lemma test (x y z : nat) (H : x = y) : x = z. - congr (_ = _) : H. - Abort. + Lemma test (x y z : nat) (H : x = y) : x = z. + congr (_ = _) : H. + Abort. - Lemma test (x y z : nat) : x = y -> x = z. - congr (_ = _). + Lemma test (x y z : nat) : x = y -> x = z. + congr (_ = _). -The optional :token:`num` forces the number of arguments for which the -tactic should generate equality proof obligations. + The optional :token:`num` forces the number of arguments for which the + tactic should generate equality proof obligations. -This tactic supports equalities between applications with dependent -arguments. Yet dependent arguments should have exactly the same -parameters on both sides, and these parameters should appear as first -arguments. + This tactic supports equalities between applications with dependent + arguments. Yet dependent arguments should have exactly the same + parameters on both sides, and these parameters should appear as first + arguments. -.. example:: + .. example:: - .. coqtop:: reset + .. coqtop:: reset - From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. - Section Test. + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + Section Test. - .. coqtop:: all + .. coqtop:: all - Definition f n := - if n is 0 then plus else mult. - Definition g (n m : nat) := plus. + Definition f n := + if n is 0 then plus else mult. + Definition g (n m : nat) := plus. - Lemma test x y : f 0 x y = g 1 1 x y. - congr plus. + Lemma test x y : f 0 x y = g 1 1 x y. + congr plus. - This script shows that the ``congr`` tactic matches ``plus`` - with ``f 0`` on the left hand side and ``g 1 1`` on the right hand - side, and solves the goal. + This script shows that the ``congr`` tactic matches ``plus`` + with ``f 0`` on the left hand side and ``g 1 1`` on the right hand + side, and solves the goal. -.. example:: + .. example:: - .. coqtop:: reset + .. coqtop:: reset - From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. - Section Test. + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + Section Test. - .. coqtop:: all + .. coqtop:: all - Lemma test n m (Hnm : m <= n) : S m + (S n - S m) = S n. - congr S; rewrite -/plus. + Lemma test n m (Hnm : m <= n) : S m + (S n - S m) = S n. + congr S; rewrite -/plus. - The tactic ``rewrite -/plus`` folds back the expansion of plus - which was necessary for matching both sides of the equality with - an application of ``S``. + The tactic ``rewrite -/plus`` folds back the expansion of plus + which was necessary for matching both sides of the equality with + an application of ``S``. -Like most |SSR| arguments, term can contain wildcards. + Like most |SSR| arguments, :token:`term` can contain wildcards. -.. example:: + .. example:: - .. coqtop:: reset + .. coqtop:: reset - From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. - Section Test. + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + Section Test. - .. coqtop:: all + .. coqtop:: all - Lemma test x y : x + (y * (y + x - x)) = x * 1 + (y + 0) * y. - congr ( _ + (_ * _)). + Lemma test x y : x + (y * (y + x - x)) = x * 1 + (y + 0) * y. + congr ( _ + (_ * _)). .. _contextual_patterns_ssr: @@ -4883,6 +4851,7 @@ Interpreting assumptions The general form of an assumption view tactic is: .. tacv:: [move | case] / @term + :undocumented: The term , called the *view lemma* can be: @@ -4997,6 +4966,7 @@ Interpreting goals A goal interpretation view tactic of the form: .. tacv:: apply/@term + :undocumented: applied to a goal ``top`` is interpreted in the following way: @@ -5027,6 +4997,7 @@ both sides. The syntax of double views is: .. tacv:: apply/@term/@term + :undocumented: The first term is the view lemma applied to the left hand side of the equality, while the second term is the one applied to the right hand side. @@ -5074,31 +5045,30 @@ In this context, the identity view can be used when no view has to be applied: Declaring new Hint Views ~~~~~~~~~~~~~~~~~~~~~~~~ -The database of hints for the view mechanism is extensible via a -dedicated vernacular command. As library ``ssrbool.v`` already declares a -corpus of hints, this feature is probably useful only for users who -define their own logical connectives. Users can declare their own -hints following the syntax used in ``ssrbool.v``: - .. cmd:: Hint View for move / @ident {? | @num } -.. cmd:: Hint View for apply / @ident {? | @num } + Hint View for apply / @ident {? | @num } + + This command can be used to extend the database of hints for the view + mechanism. -The :token:`ident` is the name of the lemma to be -declared as a hint. If `move` is used as -tactic, the hint is declared for assumption interpretation tactics, -`apply` declares hints for goal interpretations. Goal interpretation -view hints are declared for both simple views and left hand side -views. The optional natural number is the number of implicit -arguments to be considered for the declared hint view lemma. + As library ``ssrbool.v`` already declares a + corpus of hints, this feature is probably useful only for users who + define their own logical connectives. -The command: + The :token:`ident` is the name of the lemma to be + declared as a hint. If ``move`` is used as + tactic, the hint is declared for assumption interpretation tactics, + ``apply`` declares hints for goal interpretations. Goal interpretation + view hints are declared for both simple views and left hand side + views. The optional natural number is the number of implicit + arguments to be considered for the declared hint view lemma. -.. cmd:: Hint View for apply//@ident {? | @num } + .. cmdv:: Hint View for apply//@ident {? | @num } -with a double slash ``//``, declares hint views for right hand sides of -double views. + This variant with a double slash ``//``, declares hint views for right + hand sides of double views. -See the files ``ssreflect.v`` and ``ssrbool.v`` for examples. + See the files ``ssreflect.v`` and ``ssrbool.v`` for examples. Multiple views @@ -5157,73 +5127,66 @@ equivalences are indeed taken into account, otherwise only single |SSR| searching tool -------------------- -|SSR| proposes an extension of the Search command. Its syntax is: - .. cmd:: Search {? @pattern } {* {? - } %( @string %| @pattern %) {? % @ident} } {? in {+ {? - } @qualid } } :name: Search (ssreflect) -where :token:`qualid` is the name of an open module. This command returns -the list of lemmas: - + This is the |SSR| extension of the Search command. :token:`qualid` is the + name of an open module. This command returns the list of lemmas: + + + whose *conclusion* contains a subterm matching the optional first + pattern. A - reverses the test, producing the list of lemmas whose + conclusion does not contain any subterm matching the pattern; + + whose name contains the given string. A ``-`` prefix reverses the test, + producing the list of lemmas whose name does not contain the string. A + string that contains symbols or is followed by a scope key, is + interpreted as the constant whose notation involves that string (e.g., + :g:`+` for :g:`addn`), if this is unambiguous; otherwise the diagnostic + includes the output of the :cmd:`Locate` vernacular command. + + whose statement, including assumptions and types, contains a subterm + matching the next patterns. If a pattern is prefixed by ``-``, the test is + reversed; + + contained in the given list of modules, except the ones in the + modules prefixed by a ``-``. + +.. note:: + + + As for regular terms, patterns can feature scope indications. For + instance, the command: ``Search _ (_ + _)%N.`` lists all the lemmas whose + statement (conclusion or hypotheses) involves an application of the + binary operation denoted by the infix ``+`` symbol in the ``N`` scope (which is + |SSR| scope for natural numbers). + + Patterns with holes should be surrounded by parentheses. + + Search always volunteers the expansion of the notation, avoiding the + need to execute Locate independently. Moreover, a string fragment + looks for any notation that contains fragment as a substring. If the + ``ssrbool.v`` library is imported, the command: ``Search "~~".`` answers : -+ whose *conclusion* contains a subterm matching the optional first - pattern. A - reverses the test, producing the list of lemmas whose - conclusion does not contain any subterm matching the pattern; -+ whose name contains the given string. A ``-`` prefix reverses the test, - producing the list of lemmas whose name does not contain the string. A - string that contains symbols or is followed by a scope key, is - interpreted as the constant whose notation involves that string (e.g., - `+` for `addn`), if this is unambiguous; otherwise the diagnostic - includes the output of the ``Locate`` vernacular command. -+ whose statement, including assumptions and types, contains a subterm - matching the next patterns. If a pattern is prefixed by ``-``, the test is - reversed; -+ contained in the given list of modules, except the ones in the - modules prefixed by a ``-``. - - -Note that: - - -+ As for regular terms, patterns can feature scope indications. For - instance, the command: ``Search _ (_ + _)%N.`` lists all the lemmas whose - statement (conclusion or hypotheses) involves an application of the - binary operation denoted by the infix ``+`` symbol in the ``N`` scope (which is - |SSR| scope for natural numbers). -+ Patterns with holes should be surrounded by parentheses. -+ Search always volunteers the expansion of the notation, avoiding the - need to execute Locate independently. Moreover, a string fragment - looks for any notation that contains fragment as a substring. If the - ``ssrbool.v`` library is imported, the command: ``Search "~~".`` answers : - - .. example:: - - .. coqtop:: reset + .. coqtop:: reset - From Coq Require Import ssreflect ssrbool. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + From Coq Require Import ssreflect ssrbool. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. - .. coqtop:: all + .. coqtop:: all - Search "~~". + Search "~~". -+ A diagnostic is issued if there are different matching notations; it - is an error if all matches are partial. -+ Similarly, a diagnostic warns about multiple interpretations, and - signals an error if there is no default one. -+ The command ``Search in M.`` is a way of obtaining the complete - signature of the module ``M``. -+ Strings and pattern indications can be interleaved, but the first - indication has a special status if it is a pattern, and only filters - the conclusion of lemmas: + + A diagnostic is issued if there are different matching notations; it + is an error if all matches are partial. + + Similarly, a diagnostic warns about multiple interpretations, and + signals an error if there is no default one. + + The command ``Search in M.`` is a way of obtaining the complete + signature of the module ``M``. + + Strings and pattern indications can be interleaved, but the first + indication has a special status if it is a pattern, and only filters + the conclusion of lemmas: - + The command : ``Search (_ =1 _) "bij".`` lists all the lemmas whose - conclusion features a ``=1`` and whose name contains the string ``bij``. - + The command : ``Search "bij" (_ =1 _).`` lists all the lemmas whose - statement, including hypotheses, features a ``=1`` and whose name - contains the string ``bij``. + + The command : ``Search (_ =1 _) "bij".`` lists all the lemmas whose + conclusion features a ``=1`` and whose name contains the string ``bij``. + + The command : ``Search "bij" (_ =1 _).`` lists all the lemmas whose + statement, including hypotheses, features a ``=1`` and whose name + contains the string ``bij``. Synopsis and Index ------------------ @@ -5327,80 +5290,78 @@ respectively. .. tacn:: move -idtac or hnf see :ref:`bookkeeping_ssr` + :tacn:`idtac` or :tacn:`hnf` (see :ref:`bookkeeping_ssr`) .. tacn:: apply -.. tacn:: exact + exact -application see :ref:`the_defective_tactics_ssr` + application (see :ref:`the_defective_tactics_ssr`) .. tacn:: abstract - see :ref:`abstract_ssr` and :ref:`generating_let_ssr` + see :ref:`abstract_ssr` and :ref:`generating_let_ssr` .. tacn:: elim -induction see :ref:`the_defective_tactics_ssr` + induction (see :ref:`the_defective_tactics_ssr`) .. tacn:: case -case analysis see :ref:`the_defective_tactics_ssr` + case analysis (see :ref:`the_defective_tactics_ssr`) .. tacn:: rewrite {+ @r_step } -rewrite see :ref:`rewriting_ssr` + rewrite (see :ref:`rewriting_ssr`) .. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } {? : @term } := @term -.. tacv:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic } -.. tacn:: have suff {? @clear_switch } {? @i_pattern } {? : @term } := @term -.. tacv:: have suff {? @clear_switch } {? @i_pattern } : @term {? by @tactic } -.. tacv:: gen have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } -.. tacv:: generally have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } - :name: generally have - -forward chaining see :ref:`structure_ssr` + have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic } + have suff {? @clear_switch } {? @i_pattern } {? : @term } := @term + have suff {? @clear_switch } {? @i_pattern } : @term {? by @tactic } + gen have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } + generally have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } + :name: _; _; _; _; _; generally have + forward chaining (see :ref:`structure_ssr`) .. tacn:: wlog {? suff } {? @i_item } : {* @gen_item %| @clear_switch } / @term -specializing see :ref:`structure_ssr` + specializing (see :ref:`structure_ssr`) .. tacn:: suff {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic } - :name: suff -.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic } - :name: suffices -.. tacv:: suff {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } -.. tacv:: suffices {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } + suffices {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic } + suff {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } + suffices {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } + :name: suff; suffices; _; _ -backchaining see :ref:`structure_ssr` + backchaining (see :ref:`structure_ssr`) .. tacn:: pose @ident := @term -local definition :ref:`definitions_ssr` + local definition (see :ref:`definitions_ssr`) .. tacv:: pose @ident {+ @ssr_binder } := @term -local function definition + local function definition .. tacv:: pose fix @fix_body -local fix definition + local fix definition .. tacv:: pose cofix @fix_body -local cofix definition + local cofix definition .. tacn:: set @ident {? : @term } := {? @occ_switch } %( @term %| ( @c_pattern) %) -abbreviation see :ref:`abbreviations_ssr` + abbreviation (see :ref:`abbreviations_ssr`) .. tacn:: unlock {* {? @r_prefix } @ident } -unlock see :ref:`locking_ssr` + unlock (see :ref:`locking_ssr`) .. tacn:: congr {? @num } @term -congruence :ref:`congruence_ssr` + congruence (see :ref:`congruence_ssr`) Tacticals @@ -5439,15 +5400,15 @@ Commands .. cmd:: Hint View for %( move %| apply %) / @ident {? | @num } -view hint declaration see :ref:`declaring_new_hints_ssr` + view hint declaration (see :ref:`declaring_new_hints_ssr`) .. cmd:: Hint View for apply // @ident {? @num } -right hand side double , view hint declaration see :ref:`declaring_new_hints_ssr` + right hand side double , view hint declaration (see :ref:`declaring_new_hints_ssr`) .. cmd:: Prenex Implicits {+ @ident } -prenex implicits declaration see :ref:`parametric_polymorphism_ssr` + prenex implicits declaration (see :ref:`parametric_polymorphism_ssr`) Settings ~~~~~~~~ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index ad80cb62e1..59602581c7 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3425,7 +3425,9 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. cmdv:: Hint @hint_definition - No database name is given: the hint is registered in the core database. + No database name is given: the hint is registered in the ``core`` database. + + .. deprecated:: 8.10 .. cmdv:: Local Hint @hint_definition : {+ @ident} diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index a54da6faf2..47afa5ba0c 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -70,7 +70,7 @@ associativity rules have to be given. The right-hand side of a notation is interpreted at the time the notation is given. In particular, disambiguation of constants, :ref:`implicit arguments - <ImplicitArguments>`, :ref:`coercions <Coercions>`, etc. are resolved at the + <ImplicitArguments>` and other notations are resolved at the time of the declaration of the notation. Precedences and associativity diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index 57adcb287c..1de9890992 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -35,7 +35,7 @@ COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SY def coqdoc(coq_code, coqdoc_bin=None): """Get the output of coqdoc on coq_code.""" - coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN"), "coqdoc") + coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN", ""), "coqdoc") fd, filename = mkstemp(prefix="coqdoc-", suffix=".v") if platform.system().startswith("CYGWIN"): # coqdoc currently doesn't accept cygwin style paths in the form "/cygdrive/c/..." diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 2c69dcfe08..827b7c13c1 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -198,6 +198,25 @@ class CoqObject(ObjectDescription): self._add_index_entry(name, target) return target + def _prepare_names(self): + sigs = self.get_signatures() + names = self.options.get("name") + if names is None: + self._names = {} + else: + names = [n.strip() for n in names.split(";")] + if len(names) != len(sigs): + ERR = ("Expected {} semicolon-separated names, got {}. " + + "Please provide one name per signature line.") + raise self.error(ERR.format(len(names), len(sigs))) + self._names = dict(zip(sigs, names)) + + def run(self): + self._prepare_names() + return super().run() + +class DocumentableObject(CoqObject): + def _warn_if_undocumented(self): document = self.state.document config = document.settings.env.config @@ -212,30 +231,16 @@ class CoqObject(ObjectDescription): if report == "warning": raise self.warning(msg) - def _prepare_names(self): - sigs = self.get_signatures() - names = self.options.get("name") - if names is None: - self._names = {} - else: - names = [n.strip() for n in names.split(";")] - if len(names) != len(sigs): - ERR = ("Expected {} semicolon-separated names, got {}. " + - "Please provide one name per signature line.") - raise self.error(ERR.format(len(names), len(sigs))) - self._names = dict(zip(sigs, names)) - def run(self): self._warn_if_undocumented() - self._prepare_names() return super().run() -class PlainObject(CoqObject): +class PlainObject(DocumentableObject): """A base class for objects whose signatures should be rendered literally.""" def _render_signature(self, signature, signode): signode += addnodes.desc_name(signature, signature) -class NotationObject(CoqObject): +class NotationObject(DocumentableObject): """A base class for objects whose signatures should be rendered as nested boxes. Objects that inherit from this class can use the notation grammar (“{+ …}”, diff --git a/dune-project b/dune-project index 85238c70c5..f0ac11ba61 100644 --- a/dune-project +++ b/dune-project @@ -1,3 +1,2 @@ -(lang dune 1.4) - +(lang dune 1.6) (name coq) diff --git a/ide/idetop.ml b/ide/idetop.ml index 6a4c7603ee..716a942d5c 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -196,12 +196,24 @@ let process_goal sigma g = (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } -let export_pre_goals pgs = - { - Interface.fg_goals = pgs.Proof.fg_goals; - Interface.bg_goals = pgs.Proof.bg_goals; - Interface.shelved_goals = pgs.Proof.shelved_goals; - Interface.given_up_goals = pgs.Proof.given_up_goals +let process_goal_diffs diff_goal_map oldp nsigma ng = + let open Evd in + let og_s = match oldp with + | Some oldp -> + let Proof.{ sigma=osigma } = Proof.data oldp in + (try Some { it = Evar.Map.find ng diff_goal_map; sigma = osigma } + with Not_found -> None) + | None -> None + in + let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in + { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng } + +let export_pre_goals Proof.{ sigma; goals; stack; shelf; given_up } process = + let process = List.map (process sigma) in + { Interface.fg_goals = process goals + ; Interface.bg_goals = List.(map (fun (lg,rg) -> process lg, process rg)) stack + ; Interface.shelved_goals = process shelf + ; Interface.given_up_goals = process given_up } let goals () = @@ -212,22 +224,9 @@ let goals () = if Proof_diffs.show_diffs () then begin let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in let diff_goal_map = Proof_diffs.make_goal_map oldp newp in - - let process_goal_diffs nsigma ng = - let open Evd in - let og_s = match oldp with - | Some oldp -> - let (_,_,_,_,osigma) = Proof.proof oldp in - (try Some { it = Evar.Map.find ng diff_goal_map; sigma = osigma } - with Not_found -> None) (* will appear as a new goal *) - | None -> None - in - let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in - { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng } - in - Some (export_pre_goals (Proof.map_structured_proof newp process_goal_diffs)) + Some (export_pre_goals Proof.(data newp) (process_goal_diffs diff_goal_map oldp)) end else - Some (export_pre_goals (Proof.map_structured_proof newp process_goal)) + Some (export_pre_goals Proof.(data newp) process_goal) with Proof_global.NoCurrentProof -> None;; let evars () = @@ -235,7 +234,7 @@ let evars () = let doc = get_doc () in set_doc @@ Stm.finish ~doc; let pfts = Proof_global.give_me_the_proof () in - let all_goals, _, _, _, sigma = Proof.proof pfts in + let Proof.{ sigma } = Proof.data pfts in let exl = Evar.Map.bindings (Evd.undefined_map sigma) in let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in let el = List.map map_evar exl in @@ -245,8 +244,8 @@ let evars () = let hints () = try let pfts = Proof_global.give_me_the_proof () in - let all_goals, _, _, _, sigma = Proof.proof pfts in - match all_goals with + let Proof.{ goals; sigma } = Proof.data pfts in + match goals with | [] -> None | g :: _ -> let env = Goal.V82.env sigma g in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 40922b5c35..7aa85a0810 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1527,8 +1527,8 @@ let drop_notations_pattern looked_for genv = try match Nametab.locate_extended qid with | SynDef sp -> - let (vars,a) = Syntax_def.search_syntactic_definition sp in - (match a with + let filter (vars,a) = + try match a with | NRef g -> (* Convention: do not deactivate implicit arguments and scopes for further arguments *) test_kind top g; @@ -1549,7 +1549,9 @@ let drop_notations_pattern looked_for genv = let idspl1 = List.map (in_not false qid.loc scopes (subst, Id.Map.empty) []) args in let (_,argscs) = find_remaining_scopes pats1 pats2 g in Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2) - | _ -> raise Not_found) + | _ -> raise Not_found + with Not_found -> None in + Syntax_def.search_filtered_syntactic_definition filter sp | TrueGlobal g -> test_kind top g; Dumpglob.add_glob ?loc:qid.loc g; diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index b73d238c22..49273c4146 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -105,3 +105,10 @@ let search_syntactic_definition ?loc kn = let def = out_pat pat in verbose_compat ?loc kn def v; def + +let search_filtered_syntactic_definition ?loc filter kn = + let pat,v = KNmap.find kn !syntax_table in + let def = out_pat pat in + let res = filter def in + (match res with Some _ -> verbose_compat ?loc kn def v | None -> ()); + res diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index c5b6655ff8..77873f8f67 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -19,3 +19,6 @@ val declare_syntactic_definition : bool -> Id.t -> Flags.compat_version option -> syndef_interpretation -> unit val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation + +val search_filtered_syntactic_definition : ?loc:Loc.t -> + (syndef_interpretation -> 'a option) -> KerName.t -> 'a option diff --git a/kernel/univ.ml b/kernel/univ.ml index 93a91af1d7..d7c0cf13ec 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1034,6 +1034,8 @@ module ACumulativityInfo = struct type t = AUContext.t * Variance.t array + let repr (auctx,var) = AUContext.repr auctx, var + let pr prl (univs, variance) = AUContext.pr prl ~variance univs diff --git a/kernel/univ.mli b/kernel/univ.mli index 8327ff1644..d7097be570 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -400,6 +400,7 @@ module ACumulativityInfo : sig type t + val repr : t -> CumulativityInfo.t val univ_context : t -> AUContext.t val variance : t -> Variance.t array val leq_constraints : t -> Instance.t constraint_function diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index c1a673edf0..171d51800e 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -57,7 +57,6 @@ type assumption_object_kind = Definitional | Logical | Conjectural *) type assumption_kind = locality * polymorphic * assumption_object_kind - type definition_kind = locality * polymorphic * definition_object_kind (** Kinds used in proofs *) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index e626df5579..4bb52f599a 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -632,7 +632,8 @@ let solve_remaining_by env sigma holes by = | Some evi -> let env = Environ.reset_with_named_context evi.evar_hyps env in let ty = evi.evar_concl in - let c, sigma = Pfedit.refine_by_tactic env sigma ty solve_tac in + let name, poly = Id.of_string "rewrite", false in + let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma ty solve_tac in Evd.define evk (EConstr.of_constr c) sigma in List.fold_left solve sigma indep diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 284642b38c..816741b894 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2031,7 +2031,8 @@ let _ = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun = lfun; extra; } in let tac = interp_tactic ist tac in - let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in + let name, poly = Id.of_string "ltac_sub", false in + let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in (EConstr.of_constr c, sigma) in GlobEnv.register_constr_interp0 wit_tactic eval diff --git a/plugins/rtauto/g_rtauto.mlg b/plugins/rtauto/g_rtauto.mlg index 9c9fdcfa2f..d8724eb976 100644 --- a/plugins/rtauto/g_rtauto.mlg +++ b/plugins/rtauto/g_rtauto.mlg @@ -17,6 +17,6 @@ open Ltac_plugin DECLARE PLUGIN "rtauto_plugin" TACTIC EXTEND rtauto -| [ "rtauto" ] -> { Proofview.V82.tactic (Refl_tauto.rtauto_tac) } +| [ "rtauto" ] -> { Refl_tauto.rtauto_tac } END diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index f1fa694356..a6b6c57ff9 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -16,7 +16,6 @@ open CErrors open Util open Term open Constr -open Tacmach open Proof_search open Context.Named.Declaration @@ -60,12 +59,11 @@ let l_I_Or_r = gen_constant "plugins.rtauto.I_Or_r" let l_E_Or = gen_constant "plugins.rtauto.E_Or" let l_D_Or = gen_constant "plugins.rtauto.D_Or" +let special_whd env sigma c = + Reductionops.clos_whd_flags CClosure.all env sigma c -let special_whd gl c = - Reductionops.clos_whd_flags CClosure.all (pf_env gl) (Tacmach.project gl) c - -let special_nf gl c = - Reductionops.clos_norm_flags CClosure.betaiotazeta (pf_env gl) (Tacmach.project gl) c +let special_nf env sigma c = + Reductionops.clos_norm_flags CClosure.betaiotazeta env sigma c type atom_env= {mutable next:int; @@ -83,61 +81,58 @@ let make_atom atom_env term= atom_env.next<- i + 1; Atom i -let rec make_form atom_env gls term = +let rec make_form env sigma atom_env term = let open EConstr in let open Vars in - let normalize=special_nf gls in - let cciterm=special_whd gls term in - let sigma = Tacmach.project gls in - match EConstr.kind sigma cciterm with - Prod(_,a,b) -> - if noccurn sigma 1 b && - Retyping.get_sort_family_of - (pf_env gls) sigma a == InProp - then - let fa=make_form atom_env gls a in - let fb=make_form atom_env gls b in - Arrow (fa,fb) - else - make_atom atom_env (normalize term) - | Cast(a,_,_) -> - make_form atom_env gls a - | Ind (ind, _) -> - if Names.eq_ind ind (fst (Lazy.force li_False)) then - Bot - else - make_atom atom_env (normalize term) - | App(hd,argv) when Int.equal (Array.length argv) 2 -> - begin - try - let ind, _ = destInd sigma hd in - if Names.eq_ind ind (fst (Lazy.force li_and)) then - let fa=make_form atom_env gls argv.(0) in - let fb=make_form atom_env gls argv.(1) in - Conjunct (fa,fb) - else if Names.eq_ind ind (fst (Lazy.force li_or)) then - let fa=make_form atom_env gls argv.(0) in - let fb=make_form atom_env gls argv.(1) in - Disjunct (fa,fb) - else make_atom atom_env (normalize term) - with DestKO -> make_atom atom_env (normalize term) - end - | _ -> make_atom atom_env (normalize term) - -let rec make_hyps atom_env gls lenv = function + let normalize = special_nf env sigma in + let cciterm = special_whd env sigma term in + match EConstr.kind sigma cciterm with + Prod(_,a,b) -> + if noccurn sigma 1 b && + Retyping.get_sort_family_of env sigma a == InProp + then + let fa = make_form env sigma atom_env a in + let fb = make_form env sigma atom_env b in + Arrow (fa,fb) + else + make_atom atom_env (normalize term) + | Cast(a,_,_) -> + make_form env sigma atom_env a + | Ind (ind, _) -> + if Names.eq_ind ind (fst (Lazy.force li_False)) then + Bot + else + make_atom atom_env (normalize term) + | App(hd,argv) when Int.equal (Array.length argv) 2 -> + begin + try + let ind, _ = destInd sigma hd in + if Names.eq_ind ind (fst (Lazy.force li_and)) then + let fa = make_form env sigma atom_env argv.(0) in + let fb = make_form env sigma atom_env argv.(1) in + Conjunct (fa,fb) + else if Names.eq_ind ind (fst (Lazy.force li_or)) then + let fa = make_form env sigma atom_env argv.(0) in + let fb = make_form env sigma atom_env argv.(1) in + Disjunct (fa,fb) + else make_atom atom_env (normalize term) + with DestKO -> make_atom atom_env (normalize term) + end + | _ -> make_atom atom_env (normalize term) + +let rec make_hyps env sigma atom_env lenv = function [] -> [] | LocalDef (_,body,typ)::rest -> - make_hyps atom_env gls (typ::body::lenv) rest + make_hyps env sigma atom_env (typ::body::lenv) rest | LocalAssum (id,typ)::rest -> - let hrec= - make_hyps atom_env gls (typ::lenv) rest in - if List.exists (fun c -> Termops.local_occur_var Evd.empty (* FIXME *) id c) lenv || - (Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) typ != InProp) - then - hrec - else - (id,make_form atom_env gls typ)::hrec + let hrec= + make_hyps env sigma atom_env (typ::lenv) rest in + if List.exists (fun c -> Termops.local_occur_var Evd.empty (* FIXME *) id c) lenv || + (Retyping.get_sort_family_of env sigma typ != InProp) + then + hrec + else + (id,make_form env sigma atom_env typ)::hrec let rec build_pos n = if n<=1 then force node_count l_xH @@ -251,73 +246,76 @@ let () = declare_bool_option opt_check open Pp -let rtauto_tac gls= - Coqlib.check_required_library ["Coq";"rtauto";"Rtauto"]; - let gamma={next=1;env=[]} in - let gl=pf_concl gls in - let () = - if Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) gl != InProp - then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in - let glf=make_form gamma gls gl in - let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in - let formula= - List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in - let search_fun = match Tacinterp.get_debug() with - | Tactic_debug.DebugOn 0 -> Search.debug_depth_first - | _ -> Search.depth_first - in - let () = - begin - reset_info (); +let rtauto_tac = + Proofview.Goal.enter begin fun gl -> + let hyps = Proofview.Goal.hyps gl in + let concl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + Coqlib.check_required_library ["Coq";"rtauto";"Rtauto"]; + let gamma={next=1;env=[]} in + let () = + if Retyping.get_sort_family_of env sigma concl != InProp + then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in + let glf = make_form env sigma gamma concl in + let hyps = make_hyps env sigma gamma [concl] hyps in + let formula= + List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in + let search_fun = match Tacinterp.get_debug() with + | Tactic_debug.DebugOn 0 -> Search.debug_depth_first + | _ -> Search.depth_first + in + let () = + begin + reset_info (); + if !verbose then + Feedback.msg_info (str "Starting proof-search ..."); + end in + let search_start_time = System.get_time () in + let prf = + try project (search_fun (init_state [] formula)) + with Not_found -> + user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in + let search_end_time = System.get_time () in + let () = if !verbose then + begin + Feedback.msg_info (str "Proof tree found in " ++ + System.fmt_time_difference search_start_time search_end_time); + pp_info (); + Feedback.msg_info (str "Building proof term ... ") + end in + let build_start_time=System.get_time () in + let () = step_count := 0; node_count := 0 in + let main = mkApp (force node_count l_Reflect, + [|build_env gamma; + build_form formula; + build_proof [] 0 prf|]) in + let term= + applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in + let build_end_time=System.get_time () in + let () = if !verbose then + begin + Feedback.msg_info (str "Proof term built in " ++ + System.fmt_time_difference build_start_time build_end_time ++ + fnl () ++ + str "Proof size : " ++ int !step_count ++ + str " steps" ++ fnl () ++ + str "Proof term size : " ++ int (!step_count+ !node_count) ++ + str " nodes (constants)" ++ fnl () ++ + str "Giving proof term to Coq ... ") + end in + let tac_start_time = System.get_time () in + let term = EConstr.of_constr term in + let result= + if !check then + Tactics.exact_check term + else + Tactics.exact_no_check term in + let tac_end_time = System.get_time () in + let () = + if !check then Feedback.msg_info (str "Proof term type-checking is on"); if !verbose then - Feedback.msg_info (str "Starting proof-search ..."); - end in - let search_start_time = System.get_time () in - let prf = - try project (search_fun (init_state [] formula)) - with Not_found -> - user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in - let search_end_time = System.get_time () in - let () = if !verbose then - begin - Feedback.msg_info (str "Proof tree found in " ++ - System.fmt_time_difference search_start_time search_end_time); - pp_info (); - Feedback.msg_info (str "Building proof term ... ") - end in - let build_start_time=System.get_time () in - let () = step_count := 0; node_count := 0 in - let main = mkApp (force node_count l_Reflect, - [|build_env gamma; - build_form formula; - build_proof [] 0 prf|]) in - let term= - applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in - let build_end_time=System.get_time () in - let () = if !verbose then - begin - Feedback.msg_info (str "Proof term built in " ++ - System.fmt_time_difference build_start_time build_end_time ++ - fnl () ++ - str "Proof size : " ++ int !step_count ++ - str " steps" ++ fnl () ++ - str "Proof term size : " ++ int (!step_count+ !node_count) ++ - str " nodes (constants)" ++ fnl () ++ - str "Giving proof term to Coq ... ") - end in - let tac_start_time = System.get_time () in - let term = EConstr.of_constr term in - let result= - if !check then - Proofview.V82.of_tactic (Tactics.exact_check term) gls - else - Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in - let tac_end_time = System.get_time () in - let () = - if !check then Feedback.msg_info (str "Proof term type-checking is on"); - if !verbose then - Feedback.msg_info (str "Internal tactic executed in " ++ - System.fmt_time_difference tac_start_time tac_end_time) in + Feedback.msg_info (str "Internal tactic executed in " ++ + System.fmt_time_difference tac_start_time tac_end_time) in result - + end diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index a91dd666a6..49b5ee5ac7 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -14,14 +14,15 @@ type atom_env= {mutable next:int; mutable env:(Constr.t*int) list} -val make_form : atom_env -> - Goal.goal Evd.sigma -> EConstr.types -> Proof_search.form +val make_form + : Environ.env -> Evd.evar_map -> atom_env + -> EConstr.types -> Proof_search.form -val make_hyps : - atom_env -> - Goal.goal Evd.sigma -> - EConstr.types list -> - EConstr.named_context -> - (Names.Id.t * Proof_search.form) list +val make_hyps + : Environ.env -> Evd.evar_map + -> atom_env + -> EConstr.types list + -> EConstr.named_context + -> (Names.Id.t * Proof_search.form) list -val rtauto_tac : Tacmach.tactic +val rtauto_tac : unit Proofview.tactic diff --git a/printing/printer.ml b/printing/printer.ml index b80133b171..be0139da06 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -546,10 +546,10 @@ let rec pr_evars_int_hd pr sigma i = function (hov 0 (pr i evk evi)) ++ (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd pr sigma (i+1) rest) -let pr_evars_int sigma ~shelf ~givenup i evs = +let pr_evars_int sigma ~shelf ~given_up i evs = let pr_status i = if List.mem i shelf then str " (shelved)" - else if List.mem i givenup then str " (given up)" + else if List.mem i given_up then str " (given up)" else mt () in pr_evars_int_hd (fun i evk evi -> @@ -761,7 +761,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map if Evar.Map.is_empty exl then (str"No more subgoals." ++ print_dependent_evars None sigma seeds) else - let pei = pr_evars_int sigma ~shelf ~givenup:[] 1 exl in + let pei = pr_evars_int sigma ~shelf ~given_up:[] 1 exl in v 0 ((str "No more subgoals," ++ str " but there are non-instantiated existential variables:" ++ cut () ++ (hov 0 pei) @@ -789,7 +789,7 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof = straightforward, but seriously, [Proof.proof] should return [evar_info]-s instead. *) let p = proof in - let (goals , stack , shelf, given_up, sigma ) = Proof.proof p in + let Proof.{goals; stack; shelf; given_up; sigma} = Proof.data p in let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in let seeds = Proof.V82.top_evars p in begin match goals with @@ -821,7 +821,7 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof = let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in let os_map = match oproof with | Some op when diffs -> - let (_,_,_,_, osigma) = Proof.proof op in + let Proof.{sigma=osigma} = Proof.data op in let diff_goal_map = Proof_diffs.make_goal_map oproof proof in Some (osigma, diff_goal_map) | _ -> None @@ -834,8 +834,8 @@ let pr_open_subgoals ~proof = pr_open_subgoals_diff proof let pr_nth_open_subgoal ~proof n = - let gls,_,_,_,sigma = Proof.proof proof in - pr_subgoal n sigma gls + let Proof.{goals;sigma} = Proof.data proof in + pr_subgoal n sigma goals let pr_goal_by_id ~proof id = try diff --git a/printing/printer.mli b/printing/printer.mli index 357f30d1f4..fd4682a086 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -182,7 +182,7 @@ val pr_open_subgoals_diff : ?quiet:bool -> ?diffs:bool -> ?oproof:Proof.t -> Pr val pr_open_subgoals : proof:Proof.t -> Pp.t val pr_nth_open_subgoal : proof:Proof.t -> int -> Pp.t val pr_evar : evar_map -> (Evar.t * evar_info) -> Pp.t -val pr_evars_int : evar_map -> shelf:Goal.goal list -> givenup:Goal.goal list -> int -> evar_info Evar.Map.t -> Pp.t +val pr_evars_int : evar_map -> shelf:Goal.goal list -> given_up:Goal.goal list -> int -> evar_info Evar.Map.t -> Pp.t val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> Evar.Set.t -> Pp.t diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index a381266976..b280ce909b 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -553,7 +553,7 @@ open Goal.Set let db_goal_map op np ng_to_og = let pr_goals title prf = Printf.printf "%s: " title; - let (goals,_,_,_,sigma) = Proof.proof prf in + let Proof.{goals;sigma} = Proof.data prf in List.iter (fun g -> Printf.printf "%d -> %s " (Evar.repr g) (goal_to_evar g sigma)) goals; let gs = diff (Proof.all_goals prf) (List.fold_left (fun s g -> add g s) empty goals) in List.iter (fun g -> Printf.printf "%d " (Evar.repr g)) (elements gs); @@ -626,11 +626,11 @@ let make_goal_map_i op np = let nevar_to_oevar = match_goals (Some (to_constr op)) (to_constr np) in let oevar_to_og = ref StringMap.empty in - let (_,_,_,_,osigma) = Proof.proof op in + let Proof.{sigma=osigma} = Proof.data op in List.iter (fun og -> oevar_to_og := StringMap.add (goal_to_evar og osigma) og !oevar_to_og) (Goal.Set.elements rem_gs); - let (_,_,_,_,nsigma) = Proof.proof np in + let Proof.{sigma=nsigma} = Proof.data np in let get_og ng = let nevar = goal_to_evar ng nsigma in let oevar = StringMap.find nevar nevar_to_oevar in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index acf5510aa0..e2b7df19de 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -33,7 +33,7 @@ let () = CErrors.register_handler begin function end let get_nth_V82_goal p i = - let goals,_,_,_,sigma = Proof.proof p in + let Proof.{ sigma; goals } = Proof.data p in try { it = List.nth goals (i-1) ; sigma } with Failure _ -> raise NoSuchGoal @@ -120,7 +120,8 @@ let solve ?with_end_tac gi info_lvl tac pr = let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac) let instantiate_nth_evar_com n com = - Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p) + Proof_global.simple_with_current_proof (fun _ p -> + Proof.V82.instantiate_evar Global.(env ())n com p) (**********************************************************************) @@ -166,7 +167,7 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in cb, status, univs -let refine_by_tactic env sigma ty tac = +let refine_by_tactic ~name ~poly env sigma ty tac = (* Save the initial side-effects to restore them afterwards. We set the current set of side-effects to be empty so that we can retrieve the ones created during the tactic invocation easily. *) @@ -175,7 +176,7 @@ let refine_by_tactic env sigma ty tac = (* Save the existing goals *) let prev_future_goals = save_future_goals sigma in (* Start a proof *) - let prf = Proof.start sigma [env, ty] in + let prf = Proof.start ~name ~poly sigma [env, ty] in let (prf, _) = try Proof.run_tactic env tac prf with Logic_monad.TacticFailure e as src -> @@ -184,9 +185,9 @@ let refine_by_tactic env sigma ty tac = iraise (e, info) in (* Plug back the retrieved sigma *) - let (goals,stack,shelf,given_up,sigma) = Proof.proof prf in + let Proof.{ goals; stack; shelf; given_up; sigma; entry } = Proof.data prf in assert (stack = []); - let ans = match Proof.initial_goals prf with + let ans = match Proofview.initial_goals entry with | [c, _] -> c | _ -> assert false in diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 155221947a..5699320af5 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -81,8 +81,13 @@ val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic -> EConstr.types -> unit Proofview.tactic -> constr * bool * UState.t -val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic -> - constr * Evd.evar_map +val refine_by_tactic + : name:Id.t + -> poly:bool + -> env -> Evd.evar_map + -> EConstr.types + -> unit Proofview.tactic + -> constr * Evd.evar_map (** A variant of the above function that handles open terms as well. Caveat: all effects are purged in the returned term at the end, but other evars solved by side-effects are NOT purged, so that unexpected failures may diff --git a/proofs/proof.ml b/proofs/proof.ml index 6c13c4946a..1aeb24606b 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -105,22 +105,29 @@ let done_cond ?(loose_end=false) k = CondDone (loose_end,k) (* Subpart of the type of proofs. It contains the parts of the proof which are under control of the undo mechanism *) -type t = { - (* Current focused proofview *) - proofview: Proofview.proofview; - (* Entry for the proofview *) - entry : Proofview.entry; - (* History of the focusings, provides information on how - to unfocus the proof and the extra information stored while focusing. - The list is empty when the proof is fully unfocused. *) - focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list; - (* List of goals that have been shelved. *) - shelf : Goal.goal list; - (* List of goals that have been given up *) - given_up : Goal.goal list; - (* The initial universe context (for the statement) *) - initial_euctx : UState.t -} +type t = + { proofview: Proofview.proofview + (** Current focused proofview *) + ; entry : Proofview.entry + (** Entry for the proofview *) + ; focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list + (** History of the focusings, provides information on how to unfocus + the proof and the extra information stored while focusing. The + list is empty when the proof is fully unfocused. *) + ; shelf : Goal.goal list + (** List of goals that have been shelved. *) + ; given_up : Goal.goal list + (** List of goals that have been given up *) + ; initial_euctx : UState.t + (** The initial universe context (for the statement) *) + ; name : Names.Id.t + (** the name of the theorem whose proof is being constructed *) + ; poly : bool + (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *) + } + +let initial_goals pf = Proofview.initial_goals pf.entry +let initial_euctx pf = pf.initial_euctx (*** General proof functions ***) @@ -141,7 +148,7 @@ let proof p = (goals,stack,shelf,given_up,sigma) type 'a pre_goals = { - fg_goals : 'a list; + fg_goals : 'a list; (** List of the focussed goals *) bg_goals : ('a list * 'a list) list; (** Zipper representing the unfocussed background goals *) @@ -311,7 +318,7 @@ let end_of_stack = CondEndStack end_of_stack_kind let unfocused = is_last_focus end_of_stack_kind -let start sigma goals = +let start ~name ~poly sigma goals = let entry, proofview = Proofview.init sigma goals in let pr = { proofview; @@ -320,9 +327,13 @@ let start sigma goals = shelf = [] ; given_up = []; initial_euctx = - Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in + Evd.evar_universe_context (snd (Proofview.proofview proofview)) + ; name + ; poly + } in _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr -let dependent_start goals = + +let dependent_start ~name ~poly goals = let entry, proofview = Proofview.dependent_init goals in let pr = { proofview; @@ -331,7 +342,10 @@ let dependent_start goals = shelf = [] ; given_up = []; initial_euctx = - Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in + Evd.evar_universe_context (snd (Proofview.proofview proofview)) + ; name + ; poly + } in let number_of_goals = List.length (Proofview.initial_goals pr.entry) in _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr @@ -375,9 +389,6 @@ let return ?pid (p : t) = let p = unfocus end_of_stack_kind p () in Proofview.return p.proofview -let initial_goals p = Proofview.initial_goals p.entry -let initial_euctx p = p.initial_euctx - let compact p = let entry, proofview = Proofview.compact p.entry p.proofview in { p with proofview; entry } @@ -468,7 +479,7 @@ module V82 = struct { p with proofview = Proofview.V82.grab p.proofview } (* Main component of vernac command Existential *) - let instantiate_evar n com pr = + let instantiate_evar env n com pr = let tac = Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma -> let (evk, evi) = @@ -487,7 +498,7 @@ module V82 = struct let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in Proofview.Unsafe.tclEVARS sigma end in - let ((), proofview, _, _) = Proofview.apply (Global.env ()) tac pr.proofview in + let ((), proofview, _, _) = Proofview.apply env tac pr.proofview in let shelf = List.filter begin fun g -> Evd.is_undefined (Proofview.return proofview) g @@ -507,3 +518,37 @@ let all_goals p = let set = add given_up set in let { Evd.it = bgoals ; sigma = bsigma } = V82.background_subgoals p in add bgoals set + +type data = + { sigma : Evd.evar_map + (** A representation of the evar_map [EJGA wouldn't it better to just return the proofview?] *) + ; goals : Evar.t list + (** Focused goals *) + ; entry : Proofview.entry + (** Entry for the proofview *) + ; stack : (Evar.t list * Evar.t list) list + (** A representation of the focus stack *) + ; shelf : Evar.t list + (** A representation of the shelf *) + ; given_up : Evar.t list + (** A representation of the given up goals *) + ; initial_euctx : UState.t + (** The initial universe context (for the statement) *) + ; name : Names.Id.t + (** The name of the theorem whose proof is being constructed *) + ; poly : bool + (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *) + } + +let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name; poly } = + let goals, sigma = Proofview.proofview proofview in + (* spiwack: beware, the bottom of the stack is used by [Proof] + internally, and should not be exposed. *) + let rec map_minus_one f = function + | [] -> assert false + | [_] -> [] + | a::l -> f a :: (map_minus_one f l) + in + let stack = + map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in + { sigma; goals; entry; stack; shelf; given_up; initial_euctx; name; poly } diff --git a/proofs/proof.mli b/proofs/proof.mli index aaabea3454..fd5e905a3b 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -50,27 +50,70 @@ val proof : t -> * Goal.goal list * Goal.goal list * Evd.evar_map +[@@ocaml.deprecated "use [Proof.data]"] + +val initial_goals : t -> (EConstr.constr * EConstr.types) list +[@@ocaml.deprecated "use [Proof.data]"] + +val initial_euctx : t -> UState.t +[@@ocaml.deprecated "use [Proof.data]"] + +type data = + { sigma : Evd.evar_map + (** A representation of the evar_map [EJGA wouldn't it better to just return the proofview?] *) + ; goals : Evar.t list + (** Focused goals *) + ; entry : Proofview.entry + (** Entry for the proofview *) + ; stack : (Evar.t list * Evar.t list) list + (** A representation of the focus stack *) + ; shelf : Evar.t list + (** A representation of the shelf *) + ; given_up : Evar.t list + (** A representation of the given up goals *) + ; initial_euctx : UState.t + (** The initial universe context (for the statement) *) + ; name : Names.Id.t + (** The name of the theorem whose proof is being constructed *) + ; poly : bool; + (** polymorphism *) + } + +val data : t -> data (* Generic records structured like the return type of proof *) type 'a pre_goals = { fg_goals : 'a list; + [@ocaml.deprecated "use [Proof.data]"] (** List of the focussed goals *) bg_goals : ('a list * 'a list) list; + [@ocaml.deprecated "use [Proof.data]"] (** Zipper representing the unfocussed background goals *) shelved_goals : 'a list; + [@ocaml.deprecated "use [Proof.data]"] (** List of the goals on the shelf. *) given_up_goals : 'a list; + [@ocaml.deprecated "use [Proof.data]"] (** List of the goals that have been given up *) } +[@@ocaml.deprecated "use [Proof.data]"] -val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) - +(* needed in OCaml 4.05.0, not needed in newer ones *) +[@@@ocaml.warning "-3"] +val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) [@ocaml.warning "-3"] +[@@ocaml.deprecated "use [Proof.data]"] +[@@@ocaml.warning "+3"] (*** General proof functions ***) -val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> t -val dependent_start : Proofview.telescope -> t -val initial_goals : t -> (EConstr.constr * EConstr.types) list -val initial_euctx : t -> UState.t +val start + : name:Names.Id.t + -> poly:bool + -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t + +val dependent_start + : name:Names.Id.t + -> poly:bool + -> Proofview.telescope -> t (* Returns [true] if the considered proof is completed, that is if no goal remain to be considered (this does not require that all evars have been solved). *) @@ -177,8 +220,9 @@ val no_focused_goal : t -> bool (* the returned boolean signal whether an unsafe tactic has been used. In which case it is [false]. *) -val run_tactic : Environ.env -> - unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) +val run_tactic + : Environ.env + -> unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) val maximal_unfocus : 'a focus_kind -> t -> t @@ -208,7 +252,8 @@ module V82 : sig val grab_evars : t -> t (* Implements the Existential command *) - val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t + val instantiate_evar : + Environ.env -> int -> Constrexpr.constr_expr -> t -> t end (* returns the set of all goals in the proof *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 898fbe50f6..8077da8807 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -90,14 +90,13 @@ type proof_terminator = proof_ending -> unit type closed_proof = proof_object * proof_terminator type pstate = { - pid : Id.t; (* the name of the theorem whose proof is being constructed *) terminator : proof_terminator CEphemeron.key; endline_tactic : Genarg.glob_generic_argument option; section_vars : Constr.named_context option; proof : Proof.t; - strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; universe_decl: UState.universe_decl; + strength : Decl_kinds.goal_kind; } type t = pstate list @@ -142,7 +141,7 @@ end (*** Proof Global manipulation ***) let get_all_proof_names () = - List.map (function { pid = id } -> id) !pstates + List.map Proof.(function pf -> (data pf.proof).name) !pstates let cur_pstate () = match !pstates with @@ -151,7 +150,7 @@ let cur_pstate () = let give_me_the_proof () = (cur_pstate ()).proof let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None -let get_current_proof_name () = (cur_pstate ()).pid +let get_current_proof_name () = (Proof.data (cur_pstate ()).proof).Proof.name let with_current_proof f = match !pstates with @@ -205,8 +204,12 @@ let check_no_pending_proof () = str"Use \"Abort All\" first or complete proof(s).") end +let pf_name_eq id ps = + let Proof.{ name } = Proof.data ps.proof in + Id.equal name id + let discard_gen id = - pstates := List.filter (fun { pid = id' } -> not (Id.equal id id')) !pstates + pstates := List.filter (fun pf -> not (pf_name_eq id pf)) !pstates let discard {CAst.loc;v=id} = let n = List.length !pstates in @@ -223,9 +226,9 @@ let discard_all () = pstates := [] (* [set_proof_mode] sets the proof mode to be used after it's called. It is typically called by the Proof Mode command. *) let set_proof_mode m id = - pstates := - List.map (function { pid = id' } as p -> - if Id.equal id' id then { p with mode = m } else p) !pstates; + pstates := List.map + (fun ps -> if pf_name_eq id ps then { ps with mode = m } else ps) + !pstates; update_proof_mode () let set_proof_mode mn = @@ -244,28 +247,26 @@ let disactivate_current_proof_mode () = end of the proof to close the proof. The proof is started in the evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) -let start_proof sigma id ?(pl=UState.default_univ_decl) str goals terminator = +let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator = let initial_state = { - pid = id; terminator = CEphemeron.create terminator; - proof = Proof.start sigma goals; + proof = Proof.start ~name ~poly:(pi2 kind) sigma goals; endline_tactic = None; section_vars = None; - strength = str; mode = find_proof_mode "No"; - universe_decl = pl } in + universe_decl = pl; + strength = kind } in push initial_state pstates -let start_dependent_proof id ?(pl=UState.default_univ_decl) str goals terminator = +let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator = let initial_state = { - pid = id; terminator = CEphemeron.create terminator; - proof = Proof.dependent_start goals; + proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals; endline_tactic = None; section_vars = None; - strength = str; mode = find_proof_mode "No"; - universe_decl = pl } in + universe_decl = pl; + strength = kind } in push initial_state pstates let get_used_variables () = (cur_pstate ()).section_vars @@ -301,10 +302,10 @@ let set_used_variables l = ctx, [] let get_open_goals () = - let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in - List.length gl + + let Proof.{ goals; stack; shelf } = Proof.data (cur_pstate ()).proof in + List.length goals + List.fold_left (+) 0 - (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + + (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + List.length shelf type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t @@ -323,12 +324,9 @@ let private_poly_univs = let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now (fpl : closed_proof_output Future.computation) = - let { pid; section_vars; strength; proof; terminator; universe_decl } = - cur_pstate () in + let { section_vars; proof; terminator; universe_decl; strength } = cur_pstate () in + let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in let opaque = match opaque with Opaque -> true | Transparent -> false in - let poly = pi2 strength (* Polymorphic *) in - let initial_goals = Proof.initial_goals proof in - let initial_euctx = Proof.initial_euctx proof in let constrain_variables ctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx in @@ -411,16 +409,16 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now const_entry_opaque = opaque; const_entry_universes = univs; } in - let entries = Future.map2 entry_fn fpl initial_goals in - { id = pid; entries = entries; persistence = strength; + let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in + { id = name; entries = entries; persistence = strength; universes }, fun pr_ending -> CEphemeron.get terminator pr_ending let return_proof ?(allow_partial=false) () = - let { pid; proof; strength = (_,poly,_) } = cur_pstate () in + let { proof } = cur_pstate () in if allow_partial then begin let proofs = Proof.partial_proof proof in - let _,_,_,_, evd = Proof.proof proof in + let Proof.{sigma=evd} = Proof.data proof in let eff = Evd.eval_side_effects evd in (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects @@ -428,7 +426,8 @@ let return_proof ?(allow_partial=false) () = let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in proofs, Evd.evar_universe_context evd end else - let initial_goals = Proof.initial_goals proof in + let Proof.{name=pid;entry} = Proof.data proof in + let initial_goals = Proofview.initial_goals entry in let evd = Proof.return ~pid proof in let eff = Evd.eval_side_effects evd in let evd = Evd.minimize_universes evd in @@ -455,10 +454,11 @@ let set_terminator hook = module V82 = struct let get_current_initial_conclusions () = - let { pid; strength; proof } = cur_pstate () in - let initial = Proof.initial_goals proof in + let { proof; strength } = cur_pstate () in + let Proof.{ name; entry } = Proof.data proof in + let initial = Proofview.initial_goals entry in let goals = List.map (fun (o, c) -> c) initial in - pid, (goals, strength) + name, (goals, strength) end let freeze ~marshallable = @@ -470,7 +470,7 @@ let copy_terminators ~src ~tgt = assert(List.length src = List.length tgt); List.map2 (fun op p -> { p with terminator = op.terminator }) src tgt -let update_global_env () = +let update_global_env pf_info = with_current_proof (fun _ p -> Proof.in_proof p (fun sigma -> let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index b8af2bcd56..230a3207a8 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -49,12 +49,12 @@ let is_focused_goal_simple ~doc id = match state_of_id ~doc id with | `Expired | `Error _ | `Valid None -> `Not | `Valid (Some { Vernacstate.proof }) -> - let proof = Proof_global.proof_of_state proof in - let focused, r1, r2, r3, sigma = Proof.proof proof in - let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in - if List.for_all (fun x -> simple_goal sigma x rest) focused - then `Simple focused - else `Not + let proof = Proof_global.proof_of_state proof in + let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in + let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in + if List.for_all (fun x -> simple_goal sigma x rest) focused + then `Simple focused + else `Not type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ] diff --git a/stm/stm.ml b/stm/stm.ml index 28efb88237..ffd13fcb73 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1939,7 +1939,7 @@ end = struct (* {{{ *) try Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:false id; stm_purify (fun () -> - let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in + let Proof.{sigma=sigma0} = Proof.data (Proof_global.give_me_the_proof ()) in let g = Evd.find sigma0 r_goal in let is_ground c = Evarutil.is_ground_term sigma0 c in if not ( @@ -1960,7 +1960,7 @@ end = struct (* {{{ *) *) let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp r_state_fb st ast); - let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in + let Proof.{sigma} = Proof.data (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> RespNoProgress | Evd.Evar_defined t -> @@ -2002,7 +2002,7 @@ end = struct (* {{{ *) (if time then System.with_time ~batch else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> Proof_global.with_current_proof (fun _ p -> - let goals, _, _, _, _ = Proof.proof p in + let Proof.{goals} = Proof.data p in let open TacTask in let res = CList.map_i (fun i g -> let f, assign = diff --git a/tactics/auto.ml b/tactics/auto.ml index c030c77d4d..f5c3619e64 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -211,30 +211,26 @@ let tclLOG (dbg,_,depth,trace) pp tac = match dbg with | Off -> tac | Debug -> - (* For "debug (trivial/auto)", we directly output messages *) + (* For "debug (trivial/auto)", we directly output messages *) let s = String.make (depth+1) '*' in - Proofview.V82.tactic begin fun gl -> - try - let out = Proofview.V82.of_tactic tac gl in - Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)"); - out - with reraise -> - let reraise = CErrors.push reraise in - Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)"); - iraise reraise - end + Proofview.(tclIFCATCH ( + tac >>= fun v -> + Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)"); + tclUNIT v + ) Proofview.tclUNIT + (fun (exn, info) -> + Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)"); + tclZERO ~info exn)) | Info -> (* For "info (trivial/auto)", we store a log trace *) - Proofview.V82.tactic begin fun gl -> - try - let out = Proofview.V82.of_tactic tac gl in - trace := (depth, Some pp) :: !trace; - out - with reraise -> - let reraise = CErrors.push reraise in - trace := (depth, None) :: !trace; - iraise reraise - end + Proofview.(tclIFCATCH ( + tac >>= fun v -> + trace := (depth, Some pp) :: !trace; + tclUNIT v + ) Proofview.tclUNIT + (fun (exn, info) -> + trace := (depth, None) :: !trace; + tclZERO ~info exn)) (** For info, from the linear trace information, we reconstitute the part of the proof tree we're interested in. The last executed tactic diff --git a/tactics/hints.ml b/tactics/hints.ml index faff116af4..571ad9d160 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1516,8 +1516,8 @@ let pr_hint_term env sigma cl = let pr_applicable_hint () = let env = Global.env () in let pts = Proof_global.give_me_the_proof () in - let glss,_,_,_,sigma = Proof.proof pts in - match glss with + let Proof.{goals;sigma} = Proof.data pts in + match goals with | [] -> CErrors.user_err Pp.(str "No focused goal.") | g::_ -> pr_hint_term env sigma (Goal.V82.concl sigma g) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index caf4c1eca3..356b43ec14 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -183,7 +183,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = scheme on sort [sort]. Depending on the value of [dep_option] it will build a dependent lemma or a non-dependent one *) -let inversion_scheme env sigma t sort dep_option inv_op = +let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = let (env,i) = add_prods_sign env sigma t in let ind = try find_rectype env sigma i @@ -201,7 +201,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = user_err ~hdr:"lemma_inversion" (str"Computed inversion goal was not closed in initial signature."); *) - let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in + let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in let pf = fst (Proof.run_tactic env ( tclTHEN intro (onLastHypId inv_op)) pf) @@ -217,7 +217,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = invEnv ~init:Context.Named.empty end in let avoid = ref Id.Set.empty in - let _,_,_,_,sigma = Proof.proof pf in + let Proof.{sigma} = Proof.data pf in let sigma = Evd.minimize_universes sigma in let rec fill_holes c = match EConstr.kind sigma c with @@ -236,7 +236,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = p, sigma let add_inversion_lemma ~poly name env sigma t sort dep inv_op = - let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in + let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in let univs = Evd.const_univ_entry ~poly sigma in diff --git a/test-suite/bugs/closed/bug_4509.v b/test-suite/bugs/closed/bug_4509.v new file mode 100644 index 0000000000..ceae7c5fc3 --- /dev/null +++ b/test-suite/bugs/closed/bug_4509.v @@ -0,0 +1,11 @@ +(* Was solved at some time, suspectingly in PR #6328 *) + +Goal exists n, n > 1. +Proof. + unshelve eexists. (*2 goals, as expected*) + Undo. + unshelve (eexists; instantiate (1:=ltac:(idtac))). (*only 1 goal*) + shelve. + Undo. + 2:unshelve instantiate (1:=_). +Abort. diff --git a/test-suite/bugs/closed/bug_6202.v b/test-suite/bugs/closed/bug_6202.v new file mode 100644 index 0000000000..899260f59a --- /dev/null +++ b/test-suite/bugs/closed/bug_6202.v @@ -0,0 +1,11 @@ +(* This was fixed at some time, suspectingly in PR #6328 *) + +Inductive foo := F (a : forall var : Type -> Type, unit -> var unit) (_ : a = a). +Goal foo. + eexists (fun var => fun u : unit => ltac:(clear u)). + shelve. + Unshelve. + all:[ > | ]. + shelve. + Fail Grab Existential Variables. +Abort. diff --git a/test-suite/bugs/closed/bug_9166.v b/test-suite/bugs/closed/bug_9166.v new file mode 100644 index 0000000000..8a7e9c37b0 --- /dev/null +++ b/test-suite/bugs/closed/bug_9166.v @@ -0,0 +1,9 @@ +Set Warnings "+deprecated". + +Notation bar := option (compat "8.7"). + +Definition foo (x: nat) : nat := + match x with + | 0 => 0 + | S bar => bar + end. diff --git a/test-suite/coqchk/inductive_functor_params.v b/test-suite/coqchk/inductive_functor_params.v new file mode 100644 index 0000000000..f364a62818 --- /dev/null +++ b/test-suite/coqchk/inductive_functor_params.v @@ -0,0 +1,16 @@ + +Module Type T. + Parameter foo : nat -> nat. +End T. + +Module F (A:T). + Inductive ind (n:nat) : nat -> Prop := + | C : (forall x, x < n -> ind (A.foo n) x) -> ind n n. +End F. + +Module A. Definition foo (n:nat) := n. End A. + +Module M := F A. +(* Note: M.ind could be seen as having 1 recursively uniform + parameter, but module substitution does not recognize it, so it is + treated as a non-uniform parameter. *) diff --git a/test-suite/coqchk/inductive_functor_template.v b/test-suite/coqchk/inductive_functor_template.v new file mode 100644 index 0000000000..bc5cd0fb68 --- /dev/null +++ b/test-suite/coqchk/inductive_functor_template.v @@ -0,0 +1,11 @@ + +Module Type E. Parameter T : Type. End E. + +Module F (X:E). + #[universes(template)] Inductive foo := box : X.T -> foo. +End F. + +Module ME. Definition T := nat. End ME. +Module A := F ME. +(* Note: A.foo could live in Set, and coqchk sees that (because of + template polymorphism implementation details) *) diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index 97df40f882..844f96aaa1 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -51,7 +51,7 @@ Arguments pi _ _%F _%B. Check (forall w : r, pi w $ $ = tt). Fail Check (forall w : r, w $ $ = tt). Axiom w : r. -Arguments w _%F _%B : extra scopes. +Arguments w x%F y%B : extra scopes. Check (w $ $ = tt). Fail Arguments w _%F _%B. diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 5cf2157044..e58b9ccac7 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -323,7 +323,8 @@ let loop_flush_all () = let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2 let evleq e1 e2 = CList.equal Evar.equal e1 e2 let cproof p1 p2 = - let (a1,a2,a3,a4,_),(b1,b2,b3,b4,_) = Proof.proof p1, Proof.proof p2 in + let Proof.{goals=a1;stack=a2;shelf=a3;given_up=a4} = Proof.data p1 in + let Proof.{goals=b1;stack=b2;shelf=b3;given_up=b4} = Proof.data p2 in evleq a1 b1 && CList.equal (pequal evleq evleq) a2 b2 && CList.equal Evar.equal a3 b3 && diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 1a6eda446c..8f155adb8a 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -483,7 +483,7 @@ let save_proof ?proof = function let pftree = Proof_global.give_me_the_proof () in let id, k, typ = Pfedit.current_proof_statement () in let typ = EConstr.Unsafe.to_constr typ in - let universes = Proof.initial_euctx pftree in + let universes = Proof.((data pftree).initial_euctx) in (* This will warn if the proof is complete *) let pproofs, _univs = Proof_global.return_proof ~allow_partial:true () in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 838b1443b6..e6e3db4beb 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -82,12 +82,12 @@ let show_proof () = let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) let pfts = Proof_global.give_me_the_proof () in - let gls,_,shelf,givenup,sigma = Proof.proof pfts in - pr_evars_int sigma ~shelf ~givenup 1 (Evd.undefined_map sigma) + let Proof.{goals;shelf;given_up;sigma} = Proof.data pfts in + pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma) let show_universes () = let pfts = Proof_global.give_me_the_proof () in - let gls,_,_,_,sigma = Proof.proof pfts in + let Proof.{goals;sigma} = Proof.data pfts in let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++ str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx @@ -96,9 +96,9 @@ let show_universes () = let show_intro all = let open EConstr in let pf = Proof_global.give_me_the_proof() in - let gls,_,_,_,sigma = Proof.proof pf in - if not (List.is_empty gls) then begin - let gl = {Evd.it=List.hd gls ; sigma = sigma; } in + let Proof.{goals;sigma} = Proof.data pf in + if not (List.is_empty goals) then begin + let gl = {Evd.it=List.hd goals ; sigma = sigma; } in let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in if all then let lid = Tactics.find_intro_names l gl in @@ -1047,8 +1047,9 @@ let vernac_set_end_tac tac = let vernac_set_used_variables e = let env = Global.env () in + let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in let tys = - List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in + List.map snd (initial_goals (Proof_global.give_me_the_proof ())) in let tys = List.map EConstr.Unsafe.to_constr tys in let l = Proof_using.process_expr env e tys in let vars = Environ.named_context env in @@ -1221,11 +1222,9 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red let rec check_extra_args extra_args = match extra_args with | [] -> () - | { notation_scope = None } :: _ -> err_extra_args (names_of extra_args) - | { name = Anonymous; notation_scope = Some _ } :: args -> - check_extra_args args - | _ -> - user_err Pp.(str "Extra notation scopes can be set on anonymous and explicit arguments only.") + | { notation_scope = None } :: _ -> + user_err Pp.(str"Extra arguments should specify a scope.") + | { notation_scope = Some _ } :: args -> check_extra_args args in let args, scopes = @@ -1817,8 +1816,8 @@ let vernac_global_check c = let get_nth_goal n = let pf = Proof_global.give_me_the_proof() in - let gls,_,_,_,sigma = Proof.proof pf in - let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in + let Proof.{goals;sigma} = Proof.data pf in + let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in gl exception NoHyp |