From d12d696c21e73016581a53793eaa8c3bf4f00833 Mon Sep 17 00:00:00 2001 From: SimonBoulier Date: Thu, 19 Dec 2019 11:40:20 +0100 Subject: Update doc for non max implicit arguments --- doc/sphinx/language/gallina-extensions.rst | 85 ++++++++++++++++------ .../language/gallina-specification-language.rst | 2 + 2 files changed, 66 insertions(+), 21 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 510e271951..64864bb195 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1570,11 +1570,26 @@ inserted. In the second case, the function is considered to be implicitly applied to the implicit arguments it is waiting for: one says that the implicit argument is maximally inserted. -Each implicit argument can be declared to have to be inserted maximally or non -maximally. This can be governed argument per argument by the command -:cmd:`Arguments (implicits)` or globally by the :flag:`Maximal Implicit Insertion` flag. +Each implicit argument can be declared to be inserted maximally or non +maximally. In Coq, maximally inserted implicits are written between curly braces +"{ }" and non maximally inserted implicits are written in square brackets "[ ]". -.. seealso:: :ref:`displaying-implicit-args`. +.. seealso:: :flag:`Maximal Implicit Insertion` + +Trailing Implicit Arguments ++++++++++++++++++++++++++++ + +An implicit argument is considered trailing when all following arguments are declared +implicit. Trailing implicit arguments cannot be declared non maximally inserted, +otherwise they would never be inserted. + +.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. + + For instance: + + .. coqtop:: all fail + + Fail Definition double [n] := n + n. Casual use of implicit arguments @@ -1608,7 +1623,7 @@ Implicit Argument Binders In the first setting, one wants to explicitly give the implicit arguments of a declared object as part of its definition. To do this, one has to surround the bindings of implicit arguments by curly -braces: +braces or square braces: .. coqtop:: all @@ -1624,6 +1639,17 @@ absent in every situation but still be able to specify it if needed: Goal forall A, compose id id = id (A:=A). +For non maximally inserted implicit arguments, use square brackets: + +.. coqtop:: all + + Fixpoint map [A B : Type] (f : A -> B) (l : list A) : list B := + match l with + | nil => nil + | cons a t => cons (f a) (map f t) + end. + + Print Implicit map. The syntax is supported in all top-level definitions: :cmd:`Definition`, :cmd:`Fixpoint`, :cmd:`Lemma` and so on. For (co-)inductive datatype @@ -1728,14 +1754,6 @@ Declaring Implicit Arguments To know which are the implicit arguments of an object, use the command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`). -.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. - - For instance in - - .. coqtop:: all fail - - Arguments prod _ [_]. - Automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1811,7 +1829,7 @@ appear strictly in the body of the type, they are implicit. Mode for automatic declaration of implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +++++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Implicit Arguments @@ -1823,7 +1841,7 @@ Mode for automatic declaration of implicit arguments .. _controlling-strict-implicit-args: Controlling strict implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++ .. flag:: Strict Implicit @@ -1842,7 +1860,7 @@ Controlling strict implicit arguments .. _controlling-contextual-implicit-args: Controlling contextual implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++++++ .. flag:: Contextual Implicit @@ -1853,7 +1871,7 @@ Controlling contextual implicit arguments .. _controlling-rev-pattern-implicit-args: Controlling reversible-pattern implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Reversible Pattern Implicit @@ -1864,7 +1882,7 @@ Controlling reversible-pattern implicit arguments .. _controlling-insertion-implicit-args: Controlling the insertion of implicit arguments not followed by explicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Maximal Implicit Insertion @@ -1873,6 +1891,28 @@ Controlling the insertion of implicit arguments not followed by explicit argumen function is partially applied and the next argument of the function is an implicit one. +Combining manual declaration and automatic declaration +++++++++++++++++++++++++++++++++++++++++++++++++++++++ + +When some arguments are manually specified implicit with binders in a definition +and the automatic declaration mode in on, the manual implicits are added to the +automatic ones. + +In that case, and when the flag :flag:`Maximal Implicit Insertion` is set to off, +some trailing implicit arguments can be inferred to be non maximally inserted. In +this case, they are converted to maximally inserted ones. + +.. example:: + + .. coqtop:: all + + Set Implicit Arguments. + Axiom eq0_le0 : forall (n : nat) (x : n = 0), n <= 0. + Print Implicit eq0_le0. + Axiom eq0_le0' : forall (n : nat) {x : n = 0}, n <= 0. + Print Implicit eq0_le0'. + + .. _explicit-applications: Explicit applications @@ -2136,8 +2176,10 @@ Implicit generalization ~~~~~~~~~~~~~~~~~~~~~~~ .. index:: `{ } +.. index:: `[ ] .. index:: `( ) .. index:: `{! } +.. index:: `[! ] .. index:: `(! ) Implicit generalization is an automatic elaboration of a statement @@ -2145,11 +2187,12 @@ with free variables into a closed statement where these variables are quantified explicitly. It is activated for a binder by prefixing a \`, and for terms by -surrounding it with \`{ } or \`( ). +surrounding it with \`{ }, or \`[ ] or \`( ). Terms surrounded by \`{ } introduce their free variables as maximally -inserted implicit arguments, and terms surrounded by \`( ) introduce -them as explicit arguments. +inserted implicit arguments, terms surrounded by \`[ ] introduce them as +non maximally inserted implicit arguments and terms surrounded by \`( ) +introduce them as explicit arguments. Generalizing binders always introduce their free variables as maximally inserted implicit arguments. The binder itself introduces diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index d591718b17..09090ce89a 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -283,8 +283,10 @@ Binders | ( {+ @name } : @term ) | ( @name {? : @term } := @term ) | %{ {+ @name } {? : @term } %} + | [ {+ @name } {? : @term } ] | `( {+, @typeclass_constraint } ) | `%{ {+, @typeclass_constraint } %} + | `[ {+, @typeclass_constraint } ] | ' @pattern0 | ( @name : @term %| @term ) typeclass_constraint ::= {? ! } @term -- cgit v1.2.3 From 0f568166e37216a6e174e81757f6f2a2bc56fb4e Mon Sep 17 00:00:00 2001 From: SimonBoulier Date: Thu, 19 Dec 2019 13:40:36 +0100 Subject: Add changelog for non maximal implicit args --- .../02-specification-language/11235-non_maximal_implicit.rst | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 doc/changelog/02-specification-language/11235-non_maximal_implicit.rst (limited to 'doc') diff --git a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst new file mode 100644 index 0000000000..aa42ef0fee --- /dev/null +++ b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst @@ -0,0 +1,6 @@ +- **Added:** + Syntax for non maximal implicit arguments in toplevel definitions using + square brackets. The syntax is ``[x : A]``, ``[x]``, ```[A]`` + to be consistent with the command :cmd:`Arguments (implicits)`. + (`#11235 `_, + by SimonBoulier). -- cgit v1.2.3 From dd7f79809425543b8ac3ff2c2a2b8f36adf28af1 Mon Sep 17 00:00:00 2001 From: SimonBoulier Date: Mon, 6 Jan 2020 14:35:14 +0100 Subject: Non maximal implicits: entry in dev/doc/changes.md --- doc/changelog/02-specification-language/11235-non_maximal_implicit.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst index aa42ef0fee..d8ff1fec31 100644 --- a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst +++ b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst @@ -1,5 +1,5 @@ - **Added:** - Syntax for non maximal implicit arguments in toplevel definitions using + Syntax for non maximal implicit arguments in definitions and terms using square brackets. The syntax is ``[x : A]``, ``[x]``, ```[A]`` to be consistent with the command :cmd:`Arguments (implicits)`. (`#11235 `_, -- cgit v1.2.3 From 2c9d58c4680dd3c60dacf387a7ea457584bec42f Mon Sep 17 00:00:00 2001 From: SimonBoulier Date: Tue, 4 Feb 2020 16:06:29 +0100 Subject: Apply suggestions from Hugo Co-Authored-By: Hugo Herbelin --- doc/sphinx/language/gallina-extensions.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 64864bb195..b3ebb4d8df 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1571,8 +1571,8 @@ implicitly applied to the implicit arguments it is waiting for: one says that the implicit argument is maximally inserted. Each implicit argument can be declared to be inserted maximally or non -maximally. In Coq, maximally inserted implicits are written between curly braces -"{ }" and non maximally inserted implicits are written in square brackets "[ ]". +maximally. In Coq, maximally-inserted implicit arguments are written between curly braces +"{ }" and non-maximally-inserted implicit arguments are written in square brackets "[ ]". .. seealso:: :flag:`Maximal Implicit Insertion` @@ -1895,8 +1895,8 @@ Combining manual declaration and automatic declaration ++++++++++++++++++++++++++++++++++++++++++++++++++++++ When some arguments are manually specified implicit with binders in a definition -and the automatic declaration mode in on, the manual implicits are added to the -automatic ones. +and the automatic declaration mode in on, the manual implicit arguments are added to the +automatically declared ones. In that case, and when the flag :flag:`Maximal Implicit Insertion` is set to off, some trailing implicit arguments can be inferred to be non maximally inserted. In -- cgit v1.2.3