From 2cbc36c6ae4ca22e000dbb045c865f54a454aca3 Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser Date: Thu, 14 May 2020 17:08:20 +0200 Subject: Enable canonical `fun _ => _` projections. --- pretyping/evarconv.ml | 10 ++++++++++ pretyping/structures.ml | 2 ++ test-suite/output/Warnings.out | 5 +++-- test-suite/output/Warnings.v | 4 ++-- test-suite/success/CanonicalStructure.v | 32 ++++++++++++++++++++++++++++++++ theories/ssr/ssrbool.v | 3 ++- 6 files changed, 51 insertions(+), 5 deletions(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 5eb8a88698..d6ba84d0bf 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -232,7 +232,17 @@ let occur_rigidly flags env evd (evk,_) t = let check_conv_record env sigma (t1,sk1) (t2,sk2) = let open ValuePattern in let (proji, u), arg = Termops.global_app_of_constr sigma t1 in + let t2, sk2' = decompose_app_vect sigma (shrink_eta env t2) in + let sk2 = Stack.append_app sk2' sk2 in let (sigma, solution), sk2_effective = + let t2 = + let rec remove_lambda t2 = + match EConstr.kind sigma t2 with + | Lambda (_,_,t2) -> remove_lambda t2 + | Cast (t2,_,_) -> remove_lambda t2 + | App (t2,_) -> t2 + | _ -> t2 in + if Stack.is_empty sk2 then remove_lambda t2 else t2 in try match EConstr.kind sigma t2 with Prod (_,a,b) -> (* assert (l2=[]); *) diff --git a/pretyping/structures.ml b/pretyping/structures.ml index 3ef6e98373..145663d3b9 100644 --- a/pretyping/structures.ml +++ b/pretyping/structures.ml @@ -161,6 +161,7 @@ let rec of_constr env t = let patt, n, args = of_constr env f in patt, n, args @ Array.to_list vargs | Rel n -> Default_cs, Some n, [] + | Lambda (_, _, b) -> let patt, _, _ = of_constr env b in patt, None, [] | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] | Proj (p, c) -> Proj_cs (Names.Projection.repr p), None, [c] | Sort s -> Sort_cs (Sorts.family s), None, [] @@ -222,6 +223,7 @@ let compute_canonical_projections env ~warn (gref,ind) = let lpj = keep_true_projections lpj in let nenv = Termops.push_rels_assum sign env in List.fold_left2 (fun acc (spopt, canonical) t -> + let t = EConstr.Unsafe.to_constr (shrink_eta env (EConstr.of_constr t)) in if canonical then Option.cata (fun proji_sp -> diff --git a/test-suite/output/Warnings.out b/test-suite/output/Warnings.out index a70f8ca45a..23119bab97 100644 --- a/test-suite/output/Warnings.out +++ b/test-suite/output/Warnings.out @@ -1,3 +1,4 @@ File "stdin", line 4, characters 0-22: -Warning: Projection value has no head constant: fun x : B => x in canonical -instance a of b, ignoring it. [projection-no-head-constant,typechecker] +Warning: Projection value has no head constant: forall x : nat, x > 0 in +canonical instance a of b, ignoring it. +[projection-no-head-constant,typechecker] diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v index 7465442cab..ce92bcbbb2 100644 --- a/test-suite/output/Warnings.v +++ b/test-suite/output/Warnings.v @@ -1,5 +1,5 @@ (* Term in warning was not printed in the right environment at some time *) -Record A := { B:Type; b:B->B }. -Definition a B := {| B:=B; b:=fun x => x |}. +Record A := { B:Type; b:Prop }. +Definition a B := {| B:=B; b:=forall x, x > 0 |}. Canonical Structure a. diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v index 88702a6e80..a833dd0bd6 100644 --- a/test-suite/success/CanonicalStructure.v +++ b/test-suite/success/CanonicalStructure.v @@ -70,3 +70,35 @@ Section W. Check (refl_equal _ : l _ = x2). End W. Fail Check (refl_equal _ : l _ = x2). + +(* Lambda keys *) +Section L1. + Structure cs_lambda := { cs_lambda_key : nat -> nat }. + #[local] Canonical Structure cs_lambda_func := + {| cs_lambda_key := fun x => x + 1 |}. + Check (refl_equal _ : cs_lambda_key _ = fun _ => _ + _). +End L1. + +Section L2. + #[local] Canonical Structure cs_lambda_func2 := + {| cs_lambda_key := fun x => 1 + x |}. + Check (refl_equal _ : cs_lambda_key _ = fun x => 1 + x). +End L2. + +Section L3. + #[local] Canonical Structure cs_lambda_func3 := + {| cs_lambda_key := fun x => 1 + x |}. + Check (refl_equal _ : cs_lambda_key _ = Nat.add 1). +End L3. + +Section L4. + #[local] Canonical Structure cs_lambda_func4 := + {| cs_lambda_key := Nat.add 1 |}. + Check (refl_equal _ : cs_lambda_key _ = Nat.add 1). +End L4. + +Section L5. + #[local] Canonical Structure cs_lambda_func5 := + {| cs_lambda_key := Nat.add 1 |}. + Check (refl_equal _ : cs_lambda_key _ = fun x => 1 + x). +End L5. diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index d8eb005ab2..72e6e757d3 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -297,7 +297,6 @@ Require Import ssreflect ssrfun. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Set Warnings "-projection-no-head-constant". Notation reflect := Bool.reflect. Notation ReflectT := Bool.ReflectT. @@ -1227,7 +1226,9 @@ Definition clone_pred T U := Notation "[ 'predType' 'of' T ]" := (@clone_pred _ T _ id _ id) : form_scope. Canonical predPredType T := PredType (@id (pred T)). +Set Warnings "-redundant-canonical-projection". Canonical boolfunPredType T := PredType (@id (T -> bool)). +Set Warnings "redundant-canonical-projection". (** The type of abstract collective predicates. While {pred T} is contertible to pred T, it presents the pred_sort coercion -- cgit v1.2.3 From 9b35db9c7eb0cbc8e27c67f2ba2783fdd28ba247 Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser Date: Fri, 15 May 2020 11:44:29 +0200 Subject: Extend Canonical Structure documentation. This commit adds a more detailed explanation of what kinds of terms are allowed in fields of a canonical instance, how the fields are used as keys for canonical extension, what terms are considered overlapping, and how Coq reacts to overlapping fields. --- doc/sphinx/language/extensions/canonical.rst | 52 +++++++++++++++++++++++++--- 1 file changed, 47 insertions(+), 5 deletions(-) diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index fbba6c30b8..e3b014d8d5 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -41,12 +41,54 @@ in :ref:`canonicalstructures`; here only a simple example is given. This command supports the :attr:`local` attribute. When used, the structure is canonical only within the :cmd:`Section` containing it. - Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the - structure :g:`struct` of which the fields are |x_1|, …, |x_n|. - Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be + :token:`qualid` (in :token:`reference`) denotes an object :n:`(Build_struct c__1 … c__n)` in the + structure :g:`struct` for which the fields are :n:`x__1, …, x__n`. + Then, each time an equation of the form :n:`(x__i _)` |eq_beta_delta_iota_zeta| :n:`c__i` has to be solved during the type checking process, :token:`qualid` is used as a solution. - Otherwise said, :token:`qualid` is canonically used to extend the field |c_i| - into a complete structure built on |c_i|. + Otherwise said, :token:`qualid` is canonically used to extend the field :n:`x__i` + into a complete structure built on :n:`c__i` when :n:`c__i` unifies with :n:`(x__i _)`. + + The following kinds of terms are supported for the fields :n:`c__i` of :token:`qualid`: + + * :term:`Constants ` and section variables of an active section, + applied to zero or more arguments. + * :token:`sort`\s. + * Literal functions: `fun … => …`. + * Literal, non-dependent function types, i.e. implications: `… -> …`. + * Variables bound in :token:`qualid`. + + Only the head symbol of an existing instance's field :n:`c__i` + is considered when searching for a canonical extension. + We call this head symbol the *key* and we say ":token:`qualid` *keys* the field :n:`x__i` to :n:`k`" when :n:`c__i`'s + head symbol is :n:`k`. + Keys are the only piece of information that is used for canonical extension. + The keys corresponding to the kinds of terms listed above are: + + * For constants and section variables, potentially applied to arguments: + the constant or variable itself, disregarding any arguments. + * For sorts: the sort itself. + * For literal functions: skip the abstractions and use the key of the body. + * For literal functions types: a disembodied implication key denoted `_ -> _`, disregarding both its + domain and codomain. + * For variables bound in :token:`qualid`: a catch-all key denoted `_`. + + This means that, for example, `(some_constant x1)` and `(some_constant (other_constant y1 y2) x2)` + are not distinct keys. + + Variables bound in :token:`qualid` match any term for the purpose of canonical extension. + This has two major consequences for a field :n:`c__i` keyed to a variable of :token:`qualid`: + + 1. Unless another key—and, thus, instance—matches :n:`c__i`, the instance will always be considered by + unification. + 2. :n:`c__i` will be considered overlapping not distinct from any other canonical instance + that keys :n:`x__i` to one of its own variables. + + A record field :n:`x__i` can only be keyed once to each key. + Coq prints a warning when :token:`qualid` keys :n:`x__i` to a term + whose head symbol is already keyed by an existing canonical instance. + In this case, Coq will not register that :token:`qualid` as a canonical + extension. + (The remaining fields of the instance can still be used for canonical extension.) Canonical structures are particularly useful when mixed with coercions and strict implicit arguments. -- cgit v1.2.3 From 82910bed2fccee7d1f4814e3339fbae374980e68 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 2 Apr 2021 14:07:39 +0200 Subject: Add changelog --- doc/changelog/12-misc/14041-cs_lambda.rst | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 doc/changelog/12-misc/14041-cs_lambda.rst diff --git a/doc/changelog/12-misc/14041-cs_lambda.rst b/doc/changelog/12-misc/14041-cs_lambda.rst new file mode 100644 index 0000000000..872b1f09eb --- /dev/null +++ b/doc/changelog/12-misc/14041-cs_lambda.rst @@ -0,0 +1,6 @@ +- **Added:** + Enable canonical `fun _ => _` projections, + see :ref:`canonicalstructures` for details. + (`#14041 `_, + by Jan-Oliver Kaiser and Pierre Roux, + reviewed by Cyril Cohen and Enrico Tassi). -- cgit v1.2.3