diff options
| -rw-r--r-- | dev/ci/user-overlays/08844-split-tactics.sh | 12 | ||||
| -rw-r--r-- | dev/doc/proof-engine.md | 31 | ||||
| -rw-r--r-- | doc/sphinx/language/cic.rst | 6 | ||||
| -rw-r--r-- | engine/eConstr.ml | 8 | ||||
| -rw-r--r-- | engine/eConstr.mli | 2 | ||||
| -rw-r--r-- | engine/evd.ml | 2 | ||||
| -rw-r--r-- | engine/evd.mli | 3 | ||||
| -rw-r--r-- | engine/termops.ml | 8 | ||||
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 4 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 2 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 1 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 20 | ||||
| -rw-r--r-- | stm/stm.ml | 2 | ||||
| -rw-r--r-- | tactics/abstract.ml | 195 | ||||
| -rw-r--r-- | tactics/abstract.mli | 16 | ||||
| -rw-r--r-- | tactics/tactics.ml | 176 | ||||
| -rw-r--r-- | tactics/tactics.mli | 4 | ||||
| -rw-r--r-- | tactics/tactics.mllib | 1 | ||||
| -rw-r--r-- | test-suite/misc/poly-capture-global-univs/.gitignore | 1 | ||||
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 3 | ||||
| -rw-r--r-- | vernac/himsg.ml | 5 | ||||
| -rw-r--r-- | vernac/obligations.ml | 12 |
22 files changed, 288 insertions, 226 deletions
diff --git a/dev/ci/user-overlays/08844-split-tactics.sh b/dev/ci/user-overlays/08844-split-tactics.sh new file mode 100644 index 0000000000..8ad8cba243 --- /dev/null +++ b/dev/ci/user-overlays/08844-split-tactics.sh @@ -0,0 +1,12 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8844" ] || [ "$CI_BRANCH" = "split-tactics" ]; then + Equations_CI_REF=split-tactics + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + ltac2_CI_REF=split-tactics + ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2 + + fiat_parsers_CI_REF=split-tactics + fiat_parsers_CI_GITURL=https://github.com/SkySkimmer/fiat +fi diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md index 8f96ac223f..774552237a 100644 --- a/dev/doc/proof-engine.md +++ b/dev/doc/proof-engine.md @@ -42,8 +42,8 @@ goal holes thanks to the `Refine` module, and in particular to the `Refine.refine` primitive. ```ocaml -val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic -(** In [refine typecheck t], [t] is a term with holes under some +val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic +(** In [refine ~typecheck t], [t] is a term with holes under some [evar_map] context. The term [t] is used as a partial solution for the current goal (refine is a goal-dependent tactic), the new holes created by [t] become the new subgoals. Exceptions @@ -51,12 +51,11 @@ val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) ``` -In a first approximation, we can think of `'a Sigma.run` as -`evar_map -> 'a * evar_map`. What the function does is first evaluate the -`Constr.t Sigma.run` argument in the current proof state, and then use the -resulting term as a filler for the proof under focus. All evars that have been -created by the invocation of this thunk are then turned into new goals added in -the order of their creation. +What the function does is first evaluate the `t` argument in the +current proof state, and then use the resulting term as a filler for +the proof under focus. All evars that have been created by the +invocation of this thunk are then turned into new goals added in the +order of their creation. To see how we can use it, let us have a look at an idealized example, the `cut` tactic. Assuming `X` is a type, `cut X` fills the current goal `[Γ ⊢ _ : A]` @@ -66,8 +65,7 @@ two new holes `[e1, e2]` are added to the goal state in this order. ```ocaml let cut c = - let open Sigma in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> (** In this block, we focus on one goal at a time indicated by gl *) let env = Proofview.Goal.env gl in (** Get the context of the goal, essentially [Γ] *) @@ -80,25 +78,22 @@ let cut c = let t = mkArrow c (Vars.lift 1 concl) in (** Build [X -> A]. Note the lifting of [A] due to being on the right hand side of the arrow. *) - Refine.refine { run = begin fun sigma -> + Refine.refine begin fun sigma -> (** All evars generated by this block will be added as goals *) - let Sigma (f, sigma, p) = Evarutil.new_evar env sigma t in + let sigma, f = Evarutil.new_evar env sigma t in (** Generate ?e1 : [Γ ⊢ _ : X -> A], add it to sigma, and return the term [f := Γ ⊢ ?e1{Γ} : X -> A] with the updated sigma. The identity substitution for [Γ] is extracted from the [env] argument, so that one must be careful to pass the correct context here in order for the resulting term to be well-typed. The [p] return value is a proof term used to enforce sigma monotonicity. *) - let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c in + let sigma, x = Evarutil.new_evar env sigma c in (** Generate ?e2 : [Γ ⊢ _ : X] in sigma and return [x := Γ ⊢ ?e2{Γ} : X]. *) let r = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 r, [|mkRel 1|])) in (** Build [r := Γ ⊢ let id : X := ?e2{Γ} in ?e1{Γ} id : A] *) - Sigma (r, sigma, p +> q) - (** Fills the current hole with [r]. The [p +> q] thingy ensures - monotonicity of sigma. *) - end } - end } + end + end ``` The `Evarutil.new_evar` function is the preferred way to generate evars in diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 835d6dcaa6..cc5d9d6205 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -678,7 +678,7 @@ form*. There are several ways (or strategies) to apply the reduction rules. Among them, we have to mention the *head reduction* which will play an important role (see Chapter :ref:`tactics`). Any term :math:`t` can be written as :math:`λ x_1 :T_1 . … λ x_k :T_k . (t_0~t_1 … t_n )` where :math:`t_0` is not an -application. We say then that :math:`t~0` is the *head of* :math:`t`. If we assume +application. We say then that :math:`t_0` is the *head of* :math:`t`. If we assume that :math:`t_0` is :math:`λ x:T. u_0` then one step of β-head reduction of :math:`t` is: .. math:: @@ -771,8 +771,8 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is \odd&:&\nat → \Prop \end{array}\right]} {\left[\begin{array}{rcl} \evenO &:& \even~0\\ - \evenS &:& \forall n, \odd~n -> \even~(\kw{S}~n)\\ - \oddS &:& \forall n, \even~n -> \odd~(\kw{S}~n) + \evenS &:& \forall n, \odd~n → \even~(\kw{S}~n)\\ + \oddS &:& \forall n, \even~n → \odd~(\kw{S}~n) \end{array}\right]} which corresponds to the result of the |Coq| declaration: diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 3385b78958..cfc4bea85f 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -99,6 +99,14 @@ let isFix sigma c = match kind sigma c with Fix _ -> true | _ -> false let isCoFix sigma c = match kind sigma c with CoFix _ -> true | _ -> false let isCase sigma c = match kind sigma c with Case _ -> true | _ -> false let isProj sigma c = match kind sigma c with Proj _ -> true | _ -> false + +let rec isType sigma c = match kind sigma c with + | Sort s -> (match ESorts.kind sigma s with + | Sorts.Type _ -> true + | _ -> false ) + | Cast (c,_,_) -> isType sigma c + | _ -> false + let isVarId sigma id c = match kind sigma c with Var id' -> Id.equal id id' | _ -> false let isRelN sigma n c = diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 1edc0ee12b..6532e08e9d 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -157,6 +157,8 @@ val isCoFix : Evd.evar_map -> t -> bool val isCase : Evd.evar_map -> t -> bool val isProj : Evd.evar_map -> t -> bool +val isType : Evd.evar_map -> constr -> bool + type arity = rel_context * ESorts.t val destArity : Evd.evar_map -> types -> arity val isArity : Evd.evar_map -> t -> bool diff --git a/engine/evd.ml b/engine/evd.ml index 3a77a2b440..b3848e1b5b 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -483,6 +483,8 @@ let is_typeclass_evar evd evk = let flags = evd.evar_flags in Evar.Set.mem evk flags.typeclass_evars +let get_obligation_evars evd = evd.evar_flags.obligation_evars + let set_obligation_evar evd evk = let flags = evd.evar_flags in let evar_flags = { flags with obligation_evars = Evar.Set.add evk flags.obligation_evars } in diff --git a/engine/evd.mli b/engine/evd.mli index b0e3c2b869..be54bebcd7 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -262,6 +262,9 @@ val get_typeclass_evars : evar_map -> Evar.Set.t val is_typeclass_evar : evar_map -> Evar.t -> bool (** Is the evar declared resolvable for typeclass resolution *) +val get_obligation_evars : evar_map -> Evar.Set.t +(** The set of obligation evars *) + val set_obligation_evar : evar_map -> Evar.t -> evar_map (** Declare an evar as an obligation *) diff --git a/engine/termops.ml b/engine/termops.ml index f720e5195d..181efa0ade 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -366,12 +366,18 @@ let pr_evar_map_gen with_univs pr_evars env sigma = else str "TYPECLASSES:" ++ brk (0, 1) ++ prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl () + and obligations = + let evars = Evd.get_obligation_evars sigma in + if Evar.Set.is_empty evars then mt () + else + str "OBLIGATIONS:" ++ brk (0, 1) ++ + prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl () and metas = if List.is_empty (Evd.meta_list sigma) then mt () else str "METAS:" ++ brk (0, 1) ++ pr_meta_map env sigma in - evs ++ svs ++ cstrs ++ typeclasses ++ metas + evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas let pr_evar_list env sigma l = let open Evd in diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index b660865e8b..05a65e4cd8 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -855,9 +855,9 @@ END TACTIC EXTEND transparent_abstract | [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl -> - Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end } | [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl -> - Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end } END (* ********************************************************************* *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 5828494454..2a046a3e65 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1078,7 +1078,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with push_trace(None,call) ist >>= fun trace -> Profile_ltac.do_profile "eval_tactic:TacAbstract" trace (catch_error_tac trace begin - Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT + Proofview.Goal.enter begin fun gl -> Abstract.tclABSTRACT (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist t) end end) | TacThen (t1,t) -> diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index e15c00f7dc..e21c2fda85 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -104,6 +104,7 @@ let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env ev Evar_kinds.qm_name=na; }) in let evd, v = Evarutil.new_evar env !evdref ~src c in + let evd = Evd.set_obligation_evar evd (fst (destEvar evd v)) in evdref := evd; v diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 55817f1b76..24767ca4d1 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -457,6 +457,15 @@ let pretype_sort ?loc sigma = function let new_type_evar env sigma loc = new_type_evar env sigma ~src:(Loc.tag ?loc Evar_kinds.InternalHole) +let mark_obligation_evar sigma k evc = + if Flags.is_program_mode () then + match k with + | Evar_kinds.QuestionMark _ + | Evar_kinds.ImplicitArg (_, _, false) -> + Evd.set_obligation_evar sigma (fst (destEvar sigma evc)) + | _ -> sigma + else sigma + (* [pretype tycon env sigma lvar lmeta cstr] attempts to type [cstr] *) (* in environment [env], with existential variables [sigma] and *) (* the type constraint tycon *) @@ -510,15 +519,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma | Some ty -> sigma, ty | None -> new_type_evar env sigma loc in let sigma, uj_val = new_evar env sigma ~src:(loc,k) ~naming ty in - let sigma = - if Flags.is_program_mode () then - match k with - | Evar_kinds.QuestionMark _ - | Evar_kinds.ImplicitArg (_, _, false) -> - Evd.set_obligation_evar sigma (fst (destEvar sigma uj_val)) - | _ -> sigma - else sigma - in + let sigma = mark_obligation_evar sigma k uj_val in sigma, { uj_val; uj_type = ty } | GHole (k, _naming, Some arg) -> @@ -1039,6 +1040,7 @@ and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get | None -> let sigma, s = new_sort_variable univ_flexible_alg sigma in let sigma, utj_val = new_evar env sigma ~src:(loc, knd) ~naming (mkSort s) in + let sigma = mark_obligation_evar sigma knd utj_val in sigma, { utj_val; utj_type = s}) | _ -> let sigma, j = pretype k0 resolve_tc empty_tycon env sigma c in diff --git a/stm/stm.ml b/stm/stm.ml index 19915b1600..b731678f6d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2028,7 +2028,7 @@ end = struct (* {{{ *) str"g=" ++ int (Evar.repr gid) ++ spc () ++ str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++ str"uc=" ++ Termops.pr_evar_universe_context uc)); - (if abstract then Tactics.tclABSTRACT None else (fun x -> x)) + (if abstract then Abstract.tclABSTRACT None else (fun x -> x)) (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*> Tactics.exact_no_check (EConstr.of_constr pt)) | None -> diff --git a/tactics/abstract.ml b/tactics/abstract.ml new file mode 100644 index 0000000000..2b4d9a7adf --- /dev/null +++ b/tactics/abstract.ml @@ -0,0 +1,195 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +module CVars = Vars + +open Util +open Names +open Termops +open EConstr +open Decl_kinds +open Evarutil + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + +(* tactical to save as name a subproof such that the generalisation of + the current goal, abstracted with respect to the local signature, + is solved by tac *) + +(** d1 is the section variable in the global context, d2 in the goal context *) +let interpretable_as_section_decl env evd d1 d2 = + let open Context.Named.Declaration in + let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes env !sigma c1 c2 with + | None -> false + | Some cstr -> + try ignore (Evd.add_universe_constraints !sigma cstr); true + with UState.UniversesDiffer -> false + in + match d2, d1 with + | LocalDef _, LocalAssum _ -> false + | LocalDef (_,b1,t1), LocalDef (_,b2,t2) -> + e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2 + | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (NamedDecl.get_type d2) + +let rec decompose len c t accu = + let open Constr in + let open Context.Rel.Declaration in + if len = 0 then (c, t, accu) + else match kind c, kind t with + | Lambda (na, u, c), Prod (_, _, t) -> + decompose (pred len) c t (LocalAssum (na, u) :: accu) + | LetIn (na, b, u, c), LetIn (_, _, _, t) -> + decompose (pred len) c t (LocalDef (na, b, u) :: accu) + | _ -> assert false + +let rec shrink ctx sign c t accu = + let open Constr in + let open CVars in + match ctx, sign with + | [], [] -> (c, t, accu) + | p :: ctx, decl :: sign -> + if noccurn 1 c && noccurn 1 t then + let c = subst1 mkProp c in + let t = subst1 mkProp t in + shrink ctx sign c t accu + else + let c = Term.mkLambda_or_LetIn p c in + let t = Term.mkProd_or_LetIn p t in + let accu = if RelDecl.is_local_assum p + then mkVar (NamedDecl.get_id decl) :: accu + else accu + in + shrink ctx sign c t accu +| _ -> assert false + +let shrink_entry sign const = + let open Entries in + let typ = match const.const_entry_type with + | None -> assert false + | Some t -> t + in + (** The body has been forced by the call to [build_constant_by_tactic] *) + let () = assert (Future.is_over const.const_entry_body) in + let ((body, uctx), eff) = Future.force const.const_entry_body in + let (body, typ, ctx) = decompose (List.length sign) body typ [] in + let (body, typ, args) = shrink ctx sign body typ [] in + let const = { const with + const_entry_body = Future.from_val ((body, uctx), eff); + const_entry_type = Some typ; + } in + (const, args) + +let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = + let open Tacticals.New in + let open Tacmach.New in + let open Proofview.Notations in + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let current_sign = Global.named_context_val () + and global_sign = Proofview.Goal.hyps gl in + let evdref = ref sigma in + let sign,secsign = + List.fold_right + (fun d (s1,s2) -> + let id = NamedDecl.get_id d in + if mem_named_context_val id current_sign && + interpretable_as_section_decl env evdref (lookup_named_val id current_sign) d + then (s1,push_named_context_val d s2) + else (Context.Named.add d s1,s2)) + global_sign (Context.Named.empty, Environ.empty_named_context_val) in + let id = Namegen.next_global_ident_away id (pf_ids_set_of_hyps gl) in + let concl = match goal_type with + | None -> Proofview.Goal.concl gl + | Some ty -> ty in + let concl = it_mkNamedProd_or_LetIn concl sign in + let concl = + try flush_and_check_evars !evdref concl + with Uninstantiated_evar _ -> + CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.") in + + let evd, ctx, concl = + (* FIXME: should be done only if the tactic succeeds *) + let evd = Evd.minimize_universes !evdref in + let ctx = Evd.universe_context_set evd in + evd, ctx, Evarutil.nf_evars_universes evd concl + in + let concl = EConstr.of_constr concl in + let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in + let ectx = Evd.evar_universe_context evd in + let (const, safe, ectx) = + try Pfedit.build_constant_by_tactic ~goal_kind:gk id ectx secsign concl solve_tac + with Logic_monad.TacticFailure e as src -> + (* if the tactic [tac] fails, it reports a [TacticFailure e], + which is an error irrelevant to the proof system (in fact it + means that [e] comes from [tac] failing to yield enough + success). Hence it reraises [e]. *) + let (_, info) = CErrors.push src in + iraise (e, info) + in + let const, args = shrink_entry sign const in + let args = List.map EConstr.of_constr args in + let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in + let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in + let cst () = + (** do not compute the implicit arguments, it may be costly *) + let () = Impargs.make_implicit_args false in + (** ppedrot: seems legit to have abstracted subproofs as local*) + Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl + in + let cst = Impargs.with_implicit_protection cst () in + let inst = match const.Entries.const_entry_universes with + | Entries.Monomorphic_const_entry _ -> EInstance.empty + | Entries.Polymorphic_const_entry ctx -> + (** We mimick what the kernel does, that is ensuring that no additional + constraints appear in the body of polymorphic constants. Ideally this + should be enforced statically. *) + let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in + let () = assert (Univ.ContextSet.is_empty body_uctx) in + EInstance.make (Univ.UContext.instance ctx) + in + let lem = mkConstU (cst, inst) in + let evd = Evd.set_universe_context evd ectx in + let open Safe_typing in + let eff = private_con_of_con (Global.safe_env ()) cst in + let effs = concat_private eff + Entries.(snd (Future.force const.const_entry_body)) in + let solve = + Proofview.tclEFFECTS effs <*> + tacK lem args + in + let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) tac + end + +let abstract_subproof ~opaque id gk tac = + cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> Tactics.exact_no_check (applist (lem, args))) + +let anon_id = Id.of_string "anonymous" + +let name_op_to_name name_op object_kind suffix = + let open Proof_global in + let default_gk = (Global, false, object_kind) in + let name, gk = match Proof_global.V82.get_current_initial_conclusions () with + | (id, (_, gk)) -> Some id, gk + | exception NoCurrentProof -> None, default_gk + in + match name_op with + | Some s -> s, gk + | None -> + let name = Option.default anon_id name in + Nameops.add_suffix name suffix, gk + +let tclABSTRACT ?(opaque=true) name_op tac = + let s, gk = if opaque + then name_op_to_name name_op (Proof Theorem) "_subproof" + else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in + abstract_subproof ~opaque s gk tac diff --git a/tactics/abstract.mli b/tactics/abstract.mli new file mode 100644 index 0000000000..7fb671fbf8 --- /dev/null +++ b/tactics/abstract.mli @@ -0,0 +1,16 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open EConstr + +val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic + +val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a6a104ccca..25f9bc5576 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -module CVars = Vars - open Pp open CErrors open Util @@ -36,7 +34,6 @@ open Refiner open Tacticals open Hipattern open Coqlib -open Decl_kinds open Evarutil open Indrec open Pretype_errors @@ -4884,179 +4881,6 @@ let transitivity t = transitivity_gen (Some t) let intros_transitivity n = Tacticals.New.tclTHEN intros (transitivity_gen n) -(* tactical to save as name a subproof such that the generalisation of - the current goal, abstracted with respect to the local signature, - is solved by tac *) - -(** d1 is the section variable in the global context, d2 in the goal context *) -let interpretable_as_section_decl env evd d1 d2 = - let open Context.Named.Declaration in - let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes env !sigma c1 c2 with - | None -> false - | Some cstr -> - try ignore (Evd.add_universe_constraints !sigma cstr); true - with UniversesDiffer -> false - in - match d2, d1 with - | LocalDef _, LocalAssum _ -> false - | LocalDef (_,b1,t1), LocalDef (_,b2,t2) -> - e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2 - | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (NamedDecl.get_type d2) - -let rec decompose len c t accu = - let open Context.Rel.Declaration in - if len = 0 then (c, t, accu) - else match Constr.kind c, Constr.kind t with - | Lambda (na, u, c), Prod (_, _, t) -> - decompose (pred len) c t (LocalAssum (na, u) :: accu) - | LetIn (na, b, u, c), LetIn (_, _, _, t) -> - decompose (pred len) c t (LocalDef (na, b, u) :: accu) - | _ -> assert false - -let rec shrink ctx sign c t accu = - let open Constr in - let open CVars in - match ctx, sign with - | [], [] -> (c, t, accu) - | p :: ctx, decl :: sign -> - if noccurn 1 c && noccurn 1 t then - let c = subst1 mkProp c in - let t = subst1 mkProp t in - shrink ctx sign c t accu - else - let c = Term.mkLambda_or_LetIn p c in - let t = Term.mkProd_or_LetIn p t in - let accu = if RelDecl.is_local_assum p - then mkVar (NamedDecl.get_id decl) :: accu - else accu - in - shrink ctx sign c t accu -| _ -> assert false - -let shrink_entry sign const = - let open Entries in - let typ = match const.const_entry_type with - | None -> assert false - | Some t -> t - in - (** The body has been forced by the call to [build_constant_by_tactic] *) - let () = assert (Future.is_over const.const_entry_body) in - let ((body, uctx), eff) = Future.force const.const_entry_body in - let (body, typ, ctx) = decompose (List.length sign) body typ [] in - let (body, typ, args) = shrink ctx sign body typ [] in - let const = { const with - const_entry_body = Future.from_val ((body, uctx), eff); - const_entry_type = Some typ; - } in - (const, args) - -let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = - let open Tacticals.New in - let open Tacmach.New in - let open Proofview.Notations in - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in - let current_sign = Global.named_context_val () - and global_sign = Proofview.Goal.hyps gl in - let evdref = ref sigma in - let sign,secsign = - List.fold_right - (fun d (s1,s2) -> - let id = NamedDecl.get_id d in - if mem_named_context_val id current_sign && - interpretable_as_section_decl env evdref (lookup_named_val id current_sign) d - then (s1,push_named_context_val d s2) - else (Context.Named.add d s1,s2)) - global_sign (Context.Named.empty, empty_named_context_val) in - let id = next_global_ident_away id (pf_ids_set_of_hyps gl) in - let concl = match goal_type with - | None -> Proofview.Goal.concl gl - | Some ty -> ty in - let concl = it_mkNamedProd_or_LetIn concl sign in - let concl = - try flush_and_check_evars !evdref concl - with Uninstantiated_evar _ -> - error "\"abstract\" cannot handle existentials." in - - let evd, ctx, concl = - (* FIXME: should be done only if the tactic succeeds *) - let evd = Evd.minimize_universes !evdref in - let ctx = Evd.universe_context_set evd in - evd, ctx, Evarutil.nf_evars_universes evd concl - in - let concl = EConstr.of_constr concl in - let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in - let ectx = Evd.evar_universe_context evd in - let (const, safe, ectx) = - try Pfedit.build_constant_by_tactic ~goal_kind:gk id ectx secsign concl solve_tac - with Logic_monad.TacticFailure e as src -> - (* if the tactic [tac] fails, it reports a [TacticFailure e], - which is an error irrelevant to the proof system (in fact it - means that [e] comes from [tac] failing to yield enough - success). Hence it reraises [e]. *) - let (_, info) = CErrors.push src in - iraise (e, info) - in - let const, args = shrink_entry sign const in - let args = List.map EConstr.of_constr args in - let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in - let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in - let cst () = - (** do not compute the implicit arguments, it may be costly *) - let () = Impargs.make_implicit_args false in - (** ppedrot: seems legit to have abstracted subproofs as local*) - Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl - in - let cst = Impargs.with_implicit_protection cst () in - let inst = match const.Entries.const_entry_universes with - | Entries.Monomorphic_const_entry _ -> EInstance.empty - | Entries.Polymorphic_const_entry ctx -> - (** We mimick what the kernel does, that is ensuring that no additional - constraints appear in the body of polymorphic constants. Ideally this - should be enforced statically. *) - let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in - let () = assert (Univ.ContextSet.is_empty body_uctx) in - EInstance.make (Univ.UContext.instance ctx) - in - let lem = mkConstU (cst, inst) in - let evd = Evd.set_universe_context evd ectx in - let open Safe_typing in - let eff = private_con_of_con (Global.safe_env ()) cst in - let effs = concat_private eff - Entries.(snd (Future.force const.const_entry_body)) in - let solve = - Proofview.tclEFFECTS effs <*> - tacK lem args - in - let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) tac - end - -let abstract_subproof ~opaque id gk tac = - cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args))) - -let anon_id = Id.of_string "anonymous" - -let name_op_to_name name_op object_kind suffix = - let open Proof_global in - let default_gk = (Global, false, object_kind) in - let name, gk = match Proof_global.V82.get_current_initial_conclusions () with - | (id, (_, gk)) -> Some id, gk - | exception NoCurrentProof -> None, default_gk - in - match name_op with - | Some s -> s, gk - | None -> - let name = Option.default anon_id name in - add_suffix name suffix, gk - -let tclABSTRACT ?(opaque=true) name_op tac = - let s, gk = if opaque - then name_op_to_name name_op (Proof Theorem) "_subproof" - else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in - abstract_subproof ~opaque s gk tac - let constr_eq ~strict x y = let fail = Tacticals.New.tclFAIL 0 (str "Not equal") in let fail_universes = Tacticals.New.tclFAIL 0 (str "Not equal (due to universes)") in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 24c12ffd82..7efadb2c28 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -418,10 +418,6 @@ val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic -val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic - -val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic - val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic val specialize_eqs : Id.t -> unit Proofview.tactic diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index f54ad86a3f..5afec74fae 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -7,6 +7,7 @@ Ind_tables Eqschemes Elimschemes Tactics +Abstract Elim Equality Contradiction diff --git a/test-suite/misc/poly-capture-global-univs/.gitignore b/test-suite/misc/poly-capture-global-univs/.gitignore index f5a6d22b8e..2a6a6bc68d 100644 --- a/test-suite/misc/poly-capture-global-univs/.gitignore +++ b/test-suite/misc/poly-capture-global-univs/.gitignore @@ -1 +1,2 @@ /Makefile* +/src/evil.ml diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index cea8af3f05..fe8ef1f0e0 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -178,7 +178,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let sigma, h_e_term = Evarutil.new_evar env sigma ~src:(Loc.tag @@ Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Evar_kinds.Define false; - }) wf_proof in + }) wf_proof in + let sigma = Evd.set_obligation_evar sigma (fst (destEvar sigma h_e_term)) in sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |]) in let sigma, def = Typing.solve_evars env sigma def in diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 844caf5a3e..ad6ca3a84e 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -391,11 +391,10 @@ let explain_unexpected_type env sigma actual_type expected_type = str "where" ++ spc () ++ prexp ++ str " was expected." let explain_not_product env sigma c = - let c = EConstr.to_constr sigma c in - let pr = pr_lconstr_env env sigma c in + let pr = pr_econstr_env env sigma c in str "The type of this term is a product" ++ spc () ++ str "while it is expected to be" ++ - (if Constr.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "." + (if EConstr.isType sigma c then str " a sort" else (brk(1,1) ++ pr)) ++ str "." (* TODO: use the names *) (* (co)fixpoints *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index fbf552e649..5c1384fba7 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -37,13 +37,11 @@ let succfix (depth, fixrels) = let check_evars env evm = Evar.Map.iter - (fun key evi -> - let (loc,k) = evar_source key evm in - match k with - | Evar_kinds.QuestionMark _ - | Evar_kinds.ImplicitArg (_,_,false) -> () - | _ -> - Pretype_errors.error_unsolvable_implicit ?loc env evm key None) + (fun key evi -> + if Evd.is_obligation_evar evm key then () + else + let (loc,k) = evar_source key evm in + Pretype_errors.error_unsolvable_implicit ?loc env evm key None) (Evd.undefined_map evm) type oblinfo = |