935 Similarly for the other binding modes. |
935 Similarly for the other binding modes. |
936 There are a few restrictions we need to impose: First, a body can only occur in |
936 There are a few restrictions we need to impose: First, a body can only occur in |
937 \emph{one} binding clause of a term constructor. |
937 \emph{one} binding clause of a term constructor. |
938 |
938 |
939 For binders we distinguish between \emph{shallow} and \emph{deep} binders. |
939 For binders we distinguish between \emph{shallow} and \emph{deep} binders. |
940 Shallow binders are of the form \isacommand{bind}\; {\it labels}\; |
940 Shallow binders are just labels. The |
941 \isacommand{in}\; {\it labels'} (similar for the other two modes). The |
941 restrictions we need to impose on them are that in case of |
942 restrictions we impose on shallow binders are that in case of |
942 \isacommand{bind\_set} and \isacommand{bind\_res} the labels must |
943 \isacommand{bind\_set} and \isacommand{bind\_res} the {\it labels} must |
|
944 either refer to atom types or to sets of atom types; in case of |
943 either refer to atom types or to sets of atom types; in case of |
945 \isacommand{bind} we allow labels to refer to atom types or lists of atom types. |
944 \isacommand{bind} the labels must refer to atom types or lists of atom types. |
946 Two examples for the use of shallow binders are the specification of |
945 Two examples for the use of shallow binders are the specification of |
947 lambda-terms, where a single name is bound, and type-schemes, where a finite |
946 lambda-terms, where a single name is bound, and type-schemes, where a finite |
948 set of names is bound: |
947 set of names is bound: |
949 |
948 |
950 \begin{center} |
949 \begin{center} |
1018 we cannot have more than one binding function for one binder. Consider for example the |
1017 we cannot have more than one binding function for one binder. Consider for example the |
1019 term-constructors: |
1018 term-constructors: |
1020 |
1019 |
1021 \begin{center} |
1020 \begin{center} |
1022 \begin{tabular}{ll} |
1021 \begin{tabular}{ll} |
1023 @{text "Foo\<^isub>1 p::pat q::pat t::trm"} & |
1022 @{text "Foo\<^isub>1 p::pat t::trm"} & |
1024 \isacommand{bind} @{text "bn(p) bn(q)"} \isacommand{in} @{text t}\\ |
1023 \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\ |
1025 @{text "Foo\<^isub>2 x::name p::pat t::trm"} & |
1024 @{text "Foo\<^isub>2 x::name p::pat t::trm"} & |
1026 \isacommand{bind} @{text "x bn(p)"} \isacommand{in} @{text t}\\ |
1025 \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}, ***\\ |
1027 \end{tabular} |
1026 \end{tabular} |
1028 \end{center} |
1027 \end{center} |
1029 |
1028 |
1030 \noindent |
1029 \noindent |
1031 In the first case the intention is to bind all atoms from the pattern @{text p} in @{text t} |
1030 In the first case the intention is to bind all atoms from the pattern @{text p} in @{text t} |