diff options
| -rw-r--r-- | CHANGES.md | 62 | ||||
| -rw-r--r-- | dev/ci/user-overlays/08889-mattam-program-obl-subst.sh | 6 | ||||
| -rw-r--r-- | vernac/classes.ml | 2 | ||||
| -rw-r--r-- | vernac/comDefinition.ml | 2 | ||||
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 4 | ||||
| -rw-r--r-- | vernac/obligations.ml | 70 | ||||
| -rw-r--r-- | vernac/obligations.mli | 4 |
7 files changed, 86 insertions, 64 deletions
diff --git a/CHANGES.md b/CHANGES.md index faf11b9a9e..91763ba35c 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -6,6 +6,25 @@ OCaml - Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the INSTALL file for more information on dependencies. +Specification language, type inference + +- Fixing a missing check in interpreting instances of existential + variables that are bound to local definitions might exceptionally + induce an overhead if the cost of checking the conversion of the + corresponding definitions is additionally high (PR #8215). + +- A few improvements in inference of the return clause of `match` can + exceptionally introduce incompatibilities (PR #262). This can be + solved by writing an explicit `return` clause, sometimes even simply + an explicit `return _` clause. + +Notations + +- New command `Declare Scope` to explicitly declare a scope name + before any use of it. Implicit declaration of a scope at the time of + `Bind Scope`, `Delimit Scope`, `Undelimit Scope`, or `Notation` is + deprecated. + Plugins - The quote plugin (https://coq.inria.fr/distrib/V8.8.1/refman/proof-engine/detailed-tactic-examples.html#quote) @@ -24,6 +43,15 @@ Tactics Simplex-based proof engine. In case of regression, 'Unset Simplex' to get the venerable Fourier-based engine. +- Names of existential variables occurring in Ltac functions + (e.g. `?[n]` or `?n` in terms - not in patterns) are now interpreted + the same way as other variable names occurring in Ltac functions. + +Vernacular commands + +- `Combined Scheme` can now work when inductive schemes are generated in sort + `Type`. It used to be limited to sort `Prop`. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: @@ -44,6 +72,12 @@ Standard Library the upper bound of number represented by a vector. Allowed implicit vector length argument in `Ndigits.Bv2N`. +- Added `Bvector.BVeq` that decides whether two `Bvector`s are equal. + +- Added notations for `BVxor`, `BVand`, `BVor`, `BVeq` and `BVneg`. + +- Added `ByteVector` type that can convert to and from [string]. + Changes from 8.8.2 to 8.9+beta1 =============================== @@ -56,11 +90,6 @@ Notations - New support for autonomous grammars of terms, called "custom entries" (see chapter "Syntax extensions" of the reference manual). -- New command `Declare Scope` to explicitly declare a scope name - before any use of it. Implicit declaration of a scope at the time of - `Bind Scope`, `Delimit Scope`, `Undelimit Scope`, or `Notation` is - deprecated. - - Deprecated compatibility notations will actually be removed in the next version of Coq. Uses of these notations are generally easy to fix thanks to the hint contained in the deprecation warnings. For @@ -113,32 +142,18 @@ Tactics - The `romega` tactics have been deprecated; please use `lia` instead. -- Names of existential variables occurring in Ltac functions - (e.g. `?[n]` or `?n` in terms - not in patterns) are now interpreted - the same way as other variable names occurring in Ltac functions. - Focusing - Focusing bracket `{` now supports named goal selectors, e.g. `[x]: {` will focus on a goal (existential variable) named `x`. As usual, unfocus with `}` once the sub-goal is fully solved. -Specification language, type inference +Specification language - A fix to unification (which was sensitive to the ascii name of variables) may occasionally change type inference in incompatible ways, especially regarding the inference of the return clause of `match`. -- Fixing a missing check in interpreting instances of existential - variables that are bound to local definitions might exceptionally - induce an overhead if the cost of checking the conversion of the - corresponding definitions is additionally high (PR #8215). - -- A few improvements in inference of the return clause of `match` can - exceptionally introduce incompatibilities (PR #262). This can be - solved by writing an explicit `return` clause, sometimes even simply - an explicit `return _` clause. - Standard Library - Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them, @@ -178,9 +193,6 @@ Standard Library impacts users running Coq without the init library (`-nois` or `-noinit`) and also issuing `Require Import Coq.Init.Datatypes`. -- Added `Bvector.BVeq` that decides whether two `Bvector`s are equal. -- Added notations for `BVxor`, `BVand`, `BVor`, `BVeq` and `BVneg`. - Tools - Coq_makefile lets one override or extend the following variables from @@ -219,8 +231,6 @@ Vernacular Commands scope. If you want the previous behavior, use `Global Set SsrHave NoTCResolution`. - Multiple sections with the same name are allowed. -- `Combined Scheme` can now work when inductive schemes are generated in sort - `Type`. It used to be limited to sort `Prop`. Coq binaries and process model @@ -260,8 +270,6 @@ Standard Library - There are now conversions between `string` and `positive`, `Z`, `nat`, and `N` in binary, octal, and hex. -- Added `ByteVector` type that can convert to and from [string]. - Display diffs between proof steps - `coqtop` and `coqide` can now highlight the differences between proof steps diff --git a/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh b/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh new file mode 100644 index 0000000000..17eb5fffae --- /dev/null +++ b/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8889" ] || [ "$CI_BRANCH" = "program-hook-obligation-subst" ]; then + + Equations_CI_REF=program-hook-obligation-subst + Equations_CI_GITURL=https://github.com/mattam82/Coq-Equations + +fi diff --git a/vernac/classes.ml b/vernac/classes.ml index 84ffb84206..f4b0015851 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -149,7 +149,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype = let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in if program_mode then - let hook _ vis gr = + let hook _ _ vis gr = let cst = match gr with ConstRef kn -> kn | _ -> assert false in Impargs.declare_manual_implicits false gr ~enriching:false [imps]; let pri = intern_info pri in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index cc03473bc6..472411ac3a 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -109,7 +109,7 @@ let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook = Obligations.eterm_obligations env ident evd 0 c typ in let ctx = Evd.evar_universe_context evd in - let hook = Obligations.mk_univ_hook (fun _ l r -> Lemmas.call_hook (fun x -> x) hook l r) in + let hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook (fun x -> x) hook l r) in ignore(Obligations.add_definition ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index fe8ef1f0e0..3d3d825bd0 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -193,7 +193,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let name = add_suffix recname "_func" in (* XXX: Mutating the evar_map in the hook! *) (* XXX: Likely the sigma is out of date when the hook is called .... *) - let hook sigma _ l gr = + let hook sigma _ _ l gr = let sigma, h_body = Evarutil.new_global sigma gr in let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in @@ -212,7 +212,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = hook, name, typ else let typ = it_mkProd_or_LetIn top_arity binders_rel in - let hook sigma _ l gr = + let hook sigma _ _ l gr = if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false gr [impls] in hook, recname, typ diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 5c1384fba7..97ed43c5f4 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -20,10 +20,10 @@ open Pp open CErrors open Util -type univ_declaration_hook = UState.t -> Decl_kinds.locality -> GlobRef.t -> unit +type univ_declaration_hook = UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit let mk_univ_hook f = f -let call_univ_hook fix_exn hook uctx l c = - try hook uctx l c +let call_univ_hook fix_exn hook uctx trans l c = + try hook uctx trans l c with e when CErrors.noncritical e -> let e = CErrors.push e in iraise (fix_exn e) @@ -415,16 +415,6 @@ let replace_appvars subst = with Not_found -> Constr.map aux c else Constr.map aux c in Constr.map aux - -let subst_prog expand obls ints prg = - let subst = obl_substitution expand obls ints in - if get_hide_obligations () then - (replace_appvars subst prg.prg_body, - replace_appvars subst ((* Termops.refresh_universes *) prg.prg_type)) - else - let subst' = List.map (fun (n, (_, b)) -> n, b) subst in - (Vars.replace_vars subst' prg.prg_body, - Vars.replace_vars subst' ((* Termops.refresh_universes *) prg.prg_type)) let subst_deps_obl obls obl = let t' = subst_deps true obls obl.obl_deps obl.obl_type in @@ -471,19 +461,30 @@ let rec intset_to = function -1 -> Int.Set.empty | n -> Int.Set.add n (intset_to (pred n)) -let subst_body expand prg = +let subst_prog subst prg = + if get_hide_obligations () then + (replace_appvars subst prg.prg_body, + replace_appvars subst ((* Termops.refresh_universes *) prg.prg_type)) + else + let subst' = List.map (fun (n, (_, b)) -> n, b) subst in + (Vars.replace_vars subst' prg.prg_body, + Vars.replace_vars subst' ((* Termops.refresh_universes *) prg.prg_type)) + +let obligation_substitution expand prg = let obls, _ = prg.prg_obligations in let ints = intset_to (pred (Array.length obls)) in - subst_prog expand obls ints prg + obl_substitution expand obls ints let declare_definition prg = - let body, typ = subst_body true prg in + let varsubst = obligation_substitution true prg in + let body, typ = subst_prog varsubst prg in let nf = UnivSubst.nf_evars_and_universes_opt_subst (fun x -> None) (UState.subst prg.prg_ctx) in let opaque = prg.prg_opaque in let fix_exn = Hook.get get_fix_exn () in let typ = nf typ in let body = nf body in + let obls = List.map (fun (id, (_, c)) -> (id, nf c)) varsubst in let uvars = Univ.LSet.union (Vars.universes_of_constr typ) (Vars.universes_of_constr body) in @@ -494,7 +495,7 @@ let declare_definition prg = let ubinders = UState.universe_binders uctx in DeclareDef.declare_definition prg.prg_name prg.prg_kind ce ubinders prg.prg_implicits - (Lemmas.mk_hook (fun l r -> call_univ_hook fix_exn prg.prg_hook uctx l r ; ())) + (Lemmas.mk_hook (fun l r -> call_univ_hook fix_exn prg.prg_hook uctx obls l r ; ())) let rec lam_index n t acc = match Constr.kind t with @@ -522,19 +523,26 @@ let mk_proof c = ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constant let declare_mutual_definition l = let len = List.length l in let first = List.hd l in - let fixdefs, fixtypes, fiximps = - List.split3 - (List.map (fun x -> - let subs, typ = (subst_body true x) in - let env = Global.env () in - let sigma = Evd.from_ctx x.prg_ctx in - let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in - let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in - let term = EConstr.to_constr sigma term in - let typ = EConstr.to_constr sigma typ in - x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l) + let defobl x = + let oblsubst = obligation_substitution true x in + let subs, typ = subst_prog oblsubst x in + let env = Global.env () in + let sigma = Evd.from_ctx x.prg_ctx in + let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in + let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in + let term = EConstr.to_constr sigma term in + let typ = EConstr.to_constr sigma typ in + let def = (x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) in + let oblsubst = List.map (fun (id, (_, c)) -> id, c) oblsubst in + def, oblsubst + in + let defs, obls = + List.fold_right (fun x (defs, obls) -> + let xdef, xobls = defobl x in + (xdef :: defs, xobls @ obls)) l ([], []) in (* let fixdefs = List.map reduce_fix fixdefs in *) + let fixdefs, fixtypes, fiximps = List.split3 defs in let fixkind = Option.get first.prg_fixkind in let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in @@ -568,7 +576,7 @@ let declare_mutual_definition l = List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; let gr = List.hd kns in - call_univ_hook fix_exn first.prg_hook first.prg_ctx local gr; + call_univ_hook fix_exn first.prg_hook first.prg_ctx obls local gr; List.iter progmap_remove l; gr let decompose_lam_prod c ty = @@ -1105,7 +1113,7 @@ let show_term n = let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic - ?(reduce=reduce) ?(hook=mk_univ_hook (fun _ _ _ -> ())) ?(opaque = false) obls = + ?(reduce=reduce) ?(hook=mk_univ_hook (fun _ _ _ _ -> ())) ?(opaque = false) obls = let sign = Lemmas.initialize_named_context_for_proof () in let info = Id.print n ++ str " has type-checked" in let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce hook in @@ -1125,7 +1133,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) - ?(hook=mk_univ_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind = + ?(hook=mk_univ_hook (fun _ _ _ _ -> ())) ?(opaque = false) notations fixkind = let sign = Lemmas.initialize_named_context_for_proof () in let deps = List.map (fun (n, b, t, imps, obls) -> n) l in List.iter diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 80294c7a76..57040b3f7c 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -14,8 +14,8 @@ open Evd open Names type univ_declaration_hook -val mk_univ_hook : (UState.t -> Decl_kinds.locality -> GlobRef.t -> unit) -> univ_declaration_hook -val call_univ_hook : Future.fix_exn -> univ_declaration_hook -> UState.t -> Decl_kinds.locality -> GlobRef.t -> unit +val mk_univ_hook : (UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit) -> univ_declaration_hook +val call_univ_hook : Future.fix_exn -> univ_declaration_hook -> UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit (* This is a hack to make it possible for Obligations to craft a Qed * behind the scenes. The fix_exn the Stm attaches to the Future proof |