diff options
29 files changed, 424 insertions, 177 deletions
diff --git a/dev/tools/make-changelog.sh b/dev/tools/make-changelog.sh index ea96de970a..ec59a6047f 100755 --- a/dev/tools/make-changelog.sh +++ b/dev/tools/make-changelog.sh @@ -7,7 +7,8 @@ echo "Where? (type a prefix)" (cd doc/changelog && ls -d */) read -r where -where=$(echo doc/changelog/"$where"*) +where="doc/changelog/$where" +if ! [ -d "$where" ]; then where=$(echo "$where"*); fi where="$where/$PR-$(git rev-parse --abbrev-ref HEAD).rst" # shellcheck disable=SC2016 diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index c08a9ed0e6..6410620b40 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1046,6 +1046,67 @@ between universes for inductive types in the Type hierarchy. exT_intro : forall X:Type, P X -> exType P. +.. example:: Negative occurrence (first example) + + The following inductive definition is rejected because it does not + satisfy the positivity condition: + + .. coqtop:: all + + Fail Inductive I : Prop := not_I_I (not_I : I -> False) : I. + + If we were to accept such definition, we could derive a + contradiction from it (we can test this by disabling the + :flag:`Positivity Checking` flag): + + .. coqtop:: none + + Unset Positivity Checking. + Inductive I : Prop := not_I_I (not_I : I -> False) : I. + Set Positivity Checking. + + .. coqtop:: all + + Definition I_not_I : I -> ~ I := fun i => + match i with not_I_I not_I => not_I end. + + .. coqtop:: in + + Lemma contradiction : False. + Proof. + enough (I /\ ~ I) as [] by contradiction. + split. + - apply not_I_I. + intro. + now apply I_not_I. + - intro. + now apply I_not_I. + Qed. + +.. example:: Negative occurrence (second example) + + Here is another example of an inductive definition which is + rejected because it does not satify the positivity condition: + + .. coqtop:: all + + Fail Inductive Lam := lam (_ : Lam -> Lam). + + Again, if we were to accept it, we could derive a contradiction + (this time through a non-terminating recursive function): + + .. coqtop:: none + + Unset Positivity Checking. + Inductive Lam := lam (_ : Lam -> Lam). + Set Positivity Checking. + + .. coqtop:: all + + Fixpoint infinite_loop l : False := + match l with lam x => infinite_loop (x l) end. + + Check infinite_loop (lam (@id Lam)) : False. .. _Template-polymorphism: diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 18d2c79461..cfdc70d50e 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -563,6 +563,20 @@ for it. - `&x` as a Coq constr expression expands to `ltac2:(Control.refine (fun () => hyp @x))`. +In the special case where Ltac2 antiquotations appear inside a Coq term +notation, the notation variables are systematically bound in the body +of the tactic expression with type `Ltac2.Init.preterm`. Such a type represents +untyped syntactic Coq expressions, which can by typed in the +current context using the `Ltac2.Constr.pretype` function. + +.. example:: + + The following notation is essentially the identity. + + .. coqtop:: in + + Notation "[ x ]" := ltac2:(let x := Ltac2.Constr.pretype x in exact $x) (only parsing). + Dynamic semantics ***************** diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 87b9a8eea3..470782a7dc 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -263,7 +263,7 @@ GRAMMAR EXTEND Gram { mkProdCN ~loc bl c } | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> { mkLambdaCN ~loc bl c } - | "let"; id=name; bl = binders; ty = type_cstr; ":="; + | "let"; id=name; bl = binders; ty = let_type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> { let ty,c1 = match ty, c1 with | (_,None), { CAst.v = CCast(c, CastConv t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *) @@ -353,7 +353,7 @@ GRAMMAR EXTEND Gram | "cofix" -> { false } ] ] ; fix_decl: - [ [ id=identref; bl=binders_fixannot; ty=type_cstr; ":="; + [ [ id=identref; bl=binders_fixannot; ty=let_type_cstr; ":="; c=operconstr LEVEL "200" -> { (id,fst bl,snd bl,c,ty) } ] ] ; @@ -525,7 +525,7 @@ GRAMMAR EXTEND Gram ] ] ; - type_cstr: + let_type_cstr: [ [ c=OPT [":"; c=lconstr -> { c } ] -> { Loc.tag ~loc c } ] ] ; END diff --git a/tactics/declare.ml b/tactics/declare.ml index 9f104590e7..fb06bb8a4f 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -139,9 +139,6 @@ let (inConstant : constant_obj -> obj) = subst_function = ident_subst_function; discharge_function = discharge_constant } -let declare_scheme = ref (fun _ _ -> assert false) -let set_declare_scheme f = declare_scheme := f - let update_tables c = Impargs.declare_constant_implicits c; Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstRef c) @@ -159,7 +156,7 @@ let register_side_effect (c, role) = let () = register_constant c Decls.(IsProof Theorem) ImportDefaultBehavior in match role with | None -> () - | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|] + | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme kind [|ind,c|] let record_aux env s_ty s_bo = let open Environ in diff --git a/tactics/declare.mli b/tactics/declare.mli index a4d3f17594..c646d2f85b 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -117,11 +117,6 @@ val inline_private_constants -> Evd.side_effects proof_entry -> Constr.t * UState.t -(** Since transparent constants' side effects are globally declared, we - * need that *) -val set_declare_scheme : - (string -> (inductive * Constant.t) array -> unit) -> unit - (** Declaration messages *) val definition_message : Id.t -> unit diff --git a/tactics/declareScheme.ml b/tactics/declareScheme.ml new file mode 100644 index 0000000000..5f4626fcb2 --- /dev/null +++ b/tactics/declareScheme.ml @@ -0,0 +1,42 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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 + +let scheme_map = Summary.ref Indmap.empty ~name:"Schemes" + +let cache_one_scheme kind (ind,const) = + let map = try Indmap.find ind !scheme_map with Not_found -> CString.Map.empty in + scheme_map := Indmap.add ind (CString.Map.add kind const map) !scheme_map + +let cache_scheme (_,(kind,l)) = + Array.iter (cache_one_scheme kind) l + +let subst_one_scheme subst (ind,const) = + (* Remark: const is a def: the result of substitution is a constant *) + (Mod_subst.subst_ind subst ind, Mod_subst.subst_constant subst const) + +let subst_scheme (subst,(kind,l)) = + (kind, CArray.Smart.map (subst_one_scheme subst) l) + +let discharge_scheme (_,(kind,l)) = + Some (kind, l) + +let inScheme : string * (inductive * Constant.t) array -> Libobject.obj = + let open Libobject in + declare_object @@ superglobal_object "SCHEME" + ~cache:cache_scheme + ~subst:(Some subst_scheme) + ~discharge:discharge_scheme + +let declare_scheme kind indcl = + Lib.add_anonymous_leaf (inScheme (kind,indcl)) + +let lookup_scheme kind ind = CString.Map.find kind (Indmap.find ind !scheme_map) diff --git a/tactics/declareScheme.mli b/tactics/declareScheme.mli new file mode 100644 index 0000000000..f2ae5e41c8 --- /dev/null +++ b/tactics/declareScheme.mli @@ -0,0 +1,12 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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) *) +(************************************************************************) + +val declare_scheme : string -> (Names.inductive * Names.Constant.t) array -> unit +val lookup_scheme : string -> Names.inductive -> Names.Constant.t diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index ac98b5f116..9c94f3c319 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -15,8 +15,6 @@ declaring schemes and generating schemes on demand *) open Names -open Mod_subst -open Libobject open Nameops open Declarations open Constr @@ -40,33 +38,8 @@ type individual_scheme_object_function = type 'a scheme_kind = string -let scheme_map = Summary.ref Indmap.empty ~name:"Schemes" - let pr_scheme_kind = Pp.str -let cache_one_scheme kind (ind,const) = - let map = try Indmap.find ind !scheme_map with Not_found -> String.Map.empty in - scheme_map := Indmap.add ind (String.Map.add kind const map) !scheme_map - -let cache_scheme (_,(kind,l)) = - Array.iter (cache_one_scheme kind) l - -let subst_one_scheme subst (ind,const) = - (* Remark: const is a def: the result of substitution is a constant *) - (subst_ind subst ind,subst_constant subst const) - -let subst_scheme (subst,(kind,l)) = - (kind,Array.Smart.map (subst_one_scheme subst) l) - -let discharge_scheme (_,(kind,l)) = - Some (kind, l) - -let inScheme : string * (inductive * Constant.t) array -> obj = - declare_object @@ superglobal_object "SCHEME" - ~cache:cache_scheme - ~subst:(Some subst_scheme) - ~discharge:discharge_scheme - (**********************************************************************) (* The table of scheme building functions *) @@ -104,11 +77,6 @@ let declare_individual_scheme_object s ?(aux="") f = (**********************************************************************) (* Defining/retrieving schemes *) -let declare_scheme kind indcl = - Lib.add_anonymous_leaf (inScheme (kind,indcl)) - -let () = Declare.set_declare_scheme declare_scheme - let is_visible_name id = try ignore (Nametab.locate (Libnames.qualid_of_ident id)); true with Not_found -> false @@ -140,7 +108,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = | None -> add_suffix mib.mind_packets.(i).mind_typename suff in let role = Evd.Schema (ind, kind) in let const, neff = define mode role id c (Declareops.inductive_is_polymorphic mib) ctx in - declare_scheme kind [|ind,const|]; + DeclareScheme.declare_scheme kind [|ind,const|]; const, Evd.concat_side_effects neff eff let define_individual_scheme kind mode names (mind,i as ind) = @@ -162,7 +130,7 @@ let define_mutual_scheme_base kind suff f mode names mind = in let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in - declare_scheme kind schemes; + DeclareScheme.declare_scheme kind schemes; consts, eff let define_mutual_scheme kind mode names mind = @@ -172,7 +140,7 @@ let define_mutual_scheme kind mode names mind = define_mutual_scheme_base kind s f mode names mind let find_scheme_on_env_too kind ind = - let s = String.Map.find kind (Indmap.find ind !scheme_map) in + let s = DeclareScheme.lookup_scheme kind ind in s, Evd.empty_side_effects let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli index 17e9c7ef42..e9a792c264 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -30,7 +30,9 @@ type mutual_scheme_object_function = type individual_scheme_object_function = internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects -(** Main functions to register a scheme builder *) +(** Main functions to register a scheme builder. Note these functions + are not safe to be used by plugins as their effects won't be undone + on backtracking *) val declare_mutual_scheme_object : string -> ?aux:string -> mutual_scheme_object_function -> mutual scheme_kind diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index c5c7969a09..0c4e496650 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,3 +1,4 @@ +DeclareScheme Declare Proof_global Pfedit diff --git a/test-suite/bugs/closed/bug_4502.v b/test-suite/bugs/closed/bug_4502.v new file mode 100644 index 0000000000..f1dcae9773 --- /dev/null +++ b/test-suite/bugs/closed/bug_4502.v @@ -0,0 +1,17 @@ +Require Import FunInd. + +Set Universe Polymorphism. +Set Primitive Projections. +Set Implicit Arguments. +Set Strongly Strict Implicit. + +Function first_false (n : nat) (f : nat -> bool) : option nat := + match n with + | O => None + | S m => + match first_false m f with + | (Some _) as s => s + | None => if f m then None else Some m + end + end. +(* undefined universe *) diff --git a/test-suite/ltac2/term_notations.v b/test-suite/ltac2/term_notations.v new file mode 100644 index 0000000000..85eb858d4e --- /dev/null +++ b/test-suite/ltac2/term_notations.v @@ -0,0 +1,33 @@ +Require Import Ltac2.Ltac2. + +(* Preterms are not terms *) +Fail Notation "[ x ]" := $x. + +Section Foo. + +Notation "[ x ]" := ltac2:(Control.refine (fun _ => Constr.pretype x)). + +Goal [ True ]. +Proof. +constructor. +Qed. + +End Foo. + +Section Bar. + +(* Have fun with context capture *) +Notation "[ x ]" := ltac2:( + let c () := Constr.pretype x in + refine constr:(forall n : nat, n = ltac2:(Notations.exact0 true c)) +). + +Goal forall n : nat, [ n ]. +Proof. +reflexivity. +Qed. + +(* This fails currently, which is arguably a bug *) +Fail Goal [ n ]. + +End Bar. diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index 81c9763ccd..6c333121da 100644 --- a/test-suite/success/Fixpoint.v +++ b/test-suite/success/Fixpoint.v @@ -96,10 +96,25 @@ Section visibility. Let Fixpoint by_proof (n:nat) : True. Proof. exact I. Defined. + + Let Fixpoint foo (n:nat) : bool with bar (n:nat) : bool. + Proof. + - destruct n as [|n]. + + exact true. + + exact (bar n). + - destruct n as [|n]. + + exact false. + + exact (foo n). + Qed. + + Let Fixpoint bla (n:nat) : Type with bli (n:nat) : bool. + Admitted. + End visibility. Fail Check imm. Fail Check by_proof. +Check bla. Check bli. Module Import mod_local. Fixpoint imm_importable (n:nat) : True := I. diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v index 1e330b06d7..942cbe8916 100644 --- a/user-contrib/Ltac2/Constr.v +++ b/user-contrib/Ltac2/Constr.v @@ -77,3 +77,6 @@ Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "lt (** On a focused goal [Γ ⊢ A], [in_context id c tac] evaluates [tac] in a focused goal [Γ, id : c ⊢ ?X] and returns [fun (id : c) => t] where [t] is the proof built by the tactic. *) + +Ltac2 @ external pretype : preterm -> constr := "ltac2" "constr_pretype". +(** Pretype the provided preterm. Assumes the goal to be focussed. *) diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v index 88454ff2fb..6eed261554 100644 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v @@ -30,6 +30,7 @@ Ltac2 Type constructor. Ltac2 Type projection. Ltac2 Type pattern. Ltac2 Type constr. +Ltac2 Type preterm. Ltac2 Type message. Ltac2 Type exn := [ .. ]. diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 8a878bb0d0..9d4a3706f4 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -838,11 +838,11 @@ END GRAMMAR EXTEND Gram Pcoq.Constr.operconstr: LEVEL "0" [ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" -> - { let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in + { let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) } | test_ampersand_ident; "&"; id = Prim.ident -> { let tac = Tac2quote.of_exact_hyp ~loc (CAst.make ~loc id) in - let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in + let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) } | test_dollar_ident; "$"; id = Prim.ident -> { let id = Loc.tag ~loc id in @@ -873,7 +873,7 @@ let rules = [ Stop ++ Aentry test_ampersand_ident ++ Atoken (PKEYWORD "&") ++ Aentry Prim.ident, begin fun id _ _ loc -> let tac = Tac2quote.of_exact_hyp ~loc (CAst.make ~loc id) in - let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) ([], tac) in + let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) end ); @@ -882,7 +882,7 @@ let rules = [ Stop ++ Atoken (PIDENT (Some "ltac2")) ++ Atoken (PKEYWORD ":") ++ Atoken (PKEYWORD "(") ++ Aentry tac2expr ++ Atoken (PKEYWORD ")"), begin fun _ tac _ _ _ loc -> - let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) ([], tac) in + let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) end ) diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 34870345a5..0268e8f9ef 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -17,6 +17,28 @@ open Tac2expr open Tac2entries.Pltac open Proofview.Notations +let constr_flags = + let open Pretyping in + { + use_typeclasses = true; + solve_unification_constraints = true; + fail_evar = true; + expand_evars = true; + program_mode = false; + polymorphic = false; + } + +let open_constr_no_classes_flags = + let open Pretyping in + { + use_typeclasses = false; + solve_unification_constraints = true; + fail_evar = false; + expand_evars = true; + program_mode = false; + polymorphic = false; + } + (** Standard values *) module Value = Tac2ffi @@ -587,6 +609,30 @@ let () = define3 "constr_in_context" ident constr closure begin fun id t c -> throw err_notfocussed end +(** preterm -> constr *) +let () = define1 "constr_pretype" (repr_ext val_preterm) begin fun c -> + let open Pretyping in + let open Ltac_pretype in + let pretype env sigma = + Proofview.V82.wrap_exceptions begin fun () -> + (* For now there are no primitives to create preterms with a non-empty + closure. I do not know whether [closed_glob_constr] is really the type + we want but it does not hurt in the meantime. *) + let { closure; term } = c in + let vars = { + ltac_constrs = closure.typed; + ltac_uconstrs = closure.untyped; + ltac_idents = closure.idents; + ltac_genargs = Id.Map.empty; + } in + let flags = constr_flags in + let sigma, t = understand_ltac flags env sigma vars WithoutTypeConstraint term in + let t = Value.of_constr t in + Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT t + end in + pf_apply pretype +end + (** Patterns *) let empty_context = EConstr.mkMeta Constr_matching.special_meta @@ -976,28 +1022,6 @@ end (** ML types *) -let constr_flags () = - let open Pretyping in - { - use_typeclasses = true; - solve_unification_constraints = true; - fail_evar = true; - expand_evars = true; - program_mode = false; - polymorphic = false; - } - -let open_constr_no_classes_flags () = - let open Pretyping in - { - use_typeclasses = false; - solve_unification_constraints = true; - fail_evar = false; - expand_evars = true; - program_mode = false; - polymorphic = false; - } - (** Embed all Ltac2 data into Values *) let to_lvar ist = let open Glob_ops in @@ -1033,7 +1057,7 @@ let interp_constr flags ist c = let () = let intern = intern_constr in - let interp ist c = interp_constr (constr_flags ()) ist c in + let interp ist c = interp_constr constr_flags ist c in let print env c = str "constr:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in let obj = { @@ -1046,7 +1070,7 @@ let () = let () = let intern = intern_constr in - let interp ist c = interp_constr (open_constr_no_classes_flags ()) ist c in + let interp ist c = interp_constr open_constr_no_classes_flags ist c in let print env c = str "open_constr:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in let obj = { @@ -1092,6 +1116,27 @@ let () = define_ml_object Tac2quote.wit_pattern obj let () = + let interp _ c = + let open Ltac_pretype in + let closure = { + idents = Id.Map.empty; + typed = Id.Map.empty; + untyped = Id.Map.empty; + } in + let c = { closure; term = c } in + return (Value.of_ext val_preterm c) + in + let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in + let print env c = str "preterm:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in + let obj = { + ml_intern = (fun _ _ e -> Empty.abort e); + ml_interp = interp; + ml_subst = subst; + ml_print = print; + } in + define_ml_object Tac2quote.wit_preterm obj + +let () = let intern self ist ref = match ref.CAst.v with | Tac2qexpr.QHypothesis id -> GlbVal (GlobRef.VarRef id), gtypref t_reference @@ -1221,15 +1266,15 @@ let () = let () = let interp ist poly env sigma concl (ids, tac) = - (* Syntax prevents bound variables in constr quotations *) - let () = assert (List.is_empty ids) in + (* Syntax prevents bound notation variables in constr quotations *) + let () = assert (Id.Set.is_empty ids) in let ist = Tac2interp.get_env ist in let tac = Proofview.tclIGNORE (Tac2interp.interp ist tac) in let name, poly = Id.of_string "ltac2", poly in let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma concl tac in (EConstr.of_constr c, sigma) in - GlobEnv.register_constr_interp0 wit_ltac2 interp + GlobEnv.register_constr_interp0 wit_ltac2_constr interp let () = let interp ist poly env sigma concl id = @@ -1247,6 +1292,29 @@ let () = let pr_top _ = Genprint.TopPrinterBasic mt in Genprint.register_print0 wit_ltac2_quotation pr_raw pr_glb pr_top +let () = + let subs globs (ids, tac) = + (* Let-bind the notation terms inside the tactic *) + let fold id (c, _) (rem, accu) = + let c = GTacExt (Tac2quote.wit_preterm, c) in + let rem = Id.Set.remove id rem in + rem, (Name id, c) :: accu + in + let rem, bnd = Id.Map.fold fold globs (ids, []) in + let () = if not @@ Id.Set.is_empty rem then + (* FIXME: provide a reasonable middle-ground with the behaviour + introduced by 8d9b66b. We should be able to pass mere syntax to + term notation without facing the wrath of the internalization. *) + let plural = if Id.Set.cardinal rem <= 1 then " " else "s " in + CErrors.user_err (str "Missing notation term for variable" ++ str plural ++ + pr_sequence Id.print (Id.Set.elements rem) ++ + str ", probably an ill-typed expression") + in + let tac = if List.is_empty bnd then tac else GTacLet (false, bnd, tac) in + (Id.Set.empty, tac) + in + Genintern.register_ntn_subst0 wit_ltac2_constr subs + (** Ltac2 in Ltac1 *) let () = diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml index 963c3aa37f..959a912ad2 100644 --- a/user-contrib/Ltac2/tac2env.ml +++ b/user-contrib/Ltac2/tac2env.ml @@ -284,6 +284,7 @@ let ltac1_prefix = (** Generic arguments *) let wit_ltac2 = Genarg.make0 "ltac2:value" +let wit_ltac2_constr = Genarg.make0 "ltac2:in-constr" let wit_ltac2_quotation = Genarg.make0 "ltac2:quotation" let () = Geninterp.register_val0 wit_ltac2 None let () = Geninterp.register_val0 wit_ltac2_quotation None diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli index 2f4a49a0f5..1dfc3400a1 100644 --- a/user-contrib/Ltac2/tac2env.mli +++ b/user-contrib/Ltac2/tac2env.mli @@ -141,7 +141,13 @@ val ltac1_prefix : ModPath.t (** {5 Generic arguments} *) val wit_ltac2 : (Id.t CAst.t list * raw_tacexpr, Id.t list * glb_tacexpr, Util.Empty.t) genarg_type +(** Ltac2 quotations in Ltac1 code *) + +val wit_ltac2_constr : (raw_tacexpr, Id.Set.t * glb_tacexpr, Util.Empty.t) genarg_type +(** Ltac2 quotations in Gallina terms *) + val wit_ltac2_quotation : (Id.t Loc.located, Id.t, Util.Empty.t) genarg_type +(** Ltac2 quotations for variables "$x" in Gallina terms *) (** {5 Helper functions} *) diff --git a/user-contrib/Ltac2/tac2ffi.ml b/user-contrib/Ltac2/tac2ffi.ml index 0e6fb94095..7c9613f31b 100644 --- a/user-contrib/Ltac2/tac2ffi.ml +++ b/user-contrib/Ltac2/tac2ffi.ml @@ -89,6 +89,7 @@ let val_exn = Val.create "exn" let val_constr = Val.create "constr" let val_ident = Val.create "ident" let val_pattern = Val.create "pattern" +let val_preterm = Val.create "preterm" let val_pp = Val.create "pp" let val_sort = Val.create "sort" let val_cast = Val.create "cast" diff --git a/user-contrib/Ltac2/tac2ffi.mli b/user-contrib/Ltac2/tac2ffi.mli index 480eee51fc..d3c9596e8f 100644 --- a/user-contrib/Ltac2/tac2ffi.mli +++ b/user-contrib/Ltac2/tac2ffi.mli @@ -165,6 +165,7 @@ val valexpr : valexpr repr val val_constr : EConstr.t Val.tag val val_ident : Id.t Val.tag val val_pattern : Pattern.constr_pattern Val.tag +val val_preterm : Ltac_pretype.closed_glob_constr Val.tag val val_pp : Pp.t Val.tag val val_sort : ESorts.t Val.tag val val_cast : Constr.cast_kind Val.tag diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml index 5b3aa799a1..4e39b21c53 100644 --- a/user-contrib/Ltac2/tac2intern.ml +++ b/user-contrib/Ltac2/tac2intern.ml @@ -28,6 +28,7 @@ let t_int = coq_type "int" let t_string = coq_type "string" let t_constr = coq_type "constr" let t_ltac1 = ltac1_type "t" +let t_preterm = coq_type "preterm" (** Union find *) @@ -1511,7 +1512,7 @@ let () = let ids = List.map (fun { CAst.v = id } -> id) ids in let env = match Genintern.Store.get ist.extra ltac2_env with | None -> - (* Only happens when Ltac2 is called from a constr or ltac1 quotation *) + (* Only happens when Ltac2 is called from a toplevel ltac1 quotation *) let env = empty_env () in if !Ltac_plugin.Tacintern.strict_check then env else { env with env_str = false } @@ -1527,7 +1528,36 @@ let () = (ist, (ids, tac)) in Genintern.register_intern0 wit_ltac2 intern + +let () = + let open Genintern in + let intern ist tac = + let env = match Genintern.Store.get ist.extra ltac2_env with + | None -> + (* Only happens when Ltac2 is called from a constr quotation *) + let env = empty_env () in + if !Ltac_plugin.Tacintern.strict_check then env + else { env with env_str = false } + | Some env -> env + in + (* Special handling of notation variables *) + let fold id _ (ids, env) = + let () = assert (not @@ Id.Map.mem id env.env_var) in + let t = monomorphic (GTypRef (Other t_preterm, [])) in + let env = push_name (Name id) t env in + (Id.Set.add id ids, env) + in + let ntn_vars = ist.intern_sign.notation_variable_status in + let ids, env = Id.Map.fold fold ntn_vars (Id.Set.empty, env) in + let loc = tac.loc in + let (tac, t) = intern_rec env tac in + let () = check_elt_unit loc env t in + (ist, (ids, tac)) + in + Genintern.register_intern0 wit_ltac2_constr intern + let () = Genintern.register_subst0 wit_ltac2 (fun s (ids, e) -> ids, subst_expr s e) +let () = Genintern.register_subst0 wit_ltac2_constr (fun s (ids, e) -> ids, subst_expr s e) let () = let open Genintern in @@ -1540,6 +1570,12 @@ let () = else { env with env_str = false } | Some env -> env in + (* Special handling of notation variables *) + let () = + if Id.Map.mem id ist.intern_sign.notation_variable_status then + (* Always fail *) + unify ?loc env (GTypRef (Other t_preterm, [])) (GTypRef (Other t_constr, [])) + in let t = try Id.Map.find id env.env_var with Not_found -> diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml index 405c80fa9b..645b92c302 100644 --- a/user-contrib/Ltac2/tac2quote.ml +++ b/user-contrib/Ltac2/tac2quote.ml @@ -23,6 +23,7 @@ let wit_reference = Arg.create "reference" let wit_ident = Arg.create "ident" let wit_constr = Arg.create "constr" let wit_open_constr = Arg.create "open_constr" +let wit_preterm = Arg.create "preterm" let wit_ltac1 = Arg.create "ltac1" let wit_ltac1val = Arg.create "ltac1val" diff --git a/user-contrib/Ltac2/tac2quote.mli b/user-contrib/Ltac2/tac2quote.mli index da28e04df0..f1564cd443 100644 --- a/user-contrib/Ltac2/tac2quote.mli +++ b/user-contrib/Ltac2/tac2quote.mli @@ -97,6 +97,8 @@ val wit_constr : (Constrexpr.constr_expr, Glob_term.glob_constr) Arg.tag val wit_open_constr : (Constrexpr.constr_expr, Glob_term.glob_constr) Arg.tag +val wit_preterm : (Util.Empty.t, Glob_term.glob_constr) Arg.tag + val wit_ltac1 : (Id.t CAst.t list * Ltac_plugin.Tacexpr.raw_tactic_expr, Id.t list * Ltac_plugin.Tacexpr.glob_tactic_expr) Arg.tag (** Ltac1 AST quotation, seen as a 'tactic'. Its type is unit in Ltac2. *) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index efcb2635be..1387ca4675 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -418,19 +418,19 @@ GRAMMAR EXTEND Gram rec_definition: [ [ id_decl = ident_decl; bl = binders_fixannot; - rtype = type_cstr; + rtype = rec_type_cstr; body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notation -> { let binders, rec_order = bl in {fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations} } ] ] ; corec_definition: - [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr; + [ [ id_decl = ident_decl; binders = binders; rtype = rec_type_cstr; body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notation -> { {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations} } ]] ; - type_cstr: + rec_type_cstr: [ [ ":"; c=lconstr -> { c } | -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) } ] ] ; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 7010aa8c6d..cf322c52d0 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -17,15 +17,10 @@ open Pp open Names open Constr open Declareops -open Entries open Nameops open Pretyping -open Termops -open Reductionops -open Constrintern open Impargs -module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (* Support for terminators and proofs with an associated constant @@ -113,13 +108,6 @@ let by tac pf = (* Creating a lemma-like constant *) (************************************************************************) -let check_name_freshness locality {CAst.loc;v=id} : unit = - (* We check existence here: it's a bit late at Qed time *) - if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || - locality <> DeclareDef.Discharge && Nametab.exists_cci (Lib.make_path_except_section id) - then - user_err ?loc (Id.print id ++ str " already exists.") - let initialize_named_context_for_proof () = let sign = Global.named_context () in List.fold_right @@ -193,41 +181,6 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua | None -> p | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma -let start_lemma_com ~program_mode ~poly ~scope ~kind ?inference_hook ?hook thms = - let env0 = Global.env () in - let decl = fst (List.hd thms) in - let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in - let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) -> - let evd, (impls, ((env, ctx), imps)) = interp_context_evars ~program_mode env0 evd bl in - let evd, (t', imps') = interp_type_evars_impls ~program_mode ~impls env evd t in - let flags = { all_and_fail_flags with program_mode } in - let hook = inference_hook in - let evd = solve_remaining_evars ?hook flags env evd in - let ids = List.map RelDecl.get_name ctx in - check_name_freshness scope id; - (* XXX: The nf_evar is critical !! *) - evd, (id.CAst.v, - (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx), - (ids, imps @ imps')))) - evd thms in - let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in - let evd = Evd.minimize_universes evd in - (* XXX: This nf_evar is critical too!! We are normalizing twice if - you look at the previous lines... *) - let thms = List.map (fun (name, (typ, (args, impargs))) -> - { Recthm.name; typ = nf_evar evd typ; args; impargs} ) thms in - let () = - let open UState in - if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then - ignore (Evd.check_univ_decl ~poly evd udecl) - in - let evd = - if poly then evd - else (* We fix the variables to ensure they won't be lowered to Set *) - Evd.fix_undefined_variables evd - in - start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl - (************************************************************************) (* Commom constant saving path, for both Qed and Admitted *) (************************************************************************) @@ -258,17 +211,9 @@ let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Rect let open DeclareDef in (match scope with | Discharge -> - let impl = Glob_term.Explicit in - let univs = match univs with - | Polymorphic_entry (_, univs) -> - (* What is going on here? *) - Univ.ContextSet.of_context univs - | Monomorphic_entry univs -> univs - in - let () = Declare.declare_universe_context ~poly univs in - let c = Declare.SectionLocalAssum {typ=t_i; impl} in - let () = Declare.declare_variable ~name ~kind c in - GlobRef.VarRef name, impargs + (* Let Fixpoint + Admitted gets turned into axiom so scope is Global, + see finish_admitted *) + assert false | Global local -> let kind = Decls.(IsAssumption Conjectural) in let decl = Declare.ParameterEntry (None,(t_i,univs),None) in diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index fbf91b3ad4..e790c39022 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -110,17 +110,6 @@ val start_lemma_with_initialization val default_thm_id : Names.Id.t -(** Main [Lemma foo args : type.] command *) -val start_lemma_com - : program_mode:bool - -> poly:bool - -> scope:DeclareDef.locality - -> kind:Decls.logical_kind - -> ?inference_hook:Pretyping.inference_hook - -> ?hook:DeclareDef.Hook.t - -> Vernacexpr.proof_expr list - -> t - (** {4 Saving proofs} *) val save_lemma_admitted : lemma:t -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4ecd815dd2..684d8a3d90 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -465,29 +465,64 @@ let vernac_custom_entry ~module_local s = (***********) (* Gallina *) -let start_proof_and_print ~program_mode ~poly ?hook ~scope ~kind l = - let inference_hook = - if program_mode then - let hook env sigma ev = - let tac = !Obligations.default_tactic in - let evi = Evd.find sigma ev in - let evi = Evarutil.nf_evar_info sigma evi in - let env = Evd.evar_filtered_env evi in - try - let concl = evi.Evd.evar_concl in - if not (Evarutil.is_ground_env sigma env && - Evarutil.is_ground_term sigma concl) - then raise Exit; - let c, _, ctx = - Pfedit.build_by_tactic ~poly:false env (Evd.evar_universe_context sigma) concl tac - in Evd.set_universe_context sigma ctx, EConstr.of_constr c - with Logic_monad.TacticFailure e when Logic.catchable_exception e -> - user_err Pp.(str "The statement obligations could not be resolved \ - automatically, write a statement definition first.") - in Some hook - else None +let check_name_freshness locality {CAst.loc;v=id} : unit = + (* We check existence here: it's a bit late at Qed time *) + if Nametab.exists_cci (Lib.make_path id) || Termops.is_section_variable id || + locality <> DeclareDef.Discharge && Nametab.exists_cci (Lib.make_path_except_section id) + then + user_err ?loc (Id.print id ++ str " already exists.") + +let program_inference_hook env sigma ev = + let tac = !Obligations.default_tactic in + let evi = Evd.find sigma ev in + let evi = Evarutil.nf_evar_info sigma evi in + let env = Evd.evar_filtered_env evi in + try + let concl = evi.Evd.evar_concl in + if not (Evarutil.is_ground_env sigma env && + Evarutil.is_ground_term sigma concl) + then raise Exit; + let c, _, ctx = + Pfedit.build_by_tactic ~poly:false env (Evd.evar_universe_context sigma) concl tac + in Evd.set_universe_context sigma ctx, EConstr.of_constr c + with Logic_monad.TacticFailure e when Logic.catchable_exception e -> + user_err Pp.(str "The statement obligations could not be resolved \ + automatically, write a statement definition first.") + +let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = + let env0 = Global.env () in + let decl = fst (List.hd thms) in + let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in + let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) -> + let evd, (impls, ((env, ctx), imps)) = interp_context_evars ~program_mode env0 evd bl in + let evd, (t', imps') = interp_type_evars_impls ~program_mode ~impls env evd t in + let flags = Pretyping.{ all_and_fail_flags with program_mode } in + let inference_hook = if program_mode then Some program_inference_hook else None in + let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in + let ids = List.map Context.Rel.Declaration.get_name ctx in + check_name_freshness scope id; + (* XXX: The nf_evar is critical !! *) + evd, (id.CAst.v, + (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx), + (ids, imps @ imps')))) + evd thms in + let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in + let evd = Evd.minimize_universes evd in + (* XXX: This nf_evar is critical too!! We are normalizing twice if + you look at the previous lines... *) + let thms = List.map (fun (name, (typ, (args, impargs))) -> + { Recthm.name; typ = Evarutil.nf_evar evd typ; args; impargs} ) thms in + let () = + let open UState in + if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then + ignore (Evd.check_univ_decl ~poly evd udecl) + in + let evd = + if poly then evd + else (* We fix the variables to ensure they won't be lowered to Set *) + Evd.fix_undefined_variables evd in - start_lemma_com ~program_mode ?inference_hook ?hook ~poly ~scope ~kind l + start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl let vernac_definition_hook ~poly = let open Decls in function | Coercion -> @@ -522,7 +557,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let program_mode = atts.program in let poly = atts.polymorphic in let name = vernac_definition_name lid local in - start_proof_and_print ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?hook [(name, pl), (bl, t)] + start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?hook [(name, pl), (bl, t)] let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt = let open DefAttributes in @@ -545,7 +580,7 @@ let vernac_start_proof ~atts kind l = let scope = enforce_locality_exp atts.locality NoDischarge in if Dumpglob.dump () then List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; - start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) l + start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) l let vernac_end_proof ~lemma = let open Vernacexpr in function | Admitted -> |