From 4f71e81915a038c8e4d7920822c681c65d500ff2 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 13 May 2020 19:55:10 +0200 Subject: Add match to new file on Variants. --- doc/sphinx/language/core/variants.rst | 144 +++++++++++++++++++++ .../language/gallina-specification-language.rst | 144 --------------------- 2 files changed, 144 insertions(+), 144 deletions(-) create mode 100644 doc/sphinx/language/core/variants.rst delete mode 100644 doc/sphinx/language/gallina-specification-language.rst (limited to 'doc') diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst new file mode 100644 index 0000000000..d9e2c07951 --- /dev/null +++ b/doc/sphinx/language/core/variants.rst @@ -0,0 +1,144 @@ +.. index:: match ... with ... + +Definition by cases: match +-------------------------- + +.. insertprodn term_match pattern0 + +.. prodn:: + term_match ::= match {+, @case_item } {? return @term100 } with {? %| } {*| @eqn } end + case_item ::= @term100 {? as @name } {? in @pattern } + eqn ::= {+| {+, @pattern } } => @term + pattern ::= @pattern10 : @term + | @pattern10 + pattern10 ::= @pattern1 as @name + | @pattern1 {* @pattern1 } + | @ @qualid {* @pattern1 } + pattern1 ::= @pattern0 % @scope_key + | @pattern0 + pattern0 ::= @qualid + | %{%| {* @qualid := @pattern } %|%} + | _ + | ( {+| @pattern } ) + | @numeral + | @string + +Objects of inductive types can be destructured by a case-analysis +construction called *pattern matching* expression. A pattern matching +expression is used to analyze the structure of an inductive object and +to apply specific treatments accordingly. + +This paragraph describes the basic form of pattern matching. See +Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description +of the general form. The basic form of pattern matching is characterized +by a single :n:`@case_item` expression, an :n:`@eqn` restricted to a +single :n:`@pattern` and :n:`@pattern` restricted to the form +:n:`@qualid {* @ident}`. + +The expression +:n:`match @term {? return @term100 } with {+| @pattern__i => @term__i } end` denotes a +*pattern matching* over the term :n:`@term` (expected to be +of an inductive type :math:`I`). The :n:`@term__i` +are the *branches* of the pattern matching +expression. Each :n:`@pattern__i` has the form :n:`@qualid @ident` +where :n:`@qualid` must denote a constructor. There should be +exactly one branch for every constructor of :math:`I`. + +The :n:`return @term100` clause gives the type returned by the whole match +expression. There are several cases. In the *non dependent* case, all +branches have the same type, and the :n:`return @term100` specifies that type. +In this case, :n:`return @term100` can usually be omitted as it can be +inferred from the type of the branches [1]_. + +In the *dependent* case, there are three subcases. In the first subcase, +the type in each branch may depend on the exact value being matched in +the branch. In this case, the whole pattern matching itself depends on +the term being matched. This dependency of the term being matched in the +return type is expressed with an :n:`@ident` clause where :n:`@ident` +is dependent in the return type. For instance, in the following example: + +.. coqtop:: in + + Inductive bool : Type := true : bool | false : bool. + Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : eq A x x. + Inductive or (A:Prop) (B:Prop) : Prop := + | or_introl : A -> or A B + | or_intror : B -> or A B. + + Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := + match b as x return or (eq bool x true) (eq bool x false) with + | true => or_introl (eq bool true true) (eq bool true false) (eq_refl bool true) + | false => or_intror (eq bool false true) (eq bool false false) (eq_refl bool false) + end. + +the branches have respective types ":g:`or (eq bool true true) (eq bool true false)`" +and ":g:`or (eq bool false true) (eq bool false false)`" while the whole +pattern matching expression has type ":g:`or (eq bool b true) (eq bool b false)`", +the identifier :g:`b` being used to represent the dependency. + +.. note:: + + When the term being matched is a variable, the ``as`` clause can be + omitted and the term being matched can serve itself as binding name in + the return type. For instance, the following alternative definition is + accepted and has the same meaning as the previous one. + + .. coqtop:: none + + Reset bool_case. + + .. coqtop:: in + + Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := + match b return or (eq bool b true) (eq bool b false) with + | true => or_introl (eq bool true true) (eq bool true false) (eq_refl bool true) + | false => or_intror (eq bool false true) (eq bool false false) (eq_refl bool false) + end. + +The second subcase is only relevant for annotated inductive types such +as the equality predicate (see Section :ref:`coq-equality`), +the order predicate on natural numbers or the type of lists of a given +length (see Section :ref:`matching-dependent`). In this configuration, the +type of each branch can depend on the type dependencies specific to the +branch and the whole pattern matching expression has a type determined +by the specific dependencies in the type of the term being matched. This +dependency of the return type in the annotations of the inductive type +is expressed with a clause in the form +:n:`in @qualid {+ _ } {+ @pattern }`, where + +- :n:`@qualid` is the inductive type of the term being matched; + +- the holes :n:`_` match the parameters of the inductive type: the + return type is not dependent on them. + +- each :n:`@pattern` matches the annotations of the + inductive type: the return type is dependent on them + +- in the basic case which we describe below, each :n:`@pattern` + is a name :n:`@ident`; see :ref:`match-in-patterns` for the + general case + +For instance, in the following example: + +.. coqtop:: in + + Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x := + match H in eq _ _ z return eq A z x with + | eq_refl _ _ => eq_refl A x + end. + +the type of the branch is :g:`eq A x x` because the third argument of +:g:`eq` is :g:`x` in the type of the pattern :g:`eq_refl`. On the contrary, the +type of the whole pattern matching expression has type :g:`eq A y x` because the +third argument of eq is y in the type of H. This dependency of the case analysis +in the third argument of :g:`eq` is expressed by the identifier :g:`z` in the +return type. + +Finally, the third subcase is a combination of the first and second +subcase. In particular, it only applies to pattern matching on terms in +a type with annotations. For this third subcase, both the clauses ``as`` and +``in`` are available. + +There are specific notations for case analysis on types with one or two +constructors: ``if … then … else …`` and ``let (…,…) := … in …`` (see +Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`). diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst deleted file mode 100644 index d9e2c07951..0000000000 --- a/doc/sphinx/language/gallina-specification-language.rst +++ /dev/null @@ -1,144 +0,0 @@ -.. index:: match ... with ... - -Definition by cases: match --------------------------- - -.. insertprodn term_match pattern0 - -.. prodn:: - term_match ::= match {+, @case_item } {? return @term100 } with {? %| } {*| @eqn } end - case_item ::= @term100 {? as @name } {? in @pattern } - eqn ::= {+| {+, @pattern } } => @term - pattern ::= @pattern10 : @term - | @pattern10 - pattern10 ::= @pattern1 as @name - | @pattern1 {* @pattern1 } - | @ @qualid {* @pattern1 } - pattern1 ::= @pattern0 % @scope_key - | @pattern0 - pattern0 ::= @qualid - | %{%| {* @qualid := @pattern } %|%} - | _ - | ( {+| @pattern } ) - | @numeral - | @string - -Objects of inductive types can be destructured by a case-analysis -construction called *pattern matching* expression. A pattern matching -expression is used to analyze the structure of an inductive object and -to apply specific treatments accordingly. - -This paragraph describes the basic form of pattern matching. See -Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description -of the general form. The basic form of pattern matching is characterized -by a single :n:`@case_item` expression, an :n:`@eqn` restricted to a -single :n:`@pattern` and :n:`@pattern` restricted to the form -:n:`@qualid {* @ident}`. - -The expression -:n:`match @term {? return @term100 } with {+| @pattern__i => @term__i } end` denotes a -*pattern matching* over the term :n:`@term` (expected to be -of an inductive type :math:`I`). The :n:`@term__i` -are the *branches* of the pattern matching -expression. Each :n:`@pattern__i` has the form :n:`@qualid @ident` -where :n:`@qualid` must denote a constructor. There should be -exactly one branch for every constructor of :math:`I`. - -The :n:`return @term100` clause gives the type returned by the whole match -expression. There are several cases. In the *non dependent* case, all -branches have the same type, and the :n:`return @term100` specifies that type. -In this case, :n:`return @term100` can usually be omitted as it can be -inferred from the type of the branches [1]_. - -In the *dependent* case, there are three subcases. In the first subcase, -the type in each branch may depend on the exact value being matched in -the branch. In this case, the whole pattern matching itself depends on -the term being matched. This dependency of the term being matched in the -return type is expressed with an :n:`@ident` clause where :n:`@ident` -is dependent in the return type. For instance, in the following example: - -.. coqtop:: in - - Inductive bool : Type := true : bool | false : bool. - Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : eq A x x. - Inductive or (A:Prop) (B:Prop) : Prop := - | or_introl : A -> or A B - | or_intror : B -> or A B. - - Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := - match b as x return or (eq bool x true) (eq bool x false) with - | true => or_introl (eq bool true true) (eq bool true false) (eq_refl bool true) - | false => or_intror (eq bool false true) (eq bool false false) (eq_refl bool false) - end. - -the branches have respective types ":g:`or (eq bool true true) (eq bool true false)`" -and ":g:`or (eq bool false true) (eq bool false false)`" while the whole -pattern matching expression has type ":g:`or (eq bool b true) (eq bool b false)`", -the identifier :g:`b` being used to represent the dependency. - -.. note:: - - When the term being matched is a variable, the ``as`` clause can be - omitted and the term being matched can serve itself as binding name in - the return type. For instance, the following alternative definition is - accepted and has the same meaning as the previous one. - - .. coqtop:: none - - Reset bool_case. - - .. coqtop:: in - - Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := - match b return or (eq bool b true) (eq bool b false) with - | true => or_introl (eq bool true true) (eq bool true false) (eq_refl bool true) - | false => or_intror (eq bool false true) (eq bool false false) (eq_refl bool false) - end. - -The second subcase is only relevant for annotated inductive types such -as the equality predicate (see Section :ref:`coq-equality`), -the order predicate on natural numbers or the type of lists of a given -length (see Section :ref:`matching-dependent`). In this configuration, the -type of each branch can depend on the type dependencies specific to the -branch and the whole pattern matching expression has a type determined -by the specific dependencies in the type of the term being matched. This -dependency of the return type in the annotations of the inductive type -is expressed with a clause in the form -:n:`in @qualid {+ _ } {+ @pattern }`, where - -- :n:`@qualid` is the inductive type of the term being matched; - -- the holes :n:`_` match the parameters of the inductive type: the - return type is not dependent on them. - -- each :n:`@pattern` matches the annotations of the - inductive type: the return type is dependent on them - -- in the basic case which we describe below, each :n:`@pattern` - is a name :n:`@ident`; see :ref:`match-in-patterns` for the - general case - -For instance, in the following example: - -.. coqtop:: in - - Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x := - match H in eq _ _ z return eq A z x with - | eq_refl _ _ => eq_refl A x - end. - -the type of the branch is :g:`eq A x x` because the third argument of -:g:`eq` is :g:`x` in the type of the pattern :g:`eq_refl`. On the contrary, the -type of the whole pattern matching expression has type :g:`eq A y x` because the -third argument of eq is y in the type of H. This dependency of the case analysis -in the third argument of :g:`eq` is expressed by the identifier :g:`z` in the -return type. - -Finally, the third subcase is a combination of the first and second -subcase. In particular, it only applies to pattern matching on terms in -a type with annotations. For this third subcase, both the clauses ``as`` and -``in`` are available. - -There are specific notations for case analysis on types with one or two -constructors: ``if … then … else …`` and ``let (…,…) := … in …`` (see -Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`). -- cgit v1.2.3